Reuse kompiled contracts.k and foundry.k in Kontrol performance test (#3845)

This PR attempts to reduce the influence of the K compiler processes on
the Kontrol performance test. To achieve that, we compile everything
in-advance, ensuring that there will be no calls to `kompile` when
running the actual proof test:

- run the single `test_foundy_kompile` test, which is essentially just a
wrapper for the `foundry` pytest
[fixture](https://github.com/runtimeverification/kontrol/blob/2fba281b0a73d76c1dba37f74220051901d04606/src/tests/integration/conftest.py#L53)
that generates and compiles the `contracts.k` and `foundry.k` files.
This produces the `foundry/out/kompiled` directory
- when running the actual proof tests, pass the generated `foundry`
directory to them explicitly. This makes sure that the pytest fixture
will not be forced to recompile stuff in every `pytest-xdist` worker.
- Re-using the `foundry` directory has a side-effect of also reusing the
`foundry/out/proofs` directory. To make sure that we actually run the
proofs in `master_shell`, and not re-use the ones produced by
`feature_shell`, we delete them between the steps.

Some things I've noticed that may be worth accounting for, but not in
this PR:
- the `server`
[fixture](https://github.com/runtimeverification/kontrol/blob/7f45d5672a59f094e2d067e41923e037544b86f1/src/tests/integration/conftest.py#L35)
is module-scoped. That means that all tests in a certain test module
will reuse the same server instance, individually in each test worker.
- the corollary of the above is that the proofs that are run later will
use a more "tired" server, since the server state will bloat due to a
bunch of duplicate (and likely empty) modules. It is not clear if this
is a performance issue, but we have certainly not considered it earlier.
- another thing is that the decision on which test to skip is taken
dynamically at the start of the test, and the tests, even if skipped,
need the fixtures to be ready for them. In most cases, however, the
server connection will be reused by other tests in the same module.

---------

Co-authored-by: rv-jenkins <[email protected]>

Author: geo2a

scripts/performance-tests-kontrol.sh

@@ -23,16 +23,24 @@ fi
 
 # Create a temporary directory and store its name in a variable.
 TEMPD=$(mktemp -d)
+KEEP_TEMPD=${KEEP_TEMPD:-''}
 
 # Exit if the temp directory wasn't created successfully.
 if [ ! -e "$TEMPD" ]; then
     >&2 echo "Failed to create temp directory"
     exit 1
 fi
 
-# Make sure the temp directory gets removed and kore-rpc-booster gets killed on script exit.
-trap "exit 1"           HUP INT PIPE QUIT TERM
-trap 'rm -rf "$TEMPD" && killall kore-rpc-booster || echo "no zombie processes found"'  EXIT
+clean_up () {
+    if [ -z "$KEEP_TEMPD" ]; then
+        rm -rf "$TEMPD"
+    fi
+    killall kore-rpc-booster || echo "no zombie processes found"
+}
+
+# Make sure the temp directory gets removed (unless KEEP_TEMPD is set) and kore-rpc-booster gets killed on script exit.
+trap "exit 1"  HUP INT PIPE QUIT TERM
+trap clean_up  EXIT
 
 cd $TEMPD
 git clone --depth 1 --branch $KONTROL_VERSION https://github.com/runtimeverification/kontrol.git
@@ -93,16 +101,27 @@ master_shell() {
   GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/haskell-backend github:runtimeverification/haskell-backend/$MASTER_COMMIT --command bash -c "$1"
 }
 
+# kompile Kontrol's K dependencies
 feature_shell "poetry install && poetry run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.foundry --jobs 4"
 
+# kompile the test contracts, to be reused in feature_shell and master_shell. Copy the result from pytest's temp directory
+PYTEST_TEMP_DIR=$TEMPD/pytest-temp-dir
+mkdir -p $PYTEST_TEMP_DIR
+FOUNDRY_DIR=$TEMPD/foundry
+mkdir -p $FOUNDRY_DIR
+feature_shell "make test-integration TEST_ARGS='--basetemp=$PYTEST_TEMP_DIR -n0 --dist=no -k test_foundry_kompile'"
+cp -r $PYTEST_TEMP_DIR/foundry/* $FOUNDRY_DIR
+
 mkdir -p $SCRIPT_DIR/logs
 
-feature_shell "make test-integration TEST_ARGS='--maxfail=0 --numprocesses=$PYTEST_PARALLEL -vv $BUG_REPORT' | tee $SCRIPT_DIR/logs/kontrol-$KONTROL_VERSION-$FEATURE_BRANCH_NAME.log"
+feature_shell "make test-integration TEST_ARGS='--foundry-root $FOUNDRY_DIR --maxfail=0 --numprocesses=$PYTEST_PARALLEL -vv $BUG_REPORT' | tee $SCRIPT_DIR/logs/kontrol-$KONTROL_VERSION-$FEATURE_BRANCH_NAME.log"
 killall kore-rpc-booster || echo "no zombie processes found"
 
 if [ -z "$BUG_REPORT" ]; then
 if [ ! -e "$SCRIPT_DIR/logs/kontrol-$KONTROL_VERSION-master-$MASTER_COMMIT_SHORT.log" ]; then
-  master_shell "make test-integration TEST_ARGS='--maxfail=0 --numprocesses=$PYTEST_PARALLEL -vv' | tee $SCRIPT_DIR/logs/kontrol-$KONTROL_VERSION-master-$MASTER_COMMIT_SHORT.log"
+  # remove proofs so that they are not reused by the master shell call
+  rm -r $FOUNDRY_DIR/out/proofs
+  master_shell "make test-integration TEST_ARGS='--foundry-root $FOUNDRY_DIR --maxfail=0 --numprocesses=$PYTEST_PARALLEL -vv' | tee $SCRIPT_DIR/logs/kontrol-$KONTROL_VERSION-master-$MASTER_COMMIT_SHORT.log"
   killall kore-rpc-booster || echo "no zombie processes found"
 fi