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

@@ -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):

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()

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()

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);
+    }
 }

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