#!/usr/bin/env bash

set -euo pipefail

shopt -s extglob

kevm_dir="${KEVM_DIR:-.}"

build_dir="$kevm_dir/.build"

defn_dir="${KEVM_DEFN_DIR:-$build_dir/defn}"

lib_dir="$build_dir/local/lib"

k_release_dir="${K_RELEASE:-$kevm_dir/deps/k/k-distribution/target/release/k}"

export PATH="$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH"

export LD_LIBRARY_PATH="$k_release_dir/lib/native/linux64:$lib_dir:${LD_LIBRARY_PATH:-}"

test_logs="$build_dir/logs"

mkdir -p "$test_logs"

test_log="$test_logs/tests.log"

KLAB_OUT="${KLAB_OUT:-$build_dir/klab}"

KLAB_NODE_STACK_SIZE="${KLAB_NODE_STACK_SIZE:-30000}"

export KLAB_OUT

# Utilities

# ---------

notif() { echo "== $@" >&2 ; }

fatal() { echo "[FATAL] $@" ; exit 1 ; }

pretty_diff() {

git --no-pager diff --no-index --ignore-all-space "$@"

}

# Runners

# -------

# User Commands

run_krun() {

export K_OPTS=-Xss500m

case "$backend" in

ocaml) args=(--interpret) ;;

*) args=() ;;

esac

krun --directory "$backend_dir" -cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' -cMODE="$cMODE" -pMODE='printf %s' "$run_file" "${args[@]-}" "$@"

}

run_kast() {

local output_mode

output_mode="${1:-kast}" ; shift

case "$run_file-$output_mode" in

*.json-@(kast|kore)) "$kevm_dir/$output_mode-json.py" "$run_file" "$cSCHEDULE" "$cMODE" ;;

*) kast --directory "$backend_dir" "$run_file" --output "$output_mode" "$@" ;;

esac

}

run_prove() {

export K_OPTS=-Xmx8G

# If --smt-prelude is not set and evm.smt2 is present in $run_dir, use it.

smt_prelude_set=

for i in "$@" ; do [[ $i == "--smt-prelude" ]] && smt_prelude_set=true && break ; done

run_dir="$(dirname "$run_file")"

smt_file="$run_dir/evm.smt2"

smt_args=()

if [[ -z $smt_prelude_set ]] && [[ -f "$smt_file" ]]; then

smt_args=(--smt-prelude "$smt_file")

fi

if $debug; then

set -x

fi

kprove --directory "$backend_dir" "${smt_args[@]-}" "$run_file" "$@"

}

run_search() {

local search_pattern

search_pattern="$1" ; shift

export K_OPTS=-Xmx8G

run_krun --search --pattern "$search_pattern" "$@"

}

run_klab() {

local run_mode klab_log

run_mode="$1" ; shift

klab_log="$(basename "${run_file%-spec.k}")"

"$0" "$run_mode" --backend java "$run_file" \

--state-log --state-log-path "$KLAB_OUT/data" --state-log-id "$klab_log" \

--state-log-events OPEN,EXECINIT,SEARCHINIT,REACHINIT,REACHTARGET,REACHPROVED,NODE,RULE,SRULE,RULEATTEMPT,IMPLICATION,Z3QUERY,Z3RESULT,CLOSE \

--output-flatten "_Map_ #And" \

--output-tokenize "_;__EVM ___EVM ____EVM _____EVM" \

--output-omit "<program> <code> <callGas> <touchedAccounts> <interimStates> <callStack> <callData>" \

--no-alpha-renaming --restore-original-names --no-sort-collections \

--output json \

"$@"

}

view_klab() {

local klab_log

klab_log="$(basename "${run_file%-spec.k}")"

# klab often runs out of stack space when running long-running KEVM programs

# klab debug "$klab_log"

node --stack-size=$KLAB_NODE_STACK_SIZE $(dirname $(which klab))/../libexec/klab-debug "$klab_log"

}

# Dev Commands

run_interpret() {

local interpreter kast output output_kast exit_status

interpreter="$backend_dir/driver-kompiled/interpreter"

kast="$(mktemp)"

output="$(mktemp)"

output_kast="$(mktemp)"

trap "rm -rf $kast $output $output_kast" INT TERM EXIT

exit_status=0

debugger=

case "$backend" in

ocaml) run_kast kast > "$kast"

if $debug; then debugger=ocamldebug; fi

$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" -c PGM "$kast" textfile \

-c SCHEDULE "$cSCHEDULE" text -c MODE "$cMODE" text --initializer 'initKevmCell' \

--output-file "$output" "$@" \

|| exit_status="$?"

;;

llvm) run_kast kore > "$kast"

if $debug; then debugger="gdb --args"; fi

$debugger "$interpreter" "$kast" -1 "$output" "$@" \

|| exit_status="$?"

;;

*) fatal "Bad backend for interpreter: '$backend'"

;;

esac

if [[ "$exit_status" != '0' ]]; then

k-bin-to-text "$output" "$output_kast"

cat "$output_kast" | "$0" kast --backend "$backend" - pretty --input kast --sort GeneratedTopCell

exit "$exit_status"

fi

}

# Main

# ----

run_command="$1" ; shift

if [[ "$run_command" == 'help' ]]; then

echo "

usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*

$0 interpret [--backend (ocaml|llvm)] [--debug] <pgm> <interpreter arg>*

$0 kast [--backend (ocaml|java|llvm|haskell|web3)] <pgm> <output format> <K arg>*

$0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>

$0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*

$0 klab-run <pgm> <K arg>*

$0 klab-prove <spec> <K arg>* -m <def_module>

$0 klab-view <spec>

$0 run : Run a single EVM program

$0 interpret : Run JSON EVM programs without K Frontend (external parser)

$0 kast : Parse an EVM program and output it in a supported format

$0 prove : Run an EVM K proof

$0 search : Search for a K pattern in an EVM program execution

$0 klab-(run|prove) : Run program or prove spec and dump StateLogs which KLab can read

$0 klab-view : View the statelog associated with a given program or spec

Note: <pgm> is a path to a file containing an EVM program/test.

<spec> is a K specification to be proved.

<K arg> is an argument you want to pass to K.

<interpreter arg> is an argument you want to pass to the derived interpreter.

<output format> is the format for Kast to output the term in.

<pattern> is the configuration pattern to search for.

<def_module> is the module to take as axioms when doing verification.

klab-view: Make sure that the 'klab/bin' directory is on your PATH to use this option.

"

exit 0

fi

backend="llvm"

debug=false

dump=false

[[ ! "$run_command" == 'prove' ]] || backend='java'

[[ ! "$run_command" =~ klab* ]] || backend='java'

while [[ $# -gt 0 ]]; do

arg="$1"

case $arg in

--backend)

backend="$2"

shift 2

;;

--debug)

debug=true

shift

;;

--dump)

dump=true

shift

;;

*)

break

;;

esac

done

backend_dir="$defn_dir/$backend"

[[ ! "$backend" == "ocaml" ]] || eval $(opam config env)

# get the run file

run_file="$1" ; shift

if [[ "$run_file" == '-' ]]; then

tmp_input="$(mktemp)"

trap "rm -rf $tmp_input" INT TERM EXIT

cat - > "$tmp_input"

run_file="$tmp_input"

fi

[[ -f "$run_file" ]] || fatal "File does not exist: $run_file"

cMODE="\`${MODE:-NORMAL}\`(.KList)"

cSCHEDULE="\`${SCHEDULE:-BYZANTIUM}_EVM\`(.KList)"

cCHAINID="#token(\"${CHAINID:-28346}\",\"Int\")"

case "$run_command-$backend" in

# Running

run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;;

kast-@(ocaml|java|llvm|haskell|web3) ) run_kast "$@" ;;

interpret-@(ocaml|llvm) ) run_interpret "$@" ;;

prove-@(java|haskell) ) run_prove "$@" ;;

search-@(java|haskell) ) run_search "$@" ;;

klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;

klab-view-java ) view_klab "$@" ;;

*) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;;

esac