Skip to content

Enable pre-kompilation of K definitions and specs #3853

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 10, 2024
Merged

Enable pre-kompilation of K definitions and specs #3853

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b0a38d4
Enable pre-kompilation of K definitions and specs
geo2a May 8, 2024
6fce2a3
Merge branch 'master' into georgy/improve-performance-tests-kevm
geo2a May 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 34 additions & 10 deletions scripts/performance-tests-kevm.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,18 +21,31 @@ if [[ $FEATURE_BRANCH_NAME == "master" ]]; then
FEATURE_BRANCH_NAME="feature"
fi

# Create a temporary directory and store its name in a variable.
TEMPD=$(mktemp -d)
# Create a temporary directory (or use the one provided) and store its name in a variable.
KEEP_TEMPD=${KEEP_TEMPD:-''}
FRESH_TEMPD=0
TEMPD=${TEMPD:-''}
if [ -z "$TEMPD" ]; then
FRESH_TEMPD=1
TEMPD=$(mktemp -d)
fi

# 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

feature_shell() {
GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input k-framework/haskell-backend $SCRIPT_DIR/../ --command bash -c "$1"
Expand All @@ -43,7 +56,9 @@ master_shell() {
}

cd $TEMPD
git clone --depth 1 --branch $KEVM_VERSION https://github.com/runtimeverification/evm-semantics.git
if [[ $FRESH_TEMPD -gt 0 ]]; then
git clone --depth 1 --branch $KEVM_VERSION https://github.com/runtimeverification/evm-semantics.git
fi
cd evm-semantics

if [[ $KEVM_VERSION == "master" ]]; then
Expand All @@ -52,7 +67,9 @@ else
KEVM_VERSION="${KEVM_VERSION//\//-}"
fi

git submodule update --init --recursive --depth 1 kevm-pyk/src/kevm_pyk/kproj/plugin
if [[ $FRESH_TEMPD -gt 0 ]]; then
git submodule update --init --recursive --depth 1 kevm-pyk/src/kevm_pyk/kproj/plugin
fi

BUG_REPORT=''
POSITIONAL_ARGS=()
Expand All @@ -77,18 +94,25 @@ done

set -- "${POSITIONAL_ARGS[@]}" # restore positional parameters

feature_shell "make poetry && poetry run -C kevm-pyk -- kdist --verbose build evm-semantics.plugin evm-semantics.haskell --jobs 4"
# kompile evm-semantics or skip kompilation if using an existing TEMPD
if [[ $FRESH_TEMPD -gt 0 ]]; then
feature_shell "make poetry && poetry run -C kevm-pyk -- kdist --verbose build evm-semantics.plugin evm-semantics.haskell --jobs 4"
fi

# kompile all verification K definitions and specs
PREKOMPILED_DIR=$TEMPD/prekompiled
mkdir -p $PREKOMPILED_DIR
feature_shell "cd kevm-pyk && poetry run pytest src/tests/integration/test_prove.py::test_kompile_targets -vv --maxfail=0 --kompiled-targets-dir $PREKOMPILED_DIR"

mkdir -p $SCRIPT_DIR/logs

feature_shell "make test-prove-pyk PYTEST_PARALLEL=$PYTEST_PARALLEL PYTEST_ARGS='--maxfail=0 --timeout 7200 -vv --use-booster $BUG_REPORT' | tee $SCRIPT_DIR/logs/kevm-$KEVM_VERSION-$FEATURE_BRANCH_NAME.log"
feature_shell "make test-prove-pyk PYTEST_PARALLEL=$PYTEST_PARALLEL PYTEST_ARGS='--maxfail=0 --timeout 7200 -vv --use-booster $BUG_REPORT --kompiled-targets-dir $PREKOMPILED_DIR' | tee $SCRIPT_DIR/logs/kevm-$KEVM_VERSION-$FEATURE_BRANCH_NAME.log"
killall kore-rpc-booster || echo "No zombie processes found"


if [ -z "$BUG_REPORT" ]; then
if [ ! -e "$SCRIPT_DIR/logs/kevm-$KEVM_VERSION-master-$MASTER_COMMIT_SHORT.log" ]; then
master_shell "make test-prove-pyk PYTEST_PARALLEL=$PYTEST_PARALLEL PYTEST_ARGS='--maxfail=0 --timeout 7200 -vv --use-booster' | tee $SCRIPT_DIR/logs/kevm-$KEVM_VERSION-master-$MASTER_COMMIT_SHORT.log"
master_shell "make test-prove-pyk PYTEST_PARALLEL=$PYTEST_PARALLEL PYTEST_ARGS='--maxfail=0 --timeout 7200 -vv --use-booster --kompiled-targets-dir $PREKOMPILED_DIR' | tee $SCRIPT_DIR/logs/kevm-$KEVM_VERSION-master-$MASTER_COMMIT_SHORT.log"
killall kore-rpc-booster || echo "No zombie processes found"
fi

Expand Down
Loading