Fix CI issue with svm installed solc (#1984)

* Update Foundry image version * Update expected output * Set Foundry version in `flake.nix` * Set Version: 1.0.244 * add smt args for test_foundry_auto_abstraction * Go back to monthly Foundry release for Nix The version set previously got removed from Foundry releases. * Add -vv to CI test * kevm-pyk/src/tests: update show tests to not include module names * Increase smt limits on test_foundry_fail --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Noah Watson <[email protected]>
runtimeverification · Aug 5, 2023 · 767d1fc · 767d1fc
1 parent afca544
commit 767d1fc
Show file tree

Hide file tree

Showing 20 changed files with 13 additions and 23 deletions.
diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile
@@ -1,6 +1,6 @@
 ARG K_COMMIT
 ARG Z3_VERSION
-FROM ghcr.io/foundry-rs/foundry:nightly-aeba75e4799f1e11e3daba98d967b83e286b0c4a as FOUNDRY
+FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY
 
 ARG K_COMMIT
 ARG Z3_VERSION
@@ -48,6 +48,6 @@ ENV PATH=/home/user/.cargo/bin:/home/user/.local/bin:${PATH}
 RUN    curl -sSL https://install.python-poetry.org | python3 - \
     && poetry --version
 
-RUN    cargo install svm-rs \
-    && svm install 0.8.13   \
+RUN    cargo install svm-rs --version 0.3.0 \
+    && svm install 0.8.13                   \
     && solc --version
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -151,7 +151,7 @@ jobs:
       - name: 'Build Foundry'
         run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make build-foundry -j2'
       - name: 'Foundry Prove'
-        run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove FOUNDRY_PAR=8'
+        run: docker exec -u user kevm-ci-foundry-${GITHUB_SHA} /bin/bash -c 'make test-foundry-prove PYTEST_ARGS=-vv'
       - name: 'Tear down Docker'
         if: always()
         run: |

diff --git a/flake.nix b/flake.nix
@@ -20,7 +20,7 @@
     pyk.url = "github:runtimeverification/pyk/v0.1.378";
     pyk.inputs.flake-utils.follows = "k-framework/flake-utils";
     pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs";
-    foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent release
+    foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases
   };
   outputs = { self, k-framework, haskell-backend, nixpkgs, flake-utils
     , poetry2nix, blockchain-k-plugin, ethereum-tests, ethereum-legacytests

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.243"
+version = "1.0.244"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected
@@ -402,7 +402,6 @@ Node 8:
 
 
 
-module SUMMARY-GASTEST.TESTINFINITEGAS:0D0C9300BB23DFBDCDC05EAA3D45C39CA87798AF97F51D3A5F19E5797173F8AF
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected
@@ -37,7 +37,6 @@
 
 
 
-module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:6F4CECC6FE5B992BCA7D43B6892BCF60D87BB07FC4271E89D94AB64FD368894E
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected
@@ -241,7 +241,6 @@ Node 5:
 
 
 
-module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-TRUE:3DF2624F4C6F69C010C40126FCC08E60DE452B26F40109EA2695F3EB3C2F06C9
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected
@@ -263,7 +263,6 @@ Node 7:
 
 
 
-module SUMMARY-ASSERTTEST.TESTFAIL-EXPECT-REVERT:8C9460863E423C69EA28E6D7F6167F2A22510258C6D8534A5BF5102B7DC057BD
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected
@@ -241,7 +241,6 @@ Node 5:
 
 
 
-module SUMMARY-ASSERTTEST.TEST-ASSERT-FALSE:9320042DEDB2B6F5F55E3AE7C62249F5576BF06F63688301AF12A2C82E7F8D73
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected
@@ -37,7 +37,6 @@
 
 
 
-module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:16A7699D12C81EFD9EE27BBBBC8ACBD80FB4134DFC1D9F1CA60A78A852760CD4
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected
@@ -291,7 +291,6 @@ Node 11:
 
 
 
-module SUMMARY-ASSERTTEST.TEST-FAILING-BRANCH:57F35EE0DF89C24EE8610C076F68AA5C1E1A0338FE9DEBD59A8D478140BAD19F
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected
@@ -293,7 +293,6 @@ Node 10:
 
 
 
-module SUMMARY-ASSERTTEST.TEST-REVERT-BRANCH:80E29FA31FAB13240B669D08C849A6E04E2C01D8BDDF0AAC97F22E3430852790
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected
@@ -261,7 +261,6 @@ Node 7:
 
 
 
-module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-FALSE:FB031F786D909D69013B966019380F002F94DE195642EB3F4596C7AA12728D84
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true.expected
@@ -79,7 +79,6 @@
 
 
 
-module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:6A4EE8E0EDE6D56D6B990B931083B060CCFB8EEE20363860FE73BC57749A7477
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected
@@ -292,7 +292,6 @@ Node 11:
 
 
 
-module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:2363B07A823640CA7A46C3A8C3A408B281FF03A19BEC0CB10C58A1248D965F00
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected
@@ -104,7 +104,6 @@
 
 
 
-module SUMMARY-LOOPSTEST.SUM-N:5B83D29E7FBE9C5BFC4443B393810AAC763F8AF1E512E97BAF71B27147246E70
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected b/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected
@@ -37,7 +37,6 @@
 
 
 
-module SUMMARY-SETUPDEPLOYTEST.TEST-EXTCODESIZE:B11BF5850C2C846A7F1CAD76FA8A6B8AE36C396416A46B77329EC79D27E9744C
 
 
     rule [BASIC-BLOCK-1-TO-3]: <foundry>

diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py
@@ -128,8 +128,8 @@ def test_foundry_fail(test_id: str, foundry_root: Path, update_expected_output:
         foundry_root,
         tests=[test_id],
         simplify_init=False,
-        smt_timeout=125,
-        smt_retry_limit=4,
+        smt_timeout=300,
+        smt_retry_limit=8,
         use_booster=use_booster,
         counterexample_info=True,
     )
@@ -186,6 +186,8 @@ def test_foundry_auto_abstraction(foundry_root: Path, update_expected_output: bo
     foundry_prove(
         foundry_root,
         tests=['GasTest.testInfiniteGas'],
+        smt_timeout=125,
+        smt_retry_limit=4,
         auto_abstract_gas=True,
     )
 
@@ -231,6 +233,7 @@ def assert_or_update_show_output(show_res: str, expected_file: Path, *, update:
                 '│   src: ',
                 '┃  │   src: ',
                 '   │   src: ',
+                'module',
             )
         )
     )

diff --git a/package/debian/changelog b/package/debian/changelog
@@ -1,4 +1,4 @@
-kevm (1.0.243) unstable; urgency=medium
+kevm (1.0.244) unstable; urgency=medium
 
   * Initial Release.
 

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.243
+1.0.244