Add foundry-merge-nodes option

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.263"
+version = "1.0.264"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kontrol/foundry.py

@@ -629,11 +629,11 @@ def _init_and_run_proof(_init_problem: tuple[str, str]) -> tuple[bool, list[str]
             contract = foundry.contracts[contract_name]
             method = contract.method_by_sig[method_sig]
             proof = _method_to_apr_proof(
-                foundry,
-                contract,
-                method,
-                save_directory,
-                kcfg_explore,
+                foundry=foundry,
+                contract=contract,
+                method=method,
+                save_directory=save_directory,
+                kcfg_explore=kcfg_explore,
                 reinit=(method.qualified_name in out_of_date_methods),
                 simplify_init=simplify_init,
                 bmc_depth=bmc_depth,
@@ -813,6 +813,53 @@ def foundry_simplify_node(
     return foundry.kevm.pretty_print(res_term, unalias=False, sort_collections=sort_collections)
 
 
+def foundry_merge_nodes(
+    foundry_root: Path,
+    test: str,
+    node_ids: Iterable[NodeIdLike],
+    bug_report: bool = False,
+    include_disjunct: bool = False,
+) -> None:
+    def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
+        nodes = list(nodes)
+        if len(nodes) < 2:
+            return True
+        cell_value = nodes[0].cterm.cell(cell)
+        for node in nodes[1:]:
+            if cell_value != node.cterm.cell(cell):
+                return False
+        return True
+
+    node_ids = [int(node) for node in node_ids]
+    br = BugReport(Path(f'{test}.bug_report')) if bug_report else None
+    foundry = Foundry(foundry_root, bug_report=br)
+    proof = foundry.get_apr_proof(test)
+
+    if not isinstance(proof, APRProof):
+        raise ValueError('Specified proof is not an APRProof.')
+
+    if len(list(node_ids)) < 2:
+        raise ValueError(f'Must supply at least 2 nodes to merge, got: {node_ids}')
+
+    nodes = [proof.kcfg.node(int(node_id)) for node_id in node_ids]
+    check_cells = ['K_CELL', 'PROGRAM_CELL', 'PC_CELL', 'CALLDEPTH_CELL']
+    check_cells_ne = [check_cell for check_cell in check_cells if not check_cells_equal(check_cell, nodes)]
+    if check_cells_ne:
+        raise ValueError(f'Nodes {node_ids} cannot be merged because they differ in: {check_cells_ne}')
+
+    anti_unification = nodes[0].cterm
+    for node in nodes[1:]:
+        anti_unification, _, _ = anti_unification.anti_unify(node.cterm, keep_values=True, kdef=foundry.kevm.definition)
+    new_node = proof.kcfg.create_node(anti_unification)
+    for node in nodes:
+        proof.kcfg.create_cover(node.id, new_node.id)
+
+    proof.write_proof_data()
+
+    print(f'Merged nodes {node_ids} into new node {new_node.id}.')
+    print(foundry.kevm.pretty_print(new_node.cterm.kast))
+
+
 def foundry_step_node(
     foundry_root: Path,
     test: str,
@@ -871,8 +918,8 @@ def foundry_section_edge(
         smt_retry_limit=smt_retry_limit,
         trace_rewrites=trace_rewrites,
     ) as kcfg_explore:
-        kcfg, _ = kcfg_explore.section_edge(
-            apr_proof.kcfg, source_id=source_id, target_id=target_id, logs=apr_proof.logs, sections=sections
+        kcfg_explore.section_edge(
+            apr_proof.kcfg, source_id=int(source_id), target_id=int(target_id), logs=apr_proof.logs, sections=sections
         )
     apr_proof.write_proof_data()
 
@@ -1023,7 +1070,12 @@ def _method_to_cfg(
     calldata = method.calldata_cell(contract)
     callvalue = method.callvalue_cell
     init_cterm = _init_cterm(
-        empty_config, contract.name, kcfgs_dir, calldata=calldata, callvalue=callvalue, init_state=init_state
+        empty_config,
+        contract.name,
+        kcfgs_dir,
+        calldata=calldata,
+        callvalue=callvalue,
+        init_state=init_state,
     )
     is_test = method.name.startswith('test')
     failing = method.name.startswith('testFail')

kevm-pyk/src/tests/integration/test-data/contracts.k.expected

@@ -4790,6 +4790,8 @@ module ASSERTTEST-CONTRACT
 
     syntax AssertTestMethod ::= "failed" "(" ")" [symbol(), klabel(method_AssertTest_failed_)]
 
+    syntax AssertTestMethod ::= "kevm" "(" ")" [symbol(), klabel(method_AssertTest_kevm_)]
+
     syntax AssertTestMethod ::= "setUp" "(" ")" [symbol(), klabel(method_AssertTest_setUp_)]
 
     syntax AssertTestMethod ::= "testFail_assert_false" "(" ")" [symbol(), klabel(method_AssertTest_testFail_assert_false_)]
@@ -4804,6 +4806,8 @@ module ASSERTTEST-CONTRACT
 
     syntax AssertTestMethod ::= "test_assert_true_branch" "(" Int ":" "uint256" ")" [symbol(), klabel(method_AssertTest_test_assert_true_branch_uint256)]
 
+    syntax AssertTestMethod ::= "test_branch_merge" "(" Int ":" "uint256" ")" [symbol(), klabel(method_AssertTest_test_branch_merge_uint256)]
+
     syntax AssertTestMethod ::= "test_failing_branch" "(" Int ":" "uint256" ")" [symbol(), klabel(method_AssertTest_test_failing_branch_uint256)]
 
     syntax AssertTestMethod ::= "test_revert_branch" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol(), klabel(method_AssertTest_test_revert_branch_uint256_uint256)]
@@ -4819,6 +4823,9 @@ module ASSERTTEST-CONTRACT
     rule  ( AssertTest . failed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
 
 
+    rule  ( AssertTest . kevm ( ) => #abiCallData ( "kevm" , .TypedArgs ) )
+
+
     rule  ( AssertTest . setUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) )
 
 
@@ -4841,6 +4848,10 @@ module ASSERTTEST-CONTRACT
        ensures #rangeUInt ( 256 , V0_x )
 
 
+    rule  ( AssertTest . test_branch_merge ( V0_x : uint256 ) => #abiCallData ( "test_branch_merge" , #uint256 ( V0_x ) , .TypedArgs ) )
+       ensures #rangeUInt ( 256 , V0_x )
+
+
     rule  ( AssertTest . test_failing_branch ( V0_x : uint256 ) => #abiCallData ( "test_failing_branch" , #uint256 ( V0_x ) , .TypedArgs ) )
        ensures #rangeUInt ( 256 , V0_x )
 
@@ -4863,6 +4874,9 @@ module ASSERTTEST-CONTRACT
     rule  ( selector ( "failed()" ) => 3124842406 )
 
 
+    rule  ( selector ( "kevm()" ) => 3601001590 )
+
+
     rule  ( selector ( "setUp()" ) => 177362148 )
 
 
@@ -4884,6 +4898,9 @@ module ASSERTTEST-CONTRACT
     rule  ( selector ( "test_assert_true_branch(uint256)" ) => 3267411143 )
 
 
+    rule  ( selector ( "test_branch_merge(uint256)" ) => 1000659212 )
+
+
     rule  ( selector ( "test_failing_branch(uint256)" ) => 1176678741 )
 
 

kevm-pyk/src/tests/integration/test-data/foundry/test/Simple.t.sol

@@ -2,8 +2,9 @@
 pragma solidity =0.8.13;
 
 import "forge-std/Test.sol";
+import "../src/KEVMCheats.sol";
 
-contract AssertTest is Test {
+contract AssertTest is Test, KEVMCheats {
     uint y;
 
     function setUp() public {}
@@ -27,6 +28,16 @@ contract AssertTest is Test {
         assert(y <= x);
     }
 
+    function test_branch_merge(uint x) public {
+        kevm.infiniteGas();
+        if (x < 10) {
+            y = 0;
+        } else {
+            y = 1;
+        }
+        assert(y < 2);
+    }
+
     function test_assert_false() public pure {
         assert(false);
     }

kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected

@@ -8,21 +8,21 @@
 │  (407 steps)
 ├─ 3
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
-│   pc: 992
+│   pc: 1249
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 4
 │   k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
-│   pc: 992
+│   pc: 1249
 │   callDepth: 0
 │   statusCode: EVMC_REVERT
 │
 │  (2 steps)
 ├─ 5 (terminal)
 │   k: #halt ~> CONTINUATION:K
-│   pc: 992
+│   pc: 1249
 │   callDepth: 0
 │   statusCode: EVMC_REVERT
 │
@@ -81,7 +81,7 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( 399 : ( 212 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) ) )
+                     ( .WordStack => ( 495 : ( 250 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) ) )
                    </wordStack>
                    <localMem>
                      ( .Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
@@ -301,7 +301,7 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( 399 : ( 212 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
+                     ( 495 : ( 250 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
                    </wordStack>
                    <localMem>
                      b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80"
@@ -509,7 +509,7 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( 399 : ( 212 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
+                     ( 495 : ( 250 : ( selector ( "testFail_assert_false()" ) : .WordStack ) ) )
                    </wordStack>
                    <localMem>
                      b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80"

kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected

@@ -5,24 +5,24 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE
 │
-│  (269 steps)
+│  (303 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 213
+│   pc: 251
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 4
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
-│   pc: 213
+│   pc: 251
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
 └─ 5 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
-    pc: 213
+    pc: 251
     callDepth: 0
     statusCode: EVMC_SUCCESS