diff options
46 files changed, 2457 insertions, 1424 deletions
diff --git a/.travis.yml b/.travis.yml index 4e679237..42072095 100644 --- a/.travis.yml +++ b/.travis.yml @@ -19,14 +19,22 @@ env: # Check the matrix of: # LLVM : {2.9, 3.4} - # SOLVERS : {Z3, STP, STP:Z3} + # SOLVERS : {Z3, STP, STP:Z3, metaSMT} # STP_VERSION : {2.1.0, master} + # METASMT_DEFAULT : {btor, stp, z3} # UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled # with Asserts enabled. # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set matrix: + # Test experimental metaSMT support + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=stp KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=stp KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 + - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # Test experimental Z3 support - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 - LLVM_VERSION=2.9 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 @@ -65,18 +73,18 @@ before_install: # Set up the locations to get various packages from # We assume the Travis image uses Ubuntu 12.04 LTS ########################################################################### - - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' - - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.4 main" >> /etc/apt/sources.list.d/llvm.list' - - sudo sh -c 'echo "deb http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' - - sudo sh -c 'echo "deb-src http://llvm.org/apt/precise/ llvm-toolchain-precise-3.5 main" >> /etc/apt/sources.list.d/llvm.list' - - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list" + # Needed for Boost + - sudo add-apt-repository -y ppa:boost-latest # Needed for CMake - - sudo add-apt-repository -y ppa:ubuntu-sdk-team/ppa - sudo add-apt-repository -y ppa:kalakris/cmake + # Needed for LLVM + - sudo add-apt-repository -y ppa:h-rayflood/llvm # Needed for new libstdc++ and gcc4.8 - sudo add-apt-repository --yes ppa:ubuntu-toolchain-r/test/ - - wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add - + # Needed for Z3 + - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list" - wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key | sudo apt-key add - + # Update package information - sudo apt-get update ########################################################################### # Set up out of source build directory @@ -93,10 +101,6 @@ before_install: # Make gcc4.8 the default gcc version - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 20 - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.8 20 - # Make Clang3.4 the default clang version - - sudo apt-get install clang-3.4 - - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-3.4 20 - - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.4 20 # Install LLVM and the LLVM bitcode compiler we require to build KLEE - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh - ${KLEE_SRC}/.travis/install-tcmalloc.sh @@ -111,4 +115,4 @@ script: - ${KLEE_SRC}/.travis/testing-utils.sh - cd ../ # Build KLEE - - ${KLEE_SRC}/.travis/klee.sh + - travis_wait 30 ${KLEE_SRC}/.travis/klee.sh diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh index 13a7f140..1068d158 100755 --- a/.travis/install-llvm-and-runtime-compiler.sh +++ b/.travis/install-llvm-and-runtime-compiler.sh @@ -5,6 +5,8 @@ sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev if [ "${LLVM_VERSION}" != "2.9" ]; then sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION} + sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_VERSION} 20 + sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_VERSION} 20 else # Get llvm-gcc. We don't bother installing it wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2 diff --git a/.travis/klee.sh b/.travis/klee.sh index 296e1c83..98dbbc0d 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -51,6 +51,7 @@ fi ############################################################################### KLEE_Z3_CONFIGURE_OPTION="" KLEE_STP_CONFIGURE_OPTION="" +KLEE_METASMT_CONFIGURE_OPTION="" SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /') for solver in ${SOLVER_LIST}; do @@ -63,6 +64,10 @@ for solver in ${SOLVER_LIST}; do echo "Z3" KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr" ;; + metaSMT) + echo "metaSMT" + KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}" + ;; *) echo "Unknown solver ${solver}" exit 1 @@ -87,6 +92,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \ --with-llvmcxx=${KLEE_CXX} \ ${KLEE_STP_CONFIGURE_OPTION} \ ${KLEE_Z3_CONFIGURE_OPTION} \ + ${KLEE_METASMT_CONFIGURE_OPTION} \ ${KLEE_UCLIBC_CONFIGURE_OPTION} \ ${TCMALLOC_OPTION} \ CXXFLAGS="${COVERAGE_FLAGS}" \ diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh new file mode 100755 index 00000000..7a0d1eef --- /dev/null +++ b/.travis/metaSMT.sh @@ -0,0 +1,20 @@ +#!/bin/bash -x + +# Get Boost, Z3, libgmp +sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev + +# Clone +git clone git://github.com/hoangmle/metaSMT.git +cd metaSMT +git clone git://github.com/agra-uni-bremen/dependencies.git + +# Bootstrap +export BOOST_ROOT=/usr +sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack +./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-1.5.118 --build minisat-git -DZ3_DIR=/usr +sudo cp deps/boolector-1.5.118/lib/* /usr/lib/ # +sudo cp deps/minisat-git/lib/* /usr/lib/ # hack +sudo cp deps/stp-git-basic/lib/* /usr/lib/ # + +# Build +make -C build install diff --git a/.travis/solvers.sh b/.travis/solvers.sh index db717f2d..d64c1077 100755 --- a/.travis/solvers.sh +++ b/.travis/solvers.sh @@ -20,6 +20,10 @@ for solver in ${SOLVER_LIST}; do # Should we install libz3-dbg too? sudo apt-get -y install libz3 libz3-dev ;; + metaSMT) + echo "metaSMT" + ${KLEE_SRC}/.travis/metaSMT.sh + ;; *) echo "Unknown solver ${solver}" exit 1 diff --git a/Dockerfile b/Dockerfile index aa3ca6b6..ae5312d5 100644 --- a/Dockerfile +++ b/Dockerfile @@ -132,3 +132,8 @@ USER klee # Add KLEE binary directory to PATH RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/Release+Asserts/bin' >> /home/klee/.bashrc + +# Link klee to /usr/bin so that it can be used by docker run +USER root +RUN for exec in ${BUILD_DIR}/klee/Release+Asserts/bin/* ; do ln -s ${exec} /usr/bin/`basename ${exec}`; done +USER klee diff --git a/Makefile.common b/Makefile.common index 9bc850ba..cf7bdcf7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -78,11 +78,5 @@ ifeq ($(ENABLE_UCLIBC),1) endif # 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 +include $(PROJ_SRC_ROOT)/MetaSMT.mk diff --git a/Makefile.config.in b/Makefile.config.in index 7d3c05f6..d9572f7d 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -35,6 +35,7 @@ STP_LDFLAGS := @STP_LDFLAGS@ ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ +METASMT_DEFAULT_BACKEND := @METASMT_DEFAULT_BACKEND@ ENABLE_Z3 := @ENABLE_Z3@ Z3_CFLAGS := @Z3_CFLAGS@ @@ -50,6 +51,8 @@ HAVE_SELINUX := @HAVE_SELINUX@ HAVE_TCMALLOC := @HAVE_TCMALLOC@ TCMALLOC_LIB := @TCMALLOC_LIB@ +HAVE_ZLIB := @HAVE_ZLIB@ + RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@ RUNTIME_DISABLE_ASSERTIONS := @RUNTIME_DISABLE_ASSERTIONS@ RUNTIME_DEBUG_SYMBOLS := @RUNTIME_DEBUG_SYMBOLS@ diff --git a/MetaSMT.mk b/MetaSMT.mk index 94dd398a..817fa663 100644 --- a/MetaSMT.mk +++ b/MetaSMT.mk @@ -1,17 +1,13 @@ # This file contains common code for linking against MetaSMT # -# FIXME: This is a horribly fragile hack. -# Instead the detection of what solvers the build of MetaSMT supports should be -# done by the configure script and then the appropriate compiler flags should -# be emitted to Makefile.config for consumption here. +# Consume flags generated by metaSMT here. 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 \ - -L$(METASMT_ROOT)/../../deps/stp-svn/lib - CXX.Flags += -DBOOST_HAS_GCC_TR1 + LD.Flags += $(metaSMT_LDFLAGS) + CXX.Flags += -DMETASMT_DEFAULT_BACKEND_IS_$(METASMT_DEFAULT_BACKEND) + CXX.Flags += $(metaSMT_CXXFLAGS) + CXX.Flags += $(metaSMT_INCLUDES) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core + CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) + LIBS += $(metaSMT_LDLIBS) endif diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 2be02321..0fb8f8db 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -604,6 +604,41 @@ AS_IF([test "x$have_tcmalloc" = "xyes"], ]) dnl ************************************************************************** +dnl Test for zlib +dnl ************************************************************************** + +AC_ARG_WITH([zlib], + AS_HELP_STRING([--without-zlib], [Ignore presence of zlib and disable it (default=detect)])) + +AS_IF([test "x$with_zlib" != "xno"], + AC_CHECK_HEADERS([zlib.h], + [have_zlib=yes], [have_zlib=no]), + [have_zlib=no]) + +AS_IF([test "x$have_zlib" = "xyes"], + [ + AC_SEARCH_LIBS(deflateEnd, z, + [ + AC_SUBST(HAVE_ZLIB, 1) + if test "${ac_cv_search_zlib}" != "none required"; then + ZLIB_LIB=${ac_cv_search_zlib} + AC_SUBST(ZLIB_LIB) + fi + ], + [ + AC_MSG_WARN([Could not link with zlib]) + AC_SUBST(HAVE_ZLIB, 0) + ],) + + ], + [AS_IF([test "x$with_zlib" = "xyes"], + [AC_MSG_ERROR([zlib requested but not found])], + [ + AC_SUBST(HAVE_ZLIB, 0) + ]) +]) + +dnl ************************************************************************** dnl Find an install of STP dnl ************************************************************************** @@ -742,7 +777,6 @@ dnl ************************************************************************** AC_ARG_WITH(metasmt, AS_HELP_STRING([--with-metasmt], [Location of metaSMT installation directory]),,) - if test X$with_metasmt = X ; then ENABLE_METASMT=0 AC_MSG_NOTICE([Not using MetaSMT solver backend]) @@ -769,13 +803,51 @@ else AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API]) AC_SUBST(METASMT_ROOT,$metasmt_root) - AC_SUBST(REQUIRES_RTTI,[[1]]) ENABLE_METASMT=1 AC_MSG_NOTICE([Using MetaSMT solver backend]) fi AC_SUBST(ENABLE_METASMT) + +dnl ************************************************************************** +dnl User option to specify the default backend of metaSMT +dnl ************************************************************************** + +AC_ARG_WITH(metasmt-default-backend, + AS_HELP_STRING([--with-metasmt-default-backend], + [Default backend of metaSMT (btor|stp|z3, stp if unspecified)]),,) + +if test "X$with_metasmt_default_backend" != X ; then + if test "X$ENABLE_METASMT" != X1 ; then + AC_MSG_ERROR([--with-metasmt-default-backend requires metaSMT to be enabled]) + fi + if test "$with_metasmt_default_backend" == "btor" ; then + METASMT_DEFAULT_BACKEND=BTOR + AC_MSG_NOTICE([metaSMT uses Boolector as default backend]) + fi + if test "$with_metasmt_default_backend" == "z3" ; then + METASMT_DEFAULT_BACKEND=Z3 + AC_MSG_NOTICE([metaSMT uses Z3 as default backend]) + fi + if test "$with_metasmt_default_backend" == "stp" ; then + METASMT_DEFAULT_BACKEND=STP + AC_MSG_NOTICE([metaSMT uses STP as default backend]) + fi + if test "X$METASMT_DEFAULT_BACKEND" == X ; then + METASMT_DEFAULT_BACKEND=STP + AC_MSG_NOTICE([$with_metasmt_default_backend unsupported, metaSMT uses STP as default backend]) + fi +else + if test "X$ENABLE_METASMT" == X1 ; then + METASMT_DEFAULT_BACKEND=STP + AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default backend]) + fi +fi + +AC_SUBST(METASMT_DEFAULT_BACKEND) + + dnl ************************************************************************** dnl Check at least one solver backend is enabled dnl ************************************************************************** diff --git a/configure b/configure index 33893680..f6059789 100755 --- a/configure +++ b/configure @@ -624,6 +624,7 @@ ac_includes_default="\ ac_subst_vars='LTLIBOBJS LIBOBJS +METASMT_DEFAULT_BACKEND ENABLE_METASMT METASMT_ROOT Z3_LDFLAGS @@ -632,6 +633,8 @@ ENABLE_Z3 STP_LDFLAGS STP_CFLAGS ENABLE_STP +ZLIB_LIB +HAVE_ZLIB TCMALLOC_LIB HAVE_TCMALLOC CXXCPP @@ -736,9 +739,11 @@ with_uclibc enable_posix_runtime with_runtime with_tcmalloc +with_zlib with_stp with_z3 with_metasmt +with_metasmt_default_backend ' ac_precious_vars='build_alias host_alias @@ -1390,9 +1395,14 @@ Optional Packages: (default [Release+Asserts]) --without-tcmalloc Ignore presence of tcmalloc and disable it (default=detect) + --without-zlib Ignore presence of zlib and disable it + (default=detect) --with-stp Location of STP installation directory --with-z3 Location of Z3 installation directory --with-metasmt Location of metaSMT installation directory + --with-metasmt-default-backend + Default backend of metaSMT (btor|stp|z3, stp if + unspecified) Some influential environment variables: CC C compiler command @@ -5029,6 +5039,119 @@ fi fi + +# Check whether --with-zlib was given. +if test "${with_zlib+set}" = set; then : + withval=$with_zlib; +fi + + +if test "x$with_zlib" != "xno"; then : + for ac_header in zlib.h +do : + ac_fn_cxx_check_header_mongrel "$LINENO" "zlib.h" "ac_cv_header_zlib_h" "$ac_includes_default" +if test "x$ac_cv_header_zlib_h" = xyes; then : + cat >>confdefs.h <<_ACEOF +#define HAVE_ZLIB_H 1 +_ACEOF + have_zlib=yes +else + have_zlib=no +fi + +done + +else + have_zlib=no +fi + +if test "x$have_zlib" = "xyes"; then : + + { $as_echo "$as_me:${as_lineno-$LINENO}: checking for library containing deflateEnd" >&5 +$as_echo_n "checking for library containing deflateEnd... " >&6; } +if ${ac_cv_search_deflateEnd+:} false; then : + $as_echo_n "(cached) " >&6 +else + ac_func_search_save_LIBS=$LIBS +cat confdefs.h - <<_ACEOF >conftest.$ac_ext +/* end confdefs.h. */ + +/* Override any GCC internal prototype to avoid an error. + Use char because int might match the return type of a GCC + builtin and then its argument prototype would still apply. */ +#ifdef __cplusplus +extern "C" +#endif +char deflateEnd (); +int +main () +{ +return deflateEnd (); + ; + return 0; +} +_ACEOF +for ac_lib in '' z; do + if test -z "$ac_lib"; then + ac_res="none required" + else + ac_res=-l$ac_lib + LIBS="-l$ac_lib $ac_func_search_save_LIBS" + fi + if ac_fn_cxx_try_link "$LINENO"; then : + ac_cv_search_deflateEnd=$ac_res +fi +rm -f core conftest.err conftest.$ac_objext \ + conftest$ac_exeext + if ${ac_cv_search_deflateEnd+:} false; then : + break +fi +done +if ${ac_cv_search_deflateEnd+:} false; then : + +else + ac_cv_search_deflateEnd=no +fi +rm conftest.$ac_ext +LIBS=$ac_func_search_save_LIBS +fi +{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_search_deflateEnd" >&5 +$as_echo "$ac_cv_search_deflateEnd" >&6; } +ac_res=$ac_cv_search_deflateEnd +if test "$ac_res" != no; then : + test "$ac_res" = "none required" || LIBS="$ac_res $LIBS" + + HAVE_ZLIB=1 + + if test "${ac_cv_search_zlib}" != "none required"; then + ZLIB_LIB=${ac_cv_search_zlib} + + fi + +else + + { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Could not link with zlib" >&5 +$as_echo "$as_me: WARNING: Could not link with zlib" >&2;} + HAVE_ZLIB=0 + + +fi + + + +else + if test "x$with_zlib" = "xyes"; then : + as_fn_error $? "zlib requested but not found" "$LINENO" 5 +else + + HAVE_ZLIB=0 + + +fi + +fi + + ENABLE_STP=0 # Check whether --with-stp was given. @@ -5324,7 +5447,6 @@ if test "${with_metasmt+set}" = set; then : withval=$with_metasmt; fi - if test X$with_metasmt = X ; then ENABLE_METASMT=0 { $as_echo "$as_me:${as_lineno-$LINENO}: Not using MetaSMT solver backend" >&5 @@ -5384,8 +5506,6 @@ $as_echo "#define ENABLE_METASMT 1" >>confdefs.h METASMT_ROOT=$metasmt_root - REQUIRES_RTTI=1 - ENABLE_METASMT=1 { $as_echo "$as_me:${as_lineno-$LINENO}: Using MetaSMT solver backend" >&5 $as_echo "$as_me: Using MetaSMT solver backend" >&6;} @@ -5394,6 +5514,50 @@ fi + + +# Check whether --with-metasmt-default-backend was given. +if test "${with_metasmt_default_backend+set}" = set; then : + withval=$with_metasmt_default_backend; +fi + + +if test "X$with_metasmt_default_backend" != X ; then + if test "X$ENABLE_METASMT" != X1 ; then + as_fn_error $? "--with-metasmt-default-backend requires metaSMT to be enabled" "$LINENO" 5 + fi + if test "$with_metasmt_default_backend" == "btor" ; then + METASMT_DEFAULT_BACKEND=BTOR + { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Boolector as default backend" >&5 +$as_echo "$as_me: metaSMT uses Boolector as default backend" >&6;} + fi + if test "$with_metasmt_default_backend" == "z3" ; then + METASMT_DEFAULT_BACKEND=Z3 + { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Z3 as default backend" >&5 +$as_echo "$as_me: metaSMT uses Z3 as default backend" >&6;} + fi + if test "$with_metasmt_default_backend" == "stp" ; then + METASMT_DEFAULT_BACKEND=STP + { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses STP as default backend" >&5 +$as_echo "$as_me: metaSMT uses STP as default backend" >&6;} + fi + if test "X$METASMT_DEFAULT_BACKEND" == X ; then + METASMT_DEFAULT_BACKEND=STP + { $as_echo "$as_me:${as_lineno-$LINENO}: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&5 +$as_echo "$as_me: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&6;} + fi +else + if test "X$ENABLE_METASMT" == X1 ; then + METASMT_DEFAULT_BACKEND=STP + { $as_echo "$as_me:${as_lineno-$LINENO}: No solver specified, metaSMT uses STP as default backend" >&5 +$as_echo "$as_me: No solver specified, metaSMT uses STP as default backend" >&6;} + fi +fi + + + + + if test "X$ENABLE_STP$ENABLE_Z3$ENABLE_METASMT" == X000 ; then as_fn_error $? "At least one solver backend must be enabled, try using --with-stp, --with-z3 or --with-metasmt" "$LINENO" 5 fi diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 008b2f90..87d6ee75 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -69,6 +69,9 @@ /* Z3 needs a Z3_context passed to Z3_get_error_msg() */ #undef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT +/* Define to 1 if you have the <zlib.h> header file. */ +#undef HAVE_ZLIB_H + /* Define to empty or 'const' depending on how SELinux qualifies its security context parameters. */ #undef KLEE_SELINUX_CTX_CONST diff --git a/include/klee/Internal/Support/CompressionStream.h b/include/klee/Internal/Support/CompressionStream.h new file mode 100644 index 00000000..fda68d89 --- /dev/null +++ b/include/klee/Internal/Support/CompressionStream.h @@ -0,0 +1,46 @@ +//===-- CompressionStream.h --------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_ +#define INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_ + +#include "llvm/Support/raw_ostream.h" +#include "zlib.h" + +namespace klee { +const size_t BUFSIZE = 128 * 1024; + +class compressed_fd_ostream : public llvm::raw_ostream { + int FD; + uint8_t buffer[BUFSIZE]; + z_stream strm; + uint64_t pos; + + /// write_impl - See raw_ostream::write_impl. + virtual void write_impl(const char *Ptr, size_t Size); + void write_file(const char *Ptr, size_t Size); + + virtual uint64_t current_pos() const { return pos; } + + void flush_compressed_data(); + void writeFullCompressedData(); + +public: + /// compressed_fd_ostream - Open the specified file for writing. If an error + /// occurs, information about the error is put into ErrorInfo, and the stream + /// should be immediately destroyed; the string will be empty if no error + /// occurred. This allows optional flags to control how the file will be + /// opened. + compressed_fd_ostream(const char *Filename, std::string &ErrorInfo); + + ~compressed_fd_ostream(); +}; +} + +#endif /* INCLUDE_KLEE_INTERNAL_SUPPORT_COMPRESSIONSTREAM_H_ */ diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index a0fbda03..20c190a5 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -84,16 +84,30 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( #ifdef ENABLE_METASMT +#ifdef METASMT_DEFAULT_BACKEND_IS_BTOR +#define METASMT_DEFAULT_BACKEND_STR "(default = btor)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_BOOLECTOR +#elif METASMT_DEFAULT_BACKEND_IS_Z3 +#define METASMT_DEFAULT_BACKEND_STR "(default = z3)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3 +#else +#define METASMT_DEFAULT_BACKEND_STR "(default = stp)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP +#endif + llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend( "metasmt-backend", - llvm::cl::desc("Specify the MetaSMT solver backend type (default=STP)."), + llvm::cl::desc("Specify the MetaSMT solver backend type " METASMT_DEFAULT_BACKEND_STR), llvm::cl::values( 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_STP)); + llvm::cl::init(METASMT_DEFAULT_BACKEND)); + +#undef METASMT_DEFAULT_BACKEND +#undef METASMT_DEFAULT_BACKEND_STR #endif /* ENABLE_METASMT */ diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 25418c13..811e52c3 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -58,6 +58,8 @@ bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr, if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) { const MemoryObject *mo = res->first; + // Check if the provided address is between start and end of the object + // [mo->address, mo->address + mo->size) or the object is a 0-sized object. if ((mo->size==0 && address==mo->address) || (address - mo->address < mo->size)) { result = *res; diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 6aeaa833..30d20266 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -370,8 +370,8 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const { out << ai->getName().str(); // XXX should go through function - ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; - if (isa<ConstantExpr>(value)) + ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; + if (value.get() && isa<ConstantExpr>(value)) out << "=" << value; } out << ")"; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ff346487..d755403f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -89,6 +89,10 @@ #include "llvm/IR/CallSite.h" #endif +#ifdef HAVE_ZLIB_H +#include "klee/Internal/Support/CompressionStream.h" +#endif + #include <cassert> #include <algorithm> #include <iomanip> @@ -158,6 +162,11 @@ namespace { "[inst_id]"), clEnumValEnd), llvm::cl::CommaSeparated); +#ifdef HAVE_ZLIB_H + cl::opt<bool> DebugCompressInstructions( + "debug-compress-instructions", cl::init(false), + cl::desc("Compress the logged instructions in gzip format.")); +#endif cl::opt<bool> DebugCheckForImpliedValues("debug-check-for-implied-values"); @@ -267,6 +276,25 @@ namespace { cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"), cl::init(0)); + cl::list<Executor::TerminateReason> + ExitOnErrorType("exit-on-error-type", + cl::desc("Stop execution after reaching a specified condition. (default=off)"), + cl::values( + clEnumValN(Executor::Abort, "Abort", "The program crashed"), + clEnumValN(Executor::Assert, "Assert", "An assertion was hit"), + clEnumValN(Executor::Exec, "Exec", "Trying to execute an unexpected instruction"), + clEnumValN(Executor::External, "External", "External objects referenced"), + clEnumValN(Executor::Free, "Free", "Freeing invalid memory"), + clEnumValN(Executor::Model, "Model", "Memory model limit hit"), + clEnumValN(Executor::Overflow, "Overflow", "An overflow occurred"), + clEnumValN(Executor::Ptr, "Ptr", "Pointer error"), + clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"), + clEnumValN(Executor::ReportError, "ReportError", "klee_report_error called"), + clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"), + clEnumValN(Executor::Unhandled, "Unhandled", "Unhandled instruction hit"), + clEnumValEnd), + cl::ZeroOrMore); + cl::opt<unsigned int> StopAfterNInstructions("stop-after-n-instructions", cl::desc("Stop execution after specified number of instructions (default=0 (off))"), @@ -298,6 +326,21 @@ namespace klee { RNG theRNG; } +const char *Executor::TerminateReasonNames[] = { + [ Abort ] = "abort", + [ Assert ] = "assert", + [ Exec ] = "exec", + [ External ] = "external", + [ Free ] = "free", + [ Model ] = "model", + [ Overflow ] = "overflow", + [ Ptr ] = "ptr", + [ ReadOnly ] = "readonly", + [ ReportError ] = "reporterror", + [ User ] = "user", + [ Unhandled ] = "xxx", +}; + Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), kmodule(0), interpreterHandler(ih), searcher(0), externalDispatcher(new ExternalDispatcher()), statsTracker(0), @@ -332,6 +375,10 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) std::string debug_file_name = interpreterHandler->getOutputFilename("instructions.txt"); std::string ErrorInfo; +#ifdef HAVE_ZLIB_H + if (!DebugCompressInstructions) { +#endif + #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), @@ -339,6 +386,16 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo); #endif +#ifdef HAVE_ZLIB_H + } else { + debugInstFile = new compressed_fd_ostream( + (debug_file_name + ".gz").c_str(), ErrorInfo); + } +#endif + if (ErrorInfo != "") { + klee_error("Could not open file %s : %s", debug_file_name.c_str(), + ErrorInfo.c_str()); + } } } @@ -364,7 +421,7 @@ const Module *Executor::setModule(llvm::Module *module, kmodule->prepare(opts, interpreterHandler); specialFunctionHandler->bind(); - if (StatsTracker::useStatistics()) { + if (StatsTracker::useStatistics() || userSearcherRequiresMD2U()) { statsTracker = new StatsTracker(*this, interpreterHandler->getOutputFilename("assembly.ll"), @@ -539,7 +596,13 @@ void Executor::initializeGlobals(ExecutionState &state) { // hack where we check the object file information. LLVM_TYPE_Q Type *ty = i->getType()->getElementType(); - uint64_t size = kmodule->targetData->getTypeStoreSize(ty); + uint64_t size = 0; + if (ty->isSized()) { + size = kmodule->targetData->getTypeStoreSize(ty); + } else { + klee_warning("Type for %.*s is not sized", (int)i->getName().size(), + i->getName().data()); + } // XXX - DWD - hardcode some things until we decide how to fix. #ifndef WINDOWS @@ -553,9 +616,8 @@ void Executor::initializeGlobals(ExecutionState &state) { #endif if (size == 0) { - llvm::errs() << "Unable to find size for global variable: " - << i->getName() - << " (use will result in out of bounds access)\n"; + klee_warning("Unable to find size for global variable: %.*s (use will result in out of bounds access)", + (int)i->getName().size(), i->getName().data()); } MemoryObject *mo = memory->allocate(size, false, true, i); @@ -642,7 +704,7 @@ void Executor::branch(ExecutionState &state, for (unsigned i=1; i<N; ++i) { ExecutionState *es = result[theRNG.getInt32() % i]; ExecutionState *ns = es->branch(); - addedStates.insert(ns); + addedStates.push_back(ns); result.push_back(ns); es->ptreeNode->data = 0; std::pair<PTree::Node*,PTree::Node*> res = @@ -860,7 +922,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { ++stats::forks; falseState = trueState->branch(); - addedStates.insert(falseState); + addedStates.push_back(falseState); if (RandomizeFork && theRNG.getBool()) std::swap(trueState, falseState); @@ -1212,8 +1274,10 @@ void Executor::executeCall(ExecutionState &state, // ExecutionState::varargs case Intrinsic::vastart: { StackFrame &sf = state.stack.back(); - assert(sf.varargs && - "vastart called in function with no vararg object"); + + // varargs can be zero if no varargs were provided + if (!sf.varargs) + return; // FIXME: This is really specific to the architecture, not the pointer // size. This happens to work fir x86-32 and x86-64, however. @@ -1270,13 +1334,13 @@ void Executor::executeCall(ExecutionState &state, KFunction *kf = kmodule->functionMap[f]; state.pushFrame(state.prevPC, kf); state.pc = kf->instructions; - + if (statsTracker) statsTracker->framePushed(state, &state.stack[state.stack.size()-2]); - + // TODO: support "byval" parameter attribute // TODO: support zeroext, signext, sret attributes - + unsigned callingArgs = arguments.size(); unsigned funcArgs = f->arg_size(); if (!f->isVarArg()) { @@ -1284,68 +1348,76 @@ void Executor::executeCall(ExecutionState &state, klee_warning_once(f, "calling %s with extra arguments.", f->getName().data()); } else if (callingArgs < funcArgs) { - terminateStateOnError(state, "calling function with too few arguments", - "user.err"); + terminateStateOnError(state, "calling function with too few arguments", + User); return; } } else { Expr::Width WordSize = Context::get().getPointerWidth(); if (callingArgs < funcArgs) { - terminateStateOnError(state, "calling function with too few arguments", - "user.err"); + terminateStateOnError(state, "calling function with too few arguments", + User); return; } - + StackFrame &sf = state.stack.back(); unsigned size = 0; + bool requires16ByteAlignment = false; for (unsigned i = funcArgs; i < callingArgs; i++) { // FIXME: This is really specific to the architecture, not the pointer - // size. This happens to work fir x86-32 and x86-64, however. + // size. This happens to work for x86-32 and x86-64, however. if (WordSize == Expr::Int32) { size += Expr::getMinBytesForWidth(arguments[i]->getWidth()); } else { Expr::Width argWidth = arguments[i]->getWidth(); - // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a 16 - // byte boundary if alignment needed by type exceeds 8 byte boundary. + // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a + // 16 byte boundary if alignment needed by type exceeds 8 byte + // boundary. // // Alignment requirements for scalar types is the same as their size if (argWidth > Expr::Int64) { size = llvm::RoundUpToAlignment(size, 16); + requires16ByteAlignment = true; } size += llvm::RoundUpToAlignment(argWidth, WordSize) / 8; } } - MemoryObject *mo = sf.varargs = memory->allocate(size, true, false, - state.prevPC->inst); - if (!mo) { + MemoryObject *mo = sf.varargs = + memory->allocate(size, true, false, state.prevPC->inst, + (requires16ByteAlignment ? 16 : 8)); + if (!mo && size) { terminateStateOnExecError(state, "out of memory (varargs)"); return; } - if ((WordSize == Expr::Int64) && (mo->address & 15)) { - // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes. - klee_warning_once(0, "While allocating varargs: malloc did not align to 16 bytes."); - } + if (mo) { + if ((WordSize == Expr::Int64) && (mo->address & 15) && + requires16ByteAlignment) { + // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes. + klee_warning_once( + 0, "While allocating varargs: malloc did not align to 16 bytes."); + } - ObjectState *os = bindObjectInState(state, mo, true); - unsigned offset = 0; - for (unsigned i = funcArgs; i < callingArgs; i++) { - // FIXME: This is really specific to the architecture, not the pointer - // size. This happens to work fir x86-32 and x86-64, however. - if (WordSize == Expr::Int32) { - os->write(offset, arguments[i]); - offset += Expr::getMinBytesForWidth(arguments[i]->getWidth()); - } else { - assert(WordSize == Expr::Int64 && "Unknown word size!"); + ObjectState *os = bindObjectInState(state, mo, true); + unsigned offset = 0; + for (unsigned i = funcArgs; i < callingArgs; i++) { + // FIXME: This is really specific to the architecture, not the pointer + // size. This happens to work for x86-32 and x86-64, however. + if (WordSize == Expr::Int32) { + os->write(offset, arguments[i]); + offset += Expr::getMinBytesForWidth(arguments[i]->getWidth()); + } else { + assert(WordSize == Expr::Int64 && "Unknown word size!"); - Expr::Width argWidth = arguments[i]->getWidth(); - if (argWidth > Expr::Int64) { - offset = llvm::RoundUpToAlignment(offset, 16); + Expr::Width argWidth = arguments[i]->getWidth(); + if (argWidth > Expr::Int64) { + offset = llvm::RoundUpToAlignment(offset, 16); + } + os->write(offset, arguments[i]); + offset += llvm::RoundUpToAlignment(argWidth, WordSize) / 8; } - os->write(offset, arguments[i]); - offset += llvm::RoundUpToAlignment(argWidth, WordSize) / 8; } } } @@ -1586,58 +1658,108 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { #endif transferToBasicBlock(si->getSuccessor(index), si->getParent(), state); } else { - std::map<BasicBlock*, ref<Expr> > targets; - ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool); -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); - i != e; ++i) { + // Handle possible different branch targets + + // We have the following assumptions: + // - each case value is mutual exclusive to all other values including the + // default value + // - order of case branches is based on the order of the expressions of + // the scase values, still default is handled last + std::vector<BasicBlock *> bbOrder; + std::map<BasicBlock *, ref<Expr> > branchTargets; + + std::map<ref<Expr>, BasicBlock *> expressionOrder; + + // Iterate through all non-default cases and order them by expressions +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); i != e; + ++i) { ref<Expr> value = evalConstant(i.getCaseValue()); #else - for (unsigned i=1, cases = si->getNumCases(); i<cases; ++i) { + for (unsigned i = 1, cases = si->getNumCases(); i < cases; ++i) { ref<Expr> value = evalConstant(si->getCaseValue(i)); #endif - ref<Expr> match = EqExpr::create(cond, value); - isDefault = AndExpr::create(isDefault, Expr::createIsZero(match)); + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + BasicBlock *caseSuccessor = i.getCaseSuccessor(); +#else + BasicBlock *caseSuccessor = si->getSuccessor(i); +#endif + expressionOrder.insert(std::make_pair(value, caseSuccessor)); + } + + // Track default branch values + ref<Expr> defaultValue = ConstantExpr::alloc(1, Expr::Bool); + + // iterate through all non-default cases but in order of the expressions + for (std::map<ref<Expr>, BasicBlock *>::iterator + it = expressionOrder.begin(), + itE = expressionOrder.end(); + it != itE; ++it) { + ref<Expr> match = EqExpr::create(cond, it->first); + + // Make sure that the default value does not contain this target's value + defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match)); + + // Check if control flow could take this case bool result; bool success = solver->mayBeTrue(state, match, result); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (result) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - BasicBlock *caseSuccessor = i.getCaseSuccessor(); -#else - BasicBlock *caseSuccessor = si->getSuccessor(i); -#endif - std::map<BasicBlock*, ref<Expr> >::iterator it = - targets.insert(std::make_pair(caseSuccessor, - ConstantExpr::alloc(0, Expr::Bool))).first; - - it->second = OrExpr::create(match, it->second); + BasicBlock *caseSuccessor = it->second; + + // Handle the case that a basic block might be the target of multiple + // switch cases. + // Currently we generate an expression containing all switch-case + // values for the same target basic block. We spare us forking too + // many times but we generate more complex condition expressions + // TODO Add option to allow to choose between those behaviors + std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> res = + branchTargets.insert(std::make_pair( + caseSuccessor, ConstantExpr::alloc(0, Expr::Bool))); + + res.first->second = OrExpr::create(match, res.first->second); + + // Only add basic blocks which have not been target of a branch yet + if (res.second) { + bbOrder.push_back(caseSuccessor); + } } } + + // Check if control could take the default case bool res; - bool success = solver->mayBeTrue(state, isDefault, res); + bool success = solver->mayBeTrue(state, defaultValue, res); assert(success && "FIXME: Unhandled solver failure"); (void) success; - if (res) - targets.insert(std::make_pair(si->getDefaultDest(), isDefault)); - + if (res) { + std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> ret = + branchTargets.insert( + std::make_pair(si->getDefaultDest(), defaultValue)); + if (ret.second) { + bbOrder.push_back(si->getDefaultDest()); + } + } + + // Fork the current state with each state having one of the possible + // successors of this switch std::vector< ref<Expr> > conditions; - for (std::map<BasicBlock*, ref<Expr> >::iterator it = - targets.begin(), ie = targets.end(); - it != ie; ++it) - conditions.push_back(it->second); - + for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(), + ie = bbOrder.end(); + it != ie; ++it) { + conditions.push_back(branchTargets[*it]); + } std::vector<ExecutionState*> branches; branch(state, conditions, branches); - + std::vector<ExecutionState*>::iterator bit = branches.begin(); - for (std::map<BasicBlock*, ref<Expr> >::iterator it = - targets.begin(), ie = targets.end(); + for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(), + ie = bbOrder.end(); it != ie; ++it) { ExecutionState *es = *bit; if (es) - transferToBasicBlock(it->first, bb, *es); + transferToBasicBlock(*it, bb, *es); ++bit; } } @@ -2428,7 +2550,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { case Instruction::InsertElement: case Instruction::ShuffleVector: terminateStateOnError(state, "XXX vector instructions unhandled", - "xxx.err"); + Unhandled); break; default: @@ -2444,9 +2566,9 @@ void Executor::updateStates(ExecutionState *current) { states.insert(addedStates.begin(), addedStates.end()); addedStates.clear(); - - for (std::set<ExecutionState*>::iterator - it = removedStates.begin(), ie = removedStates.end(); + + for (std::vector<ExecutionState *>::iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::iterator it2 = states.find(es); @@ -2531,7 +2653,9 @@ void Executor::checkMemoryUsage() { // We need to avoid calling GetTotalMallocUsage() 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. - unsigned mbs = util::GetTotalMallocUsage() >> 20; + unsigned mbs = (util::GetTotalMallocUsage() >> 20) + + (memory->getUsedDeterministicSize() >> 20); + if (mbs > MaxMemory) { if (mbs > MaxMemory + 100) { // just guess at how many to kill @@ -2557,6 +2681,20 @@ void Executor::checkMemoryUsage() { } } +void Executor::doDumpStates() { + if (!DumpStatesOnHalt || states.empty()) + return; + klee_message("halting execution, dumping remaining states"); + for (std::set<ExecutionState *>::iterator it = states.begin(), + ie = states.end(); + it != ie; ++it) { + ExecutionState &state = **it; + stepInstruction(state); // keep stats rolling + terminateStateEarly(state, "Execution halting."); + } + updateStates(0); +} + void Executor::run(ExecutionState &initialState) { bindModuleConstants(); @@ -2577,7 +2715,10 @@ void Executor::run(ExecutionState &initialState) { double lastTime, startTime = lastTime = util::getWallTime(); ExecutionState *lastState = 0; while (!seedMap.empty()) { - if (haltExecution) goto dump; + if (haltExecution) { + doDumpStates(); + return; + } std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it = seedMap.upper_bound(lastState); @@ -2626,13 +2767,16 @@ void Executor::run(ExecutionState &initialState) { (*it)->weight = 1.; } - if (OnlySeed) - goto dump; + if (OnlySeed) { + doDumpStates(); + return; + } } searcher = constructUserSearcher(*this); - searcher->update(0, states, std::set<ExecutionState*>()); + std::vector<ExecutionState *> newStates(states.begin(), states.end()); + searcher->update(0, newStates, std::vector<ExecutionState *>()); while (!states.empty() && !haltExecution) { ExecutionState &state = searcher->selectState(); @@ -2649,19 +2793,8 @@ void Executor::run(ExecutionState &initialState) { delete searcher; searcher = 0; - - dump: - if (DumpStatesOnHalt && !states.empty()) { - llvm::errs() << "KLEE: halting execution, dumping remaining states\n"; - for (std::set<ExecutionState*>::iterator - it = states.begin(), ie = states.end(); - it != ie; ++it) { - ExecutionState &state = **it; - stepInstruction(state); // keep stats rolling - terminateStateEarly(state, "Execution halting."); - } - updateStates(0); - } + + doDumpStates(); } std::string Executor::getAddressInfo(ExecutionState &state, @@ -2722,11 +2855,12 @@ void Executor::terminateState(ExecutionState &state) { interpreterHandler->incPathsExplored(); - std::set<ExecutionState*>::iterator it = addedStates.find(&state); + std::vector<ExecutionState *>::iterator it = + std::find(addedStates.begin(), addedStates.end(), &state); if (it==addedStates.end()) { state.pc = state.prevPC; - removedStates.insert(&state); + removedStates.push_back(&state); } else { // never reached searcher, just delete immediately std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 = @@ -2797,8 +2931,21 @@ const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const Execut } return *ii; } + +bool Executor::shouldExitOn(enum TerminateReason termReason) { + std::vector<TerminateReason>::iterator s = ExitOnErrorType.begin(); + std::vector<TerminateReason>::iterator e = ExitOnErrorType.end(); + + for (; s != e; ++s) + if (termReason == *s) + return true; + + return false; +} + void Executor::terminateStateOnError(ExecutionState &state, const llvm::Twine &messaget, + enum TerminateReason termReason, const char *suffix, const llvm::Twine &info) { std::string message = messaget.str(); @@ -2831,10 +2978,20 @@ void Executor::terminateStateOnError(ExecutionState &state, if (info_str != "") msg << "Info: \n" << info_str; + std::string suffix_buf; + if (!suffix) { + suffix_buf = TerminateReasonNames[termReason]; + suffix_buf += ".err"; + suffix = suffix_buf.c_str(); + } + interpreterHandler->processTestCase(state, msg.str().c_str(), suffix); } terminateState(state); + + if (shouldExitOn(termReason)) + haltExecution = true; } // XXX shoot me @@ -2857,7 +3014,7 @@ void Executor::callExternalFunction(ExecutionState &state, if (NoExternals && !okExternals.count(function->getName())) { llvm::errs() << "KLEE:ERROR: Calling not-OK external function : " << function->getName().str() << "\n"; - terminateStateOnError(state, "externals disallowed", "user.err"); + terminateStateOnError(state, "externals disallowed", User); return; } @@ -2915,13 +3072,13 @@ void Executor::callExternalFunction(ExecutionState &state, bool success = externalDispatcher->executeCall(function, target->inst, args); if (!success) { terminateStateOnError(state, "failed external call: " + function->getName(), - "external.err"); + External); return; } if (!state.addressSpace.copyInConcretes()) { terminateStateOnError(state, "external modified read-only object", - "external.err"); + External); return; } @@ -3075,10 +3232,8 @@ void Executor::executeAlloc(ExecutionState &state, ExprPPrinter::printOne(info, " size expr", size); info << " concretization : " << example << "\n"; info << " unbound example: " << tmp << "\n"; - terminateStateOnError(*hugeSize.second, - "concretized symbolic size", - "model.err", - info.str()); + terminateStateOnError(*hugeSize.second, "concretized symbolic size", + Model, NULL, info.str()); } } } @@ -3105,14 +3260,10 @@ void Executor::executeFree(ExecutionState &state, ie = rl.end(); it != ie; ++it) { const MemoryObject *mo = it->first.first; if (mo->isLocal) { - terminateStateOnError(*it->second, - "free of alloca", - "free.err", + terminateStateOnError(*it->second, "free of alloca", Free, NULL, getAddressInfo(*it->second, address)); } else if (mo->isGlobal) { - terminateStateOnError(*it->second, - "free of global", - "free.err", + terminateStateOnError(*it->second, "free of global", Free, NULL, getAddressInfo(*it->second, address)); } else { it->second->addressSpace.unbindObject(mo); @@ -3147,10 +3298,8 @@ void Executor::resolveExact(ExecutionState &state, } if (unbound) { - terminateStateOnError(*unbound, - "memory error: invalid pointer: " + name, - "ptr.err", - getAddressInfo(*unbound, p)); + terminateStateOnError(*unbound, "memory error: invalid pointer: " + name, + Ptr, NULL, getAddressInfo(*unbound, p)); } } @@ -3205,9 +3354,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, const ObjectState *os = op.second; if (isWrite) { if (os->readOnly) { - terminateStateOnError(state, - "memory error: object read only", - "readonly.err"); + terminateStateOnError(state, "memory error: object read only", + ReadOnly); } else { ObjectState *wos = state.addressSpace.getWriteable(mo, os); wos->write(offset, value); @@ -3249,9 +3397,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (bound) { if (isWrite) { if (os->readOnly) { - terminateStateOnError(*bound, - "memory error: object read only", - "readonly.err"); + terminateStateOnError(*bound, "memory error: object read only", + ReadOnly); } else { ObjectState *wos = bound->addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), value); @@ -3272,10 +3419,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (incomplete) { terminateStateEarly(*unbound, "Query timed out (resolve)."); } else { - terminateStateOnError(*unbound, - "memory error: out of bound pointer", - "ptr.err", - getAddressInfo(*unbound, address)); + terminateStateOnError(*unbound, "memory error: out of bound pointer", Ptr, + NULL, getAddressInfo(*unbound, address)); } } } @@ -3310,9 +3455,8 @@ void Executor::executeMakeSymbolic(ExecutionState &state, std::vector<unsigned char> &values = si.assignment.bindings[array]; values = std::vector<unsigned char>(mo->size, '\0'); } else if (!AllowSeedExtension) { - terminateStateOnError(state, - "ran out of inputs during seeding", - "user.err"); + terminateStateOnError(state, "ran out of inputs during seeding", + User); break; } } else { @@ -3326,9 +3470,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, << " vs " << obj->name << "[" << obj->numBytes << "]" << " in test\n"; - terminateStateOnError(state, - msg.str(), - "user.err"); + terminateStateOnError(state, msg.str(), User); break; } else { std::vector<unsigned char> &values = si.assignment.bindings[array]; @@ -3345,11 +3487,11 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } else { ObjectState *os = bindObjectInState(state, mo, false); if (replayPosition >= replayKTest->numObjects) { - terminateStateOnError(state, "replay count mismatch", "user.err"); + terminateStateOnError(state, "replay count mismatch", User); } else { KTestObject *obj = &replayKTest->objects[replayPosition++]; if (obj->numBytes != mo->size) { - terminateStateOnError(state, "replay size mismatch", "user.err"); + terminateStateOnError(state, "replay size mismatch", User); } else { for (unsigned i=0; i<mo->size; i++) os->write8(i, obj->bytes[i]); @@ -3390,7 +3532,10 @@ void Executor::runFunctionAsMain(Function *f, if (++ai!=ae) { argvMO = memory->allocate((argc+1+envc+1+1) * NumPtrBytes, false, true, f->begin()->begin()); - + + if (!argvMO) + klee_error("Could not allocate memory for function arguments"); + arguments.push_back(argvMO->getBaseExpr()); if (++ai!=ae) { @@ -3430,6 +3575,8 @@ void Executor::runFunctionAsMain(Function *f, int j, len = strlen(s); MemoryObject *arg = memory->allocate(len+1, false, true, state->pc->inst); + if (!arg) + klee_error("Could not allocate memory for function arguments"); ObjectState *os = bindObjectInState(*state, arg, false); for (j=0; j<len+1; j++) os->write8(j, s[j]); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 600c7b90..93d1443e 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -101,7 +101,24 @@ public: typedef std::pair<ExecutionState*,ExecutionState*> StatePair; + enum TerminateReason { + Abort, + Assert, + Exec, + External, + Free, + Model, + Overflow, + Ptr, + ReadOnly, + ReportError, + User, + Unhandled + }; + private: + static const char *TerminateReasonNames[]; + class TimerInfo; KModule *kmodule; @@ -122,12 +139,12 @@ private: /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> addedStates; + std::vector<ExecutionState *> addedStates; /// Used to track states that have been removed during the current /// instructions step. /// \invariant \ref removedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> removedStates; + std::vector<ExecutionState *> removedStates; /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order @@ -362,6 +379,8 @@ private: const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction** lastInstruction); + bool shouldExitOn(enum TerminateReason termReason); + // remove state from queue and delete void terminateState(ExecutionState &state); // call exit handler and terminate state @@ -369,10 +388,10 @@ private: // call exit handler and terminate state void terminateStateOnExit(ExecutionState &state); // call error handler and terminate state - void terminateStateOnError(ExecutionState &state, - const llvm::Twine &message, - const char *suffix, - const llvm::Twine &longMessage=""); + void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, + enum TerminateReason termReason, + const char *suffix = NULL, + const llvm::Twine &longMessage = ""); // call error handler and terminate state, for execution errors // (things that should not be possible, like illegal instruction or @@ -380,7 +399,7 @@ private: void terminateStateOnExecError(ExecutionState &state, const llvm::Twine &message, const llvm::Twine &info="") { - terminateStateOnError(state, message, "exec.err", info); + terminateStateOnError(state, message, Exec, NULL, info); } /// bindModuleConstants - Initialize the module constant table. @@ -412,6 +431,7 @@ private: double maxInstTime); void checkMemoryUsage(); void printDebugInstructions(ExecutionState &state); + void doDumpStates(); public: Executor(const InterpreterOptions &opts, InterpreterHandler *ie); diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index b8ea97c2..f1c45105 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -52,7 +52,7 @@ public: ~HaltTimer() {} void run() { - llvm::errs() << "KLEE: HaltTimer invoked\n"; + klee_message("HaltTimer invoked"); executor->setHaltExecution(true); } }; @@ -179,7 +179,9 @@ void Executor::processTimers(ExecutionState *current, dumpStates = 0; } - if (maxInstTime>0 && current && !removedStates.count(current)) { + if (maxInstTime > 0 && current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) { if (timerTicks*kSecondsPerTick > maxInstTime) { klee_warning("max-instruction-time exceeded: %.2fs", timerTicks*kSecondsPerTick); diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index 7c76d480..f9f4b105 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -11,37 +11,135 @@ #include "Memory.h" #include "MemoryManager.h" -#include "klee/ExecutionState.h" #include "klee/Expr.h" -#include "klee/Solver.h" #include "klee/Internal/Support/ErrorHandling.h" #include "llvm/Support/CommandLine.h" +#include "llvm/Support/MathExtras.h" +#include <sys/mman.h> using namespace klee; +namespace { +llvm::cl::opt<bool> DeterministicAllocation( + "allocate-determ", + llvm::cl::desc("Allocate memory deterministically(default=off)"), + llvm::cl::init(false)); + +llvm::cl::opt<unsigned> DeterministicAllocationSize( + "allocate-determ-size", + llvm::cl::desc( + "Preallocated memory for deterministic allocation in MB (default=100)"), + llvm::cl::init(100)); + +llvm::cl::opt<bool> + NullOnZeroMalloc("return-null-on-zero-malloc", + llvm::cl::desc("Returns NULL in case malloc(size) was " + "called with size 0 (default=off)."), + llvm::cl::init(false)); + +llvm::cl::opt<unsigned> RedZoneSpace( + "red-zone-space", + llvm::cl::desc("Set the amount of free space between allocations. This is " + "important to detect out-of-bound accesses (default=10)."), + llvm::cl::init(10)); + +llvm::cl::opt<unsigned long long> DeterministicStartAddress( + "allocate-determ-start-address", + llvm::cl::desc("Start address for deterministic allocation. Has to be page " + "aligned (default=0x7ff30000000)."), + llvm::cl::init(0x7ff30000000)); +} + /***/ +MemoryManager::MemoryManager(ArrayCache *_arrayCache) + : arrayCache(_arrayCache), deterministicSpace(0), nextFreeSlot(0), + spaceSize(DeterministicAllocationSize.getValue() * 1024 * 1024) { + if (DeterministicAllocation) { + // Page boundary + void *expectedAddress = (void *)DeterministicStartAddress.getValue(); + + char *newSpace = + (char *)mmap(expectedAddress, spaceSize, PROT_READ | PROT_WRITE, + MAP_ANONYMOUS | MAP_PRIVATE, -1, 0); -MemoryManager::~MemoryManager() { + if (newSpace == MAP_FAILED) { + klee_error("Couldn't mmap() memory for deterministic allocations"); + } + if (expectedAddress != newSpace && expectedAddress != 0) { + klee_error("Could not allocate memory deterministically"); + } + + klee_message("Deterministic memory allocation starting from %p", newSpace); + deterministicSpace = newSpace; + nextFreeSlot = newSpace; + } +} + +MemoryManager::~MemoryManager() { while (!objects.empty()) { MemoryObject *mo = *objects.begin(); - if (!mo->isFixed) + if (!mo->isFixed && !DeterministicAllocation) free((void *)mo->address); objects.erase(mo); delete mo; } + + if (DeterministicAllocation) + munmap(deterministicSpace, spaceSize); } -MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, +MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, bool isGlobal, - const llvm::Value *allocSite) { - if (size>10*1024*1024) - klee_warning_once(0, "Large alloc: %u bytes. KLEE may run out of memory.", (unsigned) size); - - uint64_t address = (uint64_t) (unsigned long) malloc((unsigned) size); + const llvm::Value *allocSite, + size_t alignment) { + if (size > 10 * 1024 * 1024) + klee_warning_once(0, "Large alloc: %lu bytes. KLEE may run out of memory.", + size); + + // Return NULL if size is zero, this is equal to error during allocation + if (NullOnZeroMalloc && size == 0) + return 0; + + if (!llvm::isPowerOf2_64(alignment)) { + klee_warning("Only alignment of power of two is supported"); + return 0; + } + + uint64_t address = 0; + if (DeterministicAllocation) { + + address = llvm::RoundUpToAlignment((uint64_t)nextFreeSlot + alignment - 1, + alignment); + + // Handle the case of 0-sized allocations as 1-byte allocations. + // This way, we make sure we have this allocation between its own red zones + size_t alloc_size = std::max(size, (uint64_t)1); + if ((char *)address + alloc_size < deterministicSpace + spaceSize) { + nextFreeSlot = (char *)address + alloc_size + RedZoneSpace; + } else { + klee_warning_once( + 0, + "Couldn't allocate %lu bytes. Not enough deterministic space left.", + size); + address = 0; + } + } else { + // Use malloc for the standard case + if (alignment <= 8) + address = (uint64_t)malloc(size); + else { + int res = posix_memalign((void **)&address, alignment, size); + if (res < 0) { + klee_warning("Allocating aligned memory failed."); + address = 0; + } + } + } + if (!address) return 0; - + ++stats::allocations; MemoryObject *res = new MemoryObject(address, size, isLocal, isGlobal, false, allocSite, this); @@ -52,30 +150,31 @@ MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, MemoryObject *MemoryManager::allocateFixed(uint64_t address, uint64_t size, const llvm::Value *allocSite) { #ifndef NDEBUG - for (objects_ty::iterator it = objects.begin(), ie = objects.end(); - it != ie; ++it) { + for (objects_ty::iterator it = objects.begin(), ie = objects.end(); it != ie; + ++it) { MemoryObject *mo = *it; - if (address+size > mo->address && address < mo->address+mo->size) + if (address + size > mo->address && address < mo->address + mo->size) klee_error("Trying to allocate an overlapping object"); } #endif ++stats::allocations; - MemoryObject *res = new MemoryObject(address, size, false, true, true, - allocSite, this); + MemoryObject *res = + new MemoryObject(address, size, false, true, true, allocSite, this); objects.insert(res); return res; } -void MemoryManager::deallocate(const MemoryObject *mo) { - assert(0); -} +void MemoryManager::deallocate(const MemoryObject *mo) { assert(0); } void MemoryManager::markFreed(MemoryObject *mo) { - if (objects.find(mo) != objects.end()) - { - if (!mo->isFixed) + if (objects.find(mo) != objects.end()) { + if (!mo->isFixed && !DeterministicAllocation) free((void *)mo->address); objects.erase(mo); } } + +size_t MemoryManager::getUsedDeterministicSize() { + return nextFreeSlot - deterministicSpace; +} diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h index 01683443..fc77b476 100644 --- a/lib/Core/MemoryManager.h +++ b/lib/Core/MemoryManager.h @@ -14,31 +14,44 @@ #include <stdint.h> namespace llvm { - class Value; +class Value; } namespace klee { - class MemoryObject; - class ArrayCache; - - class MemoryManager { - private: - typedef std::set<MemoryObject*> objects_ty; - objects_ty objects; - ArrayCache *const arrayCache; - - public: - MemoryManager(ArrayCache *arrayCache) : arrayCache(arrayCache) {} - ~MemoryManager(); - - MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal, - const llvm::Value *allocSite); - MemoryObject *allocateFixed(uint64_t address, uint64_t size, - const llvm::Value *allocSite); - void deallocate(const MemoryObject *mo); - void markFreed(MemoryObject *mo); - ArrayCache *getArrayCache() const { return arrayCache; } - }; +class MemoryObject; +class ArrayCache; + +class MemoryManager { +private: + typedef std::set<MemoryObject *> objects_ty; + objects_ty objects; + ArrayCache *const arrayCache; + + char *deterministicSpace; + char *nextFreeSlot; + size_t spaceSize; + +public: + MemoryManager(ArrayCache *arrayCache); + ~MemoryManager(); + + /** + * Returns memory object which contains a handle to real virtual process + * memory. + */ + MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal, + const llvm::Value *allocSite, size_t alignment = 8); + MemoryObject *allocateFixed(uint64_t address, uint64_t size, + const llvm::Value *allocSite); + void deallocate(const MemoryObject *mo); + void markFreed(MemoryObject *mo); + ArrayCache *getArrayCache() const { return arrayCache; } + + /* + * Returns the size used by deterministic allocation in bytes + */ + size_t getUsedDeterministicSize(); +}; } // End klee namespace diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index cbb88727..973057c3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -67,13 +67,14 @@ ExecutionState &DFSSearcher::selectState() { } void DFSSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.back()) { states.pop_back(); @@ -101,13 +102,14 @@ ExecutionState &BFSSearcher::selectState() { } void BFSSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.front()) { states.pop_front(); @@ -134,14 +136,16 @@ ExecutionState &RandomSearcher::selectState() { return *states[theRNG.getInt32()%states.size()]; } -void RandomSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +RandomSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; bool ok = false; @@ -224,20 +228,24 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { } } -void WeightedRandomSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { - if (current && updateWeights && !removedStates.count(current)) +void WeightedRandomSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + if (current && updateWeights && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) states->update(current, getWeight(current)); - - for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(), - ie = addedStates.end(); it != ie; ++it) { + + for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(), + ie = addedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; states->insert(es, getWeight(es)); } - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { states->remove(*it); } } @@ -277,9 +285,10 @@ ExecutionState &RandomPathSearcher::selectState() { return *n->data; } -void RandomPathSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +RandomPathSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { } bool RandomPathSearcher::empty() { @@ -358,9 +367,9 @@ entry: } } -void BumpMergingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void BumpMergingSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { baseSearcher->update(current, addedStates, removedStates); } @@ -472,18 +481,21 @@ ExecutionState &MergingSearcher::selectState() { return selectState(); } -void MergingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +MergingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { if (!removedStates.empty()) { - std::set<ExecutionState *> alt = removedStates; - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + std::vector<ExecutionState *> alt = removedStates; + for (std::vector<ExecutionState *>::const_iterator + it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::const_iterator it2 = statesAtMerge.find(es); if (it2 != statesAtMerge.end()) { statesAtMerge.erase(it2); - alt.erase(alt.find(es)); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -529,10 +541,12 @@ ExecutionState &BatchingSearcher::selectState() { } } -void BatchingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { - if (removedStates.count(lastState)) +void +BatchingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + if (std::find(removedStates.begin(), removedStates.end(), lastState) != + removedStates.end()) lastState = 0; baseSearcher->update(current, addedStates, removedStates); } @@ -554,20 +568,22 @@ ExecutionState &IterativeDeepeningTimeSearcher::selectState() { return res; } -void IterativeDeepeningTimeSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void IterativeDeepeningTimeSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { double elapsed = util::getWallTime() - startTime; if (!removedStates.empty()) { - std::set<ExecutionState *> alt = removedStates; - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + std::vector<ExecutionState *> alt = removedStates; + for (std::vector<ExecutionState *>::const_iterator + it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::const_iterator it2 = pausedStates.find(es); if (it2 != pausedStates.end()) { - pausedStates.erase(it); - alt.erase(alt.find(es)); + pausedStates.erase(it2); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -575,7 +591,10 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, baseSearcher->update(current, addedStates, removedStates); } - if (current && !removedStates.count(current) && elapsed>time) { + if (current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end() && + elapsed > time) { pausedStates.insert(current); baseSearcher->removeState(current); } @@ -583,7 +602,8 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, if (baseSearcher->empty()) { time *= 2; llvm::errs() << "KLEE: increasing time budget to: " << time << "\n"; - baseSearcher->update(0, pausedStates, std::set<ExecutionState*>()); + std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); + baseSearcher->update(0, ps, std::vector<ExecutionState *>()); pausedStates.clear(); } } @@ -607,9 +627,9 @@ ExecutionState &InterleavedSearcher::selectState() { return s->selectState(); } -void InterleavedSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void InterleavedSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { for (std::vector<Searcher*>::const_iterator it = searchers.begin(), ie = searchers.end(); it != ie; ++it) (*it)->update(current, addedStates, removedStates); diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index d866f521..4ede3640 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -35,8 +35,8 @@ namespace klee { virtual ExecutionState &selectState() = 0; virtual void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) = 0; + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) = 0; virtual bool empty() = 0; @@ -55,15 +55,15 @@ namespace klee { // utility functions void addState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, tmp, std::set<ExecutionState*>()); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, tmp, std::vector<ExecutionState *>()); } void removeState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, std::set<ExecutionState*>(), tmp); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, std::vector<ExecutionState *>(), tmp); } enum CoreSearchType { @@ -86,8 +86,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; @@ -100,8 +100,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; @@ -114,8 +114,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; @@ -146,8 +146,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "WeightedRandomSearcher::"; @@ -172,8 +172,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; @@ -195,8 +195,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; @@ -218,8 +218,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; @@ -243,8 +243,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty(); } void printName(llvm::raw_ostream &os) { os << "<BatchingSearcher> timeBudget: " << timeBudget @@ -266,8 +266,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; @@ -286,8 +286,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return searchers[0]->empty(); } void printName(llvm::raw_ostream &os) { os << "<InterleavedSearcher> containing " diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 542d7f5b..0ecbdd07 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -281,7 +281,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { assert(arguments.size()==0 && "invalid number of arguments to abort"); - executor.terminateStateOnError(state, "abort failure", "abort.err"); + executor.terminateStateOnError(state, "abort failure", Executor::Abort); } void SpecialFunctionHandler::handleExit(ExecutionState &state, @@ -318,7 +318,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state, assert(arguments.size()==3 && "invalid number of arguments to _assert"); executor.terminateStateOnError(state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - "assert.err"); + Executor::Assert); } void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, @@ -327,7 +327,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, assert(arguments.size()==4 && "invalid number of arguments to __assert_fail"); executor.terminateStateOnError(state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - "assert.err"); + Executor::Assert); } void SpecialFunctionHandler::handleReportError(ExecutionState &state, @@ -338,6 +338,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, // arguments[0], arguments[1] are file, line executor.terminateStateOnError(state, readStringAtAddress(state, arguments[2]), + Executor::ReportError, readStringAtAddress(state, arguments[3]).c_str()); } @@ -410,7 +411,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, } else { executor.terminateStateOnError(state, "invalid klee_assume call (provably false)", - "user.err"); + Executor::User); } } else { executor.addConstraint(state, e); @@ -475,7 +476,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, } else { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", - "user.err"); + Executor::User); } } @@ -634,14 +635,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) { executor.terminateStateOnError(state, "check_memory_access requires constant args", - "user.err"); + Executor::User); } else { ObjectPair op; if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) { executor.terminateStateOnError(state, "check_memory_access: memory error", - "ptr.err", + Executor::Ptr, NULL, executor.getAddressInfo(state, address)); } else { ref<Expr> chk = @@ -650,7 +651,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!chk->isTrue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", - "ptr.err", + Executor::Ptr, NULL, executor.getAddressInfo(state, address)); } } @@ -711,9 +712,8 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, ExecutionState *s = it->second; if (old->readOnly) { - executor.terminateStateOnError(*s, - "cannot make readonly object symbolic", - "user.err"); + executor.terminateStateOnError(*s, "cannot make readonly object symbolic", + Executor::User); return; } @@ -732,7 +732,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, } else { executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", - "user.err"); + Executor::User); } } } @@ -757,31 +757,27 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned addition", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned addition", + Executor::Overflow); } void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned subtraction", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned subtraction", + Executor::Overflow); } void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned multiplication", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned multiplication", + Executor::Overflow); } void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on division or remainder", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on division or remainder", + Executor::Overflow); } diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 5e77172e..97ed26ea 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -86,17 +86,20 @@ namespace { cl::init(1.), cl::desc("Approximate number of seconds between stats writes (default=1.0s)")); + cl::opt<unsigned> StatsWriteAfterInstructions( + "stats-write-after-instructions", cl::init(0), + cl::desc("Write statistics after each n instructions, 0 to disable " + "(default=0)")); + cl::opt<double> IStatsWriteInterval("istats-write-interval", cl::init(10.), cl::desc("Approximate number of seconds between istats writes (default: 10.0s)")); - /* - cl::opt<double> - BranchCovCountsWriteInterval("branch-cov-counts-write-interval", - cl::desc("Approximate number of seconds between run.branches writes (default: 5.0s)"), - cl::init(5.)); - */ + cl::opt<unsigned> IStatsWriteAfterInstructions( + "istats-write-after-instructions", cl::init(0), + cl::desc("Write istats after each n instructions, 0 to disable " + "(default=0)")); // XXX I really would like to have dynamic rate control for something like this. cl::opt<double> @@ -185,6 +188,18 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, fullBranches(0), partialBranches(0), updateMinDistToUncovered(_updateMinDistToUncovered) { + + if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0) + klee_error("Both options --stats-write-interval and " + "--stats-write-after-instructions cannot be enabled at the same " + "time."); + + if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0) + klee_error( + "Both options --istats-write-interval and " + "--istats-write-after-instructions cannot be enabled at the same " + "time."); + KModule *km = executor.kmodule; if (!sys::path::is_absolute(objectFilename)) { @@ -235,19 +250,22 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, writeStatsHeader(); writeStatsLine(); - executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + if (StatsWriteInterval > 0) + executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + } - if (updateMinDistToUncovered) { - computeReachableUncovered(); - executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval); - } + // Add timer to calculate uncovered instructions if needed by the solver + if (updateMinDistToUncovered) { + computeReachableUncovered(); + executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval); } if (OutputIStats) { istatsFile = executor.interpreterHandler->openOutputFile("run.istats"); assert(istatsFile && "unable to open istats file"); - executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); + if (IStatsWriteInterval > 0) + executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); } } @@ -261,8 +279,12 @@ StatsTracker::~StatsTracker() { void StatsTracker::done() { if (statsFile) writeStatsLine(); - if (OutputIStats) + + if (OutputIStats) { + if (updateMinDistToUncovered) + computeReachableUncovered(); writeIStats(); + } } void StatsTracker::stepInstruction(ExecutionState &es) { @@ -310,6 +332,14 @@ void StatsTracker::stepInstruction(ExecutionState &es) { } } } + + if (statsFile && StatsWriteAfterInstructions && + stats::instructions % StatsWriteAfterInstructions.getValue() == 0) + writeStatsLine(); + + if (istatsFile && IStatsWriteAfterInstructions && + stats::instructions % IStatsWriteAfterInstructions.getValue() == 0) + writeIStats(); } /// @@ -327,15 +357,17 @@ void StatsTracker::framePushed(ExecutionState &es, StackFrame *parentFrame) { sf.callPathNode = cp; cp->count++; } + } - if (updateMinDistToUncovered) { - uint64_t minDistAtRA = 0; - if (parentFrame) - minDistAtRA = parentFrame->minDistToUncoveredOnReturn; - - sf.minDistToUncoveredOnReturn = sf.caller ? - computeMinDistToUncovered(sf.caller, minDistAtRA) : 0; - } + if (updateMinDistToUncovered) { + StackFrame &sf = es.stack.back(); + + uint64_t minDistAtRA = 0; + if (parentFrame) + minDistAtRA = parentFrame->minDistToUncoveredOnReturn; + + sf.minDistToUncoveredOnReturn = + sf.caller ? computeMinDistToUncovered(sf.caller, minDistAtRA) : 0; } } @@ -406,7 +438,7 @@ void StatsTracker::writeStatsLine() { << "," << numBranches << "," << util::getUserTime() << "," << executor.states.size() - << "," << util::GetTotalMallocUsage() + << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize() << "," << stats::queries << "," << stats::queryConstructs << "," << 0 // was numObjects diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 94bb3a5e..66328f30 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -15,14 +15,9 @@ #ifdef ENABLE_METASMT -#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/DirectSolver_Context.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 diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile index a44b4f6e..715f4b2d 100755 --- a/lib/Solver/Makefile +++ b/lib/Solver/Makefile @@ -16,11 +16,5 @@ NO_INSTALL=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 +include $(PROJ_SRC_ROOT)/MetaSMT.mk + diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 9e1f9a62..ad26f2ed 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -7,7 +7,6 @@ // //===----------------------------------------------------------------------===// - /* * MetaSMTBuilder.h * @@ -32,336 +31,357 @@ #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)); +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::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 MetaSMTBuilder; + +template <typename SolverContext> +class MetaSMTArrayExprHash + : public ArrayExprHash<typename SolverContext::result_type> { + + friend class MetaSMTBuilder<SolverContext>; -template<typename SolverContext> -class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > { - - friend class MetaSMTBuilder<SolverContext>; - public: - MetaSMTArrayExprHash() {}; - virtual ~MetaSMTArrayExprHash() {}; + MetaSMTArrayExprHash(){}; + virtual ~MetaSMTArrayExprHash(){}; }; static const bool mimic_stp = true; - -template<typename SolverContext> -class MetaSMTBuilder { +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); + typename SolverContext::result_type + bvRightShift(typename SolverContext::result_type expr, unsigned width, + unsigned shift); + typename SolverContext::result_type + bvVarLeftShift(typename SolverContext::result_type expr, + typename SolverContext::result_type shift, unsigned width); + typename SolverContext::result_type + bvVarRightShift(typename SolverContext::result_type expr, + typename SolverContext::result_type shift, unsigned width); + typename SolverContext::result_type + bvVarArithRightShift(typename SolverContext::result_type expr, + typename SolverContext::result_type shift, + 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); - 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); - } + 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); + 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); }; -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>::getArrayForUpdate(const Array *root, + const UpdateNode *un) { -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 (!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); + } +} - array_expr = evaluate(_solver, buildArray(root->getRange(), root->getDomain())); - - 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); +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(root->getRange(), root->getDomain())); + + 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); + 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> +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>::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) { -template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) { - - typename SolverContext::result_type res; + 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); + 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)); + for (width -= 64; width > 64; width -= 64) { + expr = evaluate(_solver, concat(zero, expr)); } + res = evaluate(_solver, concat(bvConst64(width, 0), expr)); + } - return(res); + return (res); } -template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) { - +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))); + 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); + 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>::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>::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>::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) { - 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); +template <typename SolverContext> +typename SolverContext::result_type +MetaSMTBuilder<SolverContext>::constructAShrByConstant( + typename SolverContext::result_type expr, unsigned width, unsigned shift, + typename SolverContext::result_type isSigned) { + typename SolverContext::result_type res; + + if (shift == 0) { + res = expr; + } else if (shift >= width) { + res = bvZero(width); + } else { + res = evaluate( + _solver, + metaSMT::logic::Ite(isSigned, concat(bvMinusOne(shift), + bvExtract(expr, width - 1, shift)), + bvRightShift(expr, width, shift))); + } + + 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; +template <typename SolverContext> +typename SolverContext::result_type +MetaSMTBuilder<SolverContext>::constructMulByConstant( + typename SolverContext::result_type expr, unsigned width, uint64_t x) { - // expr*x == expr*(add-sub) == expr*add - expr*sub - ComputeMultConstants64(x, add, sub); + uint64_t add, sub; + typename SolverContext::result_type res; + bool first = true; - // 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; + // expr*x == expr*(add-sub) == expr*add - expr*sub + ComputeMultConstants64(x, add, sub); - if ((add & bit) || (sub & bit)) { - assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + // legal, these would overflow completely + add = bits64::truncateToNBits(add, width); + sub = bits64::truncateToNBits(sub, width); - typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits); + for (int j = 63; j >= 0; j--) { + uint64_t bit = 1LL << j; - 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 ((add & bit) || (sub & bit)) { + assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + + typename SolverContext::result_type op = bvLeftShift(expr, width, j); + + 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); -} + if (first) { + res = bvZero(width); + } + return (res); +} -/* - * Compute the 32-bit unsigned integer division of n by a divisor d based on +/* + * 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, + * 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 @@ -370,36 +390,46 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulB * * @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); +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 +/* + * 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, + * 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 @@ -408,519 +438,549 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDiv * * @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>::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(64, 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); +template <typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift( + typename SolverContext::result_type expr, unsigned width, unsigned shift) { - 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))); - } + typename SolverContext::result_type res; - return(res); + 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))); - } +template <typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift( + typename SolverContext::result_type expr, unsigned width, unsigned shift) { + + typename SolverContext::result_type res; + + 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); + 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); +template <typename SolverContext> +typename SolverContext::result_type +MetaSMTBuilder<SolverContext>::bvVarLeftShift( + typename SolverContext::result_type expr, + typename SolverContext::result_type shift, unsigned width) { + + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + + typename SolverContext::result_type res = bvZero(width); + + // 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(width, i)), + bvLeftShift(expr, width, i), res)); + } - //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)); + // If overshifting, shift to zero + res = evaluate(_solver, + metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, + bvZero(width))); - //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)); - } - - // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), - res, - bvZero(width))); - - return(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 - } - - // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), - res, - bvZero(width))); +// 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 shift, unsigned width) { + + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + + typename SolverContext::result_type res = bvZero(width); + + // 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(width, i)), + bvRightShift(expr, width, i), res)); + // ToDo Reconsider widht to provide to bvRightShift + } + + // If overshifting, shift to zero + res = evaluate(_solver, + metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, + bvZero(width))); - return(res); + 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); +// 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 shift, unsigned width) { + + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + + // 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); + + // 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(width, i)), + constructAShrByConstant(expr, width, i, signedBool), res)); + } - //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)); - } - - // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(shiftBits, width)), - res, - bvZero(width))); + // If overshifting, shift to zero + res = evaluate(_solver, + metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, + bvZero(width))); - return(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; +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)); +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 { - 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; - } + 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) { +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; + typename SolverContext::result_type res; + + int width = 0; + if (!width_out) { + // assert(false); + width_out = &width; + } + + ++stats::queryConstructs; + + // llvm::errs() << "Constructing expression "; + // ExprPPrinter::printSingleExpr(llvm::errs(), e); + // llvm::errs() << "\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)); + } } - - ++stats::queryConstructs; - -// llvm::errs() << "Constructing expression "; -// ExprPPrinter::printSingleExpr(llvm::errs(), e); -// llvm::errs() << "\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; - } + 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::NotOptimized: { + NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e); + assert(noe); + res = construct(noe->src, width_out); + break; + } - case Expr::Read: - { - ReadExpr *re = cast<ReadExpr>(e); - assert(re && re->updates.root); - *width_out = re->updates.root->getRange(); - // FixMe call method of Array - res = evaluate(_solver, - metaSMT::logic::Array::select( - getArrayForUpdate(re->updates.root, re->updates.head), - construct(re->index, 0))); - 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::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::Read: { + ReadExpr *re = cast<ReadExpr>(e); + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); + // FixMe call method of Array + res = evaluate(_solver, + metaSMT::logic::Array::select( + getArrayForUpdate(re->updates.root, re->updates.head), + construct(re->index, 0))); + 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)); + 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; + } - unsigned ee_width = ee->getWidth(); - *width_out = ee_width; + 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)); - if (ee_width == 1) { - res = bvBoolExtract(child, ee->offset); - } - else { - res = evaluate(_solver, - extract(ee->offset + ee_width - 1, ee->offset, child)); - } - break; - } + unsigned ee_width = ee->getWidth(); + *width_out = ee_width; - case Expr::ZExt: - { - CastExpr *ce = cast<CastExpr>(e); - assert(ce); + if (ee_width == 1) { + res = bvBoolExtract(child, ee->offset); + } else { + res = evaluate(_solver, + extract(ee->offset + ee_width - 1, ee->offset, child)); + } + break; + } - int child_width = 0; - typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + case Expr::ZExt: { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); - unsigned ce_width = ce->getWidth(); - *width_out = ce_width; + int child_width = 0; + typename SolverContext::result_type child = + evaluate(_solver, construct(ce->src, &child_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)); - } + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; - // 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)); - } + 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)); + } - 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; - } + // 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))); - 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; - } - } - } + break; + } - if (construct_both) { - res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); - } - break; - } + case Expr::SExt: { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); - case Expr::SDiv: - { - SDivExpr *de = cast<SDivExpr>(e); - assert(de); + int child_width = 0; + typename SolverContext::result_type child = + evaluate(_solver, construct(ce->src, &child_width)); - typename SolverContext::result_type left_expr = construct(de->left, width_out); - assert(*width_out != 1 && "uncanonicalized sdiv"); + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; - 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; + 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)); + 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; } + } + } - case Expr::URem: - { - URemExpr *de = cast<URemExpr>(e); - assert(de); + if (construct_both) { + res = + evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); + } + break; + } - 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; - } - } + 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"); + + bool optimized = false; + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && _optimizeDivides && (*width_out == 32)) { + llvm::APInt divisor = CE->getAPValue(); + if (divisor != llvm::APInt(CE->getWidth(), 1, false /*unsigned*/) && + divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) { + res = constructSDivByConstant(left_expr, *width_out, + CE->getZExtValue(32)); + optimized = true; + } + } + if (!optimized) { + res = + evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); + } + break; + } - // 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::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; + } + } - 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 (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()) { @@ -935,257 +995,259 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu } } } - + #endif - if (construct_both) { - res = evaluate(_solver, bvsrem(left_expr, right_expr)); - } - break; - } + 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; + 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()); + } 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()); + } 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); + } 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)); } - - // unused due to canonicalization + } 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; -} +#endif + default: + assert(false); + break; + }; + return res; +} -} /* end of namespace klee */ +} /* end of namespace klee */ #endif /* ENABLE_METASMT */ diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index c4f6a5d0..411c07b1 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -11,6 +11,7 @@ #include "MetaSMTBuilder.h" #include "klee/Constraints.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "klee/util/Assignment.h" @@ -19,11 +20,15 @@ #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> +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + #include <errno.h> #include <unistd.h> #include <signal.h> @@ -277,7 +282,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( fflush(stderr); int pid = fork(); if (pid == -1) { - fprintf(stderr, "error: fork failed (for metaSMT)"); + klee_warning("fork failed (for metaSMT)"); return (SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED); } @@ -384,7 +389,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( } while (res < 0 && errno == EINTR); if (res < 0) { - fprintf(stderr, "error: waitpid() for metaSMT failed"); + klee_warning("waitpid() for metaSMT failed"); return (SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED); } @@ -404,10 +409,10 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( } else if (exitcode == 1) { hasSolution = false; } else if (exitcode == 52) { - fprintf(stderr, "error: metaSMT timed out"); + klee_warning("metaSMT timed out"); return (SolverImpl::SOLVER_RUN_STATUS_TIMEOUT); } else { - fprintf(stderr, "error: metaSMT did not return a recognized code"); + klee_warning("metaSMT did not return a recognized code"); return (SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE); } diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index f93bec3c..a858a7d7 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -7,8 +7,13 @@ // //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" +#include "klee/Config/config.h" #include "klee/Internal/System/Time.h" #include "klee/Statistics.h" +#ifdef HAVE_ZLIB_H +#include "klee/Internal/Support/CompressionStream.h" +#include "klee/Internal/Support/ErrorHandling.h" +#endif #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) #include "llvm/Support/FileSystem.h" @@ -20,30 +25,50 @@ namespace { llvm::cl::opt<bool> DumpPartialQueryiesEarly( "log-partial-queries-early", llvm::cl::init(false), llvm::cl::desc("Log queries before calling the solver (default=off)")); + +#ifdef HAVE_ZLIB_H +llvm::cl::opt<bool> CreateCompressedQueryLog( + "compress-query-log", llvm::cl::init(false), + llvm::cl::desc("Compress query log files (default=off)")); +#endif } QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign, int queryTimeToLog) - : solver(_solver), + : solver(_solver), os(0), BufferString(""), logBuffer(BufferString), + queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f), + lastQueryTime(0.0f), queryCommentSign(commentSign) { +#ifdef HAVE_ZLIB_H + if (!CreateCompressedQueryLog) { +#endif #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) - os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), + os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo, + llvm::sys::fs::OpenFlags::F_Text); #else - os(path.c_str(), ErrorInfo), + os = new llvm::raw_fd_ostream(path.c_str(), ErrorInfo); +#endif +#ifdef HAVE_ZLIB_H + } else { + os = new compressed_fd_ostream((path + ".gz").c_str(), ErrorInfo); + } + if (ErrorInfo != "") { + klee_error("Could not open file %s : %s", path.c_str(), ErrorInfo.c_str()); + } #endif - BufferString(""), logBuffer(BufferString), queryCount(0), - minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), - queryCommentSign(commentSign) { assert(0 != solver); } -QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } +QueryLoggingSolver::~QueryLoggingSolver() { + delete solver; + delete os; +} void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { logBuffer.flush(); if (writeToFile) { - os << logBuffer.str(); - os.flush(); + *os << logBuffer.str(); + os->flush(); } // prepare the buffer for reuse BufferString = ""; diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index bb266c67..7ac783d1 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -26,7 +26,7 @@ class QueryLoggingSolver : public SolverImpl { protected: Solver *solver; std::string ErrorInfo; - llvm::raw_fd_ostream os; + llvm::raw_ostream *os; // @brief Buffer used by logBuffer std::string BufferString; // @brief buffer to store logs before flushing to file diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 307ae0fb..8ec35762 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -152,6 +152,7 @@ ExprHandle STPBuilder::bvExtract(ExprHandle expr, unsigned top, unsigned bottom) return vc_bvExtract(vc, expr, top, bottom); } ExprHandle STPBuilder::eqExpr(ExprHandle a, ExprHandle b) { + assert((vc_getBVLength(vc, a) == vc_getBVLength(vc, b)) && "a and b should be same type"); return vc_eqExpr(vc, a, b); } @@ -187,76 +188,93 @@ ExprHandle STPBuilder::bvLeftShift(ExprHandle expr, unsigned shift) { } } +ExprHandle STPBuilder::extractPartialShiftValue(ExprHandle shift, + unsigned width, + unsigned &shiftBits) { + // Assuming width is power of 2 + llvm::APInt sw(32, width); + shiftBits = sw.getActiveBits(); + + // get the shift amount (looking only at the bits appropriate for the given + // width) + return vc_bvExtract(vc, shift, shiftBits - 1, 0); +} + // left shift by a variable amount on an expression of the specified width ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) { unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - //construct a big if-then-elif-elif-... with one case per possible shift amount - for( int i=width-1; i>=0; i-- ) { - res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(width, i)), - bvLeftShift(expr, i), - res); + unsigned shiftBits = 0; + ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits); + + // construct a big if-then-elif-elif-... with one case per possible shift + // amount + for (int i = width - 1; i >= 0; i--) { + res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)), + bvLeftShift(expr, i), res); } // If overshifting, shift to zero - ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); + ExprHandle ex = + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width)); res = vc_iteExpr(vc, ex, res, bvZero(width)); return res; } -// logical right shift by a variable amount on an expression of the specified width +// logical right shift by a variable amount on an expression of the specified +// width ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { unsigned width = vc_getBVLength(vc, expr); ExprHandle res = bvZero(width); - //construct a big if-then-elif-elif-... with one case per possible shift amount - for( int i=width-1; i>=0; i-- ) { - res = vc_iteExpr(vc, - eqExpr(shift, bvConst32(width, i)), - bvRightShift(expr, i), - res); + unsigned shiftBits = 0; + ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits); + + // construct a big if-then-elif-elif-... with one case per possible shift + // amount + for (int i = width - 1; i >= 0; i--) { + res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)), + bvRightShift(expr, i), res); } // If overshifting, shift to zero - ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); - res = vc_iteExpr(vc, - ex, - res, - bvZero(width)); + // If overshifting, shift to zero + ExprHandle ex = + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width)); + res = vc_iteExpr(vc, ex, res, bvZero(width)); + return res; } -// arithmetic right shift by a variable amount on an expression of the specified width +// arithmetic right shift by a variable amount on an expression of the specified +// width ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { unsigned width = vc_getBVLength(vc, expr); - //get the sign bit to fill with - ExprHandle signedBool = bvBoolExtract(expr, width-1); + unsigned shiftBits = 0; + ExprHandle shift_ext = extractPartialShiftValue(shift, width, shiftBits); - //start with the result if shifting by width-1 - ExprHandle res = constructAShrByConstant(expr, width-1, signedBool); + // get the sign bit to fill with + ExprHandle signedBool = bvBoolExtract(expr, width - 1); - //construct a big if-then-elif-elif-... with one case per possible shift amount + // start with the result if shifting by width-1 + ExprHandle res = constructAShrByConstant(expr, width - 1, signedBool); + + // 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 = vc_iteExpr(vc, - eqExpr(shift, bvConst32(width,i)), - constructAShrByConstant(expr, - i, - signedBool), - res); + for (int i = width - 2; i >= 0; i--) { + res = vc_iteExpr(vc, eqExpr(shift_ext, bvConst32(shiftBits, i)), + constructAShrByConstant(expr, i, signedBool), res); } // If overshifting, shift to zero - ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); - res = vc_iteExpr(vc, - ex, - res, - bvZero(width)); + ExprHandle ex = + vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc, shift), width)); + res = vc_iteExpr(vc, ex, res, bvZero(width)); return res; } diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index 3b17ccf1..5be34029 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -93,6 +93,8 @@ private: ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift); ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift); + ExprHandle extractPartialShiftValue(ExprHandle shift, unsigned width, + unsigned &shiftBits); ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, ExprHandle isSigned); diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index 5c49521e..e1d41eba 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -98,6 +98,8 @@ STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) // we restore the old behaviour. vc_setInterfaceFlags(vc, EXPRDELETE, 0); + make_division_total(vc); + vc_registerErrorHandler(::stp_error_handler); if (useForkedSTP) { @@ -229,7 +231,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, fflush(stderr); int pid = fork(); if (pid == -1) { - fprintf(stderr, "ERROR: fork failed (for STP)"); + klee_warning("fork failed (for STP)"); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED; @@ -264,7 +266,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, } while (res < 0 && errno == EINTR); if (res < 0) { - fprintf(stderr, "ERROR: waitpid() for STP failed"); + klee_warning("waitpid() for STP failed"); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED; @@ -274,8 +276,8 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, // "occasion" return a status when the process was terminated by a // signal, so test signal first. if (WIFSIGNALED(status) || !WIFEXITED(status)) { - fprintf(stderr, "ERROR: STP did not return successfully. Most likely " - "you forgot to run 'ulimit -s unlimited'\n"); + klee_warning("STP did not return successfully. Most likely you forgot " + "to run 'ulimit -s unlimited'"); if (!IgnoreSolverFailures) { exit(1); } @@ -288,11 +290,11 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, } else if (exitcode == 1) { hasSolution = false; } else if (exitcode == 52) { - fprintf(stderr, "error: STP timed out"); + klee_warning("STP timed out"); // mark that a timeout occurred return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } else { - fprintf(stderr, "error: STP did not return a recognized code"); + klee_warning("STP did not return a recognized code"); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; diff --git a/lib/Support/CompressionStream.cpp b/lib/Support/CompressionStream.cpp new file mode 100644 index 00000000..eb208edf --- /dev/null +++ b/lib/Support/CompressionStream.cpp @@ -0,0 +1,119 @@ +//===-- CompressionStream.cpp --------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/Config/config.h" +#include "klee/Config/Version.h" +#ifdef HAVE_ZLIB_H +#include "klee/Internal/Support/CompressionStream.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/Support/system_error.h" +#else +#include <fcntl.h> +#include <errno.h> +#include <sys/types.h> +#include <sys/stat.h> +#endif + +namespace klee { + +compressed_fd_ostream::compressed_fd_ostream(const char *Filename, + std::string &ErrorInfo) + : llvm::raw_ostream(), pos(0) { + ErrorInfo = ""; +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + // Open file in binary mode + llvm::error_code EC = + llvm::sys::fs::openFileForWrite(Filename, FD, llvm::sys::fs::F_Binary); + + if (EC) { + ErrorInfo = EC.message(); + FD = -1; + } +#else + FD = ::open(Filename, O_WRONLY | O_CREAT | O_TRUNC, 0666); + if (FD < 0) { + ErrorInfo = "Could not open file."; + FD = -1; + } +#endif + // Initialize the compression library + strm.zalloc = 0; + strm.zfree = 0; + strm.next_out = buffer; + strm.avail_out = BUFSIZE; + + deflateInit2(&strm, Z_BEST_COMPRESSION, Z_DEFLATED, 15 | 16, + 8 /* memory usage default, 0 smalles, 9 highest*/, + Z_DEFAULT_STRATEGY); +} + +void compressed_fd_ostream::writeFullCompressedData() { + // Check if no space available and write the buffer + if (strm.avail_out == 0) { + write_file(reinterpret_cast<const char *>(buffer), BUFSIZE); + strm.next_out = buffer; + strm.avail_out = BUFSIZE; + } +} + +void compressed_fd_ostream::flush_compressed_data() { + // flush data from the raw buffer + flush(); + + // write the remaining data + int deflate_res = Z_OK; + while (deflate_res == Z_OK) { + // Check if no space available and write the buffer + writeFullCompressedData(); + deflate_res = deflate(&strm, Z_FINISH); + } + assert(deflate_res == Z_STREAM_END); + write_file(reinterpret_cast<const char *>(buffer), BUFSIZE - strm.avail_out); +} + +compressed_fd_ostream::~compressed_fd_ostream() { + if (FD >= 0) { + // write the remaining data + flush_compressed_data(); + close(FD); + } + deflateEnd(&strm); +} + +void compressed_fd_ostream::write_impl(const char *Ptr, size_t Size) { + strm.next_in = + const_cast<unsigned char *>(reinterpret_cast<const unsigned char *>(Ptr)); + strm.avail_in = Size; + + // Check if there is still data to compress + while (strm.avail_in != 0) { + // compress data + int res = deflate(&strm, Z_NO_FLUSH); + assert(res == Z_OK); + writeFullCompressedData(); + } +} + +void compressed_fd_ostream::write_file(const char *Ptr, size_t Size) { + pos += Size; + assert(FD >= 0 && "File already closed"); + do { + ssize_t ret = ::write(FD, Ptr, Size); + if (ret < 0) { + if (errno == EINTR || errno == EAGAIN) + continue; + assert(0 && "Could not write to file"); + break; + } + + Ptr += ret; + Size -= ret; + } while (Size > 0); +} +} +#endif diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp index a9f4026d..d141593a 100644 --- a/lib/Support/MemoryUsage.cpp +++ b/lib/Support/MemoryUsage.cpp @@ -26,7 +26,7 @@ using namespace klee; size_t util::GetTotalMallocUsage() { #ifdef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H - uint64_t value; + size_t value = 0; MallocExtension::instance()->GetNumericProperty( "generic.current_allocated_bytes", &value); return value; @@ -36,9 +36,9 @@ size_t util::GetTotalMallocUsage() { // does not include mmap()'ed memory in mi.uordblks // but other implementations (e.g. tcmalloc) do. #if defined(__GLIBC__) - return mi.uordblks + mi.hblkhd; + return (size_t)(unsigned)mi.uordblks + (unsigned)mi.hblkhd; #else - return mi.uordblks; + return (unsigned)mi.uordblks; #endif #elif defined(HAVE_MALLOC_ZONE_STATISTICS) && defined(HAVE_MALLOC_MALLOC_H) diff --git a/runtime/POSIX/stubs.c b/runtime/POSIX/stubs.c index 99e2e768..b4f31bf7 100644 --- a/runtime/POSIX/stubs.c +++ b/runtime/POSIX/stubs.c @@ -174,10 +174,15 @@ time_t time(time_t *t) { clock_t times(struct tms *buf) { /* Fake */ - buf->tms_utime = 0; - buf->tms_stime = 0; - buf->tms_cutime = 0; - buf->tms_cstime = 0; + if (!buf) + klee_warning("returning 0\n"); + else { + klee_warning("setting all times to 0 and returning 0\n"); + buf->tms_utime = 0; + buf->tms_stime = 0; + buf->tms_cutime = 0; + buf->tms_cstime = 0; + } return 0; } diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c new file mode 100644 index 00000000..a2a07d8b --- /dev/null +++ b/test/Feature/CompressedExprLogging.c @@ -0,0 +1,42 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc +// 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: rm -rf %t.klee-out %t.klee-out2 +// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:pc %t1.bc +// RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:pc %t1.bc +// RUN: gunzip -d %t.klee-out2/all-queries.pc.gz +// RUN: diff %t.klee-out/all-queries.pc %t.klee-out/all-queries.pc + +#include <assert.h> + +int constantArr[16] = {1 << 0, 1 << 1, 1 << 2, 1 << 3, 1 << 4, 1 << 5, + 1 << 6, 1 << 7, 1 << 8, 1 << 9, 1 << 10, 1 << 11, + 1 << 12, 1 << 13, 1 << 14, 1 << 15}; + +int main() { + char buf[4]; + klee_make_symbolic(buf, sizeof buf); + + buf[1] = 'a'; + + constantArr[klee_range(0, 16, "idx.0")] = buf[0]; + + // Use this to trigger an interior update list usage. + int y = constantArr[klee_range(0, 16, "idx.1")]; + + constantArr[klee_range(0, 16, "idx.2")] = buf[3]; + + buf[klee_range(0, 4, "idx.3")] = 0; + klee_assume(buf[0] == 'h'); + + int x = *((int *)buf); + klee_assume(x > 2); + klee_assume(x == constantArr[12]); + + klee_assume(y != (1 << 5)); + + assert(0); + + return 0; +} diff --git a/test/Feature/DeterministicSwitch.c b/test/Feature/DeterministicSwitch.c new file mode 100644 index 00000000..b6c186ff --- /dev/null +++ b/test/Feature/DeterministicSwitch.c @@ -0,0 +1,38 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=dfs %t.bc >%t.switch.log 2>&1 +// RUN: FileCheck %s -input-file=%t.switch.log -check-prefix=CHECK-DFS +// RUN: rm -rf %t.klee-out +// RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=bfs %t.bc >%t.switch.log 2>&1 +// RUN: FileCheck %s -input-file=%t.switch.log -check-prefix=CHECK-BFS + +#include "klee/klee.h" +#include <stdio.h> + +int main(int argc, char **argv) { + char c; + + klee_make_symbolic(&c, sizeof(c), "index"); + + switch (c) { + case '\t': + printf("tab\n"); + break; + case ' ': + printf("space\n"); + break; + default: + printf("default\n"); + break; + } + + // CHECK-DFS: default + // CHECK-DFS: space + // CHECK-DFS: tab + + // CHECK-BFS: tab + // CHECK-BFS: space + // CHECK-BFS: default + + return 0; +} diff --git a/test/Feature/ExitOnErrorType.c b/test/Feature/ExitOnErrorType.c new file mode 100644 index 00000000..a68a92e0 --- /dev/null +++ b/test/Feature/ExitOnErrorType.c @@ -0,0 +1,15 @@ +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -exit-on-error-type Assert %t1.bc 2>&1 + +#include <assert.h> +#include <klee/klee.h> + +int main() { + assert(klee_int("assert")); + + while (1) { + } + + return 0; +} diff --git a/test/Feature/NonSizedGlobals.c b/test/Feature/NonSizedGlobals.c new file mode 100644 index 00000000..b98f7bf1 --- /dev/null +++ b/test/Feature/NonSizedGlobals.c @@ -0,0 +1,12 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc + +struct X; +extern struct X Y; +void *ptr = &Y; + +int main() +{ + return 0; +} diff --git a/test/regression/2016-04-14-sdiv-2.c_ b/test/regression/2016-04-14-sdiv-2.c index 88a5fca3..974036ee 100644 --- a/test/regression/2016-04-14-sdiv-2.c_ +++ b/test/regression/2016-04-14-sdiv-2.c @@ -1,10 +1,11 @@ -// XFAIL: * // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out -exit-on-error -solver-optimize-divides=true %t.bc >%t1.log // RUN: grep "m is 2" %t1.log - #include <assert.h> +#include <stdio.h> + +#include "klee/klee.h" int main(void) { diff --git a/test/regression/2016-06-28-div-zero-bug.c b/test/regression/2016-06-28-div-zero-bug.c new file mode 100644 index 00000000..11689aa0 --- /dev/null +++ b/test/regression/2016-06-28-div-zero-bug.c @@ -0,0 +1,23 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false %t.bc >%t1.log + +// This bug is triggered when using STP up to an including 2.1.0 +// See https://github.com/klee/klee/issues/308 +// and https://github.com/stp/stp/issues/206 + +int b, a, g; + +int *c = &b, *d = &b, *f = &a; + +int safe_div(short p1, int p2) { + return p2 == 0 ? p1 : p2; +} + +int main() { + klee_make_symbolic(&b, sizeof b); + if (safe_div(*c, 0)) + *f = (int)&b % *c; + + safe_div(a && g, *d); +} diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index 1631dda6..a2250fe0 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -32,3 +32,7 @@ include $(PROJ_SRC_ROOT)/MetaSMT.mk ifeq ($(HAVE_TCMALLOC),1) LIBS += $(TCMALLOC_LIB) endif + +ifeq ($(HAVE_ZLIB),1) + LIBS += -lz +endif diff --git a/tools/klee/Makefile b/tools/klee/Makefile index 676507e0..8d50403f 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -33,3 +33,7 @@ include $(PROJ_SRC_ROOT)/MetaSMT.mk ifeq ($(HAVE_TCMALLOC),1) LIBS += $(TCMALLOC_LIB) endif + +ifeq ($(HAVE_ZLIB),1) + LIBS += -lz +endif \ No newline at end of file diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 7fe64c72..3e469a6e 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -40,6 +40,7 @@ #include "llvm/LLVMContext.h" #include "llvm/Support/FileSystem.h" #endif +#include "llvm/Support/Errno.h" #include "llvm/Support/FileSystem.h" #include "llvm/Bitcode/ReaderWriter.h" #include "llvm/Support/CommandLine.h" @@ -1430,7 +1431,8 @@ int main(int argc, char **argv, char **envp) { if (RunInDir != "") { int res = chdir(RunInDir.c_str()); if (res < 0) { - klee_error("Unable to change directory to: %s", RunInDir.c_str()); + klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(), + sys::StrError(errno).c_str()); } } @@ -1492,7 +1494,8 @@ int main(int argc, char **argv, char **envp) { if (RunInDir != "") { int res = chdir(RunInDir.c_str()); if (res < 0) { - klee_error("Unable to change directory to: %s", RunInDir.c_str()); + klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(), + sys::StrError(errno).c_str()); } } interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp); |