diff --git a/deps/k_release b/deps/k_release index abf92f03d7..baf7c35f3a 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.163 +7.1.169 diff --git a/flake.lock b/flake.lock index 898368b678..8e6f6e3ee3 100644 --- a/flake.lock +++ b/flake.lock @@ -243,16 +243,16 @@ "z3": "z3_2" }, "locked": { - "lastModified": 1729168859, - "narHash": "sha256-S9Vx0p6kDorS9NwnZb+QOTGpMKXwGlchCiiow881nTs=", + "lastModified": 1730331357, + "narHash": "sha256-94XaYki+qhuQHR6K5YkajbL6Vby0EjggReTP9unzPk4=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "712543ed61f5ca4365b84d0f7ef6d71a35349662", + "rev": "81fe80ccdfadb21c0a0c8488632afe8365cd884a", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.90", + "ref": "v0.1.95", "repo": "haskell-backend", "type": "github" } @@ -352,16 +352,16 @@ ] }, "locked": { - "lastModified": 1729209879, - "narHash": "sha256-6kDVw8CTZWJf8iHeWGO95/PZYJiQ85UtmqsN43oZ/JI=", + "lastModified": 1730344128, + "narHash": "sha256-tADlTseeQ2+/chkZ+1BKnBDhLuKptDzb3+yK2K4z1pg=", "owner": "runtimeverification", "repo": "k", - "rev": "bf646f946cebf36aa77f2eec4dd695cc1d99823e", + "rev": "ac5555f78ee2958c3f846dde5936357eafad891b", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.163", + "ref": "v7.1.169", "repo": "k", "type": "github" } @@ -432,16 +432,16 @@ "utils": "utils_2" }, "locked": { - "lastModified": 1729095682, - "narHash": "sha256-+mUxQhIwzIfBFIfnCjlbp06uWDYVbxq78FEQAgAB40E=", + "lastModified": 1730229432, + "narHash": "sha256-2Y4U7TCmSf9NAZCBmvXiHLOXrHxpiRgIpw5ERYDdNSM=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "84a419e02b1e378df4f012d8975c0e4f16f71783", + "rev": "d5eab4b0f0e610bc60843ebb482f79c043b92702", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.100", + "ref": "v0.1.103", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index a275238dbd..eb26ceb74e 100644 --- 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 index 55ed8934c7..da59bb29cf 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -400,13 +400,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.115.5" +version = "6.115.6" description = "A library for property-based testing" optional = false python-versions = ">=3.9" files = [ - {file = "hypothesis-6.115.5-py3-none-any.whl", hash = "sha256:b7733459ae9a93020fac3b91b41473c9b85e975139a152a70d88f3a5caa3fa3f"}, - {file = "hypothesis-6.115.5.tar.gz", hash = "sha256:4768c5fb426b305462ed31032d6e216a31daaefb1dc3134fdf2795b7961d7cb3"}, + {file = "hypothesis-6.115.6-py3-none-any.whl", hash = "sha256:d7b7173934753b9624680b38a85749de4fce367c44acb36c08b62765cc0a7a19"}, + {file = "hypothesis-6.115.6.tar.gz", hash = "sha256:d4db48eef183591085676783967e943bb89fef4d596f78c3e4116c61fcc63a6b"}, ] [package.dependencies] @@ -495,13 +495,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.163" +version = "7.1.169" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.163-py3-none-any.whl", hash = "sha256:811990c7bb1421928b2d823f38c652ae13c6e2618acd7de887d31c1da335011b"}, - {file = "kframework-7.1.163.tar.gz", hash = "sha256:5ddf3d3041505eae2aaafeca75371d56cef4add54ad441e32aa5e49de9114d12"}, + {file = "kframework-7.1.169-py3-none-any.whl", hash = "sha256:af0419d93285834568f2727bb66af4188736faf625a3bdfc331d9294ade1ea95"}, + {file = "kframework-7.1.169.tar.gz", hash = "sha256:e8e432466fc0a99fff230d4db826a0f2296899ff4dbd4f1226ab07fded3ce884"}, ] [package.dependencies] @@ -943,17 +943,17 @@ testing = ["argcomplete", "attrs (>=19.2.0)", "hypothesis (>=3.56)", "mock", "no [[package]] name = "pytest-cov" -version = "5.0.0" +version = "6.0.0" description = "Pytest plugin for measuring coverage." optional = false -python-versions = ">=3.8" +python-versions = ">=3.9" files = [ - {file = "pytest-cov-5.0.0.tar.gz", hash = "sha256:5837b58e9f6ebd335b0f8060eecce69b662415b16dc503883a02f45dfeb14857"}, - {file = "pytest_cov-5.0.0-py3-none-any.whl", hash = "sha256:4f0764a1219df53214206bf1feea4633c3b558a2925c8b59f144f682861ce652"}, + {file = "pytest-cov-6.0.0.tar.gz", hash = "sha256:fde0b595ca248bb8e2d76f020b465f3b107c9632e6a1d1705f17834c89dcadc0"}, + {file = "pytest_cov-6.0.0-py3-none-any.whl", hash = "sha256:eee6f1b9e61008bd34975a4d5bab25801eb31898b032dd55addc93e96fcaaa35"}, ] [package.dependencies] -coverage = {version = ">=5.2.1", extras = ["toml"]} +coverage = {version = ">=7.5", extras = ["toml"]} pytest = ">=4.6" [package.extras] @@ -1045,23 +1045,23 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"] [[package]] name = "setuptools" -version = "75.2.0" +version = "75.3.0" description = "Easily download, build, install, upgrade, and uninstall Python packages" optional = false python-versions = ">=3.8" files = [ - {file = "setuptools-75.2.0-py3-none-any.whl", hash = "sha256:a7fcb66f68b4d9e8e66b42f9876150a3371558f98fa32222ffaa5bced76406f8"}, - {file = "setuptools-75.2.0.tar.gz", hash = "sha256:753bb6ebf1f465a1912e19ed1d41f403a79173a9acf66a42e7e6aec45c3c16ec"}, + {file = "setuptools-75.3.0-py3-none-any.whl", hash = "sha256:f2504966861356aa38616760c0f66568e535562374995367b4e69c7143cf6bcd"}, + {file = "setuptools-75.3.0.tar.gz", hash = "sha256:fba5dd4d766e97be1b1681d98712680ae8f2f26d7881245f2ce9e40714f1a686"}, ] [package.extras] check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)", "ruff (>=0.5.2)"] -core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.collections", "jaraco.functools", "jaraco.text (>=3.7)", "more-itertools", "more-itertools (>=8.8)", "packaging", "packaging (>=24)", "platformdirs (>=2.6.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"] +core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.collections", "jaraco.functools", "jaraco.text (>=3.7)", "more-itertools", "more-itertools (>=8.8)", "packaging", "packaging (>=24)", "platformdirs (>=4.2.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"] cover = ["pytest-cov"] doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier", "towncrier (<24.7)"] enabler = ["pytest-enabler (>=2.2)"] -test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-home (>=0.5)", "pytest-perf", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel (>=0.44.0)"] -type = ["importlib-metadata (>=7.0.2)", "jaraco.develop (>=7.21)", "mypy (==1.11.*)", "pytest-mypy"] +test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test (>=5.5)", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-home (>=0.5)", "pytest-perf", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel (>=0.44.0)"] +type = ["importlib-metadata (>=7.0.2)", "jaraco.develop (>=7.21)", "mypy (==1.12.*)", "pytest-mypy"] [[package]] name = "sortedcontainers" @@ -1196,4 +1196,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "c1ee12c1c59bbde777325841ffc337a34b7c0aac95e09d9763677067282e335a" +content-hash = "4b85ffb505cd654b4bab0173d61d9e8e3bc07849881fc29ab065997c8874d861" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 5ef7ec0f92..b6a95bd885 100644 --- 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 index 02eb3da773..23f1453486 100644 --- 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 index ee4f4617e1..43e3f90daa 100644 --- 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 index bf74746c3f..82f8c788d3 100644 --- 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 index 56f673a5cc..5708f1ae4b 100644 --- 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 JUMP DEST => #endBasicBlock ... + rule [jump]: + JUMP DEST => #endBasicBlock ... _ => DEST DESTS requires DEST