merge_node Support (#829)

* update copytree * introduce solidity code * add some comments * comment * replace copy_tree by copytree for py3.12 * fix * dirs_exist_ok=True * delete test * fix copytree * provide `merge` option for `minimize_proof` * provide `Branches` contract for merging node testing * add a test for merging node * add arguments to the parser * test configuration for merging node * make format/check * submit the expected * fix for kompile * fix kompile * fix `cse tests` * fix * fix * add endmodule * fix constracts.k.expected * fix * fix * Update help message for node merging Co-authored-by: JianHong Zhao <[email protected]> --------- Co-authored-by: Palina <[email protected]>
runtimeverification · Nov 13, 2024 · 0493bd4 · 0493bd4
1 parent b642aab
commit 0493bd4
Show file tree

Hide file tree

Showing 14 changed files with 1,913 additions and 11 deletions.
diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py
@@ -692,7 +692,7 @@ def parse(s: str) -> list[T]:
         help='Print elements in hexadecimal encoding.',
     )
 
-    command_parser.add_parser(
+    minimize_proof_args = command_parser.add_parser(
         'minimize-proof',
         help='Minimize the KCFG of the proof for a given test.',
         parents=[
@@ -702,6 +702,13 @@ def parse(s: str) -> list[T]:
             config_args.config_args,
         ],
     )
+    minimize_proof_args.add_argument(
+        '--merge',
+        dest='merge',
+        default=None,
+        action='store_true',
+        help='Merge the nodes of the KCFG into a successful branch and a revert branch.',
+    )
 
     remove_node = command_parser.add_parser(
         'remove-node',

diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -1034,7 +1034,7 @@ def foundry_to_xml(foundry: Foundry, proofs: list[APRProof]) -> None:
 def foundry_minimize_proof(foundry: Foundry, options: MinimizeProofOptions) -> None:
     test_id = foundry.get_test_id(options.test, options.version)
     apr_proof = foundry.get_apr_proof(test_id)
-    apr_proof.minimize_kcfg()
+    apr_proof.minimize_kcfg(merge=options.merge)
     apr_proof.write_proof_data()
 
 

diff --git a/src/kontrol/options.py b/src/kontrol/options.py
@@ -328,6 +328,13 @@ def get_argument_type() -> dict[str, Callable]:
 
 
 class MinimizeProofOptions(FoundryTestOptions, LoggingOptions, FoundryOptions):
+    merge: bool
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'merge': False,
+        }
 
     @staticmethod
     def from_option_string() -> dict[str, str]:

diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py
@@ -1,7 +1,7 @@
 from __future__ import annotations
 
-from distutils.dir_util import copy_tree
 from functools import partial
+from shutil import copytree
 from typing import TYPE_CHECKING
 
 import pytest
@@ -64,7 +64,7 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
     foundry_root = root_tmp_dir / 'foundry'
     with FileLock(str(foundry_root) + '.lock'):
         if not foundry_root.is_dir():
-            copy_tree(str(TEST_DATA_DIR / 'foundry'), str(foundry_root))
+            copytree(str(TEST_DATA_DIR / 'foundry'), str(foundry_root), dirs_exist_ok=True)
 
             run_process_2(['forge', 'install', '--no-git', f'foundry-rs/forge-std@{FORGE_STD_REF}'], cwd=foundry_root)
             run_process_2(
@@ -98,5 +98,5 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
             )
 
     session_foundry_root = tmp_path_factory.mktemp('foundry')
-    copy_tree(str(foundry_root), str(session_foundry_root))
+    copytree(str(foundry_root), str(session_foundry_root), dirs_exist_ok=True)
     return Foundry(session_foundry_root, add_enum_constraints=True)
diff --git a/src/tests/integration/test-data/foundry-minimize b/src/tests/integration/test-data/foundry-minimize
@@ -2,3 +2,4 @@ AssertTest.test_assert_false()
 AssertTest.testFail_expect_revert()
 AssertTest.test_failing_branch(uint256)
 AssertTest.test_revert_branch(uint256,uint256)
+MergeKCFGTest.test_branch_merge(uint256,uint256,bool)
diff --git a/src/tests/integration/test-data/foundry-minimize-merge b/src/tests/integration/test-data/foundry-minimize-merge
@@ -0,0 +1 @@
+MergeKCFGTest.test_branch_merge(uint256,uint256,bool)
diff --git a/src/tests/integration/test-data/foundry/src/Branches.sol b/src/tests/integration/test-data/foundry/src/Branches.sol
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+
+// CSE challenge: multiple branches that slow down the verification
+contract Branches{
+    function applyOp(uint256 x, uint256 y, bool z) public returns (uint256) {
+        if (z) {
+            return x + y;
+        } else {
+            return x * y;
+        }
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/test/MergeKCFGTest.t.sol b/src/tests/integration/test-data/foundry/test/MergeKCFGTest.t.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+import "src/Branches.sol";
+
+contract MergeKCFGTest is Test {
+    Branches c;
+
+    function setUp() external {
+        c = new Branches();
+    }
+
+    function test_branch_merge(uint256 x, uint256 y, bool z) external{
+        vm.assume(x <= type(uint256).max - y);
+        try c.applyOp(x, y, z) returns (uint256 res) {
+            // This check will fail if the backend cannot recover the preds in the merged postcondition
+            // If so, assert res == x + y | res == x * y will pass
+            // If so, we should not always use merge_node, but provide both on need.
+            if (z) {
+                assert(res == x + y);
+            } else {
+                assert(res == x * y);
+            }
+        } catch {
+            assert(x != 0 && 2 ** 62 / x < y && !z);
+        }
+    }
+}
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
@@ -2212,6 +2212,29 @@ module S2KtestZModWarpTest-CONTRACT
     rule  ( selector ( "test_warp_setup()" ) => 1375900050 )
 
 
+endmodule
+
+module S2KsrcZModBranches-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KsrcZModBranchesContract
+
+    syntax S2KsrcZModBranchesContract ::= "S2KsrcZModBranches" [symbol("contract_src%Branches")]
+
+    syntax Bytes ::= S2KsrcZModBranchesContract "." S2KsrcZModBranchesMethod [function, symbol("method_src%Branches")]
+
+    syntax S2KsrcZModBranchesMethod ::= "S2KapplyOp" "(" Int ":" "uint256" "," Int ":" "uint256" "," Int ":" "bool" ")" [symbol("method_src%Branches_S2KapplyOp_uint256_uint256_bool")]
+
+    rule  ( S2KsrcZModBranches . S2KapplyOp ( KV0_x : uint256 , KV1_y : uint256 , KV2_z : bool ) => #abiCallData ( "applyOp" , ( #uint256 ( KV0_x ) , ( #uint256 ( KV1_y ) , ( #bool ( KV2_z ) , .TypedArgs ) ) ) ) )
+       ensures ( #rangeUInt ( 256 , KV0_x )
+       andBool ( #rangeUInt ( 256 , KV1_y )
+       andBool ( #rangeBool ( KV2_z )
+               )))
+
+
+    rule  ( selector ( "applyOp(uint256,uint256,bool)" ) => 3766377623 )
+
+
 endmodule
 
 module S2KtestZModBroadcastTest-CONTRACT
@@ -7652,6 +7675,117 @@ module S2KtestZModMergeTest-CONTRACT
     rule  ( selector ( "test_branch_merge(uint256)" ) => 1000659212 )
 
 
+endmodule
+
+module S2KtestZModMergeKCFGTest-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KtestZModMergeKCFGTestContract
+
+    syntax S2KtestZModMergeKCFGTestContract ::= "S2KtestZModMergeKCFGTest" [symbol("contract_test%MergeKCFGTest")]
+
+    syntax Bytes ::= S2KtestZModMergeKCFGTestContract "." S2KtestZModMergeKCFGTestMethod [function, symbol("method_test%MergeKCFGTest")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol("method_test%MergeKCFGTest_S2KISZUndTEST_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KexcludeArtifacts_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KexcludeContracts_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol("method_test%MergeKCFGTest_S2KexcludeSenders_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%MergeKCFGTest_S2Kfailed_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KsetUp" "(" ")" [symbol("method_test%MergeKCFGTest_S2KsetUp_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetArtifactSelectors_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetArtifacts_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetContracts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetContracts_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetSelectors_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetSenders_")]
+
+    syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtestZUndbranchZUndmerge" "(" Int ":" "uint256" "," Int ":" "uint256" "," Int ":" "bool" ")" [symbol("method_test%MergeKCFGTest_S2KtestZUndbranchZUndmerge_uint256_uint256_bool")]
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KsetUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModMergeKCFGTest . S2KtestZUndbranchZUndmerge ( KV0_x : uint256 , KV1_y : uint256 , KV2_z : bool ) => #abiCallData ( "test_branch_merge" , ( #uint256 ( KV0_x ) , ( #uint256 ( KV1_y ) , ( #bool ( KV2_z ) , .TypedArgs ) ) ) ) )
+       ensures ( #rangeUInt ( 256 , KV0_x )
+       andBool ( #rangeUInt ( 256 , KV1_y )
+       andBool ( #rangeBool ( KV2_z )
+               )))
+
+
+    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
+
+
+    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
+
+
+    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
+
+
+    rule  ( selector ( "excludeSenders()" ) => 517440284 )
+
+
+    rule  ( selector ( "failed()" ) => 3124842406 )
+
+
+    rule  ( selector ( "setUp()" ) => 177362148 )
+
+
+    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
+
+
+    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
+
+
+    rule  ( selector ( "targetContracts()" ) => 1064470260 )
+
+
+    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
+
+
+    rule  ( selector ( "targetSenders()" ) => 1046363171 )
+
+
+    rule  ( selector ( "test_branch_merge(uint256,uint256,bool)" ) => 357868196 )
+
+
 endmodule
 
 module S2KtestZModMethodDisambiguateTest-CONTRACT

diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
@@ -31,6 +31,7 @@ module FOUNDRY-MAIN
     imports public S2KtestZModFeeTest-VERIFICATION
     imports public S2KtestZModRollTest-VERIFICATION
     imports public S2KtestZModWarpTest-VERIFICATION
+    imports public S2KsrcZModBranches-VERIFICATION
     imports public S2KtestZModBroadcastTest-VERIFICATION
     imports public S2KtestZModCSETest-VERIFICATION
     imports public S2KtestZModStaticCallContract-VERIFICATION
@@ -95,6 +96,7 @@ module FOUNDRY-MAIN
     imports public S2KsrcZModLoadStateDumpCode-VERIFICATION
     imports public S2KtestZModLoopsTest-VERIFICATION
     imports public S2KtestZModMergeTest-VERIFICATION
+    imports public S2KtestZModMergeKCFGTest-VERIFICATION
     imports public S2KtestZModMethodDisambiguateTest-VERIFICATION
     imports public S2KsrcZModMock-VERIFICATION
     imports public S2KsrcZModNestedMock-VERIFICATION
@@ -343,6 +345,13 @@ module S2KtestZModWarpTest-VERIFICATION
 
 
 
+endmodule
+
+module S2KsrcZModBranches-VERIFICATION
+    imports public S2KsrcZModBranches-CONTRACT
+
+
+
 endmodule
 
 module S2KtestZModBroadcastTest-VERIFICATION
@@ -794,6 +803,13 @@ module S2KtestZModMergeTest-VERIFICATION
 
 
 
+endmodule
+
+module S2KtestZModMergeKCFGTest-VERIFICATION
+    imports public S2KtestZModMergeKCFGTest-CONTRACT
+
+
+
 endmodule
 
 module S2KtestZModMethodDisambiguateTest-VERIFICATION
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		MergeKCFGTest.test_branch_merge(uint256,uint256,bool)