#!/usr/bin/env bash

set -e # Exit immediately if any command fails

set -u # Using undefined variables is an error. Exit immediately

# https://stackoverflow.com/questions/59895/getting-the-source-directory-of-a-bash-script-from-within

kevm_script="$0"

while [[ -h "$kevm_script" ]]; do

kevm_dir="$(cd -P "$(dirname "$kevm_script")" && pwd)"

kevm_script="$(readlink "$kevm_script")"

[[ "$kevm_script" != /* ]] && kevm_script="$kevm_dir/$kevm_script"

done

kevm_dir="$(cd -P "$(dirname "$kevm_script")" && pwd)"

build_dir="$kevm_dir/.build"

test_logs="$build_dir/logs"

mkdir -p "$test_logs"

now_passing="$test_logs/passing.lastrun"

now_failing="$test_logs/failing.lastrun"

run_times="$test_logs/runtime"

# Utilities

# ---------

progress() { echo "== $@" ; }

warning() { echo -e "WARNING:" "$@" >&2 ; }

die() { echo -e "FATAL:" "$@" >&2 ; exit 1 ; }

pretty_diff() {

git --no-pager diff --no-index "$@"

}

# Environment Setup

# -----------------

run_env() {

local run_file=$1

local release_dir="${K_BIN:-$build_dir/k/k-distribution/target/release/k}"

local lib_dir="$build_dir/local/lib"

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

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

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

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

eval $(opam config env)

}

# Runners

# -------

# User Commands

run_krun() {

local backend=$1 ; shift

local run_file=$1 ; shift

run_env "$run_file"

export K_OPTS=-Xss500m

krun --directory "$build_dir/$backend/" -cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' -cMODE="$cMODE" -pMODE='printf %s' "$run_file" "$@"

}

run_kdebug() {

progress "debugging: $1"

run_krun java "$1" --debugger

}

run_ksearch() {

progress "searching: $1"

run_krun java "$1" --search

}

run_proof() {

local proof_file="$1" ; shift

[[ -f "$proof_file" ]] || die "$proof_file does not exist"

run_env "$proof_file"

export K_OPTS=-Xmx5G

kprove --directory "$build_dir/java/" --z3-executable "$proof_file" --def-module VERIFICATION "$@"

}

# Dev Commands

run_interpreter() {

test_file="$1"

run_env "$test_file"

interpreter="$build_dir/ocaml/driver-kompiled/interpreter"

kast="$(mktemp)"

output="$(mktemp)"

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

"$kevm_dir/kast-json.py" "$test_file" > "$kast"

$interpreter "$build_dir/ocaml/driver-kompiled/realdef.cma" -c PGM "$kast" textfile \

-c SCHEDULE "$cSCHEDULE" text -c MODE "$cMODE" text \

--output-file "$output"

}

run_test() {

local test_file="$1" ; shift

case "$test_file" in

*proofs/* ) run_proof "$test_file" --debug "$@"

;;

*interactive/*) local expected_file="$1" ; shift

local output_file="$(mktemp "$test_file.out.XXXXXX")"

trap "rm -rf $output_file" INT TERM EXIT

run_krun ocaml "$test_file" --interpret "$@" > "$output_file" \

|| pretty_diff "$expected_file" "$output_file"

;;

* ) run_interpreter "$test_file"

;;

esac

}

run_test_profile() {

local test_file="$1" ; shift

local start_time="$(date '+%s')"

local exit_status='0'

local output_log_dir="$test_logs/$(dirname -- "$test_file")"

local stdout_log="$test_logs/$test_file.out"

local stderr_log="$test_logs/$test_file.err"

[[ -d "$output_log_dir" ]] || mkdir -p "$output_log_dir"

run_test "$test_file" "$@" 1> "$stdout_log" 2> "$stderr_log" || exit_status="$?"

local end_time="$(date '+%s')"

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

echo "$test_file" >> "$now_passing"

else

echo "$test_file" >> "$now_failing"

cat "$stdout_log"

cat "$stderr_log" >&2

fi

echo "$((end_time - start_time)) $test_file" >> "$run_times"

exit "$exit_status"

}

run_sort_logs() {

local tmp_file

tmp_log="$(mktemp $test_logs/log.XXXXXX)"

for log in $now_passing $now_failing; do

if [[ -f "$log" ]]; then

sort -u "$log" > "$tmp_log"

cp "$tmp_log" "$log"

fi

done

if [[ -f "$run_times" ]]; then

sort -k2 -u "$run_times" > "$tmp_log"

cp "$tmp_log" "$run_times"

fi

}

run_get_failing() {

count="${1:-1}"

cat "$now_failing" | sort -R | head -n"$count"

}

# Main

# ----

run_command="$1" ; shift

case "$run_command" in

# Running

run) run_krun ocaml "$@" --interpret ;;

debug) run_kdebug "$@" ;;

search) run_ksearch "$@" ;;

prove) run_proof "$@" ;;

# Testing

interpret) run_interpreter "$@" ;;

test) run_test "$@" ;;

test-profile) run_test_profile "$@" ;;

sort-logs) run_sort_logs ;;

get-failing) run_get_failing "$@" ;;

*) echo "

normal usage

============

$0 [run|debug|search] <pgm> <K args>*

$0 prove <spec> <K args>*

- run Run a single EVM program

- debug Run a single EVM program in the debugger

- search Run a program searching for all execution paths

- prove Attempt to prove the specification using K's RL prover

Note: <pgm> and <spec> here are paths to files.

These files should be Ethereum programs/specifications.

<K args> are any options you want to pass directly to K.

Useful <K args> are:

- --debug: output more debugging information when running/proving.

Examples:

$ $0 run tests/ethereum-tests/VMTests/vmArithmeticTest/add0.json

$ $0 debug tests/interactive/gas-analysis/sumTo10.evm

$ $0 prove tests/proofs/specs/examples/sum-to-n-spec.k

ci usage

========

These commands are more for devs and CI servers.

$0 interpret <pgm>

$0 [test|test-profile] <pgm> <output>

$0 sort-logs

$0 get-failing [<count>]

- interpret Run a single EVM program (in JSON testing format) using fast interpreter

- test Run a single EVM program like it's a test

- test-profile Same as test, but generate list of failing tests and dump timing information

- sort-logs Normalize the test logs for CI servers to use

- get-failing Return a list of failing tests, at most <count>.

Note: <output> is the expected output of the given test.

" ; exit ;;

esac