#!/bin/bash

# Since we use regular 'make install' for the sub-projects,
# the symbiotic directory has a given hierarchy. It's easier
# to assume this hierarchy in our scripts that to set up
# autotools to install files as we want to.
#
# The directory hierarchy looks like this:
#
# symbiotic \
#           bin     \
#                   klee
#                   clang
#                   llvm-link
#                   opt
#                   stp
#           lib     \
#                   libstp.so
#                   LLVMSlicer.so
#                   LLVMsvc13.so
#                   libkleeRuntimeIntrinsic.bca
#                   ....
#           include \
#                   symbiotic.h
#                   klee \
#                           klee.h
#           build-fix.sh
#           instrument.sh
#           process_set.sh
#           runme
#           VERSIONS

result()
{
	echo $1

	if [ -z "$2" ]; then
		exit 0
	else
		exit $2
	fi
}

LOG_FILE=

error()
{
	# dump log file on error in debugging mode
	if [ "x$DEBUG" != "x" -a "x$LOG_FILE" != "x" ]; then
		cat "$LOG_FILE"
		echo "===== EOF"
	fi

	result "ERROR" 1
}

debug()
{
	if [ "x$DEBUG" != "x" ]; then
		echo "DBG: $1"
	fi
}

# return true if first argument represents given property
check_property()
{
	PROP="$1"
	PATTERN="$2"

	# if PROP is file, read property from file
	# otherwise assume that PROP is the property
	if [ -f "$PROP" ]; then
		CMD=cat
	else
		CMD=echo
	fi

	if $CMD "$PROP" | grep -q "$PATTERN"; then
		return 0
	fi

	return 1
}

if [ -z "$1" ]; then
	echo no input file >&2
	error
fi

if ! which clang >/dev/null 2>&1; then
	echo CLANG not found >&2
	error
fi

# args processing
DIR="`dirname $0`"
PROP=
while getopts 'p:6' OPT; do
	case "$OPT" in
		p) PROP="$OPTARG" ;;
		6) MFLAG="-m64" ;;
	esac
done
export MFLAG
shift $(($OPTIND-1))
FILE="$1"

if [ -n "$PROP" ] &&
   (! check_property "$PROP" 'CHECK *( *init(main()), *LTL(G *! *call(__VERIFIER_error())) *)' && \
    ! check_property "$PROP" 'CHECK *( *init(main()), *LTL(G *! *label(ERROR)) *)'); then
	result UNKNOWN
fi

# write logs into separate directory
if [ -z "$LOGSDIR" ]; then
	LOGSDIR="logs"
fi
mkdir -p "$LOGSDIR"

LOG_FILE=`basename $FILE`
LOG_FILE="${LOGSDIR}/${LOG_FILE%.c}.proc-log"

export KLEE=$DIR/bin/klee
if [ "x$MFLAG" = "x-m64" ]; then
	export KLEE_RUNTIME_LIBRARY_PATH="$DIR/lib"
else
	export KLEE_RUNTIME_LIBRARY_PATH="$DIR/lib32"
fi

export LIB="$DIR/lib.c"
export LIBo="`dirname $FILE`/lib.o"
export LIB_CFLAGS="-I$DIR/include"
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$DIR/lib"
export PATH="$DIR/bin:$PATH"

# make process_set not running klee, we'll run it here
export RUN_KLEE="no"

$DIR/instrument.sh "$FILE" >"$LOG_FILE" 2>&1
$DIR/build-fix.sh "$FILE" >>"$LOG_FILE" 2>&1
$DIR/process_set.sh "$FILE" >>"$LOG_FILE" 2>&1
case $? in
	0) ;;
	2) result UNKNOWN ;;
	*) error ;;
esac

rm -rf "$FILE-klee-out"

KLEE_OUTPUT_FILE="${FILE%.c}.log"
$DIR/bin/klee -output-dir="$FILE-klee-out" -optimize "${FILE%.c}.o" 2>&1 |
	tee $KLEE_OUTPUT_FILE |
	while read LINE; do
		# if we run into assert, we don't need to explore
		# all paths and can give result right now
		if grep -i -q 'assertion failed'; then
			# let this subshell return 3, so that whole
			# command will return 3 and we can catch it
			result FALSE 3
		fi
	done

# if we already found assert, do not parse the output
if [ $? -eq 3 ]; then
	debug "`cat $KLEE_OUTPUT_FILE`"
	exit 0
fi

KLEE_RESULT=`$DIR/klee-log-parser.sh $KLEE_OUTPUT_FILE`

if echo "$KLEE_RESULT" | grep -q '^E'; then
	debug "$KLEE_RESULT"
	debug "`cat $KLEE_OUTPUT_FILE`"

	result UNKNOWN
elif echo "$KLEE_RESULT" | grep -q '^ASSERTIONFAILED'; then
	debug "$KLEE_RESULT"
	debug "`cat $KLEE_OUTPUT_FILE`"

	result FALSE
else
	debug "$KLEE_RESULT"
	debug "`cat $KLEE_OUTPUT_FILE`"

	result TRUE
fi
