From 5064ae9772b9be415316833c667fa34431ef381c Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Tue, 6 Aug 2024 18:26:09 +0800 Subject: [PATCH 1/4] Record input names mapping to `input-mapping.json` --- src/kontrol/foundry.py | 28 +++++++++++++++++++++++++++- src/kontrol/kompile.py | 2 ++ src/kontrol/solc_to_k.py | 14 +++++++------- 3 files changed, 36 insertions(+), 8 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 8b5308706..5bc088880 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -21,7 +21,7 @@ from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model from pyk.cterm import CTerm from pyk.kast.inner import KApply, KInner, KSort, KToken, KVariable -from pyk.kast.manip import cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down +from pyk.kast.manip import abstract_term_safely, cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG from pyk.prelude.bytes import bytesToken @@ -210,6 +210,10 @@ def main_file(self) -> Path: def contracts_file(self) -> Path: return self.kompiled / 'contracts.k' + @property + def input_mapping_file(self) -> Path: + return self.kompiled / 'input-mapping.json' + @cached_property def kevm(self) -> KEVM: use_directory = self.out / 'tmp' @@ -381,6 +385,28 @@ def build(self) -> None: except CalledProcessError as err: raise RuntimeError("Couldn't forge build!") from err + def record_input_name_mapping(self, input_mapping_file: Path) -> None: + """ + Saves a JSON file storing a mapping between the names of Method's inputs and their K representation. + """ + + input_mapping = {} + + for contract in self.contracts.values(): + contract_mapping = {} + for method in contract.methods: + input_mapping = {} + for arg_name, name in method.arg_names.items(): + abstracted_term_name = abstract_term_safely(KVariable('_###SOLIDITY_ARG_VAR###_'), base_name=f'V{arg_name}').name + input_mapping[name] = abstracted_term_name + + contract_mapping[method.name] = input_mapping + + input_mapping[contract._name] = contract_mapping + + with input_mapping_file.open('w') as json_file: + json.dump(input_mapping, json_file, indent=4) + @cached_property def all_tests(self) -> list[str]: test_dir = os.path.join(self.profile.get('test', 'test'), '') diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index 2f438efbc..7ddc60f09 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -117,6 +117,8 @@ def foundry_kompile( _LOGGER.info(f'Wrote file: {foundry_contracts_file}') foundry.main_file.write_text(kevm.pretty_print(contract_main_definition) + '\n') _LOGGER.info(f'Wrote file: {foundry.main_file}') + foundry.record_input_name_mapping(foundry.input_mapping_file) + _LOGGER.info(f'Wrote file: {foundry.input_mapping_file}') def kompilation_digest() -> str: k_files = list(options.requires) + [foundry_contracts_file, foundry.main_file] diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index f2296fab1..e23f13f49 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -560,17 +560,17 @@ def flat_inputs(self) -> tuple[Input, ...]: return tuple(input for sub_inputs in self.inputs for input in sub_inputs.flattened()) @cached_property - def arg_names(self) -> tuple[str, ...]: - arg_names: list[str] = [] + def arg_names(self) -> dict[str, str]: + arg_names: dict[str, str] = {} for input in self.inputs: if input.type.endswith('[]') and not input.type.startswith('tuple'): if input.array_lengths is None: raise ValueError(f'Array length bounds missing for {input.name}') length = input.array_lengths[0] - arg_names.extend(f'{input.arg_name}_{i}' for i in range(length)) + arg_names.update({f'{input.arg_name}_{i}': f'{input.name}_{i}' for i in range(length)}) else: - arg_names.extend([sub_input.arg_name for sub_input in input.flattened()]) - return tuple(arg_names) + arg_names.update({sub_input.arg_name: sub_input.name for sub_input in input.flattened()}) + return arg_names @cached_property def arg_types(self) -> tuple[str, ...]: @@ -635,7 +635,7 @@ def rule( self, contract: KInner, application_label: KLabel, contract_name: str, enums: dict[str, int] ) -> KRule | None: prod_klabel = self.unique_klabel - arg_vars = [KVariable(name) for name in self.arg_names] + arg_vars = [KVariable(name) for name in self.arg_names.keys()] args: list[KInner] = [] conjuncts: list[KInner] = [] for input in self.inputs: @@ -712,7 +712,7 @@ def application(self) -> KInner: assert klabel is not None args = [ abstract_term_safely(KVariable('_###SOLIDITY_ARG_VAR###_'), base_name=f'V{name}') - for name in self.arg_names + for name in self.arg_names.keys() ] return klabel(args) From 0f247e77e49089bded37b892a8bcd832b55cdb7e Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Tue, 6 Aug 2024 19:02:08 +0800 Subject: [PATCH 2/4] Minor refactoring in `record_input_name_mapping` --- src/kontrol/foundry.py | 33 ++++++++++++++++++++++++++------- 1 file changed, 26 insertions(+), 7 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 5bc088880..1fe87405a 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -21,7 +21,15 @@ from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model from pyk.cterm import CTerm from pyk.kast.inner import KApply, KInner, KSort, KToken, KVariable -from pyk.kast.manip import abstract_term_safely, cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down +from pyk.kast.manip import ( + abstract_term_safely, + cell_label_to_var_name, + collect, + extract_lhs, + flatten_label, + minimize_term, + top_down, +) from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG from pyk.prelude.bytes import bytesToken @@ -387,23 +395,27 @@ def build(self) -> None: def record_input_name_mapping(self, input_mapping_file: Path) -> None: """ - Saves a JSON file storing a mapping between the names of Method's inputs and their K representation. + Saves a JSON file storing a mapping between the names of Method's inputs and their K representation. """ input_mapping = {} + # Create the mapping for each contract's method for contract in self.contracts.values(): contract_mapping = {} + + # Create the mapping for each method's arguments for method in contract.methods: - input_mapping = {} - for arg_name, name in method.arg_names.items(): - abstracted_term_name = abstract_term_safely(KVariable('_###SOLIDITY_ARG_VAR###_'), base_name=f'V{arg_name}').name - input_mapping[name] = abstracted_term_name + method_input_mapping = { + abstract_term_safely(KVariable('_###SOLIDITY_ARG_VAR###_'), base_name=f'V{arg_name}').name: name + for arg_name, name in method.arg_names.items() + } - contract_mapping[method.name] = input_mapping + contract_mapping[method.name] = method_input_mapping input_mapping[contract._name] = contract_mapping + # Write resulting mapping to JSON file with input_mapping_file.open('w') as json_file: json.dump(input_mapping, json_file, indent=4) @@ -1266,6 +1278,13 @@ def foundry_get_model( _LOGGER.warning('Node ID is not provided. Displaying models of failing and pending nodes:') failing = pending = True + # TODO(palina): use contract, test names to get relevant input mappings + # _, test_name = test_id.rsplit('%', 1) + # _contract_name, _test_name = test_name.split('(')[0].split('.') + # with open(foundry.input_mapping_file, 'r') as file: + # # Load the JSON data into a dictionary + # input_mapping = json.load(file) + nodes: Iterable[NodeIdLike] = options.nodes if pending: nodes = list(nodes) + [node.id for node in proof.pending] From 361e1bdc8e64597f9f2723961af48cb2f8f38c8f Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Tue, 6 Aug 2024 21:45:57 +0800 Subject: [PATCH 3/4] Minor tweaks to JSON writing, use signatures, full path in mapping file --- src/kontrol/foundry.py | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 1fe87405a..fee8f9779 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -411,13 +411,12 @@ def record_input_name_mapping(self, input_mapping_file: Path) -> None: for arg_name, name in method.arg_names.items() } - contract_mapping[method.name] = method_input_mapping + contract_mapping[method.signature] = method_input_mapping - input_mapping[contract._name] = contract_mapping + input_mapping[contract.name_with_path] = contract_mapping # Write resulting mapping to JSON file - with input_mapping_file.open('w') as json_file: - json.dump(input_mapping, json_file, indent=4) + input_mapping_file.write_text(json.dumps(input_mapping, indent=4)) @cached_property def all_tests(self) -> list[str]: @@ -1278,13 +1277,6 @@ def foundry_get_model( _LOGGER.warning('Node ID is not provided. Displaying models of failing and pending nodes:') failing = pending = True - # TODO(palina): use contract, test names to get relevant input mappings - # _, test_name = test_id.rsplit('%', 1) - # _contract_name, _test_name = test_name.split('(')[0].split('.') - # with open(foundry.input_mapping_file, 'r') as file: - # # Load the JSON data into a dictionary - # input_mapping = json.load(file) - nodes: Iterable[NodeIdLike] = options.nodes if pending: nodes = list(nodes) + [node.id for node in proof.pending] @@ -1319,6 +1311,11 @@ def foundry_get_model( res_lines.append('') res_lines.append(f'Node id: {node_id}') node = proof.kcfg.node(node_id) + + contract_name, test_name = test_id.split(':')[0].split('.') + input_mapping = json.loads(foundry.input_mapping_file.read_text()) + input_mapping = input_mapping.get(contract_name, {}).get(test_name, {}) + # TODO: use the input mapping to generate the model res_lines.extend(print_model(node, kcfg_explore)) return '\n'.join(res_lines) From 535a4ec4dd50de2f32e634788bfbb9c333f42f42 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Wed, 7 Aug 2024 16:38:01 +0800 Subject: [PATCH 4/4] Add env variables to the mapping, use it in `get_model`, `prove` counterexamples --- src/kontrol/foundry.py | 17 ++++++++++++++--- src/kontrol/prove.py | 6 ++++++ 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index fee8f9779..0c07419d9 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -415,6 +415,16 @@ def record_input_name_mapping(self, input_mapping_file: Path) -> None: input_mapping[contract.name_with_path] = contract_mapping + # Add environment variables to the mapping + env_variables_mapping = { + 'TIMESTAMP_CELL': 'block.timestamp', + 'NUMBER_CELL': 'block.number', + 'ORIGIN_ID': 'tx.origin', + 'CALLER_ID': 'msg.sender', + } + + input_mapping['env'] = env_variables_mapping + # Write resulting mapping to JSON file input_mapping_file.write_text(json.dumps(input_mapping, indent=4)) @@ -1314,9 +1324,10 @@ def foundry_get_model( contract_name, test_name = test_id.split(':')[0].split('.') input_mapping = json.loads(foundry.input_mapping_file.read_text()) - input_mapping = input_mapping.get(contract_name, {}).get(test_name, {}) - # TODO: use the input mapping to generate the model - res_lines.extend(print_model(node, kcfg_explore)) + proof_input_mapping = input_mapping.get(contract_name, {}).get(test_name, {}) + proof_input_mapping.update(input_mapping.get('env', {})) + + res_lines.extend(print_model(node, kcfg_explore, proof_input_mapping)) return '\n'.join(res_lines) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index f2a852549..a189a9a9f 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1,5 +1,6 @@ from __future__ import annotations +import json import logging import time from abc import abstractmethod @@ -583,6 +584,10 @@ def method_to_apr_proof( config_type=config_type, ) + input_mapping = json.loads(foundry.input_mapping_file.read_text()) + proof_input_mapping = input_mapping.get(test.contract.name_with_path, {}).get(test.method.signature, {}) + proof_input_mapping.update(input_mapping.get('env', [])) + apr_proof = APRProof( test.id, kcfg, @@ -593,6 +598,7 @@ def method_to_apr_proof( bmc_depth=bmc_depth, proof_dir=foundry.proofs_dir, subproof_ids=summary_ids, + variable_names_mapping=proof_input_mapping, ) return apr_proof