Add functionality for merging covers, target pullbacks

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__main__.py

@@ -28,6 +28,7 @@
     foundry_get_model,
     foundry_kompile,
     foundry_list,
+    foundry_merge_target,
     foundry_node_printer,
     foundry_prove,
     foundry_remove_node,
@@ -680,6 +681,10 @@ def exec_foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike, **
     foundry_remove_node(foundry_root=foundry_root, test=test, node=node)
 
 
+def exec_foundry_merge_target(foundry_root: Path, test: str, **kwargs: Any) -> None:
+    foundry_merge_target(foundry_root=foundry_root, test=test)
+
+
 def exec_foundry_simplify_node(
     foundry_root: Path,
     test: str,
@@ -1032,6 +1037,13 @@ def parse(s: str) -> list[T]:
     foundry_remove_node.add_argument('test', type=str, help='View the CFG for this test.')
     foundry_remove_node.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.')
 
+    foundry_merge_target = command_parser.add_parser(
+        'foundry-merge-target',
+        help='Merge the target subsumed node of a proof.',
+        parents=[kevm_cli_args.logging_args, kevm_cli_args.foundry_args],
+    )
+    foundry_merge_target.add_argument('test', type=str, help='Test to apply to.')
+
     foundry_simplify_node = command_parser.add_parser(
         'foundry-simplify-node',
         help='Simplify a given node, and potentially replace it.',

kevm-pyk/src/kevm_pyk/foundry.py

@@ -692,6 +692,27 @@ def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike) -> None
     apr_proof.write_proof()
 
 
+def foundry_merge_target(foundry_root: Path, test: str) -> None:
+    foundry = Foundry(foundry_root)
+    proofs_dir = foundry.out / 'apr_proofs'
+    contract_name, test_name = test.split('.')
+    proof_digest = foundry.proof_digest(contract_name, test_name)
+    proof = Proof.read_proof(proof_digest, proofs_dir)
+    assert isinstance(proof, APRProof)
+    target_subsumptions = proof.kcfg.covers(target_id=proof.target)
+    ts_by_statuscode: dict[KInner, list[KCFG.Cover]] = {}
+    for ts in target_subsumptions:
+        status_code = ts.source.cterm.cell('STATUSCODE_CELL')
+        if type(status_code) is KToken:
+            if status_code not in ts_by_statuscode:
+                ts_by_statuscode[status_code] = []
+            ts_by_statuscode[status_code].append(ts)
+    for ts_covers in ts_by_statuscode.values():
+        if len(ts_covers) > 1:
+            proof.kcfg.minimize_covers([cover.source.id for cover in ts_covers], proof.target)
+    # proof.write_proof()
+
+
 def foundry_simplify_node(
     foundry_root: Path,
     test: str,

package/debian/changelog

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

package/version

@@ -1 +1 @@
-1.0.241
+1.0.242

tests/foundry/test/Arithmetic.t.sol

@@ -143,4 +143,16 @@ contract ArithmeticTest is Test {
         assertTrue(c2 <= c1);
     }
 
+    function add_uint_int(uint x, int y) public pure returns (uint z) {
+        if (x < 10) {
+            z = uint(y) + x;
+        } else {
+            z = x + uint(y);
+        }
+    }
+
+    function test_double_add(uint x, int y) external {
+        uint z = add_uint_int(x, y);
+        z = add_uint_int(z, y);
+    }
 }