Updates to the conformance test suite (#2432)

* */: remove uses of LegacyTests in repository * test_conformance: run each test individually with log messages * .github/test-pr: skip submodule checkout on local checks * Set Version: 1.0.561 * .github/test-pr: only clone the needed submodules for each job, never LegacyTests * kevm-pyk/tests: move all unit/profiling test data as copies into this repo * .github/test-pr: correct plugin submodule directory * .github/test-pr: correct how we get submodules * .github/test-pr: stages which need ethereum-tests should rely on git caching * tests/interactive, package/test-package, flake.nix, .github/test-pr: avoid needing ethereum-tests for Nix jobs * .github/: actions/checkout@v3 => actions/checkout@v4 * .github/: update setup-poetry action from v8 => v9 * Makefile: make interactive tests not reach into submodules * flake.lock: update * tests/interactive/add.json: add newline * Set Version: 1.0.562 * Set Version: 1.0.563 * kevm-pyk/interpreter: always check return code on abnormal exit instead of running kore parser * Set Version: 1.0.566 * kevm-pyk/interpret: actually check on empty output for return code * kevm-pyk/interpreter: make an effort to fail more gracefully on bad interpreter output * Revert "kevm-pyk/interpreter: make an effort to fail more gracefully on bad interpreter output" This reverts commit 2ed9ce5. * Revert "kevm-pyk/interpret: actually check on empty output for return code" This reverts commit d623bd3. * Revert "kevm-pyk/interpreter: always check return code on abnormal exit instead of running kore parser" This reverts commit 2132b49. * Set Version: 1.0.568 * .github/Dockerfile: try upgraded poetry version * .github/Dockerfile: even newer version of poetry * Set Version: 1.0.569 * Set Version: 1.0.570 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · May 23, 2024 · cc3c92b · cc3c92b
1 parent 27cdad2
commit cc3c92b
Show file tree

Hide file tree

Showing 18 changed files with 594,119 additions and 117 deletions.
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
@@ -44,5 +44,5 @@ WORKDIR /home/${USER}/workspace
 
 ENV PATH=/home/${USER}/.local/bin:${PATH}
 
-RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.6.1 \
+RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.8.3 \
     && poetry --version
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
@@ -20,7 +20,7 @@ jobs:
     runs-on: ${{ matrix.runner }}
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           ref: ${{ github.event.push.head.sha }}
           fetch-depth: 0
@@ -59,7 +59,7 @@ jobs:
     needs: nix-cache
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           ref: ${{ github.event.push.head.sha }}
           fetch-depth: 0
@@ -88,7 +88,7 @@ jobs:
     needs: make-release
     steps:
       - name: 'Check out gh-pages'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
           submodules: true

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -14,7 +14,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           # fetch-depth 0 means deep clone the repo
@@ -40,11 +40,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Run code quality checks'
         run: make -C kevm-pyk check
       - name: 'Run pyupgrade'
@@ -56,11 +54,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Run unit tests'
         run: make -C kevm-pyk cov-unit
 
@@ -70,11 +66,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Run profiling'
         run: |
           make -C kevm-pyk profile
@@ -86,7 +80,7 @@ jobs:
     timeout-minutes: 45
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
       - name: 'Set up Docker'
@@ -128,9 +122,11 @@ jobs:
     timeout-minutes: ${{ matrix.timeout }}
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
+      - name: 'Check out select submodules'
+        run: |
+          set -eux
+          git submodule update --init --recursive -- kevm-pyk/src/kevm_pyk/kproj/plugin
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
@@ -160,10 +156,14 @@ jobs:
     timeout-minutes: 60
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           # Check out pull request HEAD instead of merge commit.
           ref: ${{ github.event.pull_request.head.sha }}
+      - name: 'Check out select submodules'
+        run: |
+          set -eux
+          git submodule update --init --recursive -- kevm-pyk/src/kevm_pyk/kproj/plugin
       - name: 'Install Nix'
         if: ${{ matrix.runner == 'macos-13' }}
         uses: cachix/install-nix-action@v25

diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 'Check out code'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
@@ -27,7 +27,7 @@ jobs:
           git config user.name devops
           git config user.email [email protected]
       - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+        uses: Gr1N/setup-poetry@v9
       - name: 'Update pyk release tag'
         run: |
           K_VERSION=v$(cat deps/k_release)

diff --git a/Makefile b/Makefile
@@ -135,8 +135,8 @@ KRUN_OPTS     ?=
 KEEP_OUTPUTS  := false
 CHECK         := git --no-pager diff --no-index --ignore-all-space -R
 
-tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_MODE     = VMTESTS
-tests/ethereum-tests/LegacyTests/Constantinople/VMTests/%: KEVM_SCHEDULE = DEFAULT
+tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_MODE     = VMTESTS
+tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/%: KEVM_SCHEDULE = DEFAULT
 
 tests/%.run-interactive: tests/%
 	$(POETRY_RUN) kevm-pyk run $< $(KEVM_OPTS) $(KRUN_OPTS) --target $(TEST_CONCRETE_BACKEND)                          \
@@ -145,8 +145,7 @@ tests/%.run-interactive: tests/%
 	    || $(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/templates/output-success-$(TEST_CONCRETE_BACKEND).json
 	$(KEEP_OUTPUTS) || rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 
-interactive_tests = tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json      \
-                    tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmIOandFlowOperations/pop1.json \
+interactive_tests = tests/interactive/add.json    \
                     tests/interactive/sumTo10.evm
 
 .PHONY: test-interactive

diff --git a/README.md b/README.md
@@ -284,10 +284,10 @@ For Developers
 If built from the source, the `kevm-pyk` executable will be installed in a virtual environemtn handled by Poetry.
 You can call `kevm-pyk --help` to get a quick summary of how to use the script.
 
-Run the file `tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json`:
+Run the file `tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json`:
 
 ```sh
-poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS
+poetry -C kevm-pyk run kevm-pyk run tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json --schedule DEFAULT --mode VMTESTS
 ```
 
 To enable the debug symbols for the llvm backend, build using this command:

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -15,20 +15,10 @@
       inputs.flake-utils.follows = "k-framework/flake-utils";
       inputs.nixpkgs.follows = "k-framework/nixpkgs";
     };
-    ethereum-tests = {
-      url = "github:ethereum/tests/6401889dec4eee58e808fd178fb2c7f628a3e039";
-      flake = false;
-    };
-    ethereum-legacytests = {
-      url =
-        "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7";
-      flake = false;
-    };
     haskell-backend.follows = "k-framework/haskell-backend";
   };
   outputs = { self, k-framework, haskell-backend, nixpkgs, flake-utils
-    , blockchain-k-plugin, ethereum-tests, ethereum-legacytests, rv-utils, pyk
-    , ... }@inputs:
+    , blockchain-k-plugin, rv-utils, pyk, ... }@inputs:
     let
       nixLibs = pkgs:
         with pkgs;
@@ -127,9 +117,6 @@
             buildInputs = [ final.kevm prev.which prev.git ];
 
             buildPhase = ''
-              mkdir -p tests/ethereum-tests/LegacyTests
-              cp -r ${ethereum-tests}/* tests/ethereum-tests/
-              cp -r ${ethereum-legacytests}/* tests/ethereum-tests/LegacyTests/
               chmod -R u+w tests
               APPLE_SILICON=${
                 if prev.stdenv.isAarch64 && prev.stdenv.isDarwin then
@@ -237,16 +224,12 @@
           };
 
           check-submodules = rv-utils.lib.check-submodules pkgs {
-            inherit k-framework blockchain-k-plugin ethereum-tests
-              ethereum-legacytests;
+            inherit k-framework blockchain-k-plugin;
           };
 
           update-from-submodules =
             rv-utils.lib.update-from-submodules pkgs ./flake.lock {
               blockchain-k-plugin.submodule = "deps/plugin";
-              ethereum-tests.submodule = "tests/ethereum-tests";
-              ethereum-legacytests.submodule =
-                "tests/ethereum-tests/LegacyTests";
             };
         };
       }) // {

diff --git a/kevm-pyk/src/tests/integration/test_conformance.py b/kevm-pyk/src/tests/integration/test_conformance.py
@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 import json
+import logging
 import sys
 from typing import TYPE_CHECKING
 
@@ -21,22 +22,24 @@
     from pyk.kore.syntax import Pattern
 
 
+_LOGGER: Final = logging.getLogger(__name__)
+_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+
+
 sys.setrecursionlimit(10**8)
 
 TEST_DIR: Final = REPO_ROOT / 'tests/ethereum-tests'
 GOLDEN: Final = (REPO_ROOT / 'tests/templates/output-success-llvm.json').read_text().rstrip()
 
 
 def _test(gst_file: Path, schedule: str, mode: str, chainid: int, usegas: bool) -> None:
-    # Given
     with gst_file.open() as f:
         gst_data = json.load(f)
 
-    # When
-    res = interpret(gst_data, schedule, mode, chainid, usegas, check=False)
-
-    # Then
-    _assert_exit_code_zero(res)
+    for test_name, test in gst_data.items():
+        _LOGGER.info(f'Running test: {gst_file} - {test_name}')
+        res = interpret({test_name: test}, schedule, mode, chainid, usegas, check=False)
+        _assert_exit_code_zero(res)
 
 
 def _assert_exit_code_zero(pattern: Pattern) -> None:
@@ -65,7 +68,7 @@ def read_test_list(path: Path) -> list[Path]:
 
 SKIPPED_TESTS: Final = _skipped_tests()
 
-VM_TEST_DIR: Final = TEST_DIR / 'LegacyTests/Constantinople/VMTests'
+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)
@@ -90,15 +93,14 @@ def test_rest_vm(test_file: Path) -> None:
     _test(test_file, 'DEFAULT', 'VMTESTS', 1, True)
 
 
-BCHAIN_NEW_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests'
-BCHAIN_NEW_TESTS: Final = tuple(BCHAIN_NEW_TEST_DIR.glob('**/*.json'))
-
-BCHAIN_LEGACY_TEST_DIR: Final = TEST_DIR / 'LegacyTests/Constantinople/BlockchainTests/GeneralStateTests'
-BCHAIN_LEGACY_TESTS: Final = tuple(BCHAIN_LEGACY_TEST_DIR.glob('*/*.json'))
-
-ALL_BCHAIN_TESTS: Final = BCHAIN_NEW_TESTS + BCHAIN_LEGACY_TESTS
-BCHAIN_TESTS: Final = tuple(test_file for test_file in ALL_BCHAIN_TESTS if test_file not in SKIPPED_TESTS)
-REST_BCHAIN_TESTS: Final = tuple(test_file for test_file in ALL_BCHAIN_TESTS if test_file in SKIPPED_TESTS)
+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
+)
 
 
 @pytest.mark.parametrize(

diff --git a/kevm-pyk/src/tests/profiling/test_gst_to_kore.py b/kevm-pyk/src/tests/profiling/test_gst_to_kore.py
@@ -9,7 +9,7 @@
     from pyk.testing import Profiler
 
 
-GST_FILE = REPO_ROOT / 'tests/ethereum-tests/BlockchainTests/GeneralStateTests/stEIP1559/intrinsic.json'
+GST_FILE = REPO_ROOT / 'tests/interactive/intrinsic.json'
 
 
 def test_gst_to_kore(profile: Profiler) -> None:

diff --git a/kevm-pyk/src/tests/unit/test_gst_to_kore.py b/kevm-pyk/src/tests/unit/test_gst_to_kore.py
@@ -16,8 +16,8 @@
 
 TEST_DATA: Final = (
     (
-        'tests/ethereum-tests/GeneralStateTests/VMTests/vmLogTest/log3.json',
-        'tests/interactive/vmLogTest/log3.gst-to-kore.expected',
+        'tests/interactive/log3.json',
+        'tests/interactive/log3.gst-to-kore.expected',
     ),
     (
         'tests/interactive/log3_MaxTopic_d0g0v0.json',

diff --git a/package/test-package.sh b/package/test-package.sh
@@ -6,17 +6,13 @@ which kevm
 kevm --help
 kevm version
 
-kevm run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json --target llvm \
-    --mode VMTESTS --schedule DEFAULT --chainid 1                                                         \
-    > tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json.llvm-out         \
-    || git --no-pager diff --no-index --ignore-all-space -R tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json.llvm-out tests/templates/output-success-llvm.json
-rm -rf tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmArithmeticTest/add0.json.llvm-out
+kevm run tests/interactive/add.json --target llvm --mode VMTESTS --schedule DEFAULT --chainid 1 \
+    > tests/interactive/add.json.llvm-out                                                       \
+    || git --no-pager diff --no-index --ignore-all-space -R tests/interactive/add.json.llvm-out tests/templates/output-success-llvm.json
+rm -rf tests/interactive/add.json.llvm-out
 
-kevm run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmSystemOperations/TestNameRegistrator.json \
-    --target llvm --mode VMTESTS --schedule DEFAULT --chainid 1
-
-kevm run tests/ethereum-tests/LegacyTests/Constantinople/VMTests/vmSystemOperations/TestNameRegistrator.json \
-    --target haskell-standalone --mode VMTESTS --schedule DEFAULT --chainid 1
+kevm run tests/interactive/TestNameRegistrator.json --target llvm               --mode VMTESTS --schedule DEFAULT --chainid 1
+kevm run tests/interactive/TestNameRegistrator.json --target haskell-standalone --mode VMTESTS --schedule DEFAULT --chainid 1
 
 kevm kast tests/interactive/log3_MaxTopic_d0g0v0.json --target llvm > tests/interactive/log3_MaxTopic_d0g0v0.json.parse-out
 git --no-pager diff --no-index --ignore-all-space -R tests/interactive/log3_MaxTopic_d0g0v0.json.parse-out tests/interactive/log3_MaxTopic_d0g0v0.json.parse-expected
@@ -48,4 +44,4 @@ kevm prove tests/specs/benchmarks/structarg01-spec.k         \
     --definition tests/specs/benchmarks/verification/haskell \
     --save-directory proofs                                  \
     --verbose                                                \
-    --use-booster
+    --use-booster