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

geo2a · 2024-05-08T15:43:12Z

This PR modifies the RPC prover test harness in test_prove.py, to allow in-advance kompilation of the K definitions. This greatly improves the reliability and precision of the Haskell Backend performance measurement in scripts when we run several proofs in parallel. By separating the kompilation and proving stages, we reduce the noise caused by the K frontend.

An overview of changes:

add a new custom --kompiled-targets-dir command line option to pytest, allowing to set persistent cache directory for the kompiled definitions used by the testsl;
add the kompiled_target_cache fixture to test_prove.py that will read the persitent cache from disk if --kompiled-targets-dir is provided;
add the test_kompile_targets test to test_prove.py that forces the kompilation of all targets. If --kompiled-targets-dir is provided, the targets' kompiled directories will be stored there and could be re-used by the following pytest sessions that are given the same --kompiled-targets-dir. This test will be skipped if --kompiled-targets-dir is not given, making sure the CI configuration does not have to be changed to ignore it explicitly.

For example, after executing

pytest src/tests/integration/test_prove.py::test_kompile_targets --kompiled-targets-dir ./prekompiled

the ./prekompiled will be populated with the following subdirectories:

benchmarks-verification
bihu-functional-spec
bihu-verification
erc20-verification
examples-erc20-spec
examples-solidity-code-spec
examples-storage-spec
functional-abi-spec
functional-evm-int-simplifications-spec
kontrol-verification
mcd-functional-spec
mcd-verification

The invocation

pytest src/tests/integration -k "test_prove_pyk" --kompiled-targets-dir ./prekompiled

will now be able to re-use the kompilation artefacts and would not have to make expensive and scheduling-disrupting calls to kompile.

This reverts commit 5858d0a.

This reverts commit 0ab98ac.

tothtamas28 · 2024-05-09T07:35:36Z

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

+                cache[file.stem] = file / 'kompiled'
+    else:
+        cache_dir.mkdir(parents=True)
+    return cache_dir, cache


Consider abstracting this in a class.

tothtamas28 · 2024-05-09T07:37:21Z

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

-            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:


Target already uniquely identifies a kompilation target, it's probably not necessary to change the key to a str derived from it.

It is not possible to construct a Target when initializing the cache from a directory in kompiled_target_cache, as I have nothing to construct the main_file field from.

tothtamas28 · 2024-05-09T07:38:44Z

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

-            cache[target] = target(output_dir)
+        if target.name not in cache:
+            output_dir = cache_dir / target.name
+            output_dir.mkdir(exist_ok=True)


Is this to cover the case when the user points to an already existing cache to rekompile it?

Right, exist_ok=True is indeed unnecessary as the directory should never exist if the target is not already cached.

Hmm, turns out it is actually easier if we keep exist_ok=True, and let the tests wait on the lock to populate/read it, rather then fail to create it if it exists.

tothtamas28 · 2024-05-09T07:46:41Z

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

+        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'


Initializing a cache might be unnecessary, you can just do the directory lookup when you request the kompiled directory.

I don't understand what you mean: could you elaborate?

My goals are:

keep using cache in so that the old behavior of the kompiled_target_for fixture is retained,

make sure that cache is never actually updated when --kompiled-targets-dir is passed.

As I see it, tests basically require an interface that takes a Target and returns a Path to the kompiled target (in the actual tests there might be another indirection from spec files to targets, but I'll not consider this for simplicity).

So you just have to ensure that Target -> Path is reproducible between runs, then accommodating both use cases (prekompiled vs on-the-fly) is straightforward.

If the Path does not exist, lock and kompile

Otherwise, return the Path.

For prekompiled mode, you pass in a non-empty directory as base. For on-the-file mode, you pass in an empty temporary directory.

cache, etc. can be dropped, the actual cache is the file system.

Yeah, that sound good, I understand what you mean. However, I'd rather get my incremental change merged quickly and now spend too much time refactoring the test suite. Would that be OK if I let you refactor it as you see fit?

I can live with that, but please open an issue for the refactoring and assign it to me.

Thanks, will do!

This reverts commit 54c5c4a.

…ompile-in-advance

~Needs runtimeverification/evm-semantics#2417 Allows compiling the K definitions needs for proofs in advance, with the hope of reducing measurement noise. In the spirit of #3845, but now for KEVM rather than Kontrol.

geo2a and others added 20 commits May 8, 2024 17:16

Towards in-advance kompilation of definitions in tests

0746d93

Allow a permanent prekompiled directory

0a01455

Run less tests, for debugging purposes

ee39882

Add test_kompile_targets

79bc8c5

Add file lock

1fbf00d

De-dupe targets in a smarter way

0d01474

Don't prekompile definitions for failing tests

b91a09b

Add __eq__ override to Target

9ccd0a8

Use target name as cache key, add cache debug msgs

37b10fd

Actually read cache from disk

870f723

Revert "Run less tests, for debugging purposes"

cb0e941

This reverts commit 5858d0a.

Remove debugging messages

00bb4b9

Correct path stuff

0056a78

Consolidate conftest.py

792b7c1

Add comments

c49ab2a

Add pytest marker for prekompilation

9086efd

Add more comments

5d8f909

Skip prekompiling in the same way as proving

aada391

Remove Target.__eq__, improve comments

4a124e0

Set Version: 1.0.546

b30fd19

geo2a changed the title ~~Georgy/test prove kompile in advance~~ Pre-kompile K definitions and specs for integration tests May 8, 2024

geo2a requested review from tothtamas28, ehildenb and nwatson22 May 8, 2024 15:43

geo2a self-assigned this May 8, 2024

Merge branch 'master' into georgy/test-prove-kompile-in-advance

3701ddc

geo2a force-pushed the georgy/test-prove-kompile-in-advance branch 2 times, most recently from f2359e8 to bc1f3ea Compare May 8, 2024 16:18

Skip kompilation cache test

ef47d11

geo2a force-pushed the georgy/test-prove-kompile-in-advance branch from bc1f3ea to ef47d11 Compare May 8, 2024 16:18

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

5ce032d

geo2a mentioned this pull request May 8, 2024

Enable pre-kompilation of K definitions and specs runtimeverification/haskell-backend#3853

Merged

geo2a added 4 commits May 8, 2024 19:07

Code style

3a9d51f

Add smtlib markers to Word operations

0ab98ac

Merge branch 'master' into georgy/test-prove-kompile-in-advance

75852dc

Revert "Add smtlib markers to Word operations"

6981c85

This reverts commit 0ab98ac.

nwatson22 approved these changes May 8, 2024

View reviewed changes

tothtamas28 reviewed May 9, 2024

View reviewed changes

geo2a added 2 commits May 9, 2024 15:06

Remove redundant parameter

54c5c4a

Revert "Remove redundant parameter"

87b7891

This reverts commit 54c5c4a.

geo2a mentioned this pull request May 9, 2024

Refactor kompilation cache in the intergration tests #2419

Closed

geo2a added the automerge label May 9, 2024

geo2a and others added 2 commits May 10, 2024 08:49

Merge remote-tracking branch 'origin/master' into georgy/test-prove-k…

ed881e7

…ompile-in-advance

Set Version: 1.0.548

19c4b81

rv-jenkins merged commit 1683cd4 into master May 10, 2024

rv-jenkins deleted the georgy/test-prove-kompile-in-advance branch May 10, 2024 08:25

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

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

Uh oh!

geo2a commented May 8, 2024 •

edited

Loading

Uh oh!

tothtamas28 May 9, 2024

Uh oh!

tothtamas28 May 9, 2024

Uh oh!

geo2a May 9, 2024

Uh oh!

tothtamas28 May 9, 2024

Uh oh!

geo2a May 9, 2024

Uh oh!

geo2a May 9, 2024

Uh oh!

tothtamas28 May 9, 2024

Uh oh!

geo2a May 9, 2024

Uh oh!

tothtamas28 May 9, 2024

Uh oh!

geo2a May 9, 2024

Uh oh!

tothtamas28 May 9, 2024

Uh oh!

geo2a May 9, 2024

Uh oh!

Uh oh!

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

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

Uh oh!

Conversation

geo2a commented May 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

geo2a commented May 8, 2024 •

edited

Loading