diff options
80 files changed, 3557 insertions, 662 deletions
diff --git a/.gitignore b/.gitignore index f421d69f..fb468a14 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ Release/ Release+Asserts/ Debug/ Debug+Asserts/ +Output/ cscope.* @@ -14,3 +15,4 @@ cscope.* *.cfg config.h +site.exp diff --git a/Makefile.common b/Makefile.common index bf99b1f3..3f60bbec 100644 --- a/Makefile.common +++ b/Makefile.common @@ -16,6 +16,7 @@ override ENABLE_OPTIMIZED := $(RUNTIME_ENABLE_OPTIMIZED) override DISABLE_ASSERTIONS := $(RUNTIME_DISABLE_ASSERTIONS) override ENABLE_PROFILING := $(RUNTIME_ENABLE_PROFILING) override ENABLE_COVERAGE := $(RUNTIME_ENABLE_COVERAGE) +override DEBUG_SYMBOLS := $(RUNTIME_DEBUG_SYMBOLS) endif include $(PROJ_SRC_ROOT)/Makefile.rules @@ -35,3 +36,13 @@ CXX.Flags += -DKLEE_DIR=\"$(PROJ_OBJ_ROOT)\" -DKLEE_LIB_DIR=\"$(PROJ_libdir)\" # For STP. CXX.Flags += -DEXT_HASH_MAP + +# For metaSMT +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + CXX.Flags += $(metaSMT_INCLUDES) +endif + diff --git a/Makefile.config.in b/Makefile.config.in index c916a456..452cc1a1 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -11,6 +11,9 @@ LLVM_SRC_ROOT = @LLVM_SRC@ # (this is *not* the same as OBJ_ROOT as defined in LLVM's Makefile.config). LLVM_OBJ_ROOT = @LLVM_OBJ@ +LLVM_VERSION_MAJOR = @LLVM_VERSION_MAJOR@ +LLVM_VERSION_MINOR = @LLVM_VERSION_MINOR@ + # Set this to the build mode used to build LLVM (not necessarily the same # as the build mode used for KLEE) LLVM_BUILD_MODE = @LLVM_BUILD_MODE@ @@ -26,6 +29,9 @@ PROJ_INSTALL_ROOT := @prefix@ STP_ROOT := @STP_ROOT@ +ENABLE_METASMT := @ENABLE_METASMT@ +METASMT_ROOT := @METASMT_ROOT@ + ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@ ENABLE_STPLOG := @ENABLE_STPLOG@ ENABLE_UCLIBC := @ENABLE_UCLIBC@ @@ -34,9 +40,14 @@ HAVE_SELINUX := @HAVE_SELINUX@ RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@ RUNTIME_DISABLE_ASSERTIONS := @RUNTIME_DISABLE_ASSERTIONS@ +RUNTIME_DEBUG_SYMBOLS := @RUNTIME_DEBUG_SYMBOLS@ RUNTIME_ENABLE_COVERAGE := RUNTIME_ENABLE_PROFILING := +# Compilers used to build runtime library and run tests +KLEE_BITCODE_C_COMPILER := @KLEE_BITCODE_C_COMPILER@ +KLEE_BITCODE_CXX_COMPILER := @KLEE_BITCODE_CXX_COMPILER@ + # A list of "features" which tests can check for in XFAIL: TEST_FEATURE_LIST := @@ -46,9 +57,12 @@ else TEST_FEATURE_LIST += no-selinux endif -CFLAGS := @CFLAGS@ -CXXFLAGS := @CXXFLAGS@ -LDFLAGS := @LDFLAGS@ +# disable unwind test +TEST_FEATURE_LIST += no-unwind + +CFLAGS := @CFLAGS@ -Wall -g +CXXFLAGS := @CXXFLAGS@ -g -Wall +LDFLAGS := @LDFLAGS@ -g REQUIRES_RTTI := @REQUIRES_RTTI@ RUNTEST := @RUNTEST@ diff --git a/Makefile.rules b/Makefile.rules index ef72c06c..5e954adf 100644 --- a/Makefile.rules +++ b/Makefile.rules @@ -433,24 +433,9 @@ endif # LLVM Capable Compiler #-------------------------------------------------------------------- -ifeq ($(LLVMCC_OPTION),llvm-gcc) - LLVMCC := $(LLVMGCC) - LLVMCXX := $(LLVMGXX) -else - ifeq ($(LLVMCC_OPTION),clang) - ifneq ($(CLANGPATH),) - LLVMCC := $(CLANGPATH) - LLVMCXX := $(CLANGXXPATH) - else - ifeq ($(ENABLE_BUILT_CLANG),1) - LLVMCC := $(LLVMToolDir)/clang - LLVMCXX := $(LLVMToolDir)/clang++ - endif - endif - else - LLVMCC := $(LLVMGCC) - LLVMCXX := $(LLVMGXX) - endif +# Use detected compiler at KLEE configure time, not llvm configure time +LLVMCC := $(KLEE_BITCODE_C_COMPILER) +LLVMCXX := $(KLEE_BITCODE_CXX_COMPILER) ifeq ($(wildcard $(LLVMCC)),) $(warning Provided Compiler "$(LLVMCC)" is not found. Provide full path!) @@ -458,7 +443,6 @@ else ifeq ($(wildcard $(LLVMCXX)),) $(warning Provided Compiler "$(LLVMCXX)" is not found. Provide full path!) endif -endif #-------------------------------------------------------------------- # Full Paths To Compiled Tools and Utilities @@ -692,7 +676,7 @@ TableGen = $(TBLGEN) -I $(call SYSPATH, $(PROJ_SRC_DIR)) \ -I $(call SYSPATH, $(PROJ_SRC_ROOT)/lib/Target) Archive = $(AR) $(AR.Flags) -LArchive = $(LLVMToolDir)/llvm-ar rcsf +LArchive = $(LLVMToolDir)/llvm-link ifdef RANLIB Ranlib = $(RANLIB) else @@ -1192,13 +1176,13 @@ $(LibName.BCA): $(ObjectsBC) $(LibDir)/.dir $(LLVMLD) \ "(internalize)" $(Verb) $(BCLinkLib) -o $(ObjDir)/$(LIBRARYNAME).internalize $(ObjectsBC) $(Verb) $(RM) -f $@ - $(Verb) $(LArchive) $@ $(ObjDir)/$(LIBRARYNAME).internalize.bc + $(Verb) $(LArchive) -o $@ $(ObjDir)/$(LIBRARYNAME).internalize.bc else $(LibName.BCA): $(ObjectsBC) $(LibDir)/.dir \ $(LLVMToolDir)/llvm-ar $(Echo) Building $(BuildMode) Bytecode Archive $(notdir $@) $(Verb) $(RM) -f $@ - $(Verb) $(LArchive) $@ $(ObjectsBC) + $(Verb) $(LArchive) -o $@ $(ObjectsBC) endif diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 82574314..4bd79557 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -181,6 +181,163 @@ AC_MSG_RESULT([$llvm_build_mode]) AC_SUBST(LLVM_BUILD_MODE,$llvm_build_mode) dnl ************************************************************************** +dnl Detect a LLVM Bitcode compiler for building KLEE runtime library + +dnl Check for clang built with llvm build +AC_MSG_CHECKING([LLVM Bitcode compiler]) +klee_llvm_bc_c_compiler="" +klee_llvm_bc_cxx_compiler="" + +AC_ARG_WITH([llvmcc], + AS_HELP_STRING([--with-llvmcc], + [Set the path to the C LLVM bitcode compiler to use (Default: auto-detect). If set, --with-llvmcxx= must be set too.] + ), + [], + [with_llvmcc=none] + ) + +AC_ARG_WITH([llvmcxx], + AS_HELP_STRING([--with-llvmcxx], + [Set the path to the C++ LLVM bitcode compiler to use (Default: auto-detect). If set, --with-llvmcc= must be set too.] + ), + [], + [with_llvmcxx=none] + ) +if test \( "X$with_llvmcc" != Xnone -a "X$with_llvmcxx" = Xnone \) -o \( "X$with_llvmcxx" != Xnone -a "X$with_llvmcc" = Xnone \) ; then + AC_MSG_ERROR([You must set both --with-llvmcc= and --with-llvmcxx= or set neither]) +fi + +if test X$with_llvmcc = Xnone ; then + dnl Try to automatically find compiler + + dnl Try Clang inside the LLVM build + if test -x "$llvm_obj/$llvm_build_mode/bin/clang" ; then + AC_MSG_RESULT([Found clang in LLVM Build]) + klee_llvm_bc_c_compiler="$llvm_obj/$llvm_build_mode/bin/clang" + + if test -x "$llvm_obj/$llvm_build_mode/bin/clang++" ; then + klee_llvm_bc_cxx_compiler="$llvm_obj/$llvm_build_mode/bin/clang++" + else + AC_MSG_ERROR([Found clang but could not find clang++]) + fi + fi + + dnl Try llvm-gcc in PATH + if test "X${klee_llvm_bc_c_compiler}" = X ; then + AC_MSG_RESULT([]) # Force a new line + AC_CHECK_PROG(llvm_gcc,llvm-gcc,FOUND,NOT_FOUND) + if test ${llvm_gcc} = FOUND ; then + klee_llvm_bc_c_compiler=`which llvm-gcc` + + AC_CHECK_PROG(llvm_gxx,llvm-g++,FOUND,NOT_FOUND) + if test ${llvm_gxx} = FOUND; then + klee_llvm_bc_cxx_compiler=`which llvm-g++` + else + AC_MSG_ERROR([Found llvm-gcc but could not find llvm-g++ in PATH]) + fi + fi + + fi + + dnl Try clang in PATH + if test "X${klee_llvm_bc_c_compiler}" = X ; then + AC_MSG_RESULT([]) # Force a new line + AC_CHECK_PROG(clang,clang,FOUND,NOT_FOUND) + if test ${clang} = FOUND ; then + klee_llvm_bc_c_compiler=`which clang` + + AC_CHECK_PROG(clang_cxx,clang++,FOUND,NOT_FOUND) + if test ${clang_cxx} = FOUND; then + klee_llvm_bc_cxx_compiler=`which clang++` + else + AC_MSG_ERROR([Found clang but could not find clang++ in PATH]) + fi + fi + + fi + + if test X"${klee_llvm_bc_c_compiler}" = X ; then + AC_MSG_ERROR([Could not find a C LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?]) + fi + + if test X"${klee_llvm_bc_cxx_compiler}" = X ; then + AC_MSG_ERROR([Could not find a C++ LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?]) + fi + +else + dnl Use user supplied values + klee_llvm_bc_c_compiler="$with_llvmcc" + klee_llvm_bc_cxx_compiler="$with_llvmcxx" + + if test \! -x "${klee_llvm_bc_c_compiler}"; then + AC_MSG_ERROR([--with-llvmcc= supplied compiler does not exist]) + fi + + if test \! -x "${klee_llvm_bc_cxx_compiler}"; then + AC_MSG_ERROR([--with-llvmcxx= supplied compiler does not exist]) + fi + AC_MSG_RESULT([Using user supplied LLVM bitcode compilers.]) +fi + +dnl Tell the user what we are going to try and use +AC_MSG_RESULT([Using C llvm compiler : $klee_llvm_bc_c_compiler]) +AC_MSG_RESULT([Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler]) + +dnl Test that the bitcode compiler works + +dnl Function for checking bitcode compiler works +dnl $1 : compiler to invoke +dnl $2 : source code extension (e.g. cpp or c) +dnl $3 : Compiler string (e.g. CXX or C) +function klee_check_bc() +{ + AC_MSG_CHECKING([${3} LLVM Bitcode compiler works]) + dnl FIXME: write to tmp directory instead of binary build dir + klee_bc_test_file="./.klee_llvm_bitcode_test.${2}" + + echo "int main() { return 0;}" > "${klee_bc_test_file}" + "${1}" -emit-llvm -c "${klee_bc_test_file}" -o "${klee_bc_test_file}.bc" + if test $? -ne 0 ; then + AC_MSG_ERROR([Failed running ${3} LLVM Bitcode compiler]) + fi + + if test \! -e "${klee_bc_test_file}.bc"; then + AC_MSG_ERROR([ ${3} LLVM Bitcode compiler did not produce any output]) + fi + + dnl Convert bitcode to human readable form as a hacky check + dnl that the version of LLVM we are configuring with can + dnl parse the LLVM bitcode produced by the detected compiler + if test -x "$llvm_obj/$llvm_build_mode/bin/llvm-dis" ; then + "$llvm_obj/$llvm_build_mode/bin/llvm-dis" -o "${klee_bc_test_file}.ll" "${klee_bc_test_file}.bc" + + if test $? -ne 0; then + AC_MSG_ERROR([Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?]) + fi + + if test -e "${klee_bc_test_file}.ll" ; then + AC_MSG_RESULT([Success]) + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" + else + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" + AC_MSG_ERROR([Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?]) + fi + + else + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" + AC_MSG_ERROR([Could not find llvm-dis]) + fi +} + +dnl Invoke previously defined function to check the LLVM bitcode compilers +klee_check_bc "${klee_llvm_bc_c_compiler}" "c" "C" +klee_check_bc "${klee_llvm_bc_cxx_compiler}" "cpp" "CXX" + +dnl Set variable for Makefile.config +AC_SUBST(KLEE_BITCODE_C_COMPILER,$klee_llvm_bc_c_compiler) +AC_SUBST(KLEE_BITCODE_CXX_COMPILER,$klee_llvm_bc_cxx_compiler) + +dnl ************************************************************************** dnl User option to enable uClibc support. AC_ARG_WITH(uclibc, @@ -269,18 +426,22 @@ if test X${with_runtime} = XRelease; then AC_MSG_RESULT([Release]) AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]]) AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[1]]) + AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[]]) elif test X${with_runtime} = XRelease+Asserts; then AC_MSG_RESULT([Release+Asserts]) AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]]) AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[0]]) + AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[]]) elif test X${with_runtime} = XDebug; then AC_MSG_RESULT([Debug]) AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]]) AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[1]]) + AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[1]]) elif test X${with_runtime} = XDebug+Asserts; then AC_MSG_RESULT([Debug+Asserts]) AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]]) AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[0]]) + AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[1]]) else AC_MSG_ERROR([invalid configuration: ${with_runtime}]) fi @@ -357,6 +518,40 @@ else fi dnl ************************************************************************** +dnl User option to enable metaSMT constraint solvers and to specify the +dnl the location of the metaSMT root directory +dnl ************************************************************************** + +AC_ARG_WITH(metasmt, + AS_HELP_STRING([--with-metasmt], + [Location of metaSMT installation directory]),,) + +if test X$with_metasmt = X ; then + AC_SUBST(ENABLE_METASMT,[[0]]) +else + metasmt_root=`cd $with_metasmt 2> /dev/null; pwd` + + dnl AC_LANG(C++) + old_CPPFLAGS="$CPPFLAGS" + old_LDFLAGS="$LDFLAGS" + CPPFLAGS="$CPPFLAGS -I$metasmt_root/include" + LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT" + AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [ + AC_MSG_ERROR([Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header]) + ]) + AC_LINK_IFELSE( + [AC_LANG_PROGRAM([#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp], [metaSMT::logic::QF_BV::new_bitvector(3)])], + [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])]) + CPPFLAGS="$old_CPPFLAGS" + LDFLAGS="$old_LDFLAGS" + + AC_DEFINE(SUPPORT_METASMT, 1, [Supporting metaSMT API]) + AC_SUBST(ENABLE_METASMT,[[1]]) + AC_SUBST(METASMT_ROOT,$metasmt_root) + AC_SUBST(REQUIRES_RTTI,[[1]]) +fi + +dnl ************************************************************************** dnl * Check for dejagnu dnl ************************************************************************** AC_PATH_PROG(RUNTEST, [runtest]) diff --git a/configure b/configure index 19332245..ab148c2c 100755 --- a/configure +++ b/configure @@ -625,6 +625,8 @@ ac_includes_default="\ ac_subst_vars='LTLIBOBJS LIBOBJS RUNTEST +METASMT_ROOT +ENABLE_METASMT STP_ROOT CXXCPP ac_ct_CXX @@ -642,11 +644,18 @@ LDFLAGS CFLAGS CC RUNTIME_CONFIGURATION +RUNTIME_DEBUG_SYMBOLS RUNTIME_DISABLE_ASSERTIONS RUNTIME_ENABLE_OPTIMIZED ENABLE_POSIX_RUNTIME ENABLE_UCLIBC KLEE_UCLIBC +KLEE_BITCODE_CXX_COMPILER +KLEE_BITCODE_C_COMPILER +clang_cxx +clang +llvm_gxx +llvm_gcc LLVM_BUILD_MODE REQUIRES_RTTI LLVM_IS_RELEASE @@ -711,10 +720,13 @@ with_llvmsrc with_llvmobj with_llvm with_llvm_build_mode +with_llvmcc +with_llvmcxx with_uclibc enable_posix_runtime with_runtime with_stp +with_metasmt ' ac_precious_vars='build_alias host_alias @@ -1353,10 +1365,17 @@ Optional Packages: --with-llvm Location of LLVM Source and Object code --with-llvm-build-mode LLVM build mode (e.g. Debug or Release, default autodetect) + --with-llvmcc Set the path to the C LLVM bitcode compiler to use + (Default: auto-detect). If set, --with-llvmcxx= must + be set too. + --with-llvmcxx Set the path to the C++ LLVM bitcode compiler to use + (Default: auto-detect). If set, --with-llvmcc= must + be set too. --with-uclibc Enable use of the klee uclibc at the given path --with-runtime Select build configuration for runtime libraries (default [Release+Asserts]) --with-stp Location of STP installation directory + --with-metasmt Location of metaSMT installation directory Some influential environment variables: CC C compiler command @@ -2662,6 +2681,306 @@ LLVM_BUILD_MODE=$llvm_build_mode +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking LLVM Bitcode compiler" >&5 +$as_echo_n "checking LLVM Bitcode compiler... " >&6; } +klee_llvm_bc_c_compiler="" +klee_llvm_bc_cxx_compiler="" + + +# Check whether --with-llvmcc was given. +if test "${with_llvmcc+set}" = set; then : + withval=$with_llvmcc; +else + with_llvmcc=none + +fi + + + +# Check whether --with-llvmcxx was given. +if test "${with_llvmcxx+set}" = set; then : + withval=$with_llvmcxx; +else + with_llvmcxx=none + +fi + +if test \( "X$with_llvmcc" != Xnone -a "X$with_llvmcxx" = Xnone \) -o \( "X$with_llvmcxx" != Xnone -a "X$with_llvmcc" = Xnone \) ; then + as_fn_error $? "You must set both --with-llvmcc= and --with-llvmcxx= or set neither" "$LINENO" 5 +fi + +if test X$with_llvmcc = Xnone ; then + + if test -x "$llvm_obj/$llvm_build_mode/bin/clang" ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Found clang in LLVM Build" >&5 +$as_echo "Found clang in LLVM Build" >&6; } + klee_llvm_bc_c_compiler="$llvm_obj/$llvm_build_mode/bin/clang" + + if test -x "$llvm_obj/$llvm_build_mode/bin/clang++" ; then + klee_llvm_bc_cxx_compiler="$llvm_obj/$llvm_build_mode/bin/clang++" + else + as_fn_error $? "Found clang but could not find clang++" "$LINENO" 5 + fi + fi + + if test "X${klee_llvm_bc_c_compiler}" = X ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: " >&5 +$as_echo "" >&6; } # Force a new line + # Extract the first word of "llvm-gcc", so it can be a program name with args. +set dummy llvm-gcc; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_llvm_gcc+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$llvm_gcc"; then + ac_cv_prog_llvm_gcc="$llvm_gcc" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_llvm_gcc="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_llvm_gcc" && ac_cv_prog_llvm_gcc="NOT_FOUND" +fi +fi +llvm_gcc=$ac_cv_prog_llvm_gcc +if test -n "$llvm_gcc"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $llvm_gcc" >&5 +$as_echo "$llvm_gcc" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${llvm_gcc} = FOUND ; then + klee_llvm_bc_c_compiler=`which llvm-gcc` + + # Extract the first word of "llvm-g++", so it can be a program name with args. +set dummy llvm-g++; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_llvm_gxx+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$llvm_gxx"; then + ac_cv_prog_llvm_gxx="$llvm_gxx" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_llvm_gxx="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_llvm_gxx" && ac_cv_prog_llvm_gxx="NOT_FOUND" +fi +fi +llvm_gxx=$ac_cv_prog_llvm_gxx +if test -n "$llvm_gxx"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $llvm_gxx" >&5 +$as_echo "$llvm_gxx" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${llvm_gxx} = FOUND; then + klee_llvm_bc_cxx_compiler=`which llvm-g++` + else + as_fn_error $? "Found llvm-gcc but could not find llvm-g++ in PATH" "$LINENO" 5 + fi + fi + + fi + + if test "X${klee_llvm_bc_c_compiler}" = X ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: " >&5 +$as_echo "" >&6; } # Force a new line + # Extract the first word of "clang", so it can be a program name with args. +set dummy clang; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_clang+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$clang"; then + ac_cv_prog_clang="$clang" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_clang="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_clang" && ac_cv_prog_clang="NOT_FOUND" +fi +fi +clang=$ac_cv_prog_clang +if test -n "$clang"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $clang" >&5 +$as_echo "$clang" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${clang} = FOUND ; then + klee_llvm_bc_c_compiler=`which clang` + + # Extract the first word of "clang++", so it can be a program name with args. +set dummy clang++; ac_word=$2 +{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 +$as_echo_n "checking for $ac_word... " >&6; } +if ${ac_cv_prog_clang_cxx+:} false; then : + $as_echo_n "(cached) " >&6 +else + if test -n "$clang_cxx"; then + ac_cv_prog_clang_cxx="$clang_cxx" # Let the user override the test. +else +as_save_IFS=$IFS; IFS=$PATH_SEPARATOR +for as_dir in $PATH +do + IFS=$as_save_IFS + test -z "$as_dir" && as_dir=. + for ac_exec_ext in '' $ac_executable_extensions; do + if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then + ac_cv_prog_clang_cxx="FOUND" + $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5 + break 2 + fi +done + done +IFS=$as_save_IFS + + test -z "$ac_cv_prog_clang_cxx" && ac_cv_prog_clang_cxx="NOT_FOUND" +fi +fi +clang_cxx=$ac_cv_prog_clang_cxx +if test -n "$clang_cxx"; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: $clang_cxx" >&5 +$as_echo "$clang_cxx" >&6; } +else + { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5 +$as_echo "no" >&6; } +fi + + + if test ${clang_cxx} = FOUND; then + klee_llvm_bc_cxx_compiler=`which clang++` + else + as_fn_error $? "Found clang but could not find clang++ in PATH" "$LINENO" 5 + fi + fi + + fi + + if test X"${klee_llvm_bc_c_compiler}" = X ; then + as_fn_error $? "Could not find a C LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?" "$LINENO" 5 + fi + + if test X"${klee_llvm_bc_cxx_compiler}" = X ; then + as_fn_error $? "Could not find a C++ LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?" "$LINENO" 5 + fi + +else + klee_llvm_bc_c_compiler="$with_llvmcc" + klee_llvm_bc_cxx_compiler="$with_llvmcxx" + + if test \! -x "${klee_llvm_bc_c_compiler}"; then + as_fn_error $? "--with-llvmcc= supplied compiler does not exist" "$LINENO" 5 + fi + + if test \! -x "${klee_llvm_bc_cxx_compiler}"; then + as_fn_error $? "--with-llvmcxx= supplied compiler does not exist" "$LINENO" 5 + fi + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Using user supplied LLVM bitcode compilers." >&5 +$as_echo "Using user supplied LLVM bitcode compilers." >&6; } +fi + +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: Using C llvm compiler : $klee_llvm_bc_c_compiler" >&5 +$as_echo "Using C llvm compiler : $klee_llvm_bc_c_compiler" >&6; } +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler" >&5 +$as_echo "Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler" >&6; } + + +function klee_check_bc() +{ + { $as_echo "$as_me:${as_lineno-$LINENO}: checking ${3} LLVM Bitcode compiler works" >&5 +$as_echo_n "checking ${3} LLVM Bitcode compiler works... " >&6; } + klee_bc_test_file="./.klee_llvm_bitcode_test.${2}" + + echo "int main() { return 0;}" > "${klee_bc_test_file}" + "${1}" -emit-llvm -c "${klee_bc_test_file}" -o "${klee_bc_test_file}.bc" + if test $? -ne 0 ; then + as_fn_error $? "Failed running ${3} LLVM Bitcode compiler" "$LINENO" 5 + fi + + if test \! -e "${klee_bc_test_file}.bc"; then + as_fn_error $? " ${3} LLVM Bitcode compiler did not produce any output" "$LINENO" 5 + fi + + if test -x "$llvm_obj/$llvm_build_mode/bin/llvm-dis" ; then + "$llvm_obj/$llvm_build_mode/bin/llvm-dis" -o "${klee_bc_test_file}.ll" "${klee_bc_test_file}.bc" + + if test $? -ne 0; then + as_fn_error $? "Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?" "$LINENO" 5 + fi + + if test -e "${klee_bc_test_file}.ll" ; then + { $as_echo "$as_me:${as_lineno-$LINENO}: result: Success" >&5 +$as_echo "Success" >&6; } + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" + else + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll" + as_fn_error $? "Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?" "$LINENO" 5 + fi + + else + rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" + as_fn_error $? "Could not find llvm-dis" "$LINENO" 5 + fi +} + +klee_check_bc "${klee_llvm_bc_c_compiler}" "c" "C" +klee_check_bc "${klee_llvm_bc_cxx_compiler}" "cpp" "CXX" + +KLEE_BITCODE_C_COMPILER=$klee_llvm_bc_c_compiler + +KLEE_BITCODE_CXX_COMPILER=$klee_llvm_bc_cxx_compiler + + + # Check whether --with-uclibc was given. if test "${with_uclibc+set}" = set; then : @@ -2771,6 +3090,8 @@ $as_echo "Release" >&6; } RUNTIME_DISABLE_ASSERTIONS=1 + RUNTIME_DEBUG_SYMBOLS= + elif test X${with_runtime} = XRelease+Asserts; then { $as_echo "$as_me:${as_lineno-$LINENO}: result: Release+Asserts" >&5 $as_echo "Release+Asserts" >&6; } @@ -2778,6 +3099,8 @@ $as_echo "Release+Asserts" >&6; } RUNTIME_DISABLE_ASSERTIONS=0 + RUNTIME_DEBUG_SYMBOLS= + elif test X${with_runtime} = XDebug; then { $as_echo "$as_me:${as_lineno-$LINENO}: result: Debug" >&5 $as_echo "Debug" >&6; } @@ -2785,6 +3108,8 @@ $as_echo "Debug" >&6; } RUNTIME_DISABLE_ASSERTIONS=1 + RUNTIME_DEBUG_SYMBOLS=1 + elif test X${with_runtime} = XDebug+Asserts; then { $as_echo "$as_me:${as_lineno-$LINENO}: result: Debug+Asserts" >&5 $as_echo "Debug+Asserts" >&6; } @@ -2792,6 +3117,8 @@ $as_echo "Debug+Asserts" >&6; } RUNTIME_DISABLE_ASSERTIONS=0 + RUNTIME_DEBUG_SYMBOLS=1 + else as_fn_error $? "invalid configuration: ${with_runtime}" "$LINENO" 5 fi @@ -4590,6 +4917,74 @@ fi fi + + +# Check whether --with-metasmt was given. +if test "${with_metasmt+set}" = set; then : + withval=$with_metasmt; +fi + + +if test X$with_metasmt = X ; then + ENABLE_METASMT=0 + +else + metasmt_root=`cd $with_metasmt 2> /dev/null; pwd` + + old_CPPFLAGS="$CPPFLAGS" + old_LDFLAGS="$LDFLAGS" + CPPFLAGS="$CPPFLAGS -I$metasmt_root/include" + LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT" + for ac_header in $metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp +do : + as_ac_Header=`$as_echo "ac_cv_header_$ac_header" | $as_tr_sh` +ac_fn_cxx_check_header_mongrel "$LINENO" "$ac_header" "$as_ac_Header" "$ac_includes_default" +if eval test \"x\$"$as_ac_Header"\" = x"yes"; then : + cat >>confdefs.h <<_ACEOF +#define `$as_echo "HAVE_$ac_header" | $as_tr_cpp` 1 +_ACEOF + +else + + as_fn_error $? "Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header" "$LINENO" 5 + +fi + +done + + cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ +#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp +int +main () +{ +metaSMT::logic::QF_BV::new_bitvector(3) + ; + return 0; +} +_ACEOF +if ac_fn_cxx_try_link "$LINENO"; then : + +else + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for new_bitvector() in -lmetaSMT" >&5 +$as_echo_n "checking for new_bitvector() in -lmetaSMT... " >&6; } +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext conftest.$ac_ext + CPPFLAGS="$old_CPPFLAGS" + LDFLAGS="$old_LDFLAGS" + + +$as_echo "#define SUPPORT_METASMT 1" >>confdefs.h + + ENABLE_METASMT=1 + + METASMT_ROOT=$metasmt_root + + REQUIRES_RTTI=1 + +fi + # Extract the first word of "runtest", so it can be a program name with args. set dummy runtest; ac_word=$2 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5 diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index 38b22c6f..c4c70069 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -7,6 +7,7 @@ #define KLEE_COMMANDLINE_H #include "llvm/Support/CommandLine.h" +#include "klee/Config/config.h" namespace klee { @@ -43,6 +44,19 @@ enum QueryLoggingSolverType */ extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions; +#ifdef SUPPORT_METASMT + +enum MetaSMTBackendType +{ + METASMT_BACKEND_NONE, + METASMT_BACKEND_STP, + METASMT_BACKEND_Z3, + METASMT_BACKEND_BOOLECTOR +}; + +extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT; + +#endif /* SUPPORT_METASMT */ //A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions template <typename T> diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 0f79e01d..0a94de8f 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -81,4 +81,7 @@ /* Define to 1 if you have the ANSI C header files. */ #undef STDC_HEADERS +/* Supporting metaSMT API */ +#undef SUPPORT_METASMT + #endif diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h index 20db560d..fc86070b 100644 --- a/include/klee/Internal/Module/KInstruction.h +++ b/include/klee/Internal/Module/KInstruction.h @@ -11,11 +11,7 @@ #define KLEE_KINSTRUCTION_H #include "klee/Config/Version.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) && LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/System/DataTypes.h" -#else #include "llvm/Support/DataTypes.h" -#endif #include <vector> namespace llvm { diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h index 1d305374..f1f16c5e 100644 --- a/include/klee/Internal/Support/FloatEvaluation.h +++ b/include/klee/Internal/Support/FloatEvaluation.h @@ -17,6 +17,8 @@ #include "llvm/Support/MathExtras.h" +#include <cassert> + namespace klee { namespace floats { diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index e29db411..e93284d6 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -51,11 +51,13 @@ public: std::string LibraryDir; bool Optimize; bool CheckDivZero; + bool CheckOvershift; ModuleOptions(const std::string& _LibraryDir, - bool _Optimize, bool _CheckDivZero) + bool _Optimize, bool _CheckDivZero, + bool _CheckOvershift) : LibraryDir(_LibraryDir), Optimize(_Optimize), - CheckDivZero(_CheckDivZero) {} + CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {} }; enum LogType diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 8fe33c7c..00e4c962 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -219,6 +219,21 @@ namespace klee { virtual void setCoreSolverTimeout(double timeout); }; + +#ifdef SUPPORT_METASMT + + template<typename SolverContext> + class MetaSMTSolver : public Solver { + public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query&); + virtual void setCoreSolverTimeout(double timeout); +}; + +#endif /* SUPPORT_METASMT */ + /* *** */ /// createValidatingSolver - Create a solver which will validate all query diff --git a/include/klee/Statistic.h b/include/klee/Statistic.h index 1e5b1c92..6b8fb165 100644 --- a/include/klee/Statistic.h +++ b/include/klee/Statistic.h @@ -11,11 +11,7 @@ #define KLEE_STATISTIC_H #include "klee/Config/Version.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) && LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/System/DataTypes.h" -#else #include "llvm/Support/DataTypes.h" -#endif #include <string> namespace klee { diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h index aa78e534..f228b289 100644 --- a/include/klee/util/Bits.h +++ b/include/klee/util/Bits.h @@ -11,11 +11,7 @@ #define KLEE_UTIL_BITS_H #include "klee/Config/Version.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) && LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/System/DataTypes.h" -#else #include "llvm/Support/DataTypes.h" -#endif namespace klee { namespace bits32 { diff --git a/include/klee/util/GetElementPtrTypeIterator.h b/include/klee/util/GetElementPtrTypeIterator.h index 4446914d..2d145cd6 100644 --- a/include/klee/util/GetElementPtrTypeIterator.h +++ b/include/klee/util/GetElementPtrTypeIterator.h @@ -18,15 +18,21 @@ #ifndef KLEE_UTIL_GETELEMENTPTRTYPE_H #define KLEE_UTIL_GETELEMENTPTRTYPE_H -#include "klee/Config/Version.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/User.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Constants.h" +#else #include "llvm/User.h" #include "llvm/DerivedTypes.h" #include "llvm/Instructions.h" -#include "klee/Config/Version.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) #include "llvm/Constants.h" #endif +#endif + +#include "klee/Config/Version.h" namespace klee { template<typename ItTy = llvm::User::const_op_iterator> diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index ac0474fb..eac54141 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,5 +73,22 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( llvm::cl::CommaSeparated ); +#ifdef SUPPORT_METASMT + +llvm::cl::opt<klee::MetaSMTBackendType> +UseMetaSMT("use-metasmt", + llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."), + llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"), + clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), + clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), + clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), + clEnumValEnd), + llvm::cl::init(METASMT_BACKEND_NONE)); + +#endif /* SUPPORT_METASMT */ + } + + + diff --git a/lib/Core/CallPathManager.cpp b/lib/Core/CallPathManager.cpp index ca127f25..03e75108 100644 --- a/lib/Core/CallPathManager.cpp +++ b/lib/Core/CallPathManager.cpp @@ -13,7 +13,12 @@ #include <map> #include <vector> +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else #include "llvm/Function.h" +#endif + #include "llvm/Support/raw_ostream.h" using namespace llvm; diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp index 979970aa..935e4316 100644 --- a/lib/Core/Context.cpp +++ b/lib/Core/Context.cpp @@ -11,8 +11,13 @@ #include "klee/Expr.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Type.h" +#include "llvm/IR/DerivedTypes.h" +#else #include "llvm/Type.h" #include "llvm/DerivedTypes.h" +#endif #include <cassert> diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index db685639..b2c2a737 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -17,8 +17,11 @@ #include "klee/Expr.h" #include "Memory.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else #include "llvm/Function.h" +#endif #include "llvm/Support/CommandLine.h" #include <iostream> diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 069022a2..ef55f21f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -24,6 +24,7 @@ #include "StatsTracker.h" #include "TimingSolver.h" #include "UserSearcher.h" +#include "ExecutorTimerInfo.h" #include "../Solver/SolverStats.h" #include "klee/ExecutionState.h" @@ -47,31 +48,40 @@ #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Attributes.h" +#include "llvm/IR/BasicBlock.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#include "llvm/IR/TypeBuilder.h" +#else #include "llvm/Attributes.h" #include "llvm/BasicBlock.h" #include "llvm/Constants.h" #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" +#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) +#include "llvm/Target/TargetData.h" +#else +#include "llvm/DataLayout.h" +#include "llvm/TypeBuilder.h" +#endif +#endif #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CallSite.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif -#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) -#include "llvm/Target/TargetData.h" -#else -#include "llvm/DataLayout.h" -#endif #include <cassert> #include <algorithm> @@ -90,6 +100,33 @@ using namespace llvm; using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + namespace { cl::opt<bool> DumpStatesOnHalt("dump-states-on-halt", @@ -253,7 +290,41 @@ Executor::Executor(const InterpreterOptions &opts, : std::max(MaxCoreSolverTime,MaxInstructionTime)) { if (coreSolverTimeout) UseForkedCoreSolver = true; - Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + + Solver *coreSolver = NULL; + +#ifdef SUPPORT_METASMT + if (UseMetaSMT != METASMT_BACKEND_NONE) { + + std::string backend; + + switch (UseMetaSMT) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + assert(false); + break; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + } +#else + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#endif /* SUPPORT_METASMT */ + + Solver *solver = constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), @@ -309,6 +380,10 @@ Executor::~Executor() { delete statsTracker; delete solver; delete kmodule; + while(!timers.empty()) { + delete timers.back(); + timers.pop_back(); + } } /***/ @@ -386,10 +461,10 @@ void Executor::initializeGlobals(ExecutionState &state) { if (m->getModuleInlineAsm() != "") klee_warning("executable has module level assembly (ignoring)"); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) assert(m->lib_begin() == m->lib_end() && "XXX do not support dependent libraries"); - +#endif // represent function globals using the address of the actual llvm function // object. given that we use malloc to allocate memory in states this also // ensures that we won't conflict. we don't need to allocate a memory object @@ -501,9 +576,17 @@ void Executor::initializeGlobals(ExecutionState &state) { uint64_t size = kmodule->targetData->getTypeStoreSize(ty); MemoryObject *mo = 0; +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) if (UseAsmAddresses && i->getName()[0]=='\01') { +#else + if (UseAsmAddresses && !i->getName().empty()) { +#endif char *end; +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) uint64_t address = ::strtoll(i->getName().str().c_str()+1, &end, 0); +#else + uint64_t address = ::strtoll(i->getName().str().c_str(), &end, 0); +#endif if (end && *end == '\0') { klee_message("NOTE: allocated global at asm specified address: %#08llx" @@ -557,20 +640,31 @@ void Executor::branch(ExecutionState &state, unsigned N = conditions.size(); assert(N); - stats::forks += N-1; + if (MaxForks!=~0u && stats::forks >= MaxForks) { + unsigned next = theRNG.getInt32() % N; + for (unsigned i=0; i<N; ++i) { + if (i == next) { + result.push_back(&state); + } else { + result.push_back(NULL); + } + } + } else { + stats::forks += N-1; - // XXX do proper balance or keep random? - result.push_back(&state); - for (unsigned i=1; i<N; ++i) { - ExecutionState *es = result[theRNG.getInt32() % i]; - ExecutionState *ns = es->branch(); - addedStates.insert(ns); - result.push_back(ns); - es->ptreeNode->data = 0; - std::pair<PTree::Node*,PTree::Node*> res = - processTree->split(es->ptreeNode, ns, es); - ns->ptreeNode = res.first; - es->ptreeNode = res.second; + // XXX do proper balance or keep random? + result.push_back(&state); + for (unsigned i=1; i<N; ++i) { + ExecutionState *es = result[theRNG.getInt32() % i]; + ExecutionState *ns = es->branch(); + addedStates.insert(ns); + result.push_back(ns); + es->ptreeNode->data = 0; + std::pair<PTree::Node*,PTree::Node*> res = + processTree->split(es->ptreeNode, ns, es); + ns->ptreeNode = res.first; + es->ptreeNode = res.second; + } } // If necessary redistribute seeds to match conditions, killing @@ -605,12 +699,14 @@ void Executor::branch(ExecutionState &state, if (i==N) i = theRNG.getInt32() % N; - seedMap[result[i]].push_back(*siit); + // Extra check in case we're replaying seeds with a max-fork + if (result[i]) + seedMap[result[i]].push_back(*siit); } if (OnlyReplaySeeds) { for (unsigned i=0; i<N; ++i) { - if (!seedMap.count(result[i])) { + if (result[i] && !seedMap.count(result[i])) { terminateState(*result[i]); result[i] = NULL; } @@ -1302,26 +1398,9 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { } } +/// TODO remove? static bool isDebugIntrinsic(const Function *f, KModule *KM) { -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - // Fast path, getIntrinsicID is slow. - if (f == KM->dbgStopPointFn) - return true; - - switch (f->getIntrinsicID()) { - case Intrinsic::dbg_stoppoint: - case Intrinsic::dbg_region_start: - case Intrinsic::dbg_region_end: - case Intrinsic::dbg_func_start: - case Intrinsic::dbg_declare: - return true; - - default: - return false; - } -#else return false; -#endif } static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) { @@ -1380,7 +1459,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { CallSite(cast<CallInst>(caller))); // XXX need to check other param attrs ? -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) bool isSExt = cs.paramHasAttr(0, llvm::Attributes::SExt); #else bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt); @@ -1584,7 +1665,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (from != to) { // XXX need to check other param attrs ? -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) bool isSExt = cs.paramHasAttr(i+1, llvm::Attributes::SExt); #else bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt); @@ -1867,14 +1950,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } // Memory instructions... -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - case Instruction::Malloc: - case Instruction::Alloca: { - AllocationInst *ai = cast<AllocationInst>(i); -#else case Instruction::Alloca: { AllocaInst *ai = cast<AllocaInst>(i); -#endif unsigned elementSize = kmodule->targetData->getTypeStoreSize(ai->getAllocatedType()); ref<Expr> size = Expr::createPointer(elementSize); @@ -1887,12 +1964,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { executeAlloc(state, size, isLocal, ki); break; } -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - case Instruction::Free: { - executeFree(state, eval(ki, 0, state).value); - break; - } -#endif case Instruction::Load: { ref<Expr> base = eval(ki, 0, state).value; @@ -1982,8 +2053,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FAdd operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.add(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -1996,9 +2072,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(left->getWidth()) || !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FSub operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.subtract(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2012,8 +2092,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FMul operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.multiply(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2027,8 +2112,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FDiv operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.divide(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2041,9 +2131,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(left->getWidth()) || !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FRem operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.remainder(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue())); +#else llvm::APFloat Res(left->getAPValue()); Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2056,7 +2150,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth()) return terminateStateOnExecError(state, "Unsupported FPTrunc operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Res(arg->getAPValue()); +#endif bool losesInfo = false; Res.convert(*fpWidthToSemantics(resultType), llvm::APFloat::rmNearestTiesToEven, @@ -2072,8 +2170,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType) return terminateStateOnExecError(state, "Unsupported FPExt operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Res(arg->getAPValue()); +#endif bool losesInfo = false; Res.convert(*fpWidthToSemantics(resultType), llvm::APFloat::rmNearestTiesToEven, @@ -2090,7 +2191,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToUI operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Arg(arg->getAPValue()); +#endif uint64_t value = 0; bool isExact = true; Arg.convertToInteger(&value, resultType, false, @@ -2106,8 +2211,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToSI operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Arg(arg->getAPValue()); + +#endif uint64_t value = 0; bool isExact = true; Arg.convertToInteger(&value, resultType, true, @@ -2158,8 +2267,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FCmp operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + APFloat LHS(*fpWidthToSemantics(left->getWidth()),left->getAPValue()); + APFloat RHS(*fpWidthToSemantics(right->getWidth()),right->getAPValue()); +#else APFloat LHS(left->getAPValue()); APFloat RHS(right->getAPValue()); +#endif APFloat::cmpResult CmpRes = LHS.compare(RHS); bool Result = false; @@ -2470,8 +2584,11 @@ void Executor::run(ExecutionState &initialState) { // We need to avoid calling GetMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + unsigned mbs = sys::Process::GetMallocUsage() >> 20; +#else unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20; - +#endif if (mbs > MaxMemory) { if (mbs > MaxMemory + 100) { // just guess at how many to kill diff --git a/lib/Core/ExecutorTimerInfo.h b/lib/Core/ExecutorTimerInfo.h new file mode 100644 index 00000000..60977b74 --- /dev/null +++ b/lib/Core/ExecutorTimerInfo.h @@ -0,0 +1,42 @@ +//===-- Executor.h ----------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// Class to wrap information for a timer. +// +//===----------------------------------------------------------------------===// + +#ifndef EXECUTORTIMERINFO_H_ +#define EXECUTORTIMERINFO_H_ + +#include "klee/Internal/System/Time.h" + +namespace klee { + +class Executor::TimerInfo { +public: + Timer *timer; + + /// Approximate delay per timer firing. + double rate; + /// Wall time for next firing. + double nextFireTime; + +public: + TimerInfo(Timer *_timer, double _rate) + : timer(_timer), + rate(_rate), + nextFireTime(util::getWallTime() + rate) {} + ~TimerInfo() { delete timer; } +}; + + +} + + +#endif /* EXECUTORTIMERINFO_H_ */ diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 2fda5cba..06fd4be7 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -13,6 +13,7 @@ #include "Executor.h" #include "PTree.h" #include "StatsTracker.h" +#include "ExecutorTimerInfo.h" #include "klee/ExecutionState.h" #include "klee/Internal/Module/InstructionInfoTable.h" @@ -20,7 +21,12 @@ #include "klee/Internal/Module/KModule.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else #include "llvm/Function.h" +#endif + #include "llvm/Support/CommandLine.h" #include <unistd.h> @@ -88,7 +94,7 @@ void Executor::initTimers() { } if (MaxTime) { - addTimer(new HaltTimer(this), MaxTime); + addTimer(new HaltTimer(this), MaxTime.getValue()); } } @@ -98,23 +104,6 @@ Executor::Timer::Timer() {} Executor::Timer::~Timer() {} -class Executor::TimerInfo { -public: - Timer *timer; - - /// Approximate delay per timer firing. - double rate; - /// Wall time for next firing. - double nextFireTime; - -public: - TimerInfo(Timer *_timer, double _rate) - : timer(_timer), - rate(_rate), - nextFireTime(util::getWallTime() + rate) {} - ~TimerInfo() { delete timer; } -}; - void Executor::addTimer(Timer *timer, double rate) { timers.push_back(new TimerInfo(timer, rate)); } diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 0d85afee..0d828ec4 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -20,19 +20,27 @@ #include "klee/util/GetElementPtrTypeIterator.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#else #include "llvm/Constants.h" #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -#include "llvm/ModuleProvider.h" -#endif -#include "llvm/Support/CallSite.h" #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif + +#include "llvm/Support/CallSite.h" + + #include <iostream> #include <cassert> diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 7da0c350..2dc16767 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -17,24 +17,23 @@ #undef PACKAGE_TARNAME #undef PACKAGE_VERSION +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Module.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/Module.h" #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Instructions.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -#include "llvm/ModuleProvider.h" -#endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif #include "llvm/ExecutionEngine/JIT.h" #include "llvm/ExecutionEngine/GenericValue.h" #include "llvm/Support/CallSite.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/DynamicLibrary.h" -#else #include "llvm/Support/DynamicLibrary.h" -#endif #include "llvm/Support/raw_ostream.h" #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0) #include "llvm/Target/TargetSelect.h" @@ -89,16 +88,9 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) { ExternalDispatcher::ExternalDispatcher() { dispatchModule = new Module("ExternalDispatcher", getGlobalContext()); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - ExistingModuleProvider* MP = new ExistingModuleProvider(dispatchModule); -#endif std::string error; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - executionEngine = ExecutionEngine::createJIT(MP, &error); -#else executionEngine = ExecutionEngine::createJIT(dispatchModule, &error); -#endif if (!executionEngine) { std::cerr << "unable to make jit: " << error << "\n"; abort(); diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 08c95d48..4bcdd9f7 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -19,9 +19,16 @@ #include "ObjectHolder.h" #include "MemoryManager.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include <llvm/IR/Function.h> +#include <llvm/IR/Instruction.h> +#include <llvm/IR/Value.h> +#else #include <llvm/Function.h> #include <llvm/Instruction.h> #include <llvm/Value.h> +#endif + #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 778ef0ef..2dbabd01 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -25,10 +25,15 @@ #include "klee/Internal/ADT/RNG.h" #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#else #include "llvm/Constants.h" #include "llvm/Instructions.h" #include "llvm/Module.h" +#endif #include "llvm/Support/CallSite.h" #include "llvm/Support/CFG.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index d44e13b6..04f32780 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -21,7 +21,11 @@ #include "Executor.h" #include "MemoryManager.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Module.h" +#else #include "llvm/Module.h" +#endif #include "llvm/ADT/Twine.h" #include <errno.h> @@ -131,7 +135,9 @@ void SpecialFunctionHandler::prepare() { // Make sure NoReturn attribute is set, for optimization and // coverage counting. if (hi.doesNotReturn) -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + f->addFnAttr(Attribute::NoReturn); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) f->addFnAttr(Attributes::NoReturn); #else f->addFnAttr(Attribute::NoReturn); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index c0028a05..8161a52c 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -27,6 +27,15 @@ #include "UserSearcher.h" #include "../Solver/SolverStats.h" +#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) +#include "llvm/IR/BasicBlock.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/InlineAsm.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Type.h" +#else #include "llvm/BasicBlock.h" #include "llvm/Function.h" #include "llvm/Instructions.h" @@ -34,21 +43,15 @@ #include "llvm/InlineAsm.h" #include "llvm/Module.h" #include "llvm/Type.h" +#endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/CFG.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else +#include "llvm/Support/raw_os_ostream.h" #include "llvm/Support/Process.h" -#endif -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Path.h" -#else #include "llvm/Support/Path.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) #include "llvm/Support/FileSystem.h" #endif -#endif #include <iostream> #include <fstream> @@ -294,9 +297,6 @@ void StatsTracker::stepInstruction(ExecutionState &es) { // // FIXME: This trick no longer works, we should fix this in the line // number propogation. -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - if (isa<DbgStopPointInst>(inst)) -#endif es.coveredLines[&ii.file].insert(ii.line); es.coveredNew = true; es.instsSinceCovNew = 1; @@ -401,7 +401,11 @@ void StatsTracker::writeStatsLine() { << "," << numBranches << "," << util::getUserTime() << "," << executor.states.size() +#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) + << "," << sys::Process::GetMallocUsage() +#else << "," << sys::Process::GetTotalMemoryUsage() +#endif << "," << stats::queries << "," << stats::queryConstructs << "," << 0 // was numObjects diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index d2c07f46..037b23f3 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -16,11 +16,7 @@ #include "CoreStats.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif using namespace klee; using namespace llvm; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index b759daae..90d9bcd4 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -11,6 +11,13 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else +#include "llvm/Function.h" +#endif +#include "llvm/Support/CommandLine.h" +#include "klee/Internal/Module/KModule.h" #include <iostream> #include <map> diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index a28ad907..82c60205 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -354,11 +354,7 @@ void ConstantExpr::toString(std::string &Res, unsigned radix) const { ref<ConstantExpr> ConstantExpr::Concat(const ref<ConstantExpr> &RHS) { Expr::Width W = getWidth() + RHS->getWidth(); APInt Tmp(value); -#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8) - Tmp.zext(W); -#else Tmp=Tmp.zext(W); -#endif Tmp <<= RHS->getWidth(); Tmp |= APInt(RHS->value).zext(W); diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 3871286e..5b3e96b7 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -1496,17 +1496,9 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) { Val = -Val; if (Type < Val.getBitWidth()) -#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8) - Val.trunc(Type); -#else Val=Val.trunc(Type); -#endif else if (Type > Val.getBitWidth()) -#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8) - Val.zext(Type); -#else Val=Val.zext(Type); -#endif return ExprResult(Builder->Constant(Val)); } diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp index 18ef398a..79fd4afc 100644 --- a/lib/Module/Checks.cpp +++ b/lib/Module/Checks.cpp @@ -11,6 +11,19 @@ #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/InstrTypes.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Type.h" +#include "llvm/IR/DataLayout.h" +#else #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Function.h" @@ -18,19 +31,22 @@ #include "llvm/Instruction.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" -#include "llvm/Pass.h" #include "llvm/Type.h" -#include "llvm/Transforms/Scalar.h" -#include "llvm/Transforms/Utils/BasicBlockUtils.h" + +#include "llvm/LLVMContext.h" + #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif +#include "llvm/Pass.h" +#include "llvm/Transforms/Scalar.h" +#include "llvm/Transforms/Utils/BasicBlockUtils.h" +#include "llvm/Support/CallSite.h" +#include <iostream> using namespace llvm; using namespace klee; @@ -76,3 +92,62 @@ bool DivCheckPass::runOnModule(Module &M) { } return moduleChanged; } + +char OvershiftCheckPass::ID; + +bool OvershiftCheckPass::runOnModule(Module &M) { + Function *overshiftCheckFunction = 0; + + bool moduleChanged = false; + + for (Module::iterator f = M.begin(), fe = M.end(); f != fe; ++f) { + for (Function::iterator b = f->begin(), be = f->end(); b != be; ++b) { + for (BasicBlock::iterator i = b->begin(), ie = b->end(); i != ie; ++i) { + if (BinaryOperator* binOp = dyn_cast<BinaryOperator>(i)) { + // find all shift instructions + Instruction::BinaryOps opcode = binOp->getOpcode(); + + if (opcode == Instruction::Shl || + opcode == Instruction::LShr || + opcode == Instruction::AShr ) { + std::vector<llvm::Value*> args; + + // Determine bit width of first operand + uint64_t bitWidth=i->getOperand(0)->getType()->getScalarSizeInBits(); + + ConstantInt *bitWidthC = ConstantInt::get(Type::getInt64Ty(getGlobalContext()),bitWidth,false); + args.push_back(bitWidthC); + + CastInst *shift = + CastInst::CreateIntegerCast(i->getOperand(1), + Type::getInt64Ty(getGlobalContext()), + false, /* sign doesn't matter */ + "int_cast_to_i64", + i); + args.push_back(shift); + + + // Lazily bind the function to avoid always importing it. + if (!overshiftCheckFunction) { + Constant *fc = M.getOrInsertFunction("klee_overshift_check", + Type::getVoidTy(getGlobalContext()), + Type::getInt64Ty(getGlobalContext()), + Type::getInt64Ty(getGlobalContext()), + NULL); + overshiftCheckFunction = cast<Function>(fc); + } + + // Inject CallInstr to check if overshifting possible +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) + CallInst::Create(overshiftCheckFunction, args, "", &*i); +#else + CallInst::Create(overshiftCheckFunction, args.begin(), args.end(), "", &*i); +#endif + moduleChanged = true; + } + } + } + } + } + return moduleChanged; +} diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp index d0ef52d0..301db1ff 100644 --- a/lib/Module/InstructionInfoTable.cpp +++ b/lib/Module/InstructionInfoTable.cpp @@ -10,23 +10,26 @@ #include "klee/Internal/Module/InstructionInfoTable.h" #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#else #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#include "llvm/Linker.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) -#include "llvm/Assembly/AsmAnnotationWriter.h" -#else +#endif +#include "llvm/Linker.h" #include "llvm/Assembly/AssemblyAnnotationWriter.h" #include "llvm/Support/FormattedStream.h" -#endif #include "llvm/Support/CFG.h" #include "llvm/Support/InstIterator.h" #include "llvm/Support/raw_ostream.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) #include "llvm/DebugInfo.h" -#elif LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) +#else #include "llvm/Analysis/DebugInfo.h" #endif #include "llvm/Analysis/ValueTracking.h" @@ -39,12 +42,8 @@ using namespace klee; class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter { public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - void emitInstructionAnnot(const Instruction *i, llvm::raw_ostream &os) { -#else void emitInstructionAnnot(const Instruction *i, llvm::formatted_raw_ostream &os) { -#endif os << "%%%"; os << (uintptr_t) i; } @@ -76,18 +75,9 @@ static void buildInstructionToLineMap(Module *m, } } -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -static std::string getDSPIPath(const DbgStopPointInst *dspi) { - std::string dir, file; - bool res = GetConstantStringInfo(dspi->getDirectory(), dir); - assert(res && "GetConstantStringInfo failed"); - res = GetConstantStringInfo(dspi->getFileName(), file); - assert(res && "GetConstantStringInfo failed"); -#else static std::string getDSPIPath(DILocation Loc) { std::string dir = Loc.getDirectory(); std::string file = Loc.getFilename(); -#endif if (dir.empty() || file[0] == '/') { return file; } else if (*dir.rbegin() == '/') { @@ -100,20 +90,12 @@ static std::string getDSPIPath(DILocation Loc) { bool InstructionInfoTable::getInstructionDebugInfo(const llvm::Instruction *I, const std::string *&File, unsigned &Line) { -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - if (const DbgStopPointInst *dspi = dyn_cast<DbgStopPointInst>(I)) { - File = internString(getDSPIPath(dspi)); - Line = dspi->getLine(); - return true; - } -#else if (MDNode *N = I->getMetadata("dbg")) { DILocation Loc(N); File = internString(getDSPIPath(Loc)); Line = Loc.getLineNumber(); return true; } -#endif return false; } diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 2f18c17e..0f095269 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -10,6 +10,19 @@ #include "Passes.h" #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/InstrTypes.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Type.h" +#include "llvm/IR/IRBuilder.h" + +#else #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Function.h" @@ -17,24 +30,23 @@ #include "llvm/Instruction.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" -#include "llvm/Pass.h" #include "llvm/Type.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) #include "llvm/IRBuilder.h" #else #include "llvm/Support/IRBuilder.h" #endif -#include "llvm/Transforms/Scalar.h" -#include "llvm/Transforms/Utils/BasicBlockUtils.h" #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif +#include "llvm/Pass.h" +#include "llvm/Transforms/Scalar.h" +#include "llvm/Transforms/Utils/BasicBlockUtils.h" using namespace llvm; @@ -46,11 +58,13 @@ bool IntrinsicCleanerPass::runOnModule(Module &M) { bool dirty = false; for (Module::iterator f = M.begin(), fe = M.end(); f != fe; ++f) for (Function::iterator b = f->begin(), be = f->end(); b != be; ++b) - dirty |= runOnBasicBlock(*b); + dirty |= runOnBasicBlock(*b, M); + if (Function *Declare = M.getFunction("llvm.trap")) + Declare->eraseFromParent(); return dirty; } -bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { +bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { bool dirty = false; #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) @@ -74,13 +88,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { // FIXME: This is much more target dependent than just the word size, // however this works for x86-32 and x86-64. case Intrinsic::vacopy: { // (dst, src) -> *((i8**) dst) = *((i8**) src) -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - Value *dst = ii->getOperand(1); - Value *src = ii->getOperand(2); -#else Value *dst = ii->getArgOperand(0); Value *src = ii->getArgOperand(1); -#endif if (WordSize == 4) { Type *i8pp = PointerType::getUnqual(PointerType::getUnqual(Type::getInt8Ty(getGlobalContext()))); @@ -111,13 +120,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { case Intrinsic::umul_with_overflow: { IRBuilder<> builder(ii->getParent(), ii); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - Value *op1 = ii->getOperand(1); - Value *op2 = ii->getOperand(2); -#else Value *op1 = ii->getArgOperand(0); Value *op2 = ii->getArgOperand(1); -#endif Value *result = 0; if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow) @@ -138,42 +142,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { break; } -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - case Intrinsic::dbg_stoppoint: { - // We can remove this stoppoint if the next instruction is - // sure to be another stoppoint. This is nice for cleanliness - // but also important for switch statements where it can allow - // the targets to be joined. - bool erase = false; - if (isa<DbgStopPointInst>(i) || - isa<UnreachableInst>(i)) { - erase = true; - } else if (isa<BranchInst>(i) || - isa<SwitchInst>(i)) { - BasicBlock *bb = i->getParent(); - erase = true; - for (succ_iterator it=succ_begin(bb), ie=succ_end(bb); - it!=ie; ++it) { - if (!isa<DbgStopPointInst>(it->getFirstNonPHI())) { - erase = false; - break; - } - } - } - - if (erase) { - ii->eraseFromParent(); - dirty = true; - } - break; - } - - case Intrinsic::dbg_region_start: - case Intrinsic::dbg_region_end: - case Intrinsic::dbg_func_start: -#else case Intrinsic::dbg_value: -#endif case Intrinsic::dbg_declare: // Remove these regardless of lower intrinsics flag. This can // be removed once IntrinsicLowering is fixed to not have bad @@ -181,6 +150,24 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { ii->eraseFromParent(); dirty = true; break; + + case Intrinsic::trap: { + // Intrisic instruction "llvm.trap" found. Directly lower it to + // a call of the abort() function. + Function *F = cast<Function>( + M.getOrInsertFunction( + "abort", Type::getVoidTy(getGlobalContext()), NULL)); + F->setDoesNotReturn(); + F->setDoesNotThrow(); + + CallInst::Create(F, Twine(), ii); + new UnreachableInst(getGlobalContext(), ii); + + ii->eraseFromParent(); + + dirty = true; + break; + } default: if (LowerIntrinsics) diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 1629bb79..d889b51f 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -22,31 +22,37 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "llvm/Bitcode/ReaderWriter.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Instructions.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/ValueSymbolTable.h" +#include "llvm/IR/DataLayout.h" +#else #include "llvm/Instructions.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" -#include "llvm/PassManager.h" #include "llvm/ValueSymbolTable.h" -#include "llvm/Support/CallSite.h" -#include "llvm/Support/CommandLine.h" -#include "llvm/Support/raw_ostream.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/Support/raw_os_ostream.h" -#endif -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Path.h" -#else -#include "llvm/Support/Path.h" -#endif #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif + +#endif + +#include "llvm/PassManager.h" +#include "llvm/Support/CallSite.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" +#include "llvm/Support/raw_os_ostream.h" +#include "llvm/Support/Path.h" #include "llvm/Transforms/Scalar.h" +#include <llvm/Transforms/Utils/Cloning.h> +#include <llvm/Support/InstIterator.h> +#include <llvm/Support/Debug.h> + #include <sstream> using namespace llvm; @@ -99,7 +105,6 @@ KModule::KModule(Module *_module) #else targetData(new DataLayout(module)), #endif - dbgStopPointFn(0), kleeMergeFn(0), infos(0), constantTable(0) { @@ -113,6 +118,10 @@ KModule::~KModule() { ie = functions.end(); it != ie; ++it) delete *it; + for (std::map<llvm::Constant*, KConstant*>::iterator it=constantMap.begin(), + itE=constantMap.end(); it!=itE;++it) + delete it->second; + delete targetData; delete module; } @@ -189,6 +198,7 @@ static void injectStaticConstructorsAndDestructors(Module *m) { } } +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType, ...) { // If module lacks an externally visible symbol for the name then we @@ -211,6 +221,53 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType, m->getOrInsertFunction(name, FunctionType::get(retType, argTypes, false)); } } +#endif + +/// This function will take try to inline all calls to \p functionName +/// in the module \p module . +/// +/// It is intended that this function be used for inling calls to +/// check functions like <tt>klee_div_zero_check()</tt> +static void inlineChecks(Module *module, const char * functionName) { + std::vector<CallInst*> checkCalls; + Function* runtimeCheckCall = module->getFunction(functionName); + if (runtimeCheckCall == 0) + { + DEBUG( klee_warning("Failed to inline %s because no calls were made to it in module", functionName) ); + return; + } + + // Iterate through instructions in module and collect all + // call instructions to "functionName" that we care about. + for (Module::iterator f = module->begin(), fe = module->end(); f != fe; ++f) { + for (inst_iterator i=inst_begin(f), ie = inst_end(f); i != ie; ++i) { + if ( CallInst* ci = dyn_cast<CallInst>(&*i) ) + { + if ( ci->getCalledFunction() == runtimeCheckCall) + checkCalls.push_back(ci); + } + } + } + + unsigned int successCount=0; + unsigned int failCount=0; + InlineFunctionInfo IFI(0,0); + for ( std::vector<CallInst*>::iterator ci = checkCalls.begin(), + cie = checkCalls.end(); + ci != cie; ++ci) + { + // Try to inline the function + if (InlineFunction(*ci,IFI)) + ++successCount; + else + { + ++failCount; + klee_warning("Failed to inline function %s", functionName); + } + } + + DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) ); +} void KModule::prepare(const Interpreter::ModuleOptions &opts, InterpreterHandler *ih) { @@ -272,6 +329,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, PassManager pm; pm.add(new RaiseAsmPass()); if (opts.CheckDivZero) pm.add(new DivCheckPass()); + if (opts.CheckOvershift) pm.add(new OvershiftCheckPass()); // FIXME: This false here is to work around a bug in // IntrinsicLowering which caches values which may eventually be // deleted (via RAUW). This can be removed once LLVM fixes this @@ -281,7 +339,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, if (opts.Optimize) Optimize(module); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) // Force importing functions required by intrinsic lowering. Kind of // unfortunate clutter when we don't need them but we won't know // that until after all linking and intrinsic lowering is @@ -302,16 +360,33 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, PointerType::getUnqual(i8Ty), Type::getInt32Ty(getGlobalContext()), targetData->getIntPtrType(getGlobalContext()), (Type*) 0); - +#endif // FIXME: Missing force import for various math functions. // FIXME: Find a way that we can test programs without requiring // this to be linked in, it makes low level debugging much more // annoying. llvm::sys::Path path(opts.LibraryDir); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + path.appendComponent("kleeRuntimeIntrinsic.bc"); +#else path.appendComponent("libkleeRuntimeIntrinsic.bca"); +#endif module = linkWithLibrary(module, path.c_str()); + /* In order for KLEE to report ALL errors at instrumented + * locations the instrumentation call (e.g. "klee_div_zero_check") + * must be inlined. Otherwise one of the instructions in the + * instrumentation function will be used as the the location of + * the error which means that the error cannot be recorded again + * ( unless -emit-all-errors is used). + */ + if (opts.CheckDivZero) + inlineChecks(module, "klee_div_zero_check"); + if (opts.CheckOvershift) + inlineChecks(module, "klee_overshift_check"); + + // Needs to happen after linking (since ctors/dtors can be modified) // and optimization (since global optimization can rewrite lists). injectStaticConstructorsAndDestructors(module); @@ -332,7 +407,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, pm3.add(new IntrinsicCleanerPass(*targetData)); pm3.add(new PhiCleanerPass()); pm3.run(*module); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) // For cleanliness see if we can discard any of the functions we // forced to import. Function *f; @@ -342,7 +417,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, if (f && f->use_empty()) f->eraseFromParent(); f = module->getFunction("memset"); if (f && f->use_empty()) f->eraseFromParent(); - +#endif // Write out the .ll assembly file. We truncate long lines to work // around a kcachegrind parsing bug (it puts them on new lines), so @@ -351,38 +426,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, std::ostream *os = ih->openOutputFile("assembly.ll"); assert(os && os->good() && "unable to open source output"); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 6) - // We have an option for this in case the user wants a .ll they - // can compile. - if (NoTruncateSourceLines) { - os << *module; - } else { - bool truncated = false; - std::string string; - llvm::raw_string_ostream rss(string); - rss << *module; - rss.flush(); - const char *position = string.c_str(); - - for (;;) { - const char *end = index(position, '\n'); - if (!end) { - os << position; - break; - } else { - unsigned count = (end - position) + 1; - if (count<255) { - os->write(position, count); - } else { - os->write(position, 254); - os << "\n"; - truncated = true; - } - position = end+1; - } - } - } -#else llvm::raw_os_ostream *ros = new llvm::raw_os_ostream(*os); // We have an option for this in case the user wants a .ll they @@ -414,7 +457,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, } } delete ros; -#endif delete os; } @@ -427,7 +469,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, delete f; } - dbgStopPointFn = module->getFunction("llvm.dbg.stoppoint"); kleeMergeFn = module->getFunction("klee_merge"); /* Build shadow structures */ diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp index e5382c1a..a98b84ad 100644 --- a/lib/Module/LowerSwitch.cpp +++ b/lib/Module/LowerSwitch.cpp @@ -16,7 +16,9 @@ #include "Passes.h" #include "klee/Config/Version.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/LLVMContext.h" #endif #include <algorithm> diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 029540ae..fcdfa35a 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -10,26 +10,30 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/Bitcode/ReaderWriter.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IRReader/IRReader.h" +#include "llvm/IR/Module.h" +#include "llvm/Support/SourceMgr.h" +#include "llvm/Support/DataStream.h" +#else #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#include "llvm/Linker.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) -#include "llvm/Assembly/AsmAnnotationWriter.h" -#else -#include "llvm/Assembly/AssemblyAnnotationWriter.h" #endif + +#include "llvm/Linker.h" +#include "llvm/Assembly/AssemblyAnnotationWriter.h" #include "llvm/Support/CFG.h" #include "llvm/Support/CallSite.h" #include "llvm/Support/InstIterator.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Analysis/ValueTracking.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Path.h" -#else #include "llvm/Support/Path.h" -#endif #include <map> #include <iostream> @@ -42,6 +46,20 @@ using namespace klee; Module *klee::linkWithLibrary(Module *module, const std::string &libraryName) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + SMDiagnostic err; + std::string err_str; + sys::Path libraryPath(libraryName); + Module *new_mod = ParseIRFile(libraryPath.str(), err, +module->getContext()); + + if (Linker::LinkModules(module, new_mod, Linker::DestroySource, +&err_str)) { + assert(0 && "linked in library failed!"); + } + + return module; +#else Linker linker("klee", module, false); llvm::sys::Path libraryPath(libraryName); @@ -52,6 +70,7 @@ Module *klee::linkWithLibrary(Module *module, } return linker.releaseModule(); +#endif } Function *klee::getDirectCallTarget(CallSite cs) { @@ -72,13 +91,8 @@ Function *klee::getDirectCallTarget(CallSite cs) { } static bool valueIsOnlyCalled(const Value *v) { -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - for (Value::use_const_iterator it = v->use_begin(), ie = v->use_end(); - it != ie; ++it) { -#else for (Value::const_use_iterator it = v->use_begin(), ie = v->use_end(); it != ie; ++it) { -#endif if (const Instruction *instr = dyn_cast<Instruction>(*it)) { if (instr->getOpcode()==0) continue; // XXX function numbering inst if (!isa<CallInst>(instr) && !isa<InvokeInst>(instr)) return false; diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 6da9a2c1..41a106f1 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -16,22 +16,25 @@ //===----------------------------------------------------------------------===// #include "klee/Config/Version.h" -#include "llvm/Module.h" #include "llvm/PassManager.h" #include "llvm/Analysis/Passes.h" #include "llvm/Analysis/LoopPass.h" #include "llvm/Analysis/Verifier.h" #include "llvm/Support/CommandLine.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/DynamicLibrary.h" -#else #include "llvm/Support/DynamicLibrary.h" -#endif + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#else +#include "llvm/Module.h" #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif + #include "llvm/Target/TargetMachine.h" #include "llvm/Transforms/IPO.h" #include "llvm/Transforms/Scalar.h" @@ -105,9 +108,6 @@ static void AddStandardCompilePasses(PassManager &PM) { if (DisableOptimizations) return; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - addPass(PM, createRaiseAllocationsPass()); // call %malloc -> malloc inst -#endif addPass(PM, createCFGSimplificationPass()); // Clean up disgusting code addPass(PM, createPromoteMemoryToRegisterPass());// Kill useless allocas addPass(PM, createGlobalOptimizerPass()); // Optimize out global vars @@ -130,9 +130,6 @@ static void AddStandardCompilePasses(PassManager &PM) { addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs addPass(PM, createScalarReplAggregatesPass()); // Break up aggregate allocas addPass(PM, createInstructionCombiningPass()); // Combine silly seq's -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - addPass(PM, createCondPropagationPass()); // Propagate conditionals -#endif addPass(PM, createTailCallEliminationPass()); // Eliminate tail calls addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs @@ -140,9 +137,6 @@ static void AddStandardCompilePasses(PassManager &PM) { addPass(PM, createLoopRotatePass()); addPass(PM, createLICMPass()); // Hoist loop invariants addPass(PM, createLoopUnswitchPass()); // Unswitch loops. -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - addPass(PM, createLoopIndexSplitPass()); // Index split loops. -#endif // FIXME : Removing instcombine causes nestedloop regression. addPass(PM, createInstructionCombiningPass()); addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars @@ -156,9 +150,6 @@ static void AddStandardCompilePasses(PassManager &PM) { // Run instcombine after redundancy elimination to exploit opportunities // opened up by them. addPass(PM, createInstructionCombiningPass()); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - addPass(PM, createCondPropagationPass()); // Propagate conditionals -#endif addPass(PM, createDeadStoreEliminationPass()); // Delete dead stores addPass(PM, createAggressiveDCEPass()); // Delete dead instructions diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h index b3c46124..accb64d0 100644 --- a/lib/Module/Passes.h +++ b/lib/Module/Passes.h @@ -12,9 +12,15 @@ #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#else #include "llvm/Constants.h" #include "llvm/Instructions.h" #include "llvm/Module.h" +#endif #include "llvm/Pass.h" #include "llvm/CodeGen/IntrinsicLowering.h" @@ -38,9 +44,7 @@ namespace klee { class RaiseAsmPass : public llvm::ModulePass { static char ID; -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) const llvm::TargetLowering *TLI; -#endif llvm::Function *getIntrinsic(llvm::Module &M, unsigned IID, @@ -55,11 +59,7 @@ class RaiseAsmPass : public llvm::ModulePass { bool runOnInstruction(llvm::Module &M, llvm::Instruction *I); public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - RaiseAsmPass() : llvm::ModulePass((intptr_t) &ID) {} -#else - RaiseAsmPass() : llvm::ModulePass(ID) {} -#endif + RaiseAsmPass() : llvm::ModulePass(ID), TLI(0) {} virtual bool runOnModule(llvm::Module &M); }; @@ -76,7 +76,7 @@ class IntrinsicCleanerPass : public llvm::ModulePass { llvm::IntrinsicLowering *IL; bool LowerIntrinsics; - bool runOnBasicBlock(llvm::BasicBlock &b); + bool runOnBasicBlock(llvm::BasicBlock &b, llvm::Module &M); public: #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) IntrinsicCleanerPass(const llvm::TargetData &TD, @@ -84,11 +84,7 @@ public: IntrinsicCleanerPass(const llvm::DataLayout &TD, #endif bool LI=true) -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - : llvm::ModulePass((intptr_t) &ID), -#else : llvm::ModulePass(ID), -#endif #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) TargetData(TD), #else @@ -117,11 +113,7 @@ class PhiCleanerPass : public llvm::FunctionPass { static char ID; public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - PhiCleanerPass() : llvm::FunctionPass((intptr_t) &ID) {} -#else PhiCleanerPass() : llvm::FunctionPass(ID) {} -#endif virtual bool runOnFunction(llvm::Function &f); }; @@ -129,11 +121,28 @@ public: class DivCheckPass : public llvm::ModulePass { static char ID; public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - DivCheckPass(): ModulePass((intptr_t) &ID) {} -#else DivCheckPass(): ModulePass(ID) {} -#endif + virtual bool runOnModule(llvm::Module &M); +}; + +/// This pass injects checks to check for overshifting. +/// +/// Overshifting is where a Shl, LShr or AShr is performed +/// where the shift amount is greater than width of the bitvector +/// being shifted. +/// In LLVM (and in C/C++) this undefined behaviour! +/// +/// Example: +/// \code +/// unsigned char x=15; +/// x << 4 ; // Defined behaviour +/// x << 8 ; // Undefined behaviour +/// x << 255 ; // Undefined behaviour +/// \endcode +class OvershiftCheckPass : public llvm::ModulePass { + static char ID; +public: + OvershiftCheckPass(): ModulePass(ID) {} virtual bool runOnModule(llvm::Module &M); }; @@ -143,11 +152,7 @@ public: class LowerSwitchPass : public llvm::FunctionPass { public: static char ID; // Pass identification, replacement for typeid -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - LowerSwitchPass() : FunctionPass((intptr_t) &ID) {} -#else LowerSwitchPass() : FunctionPass(ID) {} -#endif virtual bool runOnFunction(llvm::Function &F); diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp index b5526f35..d9145a1e 100644 --- a/lib/Module/RaiseAsm.cpp +++ b/lib/Module/RaiseAsm.cpp @@ -9,12 +9,14 @@ #include "Passes.h" #include "klee/Config/Version.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/InlineAsm.h" +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/InlineAsm.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) + #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Host.h" #include "llvm/Target/TargetLowering.h" @@ -23,7 +25,6 @@ #else #include "llvm/Support/TargetRegistry.h" #endif -#endif using namespace llvm; using namespace klee; @@ -47,38 +48,8 @@ Function *RaiseAsmPass::getIntrinsic(llvm::Module &M, bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) { if (CallInst *ci = dyn_cast<CallInst>(I)) { if (InlineAsm *ia = dyn_cast<InlineAsm>(ci->getCalledValue())) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) (void) ia; return TLI && TLI->ExpandInlineAsm(ci); -#else - const std::string &as = ia->getAsmString(); - const std::string &cs = ia->getConstraintString(); - const llvm::Type *T = ci->getType(); - - // bswaps -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - unsigned NumOperands = ci->getNumOperands(); - llvm::Value *Arg0 = NumOperands > 1 ? ci->getOperand(1) : 0; -#else - unsigned NumOperands = ci->getNumArgOperands() + 1; - llvm::Value *Arg0 = NumOperands > 1 ? ci->getArgOperand(0) : 0; -#endif - if (Arg0 && T == Arg0->getType() && - ((T == llvm::Type::getInt16Ty(getGlobalContext()) && - as == "rorw $$8, ${0:w}" && - cs == "=r,0,~{dirflag},~{fpsr},~{flags},~{cc}") || - (T == llvm::Type::getInt32Ty(getGlobalContext()) && - as == "rorw $$8, ${0:w};rorl $$16, $0;rorw $$8, ${0:w}" && - cs == "=r,0,~{dirflag},~{fpsr},~{flags},~{cc}"))) { - Function *F = getIntrinsic(M, Intrinsic::bswap, Arg0->getType()); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - ci->setOperand(0, F); -#else - ci->setCalledFunction(F); -#endif - return true; - } -#endif } } @@ -88,7 +59,6 @@ bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) { bool RaiseAsmPass::runOnModule(Module &M) { bool changed = false; -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) std::string Err; #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) std::string HostTriple = llvm::sys::getDefaultTargetTriple(); @@ -110,7 +80,6 @@ bool RaiseAsmPass::runOnModule(Module &M) { #endif TLI = TM->getTargetLowering(); } -#endif for (Module::iterator fi = M.begin(), fe = M.end(); fi != fe; ++fi) { for (Function::iterator bi = fi->begin(), be = fi->end(); bi != be; ++bi) { diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile index 11d3d330..2be74c01 100755 --- a/lib/Solver/Makefile +++ b/lib/Solver/Makefile @@ -14,3 +14,12 @@ DONT_BUILD_RELINKED=1 BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) + CXX.Flags += $(metaSMT_CXXFLAGS) + CXX.Flags += $(metaSMT_INCLUDES) +endif \ No newline at end of file diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h new file mode 100644 index 00000000..2b084ac7 --- /dev/null +++ b/lib/Solver/MetaSMTBuilder.h @@ -0,0 +1,1167 @@ + /* + * MetaSMTBuilder.h + * + * Created on: 8 Aug 2012 + * Author: hpalikar + */ + +#ifndef METASMTBUILDER_H_ +#define METASMTBUILDER_H_ + +#include "klee/Config/config.h" +#include "klee/Expr.h" +#include "klee/util/ExprPPrinter.h" +#include "klee/util/ArrayExprHash.h" +#include "klee/util/ExprHashMap.h" +#include "ConstantDivision.h" + +#ifdef SUPPORT_METASMT + +#include "llvm/Support/CommandLine.h" + +#include <metaSMT/frontend/Logic.hpp> +#include <metaSMT/frontend/QF_BV.hpp> +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/support/default_visitation_unrolling_limit.hpp> +#include <metaSMT/support/run_algorithm.hpp> + +#define Expr VCExpr +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef STP + +#include <boost/mpl/vector.hpp> +#include <boost/format.hpp> + +using namespace metaSMT; +using namespace metaSMT::logic::QF_BV; + + +#define DIRECT_CONTEXT + +namespace { + llvm::cl::opt<bool> + UseConstructHashMetaSMT("use-construct-hash-metasmt", + llvm::cl::desc("Use hash-consing during metaSMT query construction."), + llvm::cl::init(true)); +} + + +namespace klee { + +typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::true_tag>::type > const MetaSMTConstTrue; +typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::false_tag>::type > const MetaSMTConstFalse; +typedef metaSMT::logic::Array::array MetaSMTArray; + +template<typename SolverContext> +class MetaSMTBuilder; + +template<typename SolverContext> +class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > { + + friend class MetaSMTBuilder<SolverContext>; + +public: + MetaSMTArrayExprHash() {}; + virtual ~MetaSMTArrayExprHash() {}; +}; + +static const bool mimic_stp = true; + + +template<typename SolverContext> +class MetaSMTBuilder { +public: + + MetaSMTBuilder(SolverContext& solver, bool optimizeDivides) : _solver(solver), _optimizeDivides(optimizeDivides) { }; + virtual ~MetaSMTBuilder() {}; + + typename SolverContext::result_type construct(ref<Expr> e); + + typename SolverContext::result_type getInitialRead(const Array *root, unsigned index); + + typename SolverContext::result_type getTrue() { + return(evaluate(_solver, metaSMT::logic::True)); + } + + typename SolverContext::result_type getFalse() { + return(evaluate(_solver, metaSMT::logic::False)); + } + + typename SolverContext::result_type bvOne(unsigned width) { + return bvZExtConst(width, 1); + } + + typename SolverContext::result_type bvZero(unsigned width) { + return bvZExtConst(width, 0); + } + + typename SolverContext::result_type bvMinusOne(unsigned width) { + return bvSExtConst(width, (int64_t) -1); + } + + typename SolverContext::result_type bvConst32(unsigned width, uint32_t value) { + return(evaluate(_solver, bvuint(value, width))); + } + + typename SolverContext::result_type bvConst64(unsigned width, uint64_t value) { + return(evaluate(_solver, bvuint(value, width))); + } + + typename SolverContext::result_type bvZExtConst(unsigned width, uint64_t value); + typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value); + + //logical left and right shift (not arithmetic) + typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits); + typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits); + typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + + + typename SolverContext::result_type getArrayForUpdate(const Array *root, const UpdateNode *un); + typename SolverContext::result_type getInitialArray(const Array *root); + MetaSMTArray buildArray(unsigned elem_width, unsigned index_width); + +private: + typedef ExprHashMap< std::pair<typename SolverContext::result_type, unsigned> > MetaSMTExprHashMap; + typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter; + typedef typename MetaSMTExprHashMap::const_iterator MetaSMTExprHashMapConstIter; + + SolverContext& _solver; + bool _optimizeDivides; + MetaSMTArrayExprHash<SolverContext> _arr_hash; + MetaSMTExprHashMap _constructed; + + typename SolverContext::result_type constructActual(ref<Expr> e, int *width_out); + typename SolverContext::result_type construct(ref<Expr> e, int *width_out); + + typename SolverContext::result_type bvBoolExtract(typename SolverContext::result_type expr, int bit); + typename SolverContext::result_type bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom); + typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b); + + typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, + typename SolverContext::result_type isSigned, unsigned shiftBits); + typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x); + typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d); + typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d); + + unsigned getShiftBits(unsigned amount) { + unsigned bits = 1; + amount--; + while (amount >>= 1) { + bits++; + } + return(bits); + } +}; + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, const UpdateNode *un) { + + if (!un) { + return(getInitialArray(root)); + } + else { + typename SolverContext::result_type un_expr; + bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); + + if (!hashed) { + un_expr = evaluate(_solver, + metaSMT::logic::Array::store(getArrayForUpdate(root, un->next), + construct(un->index, 0), + construct(un->value, 0))); + _arr_hash.hashUpdateNodeExpr(un, un_expr); + } + return(un_expr); + } +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root) +{ + assert(root); + typename SolverContext::result_type array_expr; + bool hashed = _arr_hash.lookupArrayExpr(root, array_expr); + + if (!hashed) { + + array_expr = evaluate(_solver, buildArray(8, 32)); + + if (root->isConstantArray()) { + for (unsigned i = 0, e = root->size; i != e; ++i) { + typename SolverContext::result_type tmp = + evaluate(_solver, + metaSMT::logic::Array::store(array_expr, + construct(ConstantExpr::alloc(i, root->getDomain()), 0), + construct(root->constantValues[i], 0))); + array_expr = tmp; + } + } + _arr_hash.hashArrayExpr(root, array_expr); + } + + return(array_expr); +} + +template<typename SolverContext> +MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width, unsigned index_width) { + return(metaSMT::logic::Array::new_array(elem_width, index_width)); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root, unsigned index) { + assert(root); + assert(false); + typename SolverContext::result_type array_exp = getInitialArray(root); + typename SolverContext::result_type res = evaluate( + _solver, + metaSMT::logic::Array::select(array_exp, bvuint(index, root->getDomain()))); + return(res); +} + + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) { + + typename SolverContext::result_type res; + + if (width <= 64) { + res = bvConst64(width, value); + } + else { + typename SolverContext::result_type expr = bvConst64(64, value); + typename SolverContext::result_type zero = bvConst64(64, 0); + + for (width -= 64; width > 64; width -= 64) { + expr = evaluate(_solver, concat(zero, expr)); + } + res = evaluate(_solver, concat(bvConst64(width, 0), expr)); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) { + + typename SolverContext::result_type res; + + if (width <= 64) { + res = bvConst64(width, value); + } + else { + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments + res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value))); + } + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvBoolExtract(typename SolverContext::result_type expr, int bit) { + return(evaluate(_solver, + metaSMT::logic::equal(extract(bit, bit, expr), + bvOne(1)))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom) { + return(evaluate(_solver, extract(top, bottom, expr))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b) { + return(evaluate(_solver, metaSMT::logic::equal(a, b))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount, + typename SolverContext::result_type isSigned, unsigned shiftBits) { + unsigned shift = amount & ((1 << shiftBits) - 1); + typename SolverContext::result_type res; + + if (shift == 0) { + res = expr; + } + else if (shift >= width - 1) { + res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width))); + } + else { + res = evaluate(_solver, metaSMT::logic::Ite(isSigned, + concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)), + bvRightShift(expr, width, shift, shiftBits))); + } + + return(res); +} + +// width is the width of expr; x -- number of bits to shift with +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x) { + + unsigned shiftBits = getShiftBits(width); + uint64_t add, sub; + typename SolverContext::result_type res; + bool first = true; + + // expr*x == expr*(add-sub) == expr*add - expr*sub + ComputeMultConstants64(x, add, sub); + + // legal, these would overflow completely + add = bits64::truncateToNBits(add, width); + sub = bits64::truncateToNBits(sub, width); + + for (int j = 63; j >= 0; j--) { + uint64_t bit = 1LL << j; + + if ((add & bit) || (sub & bit)) { + assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + + typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits); + + if (add & bit) { + if (!first) { + res = evaluate(_solver, bvadd(res, op)); + } else { + res = op; + first = false; + } + } else { + if (!first) { + res = evaluate(_solver, bvsub(res, op)); + } else { + // To reconsider: vc_bvUMinusExpr in STP + res = evaluate(_solver, bvsub(bvZero(width), op)); + first = false; + } + } + } + } + + if (first) { + res = bvZero(width); + } + + return(res); +} + + +/* + * Compute the 32-bit unsigned integer division of n by a divisor d based on + * the constants derived from the constant divisor d. + * + * Returns n/d without doing explicit division. The cost is 2 adds, 3 shifts, + * and a (64-bit) multiply. + * + * @param expr_n numerator (dividend) n as an expression + * @param width number of bits used to represent the value + * @param d the divisor + * + * @return n/d without doing explicit division + */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) { + + assert(width == 32 && "can only compute udiv constants for 32-bit division"); + + // Compute the constants needed to compute n/d for constant d without division by d. + uint32_t mprime, sh1, sh2; + ComputeUDivConstants32(d, mprime, sh1, sh2); + typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1); + typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2); + + // t1 = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32 + typename SolverContext::result_type expr_n_64 = evaluate(_solver, concat(bvZero(32), expr_n)); //extend to 64 bits + typename SolverContext::result_type t1_64bits = constructMulByConstant(expr_n_64, 64, (uint64_t)mprime); + typename SolverContext::result_type t1 = bvExtract(t1_64bits, 63, 32); //upper 32 bits + + // n/d = (((n - t1) >> sh1) + t1) >> sh2; + typename SolverContext::result_type n_minus_t1 = evaluate(_solver, bvsub(expr_n, t1)); + typename SolverContext::result_type shift_sh1 = bvVarRightShift(n_minus_t1, expr_sh1, 32); + typename SolverContext::result_type plus_t1 = evaluate(_solver, bvadd(shift_sh1, t1)); + typename SolverContext::result_type res = bvVarRightShift(plus_t1, expr_sh2, 32); + + return(res); +} + +/* + * Compute the 32-bitnsigned integer division of n by a divisor d based on + * the constants derived from the constant divisor d. + * + * Returns n/d without doing explicit division. The cost is 3 adds, 3 shifts, + * a (64-bit) multiply, and an XOR. + * + * @param n numerator (dividend) as an expression + * @param width number of bits used to represent the value + * @param d the divisor + * + * @return n/d without doing explicit division + */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) { + + assert(width == 32 && "can only compute udiv constants for 32-bit division"); + + // Compute the constants needed to compute n/d for constant d w/o division by d. + int32_t mprime, dsign, shpost; + ComputeSDivConstants32(d, mprime, dsign, shpost); + typename SolverContext::result_type expr_dsign = bvConst32(32, dsign); + typename SolverContext::result_type expr_shpost = bvConst32(32, shpost); + + // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32) + int64_t mprime_64 = (int64_t)mprime; + + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments + typename SolverContext::result_type expr_n_64 = evaluate(_solver, sign_extend(64 - width, expr_n)); + typename SolverContext::result_type mult_64 = constructMulByConstant(expr_n_64, 64, mprime_64); + typename SolverContext::result_type mulsh = bvExtract(mult_64, 63, 32); //upper 32-bits + typename SolverContext::result_type n_plus_mulsh = evaluate(_solver, bvadd(expr_n, mulsh)); + + // Improved variable arithmetic right shift: sign extend, shift, extract. + typename SolverContext::result_type extend_npm = evaluate(_solver, sign_extend(64 - width, n_plus_mulsh)); + typename SolverContext::result_type shift_npm = bvVarRightShift(extend_npm, expr_shpost, 64); + typename SolverContext::result_type shift_shpost = bvExtract(shift_npm, 31, 0); //lower 32-bits + + ///////////// + + // XSIGN(n) is -1 if n is negative, positive one otherwise + typename SolverContext::result_type is_signed = bvBoolExtract(expr_n, 31); + typename SolverContext::result_type neg_one = bvMinusOne(32); + typename SolverContext::result_type xsign_of_n = evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32))); + + // q0 = (n_plus_mulsh >> shpost) - XSIGN(n) + typename SolverContext::result_type q0 = evaluate(_solver, bvsub(shift_shpost, xsign_of_n)); + + // n/d = (q0 ^ dsign) - dsign + typename SolverContext::result_type q0_xor_dsign = evaluate(_solver, bvxor(q0, expr_dsign)); + typename SolverContext::result_type res = evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign)); + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { + + typename SolverContext::result_type res; + unsigned shift = amount & ((1 << shiftBits) - 1); + + if (shift == 0) { + res = expr; + } + else if (shift >= width) { + res = bvZero(width); + } + else { + // stp shift does "expr @ [0 x s]" which we then have to extract, + // rolling our own gives slightly smaller exprs + res = evaluate(_solver, concat(extract(width - shift - 1, 0, expr), + bvZero(shift))); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { + + typename SolverContext::result_type res; + unsigned shift = amount & ((1 << shiftBits) - 1); + + if (shift == 0) { + res = expr; + } + else if (shift >= width) { + res = bvZero(width); + } + else { + res = evaluate(_solver, concat(bvZero(shift), + extract(width - 1, shift, expr))); + } + + return(res); +} + +// left shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + typename SolverContext::result_type res = bvZero(width); + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount)); + + //construct a big if-then-elif-elif-... with one case per possible shift amount + for(int i = width - 1; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + bvLeftShift(expr, width, i, shiftBits), + res)); + } + + return(res); +} + +// logical right shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + typename SolverContext::result_type res = bvZero(width); + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0); + + //construct a big if-then-elif-elif-... with one case per possible shift amount + for (int i = width - 1; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + bvRightShift(expr, width, i, shiftBits), + res)); + // ToDo Reconsider widht to provide to bvRightShift + } + + return(res); +} + +// arithmetic right shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0); + + //get the sign bit to fill with + typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1); + + //start with the result if shifting by width-1 + typename SolverContext::result_type res = constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits); + + // construct a big if-then-elif-elif-... with one case per possible shift amount + // XXX more efficient to move the ite on the sign outside all exprs? + // XXX more efficient to sign extend, right shift, then extract lower bits? + for (int i = width - 2; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)), + constructAShrByConstant(expr, width, i, signedBool, shiftBits), + res)); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) { + typename SolverContext::result_type res = construct(e, 0); + _constructed.clear(); + return res; +} + + +/** if *width_out!=1 then result is a bitvector, + otherwise it is a bool */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) { + + if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) { + return(constructActual(e, width_out)); + } else { + MetaSMTExprHashMapIter it = _constructed.find(e); + if (it != _constructed.end()) { + if (width_out) { + *width_out = it->second.second; + } + return it->second.first; + } else { + int width = 0; + if (!width_out) { + width_out = &width; + } + typename SolverContext::result_type res = constructActual(e, width_out); + _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out))); + return res; + } + } +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) { + + typename SolverContext::result_type res; + + int width = 0; + if (!width_out) { + // assert(false); + width_out = &width; + } + + ++stats::queryConstructs; + +// std::cerr << "Constructing expression "; +// ExprPPrinter::printSingleExpr(std::cerr, e); +// std::cerr << "\n"; + + switch (e->getKind()) { + + case Expr::Constant: + { + ConstantExpr *coe = cast<ConstantExpr>(e); + assert(coe); + unsigned coe_width = coe->getWidth(); + *width_out = coe_width; + + // Coerce to bool if necessary. + if (coe_width == 1) { + res = (coe->isTrue()) ? getTrue() : getFalse(); + } + else if (coe_width <= 32) { + res = bvConst32(coe_width, coe->getZExtValue(32)); + } + else if (coe_width <= 64) { + res = bvConst64(coe_width, coe->getZExtValue()); + } + else { + ref<ConstantExpr> tmp = coe; + res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); + while (tmp->getWidth() > 64) { + tmp = tmp->Extract(64, tmp->getWidth() - 64); + unsigned min_width = std::min(64U, tmp->getWidth()); + res = evaluate(_solver, + concat(bvConst64(min_width, tmp->Extract(0, min_width)->getZExtValue()), + res)); + } + } + break; + } + + case Expr::NotOptimized: + { + NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e); + assert(noe); + res = construct(noe->src, width_out); + break; + } + + case Expr::Select: + { + SelectExpr *se = cast<SelectExpr>(e); + assert(se); + res = evaluate(_solver, + metaSMT::logic::Ite(construct(se->cond, 0), + construct(se->trueExpr, width_out), + construct(se->falseExpr, width_out))); + break; + } + + case Expr::Read: + { + ReadExpr *re = cast<ReadExpr>(e); + assert(re); + // FixMe call method of Array + *width_out = 8; + res = evaluate(_solver, + metaSMT::logic::Array::select( + getArrayForUpdate(re->updates.root, re->updates.head), + construct(re->index, 0))); + break; + } + + case Expr::Concat: + { + ConcatExpr *ce = cast<ConcatExpr>(e); + assert(ce); + *width_out = ce->getWidth(); + unsigned numKids = ce->getNumKids(); + + if (numKids > 0) { + res = evaluate(_solver, construct(ce->getKid(numKids-1), 0)); + for (int i = numKids - 2; i >= 0; i--) { + res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res)); + } + } + break; + } + + case Expr::Extract: + { + ExtractExpr *ee = cast<ExtractExpr>(e); + assert(ee); + // ToDo spare evaluate? + typename SolverContext::result_type child = evaluate(_solver, construct(ee->expr, width_out)); + + unsigned ee_width = ee->getWidth(); + *width_out = ee_width; + + if (ee_width == 1) { + res = bvBoolExtract(child, ee->offset); + } + else { + res = evaluate(_solver, + extract(ee->offset + ee_width - 1, ee->offset, child)); + } + break; + } + + case Expr::ZExt: + { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); + + int child_width = 0; + typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; + + if (child_width == 1) { + res = evaluate(_solver, + metaSMT::logic::Ite(child, bvOne(ce_width), bvZero(ce_width))); + } + else { + res = evaluate(_solver, zero_extend(ce_width - child_width, child)); + } + + // ToDo calculate how many zeros to add + // Note: STP and metaSMT differ in the prototype arguments; + // STP requires the width of the resulting bv; + // whereas metaSMT (and Z3) require the width of the zero vector that is to be appended + // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src))); + + break; + } + + case Expr::SExt: + { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); + + int child_width = 0; + typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; + + if (child_width == 1) { + res = evaluate(_solver, + metaSMT::logic::Ite(child, bvMinusOne(ce_width), bvZero(ce_width))); + } + else { + // ToDo ce_width - child_width? It is only ce_width in STPBuilder + res = evaluate(_solver, sign_extend(ce_width - child_width, child)); + } + + break; + } + + case Expr::Add: + { + AddExpr *ae = cast<AddExpr>(e); + assert(ae); + res = evaluate(_solver, bvadd(construct(ae->left, width_out), construct(ae->right, width_out))); + assert(*width_out != 1 && "uncanonicalized add"); + break; + } + + case Expr::Sub: + { + SubExpr *se = cast<SubExpr>(e); + assert(se); + res = evaluate(_solver, bvsub(construct(se->left, width_out), construct(se->right, width_out))); + assert(*width_out != 1 && "uncanonicalized sub"); + break; + } + + case Expr::Mul: + { + MulExpr *me = cast<MulExpr>(e); + assert(me); + + typename SolverContext::result_type right_expr = evaluate(_solver, construct(me->right, width_out)); + assert(*width_out != 1 && "uncanonicalized mul"); + + ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left); + if (CE && (CE->getWidth() <= 64)) { + res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue()); + } + else { + res = evaluate(_solver, bvmul(construct(me->left, width_out), right_expr)); + } + break; + } + + case Expr::UDiv: + { + UDivExpr *de = cast<UDivExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized udiv"); + bool construct_both = true; + + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && (CE->getWidth() <= 64)) { + uint64_t divisor = CE->getZExtValue(); + if (bits64::isPowerOfTwo(divisor)) { + res = bvRightShift(left_expr, *width_out, bits64::indexOfSingleBit(divisor), getShiftBits(*width_out)); + construct_both = false; + } + else if (_optimizeDivides) { + if (*width_out == 32) { //only works for 32-bit division + res = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor); + construct_both = false; + } + } + } + + if (construct_both) { + res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::SDiv: + { + SDivExpr *de = cast<SDivExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized sdiv"); + + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && _optimizeDivides && (*width_out == 32)) { + res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32)); + } + else { + res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::URem: + { + URemExpr *de = cast<URemExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized urem"); + + bool construct_both = true; + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && (CE->getWidth() <= 64)) { + + uint64_t divisor = CE->getZExtValue(); + + if (bits64::isPowerOfTwo(divisor)) { + + unsigned bits = bits64::indexOfSingleBit(divisor); + // special case for modding by 1 or else we bvExtract -1:0 + if (bits == 0) { + res = bvZero(*width_out); + construct_both = false; + } + else { + res = evaluate(_solver, concat(bvZero(*width_out - bits), + bvExtract(left_expr, bits - 1, 0))); + construct_both = false; + } + } + + // Use fast division to compute modulo without explicit division for constant divisor. + + if (_optimizeDivides && *width_out == 32) { //only works for 32-bit division + typename SolverContext::result_type quotient = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor); + typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor); + res = evaluate(_solver, bvsub(left_expr, quot_times_divisor)); + construct_both = false; + } + } + + if (construct_both) { + res = evaluate(_solver, bvurem(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::SRem: + { + SRemExpr *de = cast<SRemExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(de->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(de->right, width_out)); + assert(*width_out != 1 && "uncanonicalized srem"); + + bool construct_both = true; + +#if 0 //not faster per first benchmark + + if (_optimizeDivides) { + if (ConstantExpr *cre = de->right->asConstant()) { + uint64_t divisor = cre->asUInt64; + + //use fast division to compute modulo without explicit division for constant divisor + if( *width_out == 32 ) { //only works for 32-bit division + typename SolverContext::result_type quotient = constructSDivByConstant(left, *width_out, divisor); + typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor); + res = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor ); + construct_both = false; + } + } + } + +#endif + + if (construct_both) { + res = evaluate(_solver, bvsrem(left_expr, right_expr)); + } + break; + } + + case Expr::Not: + { + NotExpr *ne = cast<NotExpr>(e); + assert(ne); + + typename SolverContext::result_type child = evaluate(_solver, construct(ne->expr, width_out)); + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Not(child)); + } + else { + res = evaluate(_solver, bvnot(child)); + } + break; + } + + case Expr::And: + { + AndExpr *ae = cast<AndExpr>(e); + assert(ae); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ae->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ae->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvand(left_expr, right_expr)); + } + + break; + } + + case Expr::Or: + { + OrExpr *oe = cast<OrExpr>(e); + assert(oe); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(oe->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(oe->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvor(left_expr, right_expr)); + } + + break; + } + + case Expr::Xor: + { + XorExpr *xe = cast<XorExpr>(e); + assert(xe); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(xe->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(xe->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvxor(left_expr, right_expr)); + } + + break; + } + + case Expr::Shl: + { + ShlExpr *se = cast<ShlExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + assert(*width_out != 1 && "uncanonicalized shl"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) { + res = bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, &shiftWidth)); + res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvshl(left_expr, right_expr)); + } + + break; + } + + case Expr::LShr: + { + LShrExpr *lse = cast<LShrExpr>(e); + assert(lse); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(lse->left, width_out)); + assert(*width_out != 1 && "uncanonicalized lshr"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) { + res = bvRightShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(lse->right, &shiftWidth)); + res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvshr(left_expr, right_expr)); + } + + break; + } + + case Expr::AShr: + { + AShrExpr *ase = cast<AShrExpr>(e); + assert(ase); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ase->left, width_out)); + assert(*width_out != 1 && "uncanonicalized ashr"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) { + unsigned shift = (unsigned) CE->getLimitedValue(); + typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1); + res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ase->right, &shiftWidth)); + res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvashr(left_expr, right_expr)); + } + + break; + } + + case Expr::Eq: + { + EqExpr *ee = cast<EqExpr>(e); + assert(ee); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ee->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ee->right, width_out)); + + if (*width_out==1) { + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) { + if (CE->isTrue()) { + res = right_expr; + } + else { + res = evaluate(_solver, metaSMT::logic::Not(right_expr)); + } + } + else { + res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr)); + } + } // end of *width_out == 1 + else { + *width_out = 1; + res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr)); + } + + break; + } + + case Expr::Ult: + { + UltExpr *ue = cast<UltExpr>(e); + assert(ue); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized ult"); + *width_out = 1; + + res = evaluate(_solver, bvult(left_expr, right_expr)); + break; + } + + case Expr::Ule: + { + UleExpr *ue = cast<UleExpr>(e); + assert(ue); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized ule"); + *width_out = 1; + + res = evaluate(_solver, bvule(left_expr, right_expr)); + break; + } + + case Expr::Slt: + { + SltExpr *se = cast<SltExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized slt"); + *width_out = 1; + + res = evaluate(_solver, bvslt(left_expr, right_expr)); + break; + } + + case Expr::Sle: + { + SleExpr *se = cast<SleExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized sle"); + *width_out = 1; + + res = evaluate(_solver, bvsle(left_expr, right_expr)); + break; + } + + // unused due to canonicalization +#if 0 + case Expr::Ne: + case Expr::Ugt: + case Expr::Uge: + case Expr::Sgt: + case Expr::Sge: +#endif + + default: + assert(false); + break; + + }; + return res; +} + + +} /* end of namespace klee */ + +#endif /* SUPPORT_METASMT */ + +#endif /* METASMTBUILDER_H_ */ diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index e7187fc3..f2e38182 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -74,6 +74,7 @@ void QueryLoggingSolver::flushBuffer() { // we do additional check here to log only timeouts in case // user specified negative value for minQueryTimeToLog param os << logBuffer.str(); + os.flush(); } } diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 3414cda2..22b1545f 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -12,6 +12,7 @@ #include "SolverStats.h" #include "STPBuilder.h" +#include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Expr.h" @@ -20,6 +21,7 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/Internal/Support/Timer.h" +#include "klee/CommandLine.h" #define vc_bvBoolExtract IAMTHESPAWNOFSATAN @@ -45,6 +47,24 @@ IgnoreSolverFailures("ignore-solver-failures", using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + /***/ SolverImpl::~SolverImpl() { @@ -809,3 +829,426 @@ STPSolverImpl::computeInitialValues(const Query &query, SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { return runStatusCode; } + +#ifdef SUPPORT_METASMT + +// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------ + +template<typename SolverContext> +class MetaSMTSolverImpl : public SolverImpl { +private: + + SolverContext _meta_solver; + MetaSMTSolver<SolverContext> *_solver; + MetaSMTBuilder<SolverContext> *_builder; + double _timeout; + bool _useForked; + SolverRunStatus _runStatusCode; + +public: + MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolverImpl(); + + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout) { _timeout = timeout; } + + bool computeTruth(const Query&, bool &isValid); + bool computeValue(const Query&, ref<Expr> &result); + + bool computeInitialValues(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution, + double timeout); + + SolverRunStatus getOperationStatusCode(); + + SolverContext& get_meta_solver() { return(_meta_solver); }; + +}; + + +// ------------------------------------- MetaSMTSolver methods -------------------------------------------- + + +template<typename SolverContext> +MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) + : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides)) +{ + +} + +template<typename SolverContext> +MetaSMTSolver<SolverContext>::~MetaSMTSolver() +{ + +} + +template<typename SolverContext> +char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) { + return(impl->getConstraintLog(query)); +} + +template<typename SolverContext> +void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); +} + + +// ------------------------------------- MetaSMTSolverImpl methods ---------------------------------------- + + + +template<typename SolverContext> +MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides) + : _solver(solver), + _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)), + _timeout(0.0), + _useForked(useForked) +{ + assert(_solver && "unable to create MetaSMTSolver"); + assert(_builder && "unable to create MetaSMTBuilder"); + + if (_useForked) { + shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700); + assert(shared_memory_id >= 0 && "shmget failed"); + shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0); + assert(shared_memory_ptr != (void*) -1 && "shmat failed"); + shmctl(shared_memory_id, IPC_RMID, NULL); + } +} + +template<typename SolverContext> +MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() { + +} + +template<typename SolverContext> +char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) { + const char* msg = "Not supported"; + char *buf = new char[strlen(msg) + 1]; + strcpy(buf, msg); + return(buf); +} + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) { + + bool success = false; + std::vector<const Array*> objects; + std::vector< std::vector<unsigned char> > values; + bool hasSolution; + + if (computeInitialValues(query, objects, values, hasSolution)) { + // query.expr is valid iff !query.expr is not satisfiable + isValid = !hasSolution; + success = true; + } + + return(success); +} + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) { + + bool success = false; + std::vector<const Array*> objects; + std::vector< std::vector<unsigned char> > values; + bool hasSolution; + + // Find the object used in the expression, and compute an assignment for them. + findSymbolicObjects(query.expr, objects); + if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) { + assert(hasSolution && "state has invalid constraint set"); + // Evaluate the expression with the computed assignment. + Assignment a(objects, values); + result = a.evaluate(query.expr); + success = true; + } + + return(success); +} + + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) { + + _runStatusCode = SOLVER_RUN_STATUS_FAILURE; + + TimerStatIncrementer t(stats::queryTime); + assert(_builder); + + /* + * FIXME push() and pop() work for Z3 but not for Boolector. + * If using Z3, use push() and pop() and assert constraints. + * If using Boolector, assume constrainsts instead of asserting them. + */ + //push(_meta_solver); + + if (!_useForked) { + for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { + //assertion(_meta_solver, _builder->construct(*it)); + assumption(_meta_solver, _builder->construct(*it)); + } + } + + ++stats::queries; + ++stats::queryCounterexamples; + + bool success = true; + if (_useForked) { + _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout); + success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode)); + } + else { + _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution); + success = true; + } + + if (success) { + if (hasSolution) { + ++stats::queriesInvalid; + } + else { + ++stats::queriesValid; + } + } + + //pop(_meta_solver); + + return(success); +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) +{ + + // assume the negation of the query + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr))); + hasSolution = solve(_meta_solver); + + if (hasSolution) { + values.reserve(objects.size()); + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + std::vector<unsigned char> data; + data.reserve(array->size); + + for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp); + data.push_back(elem_value); + } + + values.push_back(data); + } + } + + if (true == hasSolution) { + return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE); + } + else { + return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE); + } +} + +static void metaSMTTimeoutHandler(int x) { + _exit(52); +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution, + double timeout) +{ + unsigned char *pos = shared_memory_ptr; + unsigned sum = 0; + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + sum += (*it)->size; + } + // sum += sizeof(uint64_t); + sum += sizeof(stats::queryConstructs); + assert(sum < shared_memory_size && "not enough shared memory for counterexample"); + + fflush(stdout); + fflush(stderr); + int pid = fork(); + if (pid == -1) { + fprintf(stderr, "error: fork failed (for metaSMT)"); + return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED); + } + + if (pid == 0) { + if (timeout) { + ::alarm(0); /* Turn off alarm so we can safely set signal handler */ + ::signal(SIGALRM, metaSMTTimeoutHandler); + ::alarm(std::max(1, (int) timeout)); + } + + for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { + assertion(_meta_solver, _builder->construct(*it)); + //assumption(_meta_solver, _builder->construct(*it)); + } + + + std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs; + if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) { + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + std::vector<typename SolverContext::result_type> aux_arr; + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + aux_arr.push_back(elem_exp); + } + aux_arr_exprs.push_back(aux_arr); + } + assert(aux_arr_exprs.size() == objects.size()); + } + + + // assume the negation of the query + // can be also asserted instead of assumed as we are in a child process + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr))); + unsigned res = solve(_meta_solver); + + if (res) { + + if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) { + + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp); + *pos++ = elem_value; + } + } + } + else { + typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end(); + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) { + const Array *array = *it; + const std::vector<typename SolverContext::result_type>& arr_exp = *eit; + assert(array); + assert(array->size == arr_exp.size()); + + for (unsigned offset = 0; offset < array->size; offset++) { + unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]); + *pos++ = elem_value; + } + } + } + } + assert((uint64_t*) pos); + *((uint64_t*) pos) = stats::queryConstructs; + + _exit(!res); + } + else { + int status; + pid_t res; + + do { + res = waitpid(pid, &status, 0); + } + while (res < 0 && errno == EINTR); + + if (res < 0) { + fprintf(stderr, "error: waitpid() for metaSMT failed"); + return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED); + } + + // From timed_run.py: It appears that linux at least will on + // "occasion" return a status when the process was terminated by a + // signal, so test signal first. + if (WIFSIGNALED(status) || !WIFEXITED(status)) { + fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status)); + return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED); + } + + int exitcode = WEXITSTATUS(status); + if (exitcode == 0) { + hasSolution = true; + } + else if (exitcode == 1) { + hasSolution = false; + } + else if (exitcode == 52) { + fprintf(stderr, "error: metaSMT timed out"); + return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT); + } + else { + fprintf(stderr, "error: metaSMT did not return a recognized code"); + return(SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE); + } + + if (hasSolution) { + values = std::vector< std::vector<unsigned char> >(objects.size()); + unsigned i = 0; + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + const Array *array = *it; + assert(array); + std::vector<unsigned char> &data = values[i++]; + data.insert(data.begin(), pos, pos + array->size); + pos += array->size; + } + } + stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs); + + if (true == hasSolution) { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + else { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + } + } +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() { + return _runStatusCode; +} + +template class MetaSMTSolver< DirectSolver_Context < Boolector> >; +template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >; +template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >; + +#endif /* SUPPORT_METASMT */ + diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp index fb0e349c..909e07da 100644 --- a/lib/Support/Time.cpp +++ b/lib/Support/Time.cpp @@ -10,11 +10,7 @@ #include "klee/Config/Version.h" #include "klee/Internal/System/Time.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif using namespace llvm; using namespace klee; diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp index 35922d4d..c61a90a3 100644 --- a/lib/Support/Timer.cpp +++ b/lib/Support/Timer.cpp @@ -10,11 +10,7 @@ #include "klee/Config/Version.h" #include "klee/Internal/Support/Timer.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif using namespace klee; using namespace llvm; diff --git a/runtime/Intrinsic/Makefile b/runtime/Intrinsic/Makefile index 849bfeee..3c6b01b3 100644 --- a/runtime/Intrinsic/Makefile +++ b/runtime/Intrinsic/Makefile @@ -17,6 +17,7 @@ BYTECODE_LIBRARY=1 DEBUG_RUNTIME=1 NO_PEDANTIC=1 +MODULE_NAME=kleeRuntimeIntrinsic C.Flags += -fno-builtin include $(LEVEL)/Makefile.common diff --git a/runtime/Intrinsic/klee_overshift_check.c b/runtime/Intrinsic/klee_overshift_check.c new file mode 100644 index 00000000..c0cb6102 --- /dev/null +++ b/runtime/Intrinsic/klee_overshift_check.c @@ -0,0 +1,31 @@ +//===-- klee_overshift_check.c ---------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <klee/klee.h> + +/* This instrumentation call is used to check for overshifting. + * If we do try to do x << y or x >> y + * where + * bitWidth = sizeof(x)*8 + * shift = y + * + * then we can detect overshifting (which has undefined behaviour). + */ +void klee_overshift_check(unsigned long long bitWidth, unsigned long long shift) { + if (shift >= bitWidth) { + /* Maybe we shouldn't throw an error because + * overshifting can be non-fatal? Perhaps + * we should generate a test case but carry + * on executing the state with a warning? + */ + klee_report_error("IGNORED", 0 /*Ignored */, "overshift error", "overshift.err"); + } +} + + diff --git a/runtime/Intrinsic/memcpy.c b/runtime/Intrinsic/memcpy.c index 7f7f133d..bd9f3e38 100644 --- a/runtime/Intrinsic/memcpy.c +++ b/runtime/Intrinsic/memcpy.c @@ -9,7 +9,7 @@ #include <stdlib.h> -void *memcpy(void *destaddr, void const *srcaddr, size_t len) { +__attribute__((weak)) void *memcpy(void *destaddr, void const *srcaddr, size_t len) { char *dest = destaddr; char const *src = srcaddr; diff --git a/runtime/Intrinsic/memmove.c b/runtime/Intrinsic/memmove.c index c6e1ada9..e89abf7d 100644 --- a/runtime/Intrinsic/memmove.c +++ b/runtime/Intrinsic/memmove.c @@ -9,7 +9,7 @@ #include <stdlib.h> -void *memmove(void *dst, const void *src, size_t count) { +__attribute__((weak)) void *memmove(void *dst, const void *src, size_t count) { char *a = dst; const char *b = src; diff --git a/runtime/Intrinsic/mempcpy.c b/runtime/Intrinsic/mempcpy.c index 31e142d9..e47a94b1 100644 --- a/runtime/Intrinsic/mempcpy.c +++ b/runtime/Intrinsic/mempcpy.c @@ -8,8 +8,7 @@ //===----------------------------------------------------------------------===// #include <stdlib.h> - -void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { +__attribute__((weak)) void *mempcpy(void *destaddr, void const *srcaddr, size_t len) { char *dest = destaddr; char const *src = srcaddr; diff --git a/runtime/Intrinsic/memset.c b/runtime/Intrinsic/memset.c index bef85e6a..c21f1fa9 100644 --- a/runtime/Intrinsic/memset.c +++ b/runtime/Intrinsic/memset.c @@ -8,8 +8,7 @@ //===----------------------------------------------------------------------===// #include <stdlib.h> - -void *memset(void * dst, int s, size_t count) { +__attribute__ ((weak)) void *memset(void * dst, int s, size_t count) { volatile char * a = dst; while (count-- > 0) *a++ = s; diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c index b9a848d0..1c75cd76 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -35,7 +35,7 @@ void klee_warning(const char*); void klee_warning_once(const char*); int klee_get_errno(void); -/* Returns pointer to the symbolic file structure is the pathname is symbolic */ +/* Returns pointer to the symbolic file structure fs the pathname is symbolic */ static exe_disk_file_t *__get_sym_file(const char *pathname) { char c = pathname[0]; unsigned i; @@ -198,6 +198,108 @@ int __fd_open(const char *pathname, int flags, mode_t mode) { return fd; } +int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode) { + exe_file_t *f; + int fd; + if (basefd != AT_FDCWD) { + exe_file_t *bf = __get_file(basefd); + + if (!bf) { + errno = EBADF; + return -1; + } else if (bf->dfile) { + klee_warning("symbolic file descriptor, ignoring (ENOENT)"); + errno = ENOENT; + return -1; + } + basefd = bf->fd; + } + + if (__get_sym_file(pathname)) { + /* for a symbolic file, it doesn't matter if/where it exists on disk */ + return __fd_open(pathname, flags, mode); + } + + for (fd = 0; fd < MAX_FDS; ++fd) + if (!(__exe_env.fds[fd].flags & eOpen)) + break; + if (fd == MAX_FDS) { + errno = EMFILE; + return -1; + } + + f = &__exe_env.fds[fd]; + + /* Should be the case if file was available, but just in case. */ + memset(f, 0, sizeof *f); + + int os_fd = syscall(__NR_openat, (long)basefd, __concretize_string(pathname), (long)flags, mode); + if (os_fd == -1) { + errno = klee_get_errno(); + return -1; + } + + f->fd = os_fd; + f->flags = eOpen; + if ((flags & O_ACCMODE) == O_RDONLY) { + f->flags |= eReadable; + } else if ((flags & O_ACCMODE) == O_WRONLY) { + f->flags |= eWriteable; + } else { /* XXX What actually happens here if != O_RDWR. */ + f->flags |= eReadable | eWriteable; + } + + return fd; +} + + +int utimes(const char *path, const struct timeval times[2]) { + exe_disk_file_t *dfile = __get_sym_file(path); + + if (dfile) { + /* don't bother with usecs */ + dfile->stat->st_atime = times[0].tv_sec; + dfile->stat->st_mtime = times[1].tv_sec; +#ifdef _BSD_SOURCE + dfile->stat->st_atim.tv_nsec = 1000000000ll * times[0].tv_sec; + dfile->stat->st_mtim.tv_nsec = 1000000000ll * times[1].tv_sec; +#endif + return 0; + } + int r = syscall(__NR_utimes, __concretize_string(path), times); + if (r == -1) + errno = klee_get_errno(); + + return r; +} + + +int futimesat(int fd, const char* path, const struct timeval times[2]) { + if (fd != AT_FDCWD) { + exe_file_t *f = __get_file(fd); + + if (!f) { + errno = EBADF; + return -1; + } else if (f->dfile) { + klee_warning("symbolic file descriptor, ignoring (ENOENT)"); + errno = ENOENT; + return -1; + } + fd = f->fd; + } + if (__get_sym_file(path)) { + return utimes(path, times); + } + + int r = syscall(__NR_futimesat, (long)fd, + (path ? __concretize_string(path) : NULL), + times); + if (r == -1) + errno = klee_get_errno(); + return r; +} + int close(int fd) { static int n_calls = 0; exe_file_t *f; @@ -387,15 +489,15 @@ off64_t __fd_lseek(int fd, off64_t offset, int whence) { the offset, but really directories should only be SEEK_SET, so this solves the problem. */ if (whence == SEEK_SET) { - new_off = syscall(__NR_lseek, f->fd, (int) offset, SEEK_SET); + new_off = syscall(__NR_lseek, f->fd, offset, SEEK_SET); } else { - new_off = syscall(__NR_lseek, f->fd, (int) f->off, SEEK_SET); + new_off = syscall(__NR_lseek, f->fd, f->off, SEEK_SET); /* If we can't seek to start off, just return same error. Probably ESPIPE. */ if (new_off != -1) { assert(new_off == f->off); - new_off = syscall(__NR_lseek, f->fd, (int) offset, whence); + new_off = syscall(__NR_lseek, f->fd, offset, whence); } } @@ -446,6 +548,42 @@ int __fd_stat(const char *path, struct stat64 *buf) { } } +int fstatat(int fd, const char *path, struct stat *buf, int flags) { + if (fd != AT_FDCWD) { + exe_file_t *f = __get_file(fd); + + if (!f) { + errno = EBADF; + return -1; + } else if (f->dfile) { + klee_warning("symbolic file descriptor, ignoring (ENOENT)"); + errno = ENOENT; + return -1; + } + fd = f->fd; + } + exe_disk_file_t *dfile = __get_sym_file(path); + if (dfile) { + memcpy(buf, dfile->stat, sizeof(*dfile->stat)); + return 0; + } + +#if (defined __NR_newfstatat) && (__NR_newfstatat != 0) + int r = syscall(__NR_newfstatat, (long)fd, + (path ? __concretize_string(path) : NULL), + buf, (long)flags); +#else + int r = syscall(__NR_fstatat64, (long)fd, + (path ? __concretize_string(path) : NULL), + buf, (long)flags); +#endif + + if (r == -1) + errno = klee_get_errno(); + return r; +} + + int __fd_lstat(const char *path, struct stat64 *buf) { exe_disk_file_t *dfile = __get_sym_file(path); if (dfile) { @@ -680,7 +818,7 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { errno = EBADF; return -1; } - + if (f->dfile) { klee_warning("symbolic file, ignoring (EINVAL)"); errno = EINVAL; @@ -688,7 +826,7 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { } else { if ((unsigned long) f->off < 4096u) { /* Return our dirents */ - unsigned i, pad, bytes=0; + off64_t i, pad, bytes=0; /* What happens for bad offsets? */ i = f->off / sizeof(*dirp); @@ -718,10 +856,12 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { dirp->d_off = 4096; bytes += dirp->d_reclen; f->off = pad; + return bytes; } else { - unsigned os_pos = f->off - 4096; - int res, s; + off64_t os_pos = f->off - 4096; + int res; + off64_t s = 0; /* For reasons which I really don't understand, if I don't memset this then sometimes the kernel returns d_ino==0 for @@ -731,14 +871,13 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { Even more bizarre, interchanging the memset and the seek also case strange behavior. Really should be debugged properly. */ memset(dirp, 0, count); - s = syscall(__NR_lseek, f->fd, (int) os_pos, SEEK_SET); + s = syscall(__NR_lseek, f->fd, os_pos, SEEK_SET); assert(s != (off64_t) -1); res = syscall(__NR_getdents64, f->fd, dirp, count); if (res == -1) { errno = klee_get_errno(); } else { int pos = 0; - f->off = syscall(__NR_lseek, f->fd, 0, SEEK_CUR) + 4096; /* Patch offsets */ @@ -747,6 +886,7 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) { struct dirent64 *dp = (struct dirent64*) ((char*) dirp + pos); dp->d_off += 4096; pos += dp->d_reclen; + } } return res; @@ -1096,6 +1236,29 @@ int unlink(const char *pathname) { return -1; } +int unlinkat(int dirfd, const char *pathname, int flags) { + /* similar to unlink. keep them separated though to avoid + problems if unlink changes to actually delete files */ + exe_disk_file_t *dfile = __get_sym_file(pathname); + if (dfile) { + /* XXX check access */ + if (S_ISREG(dfile->stat->st_mode)) { + dfile->stat->st_ino = 0; + return 0; + } else if (S_ISDIR(dfile->stat->st_mode)) { + errno = EISDIR; + return -1; + } else { + errno = EPERM; + return -1; + } + } + + klee_warning("ignoring (EPERM)"); + errno = EPERM; + return -1; +} + ssize_t readlink(const char *path, char *buf, size_t bufsize) { exe_disk_file_t *dfile = __get_sym_file(path); if (dfile) { diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h index f2780143..cb86295c 100644 --- a/runtime/POSIX/fd.h +++ b/runtime/POSIX/fd.h @@ -79,6 +79,7 @@ void klee_init_env(int *argcPtr, char ***argvPtr); /* *** */ int __fd_open(const char *pathname, int flags, mode_t mode); +int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode); off64_t __fd_lseek(int fd, off64_t offset, int whence); int __fd_stat(const char *path, struct stat64 *buf); int __fd_lstat(const char *path, struct stat64 *buf); diff --git a/runtime/POSIX/fd_32.c b/runtime/POSIX/fd_32.c index 6246f057..36c5d41f 100644 --- a/runtime/POSIX/fd_32.c +++ b/runtime/POSIX/fd_32.c @@ -6,7 +6,18 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// +// Contains 32bit definitions of posix file functions +//===--- +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + +#include "klee/Config/Version.h" #define _LARGEFILE64_SOURCE #include "fd.h" @@ -41,6 +52,12 @@ static void __stat64_to_stat(struct stat64 *a, struct stat *b) { b->st_ctime = a->st_ctime; b->st_blksize = a->st_blksize; b->st_blocks = a->st_blocks; +#ifdef _BSD_SOURCE + b->st_atim.tv_nsec = a->st_atim.tv_nsec; + b->st_mtim.tv_nsec = a->st_mtim.tv_nsec; + b->st_ctim.tv_nsec = a->st_ctim.tv_nsec; +#endif + } /***/ @@ -59,6 +76,20 @@ int open(const char *pathname, int flags, ...) { return __fd_open(pathname, flags, mode); } +int openat(int fd, const char *pathname, int flags, ...) { + mode_t mode = 0; + + if (flags & O_CREAT) { + /* get mode */ + va_list ap; + va_start(ap, flags); + mode = va_arg(ap, mode_t); + va_end(ap); + } + + return __fd_openat(fd, pathname, flags, mode); +} + off_t lseek(int fd, off_t off, int whence) { return (off_t) __fd_lseek(fd, off, whence); } @@ -173,19 +204,3 @@ __attribute__((weak)) int open64(const char *pathname, int flags, ...) { return __fd_open(pathname, flags, mode); } - -__attribute__((weak)) off64_t lseek64(int fd, off64_t off, int whence) { - return __fd_lseek(fd, off, whence); -} - -__attribute__((weak)) int stat64(const char *path, struct stat64 *buf) { - return __fd_stat(path, buf); -} - -__attribute__((weak)) int lstat64(const char *path, struct stat64 *buf) { - return __fd_lstat(path, buf); -} - -__attribute__((weak)) int fstat64(int fd, struct stat64 *buf) { - return __fd_fstat(fd, buf); -} diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c index d0710caf..03fccc49 100644 --- a/runtime/POSIX/fd_64.c +++ b/runtime/POSIX/fd_64.c @@ -7,6 +7,16 @@ // //===----------------------------------------------------------------------===// +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + + +#include "klee/Config/Version.h" #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" @@ -46,6 +56,20 @@ int open(const char *pathname, int flags, ...) { return __fd_open(pathname, flags, mode); } +int openat(int fd, const char *pathname, int flags, ...) { + mode_t mode = 0; + + if (flags & O_CREAT) { + /* get mode */ + va_list ap; + va_start(ap, flags); + mode = va_arg(ap, mode_t); + va_end(ap); + } + + return __fd_openat(fd, pathname, flags, mode); +} + off64_t lseek(int fd, off64_t offset, int whence) { return __fd_lseek(fd, offset, whence); } diff --git a/runtime/POSIX/stubs.c b/runtime/POSIX/stubs.c index 3a9d380c..99e2e768 100644 --- a/runtime/POSIX/stubs.c +++ b/runtime/POSIX/stubs.c @@ -7,19 +7,21 @@ // //===----------------------------------------------------------------------===// -#include <string.h> -#include <stdio.h> +#define _XOPEN_SOURCE 700 + #include <errno.h> +#include <limits.h> #include <signal.h> +#include <stdio.h> +#include <stdlib.h> +#include <string.h> #include <time.h> +#include <unistd.h> #include <utime.h> #include <utmp.h> -#include <unistd.h> -#include <limits.h> -#include <stdlib.h> #include <sys/mman.h> -#include <sys/stat.h> #include <sys/resource.h> +#include <sys/stat.h> #include <sys/times.h> #include <sys/types.h> #include <sys/wait.h> @@ -31,20 +33,20 @@ void klee_warning_once(const char*); /* Silent ignore */ -int __syscall_rt_sigaction(int signum, const struct sigaction *act, +int __syscall_rt_sigaction(int signum, const struct sigaction *act, struct sigaction *oldact, size_t _something) __attribute__((weak)); -int __syscall_rt_sigaction(int signum, const struct sigaction *act, +int __syscall_rt_sigaction(int signum, const struct sigaction *act, struct sigaction *oldact, size_t _something) { klee_warning_once("silently ignoring"); return 0; } -int sigaction(int signum, const struct sigaction *act, +int sigaction(int signum, const struct sigaction *act, struct sigaction *oldact) __attribute__((weak)); -int sigaction(int signum, const struct sigaction *act, +int sigaction(int signum, const struct sigaction *act, struct sigaction *oldact) { klee_warning_once("silently ignoring"); return 0; @@ -122,21 +124,21 @@ int link(const char *oldpath, const char *newpath) __attribute__((weak)); int link(const char *oldpath, const char *newpath) { klee_warning("ignoring (EPERM)"); errno = EPERM; - return -1; + return -1; } int symlink(const char *oldpath, const char *newpath) __attribute__((weak)); int symlink(const char *oldpath, const char *newpath) { klee_warning("ignoring (EPERM)"); errno = EPERM; - return -1; + return -1; } int rename(const char *oldpath, const char *newpath) __attribute__((weak)); int rename(const char *oldpath, const char *newpath) { klee_warning("ignoring (EPERM)"); errno = EPERM; - return -1; + return -1; } int nanosleep(const struct timespec *req, struct timespec *rem) __attribute__((weak)); @@ -222,13 +224,6 @@ int utime(const char *filename, const struct utimbuf *buf) { return -1; } -int utimes(const char *filename, const struct timeval times[2]) __attribute__((weak)); -int utimes(const char *filename, const struct timeval times[2]) { - klee_warning("ignoring (EPERM)"); - errno = EPERM; - return -1; -} - int futimes(int fd, const struct timeval times[2]) __attribute__((weak)); int futimes(int fd, const struct timeval times[2]) { klee_warning("ignoring (EBADF)"); @@ -253,17 +248,13 @@ unsigned int gnu_dev_minor(unsigned long long int __dev) { unsigned long long int gnu_dev_makedev(unsigned int __major, unsigned int __minor) __attribute__((weak)); unsigned long long int gnu_dev_makedev(unsigned int __major, unsigned int __minor) { return ((__minor & 0xff) | ((__major & 0xfff) << 8) - | (((unsigned long long int) (__minor & ~0xff)) << 12) - | (((unsigned long long int) (__major & ~0xfff)) << 32)); + | (((unsigned long long int) (__minor & ~0xff)) << 12) + | (((unsigned long long int) (__major & ~0xfff)) << 32)); } char *canonicalize_file_name (const char *name) __attribute__((weak)); char *canonicalize_file_name (const char *name) { - char *res = malloc(PATH_MAX); - char *rp_res = realpath(name, res); - if (!rp_res) - free(res); - return rp_res; + return realpath(name, NULL); } int getloadavg(double loadavg[], int nelem) __attribute__((weak)); diff --git a/runtime/POSIX/testing-dir/a b/runtime/POSIX/testing-dir/a deleted file mode 120000 index dc1dc0cd..00000000 --- a/runtime/POSIX/testing-dir/a +++ /dev/null @@ -1 +0,0 @@ -/dev/null \ No newline at end of file diff --git a/runtime/POSIX/testing-dir/b b/runtime/POSIX/testing-dir/b deleted file mode 120000 index b9251ec6..00000000 --- a/runtime/POSIX/testing-dir/b +++ /dev/null @@ -1 +0,0 @@ -/dev/random \ No newline at end of file diff --git a/runtime/POSIX/testing-dir/c b/runtime/POSIX/testing-dir/c deleted file mode 100755 index 2b45f6a5..00000000 --- a/runtime/POSIX/testing-dir/c +++ /dev/null @@ -1,2 +0,0 @@ -#!/bin/sh -echo "Hello world!" diff --git a/runtime/POSIX/testing-dir/d b/runtime/POSIX/testing-dir/d deleted file mode 100644 index e69de29b..00000000 --- a/runtime/POSIX/testing-dir/d +++ /dev/null diff --git a/runtime/POSIX/testing-env b/runtime/POSIX/testing-env deleted file mode 100644 index 5a6e8eb8..00000000 --- a/runtime/POSIX/testing-env +++ /dev/null @@ -1,27 +0,0 @@ -# This file is sourced prior to running the testing environment, make -# sure to quote things. - -export TERM="xterm" -export SHELL="/bin/bash" -export LS_COLORS="no=00:fi=00:di=01;34:ln=01;36:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.gz=01;31:*.bz2=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.jpg=01;35:*.jpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.tif=01;35:*.tiff=01;35:*.png=01;35:*.mov=01;35:*.mpg=01;35:*.mpeg=01;35:*.avi=01;35:*.fli=01;35:*.gl=01;35:*.dl=01;35:*.xcf=01;35:*.xwd=01;35:*.flac=01;35:*.mp3=01;35:*.mpc=01;35:*.ogg=01;35:*.wav=01;35:" -export PATH="/usr/local/bin:/usr/bin:/bin" -export COLORTERM="gnome-terminal" -export LC_ALL=C -export TABSIZE=8 -export COLUMNS=80 - -# 1 BLOCK_SIZE -# 2 COLUMNS -# 1 DF_BLOCK_SIZE -# 1 DU_BLOCK_SIZE -# 1 HOME -# 1 LS_BLOCK_SIZE -# 1 LS_COLORS -# 11 POSIXLY_CORRECT -# 1 QUOTING_STYLE -# 3 SHELL -# 4 SIMPLE_BACKUP_SUFFIX -# 1 TABSIZE -# 2 TERM -# 2 TIME_STYLE -# 4 TMPDIR diff --git a/runtime/klee-libc/Makefile b/runtime/klee-libc/Makefile index e6a7ad72..eca63169 100755 --- a/runtime/klee-libc/Makefile +++ b/runtime/klee-libc/Makefile @@ -10,11 +10,13 @@ LEVEL=../.. LIBRARYNAME=klee-libc -DONT_BUILD_RELINKED=1 +MODULE_NAME=klee-libc +#DONT_BUILD_RELINKED=1 BYTECODE_LIBRARY=1 +MODULE_NAME=klee-libc # Don't strip debug info from the module. DEBUG_RUNTIME=1 -NO_PEDANTIC=1 +#NO_PEDANTIC=1 # Add __NO_INLINE__ to prevent glibc from using inline definitions of some # builtins. diff --git a/runtime/klee-libc/putchar.c b/runtime/klee-libc/putchar.c index 4c3a57e4..497402a6 100644 --- a/runtime/klee-libc/putchar.c +++ b/runtime/klee-libc/putchar.c @@ -15,6 +15,7 @@ int putchar(int c) { char x = c; - write(1, &x, 1); - return 1; + if (1 == write(1, &x, 1)) + return c; + return EOF; } diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index ad671a5e..9e9df87a 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc -// RUN: %klee --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log +// We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands +// RUN: %klee --use-cex-cache=false --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log // RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log @@ -7,7 +8,7 @@ // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log // RUN: grep "^; Query" klee-last/all-queries.smt2 | wc -l | grep -q 17 -// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10 +// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 17 #include <assert.h> diff --git a/test/Feature/IntrinsicTrap.ll b/test/Feature/IntrinsicTrap.ll new file mode 100644 index 00000000..5af46225 --- /dev/null +++ b/test/Feature/IntrinsicTrap.ll @@ -0,0 +1,28 @@ +; RUN: llvm-as %s -f -o %t1.bc +; RUN: %klee -disable-opt %t1.bc +; RUN: grep abort() klee-last/assembly.ll | wc -l | grep -q 2 +; RUN: echo "llvm.trap()" > %t2.ll +; RUN: grep llvm.trap() klee-last/assembly.ll %t2.ll | wc -l | grep -q 1 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-f128:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +define i32 @main() nounwind { +entry: + %a = add i32 1, 2 + %b = add i32 %a, 3 + %c = icmp ne i32 %b, 6 + br i1 %c, label %btrue, label %bfalse + +btrue: + call void @llvm.trap() noreturn nounwind + unreachable + +bfalse: + br label %return + +return: + ret i32 0 +} + +declare void @llvm.trap() noreturn nounwind diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index 3b1bacaf..d959c3de 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -2,35 +2,43 @@ // RUN: %llvmgcc -g -c %s -o %t.big.bc // RUN: %klee --max-memory=20 %t.little.bc > %t.little.log // RUN: %klee --max-memory=20 %t.big.bc > %t.big.log +// RUN: not grep -q "MALLOC FAILED" %t.little.log +// RUN: not grep -q "MALLOC FAILED" %t.big.log // RUN: not grep -q "DONE" %t.little.log // RUN: not grep -q "DONE" %t.big.log #include <stdlib.h> +#include <stdio.h> int main() { - int i, j, x=0; + int i, j, x=0, malloc_failed = 0; #ifdef LITTLE_ALLOC printf("IN LITTLE ALLOC\n"); // 200 MBs total (in 32 byte chunks) - for (i=0; i<100; i++) { - for (j=0; j<(1<<16); j++) - malloc(1<<5); + for (i=0; i<100 && !malloc_failed; i++) { + for (j=0; j<(1<<16); j++){ + void * p = malloc(1<<5); + malloc_failed |= (p == 0); + } } #else printf("IN BIG ALLOC\n"); // 200 MBs total - for (i=0; i<100; i++) { - malloc(1<<21); - + for (i=0; i<100 && !malloc_failed; i++) { + void *p = malloc(1<<21); + malloc_failed |= (p == 0); // Ensure we hit the periodic check + // Use the pointer to be not optimized out by the compiler for (j=0; j<10000; j++) - x++; + x+=(unsigned)p; } #endif + if (malloc_failed) + printf("MALLOC FAILED\n"); printf("DONE!\n"); return x; diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c new file mode 100644 index 00000000..bb967166 --- /dev/null +++ b/test/Feature/OvershiftCheck.c @@ -0,0 +1,26 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: %klee -check-overshift %t.bc 2> %t.log +// RUN: grep -c "overshift error" %t.log +// RUN: grep -c "OvershiftCheck.c:19: overshift error" %t.log +// RUN: grep -c "OvershiftCheck.c:23: overshift error" %t.log + +/* This test checks that two consecutive potential overshifts + * are reported as errors. + */ +int main() +{ + unsigned int x=15; + unsigned int y; + unsigned int z; + volatile unsigned int result; + + /* Overshift if y>= sizeof(x) */ + klee_make_symbolic(&y,sizeof(y),"shift_amount1"); + result = x << y; + + /* Overshift is z>= sizeof(x) */ + klee_make_symbolic(&z,sizeof(z),"shift_amount2"); + result = x >> z; + + return 0; +} diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c new file mode 100644 index 00000000..c1185870 --- /dev/null +++ b/test/Feature/consecutive_divide_by_zero.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc +// RUN: %klee -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log +// RUN: grep "completed paths = 3" %t.log +// RUN: grep "generated tests = 3" %t.log +// RUN: grep "consecutive_divide_by_zero.c:24: divide by zero" %t.log +// RUN: grep "consecutive_divide_by_zero.c:27: divide by zero" %t.log + +/* This test case captures a bug where two distinct division +* by zero errors are treated as the same error and so +* only one test case is generated EVEN IF THERE ARE MULTIPLE +* DISTINCT ERRORS! +*/ +int main() +{ + unsigned int a=15; + unsigned int b=15; + volatile unsigned int d1; + volatile unsigned int d2; + + klee_make_symbolic(&d1, sizeof(d1),"divisor1"); + klee_make_symbolic(&d2, sizeof(d2),"divisor2"); + + // deliberate division by zero possible + unsigned int result1 = a / d1; + + // another deliberate division by zero possible + unsigned int result2 = b / d2; + + return 0; +} diff --git a/test/Runtime/POSIX/Futimesat.c b/test/Runtime/POSIX/Futimesat.c new file mode 100644 index 00000000..6ae0ca7c --- /dev/null +++ b/test/Runtime/POSIX/Futimesat.c @@ -0,0 +1,45 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t2.bc +// RUN: touch /tmp/futimesat-dummy +// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10 +// RUN: rm /tmp/futimesat-dummy + +#include <assert.h> +#include <fcntl.h> +#include <sys/stat.h> +#include <sys/time.h> +#include <time.h> +#include <unistd.h> + +int main(int argc, char **argv) { + int r; + struct stat buf; + struct timeval times[2]; + + times[0].tv_sec = time(NULL)-3600; + times[0].tv_usec = 0; + times[1].tv_sec = time(NULL)-3600; + times[1].tv_usec = 0; + + r = futimesat(AT_FDCWD, "A", times); + assert(r != -1); + + r = fstatat(AT_FDCWD, "A", &buf, 0); + assert(r != -1); + assert(buf.st_atime == times[0].tv_sec && + buf.st_mtime == times[1].tv_sec); + + /* assumes /tmp exists and is writeable */ + int fd = open("/tmp", O_RDONLY); + assert(fd > 0); + r = futimesat(fd, "futimesat-dummy", times); + assert(r != -1); + + r = fstatat(fd, "futimesat-dummy", &buf, 0); + assert(r != -1); + assert(buf.st_atime == times[0].tv_sec && + buf.st_mtime == times[1].tv_sec); + + close(fd); + + return 0; +} diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c index 4f8d1425..293ee653 100644 --- a/test/Runtime/POSIX/Isatty.c +++ b/test/Runtime/POSIX/Isatty.c @@ -1,16 +1,16 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: %klee --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout 2>%t.log - // RUN: test -f klee-last/test000001.ktest // RUN: test -f klee-last/test000002.ktest // RUN: test -f klee-last/test000003.ktest // RUN: test -f klee-last/test000004.ktest - // RUN: grep -q "stdin is a tty" %t.log // RUN: grep -q "stdin is NOT a tty" %t.log // RUN: grep -q "stdout is a tty" %t.log // RUN: grep -q "stdout is NOT a tty" %t.log +// Depending on how uClibc is compiled (i.e. without -DKLEE_SYM_PRINTF) +// fprintf prints out on stdout even stderr is provided. #include <unistd.h> #include <stdio.h> #include <assert.h> diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c new file mode 100644 index 00000000..d417ee47 --- /dev/null +++ b/test/Runtime/POSIX/Openat.c @@ -0,0 +1,18 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc +// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10 +// RUN: test -f klee-last/test000001.ktest + +#include <assert.h> +#include <fcntl.h> + +int main(int argc, char **argv) { + int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC); + if (fd != -1) { + char buf[10]; + assert(read(fd, buf, 10) == 10); + assert(klee_is_symbolic(buf[0])); + } else { + klee_silent_exit(0); + } + return 0; +} diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c index db02217a..740db664 100644 --- a/test/Runtime/POSIX/SeedAndFail.c +++ b/test/Runtime/POSIX/SeedAndFail.c @@ -1,12 +1,10 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc // RUN: rm -rf tmp-123 -// RUN: %klee --libc=klee --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10 2>%t.log +// RUN: %klee --libc=uclibc --output-dir=tmp-123 --posix-runtime %t.bc --sym-files 1 10 2>%t.log // RUN: %klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1 // RUN: ls klee-last | grep -c assert | grep 4 - - -#include <stdio.h> +#include <string.h> #include <assert.h> #include <unistd.h> #include <sys/types.h> diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c index e7e3f2ff..b5402cf1 100644 --- a/test/Runtime/POSIX/Stdin.c +++ b/test/Runtime/POSIX/Stdin.c @@ -1,5 +1,5 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc -// RUN: %klee --libc=klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log +// RUN: %klee --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log // RUN: grep "mode:file" %t.log // RUN: grep "mode:dir" %t.log // RUN: grep "mode:chr" %t.log diff --git a/test/Solver/LargeIntegers.pc b/test/Solver/LargeIntegers.pc index 99d1a61b..53ff3a51 100644 --- a/test/Solver/LargeIntegers.pc +++ b/test/Solver/LargeIntegers.pc @@ -11,7 +11,7 @@ array a[64] : w32 -> w8 = symbolic (query [] false [(Extract w5 60 (Concat w128 (w64 1) (w64 2)))]) # RUN: grep -A 1 \"Query 2\" %t > %t2 -# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0\" %t2 +# RUN: grep \"Array 0:\ta.16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1\" %t2 (query [(Eq 0x0102030405060708090A0B0C0D0E0F10 (ReadLSB w128 0 a))] false [] [a]) diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index b6ccc91f..b93e361d 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -20,3 +20,14 @@ LINK_COMPONENTS = support include $(LEVEL)/Makefile.common LIBS += -lstp + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core +endif \ No newline at end of file diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index accc48e4..abc37d4b 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -34,17 +34,35 @@ #undef PACKAGE_TARNAME #undef PACKAGE_VERSION -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Signals.h" -#else #include "llvm/Support/Signals.h" #include "llvm/Support/system_error.h" -#endif using namespace llvm; using namespace klee; using namespace klee::expr; +#ifdef SUPPORT_METASMT + +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + + namespace { llvm::cl::opt<std::string> InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional, @@ -211,7 +229,39 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + Solver *coreSolver = NULL; // + +#ifdef SUPPORT_METASMT + if (UseMetaSMT != METASMT_BACKEND_NONE) { + + std::string backend; + + switch (UseMetaSMT) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + assert(false); + break; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + } +#else + coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); +#endif /* SUPPORT_METASMT */ + if (!UseDummySolver) { if (0 != MaxCoreSolverTime) { @@ -405,20 +455,12 @@ int main(int argc, char **argv) { std::string ErrorStr; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), &ErrorStr); - if (!MB) { - std::cerr << argv[0] << ": error: " << ErrorStr << "\n"; - return 1; - } -#else OwningPtr<MemoryBuffer> MB; error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), MB); if (ec) { std::cerr << argv[0] << ": error: " << ec.message() << "\n"; return 1; } -#endif ExprBuilder *Builder = 0; switch (BuilderKind) { @@ -438,45 +480,24 @@ int main(int argc, char **argv) { switch (ToolAction) { case PrintTokens: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - PrintInputTokens(MB); -#else PrintInputTokens(MB.get()); -#endif break; case PrintAST: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB, - Builder); -#else success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB.get(), Builder); -#endif break; case Evaluate: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), - MB, Builder); -#else success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB.get(), Builder); -#endif break; case PrintSMTLIBv2: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB,Builder); -#else success = printInputAsSMTLIBv2(InputFile=="-"? "<stdin>" : InputFile.c_str(), MB.get(),Builder); -#endif break; default: std::cerr << argv[0] << ": error: Unknown program action!\n"; } delete Builder; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - delete MB; -#endif llvm::llvm_shutdown(); return success ? 0 : 1; } diff --git a/tools/klee/Makefile b/tools/klee/Makefile index 01486fef..f050bf74 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -15,6 +15,20 @@ include $(LEVEL)/Makefile.config USEDLIBS = kleeCore.a kleeBasic.a kleeModule.a kleaverSolver.a kleaverExpr.a kleeSupport.a LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine +ifeq ($(shell echo "$(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3" | bc), 1) +LINK_COMPONENTS += irreader +endif include $(LEVEL)/Makefile.common LIBS += -lstp + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core +endif \ No newline at end of file diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 92e4df67..3616bfa6 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -13,18 +13,25 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) +#include "llvm/IR/Constants.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Type.h" +#include "llvm/IR/InstrTypes.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/Constants.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -#include "llvm/ModuleProvider.h" -#endif #include "llvm/Type.h" #include "llvm/InstrTypes.h" #include "llvm/Instruction.h" #include "llvm/Instructions.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" +#include "llvm/Support/FileSystem.h" #endif +#include "llvm/Support/FileSystem.h" #include "llvm/Bitcode/ReaderWriter.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ManagedStatic.h" @@ -41,27 +48,23 @@ #else #include "llvm/Support/TargetSelect.h" #endif -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Signals.h" -#else #include "llvm/Support/Signals.h" #include "llvm/Support/system_error.h" -#endif -#include <iostream> -#include <fstream> -#include <cerrno> + #include <dirent.h> +#include <signal.h> #include <unistd.h> -#include <errno.h> #include <sys/stat.h> #include <sys/wait.h> -#include <signal.h> +#include <cerrno> +#include <fstream> +#include <iomanip> #include <iostream> #include <iterator> -#include <fstream> #include <sstream> + using namespace llvm; using namespace klee; @@ -148,7 +151,12 @@ namespace { CheckDivZero("check-div-zero", cl::desc("Inject checks for division-by-zero"), cl::init(true)); - + + cl::opt<bool> + CheckOvershift("check-overshift", + cl::desc("Inject checks for overshift"), + cl::init(true)); + cl::opt<std::string> OutputDir("output-dir", cl::desc("Directory to write results in (defaults to klee-out-N)"), @@ -211,7 +219,7 @@ private: TreeStreamWriter *m_pathWriter, *m_symPathWriter; std::ostream *m_infoFile; - char m_outputDirectory[1024]; + sys::Path m_outputDirectory; unsigned m_testIndex; // number of tests written so far unsigned m_pathsExplored; // number of paths explored so far @@ -256,79 +264,86 @@ KleeHandler::KleeHandler(int argc, char **argv) m_pathWriter(0), m_symPathWriter(0), m_infoFile(0), + m_outputDirectory(), m_testIndex(0), m_pathsExplored(0), m_argc(argc), m_argv(argv) { - std::string theDir; if (OutputDir=="") { llvm::sys::Path directory(InputFile); - std::string dirname = ""; + std::stringstream dirname; directory.eraseComponent(); if (directory.isEmpty()) directory.set("."); - for (int i = 0; ; i++) { - char buf[256], tmp[64]; - sprintf(tmp, "klee-out-%d", i); - dirname = tmp; - sprintf(buf, "%s/%s", directory.c_str(), tmp); - theDir = buf; + for (int i = 0; i< INT_MAX ; i++) { + dirname << "klee-out-"; + dirname << i; + + m_outputDirectory = llvm::sys::Path(directory); // Copy + if (!m_outputDirectory.appendComponent(dirname.str())) + klee_error("Failed to append \"%s\" to \"%s\"", dirname.str().c_str(), directory.c_str()); - if (DIR *dir = opendir(theDir.c_str())) { - closedir(dir); - } else { - break; + bool isDir = true; + llvm::error_code e = llvm::sys::fs::exists(m_outputDirectory.str(), isDir); + if ( e != llvm::errc::success ) + klee_error("Failed to check if \"%s\" exists.", m_outputDirectory.str().c_str()); + + if (!isDir) + { + break; // Found an available directory name } + + // Warn the user if the klee-out-* exists but is not a directory + e = llvm::sys::fs::is_directory(m_outputDirectory.str(), isDir); + if ( e == llvm::errc::success && !isDir ) + klee_warning("A file \"%s\" exists, but it is not a directory", + m_outputDirectory.str().c_str()); + + dirname.str(""); // Clear + m_outputDirectory.clear(); } - std::cerr << "KLEE: output directory = \"" << dirname << "\"\n"; + if (m_outputDirectory.empty()) + klee_error("Failed to find available output directory in %s", dirname.str().c_str()); + + std::cerr << "KLEE: output directory = \"" << dirname.str() << "\"\n"; llvm::sys::Path klee_last(directory); - klee_last.appendComponent("klee-last"); - - if ((unlink(klee_last.c_str()) < 0) && (errno != ENOENT)) { - perror("Cannot unlink klee-last"); - assert(0 && "exiting."); - } + if(!klee_last.appendComponent("klee-last")) + klee_error("cannot create path name for klee-last"); + + if ((unlink(klee_last.c_str()) < 0) && (errno != ENOENT)) + klee_error("cannot unlink klee-last: %s", strerror(errno)); - if (symlink(dirname.c_str(), klee_last.c_str()) < 0) { - perror("Cannot make symlink"); - assert(0 && "exiting."); - } + if (symlink(dirname.str().c_str(), klee_last.c_str()) < 0) + klee_error("cannot create klee-last symlink: %s", strerror(errno)); + } else { - theDir = OutputDir; + if (!m_outputDirectory.set(OutputDir)) + klee_error("cannot use klee output directory: %s", OutputDir.c_str()); } - sys::Path p(theDir); -#if LLVM_VERSION_CODE < LLVM_VERSION(3, 1) - if (!p.isAbsolute()) { -#else - if (!sys::path::is_absolute(p.c_str())) { -#endif + if (!sys::path::is_absolute(m_outputDirectory.c_str())) { sys::Path cwd = sys::Path::GetCurrentDirectory(); - cwd.appendComponent(theDir); - p = cwd; - } - strcpy(m_outputDirectory, p.c_str()); + if(!cwd.appendComponent( m_outputDirectory.c_str())) + klee_error("cannot create absolute path name for output directory"); - if (mkdir(m_outputDirectory, 0775) < 0) { - std::cerr << "KLEE: ERROR: Unable to make output directory: \"" - << m_outputDirectory - << "\", refusing to overwrite.\n"; - exit(1); + m_outputDirectory = cwd; } - char fname[1024]; - snprintf(fname, sizeof(fname), "%s/warnings.txt", m_outputDirectory); - klee_warning_file = fopen(fname, "w"); - assert(klee_warning_file); + if (mkdir(m_outputDirectory.c_str(), 0775) < 0) + klee_error("cannot create directory \"%s\": %s", m_outputDirectory.c_str(), strerror(errno)); + + std::string file_path = getOutputFilename("warnings.txt"); + if ((klee_warning_file = fopen(file_path.c_str(), "w")) == NULL) + klee_error("cannot open file \"%s\": %s", file_path.c_str(), strerror(errno)); - snprintf(fname, sizeof(fname), "%s/messages.txt", m_outputDirectory); - klee_message_file = fopen(fname, "w"); - assert(klee_message_file); + file_path = getOutputFilename("messages.txt"); + if ((klee_message_file = fopen(file_path.c_str(), "w")) == NULL) + klee_error("cannot open file \"%s\": %s", file_path.c_str(), strerror(errno)); m_infoFile = openOutputFile("info"); } @@ -336,6 +351,8 @@ KleeHandler::KleeHandler(int argc, char **argv) KleeHandler::~KleeHandler() { if (m_pathWriter) delete m_pathWriter; if (m_symPathWriter) delete m_symPathWriter; + fclose(klee_warning_file); + fclose(klee_message_file); delete m_infoFile; } @@ -356,9 +373,12 @@ void KleeHandler::setInterpreter(Interpreter *i) { } std::string KleeHandler::getOutputFilename(const std::string &filename) { - char outfile[1024]; - sprintf(outfile, "%s/%s", m_outputDirectory, filename.c_str()); - return outfile; + sys::Path path(m_outputDirectory); + if(!path.appendComponent(filename)) { + klee_error("cannot create path name for \"%s\"", filename.c_str()); + } + + return path.str(); } std::ostream *KleeHandler::openOutputFile(const std::string &filename) { @@ -379,15 +399,13 @@ std::ostream *KleeHandler::openOutputFile(const std::string &filename) { } std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id) { - char filename[1024]; - sprintf(filename, "test%06d.%s", id, suffix.c_str()); - return getOutputFilename(filename); + std::stringstream filename; + filename << "test" << std::setfill('0') << std::setw(6) << id << '.' << suffix; + return filename.str(); } std::ostream *KleeHandler::openTestFile(const std::string &suffix, unsigned id) { - char filename[1024]; - sprintf(filename, "test%06d.%s", id, suffix.c_str()); - return openOutputFile(filename); + return openOutputFile(getTestFilename(suffix, id)); } @@ -429,7 +447,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, std::copy(out[i].second.begin(), out[i].second.end(), o->bytes); } - if (!kTest_toFile(&b, getTestFilename("ktest", id).c_str())) { + if (!kTest_toFile(&b, getOutputFilename(getTestFilename("ktest", id)).c_str())) { klee_warning("unable to write output test case, losing it"); } @@ -544,11 +562,7 @@ void KleeHandler::getOutFiles(std::string path, } for (std::set<llvm::sys::Path>::iterator it = contents.begin(), ie = contents.end(); it != ie; ++it) { -#if LLVM_VERSION_CODE != LLVM_VERSION(2, 6) std::string f = it->str(); -#else - std::string f = it->toString(); -#endif if (f.substr(f.size()-6,f.size()) == ".ktest") { results.push_back(f); } @@ -723,7 +737,6 @@ static const char *modelledExternals[] = { "klee_warning_once", "klee_alias_function", "klee_stack_trace", - "llvm.dbg.stoppoint", #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) "llvm.dbg.declare", "llvm.dbg.value", @@ -989,6 +1002,12 @@ static void replaceOrRenameFunction(llvm::Module *module, } static llvm::Module *linkWithUclibc(llvm::Module *mainModule) { + // Ensure that KLEE_UCLIBC exists + bool uclibcRootExists=false; + llvm::sys::fs::is_directory(KLEE_UCLIBC, uclibcRootExists); + if (!uclibcRootExists) + klee_error("Cannot link with uclibc. KLEE_UCLIBC (\"" KLEE_UCLIBC "\") is not a directory."); + Function *f; // force import of __uClibc_main mainModule->getOrInsertFunction("__uClibc_main", @@ -1183,28 +1202,7 @@ int main(int argc, char **argv, char **envp) { // Load the bytecode... std::string ErrorMsg; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - ModuleProvider *MP = 0; - if (MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg)) { - MP = getBitcodeModuleProvider(Buffer, getGlobalContext(), &ErrorMsg); - if (!MP) delete Buffer; - } - - if (!MP) - klee_error("error loading program '%s': %s", InputFile.c_str(), ErrorMsg.c_str()); - - Module *mainModule = MP->materializeModule(); - MP->releaseModule(); - delete MP; -#else Module *mainModule = 0; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - MemoryBuffer *Buffer = MemoryBuffer::getFileOrSTDIN(InputFile, &ErrorMsg); - if (Buffer) { - mainModule = getLazyBitcodeModule(Buffer, getGlobalContext(), &ErrorMsg); - if (!mainModule) delete Buffer; - } -#else OwningPtr<MemoryBuffer> BufferPtr; error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), BufferPtr); if (ec) { @@ -1213,7 +1211,6 @@ int main(int argc, char **argv, char **envp) { } mainModule = getLazyBitcodeModule(BufferPtr.get(), getGlobalContext(), &ErrorMsg); -#endif if (mainModule) { if (mainModule->MaterializeAllPermanently(&ErrorMsg)) { delete mainModule; @@ -1223,7 +1220,6 @@ int main(int argc, char **argv, char **envp) { if (!mainModule) klee_error("error loading program '%s': %s", InputFile.c_str(), ErrorMsg.c_str()); -#endif if (WithPOSIXRuntime) { int r = initEnv(mainModule); @@ -1241,7 +1237,8 @@ int main(int argc, char **argv, char **envp) { #endif Interpreter::ModuleOptions Opts(LibraryDir.c_str(), /*Optimize=*/OptimizeModule, - /*CheckDivZero=*/CheckDivZero); + /*CheckDivZero=*/CheckDivZero, + /*CheckOvershift=*/CheckOvershift); switch (Libc) { case NoLibc: /* silence compiler warning */ @@ -1250,7 +1247,11 @@ int main(int argc, char **argv, char **envp) { case KleeLibc: { // FIXME: Find a reasonable solution for this. llvm::sys::Path Path(Opts.LibraryDir); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + Path.appendComponent("klee-libc.bc"); +#else Path.appendComponent("libklee-libc.bca"); +#endif mainModule = klee::linkWithLibrary(mainModule, Path.c_str()); assert(mainModule && "unable to link with klee-libc"); break; @@ -1502,9 +1503,7 @@ int main(int argc, char **argv, char **envp) { std::cerr << stats.str(); handler->getInfoStream() << stats.str(); -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) BufferPtr.take(); -#endif delete handler; return 0; |