Pre-kompile K definitions and specs for integration tests (#2417)

* Towards in-advance kompilation of definitions in tests

* Allow a permanent prekompiled directory

* Run less tests, for debugging purposes

* Add test_kompile_targets

* Add file lock

* De-dupe targets in a smarter way

* Don't prekompile definitions for failing tests

* Add __eq__ override to Target

* Use target name as cache key, add cache debug msgs

* Actually read cache from disk

* Revert "Run less tests, for debugging purposes"

This reverts commit 5858d0a.

* Remove debugging messages

* Correct path stuff

* Consolidate conftest.py

* Add comments

* Add pytest marker for prekompilation

* Add more comments

* Skip prekompiling in the same way as proving

* Remove Target.__eq__, improve comments

* Set Version: 1.0.546

* Skip kompilation cache test

* Skip prekompilation test if no --kompiled-targets-dir is given

* Code style

* Add smtlib markers to Word operations

* Revert "Add smtlib markers to Word operations"

This reverts commit 0ab98ac.

* Remove redundant parameter

* Revert "Remove redundant parameter"

This reverts commit 54c5c4a.

* Set Version: 1.0.548

---------

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

Author: geo2a

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__init__.py

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

kevm-pyk/src/tests/conftest.py

@@ -3,9 +3,12 @@
 from typing import TYPE_CHECKING
 
 import pytest
+from pyk.cli.utils import dir_path
 
 if TYPE_CHECKING:
-    from pytest import FixtureRequest, Parser
+    from pathlib import Path
+
+    from pytest import FixtureRequest, Parser, TempPathFactory
 
 
 def pytest_addoption(parser: Parser) -> None:
@@ -27,6 +30,11 @@ def pytest_addoption(parser: Parser) -> None:
         type=str,
         help='Run only this specific specification (skip others)',
     )
+    parser.addoption(
+        '--kompiled-targets-dir',
+        type=dir_path,
+        help='Use pre-kompiled definitions for proof tests',
+    )
 
 
 @pytest.fixture
@@ -42,3 +50,12 @@ def use_booster(request: FixtureRequest) -> bool:
 @pytest.fixture(scope='session')
 def spec_name(request: FixtureRequest) -> str | None:
     return request.config.getoption('--spec-name')
+
+
+@pytest.fixture(scope='session')
+def kompiled_targets_dir(request: FixtureRequest, tmp_path_factory: TempPathFactory) -> Path:
+    dir = request.config.getoption('--kompiled-targets-dir')
+    if dir:
+        return dir
+    else:
+        return tmp_path_factory.mktemp('prekompiled')

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

@@ -5,6 +5,7 @@
 from typing import TYPE_CHECKING, NamedTuple
 
 import pytest
+from filelock import FileLock
 from pyk.prelude.ml import is_top
 from pyk.proof.reachability import APRProof
 
@@ -21,7 +22,7 @@
     from typing import Any, Final
 
     from pyk.utils import BugReport
-    from pytest import LogCaptureFixture, TempPathFactory
+    from pytest import FixtureRequest, LogCaptureFixture
 
 
 sys.setrecursionlimit(10**8)
@@ -118,31 +119,58 @@ class Target(NamedTuple):
     main_file: Path
     main_module_name: str
 
+    @property
+    def name(self) -> str:
+        """
+        Target's name is the two trailing path segments and the main module name
+        """
+        return f'{self.main_file.parts[-2]}-{self.main_file.stem}-{self.main_module_name}'
+
     def __call__(self, output_dir: Path) -> Path:
-        return kevm_kompile(
-            output_dir=output_dir / 'kompiled',
-            target=KompileTarget.HASKELL,
-            main_file=self.main_file,
-            main_module=self.main_module_name,
-            syntax_module=self.main_module_name,
-            debug=True,
-        )
+        with FileLock(str(output_dir) + '.lock'):
+            return kevm_kompile(
+                output_dir=output_dir / 'kompiled',
+                target=KompileTarget.HASKELL,
+                main_file=self.main_file,
+                main_module=self.main_module_name,
+                syntax_module=self.main_module_name,
+                debug=True,
+            )
+
+
+@pytest.fixture(scope='module')
+def kompiled_target_cache(kompiled_targets_dir: Path) -> tuple[Path, dict[str, Path]]:
+    """
+    Populate the cache of kompiled definitions from an existing file system directory. If the cache is hot, the `kompiled_target_for` fixture will not containt a call to `kompile`, saving an expesive call to the K frontend.
+    """
+    cache_dir = kompiled_targets_dir / 'target'
+    cache: dict[str, Path] = {}
+    if cache_dir.exists():  # cache dir exists, populate cache
+        for file in cache_dir.iterdir():
+            if file.is_dir():
+                # the cache key is the name of the target, which is the filename by-construction.
+                cache[file.stem] = file / 'kompiled'
+    else:
+        cache_dir.mkdir(parents=True)
+    return cache_dir, cache
 
 
 @pytest.fixture(scope='module')
-def kompiled_target_for(tmp_path_factory: TempPathFactory) -> Callable[[Path], Path]:
-    cache_dir = tmp_path_factory.mktemp('target')
-    cache: dict[Target, Path] = {}
+def kompiled_target_for(kompiled_target_cache: tuple[Path, dict[str, Path]]) -> Callable[[Path], Path]:
+    """
+    Generate a function that returns a path to the kompiled defintion for a given K spec. Invoke `kompile` only if no kompiled directory is cached for the spec.
+    """
+    cache_dir, cache = kompiled_target_cache
 
     def kompile(spec_file: Path) -> Path:
         target = _target_for_spec(spec_file)
 
-        if target not in cache:
-            output_dir = cache_dir / f'{target.main_file.stem}-{len(cache)}'
-            output_dir.mkdir()
-            cache[target] = target(output_dir)
+        if target.name not in cache:
+            output_dir = cache_dir / target.name
+            output_dir.mkdir(exist_ok=True)
+            cache[target.name] = target(output_dir)
 
-        return cache[target]
+        return cache[target.name]
 
     return kompile
 
@@ -156,6 +184,32 @@ def _target_for_spec(spec_file: Path) -> Target:
     return Target(main_file, main_module_name)
 
 
+@pytest.mark.parametrize(
+    'spec_file',
+    ALL_TESTS,
+    ids=[str(spec_file.relative_to(SPEC_DIR)) for spec_file in ALL_TESTS],
+)
+def test_kompile_targets(spec_file: Path, kompiled_target_for: Callable[[Path], Path], request: FixtureRequest) -> None:
+    """
+    This test function is intended to be used to pre-kompile all definitions,
+    so that the actual proof tests do not need to do the actual compilation,
+    which is disturbing performance measurment.
+
+    To achieve the desired caching, this test should be run like this:
+    pytest src/tests/integration/test_prove.py::test_kompile_targets --kompiled-targets-dir ./prekompiled
+
+    This test will be skipped if no --kompiled-targets-dir option is given
+    """
+    dir = request.config.getoption('--kompiled-targets-dir')
+    if not dir:
+        pytest.skip()
+
+    if spec_file in FAILING_BOOSTER_TESTS:
+        pytest.skip()
+
+    kompiled_target_for(spec_file)
+
+
 # ---------
 # Pyk tests
 # ---------

package/version

@@ -1 +1 @@
-1.0.547
+1.0.548