Merge remote-tracking branch 'upstream/master' into separate-functional

Author: ehildenb

deps/k_release

@@ -1 +1 @@
-7.1.30
+7.1.33

flake.lock

@@ -2,11 +2,11 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.30";
+    k-framework.url = "github:runtimeverification/k/v7.1.33";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
-    pyk.url = "github:runtimeverification/k/v7.1.30?dir=pyk";
+    pyk.url = "github:runtimeverification/k/v7.1.33?dir=pyk";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
     blockchain-k-plugin = {

flake.nix

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.619"
+version = "1.0.622"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.30"
+kframework = "7.1.33"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

kevm-pyk/poetry.lock

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.619'
+VERSION: Final = '1.0.622'

kevm-pyk/pyproject.toml

@@ -62,6 +62,7 @@ def kevm_kompile(
     debug: bool = False,
     verbose: bool = False,
     type_inference_mode: str | TypeInferenceMode | None = None,
+    ignore_warnings: Iterable[str] = (),
 ) -> Path:
     if plugin_dir is None:
         plugin_dir = kdist.get('evm-semantics.plugin')
@@ -84,6 +85,7 @@ def kevm_kompile(
         debug=debug,
         verbose=verbose,
         type_inference_mode=type_inference_mode,
+        ignore_warnings=ignore_warnings,
     )
 
 
@@ -105,6 +107,7 @@ def run_kompile(
     debug: bool = False,
     verbose: bool = False,
     type_inference_mode: str | TypeInferenceMode | None = None,
+    ignore_warnings: Iterable[str] = (),
 ) -> Path:
     if type_inference_mode is None:
         type_inference_mode = TypeInferenceMode.SIMPLESUB
@@ -137,7 +140,11 @@ def run_kompile(
                     enable_llvm_debug=enable_llvm_debug,
                 )
                 return kompile(
-                    output_dir=output_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                    output_dir=output_dir,
+                    debug=debug,
+                    verbose=verbose,
+                    type_inference_mode=type_inference_mode,
+                    ignore_warnings=ignore_warnings,
                 )
 
             case KompileTarget.MAUDE:
@@ -155,7 +162,11 @@ def _kompile_maude() -> None:
 
                 def _kompile_haskell() -> None:
                     kompile_haskell(
-                        output_dir=output_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                        output_dir=output_dir,
+                        debug=debug,
+                        verbose=verbose,
+                        type_inference_mode=type_inference_mode,
+                        ignore_warnings=ignore_warnings,
                     )
 
                 with concurrent.futures.ThreadPoolExecutor(max_workers=2) as executor:
@@ -189,11 +200,16 @@ def _kompile_llvm() -> None:
                         debug=debug,
                         verbose=verbose,
                         type_inference_mode=type_inference_mode,
+                        ignore_warnings=ignore_warnings,
                     )
 
                 def _kompile_haskell() -> None:
                     kompile_haskell(
-                        output_dir=output_dir, debug=debug, verbose=verbose, type_inference_mode=type_inference_mode
+                        output_dir=output_dir,
+                        debug=debug,
+                        verbose=verbose,
+                        type_inference_mode=type_inference_mode,
+                        ignore_warnings=ignore_warnings,
                     )
 
                 with concurrent.futures.ThreadPoolExecutor(max_workers=2) as executor:

kevm-pyk/src/kevm_pyk/__init__.py

@@ -1,8 +1,10 @@
 from __future__ import annotations
 
+import csv
 import json
 import logging
 import sys
+from pathlib import Path
 from typing import TYPE_CHECKING
 
 import pytest
@@ -16,7 +18,6 @@
 from ..utils import REPO_ROOT
 
 if TYPE_CHECKING:
-    from pathlib import Path
     from typing import Final
 
     from pyk.kore.syntax import Pattern
@@ -33,11 +34,17 @@
 
 
 def _test(gst_file: Path, schedule: str, mode: str, chainid: int, usegas: bool) -> None:
+    skipped_gst_tests = SKIPPED_TESTS.get(gst_file, [])
+    if '*' in skipped_gst_tests:
+        pytest.skip()
+
     with gst_file.open() as f:
         gst_data = json.load(f)
 
     for test_name, test in gst_data.items():
         _LOGGER.info(f'Running test: {gst_file} - {test_name}')
+        if test_name in skipped_gst_tests:
+            continue
         res = interpret({test_name: test}, schedule, mode, chainid, usegas, check=False)
         _assert_exit_code_zero(res)
 
@@ -57,21 +64,27 @@ def _assert_exit_code_zero(pattern: Pattern) -> None:
     assert pretty == GOLDEN
 
 
-def _skipped_tests() -> set[Path]:
-    def read_test_list(path: Path) -> list[Path]:
-        return [REPO_ROOT / test_path for test_path in path.read_text().splitlines()]
+def _skipped_tests() -> dict[Path, list[str]]:
+    slow_tests = read_csv_file(REPO_ROOT / 'tests/slow.llvm')
+    failing_tests = read_csv_file(REPO_ROOT / 'tests/failing.llvm')
+    skipped: dict[Path, list[str]] = {}
+    for test_file, test in slow_tests + failing_tests:
+        test_file = TEST_DIR / test_file
+        skipped.setdefault(test_file, []).append(test)
+    return skipped
+
 
-    slow_tests = read_test_list(REPO_ROOT / 'tests/slow.llvm')
-    failing_tests = read_test_list(REPO_ROOT / 'tests/failing.llvm')
-    return set(slow_tests + failing_tests)
+def read_csv_file(csv_file: Path) -> tuple[tuple[Path, str], ...]:
+    with csv_file.open(newline='') as file:
+        reader = csv.reader(file)
+        return tuple((Path(row[0]), row[1]) for row in reader)
 
 
 SKIPPED_TESTS: Final = _skipped_tests()
 
 VM_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests/VMTests'
-ALL_VM_TESTS: Final = tuple(VM_TEST_DIR.glob('*/*.json'))
-VM_TESTS: Final = tuple(test_file for test_file in ALL_VM_TESTS if test_file not in SKIPPED_TESTS)
-REST_VM_TESTS: Final = tuple(test_file for test_file in ALL_VM_TESTS if test_file in SKIPPED_TESTS)
+VM_TESTS: Final = tuple(VM_TEST_DIR.glob('*/*.json'))
+SKIPPED_VM_TESTS: Final = tuple(test_file for test_file in VM_TESTS if test_file in SKIPPED_TESTS)
 
 
 @pytest.mark.parametrize(
@@ -86,27 +99,23 @@ def test_vm(test_file: Path) -> None:
 @pytest.mark.skip(reason='failing / slow VM tests')
 @pytest.mark.parametrize(
     'test_file',
-    REST_VM_TESTS,
-    ids=[str(test_file.relative_to(VM_TEST_DIR)) for test_file in REST_VM_TESTS],
+    SKIPPED_VM_TESTS,
+    ids=[str(test_file.relative_to(VM_TEST_DIR)) for test_file in SKIPPED_VM_TESTS],
 )
 def test_rest_vm(test_file: Path) -> None:
     _test(test_file, 'DEFAULT', 'VMTESTS', 1, True)
 
 
-BCHAIN_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests'
-ALL_BCHAIN_TESTS: Final = tuple(BCHAIN_TEST_DIR.glob('**/*.json'))
-BCHAIN_TESTS: Final = tuple(
-    test_file for test_file in ALL_BCHAIN_TESTS if test_file not in (list(SKIPPED_TESTS) + list(ALL_VM_TESTS))
-)
-REST_BCHAIN_TESTS: Final = tuple(
-    test_file for test_file in ALL_BCHAIN_TESTS if test_file in SKIPPED_TESTS and test_file not in ALL_VM_TESTS
-)
+ALL_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests'
+ALL_TESTS: Final = tuple(ALL_TEST_DIR.glob('**/*.json'))
+BCHAIN_TESTS: Final = tuple(test_file for test_file in ALL_TESTS if test_file not in set(VM_TESTS))
+SKIPPED_BCHAIN_TESTS: Final = tuple(test_file for test_file in BCHAIN_TESTS if test_file in SKIPPED_TESTS)
 
 
 @pytest.mark.parametrize(
     'test_file',
     BCHAIN_TESTS,
-    ids=[str(test_file.relative_to(TEST_DIR)) for test_file in BCHAIN_TESTS],
+    ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in BCHAIN_TESTS],
 )
 def test_bchain(test_file: Path) -> None:
     _test(test_file, 'SHANGHAI', 'NORMAL', 1, True)
@@ -115,8 +124,8 @@ def test_bchain(test_file: Path) -> None:
 @pytest.mark.skip(reason='failing / slow blockchain tests')
 @pytest.mark.parametrize(
     'test_file',
-    REST_BCHAIN_TESTS,
-    ids=[str(test_file.relative_to(TEST_DIR)) for test_file in REST_BCHAIN_TESTS],
+    SKIPPED_BCHAIN_TESTS,
+    ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in SKIPPED_BCHAIN_TESTS],
 )
 def test_rest_bchain(test_file: Path) -> None:
     _test(test_file, 'SHANGHAI', 'NORMAL', 1, True)

kevm-pyk/src/kevm_pyk/kompile.py

@@ -1 +1 @@
-1.0.619
+1.0.622

kevm-pyk/src/tests/integration/test_conformance.py

@@ -1,2 +1,2 @@
-tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmPerformance/loopMul.json
-tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmPerformance/loopExp.json
+BlockchainTests/GeneralStateTests/VMTests/vmPerformance/loopMul.json,*
+BlockchainTests/GeneralStateTests/VMTests/vmPerformance/loopExp.json,*