Merge remote-tracking branch 'origin/master' into _update-deps/runtim…

…everification/blockchain-k-plugin
runtimeverification · Nov 8, 2024 · 96b72de · 96b72de
2 parents ca4eccc + ccee56b
commit 96b72de
Show file tree

Hide file tree

Showing 10 changed files with 55 additions and 43 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.163
+7.1.169
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,7 +2,7 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.163";
+    k-framework.url = "github:runtimeverification/k/v7.1.169";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";

diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.163"
+kframework = "7.1.169"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -352,6 +352,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 max_iterations=options.max_iterations,
                 cut_point_rules=KEVMSemantics.cut_point_rules(
                     options.break_on_jumpi,
+                    options.break_on_jump,
                     options.break_on_calls,
                     options.break_on_storage,
                     options.break_on_basic_blocks,

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -334,6 +334,7 @@ def get_argument_type() -> dict[str, Callable]:
 class ExploreOptions(Options):
     break_every_step: bool
     break_on_jumpi: bool
+    break_on_jump: bool
     break_on_calls: bool
     break_on_storage: bool
     break_on_basic_blocks: bool
@@ -350,6 +351,7 @@ class ExploreOptions(Options):
     def default() -> dict[str, Any]:
         return {
             'break_every_step': False,
+            'break_on_jump': False,
             'break_on_jumpi': False,
             'break_on_calls': False,
             'break_on_storage': False,
@@ -1040,6 +1042,13 @@ def explore_args(self) -> ArgumentParser:
             dest='break_on_jumpi',
             default=None,
             action='store_true',
+            help='Store a node for every EVM jumpi opcode.',
+        )
+        args.add_argument(
+            '--break-on-jump',
+            dest='break_on_jump',
+            default=None,
+            action='store_true',
             help='Store a node for every EVM jump opcode.',
         )
         args.add_argument(

diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -164,6 +164,7 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
     @staticmethod
     def cut_point_rules(
         break_on_jumpi: bool,
+        break_on_jump: bool,
         break_on_calls: bool,
         break_on_storage: bool,
         break_on_basic_blocks: bool,
@@ -172,6 +173,8 @@ def cut_point_rules(
         cut_point_rules = []
         if break_on_jumpi:
             cut_point_rules.extend(['EVM.jumpi.true', 'EVM.jumpi.false'])
+        if break_on_jump:
+            cut_point_rules.extend(['EVM.jump'])
         if break_on_basic_blocks:
             cut_point_rules.append('EVM.end-basic-block')
         if break_on_calls or break_on_basic_blocks:

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -1076,7 +1076,8 @@ The `JUMP*` family of operations affect the current program counter.
 
     syntax UnStackOp ::= "JUMP"
  // ---------------------------
-    rule <k> JUMP DEST => #endBasicBlock ... </k>
+    rule [jump]:
+         <k> JUMP DEST => #endBasicBlock ... </k>
          <pc> _ => DEST </pc>
          <jumpDests> DESTS </jumpDests>
       requires DEST <Int lengthBytes(DESTS) andBool DESTS[DEST] ==Int 1

diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev
@@ -14,7 +14,6 @@ tests/specs/benchmarks/encodepacked-keccak01-spec.k
 tests/specs/benchmarks/functional-spec.k
 tests/specs/benchmarks/keccak00-spec.k
 tests/specs/benchmarks/overflow00-nooverflow-spec.k
-tests/specs/benchmarks/overflow00-overflow-spec.k
 tests/specs/benchmarks/requires01-a0gt0-spec.k
 tests/specs/benchmarks/requires01-a0le0-spec.k
 tests/specs/benchmarks/staticarray00-spec.k
@@ -92,6 +91,7 @@ tests/specs/kontrol/test-storetest-testaccesses-0-spec.k
 tests/specs/kontrol/test-storetest-teststoreload-0-spec.k
 tests/specs/mcd/cat-exhaustiveness-spec.k
 tests/specs/mcd/cat-file-addr-pass-rough-spec.k
+tests/specs/mcd/dai-adduu-fail-rough-spec.k
 tests/specs/mcd/dstoken-approve-fail-rough-spec.k
 tests/specs/mcd/dsvalue-peek-pass-rough-spec.k
 tests/specs/mcd/dsvalue-read-pass-spec.k
@@ -100,39 +100,37 @@ tests/specs/mcd/end-cash-pass-rough-spec.k
 tests/specs/mcd/end-pack-pass-rough-spec.k
 tests/specs/mcd/end-subuu-pass-spec.k
 tests/specs/mcd/flapper-yank-pass-rough-spec.k
+tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k
 tests/specs/mcd/flipper-bids-pass-rough-spec.k
 tests/specs/mcd/flipper-tau-pass-spec.k
 tests/specs/mcd/flipper-ttl-pass-spec.k
 tests/specs/mcd/flopper-cage-pass-spec.k
 tests/specs/mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k
 tests/specs/mcd/flopper-dent-guy-same-pass-rough-spec.k
-tests/specs/mcd/flopper-file-pass-rough-spec.k
 tests/specs/mcd/flopper-kick-pass-rough-spec.k
 tests/specs/mcd/flopper-tick-pass-rough-spec.k
 tests/specs/mcd/functional-spec.k
 tests/specs/mcd/pot-join-pass-rough-spec.k
-tests/specs/mcd/vow-fess-fail-rough-spec.k
-tests/specs/mcd/vow-flog-fail-rough-spec.k
 tests/specs/mcd-structured/cat-exhaustiveness-spec.k
 tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k
+tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k
 tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k
 tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k
-tests/specs/mcd-structured/dsvalue-read-pass-spec.k
 tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k
 tests/specs/mcd-structured/end-cash-pass-rough-spec.k
 tests/specs/mcd-structured/end-pack-pass-rough-spec.k
 tests/specs/mcd-structured/end-subuu-pass-spec.k
 tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k
+tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k
 tests/specs/mcd-structured/flipper-bids-pass-rough-spec.k
-tests/specs/mcd-structured/flipper-tau-pass-spec.k
-tests/specs/mcd-structured/flipper-ttl-pass-spec.k
 tests/specs/mcd-structured/flopper-cage-pass-spec.k
 tests/specs/mcd-structured/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k
 tests/specs/mcd-structured/flopper-dent-guy-same-pass-rough-spec.k
-tests/specs/mcd-structured/flopper-file-pass-rough-spec.k
 tests/specs/mcd-structured/flopper-kick-pass-rough-spec.k
 tests/specs/mcd-structured/flopper-tick-pass-rough-spec.k
 tests/specs/mcd-structured/functional-spec.k
 tests/specs/mcd-structured/pot-join-pass-rough-spec.k
 tests/specs/mcd-structured/vow-fess-fail-rough-spec.k
-tests/specs/mcd-structured/vow-flog-fail-rough-spec.k
+tests/specs/mcd-structured/vow-flog-fail-rough-spec.k
+tests/specs/mcd/vow-fess-fail-rough-spec.k
+tests/specs/mcd/vow-flog-fail-rough-spec.k