From 6603ed872feaf2723abddde5b03155a97af42675 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Fri, 19 Jul 2024 18:23:47 -0500 Subject: [PATCH] Add option to omit enum constraints (#687) * Add option to omit enum constraints, to allow duplicate enums in different parts of codebase * Set Version: 0.1.350 * Remove extra find_enums call * Set Version: 0.1.351 * Remove extra find_enums call * Set Version: 0.1.353 * Set Version: 0.1.356 * Invert option * Set Version: 0.1.359 * Fix inversion of option * Update src/kontrol/foundry.py Co-authored-by: Palina Tolmach * Set Version: 0.1.360 * Update contracts.k.expected * Fix test, fix dict lookup crash * Fix option not being set in build step in tests --------- Co-authored-by: devops Co-authored-by: Palina Tolmach --- src/kontrol/__main__.py | 60 ++++++++++++++++------- src/kontrol/cli.py | 7 +++ src/kontrol/foundry.py | 10 +++- src/kontrol/options.py | 2 + src/kontrol/prove.py | 19 ++++--- src/kontrol/solc_to_k.py | 34 ++++++++----- src/tests/integration/conftest.py | 7 +-- src/tests/integration/test_kontrol_cse.py | 1 + 8 files changed, 97 insertions(+), 43 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 17380f6df..dec41412d 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -90,9 +90,19 @@ def _ignore_arg(args: dict[str, Any], arg: str, cli_option: str) -> None: args.pop(arg) -def _load_foundry(foundry_root: Path, bug_report: BugReport | None = None, use_hex_encoding: bool = False) -> Foundry: +def _load_foundry( + foundry_root: Path, + bug_report: BugReport | None = None, + use_hex_encoding: bool = False, + add_enum_constraints: bool = False, +) -> Foundry: try: - foundry = Foundry(foundry_root=foundry_root, bug_report=bug_report, use_hex_encoding=use_hex_encoding) + foundry = Foundry( + foundry_root=foundry_root, + bug_report=bug_report, + use_hex_encoding=use_hex_encoding, + add_enum_constraints=add_enum_constraints, + ) except FileNotFoundError: print( f'File foundry.toml not found in: {str(foundry_root)!r}. Are you running kontrol in a Foundry project?', @@ -156,7 +166,7 @@ def _compare_versions(ver1: KVersion, ver2: KVersion) -> bool: def exec_load_state(options: LoadStateOptions) -> None: foundry_state_load( options=options, - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), ) @@ -183,7 +193,7 @@ def exec_build(options: BuildOptions) -> None: console.print(building_message) foundry_kompile( options=options, - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), ) console.print( ':white_heavy_check_mark: [bold green]Success![/bold green] [bold]Kontrol project built[/bold] :muscle:' @@ -210,7 +220,9 @@ def exec_prove(options: ProveOptions) -> None: try: console.print(proving_message) results = foundry_prove( - foundry=_load_foundry(options.foundry_root, options.bug_report), + foundry=_load_foundry( + options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints + ), options=options, recorded_state_entries=recorded_dump_entries if recorded_dump_entries else recorded_diff_entries, ) @@ -255,14 +267,18 @@ def exec_prove(options: ProveOptions) -> None: def exec_show(options: ShowOptions) -> None: output = foundry_show( - foundry=_load_foundry(options.foundry_root, use_hex_encoding=options.use_hex_encoding), + foundry=_load_foundry( + options.foundry_root, + use_hex_encoding=options.use_hex_encoding, + add_enum_constraints=options.enum_constraints, + ), options=options, ) print(output) def exec_refute_node(options: RefuteNodeOptions) -> None: - foundry = _load_foundry(options.foundry_root) + foundry = _load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints) refutation = foundry_refute_node(foundry=foundry, options=options) if refutation: @@ -276,14 +292,14 @@ def exec_refute_node(options: RefuteNodeOptions) -> None: def exec_unrefute_node(options: UnrefuteNodeOptions) -> None: foundry_unrefute_node( - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), options=options, ) def exec_split_node(options: SplitNodeOptions) -> None: node_ids = foundry_split_node( - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), options=options, ) @@ -291,16 +307,19 @@ def exec_split_node(options: SplitNodeOptions) -> None: def exec_to_dot(options: ToDotOptions) -> None: - foundry_to_dot(foundry=_load_foundry(options.foundry_root), options=options) + foundry_to_dot( + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), + options=options, + ) def exec_list(options: ListOptions) -> None: - stats = foundry_list(foundry=_load_foundry(options.foundry_root)) + stats = foundry_list(foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints)) print('\n'.join(stats)) def exec_view_kcfg(options: ViewKcfgOptions) -> None: - foundry = _load_foundry(options.foundry_root, use_hex_encoding=True) + foundry = _load_foundry(options.foundry_root, use_hex_encoding=True, add_enum_constraints=options.enum_constraints) test_id = foundry.get_test_id(options.test, options.version) contract_name, _ = test_id.split('.') proof = foundry.get_apr_proof(test_id) @@ -317,12 +336,15 @@ def _custom_view(elem: KCFGElem) -> Iterable[str]: def exec_minimize_proof(options: MinimizeProofOptions) -> None: - foundry_minimize_proof(foundry=_load_foundry(options.foundry_root), options=options) + foundry_minimize_proof( + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), + options=options, + ) def exec_remove_node(options: RemoveNodeOptions) -> None: foundry_remove_node( - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), options=options, ) @@ -330,7 +352,7 @@ def exec_remove_node(options: RemoveNodeOptions) -> None: def exec_simplify_node(options: SimplifyNodeOptions) -> None: pretty_term = foundry_simplify_node( - foundry=_load_foundry(options.foundry_root, options.bug_report), + foundry=_load_foundry(options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints), options=options, ) print(f'Simplified:\n{pretty_term}') @@ -338,14 +360,14 @@ def exec_simplify_node(options: SimplifyNodeOptions) -> None: def exec_step_node(options: StepNodeOptions) -> None: foundry_step_node( - foundry=_load_foundry(options.foundry_root, options.bug_report), + foundry=_load_foundry(options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints), options=options, ) def exec_merge_nodes(options: MergeNodesOptions) -> None: foundry_merge_nodes( - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), options=options, ) @@ -353,7 +375,7 @@ def exec_merge_nodes(options: MergeNodesOptions) -> None: def exec_section_edge(options: SectionEdgeOptions) -> None: foundry_section_edge( - foundry=_load_foundry(options.foundry_root, options.bug_report), + foundry=_load_foundry(options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints), options=options, ) @@ -361,7 +383,7 @@ def exec_section_edge(options: SectionEdgeOptions) -> None: def exec_get_model(options: GetModelOptions) -> None: output = foundry_get_model( - foundry=_load_foundry(options.foundry_root), + foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints), options=options, ) print(output) diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 3ced4abfc..4f2a6b9ff 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -168,6 +168,13 @@ def foundry_args(self) -> ArgumentParser: type=dir_path, help='Path to Foundry project root directory.', ) + args.add_argument( + '--enum-constraints', + dest='enum_constraints', + default=None, + action='store_true', + help='Add constraints for enum function arguments and storage slots.', + ) return args @cached_property diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 9445b466e..ecc02826f 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -80,6 +80,8 @@ class Foundry: _toml: dict[str, Any] _bug_report: BugReport | None _use_hex_encoding: bool + + add_enum_constraints: bool enums: dict[str, int] class Sorts: @@ -90,12 +92,14 @@ def __init__( foundry_root: Path, bug_report: BugReport | None = None, use_hex_encoding: bool = False, + add_enum_constraints: bool = False, ) -> None: self._root = foundry_root with (foundry_root / 'foundry.toml').open('rb') as f: self._toml = tomlkit.load(f) self._bug_report = bug_report self._use_hex_encoding = use_hex_encoding + self.add_enum_constraints = add_enum_constraints self.enums = {} def lookup_full_contract_name(self, contract_name: str) -> str: @@ -177,7 +181,7 @@ def find_enums(dct: dict) -> None: enum_max = len([member['name'] for member in dct['members']]) if enum_name in self.enums and enum_max != self.enums[enum_name]: raise ValueError( - f'enum name conflict: {enum_name} exists more than once in the codebase with a different size, which is not supported.' + f'enum name conflict: {enum_name} exists more than once in the codebase with a different size, which is not supported with --enum-constraints.' ) self.enums[enum_name] = len([member['name'] for member in dct['members']]) for node in dct['nodes']: @@ -187,12 +191,14 @@ def find_enums(dct: dict) -> None: contract_name = json_path.split('/')[-1] contract_json = json.loads(Path(json_path).read_text()) contract_name = contract_name[0:-5] if contract_name.endswith('.json') else contract_name + contract = Contract(contract_name, contract_json, foundry=True) + if self.add_enum_constraints: + find_enums(contract_json['ast']) try: contract = Contract(contract_name, contract_json, foundry=True) except KeyError: _LOGGER.warning(f'Skipping non-compatible JSON file for contract: {contract_name} at {json_path}.') continue - find_enums(contract_json['ast']) _contracts[contract.name_with_path] = contract # noqa: B909 diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 9cbd58991..3b73e5aa0 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -26,11 +26,13 @@ class ConfigType(Enum): class FoundryOptions(Options): foundry_root: Path + enum_constraints: bool @staticmethod def default() -> dict[str, Any]: return { 'foundry_root': Path('.'), + 'enum_constraints': False, } @staticmethod diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 7cb7a2d72..8b878796b 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1068,15 +1068,20 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner: field_name = contract_name + '_' + field.label.upper() if field.data_type.startswith('enum'): enum_name = field.data_type.split(' ')[1] - enum_max = foundry.enums[enum_name] - new_account_constraints.append( - mlEqualsTrue( - ltInt( - KEVM.lookup(storage_map, intToken(field.slot)), - intToken(enum_max), + if enum_name not in foundry.enums: + _LOGGER.warning( + f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.' + ) + else: + enum_max = foundry.enums[enum_name] + new_account_constraints.append( + mlEqualsTrue( + ltInt( + KEVM.lookup(storage_map, intToken(field.slot)), + intToken(enum_max), + ) ) ) - ) # Processing of strings if field.data_type == 'string': string_contents = KVariable(field_name + '_S_CONTENTS', sort=KSort('Bytes')) diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index b2308a8d6..3bf9ebbc7 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -464,13 +464,18 @@ def encoded_args(self, enums: dict[str, int]) -> tuple[KInner, list[KInner]]: type_constraints.append(rp) if input.internal_type is not None and input.internal_type.startswith('enum '): enum_name = input.internal_type.split(' ')[1] - enum_max = enums[enum_name] - type_constraints.append( - ltInt( - KVariable(input.arg_name), - intToken(enum_max), + if enum_name not in enums: + _LOGGER.warning( + f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.' + ) + else: + enum_max = enums[enum_name] + type_constraints.append( + ltInt( + KVariable(input.arg_name), + intToken(enum_max), + ) ) - ) encoded_args = KApply('encodeArgs', [KEVM.typed_args(args)]) return encoded_args, type_constraints @@ -698,13 +703,18 @@ def rule( conjuncts.append(rp) if input.internal_type is not None and input.internal_type.startswith('enum '): enum_name = input.internal_type.split(' ')[1] - enum_max = enums[enum_name] - conjuncts.append( - ltInt( - KVariable(input.arg_name), - intToken(enum_max), + if enum_name not in enums: + _LOGGER.warning( + f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.' + ) + else: + enum_max = enums[enum_name] + conjuncts.append( + ltInt( + KVariable(input.arg_name), + intToken(enum_max), + ) ) - ) lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)]) rhs = KEVM.abi_calldata(self.name, args) ensures = andBool(conjuncts) diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py index 62f3cc22f..b814fb212 100644 --- a/src/tests/integration/conftest.py +++ b/src/tests/integration/conftest.py @@ -54,7 +54,7 @@ def server(foundry: Foundry, no_use_booster: bool) -> Iterator[KoreServer]: @pytest.fixture(scope='session') def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, worker_id: str) -> Foundry: if foundry_root_dir: - return Foundry(foundry_root_dir) + return Foundry(foundry_root_dir, add_enum_constraints=True) if worker_id == 'master': root_tmp_dir = tmp_path_factory.getbasetemp() @@ -90,11 +90,12 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo 'PortalTest:PAUSABILITY-LEMMAS', 'ImmutableVarsTest:SYMBOLIC-BYTES-LEMMAS', ], + 'enum_constraints': True, } ), - foundry=Foundry(foundry_root), + foundry=Foundry(foundry_root, add_enum_constraints=True), ) session_foundry_root = tmp_path_factory.mktemp('foundry') copy_tree(str(foundry_root), str(session_foundry_root)) - return Foundry(session_foundry_root) + return Foundry(session_foundry_root, add_enum_constraints=True) diff --git a/src/tests/integration/test_kontrol_cse.py b/src/tests/integration/test_kontrol_cse.py index dad3114e0..9146938cd 100644 --- a/src/tests/integration/test_kontrol_cse.py +++ b/src/tests/integration/test_kontrol_cse.py @@ -69,6 +69,7 @@ def test_foundry_dependency_automated( 'config_type': config_type, 'run_constructor': run_constructor, 'force_sequential': force_sequential, + 'enum_constraints': True, } ), )