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.224"
+version = "1.0.225"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__main__.py

@@ -24,6 +24,7 @@
     Foundry,
     foundry_kompile,
     foundry_list,
+    foundry_merge_nodes,
     foundry_node_printer,
     foundry_prove,
     foundry_remove_node,
@@ -682,6 +683,16 @@ def exec_foundry_simplify_node(
     print(f'Simplified:\n{pretty_term}')
 
 
+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, nodes=nodes, test=test)
+
+
 def exec_foundry_step_node(
     foundry_root: Path,
     test: str,
@@ -1030,6 +1041,24 @@ def parse(s: str) -> list[T]:
         '--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=str,
+        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',
         help='Given an edge in the graph, cut it into sections to get intermediate nodes.',

kevm-pyk/src/kevm_pyk/foundry.py

@@ -13,7 +13,7 @@
 from pathos.pools import ProcessPool  # type: ignore
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
-from pyk.kast.manip import free_vars, minimize_term
+from pyk.kast.manip import anti_unify_with_constraints, free_vars, minimize_term
 from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire
 from pyk.kcfg import KCFG, KCFGExplore
 from pyk.ktool.kompile import LLVMKompileType
@@ -727,6 +727,40 @@ 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,
+    nodes: Iterable[NodeIdLike],
+    bug_report: bool = False,
+) -> None:
+    br = BugReport(Path(f'{test}.bug_report')) if bug_report else None
+    foundry = Foundry(foundry_root, bug_report=br)
+    apr_proofs_dir = foundry.out / 'apr_proofs'
+    contract_name, test_name = test.split('.')
+    proof_digest = foundry.proof_digest(contract_name, test_name)
+    apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir)
+
+    _nodes = [apr_proof.kcfg.node(int(node_id)) for node_id in nodes]
+
+    anti_unification: KInner
+    for i, node in enumerate(_nodes):
+        cterm = node.cterm
+        if i < 1:
+            anti_unification = cterm.kast
+            continue
+        anti_unification = anti_unify_with_constraints(anti_unification, cterm.kast, disjunct=False)
+
+    new_cterm = CTerm.from_kast(anti_unification)
+    new_node = apr_proof.kcfg.create_node(new_cterm)
+
+    for node in _nodes:
+        apr_proof.kcfg.create_cover(node.id, new_node.id)
+
+    apr_proof.write_proof()
+
+    print(f'Merged nodes {[int(node) for node in nodes]} into new node {new_node.id}.')
+
+
 def foundry_step_node(
     foundry_root: Path,
     test: str,

kevm-pyk/src/tests/integration/test-data/foundry-prove-all

@@ -39,6 +39,7 @@ ArithmeticTest.test_wmul_weakly_increasing_positive
 AssertTest.test_assert_false
 AssertTest.test_assert_true
 AssertTest.test_assert_true_branch
+AssertTest.test_branch_merge
 AssertTest.testFail_assert_false
 AssertTest.testFail_assert_true
 AssertTest.testFail_expect_revert

package/debian/changelog

@@ -1,4 +1,4 @@
-kevm (1.0.224) unstable; urgency=medium
+kevm (1.0.225) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-1.0.224
+1.0.225

tests/foundry/test/Simple.t.sol

@@ -6,8 +6,6 @@ import "forge-std/Test.sol";
 contract AssertTest is Test {
     uint y;
 
-    function setUp() public {}
-
     function test_failing_branch(uint x) public {
       assert(x >= 100);
     }
@@ -27,6 +25,15 @@ contract AssertTest is Test {
         assert(y <= x);
     }
 
+    function test_branch_merge(uint x) public {
+        if (x < 10) {
+            y = 0;
+        } else {
+            y = 1;
+        }
+        assert(y < 2);
+    }
+
     function test_assert_false() public pure {
         assert(false);
     }