From 35e08817b6ca4e78e26f67725eb907080858a2bf Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 19 Jun 2024 16:59:08 -0500 Subject: [PATCH 1/7] Add test for mapping constraints, add more detail to StorageField to accommodate generating constraints for nested types --- src/kontrol/prove.py | 10 ++- src/kontrol/solc_to_k.py | 87 ++++++++++++++----- .../foundry/test/CallableStorageTest.t.sol | 21 +++++ .../test-data/foundry/test/Mapping.t.sol | 30 +++++++ 4 files changed, 124 insertions(+), 24 deletions(-) create mode 100644 src/tests/integration/test-data/foundry/test/Mapping.t.sol diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 56144fffd..0e0a6d4d1 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -30,9 +30,11 @@ from .foundry import Foundry, foundry_to_xml from .hevm import Hevm from .options import ConfigType, TraceOptions -from .solc_to_k import Contract, hex_string_to_int +from .solc_to_k import Contract, hex_string_to_int, _range_predicate from .utils import parse_test_version_tuple +from .solc_to_k import StorageFieldMappingType + if TYPE_CHECKING: from collections.abc import Iterable from typing import Final @@ -982,6 +984,8 @@ def _create_cse_accounts( new_accounts.append(Foundry.symbolic_account(contract_name, contract_code, storage_map)) for field in storage_fields: + if isinstance(field.data_type, StorageFieldMappingType): + ... if field.data_type == 'string': lookup = KEVM.lookup(storage_map, intToken(field.slot)) length_byte_lt32 = ltInt( @@ -1030,8 +1034,8 @@ def _create_cse_accounts( new_account_constraints.append(mlEqualsTrue(lowest_bit_not_set)) new_account_constraints.append(mlEqualsTrue(length_byte_lt32)) new_account_constraints.append(mlEqualsTrue(length_byte_positive)) - if field.data_type.startswith('contract '): - contract_type = field.data_type.split(' ')[1] + if field.data_type.name.startswith('contract '): + contract_type = field.data_type.name.split(' ')[1] for full_contract_name, contract_obj in foundry.contracts.items(): # TODO: this is not enough, it is possible that the same contract comes with # src% and test%, in which case we don't know automatically which one to choose diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 654f6046c..457c49c11 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -322,13 +322,77 @@ def parse_devdoc(tag: str, devdoc: dict | None) -> dict: return natspecs -class StorageField(NamedTuple): +@dataclass +class StorageFieldType: + name: str + +@dataclass +class StorageFieldArrayType(StorageFieldType): + base_type: StorageFieldType + +@dataclass +class StorageFieldMappingType(StorageFieldType): + key_type: StorageFieldType + val_type: StorageFieldType + +@dataclass +class StorageFieldStructType(StorageFieldType): + members: tuple[StorageField, ...] + +@dataclass +class StorageField(): label: str - data_type: str + data_type: StorageFieldType slot: int offset: int +def process_data_type(dct: dict, types_dct: dict) -> StorageFieldType: + if 'key' in dct: + # Mapping + return StorageFieldMappingType( + name=dct['label'], + key_type=process_data_type(types_dct[dct['key']], types_dct), + val_type=process_data_type(types_dct[dct['value']], types_dct), + ) + elif 'members' in dct: + # Struct + return StorageFieldStructType( + name=dct['label'], + members=tuple(storage_field_from_dict(member, types_dct) for member in dct['members']), + ) + elif 'base' in dct: + # Array + return StorageFieldArrayType( + name=dct['label'], + base_type=process_data_type(types_dct[dct['base']], types_dct), + ) + else: + # Other + return StorageFieldType(name=dct['label']) + +def storage_field_from_dict(dct: dict, types_dct: dict) -> StorageField: + label= dct['label'] + slot = dct['slot'] + offset = dct['offset'] + data_type = process_data_type(types_dct[dct['type']], types_dct) + return StorageField(label, data_type, slot, offset) + + +def process_storage_layout(storage_layout: dict) -> tuple[StorageField, ...]: + storage = storage_layout.get('storage', []) + types = storage_layout.get('types', {}) + + fields_list: list[StorageField] = [] + for field in storage: + storage_field = storage_field_from_dict(field, types) + fields_list.append(storage_field) + print(storage_field) + + return tuple(fields_list) + + + @dataclass class Contract: @dataclass @@ -1325,22 +1389,3 @@ def _find_function_calls(node: dict) -> None: return function_calls -def process_storage_layout(storage_layout: dict) -> tuple[StorageField, ...]: - storage = storage_layout.get('storage', []) - types = storage_layout.get('types', {}) - - fields_list: list[StorageField] = [] - for field in storage: - try: - type_info = types.get(field['type'], {}) - storage_field = StorageField( - label=field['label'], - data_type=type_info.get('label', field['type']), - slot=int(field['slot']), - offset=int(field['offset']), - ) - fields_list.append(storage_field) - except (KeyError, ValueError) as e: - _LOGGER.error(f'Error processing field {field}: {e}') - - return tuple(fields_list) diff --git a/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol b/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol index 9608d0743..c86ea94d4 100644 --- a/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol @@ -4,9 +4,19 @@ pragma solidity =0.8.13; import "forge-std/Test.sol"; import "kontrol-cheatcodes/KontrolCheats.sol"; +enum Letter { + LETTER_A, + LETTER_B, + LETTER_C, + LETTER_D, + LETTER_E, + LETTER_F +} + contract CallableStorageContract { uint public num; string public str; + Letter public letter; constructor(string memory a) payable { str = a; @@ -14,6 +24,7 @@ contract CallableStorageContract { } contract CallableStorageTest is Test, KontrolCheats { + uint public a; CallableStorageContract member_contract; function setUp() public { @@ -23,4 +34,14 @@ contract CallableStorageTest is Test, KontrolCheats { function test_str() public { assertEq(member_contract.str(), "Test String"); } + + function test_enum_argument_range(Letter letter) public pure { + assert(uint(letter) <= 5); + assert(uint(letter) >= 0); + } + + function test_enum_storage_range() public view { + assert(uint(member_contract.letter()) <= 5); + assert(uint(member_contract.letter()) >= 0); + } } diff --git a/src/tests/integration/test-data/foundry/test/Mapping.t.sol b/src/tests/integration/test-data/foundry/test/Mapping.t.sol new file mode 100644 index 000000000..7a61bba1d --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/Mapping.t.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +contract MappingContract { + mapping(address => mapping(address => uint256)) public balances; + + function get_mapping_val(address a) public returns (uint256) { + return balances[a][a]; + } +} + +contract MappingTest is Test { + uint256 b; + uint256 val; + MappingContract c; + + constructor() public { + c = new MappingContract(); + } + + function test_mapping(address a) public { + b = 42; + val = c.get_mapping_val(a); + assert(val < 256); + } + +} From c02617edf30aeb71f48f1d83872af9a5d85f73e4 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 19 Jun 2024 22:00:00 +0000 Subject: [PATCH 2/7] Set Version: 0.1.316 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 379104056..2bc91bbb1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.314 +0.1.316 diff --git a/pyproject.toml b/pyproject.toml index afe5c7874..2cfad7308 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.314" +version = "0.1.316" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 1128f17e6..9014f0b17 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.314' +VERSION: Final = '0.1.316' From ecf1d55e1789c5366437276410afbd16c64a5bad Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 20 Jun 2024 14:46:44 -0500 Subject: [PATCH 3/7] Generate constraints for nested maps --- src/kontrol/solc_to_k.py | 46 ++++++++++++++++++- .../test-data/foundry/test/Mapping.t.sol | 10 +++- 2 files changed, 52 insertions(+), 4 deletions(-) diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 457c49c11..c288fac18 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -325,6 +325,21 @@ def parse_devdoc(tag: str, devdoc: dict | None) -> dict: @dataclass class StorageFieldType: name: str + slot: KInner + + def compute_slots(self, base_slot: KInner) -> None: + self.slot = base_slot + + def slots(self) -> list[tuple[KInner, str]]: + return [(self.slot, self.name)] + + def compute_constraints(self, storage_map: KInner) -> list[KInner]: + constraints = [] + for slot, slot_type in self.slots(): + constraint = _range_predicate(term=KEVM.lookup(storage_map, slot), type_label=slot_type) + if constraint is not None: + constraints.append(constraint) + return constraints @dataclass class StorageFieldArrayType(StorageFieldType): @@ -335,6 +350,20 @@ class StorageFieldMappingType(StorageFieldType): key_type: StorageFieldType val_type: StorageFieldType + def compute_slots(self, base_slot: KInner) -> None: + self.slot = base_slot + self.val_type.compute_slots( + KApply('keccak', [ + KApply('_+Bytes_', [ + KVariable('FRESH_VAR'), + base_slot, + ]) + ]) + ) + + def slots(self) -> list[tuple[KInner, str]]: + return [(self.slot, self.name)] + self.val_type.slots() + @dataclass class StorageFieldStructType(StorageFieldType): members: tuple[StorageField, ...] @@ -347,6 +376,14 @@ class StorageField(): offset: int + +# def constraints_for_storage_field(sf: StorageField, storage_map: KInner) -> list[KInner]: +# lookup = KEVM.lookup(storage_map, sf.data_type.get_slot(intToken(sf.slot))) +# term = sf.data_type.get_slot(KApply('asWord', [sf.slot])) +# print(term) +# range_pred = _range_predicate(type_label=sf.data_type.name, term=term) + + def process_data_type(dct: dict, types_dct: dict) -> StorageFieldType: if 'key' in dct: # Mapping @@ -354,22 +391,25 @@ def process_data_type(dct: dict, types_dct: dict) -> StorageFieldType: name=dct['label'], key_type=process_data_type(types_dct[dct['key']], types_dct), val_type=process_data_type(types_dct[dct['value']], types_dct), + slot=None, ) elif 'members' in dct: # Struct return StorageFieldStructType( name=dct['label'], members=tuple(storage_field_from_dict(member, types_dct) for member in dct['members']), + slot=None, ) elif 'base' in dct: # Array return StorageFieldArrayType( name=dct['label'], base_type=process_data_type(types_dct[dct['base']], types_dct), + slot=None, ) else: # Other - return StorageFieldType(name=dct['label']) + return StorageFieldType(name=dct['label'], slot=None) def storage_field_from_dict(dct: dict, types_dct: dict) -> StorageField: label= dct['label'] @@ -387,7 +427,9 @@ def process_storage_layout(storage_layout: dict) -> tuple[StorageField, ...]: for field in storage: storage_field = storage_field_from_dict(field, types) fields_list.append(storage_field) - print(storage_field) + storage_field.data_type.compute_slots(intToken(storage_field.slot)) + print(storage_field.data_type.compute_constraints(KVariable('STORAGE_MAP'))) + return tuple(fields_list) diff --git a/src/tests/integration/test-data/foundry/test/Mapping.t.sol b/src/tests/integration/test-data/foundry/test/Mapping.t.sol index 7a61bba1d..84a51497c 100644 --- a/src/tests/integration/test-data/foundry/test/Mapping.t.sol +++ b/src/tests/integration/test-data/foundry/test/Mapping.t.sol @@ -6,15 +6,20 @@ import "kontrol-cheatcodes/KontrolCheats.sol"; contract MappingContract { mapping(address => mapping(address => uint256)) public balances; + mapping(address => uint256) public single_map; function get_mapping_val(address a) public returns (uint256) { return balances[a][a]; } + + function get_mapping_val2(address a) public returns (uint256) { + return single_map[a]; + } } contract MappingTest is Test { - uint256 b; uint256 val; + uint256 val2; MappingContract c; constructor() public { @@ -22,9 +27,10 @@ contract MappingTest is Test { } function test_mapping(address a) public { - b = 42; val = c.get_mapping_val(a); + val2 = c.get_mapping_val2(a); assert(val < 256); + assert(val2 < 256); } } From c38b69ef5a5845125835231e9878e27d859b9a3d Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 25 Jun 2024 13:48:30 -0500 Subject: [PATCH 4/7] Add checking for enum length --- src/kontrol/foundry.py | 23 ++++++- src/kontrol/prove.py | 9 ++- src/kontrol/solc_to_k.py | 65 ++++++++++++++++--- .../foundry/test/CallableStorageTest.t.sol | 29 +++++---- .../test-data/foundry/test/EnumTest.t.sol | 25 +++++++ .../test-data/foundry/test/EnumTest2.t.sol | 25 +++++++ .../test-data/foundry/test/EnumTest3.t.sol | 15 +++++ .../test-data/foundry/test/Mapping.t.sol | 3 + 8 files changed, 169 insertions(+), 25 deletions(-) create mode 100644 src/tests/integration/test-data/foundry/test/EnumTest.t.sol create mode 100644 src/tests/integration/test-data/foundry/test/EnumTest2.t.sol create mode 100644 src/tests/integration/test-data/foundry/test/EnumTest3.t.sol diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index b3814eba3..9d30e3516 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -159,12 +159,33 @@ def contracts(self) -> dict[str, Contract]: json_paths = sorted(json_paths) # Must sort to get consistent output order on different platforms _LOGGER.info(f'Processing contract files: {json_paths}') _contracts: dict[str, Contract] = {} + exported_symbols: dict[str, list[str]] = {} + enums: dict[str, int] = {} + for json_path in json_paths: + + 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 + + exported_symbols[contract_json['ast']['absolutePath']] = [contract_json['ast']['exportedSymbols']] + + def find_enums(dct: dict): + if dct['nodeType'] == 'EnumDefinition': + enums[dct['canonicalName']] = len([member['name'] for member in dct['members']]) + for node in dct['nodes']: + find_enums(node) + + find_enums(contract_json['ast']) + + print(enums) + for json_path in json_paths: _LOGGER.debug(f'Processing contract file: {json_path}') 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) + + contract = Contract(contract_name, contract_json, exported_symbols, foundry=True) _contracts[contract.name_with_path] = contract # noqa: B909 diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 0e0a6d4d1..976935858 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -553,7 +553,8 @@ def _method_to_initialized_cfg( kcfg.let_node(target_node_id, cterm=target_cterm) _LOGGER.info(f'Simplifying KCFG for test: {test.name}') - kcfg_explore.simplify(kcfg, {}) +# kcfg_explore.simplify(kcfg, {}) + print(kcfg.node(1).cterm) return kcfg, init_node_id, target_node_id @@ -916,6 +917,7 @@ def _init_cterm( for constraint in storage_constraints: init_cterm = init_cterm.add_constraint(constraint) + print(constraint) # The calling contract is assumed to be in the present accounts for non-tests if not (config_type == ConfigType.TEST_CONFIG or active_symbolik): @@ -984,6 +986,11 @@ def _create_cse_accounts( new_accounts.append(Foundry.symbolic_account(contract_name, contract_code, storage_map)) for field in storage_fields: + + for constraint in field.data_type.compute_constraints(storage_map): + new_account_constraints.append(constraint) + print(field.data_type.slot_vars()) + if isinstance(field.data_type, StorageFieldMappingType): ... if field.data_type == 'string': diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index c288fac18..563e5dd8d 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -7,6 +7,8 @@ from functools import cached_property from subprocess import CalledProcessError from typing import TYPE_CHECKING, NamedTuple +from pyk.prelude.k import K_ITEM, GENERATED_TOP_CELL +from pyk.prelude.ml import mlEqualsTrue from kevm_pyk.kevm import KEVM from pyk.kast.att import Atts, KAtt @@ -333,11 +335,18 @@ def compute_slots(self, base_slot: KInner) -> None: def slots(self) -> list[tuple[KInner, str]]: return [(self.slot, self.name)] + def slot_vars(self) -> list[KInner]: + return [] + def compute_constraints(self, storage_map: KInner) -> list[KInner]: + constraints = [] for slot, slot_type in self.slots(): - constraint = _range_predicate(term=KEVM.lookup(storage_map, slot), type_label=slot_type) + constraint = _range_predicate(term=KEVM.lookup(storage_map, slot.args[1]), type_label=slot_type) if constraint is not None: + constraint = mlEqualsTrue(constraint) + for slot_var in self.slot_vars(): + constraint = KLabel('#Forall', K_ITEM, GENERATED_TOP_CELL)(slot_var, constraint) constraints.append(constraint) return constraints @@ -345,20 +354,31 @@ def compute_constraints(self, storage_map: KInner) -> list[KInner]: class StorageFieldArrayType(StorageFieldType): base_type: StorageFieldType + @dataclass class StorageFieldMappingType(StorageFieldType): key_type: StorageFieldType val_type: StorageFieldType + slot_var: list[KInner] = () + + def slot_vars(self) -> list[KInner]: + return list(self.slot_var) + self.val_type.slot_vars() def compute_slots(self, base_slot: KInner) -> None: + variable = KVariable('V_' + hash_str(base_slot)[0:8]) + self.slot_var = (variable,) self.slot = base_slot self.val_type.compute_slots( - KApply('keccak', [ - KApply('_+Bytes_', [ - KVariable('FRESH_VAR'), - base_slot, +# KLabel('#Forall', K_ITEM, GENERATED_TOP_CELL)(variable, + KApply('buf', [intToken(32), + KApply('keccak(_)_SERIALIZATION_Int_Bytes', [ + KEVM.bytes_append( + variable, + base_slot, + ) + ]) ]) - ]) +# ) ) def slots(self) -> list[tuple[KInner, str]]: @@ -427,8 +447,7 @@ def process_storage_layout(storage_layout: dict) -> tuple[StorageField, ...]: for field in storage: storage_field = storage_field_from_dict(field, types) fields_list.append(storage_field) - storage_field.data_type.compute_slots(intToken(storage_field.slot)) - print(storage_field.data_type.compute_constraints(KVariable('STORAGE_MAP'))) + storage_field.data_type.compute_slots(KApply('buf', [intToken(32), intToken(storage_field.slot)])) return tuple(fields_list) @@ -813,7 +832,12 @@ def application(self) -> KInner: constructor: Constructor | None PREFIX_CODE: Final = 'Z' - def __init__(self, contract_name: str, contract_json: dict, foundry: bool = False) -> None: +# importedSymbols: dict[str, int] | None = None +# +# enums: dict[str, list[str]] | None = None + + + def __init__(self, contract_name: str, contract_json: dict, exported_symbols, foundry: bool = False) -> None: self._name = contract_name self.contract_json = contract_json @@ -827,6 +851,29 @@ def __init__(self, contract_name: str, contract_json: dict, foundry: bool = Fals evm = self.contract_json['evm'] if not foundry else self.contract_json + +# def parse_node(dct: dict): +# +# if dct['nodeType'] == 'ImportDirective': +# for key, val in exported_symbols[dct['absolutePath']][0].items(): +# assert len(val) == 1 +# self.importedSymbols[key] = val[0] +# +# # +# # if dct['nodeType'] == 'EnumDefinition': +# # self.enums[dct['canonicalName']] = {member['name'] for member in dct['members']} +# for node in dct['nodes']: +# parse_node(node) +# +# +# self.enums = {} +# self.importedSymbols = {} +# parse_node(contract_json['ast']) +# print(self._name) +# print(self.importedSymbols) +# print(self.enums) + + deployed_bytecode = evm['deployedBytecode'] self.deployed_bytecode = deployed_bytecode['object'].replace('0x', '') self.raw_sourcemap = deployed_bytecode['sourceMap'] if 'sourceMap' in deployed_bytecode else None diff --git a/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol b/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol index c86ea94d4..52d51ab5b 100644 --- a/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol @@ -3,20 +3,21 @@ pragma solidity =0.8.13; import "forge-std/Test.sol"; import "kontrol-cheatcodes/KontrolCheats.sol"; +import { Letter as MyLetter } from "test/EnumTest.t.sol"; -enum Letter { - LETTER_A, - LETTER_B, - LETTER_C, - LETTER_D, - LETTER_E, - LETTER_F -} +// enum Letter { +// LETTER_A, +// LETTER_B, +// LETTER_C, +// LETTER_D, +// LETTER_E, +// LETTER_F +// } contract CallableStorageContract { uint public num; string public str; - Letter public letter; +// Letter public letter; constructor(string memory a) payable { str = a; @@ -35,13 +36,13 @@ contract CallableStorageTest is Test, KontrolCheats { assertEq(member_contract.str(), "Test String"); } - function test_enum_argument_range(Letter letter) public pure { + function test_enum_argument_range(MyLetter letter) public pure { assert(uint(letter) <= 5); assert(uint(letter) >= 0); } - function test_enum_storage_range() public view { - assert(uint(member_contract.letter()) <= 5); - assert(uint(member_contract.letter()) >= 0); - } +// function test_enum_storage_range() public view { +// assert(uint(member_contract.letter()) <= 5); +// assert(uint(member_contract.letter()) >= 0); +// } } diff --git a/src/tests/integration/test-data/foundry/test/EnumTest.t.sol b/src/tests/integration/test-data/foundry/test/EnumTest.t.sol new file mode 100644 index 000000000..0a17e6cc8 --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/EnumTest.t.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +enum Letter { + LETTER_A, + LETTER_B, + LETTER_C, + LETTER_D, + LETTER_E, + LETTER_F +} + + +contract EnumTest is Test { + uint public num; + string public str; + Letter public letter; + + constructor(string memory a) payable { + str = a; + } +} diff --git a/src/tests/integration/test-data/foundry/test/EnumTest2.t.sol b/src/tests/integration/test-data/foundry/test/EnumTest2.t.sol new file mode 100644 index 000000000..fc6517c71 --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/EnumTest2.t.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +enum Letter { + LETTER_A, + LETTER_B, + LETTER_C, + LETTER_D, + LETTER_E, + LETTER_F +} + + +contract EnumTest2 is Test { + uint public num; + string public str; + Letter public letter; + + constructor(string memory a) payable { + str = a; + } +} diff --git a/src/tests/integration/test-data/foundry/test/EnumTest3.t.sol b/src/tests/integration/test-data/foundry/test/EnumTest3.t.sol new file mode 100644 index 000000000..64c14e4db --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/EnumTest3.t.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "test/EnumTest.t.sol"; + + +contract EnumTest2 is Test { + uint public num; + string public str; + Letter public letter; + + constructor(string memory a) payable { + str = a; + } +} diff --git a/src/tests/integration/test-data/foundry/test/Mapping.t.sol b/src/tests/integration/test-data/foundry/test/Mapping.t.sol index 84a51497c..d9844e869 100644 --- a/src/tests/integration/test-data/foundry/test/Mapping.t.sol +++ b/src/tests/integration/test-data/foundry/test/Mapping.t.sol @@ -26,9 +26,12 @@ contract MappingTest is Test { c = new MappingContract(); } + function my_internal() internal { } + function test_mapping(address a) public { val = c.get_mapping_val(a); val2 = c.get_mapping_val2(a); + my_internal(); assert(val < 256); assert(val2 < 256); } From 2fe9eed7d0adb95df043d2e38b250a33c0cc53d7 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 26 Jun 2024 14:41:06 -0500 Subject: [PATCH 5/7] Clean up --- .../test-data/foundry/test/EnumTest.t.sol | 25 ------------------- .../test-data/foundry/test/EnumTest2.t.sol | 25 ------------------- .../test-data/foundry/test/EnumTest3.t.sol | 15 ----------- 3 files changed, 65 deletions(-) delete mode 100644 src/tests/integration/test-data/foundry/test/EnumTest.t.sol delete mode 100644 src/tests/integration/test-data/foundry/test/EnumTest2.t.sol delete mode 100644 src/tests/integration/test-data/foundry/test/EnumTest3.t.sol diff --git a/src/tests/integration/test-data/foundry/test/EnumTest.t.sol b/src/tests/integration/test-data/foundry/test/EnumTest.t.sol deleted file mode 100644 index 0a17e6cc8..000000000 --- a/src/tests/integration/test-data/foundry/test/EnumTest.t.sol +++ /dev/null @@ -1,25 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity =0.8.13; - -import "forge-std/Test.sol"; -import "kontrol-cheatcodes/KontrolCheats.sol"; - -enum Letter { - LETTER_A, - LETTER_B, - LETTER_C, - LETTER_D, - LETTER_E, - LETTER_F -} - - -contract EnumTest is Test { - uint public num; - string public str; - Letter public letter; - - constructor(string memory a) payable { - str = a; - } -} diff --git a/src/tests/integration/test-data/foundry/test/EnumTest2.t.sol b/src/tests/integration/test-data/foundry/test/EnumTest2.t.sol deleted file mode 100644 index fc6517c71..000000000 --- a/src/tests/integration/test-data/foundry/test/EnumTest2.t.sol +++ /dev/null @@ -1,25 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity =0.8.13; - -import "forge-std/Test.sol"; -import "kontrol-cheatcodes/KontrolCheats.sol"; - -enum Letter { - LETTER_A, - LETTER_B, - LETTER_C, - LETTER_D, - LETTER_E, - LETTER_F -} - - -contract EnumTest2 is Test { - uint public num; - string public str; - Letter public letter; - - constructor(string memory a) payable { - str = a; - } -} diff --git a/src/tests/integration/test-data/foundry/test/EnumTest3.t.sol b/src/tests/integration/test-data/foundry/test/EnumTest3.t.sol deleted file mode 100644 index 64c14e4db..000000000 --- a/src/tests/integration/test-data/foundry/test/EnumTest3.t.sol +++ /dev/null @@ -1,15 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity =0.8.13; - -import "test/EnumTest.t.sol"; - - -contract EnumTest2 is Test { - uint public num; - string public str; - Letter public letter; - - constructor(string memory a) payable { - str = a; - } -} From 4d34df5031580ed708d9992635b08f1f01ddaf85 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 26 Jun 2024 14:42:12 -0500 Subject: [PATCH 6/7] Clean up --- .../foundry/test/CallableStorageTest.t.sol | 22 ------------------- 1 file changed, 22 deletions(-) diff --git a/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol b/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol index 52d51ab5b..9608d0743 100644 --- a/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/CallableStorageTest.t.sol @@ -3,21 +3,10 @@ pragma solidity =0.8.13; import "forge-std/Test.sol"; import "kontrol-cheatcodes/KontrolCheats.sol"; -import { Letter as MyLetter } from "test/EnumTest.t.sol"; - -// enum Letter { -// LETTER_A, -// LETTER_B, -// LETTER_C, -// LETTER_D, -// LETTER_E, -// LETTER_F -// } contract CallableStorageContract { uint public num; string public str; -// Letter public letter; constructor(string memory a) payable { str = a; @@ -25,7 +14,6 @@ contract CallableStorageContract { } contract CallableStorageTest is Test, KontrolCheats { - uint public a; CallableStorageContract member_contract; function setUp() public { @@ -35,14 +23,4 @@ contract CallableStorageTest is Test, KontrolCheats { function test_str() public { assertEq(member_contract.str(), "Test String"); } - - function test_enum_argument_range(MyLetter letter) public pure { - assert(uint(letter) <= 5); - assert(uint(letter) >= 0); - } - -// function test_enum_storage_range() public view { -// assert(uint(member_contract.letter()) <= 5); -// assert(uint(member_contract.letter()) >= 0); -// } } From ed4aedbf2601c98c5b4209943b931aec5eb167b4 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 26 Jun 2024 14:44:28 -0500 Subject: [PATCH 7/7] Clean up --- src/kontrol/foundry.py | 23 +---------------------- src/kontrol/solc_to_k.py | 30 +----------------------------- 2 files changed, 2 insertions(+), 51 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 9d30e3516..b3814eba3 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -159,33 +159,12 @@ def contracts(self) -> dict[str, Contract]: json_paths = sorted(json_paths) # Must sort to get consistent output order on different platforms _LOGGER.info(f'Processing contract files: {json_paths}') _contracts: dict[str, Contract] = {} - exported_symbols: dict[str, list[str]] = {} - enums: dict[str, int] = {} - for json_path in json_paths: - - 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 - - exported_symbols[contract_json['ast']['absolutePath']] = [contract_json['ast']['exportedSymbols']] - - def find_enums(dct: dict): - if dct['nodeType'] == 'EnumDefinition': - enums[dct['canonicalName']] = len([member['name'] for member in dct['members']]) - for node in dct['nodes']: - find_enums(node) - - find_enums(contract_json['ast']) - - print(enums) - for json_path in json_paths: _LOGGER.debug(f'Processing contract file: {json_path}') 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, exported_symbols, foundry=True) + contract = Contract(contract_name, contract_json, foundry=True) _contracts[contract.name_with_path] = contract # noqa: B909 diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 563e5dd8d..bca9bbfd8 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -832,12 +832,7 @@ def application(self) -> KInner: constructor: Constructor | None PREFIX_CODE: Final = 'Z' -# importedSymbols: dict[str, int] | None = None -# -# enums: dict[str, list[str]] | None = None - - - def __init__(self, contract_name: str, contract_json: dict, exported_symbols, foundry: bool = False) -> None: + def __init__(self, contract_name: str, contract_json: dict, foundry: bool = False) -> None: self._name = contract_name self.contract_json = contract_json @@ -851,29 +846,6 @@ def __init__(self, contract_name: str, contract_json: dict, exported_symbols, fo evm = self.contract_json['evm'] if not foundry else self.contract_json - -# def parse_node(dct: dict): -# -# if dct['nodeType'] == 'ImportDirective': -# for key, val in exported_symbols[dct['absolutePath']][0].items(): -# assert len(val) == 1 -# self.importedSymbols[key] = val[0] -# -# # -# # if dct['nodeType'] == 'EnumDefinition': -# # self.enums[dct['canonicalName']] = {member['name'] for member in dct['members']} -# for node in dct['nodes']: -# parse_node(node) -# -# -# self.enums = {} -# self.importedSymbols = {} -# parse_node(contract_json['ast']) -# print(self._name) -# print(self.importedSymbols) -# print(self.enums) - - deployed_bytecode = evm['deployedBytecode'] self.deployed_bytecode = deployed_bytecode['object'].replace('0x', '') self.raw_sourcemap = deployed_bytecode['sourceMap'] if 'sourceMap' in deployed_bytecode else None