runtimeverification / evm-semantics

K Semantics of the Ethereum Virtual Machine (EVM)
BSD 3-Clause "New" or "Revised" License
503 stars 135 forks source link

Running VM tests on Haskell backend #1291

Open ehildenb opened 1 year ago

ehildenb commented 1 year ago

Apply this patch:

diff --git a/edsl.md b/edsl.md
index 125531a83..1ad3ce74e 100644
--- a/edsl.md
+++ b/edsl.md
@@ -12,6 +12,7 @@ requires "hashed-locations.md"
 requires "abi.md"
 requires "infinite-gas.md"
 requires "optimizations.md"
+requires "driver.md"

 module EDSL
     imports BUF
@@ -20,6 +21,7 @@ module EDSL
     imports EVM-OPTIMIZATIONS
     imports INFINITE-GAS
     imports BIN-RUNTIME
+    imports ETHEREUM-SIMULATION
 endmodule

 module BIN-RUNTIME

Then you can do:

make build-kevm
make build-haskell
make test-vm -j6 -k TEST_CONCRETE_BACKEND=haskell TEST_OPTIONS=--bug-report

And it will produce a bunch of bug-reports for the VM tests on Haskell backend for profiling.

ehildenb commented 1 year ago

If you are before #1315, you must additionally make this change:

diff --git a/kevm b/kevm
index 9d0a2caf2..4b05a79f2 100755
--- a/kevm
+++ b/kevm
@@ -260,7 +260,7 @@ run_interpret() {
                  ;;

         haskell) run_kast kore > "$kast"
-                 kore_exec_args=(--module ETHEREUM-SIMULATION --smt none)
+                 kore_exec_args=(--module EDSL --smt none)
                  bug_report_name="kevm-bug-$(basename "${run_file%.json}")"
                  ! ${bug_report} || kore_exec_args+=(--bug-report ${bug_report_name})
                  execute kore-exec "$backend_dir/definition.kore" --pattern "${kast}" --output "${output}" "${kore_exec_args[@]}" || exit_status="$?"