Enable breaking on all foundry actions (#261)

* kontrol/prove: make sure to break on foundry calls/returns to not generate those rules for KEVM * kontrol/cheatcodes.md, kontrol/prove.py: break on more cheatcode rules to get maximal basic-blocks for KEVM claims * kontrol/{prove,options,__main__}: add option --break-on-foundry for breaking on all foundry rules * kontrol/{options,prove}: allow KEVMs --break-on-storage cut-rule too * Set Version: 0.1.105 * kontrol/{options,__main__,prove}: enable --break-on-basic-blocks * Set Version: 0.1.106 * kontrol/: rename --break-on-foundry => --break-on-cheatcodes * kontrol/prove: enumerate rules directly from definition instead of manually * Set Version: 0.1.107 * Set Version: 0.1.108 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Jan 11, 2024 · d5d097f · d5d097f
1 parent a27a5e0
commit d5d097f
Show file tree

Hide file tree

Showing 7 changed files with 33 additions and 12 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.107
+0.1.108
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.107"
+version = "0.1.108"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.107'
+VERSION: Final = '0.1.108'
diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py
@@ -216,6 +216,7 @@ def exec_prove(
     break_on_calls: bool = True,
     break_on_storage: bool = False,
     break_on_basic_blocks: bool = False,
+    break_on_cheatcodes: bool = False,
     bmc_depth: int | None = None,
     bug_report: BugReport | None = None,
     kore_rpc_command: str | Iterable[str] | None = None,
@@ -258,6 +259,7 @@ def exec_prove(
         break_on_calls=break_on_calls,
         break_on_storage=break_on_storage,
         break_on_basic_blocks=break_on_basic_blocks,
+        break_on_cheatcodes=break_on_cheatcodes,
         workers=workers,
         counterexample_info=counterexample_info,
         max_iterations=max_iterations,
@@ -733,6 +735,13 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
     prove_args.add_argument(
         '--use-gas', dest='use_gas', default=False, action='store_true', help='Enables gas computation in KEVM.'
     )
+    prove_args.add_argument(
+        '--break-on-cheatcodes',
+        dest='break_on_cheatcodes',
+        default=False,
+        action='store_true',
+        help='Break on all Foundry rules.',
+    )
 
     show_args = command_parser.add_parser(
         'show',

diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
@@ -456,7 +456,8 @@ The check will be inserted only if the current depth is the same as the depth at
 WThe `#checkRevert` will be used to compare the status code of the execution and the output of the call against the expect reason provided.
 
 ```k
-    rule <k> #next [ _OP:CallOp ] ~> (. => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
+    rule [foundry.set.expectrevert.1]:
+         <k> #next [ _OP:CallOp ] ~> (. => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
          <callDepth> CD </callDepth>
          <wordStack> _ : _ : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
          <expectedRevert>
@@ -466,7 +467,8 @@ WThe `#checkRevert` will be used to compare the status code of the execution and
          </expectedRevert>
       [priority(40)]
 
-    rule <k> #next [ _OP:CallSixOp ] ~> (. => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
+    rule [foundry.set.expectrevert.2]:
+         <k> #next [ _OP:CallSixOp ] ~> (. => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
          <callDepth> CD </callDepth>
          <wordStack> _ : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
          <expectedRevert>
@@ -476,7 +478,8 @@ WThe `#checkRevert` will be used to compare the status code of the execution and
          </expectedRevert>
       [priority(40)]
 
-    rule <k> #next [ OP:OpCode ] ~> (. => #checkRevert) ~> #execute ... </k>
+    rule [foundry.set.expectrevert.3]:
+         <k> #next [ OP:OpCode ] ~> (. => #checkRevert) ~> #execute ... </k>
          <callDepth> CD </callDepth>
          <expectedRevert>
            <isRevertExpected> true </isRevertExpected>

diff --git a/src/kontrol/options.py b/src/kontrol/options.py
@@ -20,6 +20,7 @@ class ProveOptions:
     break_on_calls: bool
     break_on_storage: bool
     break_on_basic_blocks: bool
+    break_on_cheatcodes: bool
     workers: int
     counterexample_info: bool
     max_iterations: int | None
@@ -40,6 +41,7 @@ def __init__(
         break_on_calls: bool = True,
         break_on_storage: bool = False,
         break_on_basic_blocks: bool = False,
+        break_on_cheatcodes: bool = False,
         workers: int = 1,
         counterexample_info: bool = False,
         max_iterations: int | None = None,
@@ -57,6 +59,7 @@ def __init__(
         object.__setattr__(self, 'break_on_calls', break_on_calls)
         object.__setattr__(self, 'break_on_storage', break_on_storage)
         object.__setattr__(self, 'break_on_basic_blocks', break_on_basic_blocks)
+        object.__setattr__(self, 'break_on_cheatcodes', break_on_cheatcodes)
         object.__setattr__(self, 'workers', workers)
         object.__setattr__(self, 'counterexample_info', counterexample_info)
         object.__setattr__(self, 'max_iterations', max_iterations)

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -207,18 +207,24 @@ def init_and_run_proof(test: FoundryTest) -> Proof:
                 use_gas=prove_options.use_gas,
             )
 
+            cut_point_rules = KEVMSemantics.cut_point_rules(
+                prove_options.break_on_jumpi,
+                prove_options.break_on_calls,
+                prove_options.break_on_storage,
+                prove_options.break_on_basic_blocks,
+            )
+            if prove_options.break_on_cheatcodes:
+                cut_point_rules.extend(
+                    rule.label for rule in foundry.kevm.definition.all_modules_dict['FOUNDRY-CHEAT-CODES'].rules
+                )
+
             run_prover(
                 foundry.kevm,
                 proof,
                 kcfg_explore,
                 max_depth=prove_options.max_depth,
                 max_iterations=prove_options.max_iterations,
-                cut_point_rules=KEVMSemantics.cut_point_rules(
-                    prove_options.break_on_jumpi,
-                    prove_options.break_on_calls,
-                    prove_options.break_on_storage,
-                    prove_options.break_on_basic_blocks,
-                ),
+                cut_point_rules=cut_point_rules,
                 terminal_rules=KEVMSemantics.terminal_rules(prove_options.break_every_step),
                 counterexample_info=prove_options.counterexample_info,
             )