diff options
30 files changed, 1522 insertions, 1095 deletions
diff --git a/.travis.yml b/.travis.yml index 91e0e89b..42072095 100644 --- a/.travis.yml +++ b/.travis.yml @@ -19,16 +19,25 @@ 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 - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 # FIXME: Enable when we want to test LLVM3.5 #- LLVM_VERSION=3.5 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 @@ -64,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 @@ -92,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 @@ -110,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/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..1b0b7ba8 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@ 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..a08e190e 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -742,7 +742,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 +768,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..7f1839c0 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 @@ -739,6 +740,7 @@ with_tcmalloc with_stp with_z3 with_metasmt +with_metasmt_default_backend ' ac_precious_vars='build_alias host_alias @@ -1393,6 +1395,9 @@ Optional Packages: --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 @@ -5324,7 +5329,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 +5388,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 +5396,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/expr/Parser.h b/include/expr/Parser.h index d2135f12..a9133e9d 100644 --- a/include/expr/Parser.h +++ b/include/expr/Parser.h @@ -228,9 +228,8 @@ namespace expr { /// \arg MB - The input data. /// \arg Builder - The expression builder to use for constructing /// expressions. - static Parser *Create(const std::string Name, - const llvm::MemoryBuffer *MB, - ExprBuilder *Builder); + static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB, + ExprBuilder *Builder, bool ClearArrayAfterQuery); }; } } 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/Executor.cpp b/lib/Core/Executor.cpp index ff346487..49b022f8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2652,7 +2652,7 @@ void Executor::run(ExecutionState &initialState) { dump: if (DumpStatesOnHalt && !states.empty()) { - llvm::errs() << "KLEE: halting execution, dumping remaining states\n"; + klee_message("halting execution, dumping remaining states"); for (std::set<ExecutionState*>::iterator it = states.begin(), ie = states.end(); it != ie; ++it) { diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index b8ea97c2..480f1cde 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); } }; diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index e914cb80..572b9572 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -111,6 +111,7 @@ namespace { const MemoryBuffer *TheMemoryBuffer; ExprBuilder *Builder; ArrayCache TheArrayCache; + bool ClearArrayAfterQuery; Lexer TheLexer; unsigned MaxErrors; @@ -322,14 +323,11 @@ namespace { void Error(const char *Message) { Error(Message, Tok); } public: - ParserImpl(const std::string _Filename, - const MemoryBuffer *MB, - ExprBuilder *_Builder) : Filename(_Filename), - TheMemoryBuffer(MB), - Builder(_Builder), - TheLexer(MB), - MaxErrors(~0u), - NumErrors(0) {} + ParserImpl(const std::string _Filename, const MemoryBuffer *MB, + ExprBuilder *_Builder, bool _ClearArrayAfterQuery) + : Filename(_Filename), TheMemoryBuffer(MB), Builder(_Builder), + ClearArrayAfterQuery(_ClearArrayAfterQuery), TheLexer(MB), + MaxErrors(~0u), NumErrors(0) {} virtual ~ParserImpl(); @@ -492,9 +490,9 @@ DeclResult ParserImpl::ParseArrayDecl() { Values.clear(); } - for (unsigned i = 0; i != Size.get(); ++i) { - // FIXME: Must be constant expression. - } + // for (unsigned i = 0; i != Size.get(); ++i) { + // TODO: Check: Must be constant expression. + //} } // FIXME: Validate that size makes sense for domain type. @@ -532,7 +530,7 @@ DeclResult ParserImpl::ParseArrayDecl() { ArrayDecl *AD = new ArrayDecl(Label, Size.get(), DomainType.get(), RangeType.get(), Root); - ArraySymTab.insert(std::make_pair(Label, AD)); + ArraySymTab[Label] = AD; // Create the initial version reference. VersionSymTab.insert(std::make_pair(Label, @@ -681,7 +679,13 @@ DeclResult ParserImpl::ParseQueryCommand() { exit: if (Tok.kind != Token::EndOfFile) - ExpectRParen("unexpected argument to 'query'."); + ExpectRParen("unexpected argument to 'query'."); + + // If we assume that the queries are independent, we clear the array + // table from the previous declarations + if (ClearArrayAfterQuery) + ArraySymTab.clear(); + return new QueryCommand(Constraints, Res.get(), Values, Objects); } @@ -1641,10 +1645,9 @@ Parser::Parser() { Parser::~Parser() { } -Parser *Parser::Create(const std::string Filename, - const MemoryBuffer *MB, - ExprBuilder *Builder) { - ParserImpl *P = new ParserImpl(Filename, MB, Builder); +Parser *Parser::Create(const std::string Filename, const MemoryBuffer *MB, + ExprBuilder *Builder, bool ClearArrayAfterQuery) { + ParserImpl *P = new ParserImpl(Filename, MB, Builder, ClearArrayAfterQuery); P->Initialize(); return P; } 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..ba7ea03b 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,540 @@ 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(32, shpost); + + // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32) + int64_t mprime_64 = (int64_t)mprime; + + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend + // arguments + typename SolverContext::result_type expr_n_64 = + evaluate(_solver, sign_extend(64 - width, expr_n)); + typename SolverContext::result_type mult_64 = + constructMulByConstant(expr_n_64, 64, mprime_64); + typename SolverContext::result_type mulsh = + bvExtract(mult_64, 63, 32); // upper 32-bits + typename SolverContext::result_type n_plus_mulsh = + evaluate(_solver, bvadd(expr_n, mulsh)); + + // Improved variable arithmetic right shift: sign extend, shift, extract. + typename SolverContext::result_type extend_npm = + evaluate(_solver, sign_extend(64 - width, n_plus_mulsh)); + typename SolverContext::result_type shift_npm = + bvVarRightShift(extend_npm, expr_shpost, 64); + typename SolverContext::result_type shift_shpost = + bvExtract(shift_npm, 31, 0); // lower 32-bits + + ///////////// + + // XSIGN(n) is -1 if n is negative, positive one otherwise + typename SolverContext::result_type is_signed = bvBoolExtract(expr_n, 31); + typename SolverContext::result_type neg_one = bvMinusOne(32); + typename SolverContext::result_type xsign_of_n = + evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32))); + + // q0 = (n_plus_mulsh >> shpost) - XSIGN(n) + typename SolverContext::result_type q0 = + evaluate(_solver, bvsub(shift_shpost, xsign_of_n)); + + // n/d = (q0 ^ dsign) - dsign + typename SolverContext::result_type q0_xor_dsign = + evaluate(_solver, bvxor(q0, expr_dsign)); + typename SolverContext::result_type res = + evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign)); + + return (res); } -template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { - - typename SolverContext::result_type res; - unsigned shift = amount & ((1 << shiftBits) - 1); +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) { + + 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) { + + 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) { + + // 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 +986,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..56964b5d 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -19,11 +19,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> diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 994386ab..96a7dafa 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -15,6 +15,8 @@ #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/ErrorHandling.h" + namespace klee { class Z3SolverImpl : public SolverImpl { diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h index cb86295c..4a6fbc15 100644 --- a/runtime/POSIX/fd.h +++ b/runtime/POSIX/fd.h @@ -71,9 +71,9 @@ typedef struct { extern exe_file_system_t __exe_fs; extern exe_sym_env_t __exe_env; -void klee_init_fds(unsigned n_files, unsigned file_length, - int sym_stdout_flag, int do_all_writes_flag, - unsigned max_failures); +void klee_init_fds(unsigned n_files, unsigned file_length, + unsigned stdin_length, int sym_stdout_flag, + int do_all_writes_flag, unsigned max_failures); void klee_init_env(int *argcPtr, char ***argvPtr); /* *** */ diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 8b69fd04..9184b7ea 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -107,9 +107,9 @@ static unsigned __sym_uint32(const char *name) { writes past the initial file size are discarded (file offset is always incremented) max_failures: maximum number of system call failures */ -void klee_init_fds(unsigned n_files, unsigned file_length, - int sym_stdout_flag, int save_all_writes_flag, - unsigned max_failures) { +void klee_init_fds(unsigned n_files, unsigned file_length, + unsigned stdin_length, int sym_stdout_flag, + int save_all_writes_flag, unsigned max_failures) { unsigned k; char name[7] = "?-data"; struct stat64 s; @@ -124,9 +124,9 @@ void klee_init_fds(unsigned n_files, unsigned file_length, } /* setting symbolic stdin */ - if (file_length) { + if (stdin_length) { __exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin)); - __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s); + __create_new_dfile(__exe_fs.sym_stdin, stdin_length, "stdin", &s); __exe_env.fds[0].dfile = __exe_fs.sym_stdin; } else __exe_fs.sym_stdin = NULL; diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index cbcf31f4..7ac9804c 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -90,6 +90,7 @@ void klee_init_env(int* argcPtr, char*** argvPtr) { char* new_argv[1024]; unsigned max_len, min_argvs, max_argvs; unsigned sym_files = 0, sym_file_len = 0; + unsigned sym_stdin_len = 0; int sym_stdout_flag = 0; int save_all_writes_flag = 0; int fd_fail = 0; @@ -102,15 +103,16 @@ void klee_init_env(int* argcPtr, char*** argvPtr) { // Recognize --help when it is the sole argument. if (argc == 2 && __streq(argv[1], "--help")) { - __emit_error("klee_init_env\n\n\ + __emit_error("klee_init_env\n\n\ usage: (klee_init_env) [options] [program arguments]\n\ -sym-arg <N> - Replace by a symbolic argument with length N\n\ -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most\n\ MAX arguments, each with maximum length N\n\ - -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each\n\ - with maximum size N.\n\ + -sym-files <NUM> <N> - Make NUM symbolic files ('A', 'B', 'C', etc.),\n\ + each with size N\n\ + -sym-stdin <N> - Make stdin symbolic with size N.\n\ -sym-stdout - Make stdout symbolic.\n\ - -max-fail <N> - Allow up to <N> injected failures\n\ + -max-fail <N> - Allow up to N injected failures\n\ -fd-fail - Shortcut for '-max-fail 1'\n\n"); } @@ -156,8 +158,17 @@ usage: (klee_init_env) [options] [program arguments]\n\ sym_files = __str_to_int(argv[k++], msg); sym_file_len = __str_to_int(argv[k++], msg); - } - else if (__streq(argv[k], "--sym-stdout") || __streq(argv[k], "-sym-stdout")) { + } else if (__streq(argv[k], "--sym-stdin") || + __streq(argv[k], "-sym-stdin")) { + const char *msg = + "--sym-stdin expects one integer argument <sym-stdin-len>"; + + if (++k == argc) + __emit_error(msg); + + sym_stdin_len = __str_to_int(argv[k++], msg); + } else if (__streq(argv[k], "--sym-stdout") || + __streq(argv[k], "-sym-stdout")) { sym_stdout_flag = 1; k++; } @@ -190,8 +201,7 @@ usage: (klee_init_env) [options] [program arguments]\n\ *argcPtr = new_argc; *argvPtr = final_argv; - klee_init_fds(sym_files, sym_file_len, - sym_stdout_flag, save_all_writes_flag, - fd_fail); + klee_init_fds(sym_files, sym_file_len, sym_stdin_len, sym_stdout_flag, + save_all_writes_flag, fd_fail); } 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/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c index c2e5596b..9d7e358f 100644 --- a/test/Runtime/POSIX/FD_Fail2.c +++ b/test/Runtime/POSIX/FD_Fail2.c @@ -18,7 +18,8 @@ #include <sys/types.h> #include <sys/stat.h> #include <fcntl.h> -#include <stdio.h> +#include <string.h> +#include <unistd.h> int main(int argc, char** argv) { char buf[1024]; @@ -28,7 +29,7 @@ int main(int argc, char** argv) { int r; - r = read(fd, buf, 1, 5); + r = read(fd, buf, 5); if (r != -1) printf("read() succeeded %u\n", fd); else printf("read() failed with error '%s'\n", strerror(errno)); diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c index 241c5cbb..fdfc6ceb 100644 --- a/test/Runtime/POSIX/Isatty.c +++ b/test/Runtime/POSIX/Isatty.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout > %t.log 2>&1 +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 --sym-stdout > %t.log 2>&1 // RUN: test -f %t.klee-out/test000001.ktest // RUN: test -f %t.klee-out/test000002.ktest // RUN: test -f %t.klee-out/test000003.ktest diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c index ebf16405..09eed6d2 100644 --- a/test/Runtime/POSIX/Stdin.c +++ b/test/Runtime/POSIX/Stdin.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-stdin 4 > %t.log // RUN: grep "mode:file" %t.log // RUN: grep "mode:dir" %t.log // RUN: grep "mode:chr" %t.log diff --git a/test/Solver/2016-04-12-array-parsing-bug.kquery b/test/Solver/2016-04-12-array-parsing-bug.kquery new file mode 100644 index 00000000..d53fa35f --- /dev/null +++ b/test/Solver/2016-04-12-array-parsing-bug.kquery @@ -0,0 +1,227 @@ +# RUN: %kleaver %s > %t +# RUN: %kleaver --clear-array-decls-after-query %s > %t + +array A-data[8] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array arg0[3] : w32 -> w8 = symbolic +array arg1[3] : w32 -> w8 = symbolic +array const_arr1[768] : w32 -> w8 = [0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 3 32 2 32 2 32 2 32 2 32 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 1 96 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 213 8 213 8 213 8 213 8 213 8 213 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 4 192 4 192 4 192 4 192 4 192 4 192 8 214 8 214 8 214 8 214 8 214 8 214 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 4 192 4 192 4 192 4 192 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0] +array const_arr8[277] : w32 -> w8 = [0 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 24 2 2 25 2 2 2 2 2 2 2 2 2 2 23 2 2 2 2 2 22 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21] +array model_version[4] : w32 -> w8 = symbolic +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array stdin[8] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +array stdout[1024] : w32 -> w8 = symbolic +array stdout-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) + 2) + (Eq false (Slt 0 N0)) + (Ult N1:(ReadLSB w32 0 n_args_1) + 3) + (Slt 0 N1) + (Slt 1 N1) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 A-data-stat) + 2147483647))) + (Ult (ReadLSB w64 56 A-data-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdin-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdin-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdout-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdout-stat) + 65536) + (Eq 1 + (ReadLSB w32 0 model_version)) + (Eq 45 (Read w8 0 arg0)) + (Eq false + (Eq 0 N2:(Read w8 1 arg0))) + (Eq false (Eq 45 N2)) + (Eq 100 + (AShr w32 (Shl w32 (SExt w32 N2) 24) + 24)) + (Eq 0 + (And w16 (ReadLSB w16 N3:(Extract w32 0 (Add w64 256 + (Mul w64 2 + (ZExt w64 N4:(Read w8 0 arg1))))) const_arr1) + 8192)) + (Eq false (Eq 84 N4)) + (Eq false + (Ult (Add w64 18446744073664565360 + N5:(Select w64 (Eq 0 N4) 44986256 51741584)) + 2)) + (Eq false + (Ult (Add w32 4294967248 + (ZExt w32 N6:(Read w8 (Extract w32 0 (Add w64 18446744073657810032 N5)) + U0:[2=0] @ arg1))) + 10)) + (Eq false (Eq 45 N6)) + (Eq false (Eq 43 N6)) + (Eq 0 + (And w16 (ReadLSB w16 N7:(Extract w32 0 (Add w64 256 + (Mul w64 2 (ZExt w64 N6)))) const_arr1) + 1024)) + (Eq false (Eq 40 N6)) + (Eq false + (Slt N8:(SExt w32 N6) 1)) + (Ult 96 + (Add w32 4294967286 + (ZExt w32 (Read w8 (Extract w32 0 (SExt w64 N8)) + const_arr8)))) + (Eq 7 (Read w8 0 U0)) + (Eq 13 (Read w8 1 U0))] + false [] + [n_args + n_args_1 + arg0 + arg1 + A-data + A-data-stat + stdin + stdin-stat + stdout + stdout-stat + model_version]) + +array A-data[8] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array arg0[11] : w32 -> w8 = symbolic +array arg1[3] : w32 -> w8 = symbolic +array model_version[4] : w32 -> w8 = symbolic +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array stdin[8] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +array stdout[1024] : w32 -> w8 = symbolic +array stdout-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) + 2) + (Slt 0 N0) + (Ult N1:(ReadLSB w32 0 n_args_1) + 3) + (Slt 0 N1) + (Eq false (Slt 1 N1)) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 A-data-stat) + 2147483647))) + (Ult (ReadLSB w64 56 A-data-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdin-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdin-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdout-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdout-stat) + 65536) + (Eq 1 + (ReadLSB w32 0 model_version)) + (Eq 45 (Read w8 0 arg0)) + (Eq 45 (Read w8 1 arg0)) + (Eq 61 (Read w8 3 arg0)) + (Eq 116 (Read w8 2 arg0)) + (Eq false + (Eq 0 (Read w8 4 arg0))) + (Eq false + (Eq 0 + N2:(Read w8 7 U0:[10=0] @ arg0))) + (Eq 0 (Read w8 8 U0)) + (Eq 11 (Read w8 4 U0)) + (Eq 63 (Read w8 5 U0)) + (Eq 8 (Read w8 6 U0)) + (Eq false (Eq 39 N2)) + (Or (Eq 122 N2) + (Or (Eq 121 N2) + (Or (Eq 120 N2) + (Or (Eq 119 N2) + (Or (Eq 118 N2) + (Or (Eq 117 N2) + (Or (Eq 116 N2) + (Or (Eq 115 N2) + (Or (Eq 114 N2) + (Or (Eq 113 N2) + (Or (Eq 112 N2) + (Or (Eq 111 N2) + (Or (Eq 110 N2) + (Or (Eq 109 N2) + (Or (Eq 108 N2) + (Or (Eq 107 N2) + (Or (Eq 106 N2) + (Or (Eq 105 N2) + (Or (Eq 104 N2) + (Or (Eq 103 N2) + (Or (Eq 102 N2) + (Or (Eq 101 N2) + (Or (Eq 100 N2) + (Or (Eq 99 N2) + (Or (Eq 98 N2) + (Or (Eq 97 N2) + (Or (Eq 95 N2) + (Or (Eq 93 N2) + (Or (Eq 90 N2) + (Or (Eq 89 N2) + (Or (Eq 88 N2) + (Or (Eq 87 N2) + (Or (Eq 86 N2) + (Or (Eq 85 N2) + (Or (Eq 84 N2) + (Or (Eq 83 N2) + (Or (Eq 82 N2) + (Or (Eq 81 N2) + (Or (Eq 80 N2) + (Or (Eq 79 N2) + (Or (Eq 78 N2) + (Or (Eq 77 N2) + (Or (Eq 76 N2) + (Or (Eq 75 N2) + (Or (Eq 74 N2) + (Or (Eq 73 N2) + (Or (Eq 72 N2) + (Or (Eq 71 N2) + (Or (Eq 70 N2) + (Or (Eq 69 N2) + (Or (Eq 68 N2) + (Or (Eq 67 N2) + (Or (Eq 66 N2) + (Or (Eq 65 N2) + (Or (Eq 58 N2) + (Or (Eq 57 N2) + (Or (Eq 56 N2) + (Or (Eq 55 N2) + (Or (Eq 54 N2) + (Or (Eq 53 N2) + (Or (Eq 52 N2) + (Or (Eq 51 N2) + (Or (Eq 50 N2) + (Or (Eq 49 N2) + (Or (Eq 48 N2) + (Or (Eq 47 N2) + (Or (Eq 46 N2) + (Or (Eq 45 N2) + (Or (Eq 44 N2) + (Or (Eq 43 N2) (Eq 37 N2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))] + false [] + [n_args + arg0 + n_args_1 + arg1 + A-data + A-data-stat + stdin + stdin-stat + stdout + stdout-stat + model_version]) \ No newline at end of file diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 9c374eb8..a937d761 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -95,6 +95,11 @@ namespace { llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."), llvm::cl::init(".")); + llvm::cl::opt<bool> ClearArrayAfterQuery( + "clear-array-decls-after-query", + llvm::cl::desc("We discard the previous array declarations after a query " + "is performed. Default: false"), + llvm::cl::init(false)); } static std::string getQueryLogPath(const char filename[]) @@ -160,7 +165,7 @@ static bool PrintInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) { std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB, Builder); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); P->SetMaxErrors(20); unsigned NumQueries = 0; @@ -193,7 +198,7 @@ static bool EvaluateInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) { std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB, Builder); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); @@ -327,8 +332,8 @@ static bool printInputAsSMTLIBv2(const char *Filename, { //Parse the input file std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB, Builder); - P->SetMaxErrors(20); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); + P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 391c8fa2..de04d92e 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -606,11 +606,15 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { SmallString<128> libDir; - if ( strcmp(toolRoot.c_str(), KLEE_INSTALL_BIN_DIR ) == 0) + if (strlen( KLEE_INSTALL_BIN_DIR ) != 0 && + strlen( KLEE_INSTALL_RUNTIME_DIR ) != 0 && + toolRoot.str().endswith( KLEE_INSTALL_BIN_DIR )) { KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << "Using installed KLEE library runtime: "); - libDir = KLEE_INSTALL_RUNTIME_DIR ; + libDir = toolRoot.str().substr(0, + toolRoot.str().size() - strlen( KLEE_INSTALL_BIN_DIR )); + llvm::sys::path::append(libDir, KLEE_INSTALL_RUNTIME_DIR); } else { |