ksol

#!/usr/bin/env bash

set -euo pipefail
shopt -s extglob

ksol_script="$0"
while [[ -h "$ksol_script" ]]; do
    ksol_dir="$(cd -P "$(dirname "$ksol_script")" && pwd)"
    ksol_script="$(readlink "$ksol_script")"
    [[ "$ksol_script" != /* ]] && ksol_script="$ksol_dir/$ksol_script"
done
ksol_dir="$(cd -P "$(dirname "$ksol_script")" && pwd)"

build_dir="$ksol_dir/.build"
release_dir="$build_dir/k/k-distribution/target/release/k"
defn_dir="$build_dir/defn"

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

test_logs="$build_dir/logs"
test_log="$test_logs/tests.log"
mkdir -p "$test_logs"

klab_dir="$build_dir/klab"

# Utilities
# ---------

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

pretty_diff() {
    git --no-pager diff --no-index "$@"
}

# Runners
# -------

run_krun() {
    local run_file

    run_file="$1" ; shift

    export K_OPTS=-Xss500m
    krun --directory "$backend_dir" "$run_file" "$@"
}

run_proof() {
    local proof_file

    proof_file="$1" ; shift
    [[ -f "$proof_file" ]] || die "$proof_file does not exist"

    export K_OPTS=-Xmx8G
    kprove --directory "$backend_dir" --def-module SOLIDITY "$proof_file" "$@"
}

run_klab() {
    local run_mode run_file

    run_mode="$1" ; shift
    run_file="$1" ; shift

    $0 "$run_mode" --backend java "$run_file" \
        --state-log --state-log-path "$klab_dir/data" --state-log-id klab-statelog \
        --state-log-events OPEN,EXECINIT,SEARCHINIT,REACHINIT,REACHTARGET,REACHPROVED,NODE,RULE,SRULE,RULEATTEMPT,IMPLICATION,Z3QUERY,Z3RESULT,CLOSE \
        --output-flatten "_Map_ #And" \
        --output-tokenize "#statements #exeStmt _,__SOLIDITY-SYNTAX" \
        --no-alpha-renaming --restore-original-names --no-sort-collections \
        --output json \
        "$@" \
        >/dev/null || true

    export KLAB_OUT="$klab_dir"
    klab debug klab-statelog
}

run_test() {
    local test_file expected_file output_file

    test_file="$1" ; shift

    test_log_name="$test_logs/$test_file"
    mkdir -p "$(dirname "$test_log_name")"

    output_file="$test_log_name.out"

    if [[ -f "$test_file.out" ]]; then
        expected_file="$test_file.out"
    else
        expected_file="tests/success-$backend.out"
    fi

    [[ -f "$expected_file" ]] \
        || die "Expected output file '$expected_file' does not exist..."

    run_krun "$test_file" > "$output_file" || true
    pretty_diff "$expected_file" "$output_file"
}

# Main
# ----

cd "$(dirname $0)"

# main functionality
run_command="$1" ; shift

backend="java"
if [[ $# -gt 0 ]] && [[ $1 == '--backend' ]]; then
    backend="$2"
    shift 2
fi
backend_dir="$defn_dir/$backend"
[[ ! "$backend" == "ocaml" ]] || eval $(opam config env)

case "$run_command-$backend" in

    # Running
    run-@(ocaml|java)      ) run_krun                        "$@" ;;
    prove-java             ) run_proof                       "$@" ;;
    test-@(ocaml|java)     ) run_test                        "$@" ;;
    klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;

    *) echo "
    usage: $0 (run|test) [--backend (ocaml|java|haskell)] <pgm>      <K args>*
           $0 prove      [--backend (java|haskell)]       <spec>     <K args>*
           $0 klab-(run|prove)                            <spec/pgm> <K args>*

       $0 run              : Run a single Solidity program
       $0 prove            : Prove a single Solidity specification
       $0 test             : Run a single Solidity program like it's a test
       $0 klab-(run|prove) : Run a program and launch KLab on the execution graph

       Note: <pgm> is a path to a file containing a Solidity program.
             <K args> are any arguments you want to pass to K when executing.
             klab-run requires that the 'klab/bin' is on your PATH.
" ; exit ;;
esac