Update generate-regression-tests.sh work with modern evm-semantics (#…

…3687)

Fixes #3686

This PR does the following
- Updates `generate-regression-tests.sh` to work with modern versions of
evm-semantics which no longer use a Makefile-based build system.
- Fixes all issues reported by `shellcheck`.
- Runs the new script and updates all the `regression-evm` tests.

---

###### Review checklist

The author performs the actions on the checklist. The reviewer evaluates
the work and checks the boxes as they are completed.

- [ ] **Summary.** Write a summary of the changes. Explain what you did
to fix the issue, and why you did it. Present the changes in a logical
order. Instead of writing a summary in the pull request, you may push a
clean Git history.
- [ ] **Documentation.** Write documentation for new functions. Update
documentation for functions that changed, or complete documentation
where it is missing.
- [ ] **Tests.** Write unit tests for every change. Write the unit tests
that were missing before the changes. Include any examples from the
reported issue as integration tests.
- [ ] **Clean up.** The changes are already clean. Clean up anything
near the changes that you noticed while working. This does not mean only
spatially near the changes, but logically near: any code that interacts
with the changes!

---------

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

scripts/generate-regression-tests.sh

@@ -45,14 +45,14 @@ err() {
 
 # working directory
 if [ -z "$KORE" ]; then
-    KORE=$(cd $(dirname $0)/.. && pwd)
+    KORE=$(cd "$(dirname "$0")"/.. && pwd)
     log "No working directory, defaulting to $KORE" warn
 else
-    KORE=$(realpath $KORE)
+    KORE=$(realpath "$KORE")
     [ -d "$KORE" ] || err "$KORE: no such directory"
 fi
 
-pushd $KORE
+pushd "$KORE"
 trap popd EXIT
 
 case $(uname) in
@@ -72,136 +72,155 @@ which git > /dev/null || err "git not available"
 if [ -z "${EVM_SEMANTICS}" ]; then
     log "No evm-semantics directory provided, using $KORE/evm-semantics" info
     EVM_SEMANTICS=$KORE/evm-semantics
-    git clone [email protected]:runtimeverification/evm-semantics.git $EVM_SEMANTICS || \
-        [ -f "${EVM_SEMANTICS}/include/kframework/evm.md" ] || \
+    git clone [email protected]:runtimeverification/evm-semantics.git "$EVM_SEMANTICS" || \
+        [ -f "${EVM_SEMANTICS}/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md" ] || \
         err "Unable to use $KORE/evm-semantics directory"
-    (cd $EVM_SEMANTICS && git submodule update --init --recursive)
 else
-    EVM_SEMANTICS=$(realpath ${EVM_SEMANTICS})
+    EVM_SEMANTICS=$(realpath "${EVM_SEMANTICS}")
     log "Using directory ${EVM_SEMANTICS} for evm-semantics" info
-    [ -f "$EVM_SEMANTICS/include/kframework/evm.md" ] || \
+    [ -f "$EVM_SEMANTICS/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md" ] || \
         err "Provided evm-semantics directory '${EVM_SEMANTICS}' appears damaged"
 fi
 
 # determine K version to use from $KORE/deps/k, unless provided
 # deps/k_release contains a version number, the tag has a prefix 'v'
 if [ -z "${K_VERSION}" ]; then
-    [ -f $KORE/deps/k_release ] && K_VERSION=v$(cat $KORE/deps/k_release)
+    [ -f "$KORE"/deps/k_release ] && K_VERSION=v$(cat "$KORE"/deps/k_release)
     log "K version set to ${K_VERSION}"
 fi
 
 # build evm-semantics
 log "Checking out and building ${EVM_VERSION:-latest master} in ${EVM_SEMANTICS}"
-cd ${EVM_SEMANTICS}
+cd "${EVM_SEMANTICS}"
 git fetch
-git checkout ${EVM_VERSION:-master}
-git pull
+git checkout "${EVM_VERSION:-master}"
 git submodule update --init --recursive
-log "Manually setting K dependency to ${K_VERSION}"
 
-log "Cleaning ${EVM_SEMANTICS}"
-make clean
+log "Checking out and building K ${K_VERSION} in ${EVM_SEMANTICS}/deps/k"
 # if we are under a nix develop shell (NIX variable set), don't build K
 if [ -z "$NIX" ]; then
-    (cd deps/k && git checkout ${K_VERSION} && git submodule update --init --recursive)
-    make deps
-    export PATH=$(pwd)/.build/usr/lib/kevm/kframework/bin:$PATH
+    cd deps
+    if [ ! -d k ]; then
+        git clone [email protected]:runtimeverification/k.git
+    fi
+    cd k
+    git fetch
+    git checkout "$K_VERSION"
+    git submodule update --init --recursive
+    mvn package -DskipTests || err "Unable to build K ${K_VERSION}"
+    PATH=$(pwd)/k-distribution/target/release/k/bin:$PATH
+    export PATH
     which kore-exec
+    cd "${EVM_SEMANTICS}"
 else
     log "Testing nix-provided K (kompile --version)"
-    kompile --version && log "(^^^ nix-provided K ^^^)" || err "K unavailable but NIX=$NIX"
+    kompile --version || err "K unavailable but NIX=$NIX"
 fi
+
 log "Building evm-semantics with dependencies"
-make plugin-deps poetry kevm-pyk
-export PATH=$(pwd)/.build/usr/bin:$PATH
-make build-kevm build-haskell
+make poetry
+poetry -C kevm-pyk run kevm-dist clean
+poetry -C kevm-pyk run kevm-dist build plugin
+poetry -C kevm-pyk run kevm-dist build -j"$(nproc)"
 
 kollect() {
     local name="$1"
 
-    local archive=kevm-bug-$name.tar.gz
     local script=test-$name.sh
     local def=test-$name-definition.kore
     local spec=test-$name-spec.kore
     local tmp=$name-tmp
 
-    cd ${EVM_SEMANTICS}
+    pushd "${EVM_SEMANTICS}"/"$name"
 
-    mkdir $tmp
-    mv $archive $tmp
-    cd $tmp
-    tar -xf $archive
+    mkdir "$tmp"
+    cp kevm-bug-*.tar.gz "$tmp"
+    cd "$tmp"
+    tar -xf kevm-bug-*.tar.gz
     rm ./!(kore-exec.sh|spec.kore|vdefinition.kore)
-    mv kore-exec.sh $script
-    mv vdefinition.kore $def
-    mv spec.kore $spec
+    mv kore-exec.sh "$script"
+    mv vdefinition.kore "$def"
+    mv spec.kore "$spec"
 
     $sed -i \
          -e "s,/nix/store/[a-z0-9]*-k-[^/]*maven/include/kframework/,evm-semantics/,g" \
-         -e "s,${EVM_SEMANTICS}/.build/usr/lib/kevm/kframework/include/kframework/,evm-semantics/,g" \
-         -e "s,${EVM_SEMANTICS}/.build/usr/lib/kevm/include/kframework/,evm-semantics/,g" \
-         -e "s,${EVM_SEMANTICS}/,evm-semantics/,g" \
-         *.kore
+         -e "s,${EVM_SEMANTICS}/deps/k/k-distribution/target/release/k/include/kframework/,evm-semantics/,g" \
+         -e "s,${EVM_SEMANTICS}/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/,evm-semantics/,g" \
+         -e "s,${EVM_SEMANTICS}/kevm-pyk/src/kevm_pyk/kproj/plugin/plugin/,evm-semantics/plugin/,g" \
+         -e "s,${EVM_SEMANTICS}/tests,evm-semantics/tests,g" \
+         ./*.kore "$script"
     $sed -i -e "s/result.kore/$script.out/g" \
-        -e "s/vdefinition.kore/$def/g" \
-        -e "s/spec.kore/$spec/g" \
-        $script
+         -e "s/vdefinition.kore/$def/g" \
+         -e "s/spec.kore/$spec/g" \
+         -e "/^\s*--log \\\/,+1d;/^\s*--log\s/d" \
+         "$script"
 
     cd ..
-    mv $tmp/* .
-    rmdir $tmp
+    mv "$tmp"/* "${EVM_SEMANTICS}"
+    rmdir "$tmp"
+    popd
 }
 
 # test paths will be prefixed with tests/specs, and suffixed with -spec.k.prove
-ALL_TESTS="\
-        examples/sum-to-n \
-        functional/lemmas \
-        benchmarks/storagevar03 \
-        erc20/ds/totalSupply \
-        mcd/flipper-addu48u48-fail-rough \
-        mcd/dsvalue-peek-pass-rough \
-        benchmarks/functional \
-        "
+# conecutive entries from a pair indicating the test name followed by its main module
+ALL_TESTS=(
+        "examples/sum-to-n" "VERIFICATION"
+        "functional/lemmas" "VERIFICATION"
+        "benchmarks/storagevar03" "VERIFICATION"
+        "erc20/ds/totalSupply" "VERIFICATION"
+        "mcd/flipper-addu48u48-fail-rough" "VERIFICATION"
+        "mcd/dsvalue-peek-pass-rough" "VERIFICATION"
+        "benchmarks/functional" "FUNCTIONAL-SPEC-SYNTAX"
+)
 
 generate-evm() {
-    TARGETS=$@
-
-    if [ -z "$TARGETS" ]; then
-        TARGETS=$ALL_TESTS
-    fi
+    TARGETS=( "$@" )
 
-    log "Generating test data for tests $TARGETS"
+    if [ ${#TARGETS[@]} -eq 0 ]; then
+        TARGETS=( "${ALL_TESTS[@]}" )
+    fi 
 
-    cd ${EVM_SEMANTICS}
+    log "Generating test data for tests ${TARGETS[*]}"
 
     # check that test files actually exist before running anything
-    for TEST in $TARGETS; do
+    for (( idx=0 ; idx<${#TARGETS[@]} ; idx+=2 )); do
+        TEST=${TARGETS[idx]}
         log "Checking tests/specs/$TEST-spec.k"
-        [ -f tests/specs/$TEST-spec.k ] || err "$TEST's K file does not exist"
+        [ -f "${EVM_SEMANTICS}"/tests/specs/"$TEST"-spec.k ] || err "$TEST's K file does not exist"
     done
 
-    for TEST in $TARGETS; do
+    for (( idx=0 ; idx<${#TARGETS[@]} ; idx+=2 )); do
+        TEST=${TARGETS[idx]}
+        MOD=${TARGETS[idx+1]}
         log "Running $TEST"
-        make tests/specs/$TEST-spec.k.prove KPROVE_OPTS=--bug-report CHECK=true
+        local testabs=${EVM_SEMANTICS}/tests/specs/$TEST-spec.k
+        local testdir
+        testdir=${EVM_SEMANTICS}/$(basename "$TEST")
+        mkdir "$testdir"
+        pushd "$testdir"
+        poetry -C "${EVM_SEMANTICS}"/kevm-pyk run kevm-pyk kompile "$testabs" --target haskell --syntax-module "$MOD" --main-module "$MOD" --output .
+        poetry -C "${EVM_SEMANTICS}"/kevm-pyk run kevm-pyk prove-legacy "$testabs" --definition . --bug-report-legacy
         log "Collecting data for $TEST"
-        kollect $(basename $TEST)
+        kollect "$(basename "$TEST")"
+        popd
+        rm -rf "$testdir"
     done
 }
 
 replace-tests() {
     local testdir=$KORE/$1
-    local tests=$2/test-*
+    local tests=("$2"/test-*)
 
-    if [ ! -d $testdir ]
+    if [ ! -d "$testdir" ]
     then
-        mkdir $testdir
-        echo "include \$(CURDIR)/../include.mk" > $testdir/Makefile
-        echo "" >> $testdir/Makefile
-        echo "test-%.sh.out: \$(TEST_DIR)/test-%-*" >> $testdir/Makefile
+        mkdir "$testdir"
+        echo "include \$(CURDIR)/../include.mk" > "$testdir"/Makefile
+        echo "" >> "$testdir"/Makefile
+        echo "test-%.sh.out: \$(TEST_DIR)/test-%-*" >> "$testdir"/Makefile
     fi
-    mv $tests $testdir
+    mv "${tests[@]}" "$testdir"
 }
 
-generate-evm $@
-replace-tests "test/regression-evm" ${EVM_SEMANTICS}
-rm -rf $KORE/evm-semantics
+generate-evm "$@"
+replace-tests "test/regression-evm" "${EVM_SEMANTICS}"
+rm -rf "$KORE"/evm-semantics