From a2eecfd2acea5185b82945cb6e14f85d57e31bc6 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Wed, 25 Sep 2024 10:02:01 -0600 Subject: [PATCH] Update dependency: deps/k_release (#2626) * deps/k_release: Set Version 7.1.146 * kevm-pyk/: sync poetry files pyk version 7.1.146 * flake.{nix,lock}: update Nix derivations * deps/k_release: Set Version 7.1.147 * kevm-pyk/: sync poetry files pyk version 7.1.147 * flake.{nix,lock}: update Nix derivations * deps/k_release: Set Version 7.1.148 * kevm-pyk/: sync poetry files pyk version 7.1.148 * flake.{nix,lock}: update Nix derivations * deps/k_release: Set Version 7.1.149 * kevm-pyk/: sync poetry files pyk version 7.1.149 * flake.{nix,lock}: update Nix derivations * add is_mergeable * format * finish test * fix --------- Co-authored-by: devops Co-authored-by: JianhongZhao Co-authored-by: Palina Tolmach --- .gitignore | 1 + deps/k_release | 2 +- flake.lock | 16 ++-- flake.nix | 2 +- kevm-pyk/poetry.lock | 8 +- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/kevm.py | 23 ++++++ kevm-pyk/src/tests/unit/test_kevm.py | 109 ++++++++++++++++++++++++++- 8 files changed, 147 insertions(+), 16 deletions(-) diff --git a/.gitignore b/.gitignore index bccb8eddfb..859f6eae87 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,4 @@ /tests/vm/*.out .DS_Store .idea/ +.vscode/ diff --git a/deps/k_release b/deps/k_release index 0fc5d288c1..acf79a8b24 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.145 +7.1.149 diff --git a/flake.lock b/flake.lock index 1950948db0..16007fd653 100644 --- a/flake.lock +++ b/flake.lock @@ -352,16 +352,16 @@ ] }, "locked": { - "lastModified": 1726685098, - "narHash": "sha256-FVCrOS4IAlA08ZiYlmaSdrLoYFmSd7UFiJem/Zg2C8o=", + "lastModified": 1726963552, + "narHash": "sha256-01rb87Oc9cDh1MinneK/c96DbdQMVwnym9uYz1gKec4=", "owner": "runtimeverification", "repo": "k", - "rev": "c418935015dba62f29b9ada1a55b710126385ab6", + "rev": "7e06a35da4f5f757a8373c6cbf83e86f492bc75a", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.145", + "ref": "v7.1.149", "repo": "k", "type": "github" } @@ -432,16 +432,16 @@ "utils": "utils_2" }, "locked": { - "lastModified": 1726098480, - "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=", + "lastModified": 1726776150, + "narHash": "sha256-A4OX0ZV4/AS+tztmLG52v/ayMV43WscbF6lLKOaoPrw=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6", + "rev": "c023bc5eb734c1718243d66613044e895e8fcf7e", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.88", + "ref": "v0.1.94", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index d20ae961cf..3b4735ee0e 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.145"; + k-framework.url = "github:runtimeverification/k/v7.1.149"; 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 da3286f960..4be255f078 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -505,13 +505,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.145" +version = "7.1.149" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.145-py3-none-any.whl", hash = "sha256:a9107a75d25906200db2510ccb931358b8b50eb5bbd0f60680d50ace994baa19"}, - {file = "kframework-7.1.145.tar.gz", hash = "sha256:2e6254450247ab79227fef430d3824076a377a8ec2a7648b8274c2e403d91938"}, + {file = "kframework-7.1.149-py3-none-any.whl", hash = "sha256:2999608dd3a62556145c0e59608abde14812289b930fad44854ede3a3101c995"}, + {file = "kframework-7.1.149.tar.gz", hash = "sha256:dff520a7478a02fc9cbb041b379cc8a1a06fb6557bd1dbd1df0fb6f8d9f20f46"}, ] [package.dependencies] @@ -1195,4 +1195,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "3e2f97ce725e1d4e33b80df5e63f959a824db55e3d3c60767d492703e5176472" +content-hash = "10464615e397a582a48386b388f76d6a60cce8d03d2b90a0980f5b9b9b66d3fd" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 437a052e97..5cd130a52a 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.145" +kframework = "7.1.149" tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 84ec965406..2023cd8db4 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -225,6 +225,29 @@ def can_make_custom_step(self, cterm: CTerm) -> bool: self._cached_subst = load_pattern.match(cterm.cell('K_CELL')) return self._cached_subst is not None + def is_mergeable(self, ct1: CTerm, ct2: CTerm) -> bool: + """Given two CTerms of Edges' targets, check if they are mergeable. + + Two CTerms are mergeable if their `STATUSCODE_CELL` and `PROGRAM_CELL` are the same. + If mergeable, the two corresponding Edges are merged into one. + + :param ct1: CTerm of one Edge's target. + :param ct2: CTerm of another Edge's target. + :return: `True` if the two CTerms are mergeable; `False` otherwise. + """ + status_code_1 = ct1.cell('STATUSCODE_CELL') + status_code_2 = ct2.cell('STATUSCODE_CELL') + program_1 = ct1.cell('PROGRAM_CELL') + program_2 = ct2.cell('PROGRAM_CELL') + if ( + type(status_code_1) is KApply + and type(status_code_2) is KApply + and type(program_1) is KToken + and type(program_2) is KToken + ): + return status_code_1 == status_code_2 and program_1 == program_2 + raise ValueError(f'Attempted to merge nodes with non-concrete or : {(ct1, ct2)}') + class KEVM(KProve, KRun): _use_hex: bool diff --git a/kevm-pyk/src/tests/unit/test_kevm.py b/kevm-pyk/src/tests/unit/test_kevm.py index 99df72432b..0c6ba81560 100644 --- a/kevm-pyk/src/tests/unit/test_kevm.py +++ b/kevm-pyk/src/tests/unit/test_kevm.py @@ -8,10 +8,11 @@ from typing import Final from pyk.kast.inner import KInner +from pyk.cterm.cterm import CTerm from pyk.kast.inner import KApply, KToken, KVariable from pyk.prelude.utils import token -from kevm_pyk.kevm import KEVM, compute_jumpdests +from kevm_pyk.kevm import KEVM, KEVMSemantics, compute_jumpdests TEST_DATA: Final = [ ('single-ktoken', token(0), KToken('0x0', 'Int')), @@ -108,3 +109,109 @@ def test_process_jumpdests(test_id: str, input: list[KInner], expected: KInner) # Then assert result == expected + + +IS_MERGEABLE_DATA: Final = [ + ( + 'mergeable_total_same', + [ + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + ], + True, + False, + ), + ( + 'mergeable_not_care_others', + [ + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + KApply('', token(b'\x00')), + ) + ), + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + KApply('', token(b'\x01')), + ) + ), + ], + True, + False, + ), + ( + 'not_mergeable', + [ + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + CTerm( + KApply( + '', + KApply('', KApply('EVMC_REVERT')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + ], + False, + True, + ), + ( + 'raise_error', + [ + CTerm( + KApply( + '', + KApply('', KToken('EVMC_SUCCESS', 'StatusCode')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + CTerm( + KApply( + '', + KApply('', KToken('EVMC_SUCCESS', 'StatusCode')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + ], + False, + True, + ), +] + + +@pytest.mark.parametrize( + 'test_id,input,expected,raise_error', + IS_MERGEABLE_DATA, + ids=[test_id for test_id, *_ in IS_MERGEABLE_DATA], +) +def test_is_mergeable(test_id: str, input: list[CTerm], expected: KInner, raise_error: bool) -> None: + # When + try: + result = KEVMSemantics().is_mergeable(input[0], input[1]) + except ValueError: + assert raise_error + return + # Then + assert result == expected