#!/bin/sh
# -*- sh -*-

if test "$1" = "--export"; then
    EXPORT=1
    SRC_ROOT=.
    shift
else
    test -e lib/testcase && SILENT=1 . lib/testcase
    EXPORT= # unset
fi
export EXPORT

run()
{
    if test -n "$EXPORT"; then echo "$@"; else echo "+ divine $@"; divine "$@"; fi
}

getopt() { perl -ne "print \$1 if (m,/\* $1: (.*?) \*/, or m,// $1: (.*?)\n,)" $2; }

opts=$(eval echo $(getopt VERIFY_OPTS $1))
args=$(eval echo $(getopt PROGRAM_OPTS $1))
ccopt=$(eval echo $(getopt CC_OPTS $1))
extrasrc=$(eval echo $(getopt EXTRA_SRCS $1))
gtest=
skipcc=$(getopt SKIP_CC $1)

std=
echo "$1" | grep -q '.cpp$' && { echo $ccopts | grep -qv -- '-std'; } && std="-std=c++17"

if test -z "$EXPORT"; then
    resources="--max-memory 4GiB --threads 1"
    extra="--report-filename verify.out"
fi

if test "$(eval echo $(getopt USE_GTEST $1))" = 1; then
    gtest="$TESTS/lib/gtest/src/gtest-all.cc $TESTS/lib/gtest/src/gtest_main.cc -I$TESTS/lib/gtest"
fi

if test -z "$EXPORT" && echo "$opts" | grep "symbolic"; then
    solver=$TEST_FLAVOUR
    if test $solver = z3 && test $OPT_Z3 = OFF; then skip; fi
    if test $solver = stp && test $OPT_STP = OFF; then skip; fi
    if test $solver = smtlib; then solver=$solver:z3; z3 --version > /dev/null || skip; fi
    if test $solver = vanilla; then solver=none; fi
    extra="$extra --solver $solver"
fi

if test -n "$EXPORT"; then
    dir=$(dirname $1)
    name=$(basename $1)
    srcroot=$(readlink -f $(dirname $0)/../../)
    dios=$srcroot/dios
    incs="-isystem $dios/include -isystem $dios/libcxx/include"
    incs="$incs -I $srcroot/bricks"
    for f in $name $extrasrc; do
        deps=$(cd $dir && clang -I. $incs $std -MM -MT "" $f | sed -e 's,^: [^ ]*,,' -e 's,\\$,,')
        echo load $dir/$f $f
        for dep in $deps; do
            if ! echo $dep | grep -q '^/'; then dep=$dir/$dep; fi
            echo load $dep $(echo $dep | sed -e s,$srcroot/*,,)
        done
    done
    check=$(readlink -f $(dirname $0)/check)
    (cd $dir ; $check verify $name)
else
    name="$1"
fi

if test "$skipcc" = 1; then
    run=$name
    opts="$std $opts"
else
    run cc -o testcase.bc $std $ccopt "$name" $gtest
    run=testcase.bc
fi

run verify $resources $extra $opts $run $args

if test -n "$EXPORT"; then exit 0; fi

err=$(grep "error found:" verify.out | cut -d' ' -f3- || true)
if [ "$err" = yes ]; then
    echo "+ divine sim --batch --skip-init --load-report verify.out"
    echo "backtrace" | \
        divine sim --batch --skip-init --load-report verify.out > sim.out 2>&1
fi

check verify "$name"

# vim: syntax=sh