#!/bin/bash

export SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )/tmp"
if [ ! -d "$SCRIPT_DIR" ]
then
	mkdir "$SCRIPT_DIR"
fi
cd "$SCRIPT_DIR"

function main(){
	ulimit -s unlimited
	install_libs
	get_llvm_gcc
	get_llvm_2_9
	get_stp
	get_posix_env_for_klee #optional
	get_klee
}

function exitmsg {
	echo "$@"
	exit 1
}

# getting libs
function install_libs() {
echo "Assuming you have installed required libs"
echo "Have you installed g++ curl dejagnu subversion bison flex bc libcap? [Y/n]"
read installed
if [ "${installed:0:1}" == "n" ] || [ "${installed:0:1}" == "N" ]
then
	echo "You must install them"
	echo "For Ubuntu: sudo apt-get install g++ curl dejagnu subversion bison flex bc libcap-dev"
	echo "For Fedora: sudo yum install g++ curl dejagnu subversion bison flex bc libcap-devel"
	echo "(good luck for other OS's)"
	exit 1
fi

#handling weird export
if [ -d "/usr/include/x86_64-linux-gnu" ]
then
	export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
	export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
fi
}


# getting llvm-gcc
function get_llvm_gcc() {
if [ ! -f 'llvm-gcc4.2-2.9-x86_64-linux.tar.bz2' ]
then
	wget 'http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2'
fi
if [ ! -d "llvm-gcc4.2-2.9-x86_64-linux" ]
then
	tar xvfj llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
fi
BIN_PATH="$(pwd)""/llvm-gcc4.2-2.9-x86_64-linux/bin"
export PATH="$PATH:$BIN_PATH"

#verify llvm-gcc is on the path
which llvm-gcc 2>&1 || exitmsg 'llvm-gcc is not on the path! failed to get llvm-gcc?'
}

function print_llvm_patch() {
cat <<EOF
diff -u -r llvm-2.9/lib/ExecutionEngine/JIT/Intercept.cpp
src/lib/ExecutionEngine/JIT/Intercept.cpp
--- llvm-2.9/lib/ExecutionEngine/JIT/Intercept.cpp 2010-11-29
18:16:10.000000000 +0000
+++ src/lib/ExecutionEngine/JIT/Intercept.cpp 2013-09-27
12:11:02.464085889 +0100
@@ -50,6 +50,7 @@
 #if defined(__linux__)
 #if defined(HAVE_SYS_STAT_H)
 #include <sys/stat.h>
+#include <unistd.h>
 #endif
 #include <fcntl.h>
 /* stat functions are redirecting to __xstat with a version number.  On x86-64
EOF
}

#build llvm 2.9
function get_llvm_2_9(){

if [ ! -f 'llvm-2.9.tgz' ]
then
	wget 'http://llvm.org/releases/2.9/llvm-2.9.tgz'
fi

if [ ! -d 'llvm-2.9' ]
then
	tar zxvf llvm-2.9.tgz
fi

cd llvm-2.9

#fix via patch from mailing list
if print_llvm_patch | patch --dry-run -p1 -f
then
	print_llvm_patch | patch -p1
fi

./configure --enable-optimized --enable-assertions

make || exitmsg "Failed to build llvm 2.9"
cd ..
}

function print_stp_r940_patch(){
# with cvc.y to CVC.y rename
cat <<EOF
diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index eaff116..350618f 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -22,7 +22,6 @@
 #define YYMAXDEPTH 1048576000
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
-#define YYPARSE_PARAM AssertsQuery

   extern int cvclex(void);
   extern char* yytext;
@@ -32,9 +31,12 @@
     FatalError("");
     return YY_EXIT_FAILURE;
   };
+  int yyerror(void* AssertsQuery, const char* s) { return yyerror(s); }

   %}

+%parse-param {void* AssertsQuery}
+
 %union {

   unsigned int uintval;                 /* for numerals in types. */
diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index 2ac01e3..e7b0ea7 100644
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -54,15 +54,17 @@
     FatalError("");
     return 1;
   }
+  int yyerror(void* AssertsQuery, const char* s) { return yyerror(s); }

   ASTNode query;
 #define YYLTYPE_IS_TRIVIAL 1
 #define YYMAXDEPTH 104857600
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
-#define YYPARSE_PARAM AssertsQuery
   %}

+%parse-param {void* AssertsQuery}
+
 %union {
   // FIXME: Why is this not an UNSIGNED int?
   int uintval;                  /* for numerals in types. */
diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index a94bd6c..5263bf5 100644
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -64,6 +64,7 @@
     FatalError("");
     return 1;
   }
+  int yyerror(void* AssertsQuery, const char* s) { return yyerror(s); }

   ASTNode querysmt2;
   ASTVec assertionsSMT2;
@@ -72,9 +73,10 @@
 #define YYMAXDEPTH 104857600
 #define YYERROR_VERBOSE 1
 #define YY_EXIT_FAILURE -1
-#define YYPARSE_PARAM AssertsQuery
   %}

+%parse-param {void* AssertsQuery}
+
 %union {
   unsigned uintval;                  /* for numerals in types. */
   //ASTNode,ASTVec
EOF
}

#build stp
function get_stp() {
	get_stp_modified_wiki_way
}

function get_stp_wiki_way() {
if [ ! -f 'stp-r940.tgz' ]
then
wget 'http://www.doc.ic.ac.uk/~cristic/klee/stp-r940.tgz'
fi
tar xzfv stp-r940.tgz
cd stp-r940
./scripts/configure --with-prefix=`pwd`/install --with-cryptominisat2
make OPTIMIZE=-O2 CFLAGS_M32= install || exitmsg "Failed to build stp"
cd ..
}

function get_stp_trunk() {
echo "Warning: needs minisat!"
if [ ! -d 'stp' ]
then
git clone 'https://github.com/stp/stp.git'
fi
cd stp
mkdir -p install

cd install
cmake -G 'Unix Makefiles' ../
make || exitmsg "Failed to build stp"

cd ..
cd ..
}

function get_stp_modified_wiki_way() {
if [ ! -f 'stp-r940.tgz' ]
then
wget 'http://www.doc.ic.ac.uk/~cristic/klee/stp-r940.tgz'
fi
tar xzfv stp-r940.tgz
cd stp-r940
#fix via patch from mailing list, and git
if print_stp_r940_patch | patch --dry-run -p1 -f --verbose --ignore-whitespace
then
	print_stp_r940_patch | patch -p1 --ignore-whitespace
fi
./scripts/configure --with-prefix=`pwd`/install --with-cryptominisat2
make OPTIMIZE=-O2 CFLAGS_M32= install || exitmsg "Failed to build stp"
cd ..
}


# should run ulimit -s unlimited before running klee

# posix environment
function get_posix_env_for_klee(){
which llvm-gcc 2>&1 || exitmsg 'llvm-gcc is not on the path! failed to get llvm-gcc?'

if [ ! -d 'klee-uclibc' ]
then
git clone --depth 1 https://github.com/klee/klee-uclibc.git
fi
cd klee-uclibc
./configure --make-llvm-lib --with--lvm-config "$SCRIPT_DIR""/tmp/llvm-2.9/Release+Asserts/bin/llvm-config"
make -j2  || exitmsg "Failed to build posix/uclibc env" #why 2?
cd ..
}

#get klee
function get_klee(){
#verify llvm-gcc is on the path
which llvm-gcc 2>&1 || exitmsg 'llvm-gcc is not on the path! failed to get llvm-gcc?'
if [ ! -d "$SCRIPT_DIR""/llvm-2.9" ] || [ ! -d "$SCRIPT_DIR""/stp-r940/install" ]
then
	echo "$SCRIPT_DIR"
	echo "Failed to find either llvm 2.9 or stp in known path!"
	exit 1
fi

if [ ! -d 'klee' ]
then
	git clone https://github.com/klee/klee.git
fi
cd klee
if [ -d "../klee-uclibc" ]
then
	if [ ! -d "$SCRIPT_DIR""/klee-uclibc" ]
	then
		echo "Failed to find either uclibc  in known path!"
		exit 1
	fi
	./configure --with-llvm="$SCRIPT_DIR""/llvm-2.9" --with-stp="$SCRIPT_DIR""/stp-r940/install" \
		--with-uclibc="$SCRIPT_DIR""/klee-uclibc" --enable-posix-runtime
else
	./configure --with-llvm="$SCRIPT_DIR""/llvm-2.9" --with-stp="$SCRIPT_DIR""/stp-r940/install"
fi
make ENABLE_OPTIMIZED=1 || exitmsg "Failed to build klee"
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$SCRIPT_DIR/stp/install/lib"
make check || exitmsg "Failed to build klee"
make unittests || exitmsg "Failed to build klee"
}

main