diff options
62 files changed, 2783 insertions, 246 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..cd209127 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,6 +40,7 @@ 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 := @@ -46,9 +53,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..be1dab5d 100644 --- a/Makefile.rules +++ b/Makefile.rules @@ -692,7 +692,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 +1192,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 6d846d5d..b41b6848 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -269,18 +269,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 @@ -348,6 +352,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 eb61b85b..c4c880d9 100755 --- a/configure +++ b/configure @@ -1,6 +1,6 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.68 for KLEE 0.01. +# Generated by GNU Autoconf 2.67 for KLEE 0.01. # # Report bugs to <daniel@minormatter.com>. # @@ -91,7 +91,6 @@ fi IFS=" "" $as_nl" # Find who we are. Look in the path if we contain no directory separator. -as_myself= case $0 in #(( *[\\/]* ) as_myself=$0 ;; *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR @@ -217,18 +216,11 @@ IFS=$as_save_IFS # We cannot yet assume a decent shell, so we have to provide a # neutralization value for shells without unset; and this also # works around shells that cannot unset nonexistent variables. - # Preserve -v and -x to the replacement shell. BASH_ENV=/dev/null ENV=/dev/null (unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV export CONFIG_SHELL - case $- in # (((( - *v*x* | *x*v* ) as_opts=-vx ;; - *v* ) as_opts=-v ;; - *x* ) as_opts=-x ;; - * ) as_opts= ;; - esac - exec "$CONFIG_SHELL" $as_opts "$as_myself" ${1+"$@"} + exec "$CONFIG_SHELL" "$as_myself" ${1+"$@"} fi if test x$as_have_required = xno; then : @@ -605,6 +597,8 @@ ac_includes_default="\ ac_subst_vars='LTLIBOBJS LIBOBJS RUNTEST +METASMT_ROOT +ENABLE_METASMT STP_ROOT CXXCPP ac_ct_CXX @@ -622,6 +616,7 @@ LDFLAGS CFLAGS CC RUNTIME_CONFIGURATION +RUNTIME_DEBUG_SYMBOLS RUNTIME_DISABLE_ASSERTIONS RUNTIME_ENABLE_OPTIMIZED ENABLE_POSIX_RUNTIME @@ -695,6 +690,7 @@ with_uclibc enable_posix_runtime with_runtime with_stp +with_metasmt ' ac_precious_vars='build_alias host_alias @@ -1113,7 +1109,7 @@ Try \`$0 --help' for more information" $as_echo "$as_me: WARNING: you should use --build, --host, --target" >&2 expr "x$ac_option" : ".*[^-._$as_cr_alnum]" >/dev/null && $as_echo "$as_me: WARNING: invalid host type: $ac_option" >&2 - : "${build_alias=$ac_option} ${host_alias=$ac_option} ${target_alias=$ac_option}" + : ${build_alias=$ac_option} ${host_alias=$ac_option} ${target_alias=$ac_option} ;; esac @@ -1339,6 +1335,7 @@ Optional Packages: --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 @@ -1420,7 +1417,7 @@ test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF KLEE configure 0.01 -generated by GNU Autoconf 2.68 +generated by GNU Autoconf 2.67 Copyright (C) 2010 Free Software Foundation, Inc. This configure script is free software; the Free Software Foundation @@ -1466,7 +1463,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 fi - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} as_fn_set_status $ac_retval } # ac_fn_c_try_compile @@ -1503,7 +1500,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 fi - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} as_fn_set_status $ac_retval } # ac_fn_c_try_cpp @@ -1516,10 +1513,10 @@ fi ac_fn_c_check_header_mongrel () { as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack - if eval \${$3+:} false; then : + if eval "test \"\${$3+set}\"" = set; then : { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5 $as_echo_n "checking for $2... " >&6; } -if eval \${$3+:} false; then : +if eval "test \"\${$3+set}\"" = set; then : $as_echo_n "(cached) " >&6 fi eval ac_res=\$$3 @@ -1586,7 +1583,7 @@ $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;} esac { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5 $as_echo_n "checking for $2... " >&6; } -if eval \${$3+:} false; then : +if eval "test \"\${$3+set}\"" = set; then : $as_echo_n "(cached) " >&6 else eval "$3=\$ac_header_compiler" @@ -1595,7 +1592,7 @@ eval ac_res=\$$3 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 $as_echo "$ac_res" >&6; } fi - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} } # ac_fn_c_check_header_mongrel @@ -1636,7 +1633,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=$ac_status fi rm -rf conftest.dSYM conftest_ipa8_conftest.oo - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} as_fn_set_status $ac_retval } # ac_fn_c_try_run @@ -1650,7 +1647,7 @@ ac_fn_c_check_header_compile () as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5 $as_echo_n "checking for $2... " >&6; } -if eval \${$3+:} false; then : +if eval "test \"\${$3+set}\"" = set; then : $as_echo_n "(cached) " >&6 else cat confdefs.h - <<_ACEOF >conftest.$ac_ext @@ -1668,7 +1665,7 @@ fi eval ac_res=\$$3 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 $as_echo "$ac_res" >&6; } - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} } # ac_fn_c_check_header_compile @@ -1705,7 +1702,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 fi - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} as_fn_set_status $ac_retval } # ac_fn_cxx_try_compile @@ -1742,7 +1739,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 ac_retval=1 fi - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} as_fn_set_status $ac_retval } # ac_fn_cxx_try_cpp @@ -1755,10 +1752,10 @@ fi ac_fn_cxx_check_header_mongrel () { as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack - if eval \${$3+:} false; then : + if eval "test \"\${$3+set}\"" = set; then : { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5 $as_echo_n "checking for $2... " >&6; } -if eval \${$3+:} false; then : +if eval "test \"\${$3+set}\"" = set; then : $as_echo_n "(cached) " >&6 fi eval ac_res=\$$3 @@ -1825,7 +1822,7 @@ $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;} esac { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5 $as_echo_n "checking for $2... " >&6; } -if eval \${$3+:} false; then : +if eval "test \"\${$3+set}\"" = set; then : $as_echo_n "(cached) " >&6 else eval "$3=\$ac_header_compiler" @@ -1834,7 +1831,7 @@ eval ac_res=\$$3 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5 $as_echo "$ac_res" >&6; } fi - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} } # ac_fn_cxx_check_header_mongrel @@ -1879,7 +1876,7 @@ fi # interfere with the next link command; also delete a directory that is # left behind by Apple's compiler. We do this before executing the actions. rm -rf conftest.dSYM conftest_ipa8_conftest.oo - eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno + eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;} as_fn_set_status $ac_retval } # ac_fn_cxx_try_link @@ -1888,7 +1885,7 @@ This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. It was created by KLEE $as_me 0.01, which was -generated by GNU Autoconf 2.68. Invocation command line was +generated by GNU Autoconf 2.67. Invocation command line was $ $0 $@ @@ -2146,7 +2143,7 @@ $as_echo "$as_me: loading site script $ac_site_file" >&6;} || { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "failed to load site script $ac_site_file -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } fi done @@ -2321,7 +2318,7 @@ $SHELL "$ac_aux_dir/config.sub" sun4 >/dev/null 2>&1 || { $as_echo "$as_me:${as_lineno-$LINENO}: checking build system type" >&5 $as_echo_n "checking build system type... " >&6; } -if ${ac_cv_build+:} false; then : +if test "${ac_cv_build+set}" = set; then : $as_echo_n "(cached) " >&6 else ac_build_alias=$build_alias @@ -2337,7 +2334,7 @@ fi $as_echo "$ac_cv_build" >&6; } case $ac_cv_build in *-*-*) ;; -*) as_fn_error $? "invalid value of canonical build" "$LINENO" 5;; +*) as_fn_error $? "invalid value of canonical build" "$LINENO" 5 ;; esac build=$ac_cv_build ac_save_IFS=$IFS; IFS='-' @@ -2355,7 +2352,7 @@ case $build_os in *\ *) build_os=`echo "$build_os" | sed 's/ /-/g'`;; esac { $as_echo "$as_me:${as_lineno-$LINENO}: checking host system type" >&5 $as_echo_n "checking host system type... " >&6; } -if ${ac_cv_host+:} false; then : +if test "${ac_cv_host+set}" = set; then : $as_echo_n "(cached) " >&6 else if test "x$host_alias" = x; then @@ -2370,7 +2367,7 @@ fi $as_echo "$ac_cv_host" >&6; } case $ac_cv_host in *-*-*) ;; -*) as_fn_error $? "invalid value of canonical host" "$LINENO" 5;; +*) as_fn_error $? "invalid value of canonical host" "$LINENO" 5 ;; esac host=$ac_cv_host ac_save_IFS=$IFS; IFS='-' @@ -2388,7 +2385,7 @@ case $host_os in *\ *) host_os=`echo "$host_os" | sed 's/ /-/g'`;; esac { $as_echo "$as_me:${as_lineno-$LINENO}: checking target system type" >&5 $as_echo_n "checking target system type... " >&6; } -if ${ac_cv_target+:} false; then : +if test "${ac_cv_target+set}" = set; then : $as_echo_n "(cached) " >&6 else if test "x$target_alias" = x; then @@ -2403,7 +2400,7 @@ fi $as_echo "$ac_cv_target" >&6; } case $ac_cv_target in *-*-*) ;; -*) as_fn_error $? "invalid value of canonical target" "$LINENO" 5;; +*) as_fn_error $? "invalid value of canonical target" "$LINENO" 5 ;; esac target=$ac_cv_target ac_save_IFS=$IFS; IFS='-' @@ -2428,7 +2425,7 @@ test -n "$target_alias" && { $as_echo "$as_me:${as_lineno-$LINENO}: checking type of operating system we're going to host on" >&5 $as_echo_n "checking type of operating system we're going to host on... " >&6; } -if ${klee_cv_os_type+:} false; then : +if test "${klee_cv_os_type+set}" = set; then : $as_echo_n "(cached) " >&6 else case $host in @@ -2707,6 +2704,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; } @@ -2714,6 +2713,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; } @@ -2721,6 +2722,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; } @@ -2728,6 +2731,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 @@ -2767,7 +2772,7 @@ if test -n "$ac_tool_prefix"; then set dummy ${ac_tool_prefix}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_CC+:} false; then : +if test "${ac_cv_prog_CC+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$CC"; then @@ -2807,7 +2812,7 @@ if test -z "$ac_cv_prog_CC"; then set dummy 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_ac_ct_CC+:} false; then : +if test "${ac_cv_prog_ac_ct_CC+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$ac_ct_CC"; then @@ -2860,7 +2865,7 @@ if test -z "$CC"; then set dummy ${ac_tool_prefix}cc; 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_CC+:} false; then : +if test "${ac_cv_prog_CC+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$CC"; then @@ -2900,7 +2905,7 @@ if test -z "$CC"; then set dummy cc; 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_CC+:} false; then : +if test "${ac_cv_prog_CC+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$CC"; then @@ -2959,7 +2964,7 @@ if test -z "$CC"; then set dummy $ac_tool_prefix$ac_prog; 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_CC+:} false; then : +if test "${ac_cv_prog_CC+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$CC"; then @@ -3003,7 +3008,7 @@ do set dummy $ac_prog; 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_ac_ct_CC+:} false; then : +if test "${ac_cv_prog_ac_ct_CC+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$ac_ct_CC"; then @@ -3058,7 +3063,7 @@ fi test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "no acceptable C compiler found in \$PATH -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } # Provide some information about the compiler. $as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5 @@ -3173,7 +3178,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error 77 "C compiler cannot create executables -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } else { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5 $as_echo "yes" >&6; } @@ -3216,7 +3221,7 @@ else { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "cannot compute suffix of executables: cannot compile and link -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } fi rm -f conftest conftest$ac_cv_exeext { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_exeext" >&5 @@ -3275,7 +3280,7 @@ $as_echo "$ac_try_echo"; } >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "cannot run C compiled programs. If you meant to cross compile, use \`--host'. -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } fi fi fi @@ -3286,7 +3291,7 @@ rm -f conftest.$ac_ext conftest$ac_cv_exeext conftest.out ac_clean_files=$ac_clean_files_save { $as_echo "$as_me:${as_lineno-$LINENO}: checking for suffix of object files" >&5 $as_echo_n "checking for suffix of object files... " >&6; } -if ${ac_cv_objext+:} false; then : +if test "${ac_cv_objext+set}" = set; then : $as_echo_n "(cached) " >&6 else cat confdefs.h - <<_ACEOF >conftest.$ac_ext @@ -3327,7 +3332,7 @@ sed 's/^/| /' conftest.$ac_ext >&5 { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "cannot compute suffix of object files: cannot compile -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } fi rm -f conftest.$ac_cv_objext conftest.$ac_ext fi @@ -3337,7 +3342,7 @@ OBJEXT=$ac_cv_objext ac_objext=$OBJEXT { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5 $as_echo_n "checking whether we are using the GNU C compiler... " >&6; } -if ${ac_cv_c_compiler_gnu+:} false; then : +if test "${ac_cv_c_compiler_gnu+set}" = set; then : $as_echo_n "(cached) " >&6 else cat confdefs.h - <<_ACEOF >conftest.$ac_ext @@ -3374,7 +3379,7 @@ ac_test_CFLAGS=${CFLAGS+set} ac_save_CFLAGS=$CFLAGS { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5 $as_echo_n "checking whether $CC accepts -g... " >&6; } -if ${ac_cv_prog_cc_g+:} false; then : +if test "${ac_cv_prog_cc_g+set}" = set; then : $as_echo_n "(cached) " >&6 else ac_save_c_werror_flag=$ac_c_werror_flag @@ -3452,7 +3457,7 @@ else fi { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5 $as_echo_n "checking for $CC option to accept ISO C89... " >&6; } -if ${ac_cv_prog_cc_c89+:} false; then : +if test "${ac_cv_prog_cc_c89+set}" = set; then : $as_echo_n "(cached) " >&6 else ac_cv_prog_cc_c89=no @@ -3560,7 +3565,7 @@ if test -n "$CPP" && test -d "$CPP"; then CPP= fi if test -z "$CPP"; then - if ${ac_cv_prog_CPP+:} false; then : + if test "${ac_cv_prog_CPP+set}" = set; then : $as_echo_n "(cached) " >&6 else # Double quotes because CPP needs to be expanded @@ -3676,7 +3681,7 @@ else { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "C preprocessor \"$CPP\" fails sanity check -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } fi ac_ext=c @@ -3688,7 +3693,7 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu { $as_echo "$as_me:${as_lineno-$LINENO}: checking for grep that handles long lines and -e" >&5 $as_echo_n "checking for grep that handles long lines and -e... " >&6; } -if ${ac_cv_path_GREP+:} false; then : +if test "${ac_cv_path_GREP+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -z "$GREP"; then @@ -3751,7 +3756,7 @@ $as_echo "$ac_cv_path_GREP" >&6; } { $as_echo "$as_me:${as_lineno-$LINENO}: checking for egrep" >&5 $as_echo_n "checking for egrep... " >&6; } -if ${ac_cv_path_EGREP+:} false; then : +if test "${ac_cv_path_EGREP+set}" = set; then : $as_echo_n "(cached) " >&6 else if echo a | $GREP -E '(a|b)' >/dev/null 2>&1 @@ -3818,7 +3823,7 @@ $as_echo "$ac_cv_path_EGREP" >&6; } { $as_echo "$as_me:${as_lineno-$LINENO}: checking for ANSI C header files" >&5 $as_echo_n "checking for ANSI C header files... " >&6; } -if ${ac_cv_header_stdc+:} false; then : +if test "${ac_cv_header_stdc+set}" = set; then : $as_echo_n "(cached) " >&6 else cat confdefs.h - <<_ACEOF >conftest.$ac_ext @@ -3948,7 +3953,7 @@ done for ac_header in sys/acl.h do : ac_fn_c_check_header_mongrel "$LINENO" "sys/acl.h" "ac_cv_header_sys_acl_h" "$ac_includes_default" -if test "x$ac_cv_header_sys_acl_h" = xyes; then : +if test "x$ac_cv_header_sys_acl_h" = x""yes; then : cat >>confdefs.h <<_ACEOF #define HAVE_SYS_ACL_H 1 _ACEOF @@ -3981,7 +3986,7 @@ if test -z "$CXX"; then set dummy $ac_tool_prefix$ac_prog; 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_CXX+:} false; then : +if test "${ac_cv_prog_CXX+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$CXX"; then @@ -4025,7 +4030,7 @@ do set dummy $ac_prog; 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_ac_ct_CXX+:} false; then : +if test "${ac_cv_prog_ac_ct_CXX+set}" = set; then : $as_echo_n "(cached) " >&6 else if test -n "$ac_ct_CXX"; then @@ -4103,7 +4108,7 @@ done { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C++ compiler" >&5 $as_echo_n "checking whether we are using the GNU C++ compiler... " >&6; } -if ${ac_cv_cxx_compiler_gnu+:} false; then : +if test "${ac_cv_cxx_compiler_gnu+set}" = set; then : $as_echo_n "(cached) " >&6 else cat confdefs.h - <<_ACEOF >conftest.$ac_ext @@ -4140,7 +4145,7 @@ ac_test_CXXFLAGS=${CXXFLAGS+set} ac_save_CXXFLAGS=$CXXFLAGS { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CXX accepts -g" >&5 $as_echo_n "checking whether $CXX accepts -g... " >&6; } -if ${ac_cv_prog_cxx_g+:} false; then : +if test "${ac_cv_prog_cxx_g+set}" = set; then : $as_echo_n "(cached) " >&6 else ac_save_cxx_werror_flag=$ac_cxx_werror_flag @@ -4231,7 +4236,7 @@ ac_compiler_gnu=$ac_cv_cxx_compiler_gnu { $as_echo "$as_me:${as_lineno-$LINENO}: checking how to run the C++ preprocessor" >&5 $as_echo_n "checking how to run the C++ preprocessor... " >&6; } if test -z "$CXXCPP"; then - if ${ac_cv_prog_CXXCPP+:} false; then : + if test "${ac_cv_prog_CXXCPP+set}" = set; then : $as_echo_n "(cached) " >&6 else # Double quotes because CXXCPP needs to be expanded @@ -4347,7 +4352,7 @@ else { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} as_fn_error $? "C++ preprocessor \"$CXXCPP\" fails sanity check -See \`config.log' for more details" "$LINENO" 5; } +See \`config.log' for more details" "$LINENO" 5 ; } fi ac_ext=cpp @@ -4360,7 +4365,7 @@ ac_compiler_gnu=$ac_cv_cxx_compiler_gnu for ac_header in selinux/selinux.h do : ac_fn_cxx_check_header_mongrel "$LINENO" "selinux/selinux.h" "ac_cv_header_selinux_selinux_h" "$ac_includes_default" -if test "x$ac_cv_header_selinux_selinux_h" = xyes; then : +if test "x$ac_cv_header_selinux_selinux_h" = x""yes; then : cat >>confdefs.h <<_ACEOF #define HAVE_SELINUX_SELINUX_H 1 _ACEOF @@ -4399,7 +4404,7 @@ else old_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS -I$stp_root/include" ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default" -if test "x$ac_cv_header_stp_c_interface_h" = xyes; then : +if test "x$ac_cv_header_stp_c_interface_h" = x""yes; then : else @@ -4412,7 +4417,7 @@ fi { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; } -if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then : +if test "${ac_cv_lib_stp_vc_setInterfaceFlags+set}" = set; then : $as_echo_n "(cached) " >&6 else ac_check_lib_save_LIBS=$LIBS @@ -4446,7 +4451,7 @@ LIBS=$ac_check_lib_save_LIBS fi { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; } -if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then : +if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = x""yes; then : cat >>confdefs.h <<_ACEOF #define HAVE_LIBSTP 1 _ACEOF @@ -4464,11 +4469,79 @@ 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 $as_echo_n "checking for $ac_word... " >&6; } -if ${ac_cv_path_RUNTEST+:} false; then : +if test "${ac_cv_path_RUNTEST+set}" = set; then : $as_echo_n "(cached) " >&6 else case $RUNTEST in @@ -4595,21 +4668,10 @@ $as_echo "$as_me: WARNING: cache variable $ac_var contains a newline" >&2;} ;; :end' >>confcache if diff "$cache_file" confcache >/dev/null 2>&1; then :; else if test -w "$cache_file"; then - if test "x$cache_file" != "x/dev/null"; then + test "x$cache_file" != "x/dev/null" && { $as_echo "$as_me:${as_lineno-$LINENO}: updating cache $cache_file" >&5 $as_echo "$as_me: updating cache $cache_file" >&6;} - if test ! -f "$cache_file" || test -h "$cache_file"; then - cat confcache >"$cache_file" - else - case $cache_file in #( - */* | ?:*) - mv -f confcache "$cache_file"$$ && - mv -f "$cache_file"$$ "$cache_file" ;; #( - *) - mv -f confcache "$cache_file" ;; - esac - fi - fi + cat confcache >$cache_file else { $as_echo "$as_me:${as_lineno-$LINENO}: not updating unwritable cache $cache_file" >&5 $as_echo "$as_me: not updating unwritable cache $cache_file" >&6;} @@ -4641,7 +4703,7 @@ LTLIBOBJS=$ac_ltlibobjs -: "${CONFIG_STATUS=./config.status}" +: ${CONFIG_STATUS=./config.status} ac_write_fail=0 ac_clean_files_save=$ac_clean_files ac_clean_files="$ac_clean_files $CONFIG_STATUS" @@ -4742,7 +4804,6 @@ fi IFS=" "" $as_nl" # Find who we are. Look in the path if we contain no directory separator. -as_myself= case $0 in #(( *[\\/]* ) as_myself=$0 ;; *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR @@ -5050,7 +5111,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1 # values after options handling. ac_log=" This file was extended by KLEE $as_me 0.01, which was -generated by GNU Autoconf 2.68. Invocation command line was +generated by GNU Autoconf 2.67. Invocation command line was CONFIG_FILES = $CONFIG_FILES CONFIG_HEADERS = $CONFIG_HEADERS @@ -5116,7 +5177,7 @@ cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`" ac_cs_version="\\ KLEE config.status 0.01 -configured by $0, generated by GNU Autoconf 2.68, +configured by $0, generated by GNU Autoconf 2.67, with options \\"\$ac_cs_config\\" Copyright (C) 2010 Free Software Foundation, Inc. @@ -5254,7 +5315,7 @@ do "tools/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS tools/Makefile" ;; "unittests/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS unittests/Makefile" ;; - *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;; + *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5 ;; esac done @@ -5277,10 +5338,9 @@ fi # after its creation but before its name has been assigned to `$tmp'. $debug || { - tmp= ac_tmp= + tmp= trap 'exit_status=$? - : "${ac_tmp:=$tmp}" - { test ! -d "$ac_tmp" || rm -fr "$ac_tmp"; } && exit $exit_status + { test -z "$tmp" || test ! -d "$tmp" || rm -fr "$tmp"; } && exit $exit_status ' 0 trap 'as_fn_exit 1' 1 2 13 15 } @@ -5288,13 +5348,12 @@ $debug || { tmp=`(umask 077 && mktemp -d "./confXXXXXX") 2>/dev/null` && - test -d "$tmp" + test -n "$tmp" && test -d "$tmp" } || { tmp=./conf$$-$RANDOM (umask 077 && mkdir "$tmp") } || as_fn_error $? "cannot create a temporary directory in ." "$LINENO" 5 -ac_tmp=$tmp # Set up the scripts for CONFIG_FILES section. # No need to generate them if there are no CONFIG_FILES. @@ -5316,7 +5375,7 @@ else ac_cs_awk_cr=$ac_cr fi -echo 'BEGIN {' >"$ac_tmp/subs1.awk" && +echo 'BEGIN {' >"$tmp/subs1.awk" && _ACEOF @@ -5344,7 +5403,7 @@ done rm -f conf$$subs.sh cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 -cat >>"\$ac_tmp/subs1.awk" <<\\_ACAWK && +cat >>"\$tmp/subs1.awk" <<\\_ACAWK && _ACEOF sed -n ' h @@ -5392,7 +5451,7 @@ t delim rm -f conf$$subs.awk cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 _ACAWK -cat >>"\$ac_tmp/subs1.awk" <<_ACAWK && +cat >>"\$tmp/subs1.awk" <<_ACAWK && for (key in S) S_is_set[key] = 1 FS = "" @@ -5424,7 +5483,7 @@ if sed "s/$ac_cr//" < /dev/null > /dev/null 2>&1; then sed "s/$ac_cr\$//; s/$ac_cr/$ac_cs_awk_cr/g" else cat -fi < "$ac_tmp/subs1.awk" > "$ac_tmp/subs.awk" \ +fi < "$tmp/subs1.awk" > "$tmp/subs.awk" \ || as_fn_error $? "could not setup config files machinery" "$LINENO" 5 _ACEOF @@ -5458,7 +5517,7 @@ fi # test -n "$CONFIG_FILES" # No need to generate them if there are no CONFIG_HEADERS. # This happens for instance with `./config.status Makefile'. if test -n "$CONFIG_HEADERS"; then -cat >"$ac_tmp/defines.awk" <<\_ACAWK || +cat >"$tmp/defines.awk" <<\_ACAWK || BEGIN { _ACEOF @@ -5470,8 +5529,8 @@ _ACEOF # handling of long lines. ac_delim='%!_!# ' for ac_last_try in false false :; do - ac_tt=`sed -n "/$ac_delim/p" confdefs.h` - if test -z "$ac_tt"; then + ac_t=`sed -n "/$ac_delim/p" confdefs.h` + if test -z "$ac_t"; then break elif $ac_last_try; then as_fn_error $? "could not make $CONFIG_HEADERS" "$LINENO" 5 @@ -5572,7 +5631,7 @@ do esac case $ac_mode$ac_tag in :[FHL]*:*);; - :L* | :C*:*) as_fn_error $? "invalid tag \`$ac_tag'" "$LINENO" 5;; + :L* | :C*:*) as_fn_error $? "invalid tag \`$ac_tag'" "$LINENO" 5 ;; :[FH]-) ac_tag=-:-;; :[FH]*) ac_tag=$ac_tag:$ac_tag.in;; esac @@ -5591,7 +5650,7 @@ do for ac_f do case $ac_f in - -) ac_f="$ac_tmp/stdin";; + -) ac_f="$tmp/stdin";; *) # Look for the file first in the build tree, then in the source tree # (if the path is not absolute). The absolute path cannot be DOS-style, # because $ac_f cannot contain `:'. @@ -5600,7 +5659,7 @@ do [\\/$]*) false;; *) test -f "$srcdir/$ac_f" && ac_f="$srcdir/$ac_f";; esac || - as_fn_error 1 "cannot find input file: \`$ac_f'" "$LINENO" 5;; + as_fn_error 1 "cannot find input file: \`$ac_f'" "$LINENO" 5 ;; esac case $ac_f in *\'*) ac_f=`$as_echo "$ac_f" | sed "s/'/'\\\\\\\\''/g"`;; esac as_fn_append ac_file_inputs " '$ac_f'" @@ -5626,8 +5685,8 @@ $as_echo "$as_me: creating $ac_file" >&6;} esac case $ac_tag in - *:-:* | *:-) cat >"$ac_tmp/stdin" \ - || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;; + *:-:* | *:-) cat >"$tmp/stdin" \ + || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;; esac ;; esac @@ -5752,22 +5811,21 @@ s&@abs_builddir@&$ac_abs_builddir&;t t s&@abs_top_builddir@&$ac_abs_top_builddir&;t t $ac_datarootdir_hack " -eval sed \"\$ac_sed_extra\" "$ac_file_inputs" | $AWK -f "$ac_tmp/subs.awk" \ - >$ac_tmp/out || as_fn_error $? "could not create $ac_file" "$LINENO" 5 +eval sed \"\$ac_sed_extra\" "$ac_file_inputs" | $AWK -f "$tmp/subs.awk" >$tmp/out \ + || as_fn_error $? "could not create $ac_file" "$LINENO" 5 test -z "$ac_datarootdir_hack$ac_datarootdir_seen" && - { ac_out=`sed -n '/\${datarootdir}/p' "$ac_tmp/out"`; test -n "$ac_out"; } && - { ac_out=`sed -n '/^[ ]*datarootdir[ ]*:*=/p' \ - "$ac_tmp/out"`; test -z "$ac_out"; } && + { ac_out=`sed -n '/\${datarootdir}/p' "$tmp/out"`; test -n "$ac_out"; } && + { ac_out=`sed -n '/^[ ]*datarootdir[ ]*:*=/p' "$tmp/out"`; test -z "$ac_out"; } && { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $ac_file contains a reference to the variable \`datarootdir' which seems to be undefined. Please make sure it is defined" >&5 $as_echo "$as_me: WARNING: $ac_file contains a reference to the variable \`datarootdir' which seems to be undefined. Please make sure it is defined" >&2;} - rm -f "$ac_tmp/stdin" + rm -f "$tmp/stdin" case $ac_file in - -) cat "$ac_tmp/out" && rm -f "$ac_tmp/out";; - *) rm -f "$ac_file" && mv "$ac_tmp/out" "$ac_file";; + -) cat "$tmp/out" && rm -f "$tmp/out";; + *) rm -f "$ac_file" && mv "$tmp/out" "$ac_file";; esac \ || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;; @@ -5778,20 +5836,20 @@ which seems to be undefined. Please make sure it is defined" >&2;} if test x"$ac_file" != x-; then { $as_echo "/* $configure_input */" \ - && eval '$AWK -f "$ac_tmp/defines.awk"' "$ac_file_inputs" - } >"$ac_tmp/config.h" \ + && eval '$AWK -f "$tmp/defines.awk"' "$ac_file_inputs" + } >"$tmp/config.h" \ || as_fn_error $? "could not create $ac_file" "$LINENO" 5 - if diff "$ac_file" "$ac_tmp/config.h" >/dev/null 2>&1; then + if diff "$ac_file" "$tmp/config.h" >/dev/null 2>&1; then { $as_echo "$as_me:${as_lineno-$LINENO}: $ac_file is unchanged" >&5 $as_echo "$as_me: $ac_file is unchanged" >&6;} else rm -f "$ac_file" - mv "$ac_tmp/config.h" "$ac_file" \ + mv "$tmp/config.h" "$ac_file" \ || as_fn_error $? "could not create $ac_file" "$LINENO" 5 fi else $as_echo "/* $configure_input */" \ - && eval '$AWK -f "$ac_tmp/defines.awk"' "$ac_file_inputs" \ + && eval '$AWK -f "$tmp/defines.awk"' "$ac_file_inputs" \ || as_fn_error $? "could not create -" "$LINENO" 5 fi ;; 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 4ce9714d..a751bc07 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -78,4 +78,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/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/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/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..b2cff8ba 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -47,6 +47,19 @@ #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" @@ -57,6 +70,13 @@ #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" @@ -67,11 +87,6 @@ #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 +105,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 +295,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), @@ -386,10 +462,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 @@ -557,20 +633,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 +692,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; } @@ -1380,7 +1469,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 +1675,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); @@ -1982,8 +2075,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 +2094,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 +2114,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 +2134,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 +2153,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 +2172,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 +2192,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 +2213,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 +2233,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 +2289,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 +2606,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/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 2fda5cba..6a5314ca 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -20,7 +20,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> diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 0d85afee..9e83b32c 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -20,6 +20,13 @@ #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" @@ -27,12 +34,16 @@ #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..344811d4 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -17,6 +17,13 @@ #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" @@ -27,6 +34,7 @@ #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif +#endif #include "llvm/ExecutionEngine/JIT.h" #include "llvm/ExecutionEngine/GenericValue.h" #include "llvm/Support/CallSite.h" 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..b5f38b2e 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,8 +43,10 @@ #include "llvm/InlineAsm.h" #include "llvm/Module.h" #include "llvm/Type.h" +#endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/CFG.h" +#include "llvm/Support/raw_os_ostream.h" #if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) #include "llvm/System/Process.h" #else @@ -401,7 +412,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/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/Module/Checks.cpp b/lib/Module/Checks.cpp index 67ed9aa7..c6fc9d3a 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,24 @@ #include "llvm/Instruction.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" +#include "llvm/Module.h" +#include "llvm/Type.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" + #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; diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp index d0ef52d0..9d4053d4 100644 --- a/lib/Module/InstructionInfoTable.cpp +++ b/lib/Module/InstructionInfoTable.cpp @@ -10,11 +10,18 @@ #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" +#endif +#include "llvm/Linker.h" #if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) #include "llvm/Assembly/AsmAnnotationWriter.h" #else diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 2f18c17e..56d06d30 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" @@ -21,20 +34,21 @@ #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 +60,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) @@ -181,6 +197,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 b646ca6e..ff13efda 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -22,13 +22,28 @@ #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" +#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" @@ -40,11 +55,6 @@ #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 #include "llvm/Transforms/Scalar.h" #include <llvm/Transforms/Utils/Cloning.h> @@ -193,6 +203,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 @@ -215,6 +226,7 @@ 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 . @@ -332,7 +344,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 @@ -353,14 +365,18 @@ 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 @@ -396,7 +412,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; @@ -406,7 +422,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 diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp index e5382c1a..e1a5d5b2 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" +#elif LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif #include <algorithm> diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 029540ae..43eef0b7 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -10,11 +10,23 @@ #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" +#endif + +#include "llvm/Linker.h" #if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) #include "llvm/Assembly/AsmAnnotationWriter.h" #else @@ -42,6 +54,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 +78,7 @@ Module *klee::linkWithLibrary(Module *module, } return linker.releaseModule(); +#endif } Function *klee::getDirectCallTarget(CallSite cs) { diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 6da9a2c1..83ee93ee 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -16,7 +16,6 @@ //===----------------------------------------------------------------------===// #include "klee/Config/Version.h" -#include "llvm/Module.h" #include "llvm/PassManager.h" #include "llvm/Analysis/Passes.h" #include "llvm/Analysis/LoopPass.h" @@ -27,11 +26,19 @@ #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" diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h index b0d4c363..0c294daa 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" @@ -76,7 +82,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, diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp index b5526f35..f15273e4 100644 --- a/lib/Module/RaiseAsm.cpp +++ b/lib/Module/RaiseAsm.cpp @@ -9,11 +9,16 @@ #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 +#endif + #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Host.h" 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/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/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..09dd7be5 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -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; @@ -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) { @@ -1096,6 +1234,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..389d7ae8 100644 --- a/runtime/POSIX/fd_32.c +++ b/runtime/POSIX/fd_32.c @@ -6,7 +6,19 @@ // 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" +#if defined(ENV32) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 2)) #define _LARGEFILE64_SOURCE #include "fd.h" @@ -41,6 +53,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 +77,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); } @@ -189,3 +221,5 @@ __attribute__((weak)) int lstat64(const char *path, struct stat64 *buf) { __attribute__((weak)) int fstat64(int fd, struct stat64 *buf) { return __fd_fstat(fd, buf); } + +#endif diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c index d0710caf..21a986aa 100644 --- a/runtime/POSIX/fd_64.c +++ b/runtime/POSIX/fd_64.c @@ -7,6 +7,17 @@ // //===----------------------------------------------------------------------===// +#if __GNUC__ +#if __x86_64__ || __ppc64__ +#define ENV64 +#else +#define ENV32 +#endif +#endif + + +#include "klee/Config/Version.h" +#if defined(ENV64) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 2)) #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" @@ -46,6 +57,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); } @@ -88,3 +113,5 @@ int getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) { } int __getdents64(unsigned int fd, struct dirent *dirp, unsigned int count) __attribute__((alias("getdents64"))); + +#endif 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/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/Runtime/POSIX/Futimesat.c b/test/Runtime/POSIX/Futimesat.c new file mode 100644 index 00000000..fd9ea0de --- /dev/null +++ b/test/Runtime/POSIX/Futimesat.c @@ -0,0 +1,43 @@ +// 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 <time.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/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..f5bbfaf0 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -45,6 +45,28 @@ 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 +233,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) { 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 7cd61788..0e576415 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -13,11 +13,17 @@ #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" @@ -25,6 +31,10 @@ #if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif +#endif +#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) +#include "llvm/ModuleProvider.h" +#endif #include "llvm/Bitcode/ReaderWriter.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ManagedStatic.h" @@ -1256,7 +1266,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; diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index 3c9bf89a..94529d56 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -61,9 +61,7 @@ void testOperation(Solver &solver, // replaced value is appropriated constrained. for (unsigned kid = 0; kid < T::numKids; kid++) { std::vector<Expr::CreateArg> partiallyConstantArgs(symbolicArgs); - for (unsigned i = 0; i < T::numKids; i++) - if (i==kid) - partiallyConstantArgs[i] = getConstant(value, operandWidth); + partiallyConstantArgs[kid] = getConstant(value, operandWidth); ref<Expr> expr = NotOptimizedExpr::create(EqExpr::create(partiallyConstantArgs[kid].expr, |