#!/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_web3() {

local web3_port

web3_port="$1" ; shift

run_file='-'

if $debug; then

gdb --args ${defn_dir}/web3/build/kevm-client --port "$web3_port" "$@"

elif $dump; then

exec -a "$0 web3" ${defn_dir}/web3/build/kevm-client -p "$web3_port" "$@" 3>&2 2>&1 1>&3 \

| "$0" kast --backend web3 - pretty --input kore --sort GeneratedTopCell

else

exec -a "$0 web3" ${defn_dir}/web3/build/kevm-client - "$web3_port" "$@" 2>/dev/null

fi

}

run_web3_send() {

local web3_port web3_method web3_params

web3_port="$1" ; shift

web3_method="$1" ; shift

join_args() {

local IFS=','

echo "$*"

}

web3_params="$(join_args "$@")"

curl -X POST --data '{"jsonrpc": "2.0", "id": 1, "method": "'"$web3_method"'", "params": ['"$web3_params"']}' 127.0.0.1:"$web3_port"

}

run_web3_ganache() {

local web3_port

web3_port="$1" ; shift

notif 'Launching web3 client'

$0 web3 "$web3_port" "$@" &

while ! netcat -z 127.0.0.1 "$web3_port"; do sleep 0.1; done

notif 'Generating accounts'

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0xdc7e9a7c64933ab893160b79d099c254d274e1c40c6df6d5239e1a623e3d6de1", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0x6e2687f9732d970c6b1d5baa3dff26c4af36257552bc17df737afbc00ca70de2", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0xd34d8e873da77217abaef9424a7d87fce351b603920c7f5288d7701c5f148860", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0x976b5ec9253759d4a2746c37597841beba57527123dc3db2165b637adce58bcb", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0x23dff7ac7981167eb5386e51c3d6d2e3ca9dc219315749b2058d0a2d1e21625e", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0xe040e4bf96d8c9d3a8d1ffb22b30ed4b0a79a25342d656c5a8e2784b0fab752f", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0x13abddd7d94165fc46bed2cad6b0b14cd0267a85f70ad5c26cce82c609e0bf87", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0x0e29f7d6984bb47d60db479212ca56af516705b07d8753b474bd7f0db8bc1921", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0xea7fe1480e9ab71c261c5e1e727f36482f84dbdb07dbf8c8e9f767dcecf87568", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

curl -X POST --data '{"jsonrpc":"2.0","id":1,"method":"firefly_addAccount","params":[{"key":"0x5f9addbbf41ae2e3d6cb7b07ffabf2c5ff6edc3a38c9dd64a9afd23df02ad7ee", "balance":"0x56BC75E2D63100000"}]}' 127.0.0.1:8545

}

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 web3 [--debug|--dump] <port>

$0 web3-ganache [--debug|--dump] <port>

$0 web3-send <port> <web3 method> <web3 params>

$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 web3 : Run version of semantics which understand Web3 RPC (**UNDER CONSTRUCTION**)

$0 web3-send : Send message to running Web3 instance of KEVM (**UNDER CONSTRUCTION**)

$0 web3-ganache : Run version of semantics which understand Web3 RPC and is able to communicate with Truffle Test Framework (**UNDER CONSTRUCTION**)

$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.

<port> is the port to listen on for Web3 JSON RPC requests.

<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'

[[ ! "$run_command" =~ web3* ]] || backend='llvm'

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

if [[ ! "$run_command" =~ web3* ]]; then

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"

fi

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 "$@" ;;

web3-@(llvm) ) run_web3 "$@" ;;

web3-send-@(llvm) ) run_web3_send "$@" ;;

web3-ganache-@(llvm) ) run_web3_ganache "$@" ;;

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