From 05934f614cf9da6fa9a06e2c7bfda9e2ed990c26 Mon Sep 17 00:00:00 2001 From: Palina Date: Fri, 11 Oct 2024 08:33:33 +0800 Subject: [PATCH] Extend library refs processing, fix in error messages for `setUp` (#861) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Process library refs in both `bytecode` and `deployed_bytecode`; fix error message in case of a failed `init`, `setUp` * Update expected output for new test * Minor typo fix * Formatting * Formatting for quotes * Run `ExternalNestedLibraryTest.testExtLibs()` in `test_foundry_init_code` --------- Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- src/kontrol/prove.py | 88 ++++++----- src/kontrol/solc_to_k.py | 30 ++-- .../integration/test-data/foundry-init-code | 3 +- .../test/ExternalNestedLibraryTest.t.sol | 28 ++++ .../test-data/show/contracts.k.expected | 138 ++++++++++++++++++ .../test-data/show/foundry.k.expected | 24 +++ 6 files changed, 264 insertions(+), 47 deletions(-) create mode 100644 src/tests/integration/test-data/foundry/test/ExternalNestedLibraryTest.t.sol diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 4134c88fe..84aa15ecf 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -159,8 +159,11 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False) constructor_results = _run_prover(constructor_tests, include_summaries=False) failed = [proof for proof in constructor_results if not proof.passed] + failed_contract_names = [proof.id.split('.')[0] for proof in failed] if failed: - raise ValueError(f'Running initialization code failed for {len(failed)} contracts: {failed}') + raise ValueError( + f"Running initialization code failed for {len(failed)} contracts: {', '.join(failed_contract_names)}" + ) if options.verbose: _LOGGER.info(f'Running setup functions in parallel: {setup_method_names}') @@ -170,8 +173,9 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False) setup_results = _run_prover(setup_method_tests, include_summaries=False) failed = [proof for proof in setup_results if not proof.passed] + failed_contract_names = [proof.id.split('.')[0] for proof in failed] if failed: - raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}') + raise ValueError(f"Running setUp method failed for {len(failed)} contracts: {', '.join(failed_contract_names)}") if options.verbose: _LOGGER.info(f'Running test functions in parallel: {test_names}') @@ -1440,7 +1444,7 @@ def _final_term( def _process_external_library_references(contract: Contract, foundry_contracts: dict[str, Contract]) -> list[KInner]: """Create a list of KInner accounts for external libraries used in the given contract. - This function identifies external library placeholders within the contract's deployed bytecode, + This function identifies external library placeholders within the contract's bytecode and deployed bytecode, deploys the required external libraries at the address generated based on the first 20 bytes of the hash of the unique id, replaces the placeholders with the actual addresses of the deployed libraries, and returns a list of KEVM account cells representing the deployed external libraries. @@ -1454,39 +1458,51 @@ def _process_external_library_references(contract: Contract, foundry_contracts: external_libs: list[KInner] = [] address_list: dict[str, str] = {} - for lib, ref_locations in contract.external_lib_refs.items(): - ref_contract = foundry_contracts.get(lib) - if ref_contract is None: - raise ValueError(f'External library not found: {lib}') - - if lib not in address_list: - new_address_hex = hash_str(lib)[:40].ljust(40, '0') - new_address_int = int(new_address_hex, 16) - _LOGGER.info(f'Deploying external library {lib} at address 0x{new_address_hex}') - - ref_code = token(bytes.fromhex(ref_contract.deployed_bytecode)) - external_libs.append( - KEVM.account_cell( - id=token(new_address_int), - balance=token(0), - code=ref_code, - storage=map_empty(), - orig_storage=map_empty(), - transient_storage=map_empty(), - nonce=token(0), + for ref_type in ['bytecode_external_lib_refs', 'deployed_bytecode_external_lib_refs']: + lib_refs = getattr(contract, ref_type, {}) + + for lib, ref_locations in lib_refs.items(): + ref_contract = foundry_contracts.get(lib) + if ref_contract is None: + raise ValueError(f'External library not found: {lib}') + + if lib not in address_list: + new_address_hex = hash_str(lib)[:40].ljust(40, '0') + new_address_int = int(new_address_hex, 16) + _LOGGER.info(f'Deploying external library {lib} at address 0x{new_address_hex}') + + # `deployed_bytecode` libraries are a subset of `bytecode` libraries + if ref_contract.bytecode_external_lib_refs: + external_libs.extend(_process_external_library_references(ref_contract, foundry_contracts)) + + ref_code = token(bytes.fromhex(ref_contract.deployed_bytecode)) + external_libs.append( + KEVM.account_cell( + id=token(new_address_int), + balance=token(0), + code=ref_code, + storage=map_empty(), + orig_storage=map_empty(), + transient_storage=map_empty(), + nonce=token(0), + ) ) - ) - address_list[lib] = new_address_hex - else: - new_address_hex = address_list[lib] - - for ref_start, ref_len in ref_locations: - placeholder_start = ref_start * 2 - placeholder_len = ref_len * 2 - contract.deployed_bytecode = ( - contract.deployed_bytecode[:placeholder_start] - + new_address_hex - + contract.deployed_bytecode[placeholder_start + placeholder_len :] - ) + address_list[lib] = new_address_hex + else: + new_address_hex = address_list[lib] + + bytecode_field = 'bytecode' if ref_type == 'bytecode_external_lib_refs' else 'deployed_bytecode' + + for ref_start, ref_len in ref_locations: + placeholder_start = ref_start * 2 + placeholder_len = ref_len * 2 + + current_bytecode = getattr(contract, bytecode_field) + updated_bytecode = ( + current_bytecode[:placeholder_start] + + new_address_hex + + current_bytecode[placeholder_start + placeholder_len :] + ) + setattr(contract, bytecode_field, updated_bytecode) return external_libs diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index fb2a6f2d5..2c8a34181 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -768,7 +768,8 @@ def application(self) -> KInner: deployed_bytecode: str immutable_ranges: list[tuple[int, int]] link_ranges: list[tuple[int, int]] - external_lib_refs: dict[str, list[tuple[int, int]]] + bytecode_external_lib_refs: dict[str, list[tuple[int, int]]] + deployed_bytecode_external_lib_refs: dict[str, list[tuple[int, int]]] processed_link_refs: bool bytecode: str raw_sourcemap: str | None @@ -792,6 +793,7 @@ def __init__(self, contract_name: str, contract_json: dict, foundry: bool = Fals evm = self.contract_json['evm'] if not foundry else self.contract_json deployed_bytecode = evm['deployedBytecode'] + bytecode = evm['bytecode'] self.immutable_ranges = [ (rng['start'], rng['length']) @@ -799,22 +801,30 @@ def __init__(self, contract_name: str, contract_json: dict, foundry: bool = Fals for rng in ref ] - self.external_lib_refs = {} + self.bytecode_external_lib_refs = {} + self.deployed_bytecode_external_lib_refs = {} self.link_ranges = [] - for path, ref in deployed_bytecode.get('linkReferences', {}).items(): - for contract_name, ranges in ref.items(): - ref_name_with_path = contract_name_with_path(path, contract_name) - ranges = [(rng['start'], rng['length']) for rng in ranges] - self.link_ranges.extend(ranges) - self.external_lib_refs.setdefault(ref_name_with_path, []).extend(ranges) + def process_references(bytecode: dict, target_lib_refs: dict, update_link_ranges: bool = False) -> None: + for path, references in bytecode.get('linkReferences', {}).items(): + for contract_name, ranges in references.items(): + ref_name_with_path = contract_name_with_path(path, contract_name) + ranges = [(rng['start'], rng['length']) for rng in ranges] + + target_lib_refs.setdefault(ref_name_with_path, []).extend(ranges) + + if update_link_ranges: + self.link_ranges.extend(ranges) - self.processed_link_refs = len(self.external_lib_refs) == 0 + process_references(bytecode, self.bytecode_external_lib_refs) + process_references(deployed_bytecode, self.deployed_bytecode_external_lib_refs, update_link_ranges=True) + + # `deployed_bytecode_external_lib_refs` is a subset of `bytecode_external_lib_refs` + self.processed_link_refs = len(self.bytecode_external_lib_refs) == 0 self.deployed_bytecode = deployed_bytecode['object'].replace('0x', '') self.raw_sourcemap = deployed_bytecode['sourceMap'] if 'sourceMap' in deployed_bytecode else None - bytecode = evm['bytecode'] self.bytecode = bytecode['object'].replace('0x', '') self.constructor = None diff --git a/src/tests/integration/test-data/foundry-init-code b/src/tests/integration/test-data/foundry-init-code index 17835d018..80fe28095 100644 --- a/src/tests/integration/test-data/foundry-init-code +++ b/src/tests/integration/test-data/foundry-init-code @@ -3,4 +3,5 @@ InitCodeTest.testFail_init() ConstructorArgsTest.test_constructor_args() ConstructorTest.test_constructor() ConstructorTest.testFail_constructor() -ConstructorTest.run_constructor() \ No newline at end of file +ConstructorTest.run_constructor() +ExternalNestedLibraryTest.testExtLibs() \ No newline at end of file diff --git a/src/tests/integration/test-data/foundry/test/ExternalNestedLibraryTest.t.sol b/src/tests/integration/test-data/foundry/test/ExternalNestedLibraryTest.t.sol new file mode 100644 index 000000000..cafa960da --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/ExternalNestedLibraryTest.t.sol @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import {Test, console} from "forge-std/Test.sol"; + +library LibrarySum { + function sum(uint256 a, uint256 b) external pure returns (uint256 res) { + res = a + b; + } +} + +library LibraryEq { + function eq(uint256 a, uint256 b, uint256 c) internal returns (bool res) { + uint256 sum = LibrarySum.sum(a, b); + return (sum == c); + } +} + +contract ExternalNestedLibraryTest is Test { + uint256 public z = 10; + + function testExtLibs() public { + uint256 x = 3; + uint256 y = 7; + bool res = LibraryEq.eq(x, y, z); + assert(res); + } +} diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index 1aee2b0de..87724667e 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -4915,6 +4915,144 @@ module S2KtestZModSimpleMath-CONTRACT rule ( selector ( "square(uint256)" ) => 2066295049 ) +endmodule + +module S2KtestZModExternalNestedLibraryTest-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KtestZModExternalNestedLibraryTestContract + + syntax S2KtestZModExternalNestedLibraryTestContract ::= "S2KtestZModExternalNestedLibraryTest" [symbol("contract_test%ExternalNestedLibraryTest")] + + syntax Bytes ::= S2KtestZModExternalNestedLibraryTestContract "." S2KtestZModExternalNestedLibraryTestMethod [function, symbol("method_test%ExternalNestedLibraryTest")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KISZUndTEST_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeArtifacts_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeContracts_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeSenders_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2Kfailed_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetArtifactSelectors_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetArtifacts_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetContracts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetContracts_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetSelectors_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetSenders_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtestExtLibs" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtestExtLibs_")] + + syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2Kz" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2Kz_")] + + rule ( S2KtestZModExternalNestedLibraryTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2KtestExtLibs ( ) => #abiCallData ( "testExtLibs" , .TypedArgs ) ) + + + rule ( S2KtestZModExternalNestedLibraryTest . S2Kz ( ) => #abiCallData ( "z" , .TypedArgs ) ) + + + rule ( selector ( "IS_TEST()" ) => 4202047188 ) + + + rule ( selector ( "excludeArtifacts()" ) => 3041954473 ) + + + rule ( selector ( "excludeContracts()" ) => 3792478065 ) + + + rule ( selector ( "excludeSenders()" ) => 517440284 ) + + + rule ( selector ( "failed()" ) => 3124842406 ) + + + rule ( selector ( "targetArtifactSelectors()" ) => 1725540768 ) + + + rule ( selector ( "targetArtifacts()" ) => 2233625729 ) + + + rule ( selector ( "targetContracts()" ) => 1064470260 ) + + + rule ( selector ( "targetSelectors()" ) => 2439649222 ) + + + rule ( selector ( "targetSenders()" ) => 1046363171 ) + + + rule ( selector ( "testExtLibs()" ) => 4104885666 ) + + + rule ( selector ( "z()" ) => 3319234606 ) + + +endmodule + +module S2KtestZModLibraryEq-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KtestZModLibraryEqContract + + syntax S2KtestZModLibraryEqContract ::= "S2KtestZModLibraryEq" [symbol("contract_test%LibraryEq")] + +endmodule + +module S2KtestZModLibrarySum-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KtestZModLibrarySumContract + + syntax S2KtestZModLibrarySumContract ::= "S2KtestZModLibrarySum" [symbol("contract_test%LibrarySum")] + + syntax Bytes ::= S2KtestZModLibrarySumContract "." S2KtestZModLibrarySumMethod [function, symbol("method_test%LibrarySum")] + + syntax S2KtestZModLibrarySumMethod ::= "S2Ksum" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol("method_test%LibrarySum_S2Ksum_uint256_uint256")] + + rule ( S2KtestZModLibrarySum . S2Ksum ( V0_a : uint256 , V1_b : uint256 ) => #abiCallData ( "sum" , ( #uint256 ( V0_a ) , ( #uint256 ( V1_b ) , .TypedArgs ) ) ) ) + ensures ( #rangeUInt ( 256 , V0_a ) + andBool ( #rangeUInt ( 256 , V1_b ) + )) + + + rule ( selector ( "sum(uint256,uint256)" ) => 3402664347 ) + + endmodule module S2KtestZModFfiTest-CONTRACT diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected index 1dc9977be..31f7579ac 100644 --- a/src/tests/integration/test-data/show/foundry.k.expected +++ b/src/tests/integration/test-data/show/foundry.k.expected @@ -65,6 +65,9 @@ module FOUNDRY-MAIN imports public S2KtestZModReverterWithReturn-VERIFICATION imports public S2KtestZModExternalLibTest-VERIFICATION imports public S2KtestZModSimpleMath-VERIFICATION + imports public S2KtestZModExternalNestedLibraryTest-VERIFICATION + imports public S2KtestZModLibraryEq-VERIFICATION + imports public S2KtestZModLibrarySum-VERIFICATION imports public S2KtestZModFfiTest-VERIFICATION imports public S2KtestZModFilesTest-VERIFICATION imports public S2KtestZModForkTest-VERIFICATION @@ -584,6 +587,27 @@ module S2KtestZModSimpleMath-VERIFICATION +endmodule + +module S2KtestZModExternalNestedLibraryTest-VERIFICATION + imports public S2KtestZModExternalNestedLibraryTest-CONTRACT + + + +endmodule + +module S2KtestZModLibraryEq-VERIFICATION + imports public S2KtestZModLibraryEq-CONTRACT + + + +endmodule + +module S2KtestZModLibrarySum-VERIFICATION + imports public S2KtestZModLibrarySum-CONTRACT + + + endmodule module S2KtestZModFfiTest-VERIFICATION