From eb5f0ca3b84ba1c0b017448a0ad76a481c6e9f3f Mon Sep 17 00:00:00 2001 From: Palina Date: Mon, 16 Dec 2024 14:02:27 +0400 Subject: [PATCH] Set `processed_link_refs` to `true` only in `setup` or constructor (#916) * Set `processed_link_refs` to `true` only in `setup` or constructor * Add a second test to `ExternalLibTest` * Update expected output * Update `testSum` with necessary assumptions * Another simplification to `testSum` * update-expected-output * Fix `ExternalLibTest.testSum` signature --------- Co-authored-by: Andrei <16517508+anvacaru@users.noreply.github.com> --- src/kontrol/prove.py | 3 ++- .../integration/test-data/foundry-prove-all | 1 + .../test-data/foundry-prove-skip-legacy | 1 + .../foundry/test/ExternalLibTest.t.sol | 11 +++++++++++ .../test-data/show/contracts.k.expected | 19 +++++++++++++++++++ 5 files changed, 34 insertions(+), 1 deletion(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 58fa15991..56ff8f9c2 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -712,7 +712,8 @@ def _method_to_cfg( if not contract.processed_link_refs: external_libs = _process_external_library_references(contract, foundry.contracts) - contract.processed_link_refs = True + if method.is_setup or isinstance(method, Contract.Constructor): + contract.processed_link_refs = True contract_code = bytes.fromhex(contract.deployed_bytecode) if isinstance(method, Contract.Constructor): diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index e7add4429..2e5edf0b8 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/src/tests/integration/test-data/foundry-prove-all @@ -115,6 +115,7 @@ ExpectRevertTest.testFail_ExpectRevert_failAndSuccess() ExpectRevertTest.testFail_expectRevert_false() ExpectRevertTest.testFail_expectRevert_multipleReverts() ExternalLibTest.testSquare(uint256) +ExternalLibTest.testSum() FeeTest.test_fee_setup() FfiTest.testffi() FfiTest.testFFIFOO() diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy index 830527671..ddf75f0b1 100644 --- a/src/tests/integration/test-data/foundry-prove-skip-legacy +++ b/src/tests/integration/test-data/foundry-prove-skip-legacy @@ -103,6 +103,7 @@ ExpectRevertTest.testFail_ExpectRevert_failAndSuccess() ExpectRevertTest.testFail_expectRevert_false() ExpectRevertTest.testFail_expectRevert_multipleReverts() ExternalLibTest.testSquare(uint256) +ExternalLibTest.testSum() FeeTest.test_fee_setup() FfiTest.testffi() FfiTest.testFFIFOO() diff --git a/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol b/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol index 947bf243a..a0044b33a 100644 --- a/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol @@ -16,6 +16,10 @@ library SimpleMath { function square(uint256 x) public pure returns (uint256) { return x * x; } + + function sum(uint256 a, uint256 b) external pure returns (uint256 res) { + res = a + b; + } } contract ExternalLibTest is Test { @@ -24,4 +28,11 @@ contract ExternalLibTest is Test { vm.assume(n <= type(uint128).max); assertEq(SimpleMath.square(n), n * n); } + + function testSum() public { + vm.assume(msg.sender == address(110)); + uint256 x = 3; + uint256 y = 7; + assertEq(SimpleMath.sum(x, y), 10); + } } diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index 36b2ac7fc..7221dc48f 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -4862,6 +4862,8 @@ module S2KtestZModExternalLibTest-CONTRACT syntax S2KtestZModExternalLibTestMethod ::= "S2KtestSquare" "(" Int ":" "uint256" ")" [symbol("method_test%ExternalLibTest_S2KtestSquare_uint256")] + syntax S2KtestZModExternalLibTestMethod ::= "S2KtestSum" "(" ")" [symbol("method_test%ExternalLibTest_S2KtestSum_")] + rule ( S2KtestZModExternalLibTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) @@ -4896,6 +4898,9 @@ module S2KtestZModExternalLibTest-CONTRACT ensures #rangeUInt ( 256 , KV0_n ) + rule ( S2KtestZModExternalLibTest . S2KtestSum ( ) => #abiCallData ( "testSum" , .TypedArgs ) ) + + rule ( selector ( "IS_TEST()" ) => 4202047188 ) @@ -4928,6 +4933,9 @@ module S2KtestZModExternalLibTest-CONTRACT rule ( selector ( "testSquare(uint256)" ) => 1753280186 ) + + rule ( selector ( "testSum()" ) => 2036188522 ) + endmodule @@ -4944,6 +4952,8 @@ module S2KtestZModSimpleMath-CONTRACT syntax S2KtestZModSimpleMathMethod ::= "S2KstructInput" "(" Int ":" "uint256" "," Int ":" "address" ")" [symbol("method_test%SimpleMath_S2KstructInput_uint256_address")] + syntax S2KtestZModSimpleMathMethod ::= "S2Ksum" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol("method_test%SimpleMath_S2Ksum_uint256_uint256")] + rule ( S2KtestZModSimpleMath . S2Ksquare ( KV0_x : uint256 ) => #abiCallData ( "square" , ( #uint256 ( KV0_x ) , .TypedArgs ) ) ) ensures #rangeUInt ( 256 , KV0_x ) @@ -4954,11 +4964,20 @@ module S2KtestZModSimpleMath-CONTRACT )) + rule ( S2KtestZModSimpleMath . S2Ksum ( KV0_a : uint256 , KV1_b : uint256 ) => #abiCallData ( "sum" , ( #uint256 ( KV0_a ) , ( #uint256 ( KV1_b ) , .TypedArgs ) ) ) ) + ensures ( #rangeUInt ( 256 , KV0_a ) + andBool ( #rangeUInt ( 256 , KV1_b ) + )) + + rule ( selector ( "square(uint256)" ) => 2066295049 ) rule ( selector ( "structInput(SimpleMath.LibStruct)" ) => 1313163024 ) + + rule ( selector ( "sum(uint256,uint256)" ) => 3402664347 ) + endmodule