Skip to content

Commit 05934f6

Browse files
palinatolmachanvacaru
palinatolmach
and
anvacaru
authored
Extend library refs processing, fix in error messages for setUp (#861)
* 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 <[email protected]>
1 parent 9fa22ce commit 05934f6

File tree

6 files changed

+264
-47
lines changed

6 files changed

+264
-47
lines changed

‎src/kontrol/prove.py

Lines changed: 52 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -159,8 +159,11 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
159159

160160
constructor_results = _run_prover(constructor_tests, include_summaries=False)
161161
failed = [proof for proof in constructor_results if not proof.passed]
162+
failed_contract_names = [proof.id.split('.')[0] for proof in failed]
162163
if failed:
163-
raise ValueError(f'Running initialization code failed for {len(failed)} contracts: {failed}')
164+
raise ValueError(
165+
f"Running initialization code failed for {len(failed)} contracts: {', '.join(failed_contract_names)}"
166+
)
164167

165168
if options.verbose:
166169
_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)
170173
setup_results = _run_prover(setup_method_tests, include_summaries=False)
171174

172175
failed = [proof for proof in setup_results if not proof.passed]
176+
failed_contract_names = [proof.id.split('.')[0] for proof in failed]
173177
if failed:
174-
raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}')
178+
raise ValueError(f"Running setUp method failed for {len(failed)} contracts: {', '.join(failed_contract_names)}")
175179

176180
if options.verbose:
177181
_LOGGER.info(f'Running test functions in parallel: {test_names}')
@@ -1440,7 +1444,7 @@ def _final_term(
14401444
def _process_external_library_references(contract: Contract, foundry_contracts: dict[str, Contract]) -> list[KInner]:
14411445
"""Create a list of KInner accounts for external libraries used in the given contract.
14421446
1443-
This function identifies external library placeholders within the contract's deployed bytecode,
1447+
This function identifies external library placeholders within the contract's bytecode and deployed bytecode,
14441448
deploys the required external libraries at the address generated based on the first 20 bytes of the hash of the
14451449
unique id, replaces the placeholders with the actual addresses of the deployed libraries, and returns a list of
14461450
KEVM account cells representing the deployed external libraries.
@@ -1454,39 +1458,51 @@ def _process_external_library_references(contract: Contract, foundry_contracts:
14541458
external_libs: list[KInner] = []
14551459
address_list: dict[str, str] = {}
14561460

1457-
for lib, ref_locations in contract.external_lib_refs.items():
1458-
ref_contract = foundry_contracts.get(lib)
1459-
if ref_contract is None:
1460-
raise ValueError(f'External library not found: {lib}')
1461-
1462-
if lib not in address_list:
1463-
new_address_hex = hash_str(lib)[:40].ljust(40, '0')
1464-
new_address_int = int(new_address_hex, 16)
1465-
_LOGGER.info(f'Deploying external library {lib} at address 0x{new_address_hex}')
1466-
1467-
ref_code = token(bytes.fromhex(ref_contract.deployed_bytecode))
1468-
external_libs.append(
1469-
KEVM.account_cell(
1470-
id=token(new_address_int),
1471-
balance=token(0),
1472-
code=ref_code,
1473-
storage=map_empty(),
1474-
orig_storage=map_empty(),
1475-
transient_storage=map_empty(),
1476-
nonce=token(0),
1461+
for ref_type in ['bytecode_external_lib_refs', 'deployed_bytecode_external_lib_refs']:
1462+
lib_refs = getattr(contract, ref_type, {})
1463+
1464+
for lib, ref_locations in lib_refs.items():
1465+
ref_contract = foundry_contracts.get(lib)
1466+
if ref_contract is None:
1467+
raise ValueError(f'External library not found: {lib}')
1468+
1469+
if lib not in address_list:
1470+
new_address_hex = hash_str(lib)[:40].ljust(40, '0')
1471+
new_address_int = int(new_address_hex, 16)
1472+
_LOGGER.info(f'Deploying external library {lib} at address 0x{new_address_hex}')
1473+
1474+
# `deployed_bytecode` libraries are a subset of `bytecode` libraries
1475+
if ref_contract.bytecode_external_lib_refs:
1476+
external_libs.extend(_process_external_library_references(ref_contract, foundry_contracts))
1477+
1478+
ref_code = token(bytes.fromhex(ref_contract.deployed_bytecode))
1479+
external_libs.append(
1480+
KEVM.account_cell(
1481+
id=token(new_address_int),
1482+
balance=token(0),
1483+
code=ref_code,
1484+
storage=map_empty(),
1485+
orig_storage=map_empty(),
1486+
transient_storage=map_empty(),
1487+
nonce=token(0),
1488+
)
14771489
)
1478-
)
1479-
address_list[lib] = new_address_hex
1480-
else:
1481-
new_address_hex = address_list[lib]
1482-
1483-
for ref_start, ref_len in ref_locations:
1484-
placeholder_start = ref_start * 2
1485-
placeholder_len = ref_len * 2
1486-
contract.deployed_bytecode = (
1487-
contract.deployed_bytecode[:placeholder_start]
1488-
+ new_address_hex
1489-
+ contract.deployed_bytecode[placeholder_start + placeholder_len :]
1490-
)
1490+
address_list[lib] = new_address_hex
1491+
else:
1492+
new_address_hex = address_list[lib]
1493+
1494+
bytecode_field = 'bytecode' if ref_type == 'bytecode_external_lib_refs' else 'deployed_bytecode'
1495+
1496+
for ref_start, ref_len in ref_locations:
1497+
placeholder_start = ref_start * 2
1498+
placeholder_len = ref_len * 2
1499+
1500+
current_bytecode = getattr(contract, bytecode_field)
1501+
updated_bytecode = (
1502+
current_bytecode[:placeholder_start]
1503+
+ new_address_hex
1504+
+ current_bytecode[placeholder_start + placeholder_len :]
1505+
)
1506+
setattr(contract, bytecode_field, updated_bytecode)
14911507

14921508
return external_libs

‎src/kontrol/solc_to_k.py

Lines changed: 20 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -768,7 +768,8 @@ def application(self) -> KInner:
768768
deployed_bytecode: str
769769
immutable_ranges: list[tuple[int, int]]
770770
link_ranges: list[tuple[int, int]]
771-
external_lib_refs: dict[str, list[tuple[int, int]]]
771+
bytecode_external_lib_refs: dict[str, list[tuple[int, int]]]
772+
deployed_bytecode_external_lib_refs: dict[str, list[tuple[int, int]]]
772773
processed_link_refs: bool
773774
bytecode: str
774775
raw_sourcemap: str | None
@@ -792,29 +793,38 @@ def __init__(self, contract_name: str, contract_json: dict, foundry: bool = Fals
792793
evm = self.contract_json['evm'] if not foundry else self.contract_json
793794

794795
deployed_bytecode = evm['deployedBytecode']
796+
bytecode = evm['bytecode']
795797

796798
self.immutable_ranges = [
797799
(rng['start'], rng['length'])
798800
for ref in deployed_bytecode.get('immutableReferences', {}).values()
799801
for rng in ref
800802
]
801803

802-
self.external_lib_refs = {}
804+
self.bytecode_external_lib_refs = {}
805+
self.deployed_bytecode_external_lib_refs = {}
803806
self.link_ranges = []
804807

805-
for path, ref in deployed_bytecode.get('linkReferences', {}).items():
806-
for contract_name, ranges in ref.items():
807-
ref_name_with_path = contract_name_with_path(path, contract_name)
808-
ranges = [(rng['start'], rng['length']) for rng in ranges]
809-
self.link_ranges.extend(ranges)
810-
self.external_lib_refs.setdefault(ref_name_with_path, []).extend(ranges)
808+
def process_references(bytecode: dict, target_lib_refs: dict, update_link_ranges: bool = False) -> None:
809+
for path, references in bytecode.get('linkReferences', {}).items():
810+
for contract_name, ranges in references.items():
811+
ref_name_with_path = contract_name_with_path(path, contract_name)
812+
ranges = [(rng['start'], rng['length']) for rng in ranges]
813+
814+
target_lib_refs.setdefault(ref_name_with_path, []).extend(ranges)
815+
816+
if update_link_ranges:
817+
self.link_ranges.extend(ranges)
811818

812-
self.processed_link_refs = len(self.external_lib_refs) == 0
819+
process_references(bytecode, self.bytecode_external_lib_refs)
820+
process_references(deployed_bytecode, self.deployed_bytecode_external_lib_refs, update_link_ranges=True)
821+
822+
# `deployed_bytecode_external_lib_refs` is a subset of `bytecode_external_lib_refs`
823+
self.processed_link_refs = len(self.bytecode_external_lib_refs) == 0
813824

814825
self.deployed_bytecode = deployed_bytecode['object'].replace('0x', '')
815826
self.raw_sourcemap = deployed_bytecode['sourceMap'] if 'sourceMap' in deployed_bytecode else None
816827

817-
bytecode = evm['bytecode']
818828
self.bytecode = bytecode['object'].replace('0x', '')
819829
self.constructor = None
820830

‎src/tests/integration/test-data/foundry-init-code

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,5 @@ InitCodeTest.testFail_init()
33
ConstructorArgsTest.test_constructor_args()
44
ConstructorTest.test_constructor()
55
ConstructorTest.testFail_constructor()
6-
ConstructorTest.run_constructor()
6+
ConstructorTest.run_constructor()
7+
ExternalNestedLibraryTest.testExtLibs()

‎src/tests/integration/test-data/foundry/test/ExternalNestedLibraryTest.t.sol

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// SPDX-License-Identifier: UNLICENSED
2+
pragma solidity ^0.8.13;
3+
4+
import {Test, console} from "forge-std/Test.sol";
5+
6+
library LibrarySum {
7+
function sum(uint256 a, uint256 b) external pure returns (uint256 res) {
8+
res = a + b;
9+
}
10+
}
11+
12+
library LibraryEq {
13+
function eq(uint256 a, uint256 b, uint256 c) internal returns (bool res) {
14+
uint256 sum = LibrarySum.sum(a, b);
15+
return (sum == c);
16+
}
17+
}
18+
19+
contract ExternalNestedLibraryTest is Test {
20+
uint256 public z = 10;
21+
22+
function testExtLibs() public {
23+
uint256 x = 3;
24+
uint256 y = 7;
25+
bool res = LibraryEq.eq(x, y, z);
26+
assert(res);
27+
}
28+
}

‎src/tests/integration/test-data/show/contracts.k.expected

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4915,6 +4915,144 @@ module S2KtestZModSimpleMath-CONTRACT
49154915
rule ( selector ( "square(uint256)" ) => 2066295049 )
49164916

49174917

4918+
endmodule
4919+
4920+
module S2KtestZModExternalNestedLibraryTest-CONTRACT
4921+
imports public FOUNDRY
4922+
4923+
syntax Contract ::= S2KtestZModExternalNestedLibraryTestContract
4924+
4925+
syntax S2KtestZModExternalNestedLibraryTestContract ::= "S2KtestZModExternalNestedLibraryTest" [symbol("contract_test%ExternalNestedLibraryTest")]
4926+
4927+
syntax Bytes ::= S2KtestZModExternalNestedLibraryTestContract "." S2KtestZModExternalNestedLibraryTestMethod [function, symbol("method_test%ExternalNestedLibraryTest")]
4928+
4929+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KISZUndTEST_")]
4930+
4931+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeArtifacts_")]
4932+
4933+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeContracts_")]
4934+
4935+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeSenders_")]
4936+
4937+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2Kfailed_")]
4938+
4939+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetArtifactSelectors_")]
4940+
4941+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetArtifacts_")]
4942+
4943+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetContracts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetContracts_")]
4944+
4945+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetSelectors_")]
4946+
4947+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetSenders_")]
4948+
4949+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtestExtLibs" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtestExtLibs_")]
4950+
4951+
syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2Kz" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2Kz_")]
4952+
4953+
rule ( S2KtestZModExternalNestedLibraryTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
4954+
4955+
4956+
rule ( S2KtestZModExternalNestedLibraryTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
4957+
4958+
4959+
rule ( S2KtestZModExternalNestedLibraryTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
4960+
4961+
4962+
rule ( S2KtestZModExternalNestedLibraryTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
4963+
4964+
4965+
rule ( S2KtestZModExternalNestedLibraryTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
4966+
4967+
4968+
rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
4969+
4970+
4971+
rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
4972+
4973+
4974+
rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
4975+
4976+
4977+
rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
4978+
4979+
4980+
rule ( S2KtestZModExternalNestedLibraryTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
4981+
4982+
4983+
rule ( S2KtestZModExternalNestedLibraryTest . S2KtestExtLibs ( ) => #abiCallData ( "testExtLibs" , .TypedArgs ) )
4984+
4985+
4986+
rule ( S2KtestZModExternalNestedLibraryTest . S2Kz ( ) => #abiCallData ( "z" , .TypedArgs ) )
4987+
4988+
4989+
rule ( selector ( "IS_TEST()" ) => 4202047188 )
4990+
4991+
4992+
rule ( selector ( "excludeArtifacts()" ) => 3041954473 )
4993+
4994+
4995+
rule ( selector ( "excludeContracts()" ) => 3792478065 )
4996+
4997+
4998+
rule ( selector ( "excludeSenders()" ) => 517440284 )
4999+
5000+
5001+
rule ( selector ( "failed()" ) => 3124842406 )
5002+
5003+
5004+
rule ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
5005+
5006+
5007+
rule ( selector ( "targetArtifacts()" ) => 2233625729 )
5008+
5009+
5010+
rule ( selector ( "targetContracts()" ) => 1064470260 )
5011+
5012+
5013+
rule ( selector ( "targetSelectors()" ) => 2439649222 )
5014+
5015+
5016+
rule ( selector ( "targetSenders()" ) => 1046363171 )
5017+
5018+
5019+
rule ( selector ( "testExtLibs()" ) => 4104885666 )
5020+
5021+
5022+
rule ( selector ( "z()" ) => 3319234606 )
5023+
5024+
5025+
endmodule
5026+
5027+
module S2KtestZModLibraryEq-CONTRACT
5028+
imports public FOUNDRY
5029+
5030+
syntax Contract ::= S2KtestZModLibraryEqContract
5031+
5032+
syntax S2KtestZModLibraryEqContract ::= "S2KtestZModLibraryEq" [symbol("contract_test%LibraryEq")]
5033+
5034+
endmodule
5035+
5036+
module S2KtestZModLibrarySum-CONTRACT
5037+
imports public FOUNDRY
5038+
5039+
syntax Contract ::= S2KtestZModLibrarySumContract
5040+
5041+
syntax S2KtestZModLibrarySumContract ::= "S2KtestZModLibrarySum" [symbol("contract_test%LibrarySum")]
5042+
5043+
syntax Bytes ::= S2KtestZModLibrarySumContract "." S2KtestZModLibrarySumMethod [function, symbol("method_test%LibrarySum")]
5044+
5045+
syntax S2KtestZModLibrarySumMethod ::= "S2Ksum" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol("method_test%LibrarySum_S2Ksum_uint256_uint256")]
5046+
5047+
rule ( S2KtestZModLibrarySum . S2Ksum ( V0_a : uint256 , V1_b : uint256 ) => #abiCallData ( "sum" , ( #uint256 ( V0_a ) , ( #uint256 ( V1_b ) , .TypedArgs ) ) ) )
5048+
ensures ( #rangeUInt ( 256 , V0_a )
5049+
andBool ( #rangeUInt ( 256 , V1_b )
5050+
))
5051+
5052+
5053+
rule ( selector ( "sum(uint256,uint256)" ) => 3402664347 )
5054+
5055+
49185056
endmodule
49195057

49205058
module S2KtestZModFfiTest-CONTRACT

‎src/tests/integration/test-data/show/foundry.k.expected

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,9 @@ module FOUNDRY-MAIN
6565
imports public S2KtestZModReverterWithReturn-VERIFICATION
6666
imports public S2KtestZModExternalLibTest-VERIFICATION
6767
imports public S2KtestZModSimpleMath-VERIFICATION
68+
imports public S2KtestZModExternalNestedLibraryTest-VERIFICATION
69+
imports public S2KtestZModLibraryEq-VERIFICATION
70+
imports public S2KtestZModLibrarySum-VERIFICATION
6871
imports public S2KtestZModFfiTest-VERIFICATION
6972
imports public S2KtestZModFilesTest-VERIFICATION
7073
imports public S2KtestZModForkTest-VERIFICATION
@@ -584,6 +587,27 @@ module S2KtestZModSimpleMath-VERIFICATION
584587

585588

586589

590+
endmodule
591+
592+
module S2KtestZModExternalNestedLibraryTest-VERIFICATION
593+
imports public S2KtestZModExternalNestedLibraryTest-CONTRACT
594+
595+
596+
597+
endmodule
598+
599+
module S2KtestZModLibraryEq-VERIFICATION
600+
imports public S2KtestZModLibraryEq-CONTRACT
601+
602+
603+
604+
endmodule
605+
606+
module S2KtestZModLibrarySum-VERIFICATION
607+
imports public S2KtestZModLibrarySum-CONTRACT
608+
609+
610+
587611
endmodule
588612

589613
module S2KtestZModFfiTest-VERIFICATION

0 commit comments

Comments
 (0)