Add foundry-merge-nodes option (#1934)

* Add foundry-merge-nodes option * Set Version: 1.0.225 * Anti-unify without disjunct * Update kevm-pyk/src/kevm_pyk/foundry.py Co-authored-by: Everett Hildenbrandt <[email protected]> * Update kevm-pyk/src/kevm_pyk/foundry.py Co-authored-by: Everett Hildenbrandt <[email protected]> * Fix formatting * Rename apr_proof to proof, reduce whitespace * Disallow merging nodes if they do not match on <k>, <program>, <pc>, or <callDepth> * Improve variable naming * Add test for branch merging * Update expected contracts.k * Set Version: 1.0.226 * Set Version: 1.0.226 * Update expected output * Set Version: 1.0.227 * Update test_foundry_fail expected files * Keep disjunction of concrete values * Switch to using associated pyk branch * Set Version: 1.0.228 * Fix foundry_get_apr_proof and foundry_step_node to be compatible with APR and APRBMC proofs * Fix various commands to work with APRBMCProof * Update kevm-pyk/src/kevm_pyk/__main__.py * Update kevm-pyk/src/kevm_pyk/foundry.py * Update foundry_merge_nodes test * Fix formatting * Update expected files * Set Version: 1.0.229 * Set Version: 1.0.231 * Set Version: 1.0.232 * Set Version: 1.0.235 * Set Version: 1.0.236 * Revert poetry.lock * Fix setUp method execution being limited by max_iterations * Set Version: 1.0.239 * Set Version: 1.0.244 * Set Version: 1.0.249 * Set Version: 1.0.250 * Revert foundry_get_proof and foundry_get_apr_proof changes as they have been moved to another branch * Fix foundry_list proof_data_exists call * Use digest, not just method name for looking up setUp method * Revert change to proof loading path * Use foundry.get_apr_proof in foundry_merge_nodes * Set Version: 1.0.251 * Use foundry.get_apr_proof in test * Set Version: 1.0.252 * Set Version: 1.0.262 * Use new anti_unification function * Set Version: 1.0.263 * Set Version: 1.0.264 * Include kdefinition in anti_unify call and fix test * Re-add foundry-merge-nodes command * Set Version: 1.0.265 * Set Version: 1.0.265 * Set Version: 1.0.266 * Set Version: 1.0.267 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]>
runtimeverification · Aug 19, 2023 · f01c196 · f01c196
1 parent 8380dff
commit f01c196
Show file tree

Hide file tree

Showing 17 changed files with 324 additions and 101 deletions.
diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.266"
+version = "1.0.267"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kontrol/__main__.py b/kevm-pyk/src/kontrol/__main__.py
@@ -17,6 +17,7 @@
     foundry_get_model,
     foundry_kompile,
     foundry_list,
+    foundry_merge_nodes,
     foundry_node_printer,
     foundry_prove,
     foundry_remove_node,
@@ -330,6 +331,16 @@ def exec_foundry_step_node(
     )
 
 
+def exec_foundry_merge_nodes(
+    foundry_root: Path,
+    test: str,
+    nodes: Iterable[NodeIdLike],
+    bug_report: bool = False,
+    **kwargs: Any,
+) -> None:
+    foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test)
+
+
 def exec_foundry_section_edge(
     foundry_root: Path,
     test: str,
@@ -564,6 +575,23 @@ def parse(s: str) -> list[T]:
     foundry_step_node.add_argument(
         '--depth', type=int, default=1, help='How many steps to take from initial node on edge.'
     )
+    foundry_merge_node = command_parser.add_parser(
+        'foundry-merge-nodes',
+        help='Merge multiple nodes into one branch.',
+        parents=[
+            kevm_cli_args.logging_args,
+            kevm_cli_args.foundry_args,
+        ],
+    )
+    foundry_merge_node.add_argument(
+        '--node',
+        type=node_id_like,
+        dest='nodes',
+        default=[],
+        action='append',
+        help='One node to be merged.',
+    )
+    foundry_merge_node.add_argument('test', type=str, help='Merge nodes in this CFG.')
 
     foundry_section_edge = command_parser.add_parser(
         'foundry-section-edge',

diff --git a/kevm-pyk/src/kontrol/foundry.py b/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,52 @@ 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
+
+    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 +917,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 +1069,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')

diff --git a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected b/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 )
 
 

diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/Simple.t.sol b/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);
     }

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected b/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"

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/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