kplc

#!/usr/bin/env bash

set -euo pipefail
shopt -s extglob

notif() {
    if ${verbose}; then
        echo "== $0 [$(date)]: $@" >&2
    else
        echo "== $0: $@" >&2
    fi
}

fatal() { notif "[FATAL] $@" ; exit 1 ; }

notif_exec() {
    notif "$@"
    "$@"
}

INSTALL_BIN="$(cd $(dirname $0) && pwd)"
INSTALL_LIB="$(dirname ${INSTALL_BIN})/lib/kplutus"
INSTALL_INCLUDE=${INSTALL_LIB}/include
KPLC=kplc

install_k_bin=${INSTALL_LIB}/kframework/bin
plugin_include=${INSTALL_LIB}/blockchain-k-plugin/include
libff_dir=${INSTALL_LIB}/libff
libcryptopp_dir=${INSTALL_LIB}/cryptopp

export PATH="${INSTALL_BIN}:${INSTALL_LIB}:${install_k_bin}:${PATH}"

export K_OPTS="${K_OPTS:--Xmx16G -Xss512m}"

# Runners
# -------

run_kplutus_pyk() {
    notif_exec kplutus-pyk --kplc-lib ${INSTALL_LIB} "$@"
}

run_kompile() {
    local kompile_opts

    kompile_opts=( "${run_file}" --directory "${backend_dir}" --backend "${backend}"     )
    kompile_opts+=( -I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework" )
    kompile_opts+=( --hook-namespaces "KRYPTO"                                           )
    kompile_opts+=( --emit-json                                                          )

    case "${backend}" in
        haskell) kompile_opts+=( --md-selector "k | libcrypto-extra | symbolic" )
                 ;;
        llvm)    kompile_opts+=( --md-selector "k | libcrypto-extra | concrete"                                )
                 kompile_opts+=( -ccopt -L${libff_dir}/lib -ccopt -I${libff_dir}/include                       )
                 kompile_opts+=( -ccopt ${plugin_include}/c/plugin_util.cpp                                    )
                 kompile_opts+=( -ccopt ${plugin_include}/c/crypto.cpp                                         )
                 kompile_opts+=( -ccopt ${plugin_include}/c/hash_ext.cpp                                       )
                 kompile_opts+=( -ccopt ${plugin_include}/c/blake2.cpp                                         )
                 kompile_opts+=( -ccopt -std=c++14                                                             )
                 kompile_opts+=( -ccopt -lff -ccopt -lcryptopp -ccopt -lsecp256k1 -ccopt -lssl -ccopt -lcrypto )
                 if [[ "$(uname -s)" == 'Linux' ]]; then
                     kompile_opts+=( -ccopt -lprocps )
                 elif [[ "$(uname -s)" == 'Darwin' ]]; then
                     openssl_root="$(brew --prefix openssl)"
                     brew_root="$(brew --prefix)"
                     kompile_opts+=( -ccopt -I${brew_root}/include -ccopt -L/${brew_root}/lib -ccopt -I${openssl_root}/include -ccopt -L${openssl_root}/lib )
                 fi
                 if [[ -d ${libcryptopp_dir} ]]; then
                     kompile_opts+=( -ccopt -I${libcryptopp_dir}/include -ccopt -L/${libcryptopp_dir}/lib )
                 fi
                 ;;
        *)       fatal "Unknown backend for kompile: ${backend}" ;;
    esac

    if ${pyk}; then
        run_kplutus_pyk kompile "${kompile_opts[@]}" "$@"
    else
        notif_exec kompile "${kompile_opts[@]}" "$@"
    fi
}

run_kast() {
    notif_exec kast --directory "${backend_dir}" "${run_file}" "$@"
}

run_interpreter() {
    if ${debugger}; then
        notif_exec krun --directory "${backend_dir}" "${run_file}" --debugger "$@"
    else
        notif_exec krun --directory "${backend_dir}" "${run_file}" "$@"                        \
            | (${result_only} && ( tr '\n' ' ' | sed "s/.*<k>\(.*\)~> \. .*/\1/g" ) || cat - )
    fi
}

run_prove() {
    local def_module run_dir proof_args bug_report_name \
          eventlog_name kprove omit_cells omit_labels klab_log pyk_args

    bug_report_name="kplc-bug-$(basename "${run_file%-spec.k}")"
    eventlog_name="${run_file}.eventlog"

    proof_args=(--directory "${backend_dir}" "${run_file}")
    proof_args+=( -I "${INSTALL_INCLUDE}/kframework" -I "${plugin_include}/kframework" )
    proof_args+=( --md-selector "k | libcrypto-extra | symbolic"                       )

    ! ${bug_report} || proof_args+=(--haskell-backend-command "kore-exec --bug-report ${bug_report_name}")
    ! ${debugger}   || proof_args+=(--debugger)

    notif_exec kprove "${proof_args[@]}" "$@"
}

run_uplc_to_k() {
    run_kplutus_pyk uplc-to-k --directory "${backend_dir}" "${run_file}" "$@"
}

# Main
# ----

run_command="$1" ; shift

if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
    echo "
        usage: ${KPLC} kompile   <main> <kplc arg>* <kompile arg>*
               ${KPLC} kast      <pgm>  <kast arg>*
               ${KPLC} run       <pgm>  <kplc arg>* <krun arg>*
               ${KPLC} uplc-to-k <pgm>  <kplc arg>*

               ${KPLC} [help|--help|version|--version]

           ${KPLC} kompile   : Run kompile with arguments setup to include KPlutus semantics.
           ${KPLC} kast      : Run kast with arguments setup to include KPlutus semantics.
           ${KPLC} run       : Run the KPlutus interpreter on a UPLC program.
           ${KPLC} uplc-to-k : Generate the helper K modules for verifying a contract
           ${KPLC} help      : Display this help message.
           ${KPLC} version   : Display the versions of KPlutus.

           Arguments:
                      <main>        : Name of main file to kompile.
                      <kplc arg>    : Arguments for the kplc script.
                      <kompile arg> : Arguments for kompile.
                      <kompile arg> : Arguments for krun.

           Available <kplc arg>:
                  --debug
                  --verbose
                  --backend
                  --directory
                  --flat-format : The input program is encoded in the flat format
    "
    exit 0
fi

result_only=false
backend='llvm'
bug_report=false
debugger=false
pyk=false
debug=false
verbose=false
flat_format=false

args=()
while [[ $# -gt 0 ]]; do
    case "$1" in
        --debug)        debug=true       ; args+=("$1") ; shift   ;;
        --flat-format)  flat_format=true                ; shift   ;;
        --verbose)      verbose=true                    ; shift   ;;
        --backend)      backend="$2"                    ; shift 2 ;;
        --directory)    backend_dir="$2"                ; shift 2 ;;
        --result-only)  result_only=true                ; shift   ;;
        --bug-report)   bug_report=true                 ; shift   ;;
        --debugger)     debugger=true                   ; shift   ;;
        --pyk)          pyk=true                        ; shift   ;;
        *)              args+=("$1")                    ; shift   ;;
    esac
done

if [[ "$run_command" == 'version' ]] || [[ "$run_command" == '--version' ]]; then
    notif 'KPlutus Version'
    cat $INSTALL_LIB/version
    exit 0
fi

[[ "${#args[@]}" -le 0 ]] || set -- "${args[@]}"
backend_dir="${backend_dir:-$INSTALL_LIB/$backend}"

run_file="$1" ; shift
[[ -f "$run_file" ]] || fatal "File does not exist: $run_file"

! ${debug} || set -x

if ${flat_format}; then
    printf '%s%s' "#" `xxd -ps "${run_file}"` > "${run_file}".hex
    run_file="${run_file}".hex
fi

case "${run_command}" in
    kompile)    run_kompile     "$@"                                                ;;
    kast)       run_kast        "$@"                                                ;;
    run)        run_interpreter "$@"                                                ;;
    prove)      run_prove       "$@"                                                ;;
    uplc-to-k)  run_uplc_to_k   "$@"                                                ;;
    *)          $0 help ; fatal "Unknown command: ${run_command}" ;;
esac