Makefile.common

# Makefile to build and run the examples using KLEE.
#
# Copyright 2015 National University of Singapore


# In the following, please select where klee is located in your system
KLEE=klee
#KLEE=${HOME}/git/memdepend/klee/Release+Asserts/bin/klee

# In the following, please select suitable include directory
CFLAGS=-emit-llvm -g -I/usr/local/lib/tracerx/include
#CFLAGS=-emit-llvm -g -I${HOME}/nus/kleetest
#CFLAGS=-emit-llvm -g -I${HOME}/software/klee/include

CC=clang
AS=${CC} -S -emit-llvm
KLEE_FLAGS=${EXTRA_OPTIONS} -search=dfs

INPUT_TARGETS=$(subst .klee,.inputs,${TARGETS})
IR_TARGETS=$(subst .klee,.s,${TARGETS})
STPKLEE_TARGETS=$(subst .klee,.stpklee,${TARGETS})

all: all-ir ${INPUT_TARGETS}

all-ir: ${IR_TARGETS}

clean:
	rm -f klee-last *.o *.s *.ll *~ *.inputs core 
	rm -rf ${TARGETS} ${STPKLEE_TARGETS}

# To prevent the removal of *.klee subdirectories
.PRECIOUS: %.klee

.SUFFIXES: .klee .stpklee .inputs

# For running KLEE with Z3 and interpolation
.o.klee:
	time ${KLEE} ${KLEE_FLAGS} -output-dir=$@ $<
	opt -analyze -dot-cfg $<
	mv *.dot $@
	# Create PDFs from *.dot files
	for DOTFILE in $@/*.dot ; do \
		PDFFILE=`echo -n $$DOTFILE | sed -e s/\.dot/\.pdf/ -` ; \
		dot -Tpdf $$DOTFILE -o $$PDFFILE ; \
	done

# For running KLEE with STP without interpolation
.o.stpklee:
	time ${KLEE} ${KLEE_FLAGS} -select-solver=stp -output-dir=$@ $<
	opt -analyze -dot-cfg $<
	mv *.dot $@
	# Create PDFs from .dot files
	for DOTFILE in $@/*.dot ; do \
		PDFFILE=`echo -n $$DOTFILE | sed -e s/\.dot/\.pdf/ -` ; \
		dot -Tpdf $$DOTFILE -o $$PDFFILE ; \
	done

.klee.inputs:
	for KTEST in $</*.ktest ; do \
		( ( ktest-tool --write-ints $$KTEST ) >> $@ ) ; \
	done

.c.s:
	${AS} $<
	if [ -e $(subst .s,.ll,$@) ] ; then \
		mv $(subst .s,.ll,$@) $@ ; \
	fi