Add profile test for foundry_prove (#1982)

* Run proofs in the main process on `workers=1`

* Add profile test

* Remove `pytest.ini`

By default `pytest` would set `rootdir` to its parent.

* Add option to prove with Booster

* Run profiling in Docker container

* Update kevm-pyk/src/tests/profiling/test-data/foundry/foundry.toml

Co-authored-by: Everett Hildenbrandt <[email protected]>

* Mark target `profile` exlicitly as `.PHONY`

* Set Version: 1.0.248

---------

Co-authored-by: Everett Hildenbrandt <[email protected]>
Co-authored-by: devops <[email protected]>

.github/workflows/test-pr.yml

@@ -64,18 +64,29 @@ jobs:
   kevm-pyk-profile:
     needs: kevm-pyk-code-quality-checks
     name: 'Profiling'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 15
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
         with:
-          submodules: true
-      - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
+          submodules: recursive
+          fetch-depth: 0
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          tag: kevm-ci-profile-${{ github.sha }}
+      - name: 'Build kevm-pyk'
+        run: docker exec -u user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make poetry'
+      - name: 'Build Foundry'
+        run: docker exec -u user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make build-foundry'
       - name: 'Run profiling'
         run: |
-          make -C kevm-pyk profile
-          find /tmp/pytest-of-${USER}/pytest-current/ -type f | sort | xargs tail -n +1
+          docker exec -u user kevm-ci-profile-${GITHUB_SHA} /bin/bash -c 'make profile'
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 kevm-ci-profile-${GITHUB_SHA}
 
   test-concrete-execution:
     name: 'Build and Test KEVM concrete execution'

Makefile

@@ -50,6 +50,7 @@ export PLUGIN_FULL_PATH
         build build-haskell build-haskell-standalone build-foundry build-llvm build-node build-kevm      	\
         test test-integration test-conformance test-prove test-foundry-prove test-prove-smoke            	\
         test-vm test-rest-vm test-bchain test-rest-bchain test-node test-interactive test-interactive-run	\
+        profile                                                                                             \
         media media-pdf metropolis-theme
 
 .SECONDARY:
@@ -493,6 +494,10 @@ tests/specs/opcodes/evm-optimizations-spec.md: include/kframework/optimizations.
 test-integration: poetry build-kevm build-haskell build-llvm
 	$(MAKE) -C kevm-pyk/ test-integration TEST_ARGS+='-k "(test_kast.py or test_run.py or test_solc_to_k.py)" -n$(PYTEST_PARALLEL) $(PYTEST_ARGS)'
 
+profile: poetry build-foundry
+	$(MAKE) -C kevm-pyk/ profile PROF_ARGS+='-n$(PYTEST_PARALLEL) $(PYTEST_ARGS)'
+	find /tmp/pytest-of-$$(whoami)/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
+
 # Interactive Tests
 
 test-interactive: test-interactive-run

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.247"
+version = "1.0.248"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/foundry.py

@@ -557,11 +557,22 @@ def _init_and_run_proof(_init_problem: tuple[str, str]) -> tuple[bool, list[str]
             return passed, failure_log
 
     def run_cfg_group(tests: list[str]) -> dict[str, tuple[bool, list[str] | None]]:
-        init_problems = [tuple(test.split('.')) for test in tests]
-        with ProcessPool(ncpus=workers) as process_pool:
-            _apr_proofs = process_pool.map(_init_and_run_proof, init_problems)
-        apr_proofs = dict(zip(tests, _apr_proofs, strict=True))
+        def _split_test(test: str) -> tuple[str, str]:
+            contract, method = test.split('.')
+            return contract, method
+
+        init_problems = [_split_test(test) for test in tests]
 
+        _apr_proofs: list[tuple[bool, list[str] | None]]
+        if workers > 1:
+            with ProcessPool(ncpus=workers) as process_pool:
+                _apr_proofs = process_pool.map(_init_and_run_proof, init_problems)
+        else:
+            _apr_proofs = []
+            for init_problem in init_problems:
+                _apr_proofs.append(_init_and_run_proof(init_problem))
+
+        apr_proofs = dict(zip(tests, _apr_proofs, strict=True))
         return apr_proofs
 
     _LOGGER.info(f'Running setup functions in parallel: {list(setup_methods.values())}')

kevm-pyk/src/tests/profiling/test-data/foundry/foundry.toml

@@ -0,0 +1,4 @@
+[profile.default]
+src = 'src'
+out = 'out'
+extra_output = ['storageLayout', 'abi', 'evm.methodIdentifiers', 'evm.deployedBytecode.object']

kevm-pyk/src/tests/profiling/test-data/foundry/test/Simple.t.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+
+contract AssertTest is Test {
+
+    function test_revert_branch(uint x, uint y) public{
+        if (x < y) {
+            assert(true);
+        } else {
+            assert(false);
+        }
+    }
+}

kevm-pyk/src/tests/profiling/test_foundry_prove.py

@@ -0,0 +1,55 @@
+from __future__ import annotations
+
+import sys
+from distutils.dir_util import copy_tree
+from typing import TYPE_CHECKING
+
+from pyk.utils import run_process
+
+from kevm_pyk import config
+from kevm_pyk.foundry import foundry_kompile, foundry_prove
+
+from .utils import TEST_DATA_DIR
+
+if TYPE_CHECKING:
+    from pathlib import Path
+    from typing import Final
+
+    from pyk.testing import Profiler
+
+
+sys.setrecursionlimit(10**7)
+
+
+FORGE_STD_REF: Final = '27e14b7'
+
+
+def test_foundy_prove(profile: Profiler, use_booster: bool, tmp_path: Path) -> None:
+    foundry_root = tmp_path / 'foundry'
+
+    _forge_build(foundry_root)
+
+    with profile('kompile.prof', sort_keys=('cumtime', 'tottime'), limit=15):
+        foundry_kompile(
+            definition_dir=config.FOUNDRY_DIR,
+            foundry_root=foundry_root,
+            includes=(),
+            llvm_library=use_booster,
+        )
+
+    with profile('prove.prof', sort_keys=('cumtime', 'tottime'), limit=100):
+        foundry_prove(
+            foundry_root,
+            tests=['AssertTest.test_revert_branch'],
+            simplify_init=False,
+            smt_timeout=125,
+            smt_retry_limit=4,
+            counterexample_info=True,
+            use_booster=use_booster,
+        )
+
+
+def _forge_build(target_dir: Path) -> None:
+    copy_tree(str(TEST_DATA_DIR / 'foundry'), str(target_dir))
+    run_process(['forge', 'install', '--no-git', f'foundry-rs/forge-std@{FORGE_STD_REF}'], cwd=target_dir)
+    run_process(['forge', 'build'], cwd=target_dir)

kevm-pyk/src/tests/profiling/utils.py

@@ -0,0 +1,10 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from typing import Final
+
+
+TEST_DATA_DIR: Final = (Path(__file__).parent / 'test-data').resolve(strict=True)

package/debian/changelog

@@ -1,4 +1,4 @@
-kevm (1.0.247) unstable; urgency=medium
+kevm (1.0.248) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-1.0.247
+1.0.248