Test BMC output, improve node printing (#1922)

* kevm-pyk/: make sure to use more specific node printers for different APRProof types * tests/foundry: add test_bmc example * kevm-pyk/BMCLoops.t.sol: add test to foundry test harness * Set Version: 1.0.217 * kevm-pyk/test-data: update expected output * Set Version: 1.0.219 * Set Version: 1.0.220 * kevm-pyk/{kevm,foundry,__main__}: factor out node printer * Set Version: 1.0.221 * .github/test-pr: up timeout with more tests being run * Set Version: 1.0.222 * Set Version: 1.0.223 * Set Version: 1.0.224 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Jun 29, 2023 · b03e529 · b03e529
1 parent b5be485
commit b03e529
Show file tree

Hide file tree

Showing 22 changed files with 117 additions and 40 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -81,7 +81,7 @@ jobs:
     name: 'Build and Test KEVM concrete execution'
     needs: kevm-pyk-code-quality-checks
     runs-on: [self-hosted, linux, normal]
-    timeout-minutes: 35
+    timeout-minutes: 45
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3

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

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -22,9 +22,9 @@
 from .cli import KEVMCLIArgs, node_id_like
 from .foundry import (
     Foundry,
-    FoundryNodePrinter,
     foundry_kompile,
     foundry_list,
+    foundry_node_printer,
     foundry_prove,
     foundry_remove_node,
     foundry_section_edge,
@@ -34,7 +34,7 @@
     foundry_to_dot,
 )
 from .gst_to_kore import _mode_to_kore, _schedule_to_kore
-from .kevm import KEVM, KEVMNodePrinter
+from .kevm import KEVM, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
 from .solc_to_k import solc_compile, solc_to_k
 from .utils import arg_pair_of, ensure_ksequence_on_k_cell, get_apr_proof_for_spec, kevm_apr_prove, print_failure_info
@@ -440,7 +440,9 @@ def exec_show_kcfg(
         exclude_claim_labels=exclude_claim_labels,
     )
 
-    proof_show = APRProofShow(kevm, node_printer=KEVMNodePrinter(kevm))
+    node_printer = kevm_node_printer(kevm, proof)
+    proof_show = APRProofShow(kevm, node_printer=node_printer)
+
     res_lines = proof_show.show(
         proof,
         nodes=nodes,
@@ -469,7 +471,7 @@ def exec_view_kcfg(
     **kwargs: Any,
 ) -> None:
     kevm = KEVM(definition_dir)
-    apr_proof = get_apr_proof_for_spec(
+    proof = get_apr_proof_for_spec(
         kevm,
         spec_file,
         save_directory=save_directory,
@@ -480,8 +482,10 @@ def exec_view_kcfg(
         exclude_claim_labels=exclude_claim_labels,
     )
 
-    viewer = APRProofViewer(apr_proof, kevm, node_printer=KEVMNodePrinter(kevm))
-    viewer.run()
+    node_printer = kevm_node_printer(kevm, proof)
+    proof_view = APRProofViewer(proof, kevm, node_printer=node_printer)
+
+    proof_view.run()
 
 
 def exec_foundry_prove(
@@ -629,21 +633,20 @@ def exec_run(
 
 def exec_foundry_view_kcfg(foundry_root: Path, test: str, **kwargs: Any) -> None:
     foundry = Foundry(foundry_root)
-    apr_proofs_dir = foundry.out / 'apr_proofs'
+    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)
+    proof = APRProof.read_proof(proof_digest, proofs_dir)
 
     def _short_info(cterm: CTerm) -> Iterable[str]:
         return foundry.short_info_for_contract(contract_name, cterm)
 
     def _custom_view(elem: KCFGElem) -> Iterable[str]:
         return foundry.custom_view(contract_name, elem)
 
-    viewer = APRProofViewer(
-        apr_proof, foundry.kevm, node_printer=FoundryNodePrinter(foundry, contract_name), custom_view=_custom_view
-    )
+    node_printer = foundry_node_printer(foundry, contract_name, proof)
+    viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view)
     viewer.run()
 
 

diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py
@@ -24,7 +24,7 @@
 from pyk.prelude.ml import mlEqualsTrue
 from pyk.proof.proof import Proof
 from pyk.proof.reachability import APRBMCProof, APRProof
-from pyk.proof.show import APRProofShow
+from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter, APRProofShow
 from pyk.utils import BugReport, ensure_dir_path, hash_str, run_process, single, unique
 
 from .kevm import KEVM, KEVMNodePrinter
@@ -46,6 +46,7 @@
     from pyk.kast import KInner
     from pyk.kcfg.kcfg import NodeIdLike
     from pyk.kcfg.tui import KCFGElem
+    from pyk.proof.show import NodePrinter
 
 _LOGGER: Final = logging.getLogger(__name__)
 
@@ -623,7 +624,9 @@ def _short_info(cterm: CTerm) -> Iterable[str]:
         '<code>',
     ]
 
-    proof_show = APRProofShow(foundry.kevm, node_printer=FoundryNodePrinter(foundry, contract_name))
+    node_printer = foundry_node_printer(foundry, contract_name, proof)
+    proof_show = APRProofShow(foundry.kevm, node_printer=node_printer)
+
     res_lines = proof_show.show(
         proof,
         nodes=nodes,
@@ -644,13 +647,16 @@ def _short_info(cterm: CTerm) -> Iterable[str]:
 
 def foundry_to_dot(foundry_root: Path, test: str) -> None:
     foundry = Foundry(foundry_root)
-    apr_proofs_dir = foundry.out / 'apr_proofs'
-    dump_dir = apr_proofs_dir / 'dump'
+    proofs_dir = foundry.out / 'apr_proofs'
+    dump_dir = proofs_dir / 'dump'
     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)
-    proof_show = APRProofShow(foundry.kevm, node_printer=FoundryNodePrinter(foundry, contract_name))
-    proof_show.dump(apr_proof, dump_dir, dot=True)
+    proof = APRProof.read_proof(proof_digest, proofs_dir)
+
+    node_printer = foundry_node_printer(foundry, contract_name, proof)
+    proof_show = APRProofShow(foundry.kevm, node_printer=node_printer)
+
+    proof_show.dump(proof, dump_dir, dot=True)
 
 
 def foundry_list(foundry_root: Path) -> list[str]:
@@ -1092,7 +1098,7 @@ class FoundryNodePrinter(KEVMNodePrinter):
     contract_name: str
 
     def __init__(self, foundry: Foundry, contract_name: str):
-        super().__init__(foundry.kevm)
+        KEVMNodePrinter.__init__(self, foundry.kevm)
         self.foundry = foundry
         self.contract_name = contract_name
 
@@ -1105,3 +1111,23 @@ def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
                 path, start, end = srcmap_data
                 ret_strs.append(f'src: {str(path)}:{start}:{end}')
         return ret_strs
+
+
+class FoundryAPRNodePrinter(FoundryNodePrinter, APRProofNodePrinter):
+    def __init__(self, foundry: Foundry, contract_name: str, proof: APRProof):
+        FoundryNodePrinter.__init__(self, foundry, contract_name)
+        APRProofNodePrinter.__init__(self, proof, foundry.kevm)
+
+
+class FoundryAPRBMCNodePrinter(FoundryNodePrinter, APRBMCProofNodePrinter):
+    def __init__(self, foundry: Foundry, contract_name: str, proof: APRBMCProof):
+        FoundryNodePrinter.__init__(self, foundry, contract_name)
+        APRBMCProofNodePrinter.__init__(self, proof, foundry.kevm)
+
+
+def foundry_node_printer(foundry: Foundry, contract_name: str, proof: APRProof) -> NodePrinter:
+    if type(proof) is APRBMCProof:
+        return FoundryAPRBMCNodePrinter(foundry, contract_name, proof)
+    if type(proof) is APRProof:
+        return FoundryAPRNodePrinter(foundry, contract_name, proof)
+    raise ValueError(f'Cannot build NodePrinter for proof type: {type(proof)}')
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -14,6 +14,8 @@
 from pyk.prelude.kint import intToken, ltInt
 from pyk.prelude.ml import mlEqualsTrue
 from pyk.prelude.string import stringToken
+from pyk.proof.reachability import APRBMCProof, APRProof
+from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
@@ -393,10 +395,30 @@ class KEVMNodePrinter(NodePrinter):
     kevm: KEVM
 
     def __init__(self, kevm: KEVM):
-        super().__init__(kevm)
+        NodePrinter.__init__(self, kevm)
         self.kevm = kevm
 
     def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
         ret_strs = super().print_node(kcfg, node)
         ret_strs += self.kevm.short_info(node.cterm)
         return ret_strs
+
+
+class KEVMAPRNodePrinter(KEVMNodePrinter, APRProofNodePrinter):
+    def __init__(self, kevm: KEVM, proof: APRProof):
+        KEVMNodePrinter.__init__(self, kevm)
+        APRProofNodePrinter.__init__(self, proof, kevm)
+
+
+class KEVMAPRBMCNodePrinter(KEVMNodePrinter, APRBMCProofNodePrinter):
+    def __init__(self, kevm: KEVM, proof: APRBMCProof):
+        KEVMNodePrinter.__init__(self, kevm)
+        APRBMCProofNodePrinter.__init__(self, proof, kevm)
+
+
+def kevm_node_printer(kevm: KEVM, proof: APRProof) -> NodePrinter:
+    if type(proof) is APRBMCProof:
+        return KEVMAPRBMCNodePrinter(kevm, proof)
+    if type(proof) is APRProof:
+        return KEVMAPRNodePrinter(kevm, proof)
+    raise ValueError(f'Cannot build NodePrinter for proof type: {type(proof)}')
diff --git a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected
@@ -862,6 +862,8 @@ module BMCLOOPSTEST-CONTRACT
 
     syntax BMCLoopsTestMethod ::= "failed" "(" ")" [symbol(), klabel(method_BMCLoopsTest_failed_)]
 
+    syntax BMCLoopsTestMethod ::= "test_bmc" "(" Int ":" "uint256" ")" [symbol(), klabel(method_BMCLoopsTest_test_bmc_uint256)]
+
     syntax BMCLoopsTestMethod ::= "test_countdown_concrete" "(" ")" [symbol(), klabel(method_BMCLoopsTest_test_countdown_concrete_)]
 
     syntax BMCLoopsTestMethod ::= "test_countdown_symbolic" "(" Int ":" "uint256" ")" [symbol(), klabel(method_BMCLoopsTest_test_countdown_symbolic_uint256)]
@@ -877,6 +879,10 @@ module BMCLOOPSTEST-CONTRACT
     rule  ( BMCLoopsTest . failed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
 
 
+    rule  ( BMCLoopsTest . test_bmc ( V0_n : uint256 ) => #abiCallData ( "test_bmc" , #uint256 ( V0_n ) , .TypedArgs ) )
+       ensures #rangeUInt ( 256 , V0_n )
+
+
     rule  ( BMCLoopsTest . test_countdown_concrete ( ) => #abiCallData ( "test_countdown_concrete" , .TypedArgs ) )
 
 
@@ -896,6 +902,9 @@ module BMCLOOPSTEST-CONTRACT
     rule  ( selector ( "failed()" ) => 3124842406 )
 
 
+    rule  ( selector ( "test_bmc(uint256)" ) => 2531276689 )
+
+
     rule  ( selector ( "test_countdown_concrete()" ) => 1189516988 )
 
 

diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/BMCLoops.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/BMCLoops.t.sol
@@ -20,4 +20,12 @@ contract BMCLoopsTest is Test {
         }
         assert(n == 0);
     }
+
+    function test_bmc(uint256 n) public {
+        uint256 x = 0;
+        for (uint256 i = 0; i < n; ++i) {
+            x += 1;
+        }
+        assertEq(x, n);
+    }
 }
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
@@ -37,7 +37,7 @@
 
 
 
-module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:2A3527C34E566A9F170452CD78ECD8B40FA4041EBAB206050F339275402306E0
+module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:D9767505A49B578A77DD3E9B8A9FE01EAFE474E8A6AA79E26F018CC5DA6F799A
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

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
@@ -20,7 +20,7 @@
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-└─ 5 (leaf)
+└─ 5 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 213
     callDepth: 0
@@ -241,7 +241,7 @@ Node 5:
 
 
 
-module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-TRUE:5DDA90333A0F7F4C47CCBF2CF8C9EA5168661E8EFAE31E01F4E7535CEBDD5E2A
+module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-TRUE:B64469810687DD4D52CB523504A17EF06BC096E85D850767931F8B92A7CB4CD2
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected
@@ -34,7 +34,7 @@
 │   statusCode: EVMC_REVERT
 │
 │  (5 steps)
-└─ 7 (leaf)
+└─ 7 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 992
     callDepth: 0
@@ -263,7 +263,7 @@ Node 7:
 
 
 
-module SUMMARY-ASSERTTEST.TESTFAIL-EXPECT-REVERT:544A7CD7EC24BD75539E5995E7BA8DAD8C49229C42024AE5A37FC7A300FDB8C6
+module SUMMARY-ASSERTTEST.TESTFAIL-EXPECT-REVERT:C06C5EA6446D70FBDD360FECAB0A1147918BDDEF043645F28130D54891127053
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected
@@ -20,7 +20,7 @@
 │   statusCode: EVMC_REVERT
 │
 │  (2 steps)
-└─ 5 (leaf)
+└─ 5 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 992
     callDepth: 0
@@ -241,7 +241,7 @@ Node 5:
 
 
 
-module SUMMARY-ASSERTTEST.TEST-ASSERT-FALSE:ECCEE15056474B7F502FE275CD66FA785BDCF0201A2E45F20541204B52B78F69
+module SUMMARY-ASSERTTEST.TEST-ASSERT-FALSE:08F836935DBCC810AE1CEBB9276F3B79DE040475AFCDA8C9DC5D47AA2E65AB2C
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected
@@ -37,7 +37,7 @@
 
 
 
-module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:ED7C70C8FF6A057076CEBCAC150C6D41D6A815B024C1E7A3390E1416A302BA35
+module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:E200EADD2408C03C6CCDB315095224AC1D58DF84031A945BF166ABAB4AE2A531
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected
@@ -73,7 +73,7 @@
    │   statusCode: EVMC_REVERT
    │
    │  (2 steps)
-   └─ 11 (leaf)
+   └─ 11 (leaf, terminal)
        k: #halt ~> CONTINUATION:K
        pc: 992
        callDepth: 0
@@ -291,7 +291,7 @@ Node 11:
 
 
 
-module SUMMARY-ASSERTTEST.TEST-FAILING-BRANCH:D64D5EC416625C695FDA65AECE2A7D12DFC18C28905CDE381B286CB7B8A2571D
+module SUMMARY-ASSERTTEST.TEST-FAILING-BRANCH:C60CB1C30ED782C5B61A621FCA10BE831A7CC1ECB96FE691F94F331F484FD273
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected
@@ -36,7 +36,7 @@
 ┃  │   statusCode: EVMC_REVERT
 ┃  │
 ┃  │  (2 steps)
-┃  └─ 10 (leaf)
+┃  └─ 10 (leaf, terminal)
 ┃      k: #halt ~> CONTINUATION:K
 ┃      pc: 992
 ┃      callDepth: 0
@@ -293,7 +293,7 @@ Node 10:
 
 
 
-module SUMMARY-ASSERTTEST.TEST-REVERT-BRANCH:6FFE05225C2677A93E50834ED1E0DA7AEEBA5E533F9CB61BBDCEA13E9E7DBB75
+module SUMMARY-ASSERTTEST.TEST-REVERT-BRANCH:794968430243366DC0B838DD3DC47D2AD99E08CBBD3C2B29529697015104F332
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected
@@ -34,7 +34,7 @@
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-└─ 7 (leaf)
+└─ 7 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 183
     callDepth: 0

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected
@@ -62,7 +62,7 @@
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-└─ 11 (leaf)
+└─ 11 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 183
     callDepth: 0

diff --git a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected
@@ -104,7 +104,7 @@
 
 
 
-module SUMMARY-LOOPSTEST.SUM-N:9AB5598CDC14FE56910D2D8F0BF923F62A3151DDDBB71424C6C3C2029CDEFBAC
+module SUMMARY-LOOPSTEST.SUM-N:062CC914DAA13A8EAF189DADDC9178CE923938A59F8855C3A0DE5EB7260670A7
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>