Skip to content

Commit

Permalink
COnfig Tool: Begin JSON loading work, ENV optionally hides fields.
Browse files Browse the repository at this point in the history
  • Loading branch information
Yiannis128 committed Feb 15, 2024
1 parent ed28fba commit 35ab87f
Show file tree
Hide file tree
Showing 7 changed files with 106 additions and 19 deletions.
3 changes: 3 additions & 0 deletions esbmc_ai_config/contexts/env_menu.py
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ def _get_menu_items(self) -> list[str | urwid.Widget]:
initial_value=str(ConfigManager.env_config.values[field.name]),
)
for field in ConfigManager.env_config.fields
if field.show_in_config
]
return choices

Expand All @@ -47,6 +48,7 @@ def build_ui(self) -> urwid.Widget:

def _on_value_submit(self, title: str, value: str, ok_pressed: bool) -> None:
if ok_pressed:
# Find the correct field.
field: EnvConfigField
for i in ConfigManager.env_config.fields:
if i.name == title:
Expand All @@ -55,5 +57,6 @@ def _on_value_submit(self, title: str, value: str, ok_pressed: bool) -> None:
else:
return

# Cast to the correct type.
ConfigManager.env_config.values[title] = type(field.default_value)(value)
self.widget = self.build_ui()
15 changes: 9 additions & 6 deletions esbmc_ai_config/contexts/esbmc_menu/esbmc_manage.py
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,16 @@ class ESBMCManage(Context):
license_url: str = "https://raw.githubusercontent.com/esbmc/esbmc/master/COPYING"

def __init__(self) -> None:
response: requests.Response = requests.get(ESBMCManage.license_url)
if response.status_code == status_codes.ok:
self.license: str = response.text
if self.license_accepted:
self.license: str = ""
else:
self.license: str = (
f"Couldn't get the license: status code: {response.status_code}"
)
response: requests.Response = requests.get(ESBMCManage.license_url)
if response.status_code == status_codes.ok:
self.license: str = response.text
else:
self.license: str = (
f"Couldn't get the license: status code: {response.status_code}"
)

super().__init__(self.build_ui())

Expand Down
3 changes: 1 addition & 2 deletions esbmc_ai_config/contexts/save_menu.py
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,7 @@ def _on_cancel(self, button) -> None:
def _on_ok(self, button) -> None:
ContextManager.pop_context()
ConfigManager.env_config.save()
# TODO
# ConfigManager.json_config.save()
ConfigManager.json_config.save()
ContextManager.push_context(
DialogContext(
"Success",
Expand Down
2 changes: 1 addition & 1 deletion esbmc_ai_config/models/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

from .config_manager import ConfigManager
from .env_config_loader import EnvConfigField, EnvConfigLoader
from .json_config_loader import JsonConfigField, JsonConfigLoader
from .json_config_loader import JsonConfigNode, JsonConfigLoader

__all__ = [
"ConfigManager",
Expand Down
3 changes: 1 addition & 2 deletions esbmc_ai_config/models/config_manager.py
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,7 @@ def init(
cls, env_path: Optional[str] = None, config_path: Optional[str] = None
) -> None:
cls.load_env(env_path)
# TODO
# cls.load_json(config_path)
cls.load_json(config_path)

@classmethod
def load_json(cls, file_path: Optional[str] = None) -> None:
Expand Down
3 changes: 3 additions & 0 deletions esbmc_ai_config/models/env_config_loader.py
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ class EnvConfigField:
is_optional: bool = False
"""Will not load the config if the value is not specified by the user. If
true will assign default_value."""
show_in_config: bool = True
"""Show in config tool UI."""


class EnvConfigLoader(ConfigLoader):
Expand All @@ -36,6 +38,7 @@ def __init__(
"ESBMC_LICENSE_AGREEMENT",
default_value=False,
is_optional=True,
show_in_config=False,
),
],
create_missing_fields: bool = False,
Expand Down
96 changes: 88 additions & 8 deletions esbmc_ai_config/models/json_config_loader.py
Original file line number Diff line number Diff line change
@@ -1,35 +1,86 @@
# Author: Yiannis Charalambous

import json
from dataclasses import dataclass
from typing import Any
from typing_extensions import override

from esbmc_ai_config.models.config_loader import ConfigLoader

__ALLOWED_ENV_TYPES = bool | float | int | str
__ALLOWED_JSON_TYPES = bool | float | int | str | list | dict


@dataclass
class JsonConfigField:
name: str
default_value: "__ALLOWED_ENV_TYPES" = ""
class JsonConfigNode:
default_value: "__ALLOWED_JSON_TYPES" = ""
value: "__ALLOWED_JSON_TYPES" = ""
"""The value in the config. If type does not match the `default_value` type and the
`create_missing_fields` is set to `True`, then the `default_value` will be used."""
is_optional: bool = False
"""Will not load the config if the value is not specified by the user. If
true will assign default_value."""
show_in_config: bool = True
"""Show this field in the config tool UI."""

def __getitem__(self, subscript):
"""Allow indexing the default_values if they are a list or a dict.
Can accept an int for default_values that are list or dict.
Can accept a str for default_values that are dict."""
# NOTE TestMe
if isinstance(subscript, int) and isinstance(self.default_value, list):
# Using list and int indexing
return self.default_value[subscript]
elif isinstance(subscript, str) and isinstance(self.default_value, dict):
# Using str and dictionary indexing
return self.default_value[subscript]
raise IndexError(
f"Invalid type of subscript: {type(subscript)}: type of value: {type(self.default_value)}"
)

class JsonConfigLoader(ConfigLoader):
autogenerated_string: str = "# Generated by ESBMC-AI config tool."

class JsonConfigLoader(ConfigLoader):
def __init__(
self,
file_path: str = "~/.config/esbmc-ai.json",
fields: JsonConfigField = JsonConfigField(""), # FIXME
root_node: JsonConfigNode = JsonConfigNode(
default_value={
"esbmc_path": JsonConfigNode("~/.local/bin/esbmc"),
"ai_model": JsonConfigNode("gpt-3.5-turbo-16k"),
"ai_custom": JsonConfigNode({}),
"allow_successful": JsonConfigNode(True),
"esbmc_params": JsonConfigNode(
[
"--interval-analysis",
"--goto-unwind",
"--unlimited-goto-unwind",
"--k-induction",
"--state-hashing",
"--add-symex-value-sets",
"--k-step",
"2",
"--floatbv",
"--unlimited-k-steps",
"--memory-leak-check",
"--context-bound",
"2",
]
),
"consecutive_prompt_delay": JsonConfigNode(20),
"temp_auto_clean": JsonConfigNode(True),
"temp_file_dir": JsonConfigNode("~/.cache/esbmc-ai"),
"loading_hints": JsonConfigNode(True),
# TODO Finish fields
}
),
create_missing_fields: bool = False,
) -> None:
assert file_path.endswith(
".json"
), f"{self.file_path} is not a valid json file."

self.root_node: JsonConfigNode = root_node
self.values: dict = {}

super().__init__(
file_path=file_path,
create_missing_fields=create_missing_fields,
Expand All @@ -45,4 +96,33 @@ def _create_default_file(self) -> None:

@override
def _read_fields(self, create_missing_fields: bool = False) -> None:
raise NotImplementedError()
"""Parses the JSON config and loads all the values recursively. The self.values should
map directly to how the self.node values are laid out.
Arg:
create_missing_field: bool - Will not give an error when an invalid/missing field
is encountered, will instead initialize it to the default value."""
self.json_content: dict = json.loads(self.content)

def init_node_value(node: JsonConfigNode, json_node: "__ALLOWED_JSON_TYPES"):
# Check if the value and default_value match type
if type(json_node) is not type(node.default_value):
# Initialize with default_value
node.value = node.default_value
elif type(node.default_value) is dict[str, JsonConfigNode]:
assert isinstance(json_node, dict)
# Init children
for child_key, child_node in node.default_value:
assert isinstance(child_key, str)
assert isinstance(child_node, JsonConfigNode)
init_node_value(child_node, json_node[child_key])
elif isinstance(node.default_value, list):
assert isinstance(json_node, list)
node.value = json_node
else:
assert type(json_node) is type(node.default_value)
node.value = json_node

init_node_value(self.root_node, self.json_content)

raise Exception(self.root_node.value)

0 comments on commit 35ab87f

Please sign in to comment.