kyul

#!/usr/bin/env bash
set -e
set -euo pipefail
shopt -s extglob

kyul_dir="${KYUL_DIR:-.}"
build_dir="$kyul_dir/.build"
defn_dir="${KYUL_DEFN_DIR:-$build_dir/defn}"
lib_dir="$build_dir/local/lib"
k_release_dir="${K_RELEASE:-$kyul_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() {
    local output_mode

    output_mode=kast

    export K_OPTS=-Xss500m
    case "$backend" in
        ocaml) args=(--interpret) ;;
        *)     args=()            ;;
    esac
    krun --directory "$backend_dir" -pMODE='printf %s' "$run_file" # \
         # --output "$output_mode" \
         # --output-flatten "_Map_" \
         # "${args[@]-}" "$@" 
}

run_kast() {
    local output_mode

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

    case "$run_file-$output_mode" in
        *.json-@(kast|kore)) "$kyul_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
    kprove --directory "$backend_dir" "$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" \
        --debug \
        --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 "<programBytes> <program> <code> <callGas> <touchedAccounts> <interimStates> <callStack> <callData>" \
        --output json \
        --no-alpha-renaming --restore-original-names --no-sort-collections \
        "$@"
}

view_klab() {
    local klab_log

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

    # klab often runs out of stack space when running long-running KYUL 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
    case "$backend" in
        ocaml)  run_kast kast > "$kast"
                "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" -c PGM "$kast" textfile \
                             -c SCHEDULE "$cSCHEDULE" text -c MODE "$cMODE" text -c CHAINID "$cCHAINID" text --initializer 'initKevmCell' \
                             --output-file "$output" "$@" \
                    || exit_status="$?"
                ;;

        llvm)   run_kast kore > "$kast"
                "$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"
        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)]              <pgm>  <interpreter arg>*
               $0 kast       [--backend (ocaml|java)]              <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="java"
[[ ! "$run_command" == 'prove' ]] || backend='java'
[[ ! "$run_command" =~ klab*   ]] || backend='java'
if [[ $# -gt 0 ]] && [[ $1 == '--backend' ]]; then
    backend="$2"
    shift 2
fi
backend_dir="$defn_dir/$backend"
[[ ! "$backend" == "ocaml" ]] || eval $(opam config env)

# get the run file
if [[ ! "$run_command" == 'web3' ]]; then
    run_file="$1" ; shift
    [[ -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) ) run_kast                        "$@" ;;
    interpret-@(ocaml|llvm)         ) run_interpret                   "$@" ;;
    prove-@(java|haskell)           ) run_prove                       "$@" ;;
    search-@(java|haskell)          ) run_search                      "$@" ;;
    web3-@(llvm)                    ) run_web3                        "$@" ;;
    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