#!/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
    krun --directory "$backend_dir"                                      \
        -cSCHEDULE="$cSCHEDULE"                   -pSCHEDULE='printf %s' \
        -cMODE="$cMODE"                           -pMODE='printf %s'     \
        -cCHAINID="#token(\"$cCHAINID\",\"Int\")" -pCHAINID='printf %s'  \
        "$run_file" "$@"
}

run_kast() {
    local output_mode

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

    case "$run_file-$output_mode" in
        *.json-@(kast|kore)) "$kevm_dir/$output_mode-json.py" "$run_file" "$cSCHEDULE" "$cMODE" "$cCHAINID" ;;
        *)                   kast --directory "$backend_dir" "$run_file" --output "$output_mode" "$@"       ;;
    esac
}

run_prove() {
    local def_module smt_prelude_set run_dir smt_file smt_args

    def_module="$1" ; shift

    # 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

    export K_OPTS=-Xmx8G
    kprove --directory "$backend_dir" "${smt_args[@]-}" "$run_file" --def-module "$def_module" "$@"
}

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
    kevm_port=$(tests/web3/get_port.py)
    run_file='-'
    if $debug; then
        gdb --args ${defn_dir}/web3/build/kevm-client --port "$web3_port" --kport "$kevm_port" "$@"
    elif $dump; then
      exec -a "$0 web3" ${defn_dir}/web3/build/kevm-client --dump --port "$web3_port" --kport "$kevm_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 --port "$web3_port" --kport "$kevm_port" "$@" 2>/dev/null
    fi
}

run_web3_send() {
    local web3_port web3_method web3_params web3_file
    web3_port="$1" ; shift

    if [[ -f "$1" ]]; then
        web3_file="$1" ; shift
        curl -s -X POST 127.0.0.1:$web3_port --data @$web3_file
    else
        web3_method="$1" ; shift
        join_args() {
            local IFS=','
            echo "$*"
        }
        web3_params="$(join_args "$@")"
        curl -s -X POST --data '{"jsonrpc": "2.0", "id": 1, "method": "'"$web3_method"'", "params": ['"$web3_params"']}' 127.0.0.1:"$web3_port"
    fi
}

run_web3_ganache() {
    local web3_port
    web3_port="$1" ; shift

    notif 'Launching web3 client'
    $0 web3 "${args[@]}" "$web3_port" "$@" &
    while ! netcat -z 127.0.0.1 "$web3_port" ; do sleep 0.1; done
    notif 'Generating accounts'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xdc7e9a7c64933ab893160b79d099c254d274e1c40c6df6d5239e1a623e3d6de1", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x6e2687f9732d970c6b1d5baa3dff26c4af36257552bc17df737afbc00ca70de2", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xd34d8e873da77217abaef9424a7d87fce351b603920c7f5288d7701c5f148860", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x976b5ec9253759d4a2746c37597841beba57527123dc3db2165b637adce58bcb", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x23dff7ac7981167eb5386e51c3d6d2e3ca9dc219315749b2058d0a2d1e21625e", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xe040e4bf96d8c9d3a8d1ffb22b30ed4b0a79a25342d656c5a8e2784b0fab752f", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x13abddd7d94165fc46bed2cad6b0b14cd0267a85f70ad5c26cce82c609e0bf87", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x0e29f7d6984bb47d60db479212ca56af516705b07d8753b474bd7f0db8bc1921", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0xea7fe1480e9ab71c261c5e1e727f36482f84dbdb07dbf8c8e9f767dcecf87568", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_addAccount '{"key":"0x5f9addbbf41ae2e3d6cb7b07ffabf2c5ff6edc3a38c9dd64a9afd23df02ad7ee", "balance":"0x56BC75E2D63100000"}'
    $0 web3-send "$web3_port" firefly_genesisBlock

}

run_klab() {
    local run_mode klab_log def_module

    run_mode="$1" ; shift
    klab_log="$(basename "${run_file%-spec.k}")"

    def_module="$1" ; shift

    "$0" "$run_mode" --backend java "$run_file" "$def_module" \
        --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-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_text output_format exit_status

    interpreter="$backend_dir/driver-kompiled/interpreter"
    kast="$(mktemp)"
    output="$(mktemp)"
    output_text="$(mktemp)"
    trap "rm -rf $kast $output $output_text" INT TERM EXIT
    exit_status=0
    debugger=
    output_format='kore'
    case "$backend" in
        java)    run_kast kast > "$kast"
                 output_format='kast'
                 run_file="$kast"
                 run_krun --parser 'cat' --output kast > "$output" || exit_status="$?"
                 if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
                     cat "$output" | "$0" kast --backend "$backend" - pretty --input "$output_format"
                 fi
                 exit "$exit_status"
                 ;;

        llvm)    run_kast kore > "$kast"
                 if $debug; then debugger="gdb --args"; fi
                 $debugger "$interpreter" "$kast" -1 "$output" "$@" \
                     || exit_status="$?"
                 if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
                     cat "$output" | "$0" kast --backend "$backend" - pretty --input "$output_format" --sort GeneratedTopCell
                 fi
                 exit "$exit_status"
                 ;;

        haskell) run_kast kore > "$kast"
                 kore-exec "$backend_dir/driver-kompiled/definition.kore" --pattern "$kast" --module ETHEREUM-SIMULATION --smt none --output "$output" \
                     || exit_status="$?"
                 if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
                     cat "$output" | "$0" kast --backend "$backend" - pretty --input "$output_format" --sort GeneratedTopCell
                 fi
                 exit "$exit_status"
                 ;;

        *)      fatal "Bad backend for interpreter: '$backend'"
                ;;
    esac
}

# Main
# ----

run_command="$1" ; shift

if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
    echo "
        usage: $0 run          [--backend (llvm|java|haskell)]           <pgm>  <K arg>*
               $0 interpret    [--backend (llvm)] [--debug|--no-unparse] <pgm>  <interpreter arg>*
               $0 interpret    [--backend (java|haskell)] [--no-unparse] <pgm>
               $0 kast         [--backend (llvm|java|haskell|web3)]      <pgm>  <output format> <K arg>*
               $0 prove        [--backend (java|haskell)]                <spec> <def_module> <K arg>*
               $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>|<web3_file>]
               $0 klab-run                                               <pgm>  <K arg>*
               $0 klab-prove                                             <spec> <def_module> <K arg>*
               $0 klab-view                                              <spec>

               $0 [help|--help|version|--version]

           $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

           $0 help    : Display this help message.
           $0 version : Display the versions of KEVM, K, Kore, and Z3 in use.

           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.
                 <web3_method> is the specific web3 method to call.
                 <web3_params> is an optional list of parameters to pass to the <web3_method>.
                 <web3_file> specifies a JSON file to feed as input into the web3 server.

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

if [[ "$run_command" == 'version' ]] || [[ "$run_command" == '--version' ]]; then
    notif "KEVM Version"
    git rev-parse --short HEAD
    notif "K Version"
    kompile --version
    notif "Kore Version"
    kore-exec --version
    notif "Z3 Version"
    z3 --version
    exit 0
fi

backend="llvm"
debug=false
dump=false
unparse=true
[[ ! "$run_command" == 'prove' ]] || backend='java'
[[ ! "$run_command" =~ klab*   ]] || backend='java'
[[ ! "$run_command" =~ web3*   ]] || backend='llvm'
args=()
while [[ $# -gt 0 ]]; do
    arg="$1"
    case $arg in
        --backend)    args+=("$arg" "$2") ; backend="$2"  ; shift 2 ;;
        --debug)      args+=("$arg")      ; debug=true    ; shift   ;;
        --dump)       args+=("$arg")      ; dump=true     ; shift   ;;
        --no-unparse) args+=("$arg")      ; unparse=false ; shift   ;;
        *)            break                                         ;;
    esac
done
backend_dir="$defn_dir/$backend"

# 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:-ISTANBUL}_EVM\`(.KList)"
cCHAINID="${CHAINID:-1}"

case "$run_command-$backend" in

    # Running
    run-@(java|llvm|haskell)       ) run_krun                        "$@" ;;
    kast-@(java|llvm|haskell|web3) ) run_kast                        "$@" ;;
    interpret-@(llvm|haskell|java) ) 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