Use Makefile for generating regression tests (#2580)

* Use Makefile for evm proof

* Add kollect-file, use upcoming evm Makefile changes

* Clean-up evm part of script

* Use Makefile for wasm tests

* CLean-up

* Review: replace with shift 2

Author: ana-pantilie

scripts/generate-regression-tests.sh

@@ -7,7 +7,17 @@ kollect() {
     local name="$1"
     shift
     echo '#!/bin/sh' > "$name.sh"
-    "$@" --save-temps --dry-run | xargs $KORE/scripts/kollect.sh "$name" >> "$name.sh"
+    "$@" | xargs $KORE/scripts/kollect.sh "$name" >> "$name.sh"
+    chmod +x "$name.sh"
+}
+
+kollect-file() {
+    local name="$1"
+    local path="$2"
+    shift 2
+    echo '#!/bin/sh' > "$name.sh"
+    "$@"
+    cat $path | xargs $KORE/scripts/kollect.sh "$name" >> "$name.sh"
     chmod +x "$name.sh"
 }
 
@@ -32,63 +42,56 @@ build-wasm() {
 generate-evm() {
     cd $KORE/evm-semantics
 
-    kollect test-pop1 \
-        kevm run --backend haskell \
-            --mode VMTESTS --schedule DEFAULT \
-            tests/ethereum-tests/VMTests/vmIOandFlowOperations/pop1.json
-
-    kollect test-add0 env \
-        kevm run --backend haskell \
-            --mode VMTESTS --schedule DEFAULT \
-            tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json \
-
-    kollect test-sumTo10 \
-        kevm run --backend haskell \
-            --mode VMTESTS --schedule DEFAULT \
-            tests/interactive/sumTo10.evm \
+    export \
+        TEST_CONCRETE_BACKEND=haskell \
+        TEST_SYMBOLIC_BACKEND=haskell \
+        TEST_OPTIONS="--dry-run --save-temps" \
+        CHECK=true \
+        KEEP_OUTPUTS=true
+
+    local testpop1=tests/ethereum-tests/VMTests/vmIOandFlowOperations/pop1.json
+    local testadd0=tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json
+    local testsumTo10=tests/interactive/sumTo10.evm
+
+    kollect-file test-pop1 "$testpop1.haskell-out" \
+        make "$testpop1.run-interactive" -e
+    
+    kollect-file test-add0 "$testadd0.haskell-out" \
+        make "$testadd0.run-interactive" -e
+    
+    kollect-file test-sumTo10 $testsumTo10.haskell-out \
+        make "$testsumTo10.run-interactive" -e
 
     for search in \
         branching-no-invalid straight-line-no-invalid \
         branching-invalid straight-line
     do
-        kollect "test-$search" \
-            kevm search --backend haskell \
-                "tests/interactive/search/$search.evm" \
-                "<statusCode> EVMC_INVALID_INSTRUCTION </statusCode>"
+        kollect-file "test-$search" "tests/interactive/search/$search.evm.search-out" \
+            make "tests/interactive/search/$search.evm.search" -e
     done
 
     kollect test-sum-to-n \
-        kevm prove --backend haskell \
-            tests/specs/examples/sum-to-n-spec.k \
-            VERIFICATION --format-failures
-
+        make tests/specs/examples/sum-to-n-spec.k.prove -e
+    
     $KORE/scripts/trim-source-paths.sh *.kore
 }
 
 generate-wasm() {
     cd $KORE/wasm-semantics
 
+    export KPROVE_OPTS="--dry-run --save-temps"
+
     for spec in \
         simple-arithmetic \
         locals \
-        loops
+        loops \
+        memory \
+        wrc20
     do
         kollect "test-$spec" \
-            ./kwasm prove --backend haskell \
-                tests/proofs/"$spec"-spec.k \
-                KWASM-LEMMAS
+            make tests/proofs/"$spec"-spec.k.prove -e
     done
 
-    kollect "test-memory" \
-        ./kwasm prove --backend haskell \
-            tests/proofs/memory-spec.k \
-            KWASM-LEMMAS \
-            --concrete-rules WASM-DATA.wrap-Positive,WASM-DATA.setRange-Positive,WASM-DATA.getRange-Positive
-
-    kollect "test-wrc20" \
-        ./kwasm prove --backend haskell tests/proofs/wrc20-spec.k WRC20-LEMMAS --format-failures \
-        --concrete-rules WASM-DATA.wrap-Positive,WASM-DATA.setRange-Positive,WASM-DATA.getRange-Positive,WASM-DATA.get-Existing,WASM-DATA.set-Extend
-
     $KORE/scripts/trim-source-paths.sh *.kore
 }