Skip to content

Commit 652576c

Browse files
ehildenbrv-jenkins
ehildenb
authored and
rv-jenkins
committed
Add ./kevm interpret for haskell|java backends (#606)
* kevm: add interpret command for Haskell backend * kevm: add interpret java command * tests/slow.{haskell,java}: common slow tests * tests/slow: add slow tests on java * tests/slow.*: add tests slow on haskell * kevm: no --debug option for java/haskell backends * kevm: disable smt solver for interpret haskell * tests/slow.{haskell,java}: update slow files * tests/{slow,failing}.{haskell,java}: add lists of slow/failing tests for symbolic backends
1 parent b8817dd commit 652576c

File tree

5 files changed

+96
-27
lines changed

5 files changed

+96
-27
lines changed

‎kevm‎

Lines changed: 47 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -175,32 +175,51 @@ run_interpret() {
175175
debugger=
176176
output_format='kore'
177177
case "$backend" in
178-
ocaml) run_kast kast > "$kast"
179-
output_format='kast'
180-
if $debug; then debugger=ocamldebug; fi
181-
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" \
182-
-c PGM "$kast" textfile \
183-
-c SCHEDULE "$cSCHEDULE" text \
184-
-c MODE "$cMODE" text \
185-
--initializer 'initKevmCell' \
186-
--output-file "$output" "$@" \
187-
|| exit_status="$?"
188-
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
189-
k-bin-to-text "$output" "$output_text"
190-
cat "$output_text"
191-
fi
192-
exit "$exit_status"
193-
;;
194-
195-
llvm) run_kast kore > "$kast"
196-
if $debug; then debugger="gdb --args"; fi
197-
$debugger "$interpreter" "$kast" -1 "$output_text" "$@" \
198-
|| exit_status="$?"
199-
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
200-
cat "$output_text" | "$0" kast --backend "$backend" - pretty --input "$output_format" --sort GeneratedTopCell
201-
fi
202-
exit "$exit_status"
203-
;;
178+
ocaml) run_kast kast > "$kast"
179+
output_format='kast'
180+
if $debug; then debugger=ocamldebug; fi
181+
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" \
182+
-c PGM "$kast" textfile \
183+
-c SCHEDULE "$cSCHEDULE" text \
184+
-c MODE "$cMODE" text \
185+
--initializer 'initKevmCell' \
186+
--output-file "$output" "$@" \
187+
|| exit_status="$?"
188+
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
189+
k-bin-to-text "$output" "$output_text"
190+
cat "$output_text"
191+
fi
192+
exit "$exit_status"
193+
;;
194+
195+
java) run_kast kast > "$kast"
196+
output_format='kast'
197+
run_file="$kast"
198+
run_krun --parser 'cat' --output kast > "$output" || exit_status="$?"
199+
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
200+
cat "$output" | "$0" kast --backend "$backend" - pretty --input "$output_format"
201+
fi
202+
exit "$exit_status"
203+
;;
204+
205+
llvm) run_kast kore > "$kast"
206+
if $debug; then debugger="gdb --args"; fi
207+
$debugger "$interpreter" "$kast" -1 "$output" "$@" \
208+
|| exit_status="$?"
209+
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
210+
cat "$output" | "$0" kast --backend "$backend" - pretty --input "$output_format" --sort GeneratedTopCell
211+
fi
212+
exit "$exit_status"
213+
;;
214+
215+
haskell) run_kast kore > "$kast"
216+
kore-exec "$backend_dir/driver-kompiled/definition.kore" --pattern "$kast" --module ETHEREUM-SIMULATION --smt none --output "$output" \
217+
|| exit_status="$?"
218+
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
219+
cat "$output" | "$0" kast --backend "$backend" - pretty --input "$output_format" --sort GeneratedTopCell
220+
fi
221+
exit "$exit_status"
222+
;;
204223

205224
*) fatal "Bad backend for interpreter: '$backend'"
206225
;;
@@ -216,6 +235,7 @@ if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
216235
echo "
217236
usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*
218237
$0 interpret [--backend (ocaml|llvm)] [--debug|--no-unparse] <pgm> <interpreter arg>*
238+
$0 interpret [--backend (haskell|java)] [--no-unparse] <pgm>
219239
$0 kast [--backend (ocaml|java|llvm|haskell|web3)] <pgm> <output format> <K arg>*
220240
$0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
221241
$0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
@@ -309,7 +329,7 @@ case "$run_command-$backend" in
309329
# Running
310330
run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;;
311331
kast-@(ocaml|java|llvm|haskell|web3) ) run_kast "$@" ;;
312-
interpret-@(ocaml|llvm) ) run_interpret "$@" ;;
332+
interpret-@(ocaml|llvm|haskell|java) ) run_interpret "$@" ;;
313333
prove-@(java|haskell) ) run_prove "$@" ;;
314334
search-@(java|haskell) ) run_search "$@" ;;
315335
web3-@(llvm) ) run_web3 "$@" ;;

‎tests/failing.haskell‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
tests/ethereum-tests/VMTests/vmSystemOperations/suicide0.json
2+
tests/ethereum-tests/VMTests/vmSystemOperations/suicideSendEtherToMe.json

‎tests/failing.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/calldatacopy_DataIndexTooHigh2.json
2+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/calldatacopy_DataIndexTooHigh2_return.json
3+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/calldatacopy_DataIndexTooHigh.json
4+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/calldatacopy_DataIndexTooHigh_return.json
5+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/calldataload_BigOffset.json
6+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/calldataloadSizeTooHigh.json
7+
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/codecopy_DataIndexTooHigh.json

‎tests/slow.haskell‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
tests/ethereum-tests/VMTests/vmPerformance/loop-mulmod-2M.json
2+
tests/ethereum-tests/VMTests/vmPerformance/loop-mul.json
3+
tests/ethereum-tests/VMTests/vmPerformance/loop-divadd-10M.json
4+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-16b-100k.json
5+
tests/ethereum-tests/VMTests/vmPerformance/ackermann33.json
6+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-4b-100k.json
7+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/JDfromStorageDynamicJump0_foreverOutOfGas.json
8+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-2b-100k.json
9+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/BlockNumberDynamicJump0_foreverOutOfGas.json
10+
tests/ethereum-tests/VMTests/vmPerformance/ackermann32.json
11+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-8b-100k.json
12+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-1b-1M.json
13+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/loop_stacklimit_1021.json
14+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/DynamicJump0_foreverOutOfGas.json
15+
tests/ethereum-tests/VMTests/vmPerformance/fibonacci10.json
16+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/loop_stacklimit_1020.json
17+
tests/ethereum-tests/VMTests/vmPerformance/ackermann31.json
18+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-nop-1M.json
19+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-32b-100k.json
20+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/for_loop1.json
21+
tests/ethereum-tests/VMTests/vmPerformance/fibonacci16.json
22+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/jump0_foreverOutOfGas.json
23+
tests/ethereum-tests/VMTests/vmIOandFlowOperations/for_loop2.json
24+
tests/ethereum-tests/VMTests/vmPerformance/loop-divadd-unr100-10M.json
25+
tests/ethereum-tests/VMTests/vmPerformance/loop-add-10M.json
26+
tests/ethereum-tests/VMTests/vmPerformance/manyFunctions100.json

‎tests/slow.java‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
tests/ethereum-tests/VMTests/vmPerformance/ackermann33.json
2+
tests/ethereum-tests/VMTests/vmPerformance/fibonacci16.json
3+
tests/ethereum-tests/VMTests/vmPerformance/loop-add-10M.json
4+
tests/ethereum-tests/VMTests/vmPerformance/loop-divadd-10M.json
5+
tests/ethereum-tests/VMTests/vmPerformance/loop-divadd-unr100-10M.json
6+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-16b-100k.json
7+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-1b-1M.json
8+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-2b-100k.json
9+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-32b-100k.json
10+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-4b-100k.json
11+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-8b-100k.json
12+
tests/ethereum-tests/VMTests/vmPerformance/loop-exp-nop-1M.json
13+
tests/ethereum-tests/VMTests/vmPerformance/loop-mul.json
14+
tests/ethereum-tests/VMTests/vmPerformance/loop-mulmod-2M.json

0 commit comments

Comments
 (0)