diff options
Diffstat (limited to 'lib')
32 files changed, 2240 insertions, 371 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index ac0474fb..eac54141 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,5 +73,22 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( llvm::cl::CommaSeparated ); +#ifdef SUPPORT_METASMT + +llvm::cl::opt<klee::MetaSMTBackendType> +UseMetaSMT("use-metasmt", + llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."), + llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"), + clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), + clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), + clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), + clEnumValEnd), + llvm::cl::init(METASMT_BACKEND_NONE)); + +#endif /* SUPPORT_METASMT */ + } + + + diff --git a/lib/Core/CallPathManager.cpp b/lib/Core/CallPathManager.cpp index ca127f25..03e75108 100644 --- a/lib/Core/CallPathManager.cpp +++ b/lib/Core/CallPathManager.cpp @@ -13,7 +13,12 @@ #include <map> #include <vector> +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else #include "llvm/Function.h" +#endif + #include "llvm/Support/raw_ostream.h" using namespace llvm; diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp index 979970aa..935e4316 100644 --- a/lib/Core/Context.cpp +++ b/lib/Core/Context.cpp @@ -11,8 +11,13 @@ #include "klee/Expr.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Type.h" +#include "llvm/IR/DerivedTypes.h" +#else #include "llvm/Type.h" #include "llvm/DerivedTypes.h" +#endif #include <cassert> diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index db685639..b2c2a737 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -17,8 +17,11 @@ #include "klee/Expr.h" #include "Memory.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else #include "llvm/Function.h" +#endif #include "llvm/Support/CommandLine.h" #include <iostream> diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 069022a2..ef55f21f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -24,6 +24,7 @@ #include "StatsTracker.h" #include "TimingSolver.h" #include "UserSearcher.h" +#include "ExecutorTimerInfo.h" #include "../Solver/SolverStats.h" #include "klee/ExecutionState.h" @@ -47,31 +48,40 @@ #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Attributes.h" +#include "llvm/IR/BasicBlock.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#include "llvm/IR/TypeBuilder.h" +#else #include "llvm/Attributes.h" #include "llvm/BasicBlock.h" #include "llvm/Constants.h" #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" +#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) +#include "llvm/Target/TargetData.h" +#else +#include "llvm/DataLayout.h" +#include "llvm/TypeBuilder.h" +#endif +#endif #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CallSite.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif -#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) -#include "llvm/Target/TargetData.h" -#else -#include "llvm/DataLayout.h" -#endif #include <cassert> #include <algorithm> @@ -90,6 +100,33 @@ using namespace llvm; using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + namespace { cl::opt<bool> DumpStatesOnHalt("dump-states-on-halt", @@ -253,7 +290,41 @@ Executor::Executor(const InterpreterOptions &opts, : std::max(MaxCoreSolverTime,MaxInstructionTime)) { if (coreSolverTimeout) UseForkedCoreSolver = true; - Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + + Solver *coreSolver = NULL; + +#ifdef SUPPORT_METASMT + if (UseMetaSMT != METASMT_BACKEND_NONE) { + + std::string backend; + + switch (UseMetaSMT) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + assert(false); + break; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + } +#else + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#endif /* SUPPORT_METASMT */ + + Solver *solver = constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), @@ -309,6 +380,10 @@ Executor::~Executor() { delete statsTracker; delete solver; delete kmodule; + while(!timers.empty()) { + delete timers.back(); + timers.pop_back(); + } } /***/ @@ -386,10 +461,10 @@ void Executor::initializeGlobals(ExecutionState &state) { if (m->getModuleInlineAsm() != "") klee_warning("executable has module level assembly (ignoring)"); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) assert(m->lib_begin() == m->lib_end() && "XXX do not support dependent libraries"); - +#endif // represent function globals using the address of the actual llvm function // object. given that we use malloc to allocate memory in states this also // ensures that we won't conflict. we don't need to allocate a memory object @@ -501,9 +576,17 @@ void Executor::initializeGlobals(ExecutionState &state) { uint64_t size = kmodule->targetData->getTypeStoreSize(ty); MemoryObject *mo = 0; +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) if (UseAsmAddresses && i->getName()[0]=='\01') { +#else + if (UseAsmAddresses && !i->getName().empty()) { +#endif char *end; +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) uint64_t address = ::strtoll(i->getName().str().c_str()+1, &end, 0); +#else + uint64_t address = ::strtoll(i->getName().str().c_str(), &end, 0); +#endif if (end && *end == '\0') { klee_message("NOTE: allocated global at asm specified address: %#08llx" @@ -557,20 +640,31 @@ void Executor::branch(ExecutionState &state, unsigned N = conditions.size(); assert(N); - stats::forks += N-1; + if (MaxForks!=~0u && stats::forks >= MaxForks) { + unsigned next = theRNG.getInt32() % N; + for (unsigned i=0; i<N; ++i) { + if (i == next) { + result.push_back(&state); + } else { + result.push_back(NULL); + } + } + } else { + stats::forks += N-1; - // XXX do proper balance or keep random? - result.push_back(&state); - for (unsigned i=1; i<N; ++i) { - ExecutionState *es = result[theRNG.getInt32() % i]; - ExecutionState *ns = es->branch(); - addedStates.insert(ns); - result.push_back(ns); - es->ptreeNode->data = 0; - std::pair<PTree::Node*,PTree::Node*> res = - processTree->split(es->ptreeNode, ns, es); - ns->ptreeNode = res.first; - es->ptreeNode = res.second; + // XXX do proper balance or keep random? + result.push_back(&state); + for (unsigned i=1; i<N; ++i) { + ExecutionState *es = result[theRNG.getInt32() % i]; + ExecutionState *ns = es->branch(); + addedStates.insert(ns); + result.push_back(ns); + es->ptreeNode->data = 0; + std::pair<PTree::Node*,PTree::Node*> res = + processTree->split(es->ptreeNode, ns, es); + ns->ptreeNode = res.first; + es->ptreeNode = res.second; + } } // If necessary redistribute seeds to match conditions, killing @@ -605,12 +699,14 @@ void Executor::branch(ExecutionState &state, if (i==N) i = theRNG.getInt32() % N; - seedMap[result[i]].push_back(*siit); + // Extra check in case we're replaying seeds with a max-fork + if (result[i]) + seedMap[result[i]].push_back(*siit); } if (OnlyReplaySeeds) { for (unsigned i=0; i<N; ++i) { - if (!seedMap.count(result[i])) { + if (result[i] && !seedMap.count(result[i])) { terminateState(*result[i]); result[i] = NULL; } @@ -1302,26 +1398,9 @@ Function* Executor::getTargetFunction(Value *calledVal, ExecutionState &state) { } } +/// TODO remove? static bool isDebugIntrinsic(const Function *f, KModule *KM) { -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - // Fast path, getIntrinsicID is slow. - if (f == KM->dbgStopPointFn) - return true; - - switch (f->getIntrinsicID()) { - case Intrinsic::dbg_stoppoint: - case Intrinsic::dbg_region_start: - case Intrinsic::dbg_region_end: - case Intrinsic::dbg_func_start: - case Intrinsic::dbg_declare: - return true; - - default: - return false; - } -#else return false; -#endif } static inline const llvm::fltSemantics * fpWidthToSemantics(unsigned width) { @@ -1380,7 +1459,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { CallSite(cast<CallInst>(caller))); // XXX need to check other param attrs ? -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) bool isSExt = cs.paramHasAttr(0, llvm::Attributes::SExt); #else bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt); @@ -1584,7 +1665,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (from != to) { // XXX need to check other param attrs ? -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) bool isSExt = cs.paramHasAttr(i+1, llvm::Attributes::SExt); #else bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt); @@ -1867,14 +1950,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } // Memory instructions... -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - case Instruction::Malloc: - case Instruction::Alloca: { - AllocationInst *ai = cast<AllocationInst>(i); -#else case Instruction::Alloca: { AllocaInst *ai = cast<AllocaInst>(i); -#endif unsigned elementSize = kmodule->targetData->getTypeStoreSize(ai->getAllocatedType()); ref<Expr> size = Expr::createPointer(elementSize); @@ -1887,12 +1964,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { executeAlloc(state, size, isLocal, ki); break; } -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - case Instruction::Free: { - executeFree(state, eval(ki, 0, state).value); - break; - } -#endif case Instruction::Load: { ref<Expr> base = eval(ki, 0, state).value; @@ -1982,8 +2053,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FAdd operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.add(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -1996,9 +2072,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(left->getWidth()) || !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FSub operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.subtract(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2012,8 +2092,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FMul operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.multiply(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2027,8 +2112,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FDiv operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.divide(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2041,9 +2131,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(left->getWidth()) || !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FRem operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.remainder(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue())); +#else llvm::APFloat Res(left->getAPValue()); Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2056,7 +2150,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth()) return terminateStateOnExecError(state, "Unsupported FPTrunc operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Res(arg->getAPValue()); +#endif bool losesInfo = false; Res.convert(*fpWidthToSemantics(resultType), llvm::APFloat::rmNearestTiesToEven, @@ -2072,8 +2170,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType) return terminateStateOnExecError(state, "Unsupported FPExt operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Res(arg->getAPValue()); +#endif bool losesInfo = false; Res.convert(*fpWidthToSemantics(resultType), llvm::APFloat::rmNearestTiesToEven, @@ -2090,7 +2191,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToUI operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Arg(arg->getAPValue()); +#endif uint64_t value = 0; bool isExact = true; Arg.convertToInteger(&value, resultType, false, @@ -2106,8 +2211,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToSI operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Arg(arg->getAPValue()); + +#endif uint64_t value = 0; bool isExact = true; Arg.convertToInteger(&value, resultType, true, @@ -2158,8 +2267,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FCmp operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + APFloat LHS(*fpWidthToSemantics(left->getWidth()),left->getAPValue()); + APFloat RHS(*fpWidthToSemantics(right->getWidth()),right->getAPValue()); +#else APFloat LHS(left->getAPValue()); APFloat RHS(right->getAPValue()); +#endif APFloat::cmpResult CmpRes = LHS.compare(RHS); bool Result = false; @@ -2470,8 +2584,11 @@ void Executor::run(ExecutionState &initialState) { // We need to avoid calling GetMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + unsigned mbs = sys::Process::GetMallocUsage() >> 20; +#else unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20; - +#endif if (mbs > MaxMemory) { if (mbs > MaxMemory + 100) { // just guess at how many to kill diff --git a/lib/Core/ExecutorTimerInfo.h b/lib/Core/ExecutorTimerInfo.h new file mode 100644 index 00000000..60977b74 --- /dev/null +++ b/lib/Core/ExecutorTimerInfo.h @@ -0,0 +1,42 @@ +//===-- Executor.h ----------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// Class to wrap information for a timer. +// +//===----------------------------------------------------------------------===// + +#ifndef EXECUTORTIMERINFO_H_ +#define EXECUTORTIMERINFO_H_ + +#include "klee/Internal/System/Time.h" + +namespace klee { + +class Executor::TimerInfo { +public: + Timer *timer; + + /// Approximate delay per timer firing. + double rate; + /// Wall time for next firing. + double nextFireTime; + +public: + TimerInfo(Timer *_timer, double _rate) + : timer(_timer), + rate(_rate), + nextFireTime(util::getWallTime() + rate) {} + ~TimerInfo() { delete timer; } +}; + + +} + + +#endif /* EXECUTORTIMERINFO_H_ */ diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 2fda5cba..06fd4be7 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -13,6 +13,7 @@ #include "Executor.h" #include "PTree.h" #include "StatsTracker.h" +#include "ExecutorTimerInfo.h" #include "klee/ExecutionState.h" #include "klee/Internal/Module/InstructionInfoTable.h" @@ -20,7 +21,12 @@ #include "klee/Internal/Module/KModule.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else #include "llvm/Function.h" +#endif + #include "llvm/Support/CommandLine.h" #include <unistd.h> @@ -88,7 +94,7 @@ void Executor::initTimers() { } if (MaxTime) { - addTimer(new HaltTimer(this), MaxTime); + addTimer(new HaltTimer(this), MaxTime.getValue()); } } @@ -98,23 +104,6 @@ Executor::Timer::Timer() {} Executor::Timer::~Timer() {} -class Executor::TimerInfo { -public: - Timer *timer; - - /// Approximate delay per timer firing. - double rate; - /// Wall time for next firing. - double nextFireTime; - -public: - TimerInfo(Timer *_timer, double _rate) - : timer(_timer), - rate(_rate), - nextFireTime(util::getWallTime() + rate) {} - ~TimerInfo() { delete timer; } -}; - void Executor::addTimer(Timer *timer, double rate) { timers.push_back(new TimerInfo(timer, rate)); } diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 0d85afee..0d828ec4 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -20,19 +20,27 @@ #include "klee/util/GetElementPtrTypeIterator.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#else #include "llvm/Constants.h" #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -#include "llvm/ModuleProvider.h" -#endif -#include "llvm/Support/CallSite.h" #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif + +#include "llvm/Support/CallSite.h" + + #include <iostream> #include <cassert> diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp index 7da0c350..2dc16767 100644 --- a/lib/Core/ExternalDispatcher.cpp +++ b/lib/Core/ExternalDispatcher.cpp @@ -17,24 +17,23 @@ #undef PACKAGE_TARNAME #undef PACKAGE_VERSION +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Module.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/Module.h" #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Instructions.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -#include "llvm/ModuleProvider.h" -#endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif #include "llvm/ExecutionEngine/JIT.h" #include "llvm/ExecutionEngine/GenericValue.h" #include "llvm/Support/CallSite.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/DynamicLibrary.h" -#else #include "llvm/Support/DynamicLibrary.h" -#endif #include "llvm/Support/raw_ostream.h" #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0) #include "llvm/Target/TargetSelect.h" @@ -89,16 +88,9 @@ void *ExternalDispatcher::resolveSymbol(const std::string &name) { ExternalDispatcher::ExternalDispatcher() { dispatchModule = new Module("ExternalDispatcher", getGlobalContext()); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - ExistingModuleProvider* MP = new ExistingModuleProvider(dispatchModule); -#endif std::string error; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - executionEngine = ExecutionEngine::createJIT(MP, &error); -#else executionEngine = ExecutionEngine::createJIT(dispatchModule, &error); -#endif if (!executionEngine) { std::cerr << "unable to make jit: " << error << "\n"; abort(); diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 08c95d48..4bcdd9f7 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -19,9 +19,16 @@ #include "ObjectHolder.h" #include "MemoryManager.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include <llvm/IR/Function.h> +#include <llvm/IR/Instruction.h> +#include <llvm/IR/Value.h> +#else #include <llvm/Function.h> #include <llvm/Instruction.h> #include <llvm/Value.h> +#endif + #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 778ef0ef..2dbabd01 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -25,10 +25,15 @@ #include "klee/Internal/ADT/RNG.h" #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#else #include "llvm/Constants.h" #include "llvm/Instructions.h" #include "llvm/Module.h" +#endif #include "llvm/Support/CallSite.h" #include "llvm/Support/CFG.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index d44e13b6..04f32780 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -21,7 +21,11 @@ #include "Executor.h" #include "MemoryManager.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Module.h" +#else #include "llvm/Module.h" +#endif #include "llvm/ADT/Twine.h" #include <errno.h> @@ -131,7 +135,9 @@ void SpecialFunctionHandler::prepare() { // Make sure NoReturn attribute is set, for optimization and // coverage counting. if (hi.doesNotReturn) -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + f->addFnAttr(Attribute::NoReturn); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) f->addFnAttr(Attributes::NoReturn); #else f->addFnAttr(Attribute::NoReturn); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index c0028a05..8161a52c 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -27,6 +27,15 @@ #include "UserSearcher.h" #include "../Solver/SolverStats.h" +#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) +#include "llvm/IR/BasicBlock.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/InlineAsm.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Type.h" +#else #include "llvm/BasicBlock.h" #include "llvm/Function.h" #include "llvm/Instructions.h" @@ -34,21 +43,15 @@ #include "llvm/InlineAsm.h" #include "llvm/Module.h" #include "llvm/Type.h" +#endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/CFG.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else +#include "llvm/Support/raw_os_ostream.h" #include "llvm/Support/Process.h" -#endif -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Path.h" -#else #include "llvm/Support/Path.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) #include "llvm/Support/FileSystem.h" #endif -#endif #include <iostream> #include <fstream> @@ -294,9 +297,6 @@ void StatsTracker::stepInstruction(ExecutionState &es) { // // FIXME: This trick no longer works, we should fix this in the line // number propogation. -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - if (isa<DbgStopPointInst>(inst)) -#endif es.coveredLines[&ii.file].insert(ii.line); es.coveredNew = true; es.instsSinceCovNew = 1; @@ -401,7 +401,11 @@ void StatsTracker::writeStatsLine() { << "," << numBranches << "," << util::getUserTime() << "," << executor.states.size() +#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) + << "," << sys::Process::GetMallocUsage() +#else << "," << sys::Process::GetTotalMemoryUsage() +#endif << "," << stats::queries << "," << stats::queryConstructs << "," << 0 // was numObjects diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index d2c07f46..037b23f3 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -16,11 +16,7 @@ #include "CoreStats.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif using namespace klee; using namespace llvm; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index b759daae..90d9bcd4 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -11,6 +11,13 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#else +#include "llvm/Function.h" +#endif +#include "llvm/Support/CommandLine.h" +#include "klee/Internal/Module/KModule.h" #include <iostream> #include <map> diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index a28ad907..82c60205 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -354,11 +354,7 @@ void ConstantExpr::toString(std::string &Res, unsigned radix) const { ref<ConstantExpr> ConstantExpr::Concat(const ref<ConstantExpr> &RHS) { Expr::Width W = getWidth() + RHS->getWidth(); APInt Tmp(value); -#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8) - Tmp.zext(W); -#else Tmp=Tmp.zext(W); -#endif Tmp <<= RHS->getWidth(); Tmp |= APInt(RHS->value).zext(W); diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 3871286e..5b3e96b7 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -1496,17 +1496,9 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) { Val = -Val; if (Type < Val.getBitWidth()) -#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8) - Val.trunc(Type); -#else Val=Val.trunc(Type); -#endif else if (Type > Val.getBitWidth()) -#if LLVM_VERSION_CODE <= LLVM_VERSION(2, 8) - Val.zext(Type); -#else Val=Val.zext(Type); -#endif return ExprResult(Builder->Constant(Val)); } diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp index 18ef398a..79fd4afc 100644 --- a/lib/Module/Checks.cpp +++ b/lib/Module/Checks.cpp @@ -11,6 +11,19 @@ #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/InstrTypes.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Type.h" +#include "llvm/IR/DataLayout.h" +#else #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Function.h" @@ -18,19 +31,22 @@ #include "llvm/Instruction.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" -#include "llvm/Pass.h" #include "llvm/Type.h" -#include "llvm/Transforms/Scalar.h" -#include "llvm/Transforms/Utils/BasicBlockUtils.h" + +#include "llvm/LLVMContext.h" + #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif +#include "llvm/Pass.h" +#include "llvm/Transforms/Scalar.h" +#include "llvm/Transforms/Utils/BasicBlockUtils.h" +#include "llvm/Support/CallSite.h" +#include <iostream> using namespace llvm; using namespace klee; @@ -76,3 +92,62 @@ bool DivCheckPass::runOnModule(Module &M) { } return moduleChanged; } + +char OvershiftCheckPass::ID; + +bool OvershiftCheckPass::runOnModule(Module &M) { + Function *overshiftCheckFunction = 0; + + bool moduleChanged = false; + + for (Module::iterator f = M.begin(), fe = M.end(); f != fe; ++f) { + for (Function::iterator b = f->begin(), be = f->end(); b != be; ++b) { + for (BasicBlock::iterator i = b->begin(), ie = b->end(); i != ie; ++i) { + if (BinaryOperator* binOp = dyn_cast<BinaryOperator>(i)) { + // find all shift instructions + Instruction::BinaryOps opcode = binOp->getOpcode(); + + if (opcode == Instruction::Shl || + opcode == Instruction::LShr || + opcode == Instruction::AShr ) { + std::vector<llvm::Value*> args; + + // Determine bit width of first operand + uint64_t bitWidth=i->getOperand(0)->getType()->getScalarSizeInBits(); + + ConstantInt *bitWidthC = ConstantInt::get(Type::getInt64Ty(getGlobalContext()),bitWidth,false); + args.push_back(bitWidthC); + + CastInst *shift = + CastInst::CreateIntegerCast(i->getOperand(1), + Type::getInt64Ty(getGlobalContext()), + false, /* sign doesn't matter */ + "int_cast_to_i64", + i); + args.push_back(shift); + + + // Lazily bind the function to avoid always importing it. + if (!overshiftCheckFunction) { + Constant *fc = M.getOrInsertFunction("klee_overshift_check", + Type::getVoidTy(getGlobalContext()), + Type::getInt64Ty(getGlobalContext()), + Type::getInt64Ty(getGlobalContext()), + NULL); + overshiftCheckFunction = cast<Function>(fc); + } + + // Inject CallInstr to check if overshifting possible +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0) + CallInst::Create(overshiftCheckFunction, args, "", &*i); +#else + CallInst::Create(overshiftCheckFunction, args.begin(), args.end(), "", &*i); +#endif + moduleChanged = true; + } + } + } + } + } + return moduleChanged; +} diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp index d0ef52d0..301db1ff 100644 --- a/lib/Module/InstructionInfoTable.cpp +++ b/lib/Module/InstructionInfoTable.cpp @@ -10,23 +10,26 @@ #include "klee/Internal/Module/InstructionInfoTable.h" #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#else #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#include "llvm/Linker.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) -#include "llvm/Assembly/AsmAnnotationWriter.h" -#else +#endif +#include "llvm/Linker.h" #include "llvm/Assembly/AssemblyAnnotationWriter.h" #include "llvm/Support/FormattedStream.h" -#endif #include "llvm/Support/CFG.h" #include "llvm/Support/InstIterator.h" #include "llvm/Support/raw_ostream.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) #include "llvm/DebugInfo.h" -#elif LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) +#else #include "llvm/Analysis/DebugInfo.h" #endif #include "llvm/Analysis/ValueTracking.h" @@ -39,12 +42,8 @@ using namespace klee; class InstructionToLineAnnotator : public llvm::AssemblyAnnotationWriter { public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - void emitInstructionAnnot(const Instruction *i, llvm::raw_ostream &os) { -#else void emitInstructionAnnot(const Instruction *i, llvm::formatted_raw_ostream &os) { -#endif os << "%%%"; os << (uintptr_t) i; } @@ -76,18 +75,9 @@ static void buildInstructionToLineMap(Module *m, } } -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) -static std::string getDSPIPath(const DbgStopPointInst *dspi) { - std::string dir, file; - bool res = GetConstantStringInfo(dspi->getDirectory(), dir); - assert(res && "GetConstantStringInfo failed"); - res = GetConstantStringInfo(dspi->getFileName(), file); - assert(res && "GetConstantStringInfo failed"); -#else static std::string getDSPIPath(DILocation Loc) { std::string dir = Loc.getDirectory(); std::string file = Loc.getFilename(); -#endif if (dir.empty() || file[0] == '/') { return file; } else if (*dir.rbegin() == '/') { @@ -100,20 +90,12 @@ static std::string getDSPIPath(DILocation Loc) { bool InstructionInfoTable::getInstructionDebugInfo(const llvm::Instruction *I, const std::string *&File, unsigned &Line) { -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - if (const DbgStopPointInst *dspi = dyn_cast<DbgStopPointInst>(I)) { - File = internString(getDSPIPath(dspi)); - Line = dspi->getLine(); - return true; - } -#else if (MDNode *N = I->getMetadata("dbg")) { DILocation Loc(N); File = internString(getDSPIPath(Loc)); Line = Loc.getLineNumber(); return true; } -#endif return false; } diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 2f18c17e..0f095269 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -10,6 +10,19 @@ #include "Passes.h" #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/DerivedTypes.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/InstrTypes.h" +#include "llvm/IR/Instruction.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/Type.h" +#include "llvm/IR/IRBuilder.h" + +#else #include "llvm/Constants.h" #include "llvm/DerivedTypes.h" #include "llvm/Function.h" @@ -17,24 +30,23 @@ #include "llvm/Instruction.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" -#include "llvm/Pass.h" #include "llvm/Type.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) #include "llvm/IRBuilder.h" #else #include "llvm/Support/IRBuilder.h" #endif -#include "llvm/Transforms/Scalar.h" -#include "llvm/Transforms/Utils/BasicBlockUtils.h" #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif +#include "llvm/Pass.h" +#include "llvm/Transforms/Scalar.h" +#include "llvm/Transforms/Utils/BasicBlockUtils.h" using namespace llvm; @@ -46,11 +58,13 @@ bool IntrinsicCleanerPass::runOnModule(Module &M) { bool dirty = false; for (Module::iterator f = M.begin(), fe = M.end(); f != fe; ++f) for (Function::iterator b = f->begin(), be = f->end(); b != be; ++b) - dirty |= runOnBasicBlock(*b); + dirty |= runOnBasicBlock(*b, M); + if (Function *Declare = M.getFunction("llvm.trap")) + Declare->eraseFromParent(); return dirty; } -bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { +bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { bool dirty = false; #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) @@ -74,13 +88,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { // FIXME: This is much more target dependent than just the word size, // however this works for x86-32 and x86-64. case Intrinsic::vacopy: { // (dst, src) -> *((i8**) dst) = *((i8**) src) -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - Value *dst = ii->getOperand(1); - Value *src = ii->getOperand(2); -#else Value *dst = ii->getArgOperand(0); Value *src = ii->getArgOperand(1); -#endif if (WordSize == 4) { Type *i8pp = PointerType::getUnqual(PointerType::getUnqual(Type::getInt8Ty(getGlobalContext()))); @@ -111,13 +120,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { case Intrinsic::umul_with_overflow: { IRBuilder<> builder(ii->getParent(), ii); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - Value *op1 = ii->getOperand(1); - Value *op2 = ii->getOperand(2); -#else Value *op1 = ii->getArgOperand(0); Value *op2 = ii->getArgOperand(1); -#endif Value *result = 0; if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow) @@ -138,42 +142,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { break; } -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - case Intrinsic::dbg_stoppoint: { - // We can remove this stoppoint if the next instruction is - // sure to be another stoppoint. This is nice for cleanliness - // but also important for switch statements where it can allow - // the targets to be joined. - bool erase = false; - if (isa<DbgStopPointInst>(i) || - isa<UnreachableInst>(i)) { - erase = true; - } else if (isa<BranchInst>(i) || - isa<SwitchInst>(i)) { - BasicBlock *bb = i->getParent(); - erase = true; - for (succ_iterator it=succ_begin(bb), ie=succ_end(bb); - it!=ie; ++it) { - if (!isa<DbgStopPointInst>(it->getFirstNonPHI())) { - erase = false; - break; - } - } - } - - if (erase) { - ii->eraseFromParent(); - dirty = true; - } - break; - } - - case Intrinsic::dbg_region_start: - case Intrinsic::dbg_region_end: - case Intrinsic::dbg_func_start: -#else case Intrinsic::dbg_value: -#endif case Intrinsic::dbg_declare: // Remove these regardless of lower intrinsics flag. This can // be removed once IntrinsicLowering is fixed to not have bad @@ -181,6 +150,24 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) { ii->eraseFromParent(); dirty = true; break; + + case Intrinsic::trap: { + // Intrisic instruction "llvm.trap" found. Directly lower it to + // a call of the abort() function. + Function *F = cast<Function>( + M.getOrInsertFunction( + "abort", Type::getVoidTy(getGlobalContext()), NULL)); + F->setDoesNotReturn(); + F->setDoesNotThrow(); + + CallInst::Create(F, Twine(), ii); + new UnreachableInst(getGlobalContext(), ii); + + ii->eraseFromParent(); + + dirty = true; + break; + } default: if (LowerIntrinsics) diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 1629bb79..d889b51f 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -22,31 +22,37 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "llvm/Bitcode/ReaderWriter.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Instructions.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/ValueSymbolTable.h" +#include "llvm/IR/DataLayout.h" +#else #include "llvm/Instructions.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" -#endif #include "llvm/Module.h" -#include "llvm/PassManager.h" #include "llvm/ValueSymbolTable.h" -#include "llvm/Support/CallSite.h" -#include "llvm/Support/CommandLine.h" -#include "llvm/Support/raw_ostream.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) -#include "llvm/Support/raw_os_ostream.h" -#endif -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Path.h" -#else -#include "llvm/Support/Path.h" -#endif #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif + +#endif + +#include "llvm/PassManager.h" +#include "llvm/Support/CallSite.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" +#include "llvm/Support/raw_os_ostream.h" +#include "llvm/Support/Path.h" #include "llvm/Transforms/Scalar.h" +#include <llvm/Transforms/Utils/Cloning.h> +#include <llvm/Support/InstIterator.h> +#include <llvm/Support/Debug.h> + #include <sstream> using namespace llvm; @@ -99,7 +105,6 @@ KModule::KModule(Module *_module) #else targetData(new DataLayout(module)), #endif - dbgStopPointFn(0), kleeMergeFn(0), infos(0), constantTable(0) { @@ -113,6 +118,10 @@ KModule::~KModule() { ie = functions.end(); it != ie; ++it) delete *it; + for (std::map<llvm::Constant*, KConstant*>::iterator it=constantMap.begin(), + itE=constantMap.end(); it!=itE;++it) + delete it->second; + delete targetData; delete module; } @@ -189,6 +198,7 @@ static void injectStaticConstructorsAndDestructors(Module *m) { } } +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType, ...) { // If module lacks an externally visible symbol for the name then we @@ -211,6 +221,53 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType, m->getOrInsertFunction(name, FunctionType::get(retType, argTypes, false)); } } +#endif + +/// This function will take try to inline all calls to \p functionName +/// in the module \p module . +/// +/// It is intended that this function be used for inling calls to +/// check functions like <tt>klee_div_zero_check()</tt> +static void inlineChecks(Module *module, const char * functionName) { + std::vector<CallInst*> checkCalls; + Function* runtimeCheckCall = module->getFunction(functionName); + if (runtimeCheckCall == 0) + { + DEBUG( klee_warning("Failed to inline %s because no calls were made to it in module", functionName) ); + return; + } + + // Iterate through instructions in module and collect all + // call instructions to "functionName" that we care about. + for (Module::iterator f = module->begin(), fe = module->end(); f != fe; ++f) { + for (inst_iterator i=inst_begin(f), ie = inst_end(f); i != ie; ++i) { + if ( CallInst* ci = dyn_cast<CallInst>(&*i) ) + { + if ( ci->getCalledFunction() == runtimeCheckCall) + checkCalls.push_back(ci); + } + } + } + + unsigned int successCount=0; + unsigned int failCount=0; + InlineFunctionInfo IFI(0,0); + for ( std::vector<CallInst*>::iterator ci = checkCalls.begin(), + cie = checkCalls.end(); + ci != cie; ++ci) + { + // Try to inline the function + if (InlineFunction(*ci,IFI)) + ++successCount; + else + { + ++failCount; + klee_warning("Failed to inline function %s", functionName); + } + } + + DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) ); +} void KModule::prepare(const Interpreter::ModuleOptions &opts, InterpreterHandler *ih) { @@ -272,6 +329,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, PassManager pm; pm.add(new RaiseAsmPass()); if (opts.CheckDivZero) pm.add(new DivCheckPass()); + if (opts.CheckOvershift) pm.add(new OvershiftCheckPass()); // FIXME: This false here is to work around a bug in // IntrinsicLowering which caches values which may eventually be // deleted (via RAUW). This can be removed once LLVM fixes this @@ -281,7 +339,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, if (opts.Optimize) Optimize(module); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) // Force importing functions required by intrinsic lowering. Kind of // unfortunate clutter when we don't need them but we won't know // that until after all linking and intrinsic lowering is @@ -302,16 +360,33 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, PointerType::getUnqual(i8Ty), Type::getInt32Ty(getGlobalContext()), targetData->getIntPtrType(getGlobalContext()), (Type*) 0); - +#endif // FIXME: Missing force import for various math functions. // FIXME: Find a way that we can test programs without requiring // this to be linked in, it makes low level debugging much more // annoying. llvm::sys::Path path(opts.LibraryDir); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + path.appendComponent("kleeRuntimeIntrinsic.bc"); +#else path.appendComponent("libkleeRuntimeIntrinsic.bca"); +#endif module = linkWithLibrary(module, path.c_str()); + /* In order for KLEE to report ALL errors at instrumented + * locations the instrumentation call (e.g. "klee_div_zero_check") + * must be inlined. Otherwise one of the instructions in the + * instrumentation function will be used as the the location of + * the error which means that the error cannot be recorded again + * ( unless -emit-all-errors is used). + */ + if (opts.CheckDivZero) + inlineChecks(module, "klee_div_zero_check"); + if (opts.CheckOvershift) + inlineChecks(module, "klee_overshift_check"); + + // Needs to happen after linking (since ctors/dtors can be modified) // and optimization (since global optimization can rewrite lists). injectStaticConstructorsAndDestructors(module); @@ -332,7 +407,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, pm3.add(new IntrinsicCleanerPass(*targetData)); pm3.add(new PhiCleanerPass()); pm3.run(*module); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) // For cleanliness see if we can discard any of the functions we // forced to import. Function *f; @@ -342,7 +417,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, if (f && f->use_empty()) f->eraseFromParent(); f = module->getFunction("memset"); if (f && f->use_empty()) f->eraseFromParent(); - +#endif // Write out the .ll assembly file. We truncate long lines to work // around a kcachegrind parsing bug (it puts them on new lines), so @@ -351,38 +426,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, std::ostream *os = ih->openOutputFile("assembly.ll"); assert(os && os->good() && "unable to open source output"); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 6) - // We have an option for this in case the user wants a .ll they - // can compile. - if (NoTruncateSourceLines) { - os << *module; - } else { - bool truncated = false; - std::string string; - llvm::raw_string_ostream rss(string); - rss << *module; - rss.flush(); - const char *position = string.c_str(); - - for (;;) { - const char *end = index(position, '\n'); - if (!end) { - os << position; - break; - } else { - unsigned count = (end - position) + 1; - if (count<255) { - os->write(position, count); - } else { - os->write(position, 254); - os << "\n"; - truncated = true; - } - position = end+1; - } - } - } -#else llvm::raw_os_ostream *ros = new llvm::raw_os_ostream(*os); // We have an option for this in case the user wants a .ll they @@ -414,7 +457,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, } } delete ros; -#endif delete os; } @@ -427,7 +469,6 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, delete f; } - dbgStopPointFn = module->getFunction("llvm.dbg.stoppoint"); kleeMergeFn = module->getFunction("klee_merge"); /* Build shadow structures */ diff --git a/lib/Module/LowerSwitch.cpp b/lib/Module/LowerSwitch.cpp index e5382c1a..a98b84ad 100644 --- a/lib/Module/LowerSwitch.cpp +++ b/lib/Module/LowerSwitch.cpp @@ -16,7 +16,9 @@ #include "Passes.h" #include "klee/Config/Version.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/LLVMContext.h" #endif #include <algorithm> diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index 029540ae..fcdfa35a 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -10,26 +10,30 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/Bitcode/ReaderWriter.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IRReader/IRReader.h" +#include "llvm/IR/Module.h" +#include "llvm/Support/SourceMgr.h" +#include "llvm/Support/DataStream.h" +#else #include "llvm/Function.h" #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" -#include "llvm/Linker.h" #include "llvm/Module.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) -#include "llvm/Assembly/AsmAnnotationWriter.h" -#else -#include "llvm/Assembly/AssemblyAnnotationWriter.h" #endif + +#include "llvm/Linker.h" +#include "llvm/Assembly/AssemblyAnnotationWriter.h" #include "llvm/Support/CFG.h" #include "llvm/Support/CallSite.h" #include "llvm/Support/InstIterator.h" #include "llvm/Support/raw_ostream.h" #include "llvm/Analysis/ValueTracking.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Path.h" -#else #include "llvm/Support/Path.h" -#endif #include <map> #include <iostream> @@ -42,6 +46,20 @@ using namespace klee; Module *klee::linkWithLibrary(Module *module, const std::string &libraryName) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + SMDiagnostic err; + std::string err_str; + sys::Path libraryPath(libraryName); + Module *new_mod = ParseIRFile(libraryPath.str(), err, +module->getContext()); + + if (Linker::LinkModules(module, new_mod, Linker::DestroySource, +&err_str)) { + assert(0 && "linked in library failed!"); + } + + return module; +#else Linker linker("klee", module, false); llvm::sys::Path libraryPath(libraryName); @@ -52,6 +70,7 @@ Module *klee::linkWithLibrary(Module *module, } return linker.releaseModule(); +#endif } Function *klee::getDirectCallTarget(CallSite cs) { @@ -72,13 +91,8 @@ Function *klee::getDirectCallTarget(CallSite cs) { } static bool valueIsOnlyCalled(const Value *v) { -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - for (Value::use_const_iterator it = v->use_begin(), ie = v->use_end(); - it != ie; ++it) { -#else for (Value::const_use_iterator it = v->use_begin(), ie = v->use_end(); it != ie; ++it) { -#endif if (const Instruction *instr = dyn_cast<Instruction>(*it)) { if (instr->getOpcode()==0) continue; // XXX function numbering inst if (!isa<CallInst>(instr) && !isa<InvokeInst>(instr)) return false; diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 6da9a2c1..41a106f1 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -16,22 +16,25 @@ //===----------------------------------------------------------------------===// #include "klee/Config/Version.h" -#include "llvm/Module.h" #include "llvm/PassManager.h" #include "llvm/Analysis/Passes.h" #include "llvm/Analysis/LoopPass.h" #include "llvm/Analysis/Verifier.h" #include "llvm/Support/CommandLine.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/DynamicLibrary.h" -#else #include "llvm/Support/DynamicLibrary.h" -#endif + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#else +#include "llvm/Module.h" #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) #include "llvm/Target/TargetData.h" #else #include "llvm/DataLayout.h" #endif +#endif + #include "llvm/Target/TargetMachine.h" #include "llvm/Transforms/IPO.h" #include "llvm/Transforms/Scalar.h" @@ -105,9 +108,6 @@ static void AddStandardCompilePasses(PassManager &PM) { if (DisableOptimizations) return; -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - addPass(PM, createRaiseAllocationsPass()); // call %malloc -> malloc inst -#endif addPass(PM, createCFGSimplificationPass()); // Clean up disgusting code addPass(PM, createPromoteMemoryToRegisterPass());// Kill useless allocas addPass(PM, createGlobalOptimizerPass()); // Optimize out global vars @@ -130,9 +130,6 @@ static void AddStandardCompilePasses(PassManager &PM) { addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs addPass(PM, createScalarReplAggregatesPass()); // Break up aggregate allocas addPass(PM, createInstructionCombiningPass()); // Combine silly seq's -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - addPass(PM, createCondPropagationPass()); // Propagate conditionals -#endif addPass(PM, createTailCallEliminationPass()); // Eliminate tail calls addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs @@ -140,9 +137,6 @@ static void AddStandardCompilePasses(PassManager &PM) { addPass(PM, createLoopRotatePass()); addPass(PM, createLICMPass()); // Hoist loop invariants addPass(PM, createLoopUnswitchPass()); // Unswitch loops. -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) - addPass(PM, createLoopIndexSplitPass()); // Index split loops. -#endif // FIXME : Removing instcombine causes nestedloop regression. addPass(PM, createInstructionCombiningPass()); addPass(PM, createIndVarSimplifyPass()); // Canonicalize indvars @@ -156,9 +150,6 @@ static void AddStandardCompilePasses(PassManager &PM) { // Run instcombine after redundancy elimination to exploit opportunities // opened up by them. addPass(PM, createInstructionCombiningPass()); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 7) - addPass(PM, createCondPropagationPass()); // Propagate conditionals -#endif addPass(PM, createDeadStoreEliminationPass()); // Delete dead stores addPass(PM, createAggressiveDCEPass()); // Delete dead instructions diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h index b3c46124..accb64d0 100644 --- a/lib/Module/Passes.h +++ b/lib/Module/Passes.h @@ -12,9 +12,15 @@ #include "klee/Config/Version.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Constants.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +#else #include "llvm/Constants.h" #include "llvm/Instructions.h" #include "llvm/Module.h" +#endif #include "llvm/Pass.h" #include "llvm/CodeGen/IntrinsicLowering.h" @@ -38,9 +44,7 @@ namespace klee { class RaiseAsmPass : public llvm::ModulePass { static char ID; -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) const llvm::TargetLowering *TLI; -#endif llvm::Function *getIntrinsic(llvm::Module &M, unsigned IID, @@ -55,11 +59,7 @@ class RaiseAsmPass : public llvm::ModulePass { bool runOnInstruction(llvm::Module &M, llvm::Instruction *I); public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - RaiseAsmPass() : llvm::ModulePass((intptr_t) &ID) {} -#else - RaiseAsmPass() : llvm::ModulePass(ID) {} -#endif + RaiseAsmPass() : llvm::ModulePass(ID), TLI(0) {} virtual bool runOnModule(llvm::Module &M); }; @@ -76,7 +76,7 @@ class IntrinsicCleanerPass : public llvm::ModulePass { llvm::IntrinsicLowering *IL; bool LowerIntrinsics; - bool runOnBasicBlock(llvm::BasicBlock &b); + bool runOnBasicBlock(llvm::BasicBlock &b, llvm::Module &M); public: #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) IntrinsicCleanerPass(const llvm::TargetData &TD, @@ -84,11 +84,7 @@ public: IntrinsicCleanerPass(const llvm::DataLayout &TD, #endif bool LI=true) -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - : llvm::ModulePass((intptr_t) &ID), -#else : llvm::ModulePass(ID), -#endif #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) TargetData(TD), #else @@ -117,11 +113,7 @@ class PhiCleanerPass : public llvm::FunctionPass { static char ID; public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - PhiCleanerPass() : llvm::FunctionPass((intptr_t) &ID) {} -#else PhiCleanerPass() : llvm::FunctionPass(ID) {} -#endif virtual bool runOnFunction(llvm::Function &f); }; @@ -129,11 +121,28 @@ public: class DivCheckPass : public llvm::ModulePass { static char ID; public: -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - DivCheckPass(): ModulePass((intptr_t) &ID) {} -#else DivCheckPass(): ModulePass(ID) {} -#endif + virtual bool runOnModule(llvm::Module &M); +}; + +/// This pass injects checks to check for overshifting. +/// +/// Overshifting is where a Shl, LShr or AShr is performed +/// where the shift amount is greater than width of the bitvector +/// being shifted. +/// In LLVM (and in C/C++) this undefined behaviour! +/// +/// Example: +/// \code +/// unsigned char x=15; +/// x << 4 ; // Defined behaviour +/// x << 8 ; // Undefined behaviour +/// x << 255 ; // Undefined behaviour +/// \endcode +class OvershiftCheckPass : public llvm::ModulePass { + static char ID; +public: + OvershiftCheckPass(): ModulePass(ID) {} virtual bool runOnModule(llvm::Module &M); }; @@ -143,11 +152,7 @@ public: class LowerSwitchPass : public llvm::FunctionPass { public: static char ID; // Pass identification, replacement for typeid -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - LowerSwitchPass() : FunctionPass((intptr_t) &ID) {} -#else LowerSwitchPass() : FunctionPass(ID) {} -#endif virtual bool runOnFunction(llvm::Function &F); diff --git a/lib/Module/RaiseAsm.cpp b/lib/Module/RaiseAsm.cpp index b5526f35..d9145a1e 100644 --- a/lib/Module/RaiseAsm.cpp +++ b/lib/Module/RaiseAsm.cpp @@ -9,12 +9,14 @@ #include "Passes.h" #include "klee/Config/Version.h" - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/InlineAsm.h" +#include "llvm/IR/LLVMContext.h" +#else #include "llvm/InlineAsm.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 7) #include "llvm/LLVMContext.h" #endif -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) + #include "llvm/Support/raw_ostream.h" #include "llvm/Support/Host.h" #include "llvm/Target/TargetLowering.h" @@ -23,7 +25,6 @@ #else #include "llvm/Support/TargetRegistry.h" #endif -#endif using namespace llvm; using namespace klee; @@ -47,38 +48,8 @@ Function *RaiseAsmPass::getIntrinsic(llvm::Module &M, bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) { if (CallInst *ci = dyn_cast<CallInst>(I)) { if (InlineAsm *ia = dyn_cast<InlineAsm>(ci->getCalledValue())) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) (void) ia; return TLI && TLI->ExpandInlineAsm(ci); -#else - const std::string &as = ia->getAsmString(); - const std::string &cs = ia->getConstraintString(); - const llvm::Type *T = ci->getType(); - - // bswaps -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - unsigned NumOperands = ci->getNumOperands(); - llvm::Value *Arg0 = NumOperands > 1 ? ci->getOperand(1) : 0; -#else - unsigned NumOperands = ci->getNumArgOperands() + 1; - llvm::Value *Arg0 = NumOperands > 1 ? ci->getArgOperand(0) : 0; -#endif - if (Arg0 && T == Arg0->getType() && - ((T == llvm::Type::getInt16Ty(getGlobalContext()) && - as == "rorw $$8, ${0:w}" && - cs == "=r,0,~{dirflag},~{fpsr},~{flags},~{cc}") || - (T == llvm::Type::getInt32Ty(getGlobalContext()) && - as == "rorw $$8, ${0:w};rorl $$16, $0;rorw $$8, ${0:w}" && - cs == "=r,0,~{dirflag},~{fpsr},~{flags},~{cc}"))) { - Function *F = getIntrinsic(M, Intrinsic::bswap, Arg0->getType()); -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8) - ci->setOperand(0, F); -#else - ci->setCalledFunction(F); -#endif - return true; - } -#endif } } @@ -88,7 +59,6 @@ bool RaiseAsmPass::runOnInstruction(Module &M, Instruction *I) { bool RaiseAsmPass::runOnModule(Module &M) { bool changed = false; -#if LLVM_VERSION_CODE >= LLVM_VERSION(2, 9) std::string Err; #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) std::string HostTriple = llvm::sys::getDefaultTargetTriple(); @@ -110,7 +80,6 @@ bool RaiseAsmPass::runOnModule(Module &M) { #endif TLI = TM->getTargetLowering(); } -#endif for (Module::iterator fi = M.begin(), fe = M.end(); fi != fe; ++fi) { for (Function::iterator bi = fi->begin(), be = fi->end(); bi != be; ++bi) { diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile index 11d3d330..2be74c01 100755 --- a/lib/Solver/Makefile +++ b/lib/Solver/Makefile @@ -14,3 +14,12 @@ DONT_BUILD_RELINKED=1 BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) + CXX.Flags += $(metaSMT_CXXFLAGS) + CXX.Flags += $(metaSMT_INCLUDES) +endif \ No newline at end of file diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h new file mode 100644 index 00000000..2b084ac7 --- /dev/null +++ b/lib/Solver/MetaSMTBuilder.h @@ -0,0 +1,1167 @@ + /* + * MetaSMTBuilder.h + * + * Created on: 8 Aug 2012 + * Author: hpalikar + */ + +#ifndef METASMTBUILDER_H_ +#define METASMTBUILDER_H_ + +#include "klee/Config/config.h" +#include "klee/Expr.h" +#include "klee/util/ExprPPrinter.h" +#include "klee/util/ArrayExprHash.h" +#include "klee/util/ExprHashMap.h" +#include "ConstantDivision.h" + +#ifdef SUPPORT_METASMT + +#include "llvm/Support/CommandLine.h" + +#include <metaSMT/frontend/Logic.hpp> +#include <metaSMT/frontend/QF_BV.hpp> +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/support/default_visitation_unrolling_limit.hpp> +#include <metaSMT/support/run_algorithm.hpp> + +#define Expr VCExpr +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef STP + +#include <boost/mpl/vector.hpp> +#include <boost/format.hpp> + +using namespace metaSMT; +using namespace metaSMT::logic::QF_BV; + + +#define DIRECT_CONTEXT + +namespace { + llvm::cl::opt<bool> + UseConstructHashMetaSMT("use-construct-hash-metasmt", + llvm::cl::desc("Use hash-consing during metaSMT query construction."), + llvm::cl::init(true)); +} + + +namespace klee { + +typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::true_tag>::type > const MetaSMTConstTrue; +typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::false_tag>::type > const MetaSMTConstFalse; +typedef metaSMT::logic::Array::array MetaSMTArray; + +template<typename SolverContext> +class MetaSMTBuilder; + +template<typename SolverContext> +class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > { + + friend class MetaSMTBuilder<SolverContext>; + +public: + MetaSMTArrayExprHash() {}; + virtual ~MetaSMTArrayExprHash() {}; +}; + +static const bool mimic_stp = true; + + +template<typename SolverContext> +class MetaSMTBuilder { +public: + + MetaSMTBuilder(SolverContext& solver, bool optimizeDivides) : _solver(solver), _optimizeDivides(optimizeDivides) { }; + virtual ~MetaSMTBuilder() {}; + + typename SolverContext::result_type construct(ref<Expr> e); + + typename SolverContext::result_type getInitialRead(const Array *root, unsigned index); + + typename SolverContext::result_type getTrue() { + return(evaluate(_solver, metaSMT::logic::True)); + } + + typename SolverContext::result_type getFalse() { + return(evaluate(_solver, metaSMT::logic::False)); + } + + typename SolverContext::result_type bvOne(unsigned width) { + return bvZExtConst(width, 1); + } + + typename SolverContext::result_type bvZero(unsigned width) { + return bvZExtConst(width, 0); + } + + typename SolverContext::result_type bvMinusOne(unsigned width) { + return bvSExtConst(width, (int64_t) -1); + } + + typename SolverContext::result_type bvConst32(unsigned width, uint32_t value) { + return(evaluate(_solver, bvuint(value, width))); + } + + typename SolverContext::result_type bvConst64(unsigned width, uint64_t value) { + return(evaluate(_solver, bvuint(value, width))); + } + + typename SolverContext::result_type bvZExtConst(unsigned width, uint64_t value); + typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value); + + //logical left and right shift (not arithmetic) + typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits); + typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits); + typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + + + typename SolverContext::result_type getArrayForUpdate(const Array *root, const UpdateNode *un); + typename SolverContext::result_type getInitialArray(const Array *root); + MetaSMTArray buildArray(unsigned elem_width, unsigned index_width); + +private: + typedef ExprHashMap< std::pair<typename SolverContext::result_type, unsigned> > MetaSMTExprHashMap; + typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter; + typedef typename MetaSMTExprHashMap::const_iterator MetaSMTExprHashMapConstIter; + + SolverContext& _solver; + bool _optimizeDivides; + MetaSMTArrayExprHash<SolverContext> _arr_hash; + MetaSMTExprHashMap _constructed; + + typename SolverContext::result_type constructActual(ref<Expr> e, int *width_out); + typename SolverContext::result_type construct(ref<Expr> e, int *width_out); + + typename SolverContext::result_type bvBoolExtract(typename SolverContext::result_type expr, int bit); + typename SolverContext::result_type bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom); + typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b); + + typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, + typename SolverContext::result_type isSigned, unsigned shiftBits); + typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x); + typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d); + typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d); + + unsigned getShiftBits(unsigned amount) { + unsigned bits = 1; + amount--; + while (amount >>= 1) { + bits++; + } + return(bits); + } +}; + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, const UpdateNode *un) { + + if (!un) { + return(getInitialArray(root)); + } + else { + typename SolverContext::result_type un_expr; + bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); + + if (!hashed) { + un_expr = evaluate(_solver, + metaSMT::logic::Array::store(getArrayForUpdate(root, un->next), + construct(un->index, 0), + construct(un->value, 0))); + _arr_hash.hashUpdateNodeExpr(un, un_expr); + } + return(un_expr); + } +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root) +{ + assert(root); + typename SolverContext::result_type array_expr; + bool hashed = _arr_hash.lookupArrayExpr(root, array_expr); + + if (!hashed) { + + array_expr = evaluate(_solver, buildArray(8, 32)); + + if (root->isConstantArray()) { + for (unsigned i = 0, e = root->size; i != e; ++i) { + typename SolverContext::result_type tmp = + evaluate(_solver, + metaSMT::logic::Array::store(array_expr, + construct(ConstantExpr::alloc(i, root->getDomain()), 0), + construct(root->constantValues[i], 0))); + array_expr = tmp; + } + } + _arr_hash.hashArrayExpr(root, array_expr); + } + + return(array_expr); +} + +template<typename SolverContext> +MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width, unsigned index_width) { + return(metaSMT::logic::Array::new_array(elem_width, index_width)); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root, unsigned index) { + assert(root); + assert(false); + typename SolverContext::result_type array_exp = getInitialArray(root); + typename SolverContext::result_type res = evaluate( + _solver, + metaSMT::logic::Array::select(array_exp, bvuint(index, root->getDomain()))); + return(res); +} + + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) { + + typename SolverContext::result_type res; + + if (width <= 64) { + res = bvConst64(width, value); + } + else { + typename SolverContext::result_type expr = bvConst64(64, value); + typename SolverContext::result_type zero = bvConst64(64, 0); + + for (width -= 64; width > 64; width -= 64) { + expr = evaluate(_solver, concat(zero, expr)); + } + res = evaluate(_solver, concat(bvConst64(width, 0), expr)); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) { + + typename SolverContext::result_type res; + + if (width <= 64) { + res = bvConst64(width, value); + } + else { + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments + res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value))); + } + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvBoolExtract(typename SolverContext::result_type expr, int bit) { + return(evaluate(_solver, + metaSMT::logic::equal(extract(bit, bit, expr), + bvOne(1)))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom) { + return(evaluate(_solver, extract(top, bottom, expr))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b) { + return(evaluate(_solver, metaSMT::logic::equal(a, b))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount, + typename SolverContext::result_type isSigned, unsigned shiftBits) { + unsigned shift = amount & ((1 << shiftBits) - 1); + typename SolverContext::result_type res; + + if (shift == 0) { + res = expr; + } + else if (shift >= width - 1) { + res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width))); + } + else { + res = evaluate(_solver, metaSMT::logic::Ite(isSigned, + concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)), + bvRightShift(expr, width, shift, shiftBits))); + } + + return(res); +} + +// width is the width of expr; x -- number of bits to shift with +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x) { + + unsigned shiftBits = getShiftBits(width); + uint64_t add, sub; + typename SolverContext::result_type res; + bool first = true; + + // expr*x == expr*(add-sub) == expr*add - expr*sub + ComputeMultConstants64(x, add, sub); + + // legal, these would overflow completely + add = bits64::truncateToNBits(add, width); + sub = bits64::truncateToNBits(sub, width); + + for (int j = 63; j >= 0; j--) { + uint64_t bit = 1LL << j; + + if ((add & bit) || (sub & bit)) { + assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + + typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits); + + if (add & bit) { + if (!first) { + res = evaluate(_solver, bvadd(res, op)); + } else { + res = op; + first = false; + } + } else { + if (!first) { + res = evaluate(_solver, bvsub(res, op)); + } else { + // To reconsider: vc_bvUMinusExpr in STP + res = evaluate(_solver, bvsub(bvZero(width), op)); + first = false; + } + } + } + } + + if (first) { + res = bvZero(width); + } + + return(res); +} + + +/* + * Compute the 32-bit unsigned integer division of n by a divisor d based on + * the constants derived from the constant divisor d. + * + * Returns n/d without doing explicit division. The cost is 2 adds, 3 shifts, + * and a (64-bit) multiply. + * + * @param expr_n numerator (dividend) n as an expression + * @param width number of bits used to represent the value + * @param d the divisor + * + * @return n/d without doing explicit division + */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) { + + assert(width == 32 && "can only compute udiv constants for 32-bit division"); + + // Compute the constants needed to compute n/d for constant d without division by d. + uint32_t mprime, sh1, sh2; + ComputeUDivConstants32(d, mprime, sh1, sh2); + typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1); + typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2); + + // t1 = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32 + typename SolverContext::result_type expr_n_64 = evaluate(_solver, concat(bvZero(32), expr_n)); //extend to 64 bits + typename SolverContext::result_type t1_64bits = constructMulByConstant(expr_n_64, 64, (uint64_t)mprime); + typename SolverContext::result_type t1 = bvExtract(t1_64bits, 63, 32); //upper 32 bits + + // n/d = (((n - t1) >> sh1) + t1) >> sh2; + typename SolverContext::result_type n_minus_t1 = evaluate(_solver, bvsub(expr_n, t1)); + typename SolverContext::result_type shift_sh1 = bvVarRightShift(n_minus_t1, expr_sh1, 32); + typename SolverContext::result_type plus_t1 = evaluate(_solver, bvadd(shift_sh1, t1)); + typename SolverContext::result_type res = bvVarRightShift(plus_t1, expr_sh2, 32); + + return(res); +} + +/* + * Compute the 32-bitnsigned integer division of n by a divisor d based on + * the constants derived from the constant divisor d. + * + * Returns n/d without doing explicit division. The cost is 3 adds, 3 shifts, + * a (64-bit) multiply, and an XOR. + * + * @param n numerator (dividend) as an expression + * @param width number of bits used to represent the value + * @param d the divisor + * + * @return n/d without doing explicit division + */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) { + + assert(width == 32 && "can only compute udiv constants for 32-bit division"); + + // Compute the constants needed to compute n/d for constant d w/o division by d. + int32_t mprime, dsign, shpost; + ComputeSDivConstants32(d, mprime, dsign, shpost); + typename SolverContext::result_type expr_dsign = bvConst32(32, dsign); + typename SolverContext::result_type expr_shpost = bvConst32(32, shpost); + + // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32) + int64_t mprime_64 = (int64_t)mprime; + + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments + typename SolverContext::result_type expr_n_64 = evaluate(_solver, sign_extend(64 - width, expr_n)); + typename SolverContext::result_type mult_64 = constructMulByConstant(expr_n_64, 64, mprime_64); + typename SolverContext::result_type mulsh = bvExtract(mult_64, 63, 32); //upper 32-bits + typename SolverContext::result_type n_plus_mulsh = evaluate(_solver, bvadd(expr_n, mulsh)); + + // Improved variable arithmetic right shift: sign extend, shift, extract. + typename SolverContext::result_type extend_npm = evaluate(_solver, sign_extend(64 - width, n_plus_mulsh)); + typename SolverContext::result_type shift_npm = bvVarRightShift(extend_npm, expr_shpost, 64); + typename SolverContext::result_type shift_shpost = bvExtract(shift_npm, 31, 0); //lower 32-bits + + ///////////// + + // XSIGN(n) is -1 if n is negative, positive one otherwise + typename SolverContext::result_type is_signed = bvBoolExtract(expr_n, 31); + typename SolverContext::result_type neg_one = bvMinusOne(32); + typename SolverContext::result_type xsign_of_n = evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32))); + + // q0 = (n_plus_mulsh >> shpost) - XSIGN(n) + typename SolverContext::result_type q0 = evaluate(_solver, bvsub(shift_shpost, xsign_of_n)); + + // n/d = (q0 ^ dsign) - dsign + typename SolverContext::result_type q0_xor_dsign = evaluate(_solver, bvxor(q0, expr_dsign)); + typename SolverContext::result_type res = evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign)); + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { + + typename SolverContext::result_type res; + unsigned shift = amount & ((1 << shiftBits) - 1); + + if (shift == 0) { + res = expr; + } + else if (shift >= width) { + res = bvZero(width); + } + else { + // stp shift does "expr @ [0 x s]" which we then have to extract, + // rolling our own gives slightly smaller exprs + res = evaluate(_solver, concat(extract(width - shift - 1, 0, expr), + bvZero(shift))); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { + + typename SolverContext::result_type res; + unsigned shift = amount & ((1 << shiftBits) - 1); + + if (shift == 0) { + res = expr; + } + else if (shift >= width) { + res = bvZero(width); + } + else { + res = evaluate(_solver, concat(bvZero(shift), + extract(width - 1, shift, expr))); + } + + return(res); +} + +// left shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + typename SolverContext::result_type res = bvZero(width); + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount)); + + //construct a big if-then-elif-elif-... with one case per possible shift amount + for(int i = width - 1; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + bvLeftShift(expr, width, i, shiftBits), + res)); + } + + return(res); +} + +// logical right shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + typename SolverContext::result_type res = bvZero(width); + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0); + + //construct a big if-then-elif-elif-... with one case per possible shift amount + for (int i = width - 1; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + bvRightShift(expr, width, i, shiftBits), + res)); + // ToDo Reconsider widht to provide to bvRightShift + } + + return(res); +} + +// arithmetic right shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0); + + //get the sign bit to fill with + typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1); + + //start with the result if shifting by width-1 + typename SolverContext::result_type res = constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits); + + // construct a big if-then-elif-elif-... with one case per possible shift amount + // XXX more efficient to move the ite on the sign outside all exprs? + // XXX more efficient to sign extend, right shift, then extract lower bits? + for (int i = width - 2; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)), + constructAShrByConstant(expr, width, i, signedBool, shiftBits), + res)); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) { + typename SolverContext::result_type res = construct(e, 0); + _constructed.clear(); + return res; +} + + +/** if *width_out!=1 then result is a bitvector, + otherwise it is a bool */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) { + + if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) { + return(constructActual(e, width_out)); + } else { + MetaSMTExprHashMapIter it = _constructed.find(e); + if (it != _constructed.end()) { + if (width_out) { + *width_out = it->second.second; + } + return it->second.first; + } else { + int width = 0; + if (!width_out) { + width_out = &width; + } + typename SolverContext::result_type res = constructActual(e, width_out); + _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out))); + return res; + } + } +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) { + + typename SolverContext::result_type res; + + int width = 0; + if (!width_out) { + // assert(false); + width_out = &width; + } + + ++stats::queryConstructs; + +// std::cerr << "Constructing expression "; +// ExprPPrinter::printSingleExpr(std::cerr, e); +// std::cerr << "\n"; + + switch (e->getKind()) { + + case Expr::Constant: + { + ConstantExpr *coe = cast<ConstantExpr>(e); + assert(coe); + unsigned coe_width = coe->getWidth(); + *width_out = coe_width; + + // Coerce to bool if necessary. + if (coe_width == 1) { + res = (coe->isTrue()) ? getTrue() : getFalse(); + } + else if (coe_width <= 32) { + res = bvConst32(coe_width, coe->getZExtValue(32)); + } + else if (coe_width <= 64) { + res = bvConst64(coe_width, coe->getZExtValue()); + } + else { + ref<ConstantExpr> tmp = coe; + res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); + while (tmp->getWidth() > 64) { + tmp = tmp->Extract(64, tmp->getWidth() - 64); + unsigned min_width = std::min(64U, tmp->getWidth()); + res = evaluate(_solver, + concat(bvConst64(min_width, tmp->Extract(0, min_width)->getZExtValue()), + res)); + } + } + break; + } + + case Expr::NotOptimized: + { + NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e); + assert(noe); + res = construct(noe->src, width_out); + break; + } + + case Expr::Select: + { + SelectExpr *se = cast<SelectExpr>(e); + assert(se); + res = evaluate(_solver, + metaSMT::logic::Ite(construct(se->cond, 0), + construct(se->trueExpr, width_out), + construct(se->falseExpr, width_out))); + break; + } + + case Expr::Read: + { + ReadExpr *re = cast<ReadExpr>(e); + assert(re); + // FixMe call method of Array + *width_out = 8; + res = evaluate(_solver, + metaSMT::logic::Array::select( + getArrayForUpdate(re->updates.root, re->updates.head), + construct(re->index, 0))); + break; + } + + case Expr::Concat: + { + ConcatExpr *ce = cast<ConcatExpr>(e); + assert(ce); + *width_out = ce->getWidth(); + unsigned numKids = ce->getNumKids(); + + if (numKids > 0) { + res = evaluate(_solver, construct(ce->getKid(numKids-1), 0)); + for (int i = numKids - 2; i >= 0; i--) { + res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res)); + } + } + break; + } + + case Expr::Extract: + { + ExtractExpr *ee = cast<ExtractExpr>(e); + assert(ee); + // ToDo spare evaluate? + typename SolverContext::result_type child = evaluate(_solver, construct(ee->expr, width_out)); + + unsigned ee_width = ee->getWidth(); + *width_out = ee_width; + + if (ee_width == 1) { + res = bvBoolExtract(child, ee->offset); + } + else { + res = evaluate(_solver, + extract(ee->offset + ee_width - 1, ee->offset, child)); + } + break; + } + + case Expr::ZExt: + { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); + + int child_width = 0; + typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; + + if (child_width == 1) { + res = evaluate(_solver, + metaSMT::logic::Ite(child, bvOne(ce_width), bvZero(ce_width))); + } + else { + res = evaluate(_solver, zero_extend(ce_width - child_width, child)); + } + + // ToDo calculate how many zeros to add + // Note: STP and metaSMT differ in the prototype arguments; + // STP requires the width of the resulting bv; + // whereas metaSMT (and Z3) require the width of the zero vector that is to be appended + // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src))); + + break; + } + + case Expr::SExt: + { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); + + int child_width = 0; + typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; + + if (child_width == 1) { + res = evaluate(_solver, + metaSMT::logic::Ite(child, bvMinusOne(ce_width), bvZero(ce_width))); + } + else { + // ToDo ce_width - child_width? It is only ce_width in STPBuilder + res = evaluate(_solver, sign_extend(ce_width - child_width, child)); + } + + break; + } + + case Expr::Add: + { + AddExpr *ae = cast<AddExpr>(e); + assert(ae); + res = evaluate(_solver, bvadd(construct(ae->left, width_out), construct(ae->right, width_out))); + assert(*width_out != 1 && "uncanonicalized add"); + break; + } + + case Expr::Sub: + { + SubExpr *se = cast<SubExpr>(e); + assert(se); + res = evaluate(_solver, bvsub(construct(se->left, width_out), construct(se->right, width_out))); + assert(*width_out != 1 && "uncanonicalized sub"); + break; + } + + case Expr::Mul: + { + MulExpr *me = cast<MulExpr>(e); + assert(me); + + typename SolverContext::result_type right_expr = evaluate(_solver, construct(me->right, width_out)); + assert(*width_out != 1 && "uncanonicalized mul"); + + ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left); + if (CE && (CE->getWidth() <= 64)) { + res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue()); + } + else { + res = evaluate(_solver, bvmul(construct(me->left, width_out), right_expr)); + } + break; + } + + case Expr::UDiv: + { + UDivExpr *de = cast<UDivExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized udiv"); + bool construct_both = true; + + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && (CE->getWidth() <= 64)) { + uint64_t divisor = CE->getZExtValue(); + if (bits64::isPowerOfTwo(divisor)) { + res = bvRightShift(left_expr, *width_out, bits64::indexOfSingleBit(divisor), getShiftBits(*width_out)); + construct_both = false; + } + else if (_optimizeDivides) { + if (*width_out == 32) { //only works for 32-bit division + res = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor); + construct_both = false; + } + } + } + + if (construct_both) { + res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::SDiv: + { + SDivExpr *de = cast<SDivExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized sdiv"); + + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && _optimizeDivides && (*width_out == 32)) { + res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32)); + } + else { + res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::URem: + { + URemExpr *de = cast<URemExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized urem"); + + bool construct_both = true; + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && (CE->getWidth() <= 64)) { + + uint64_t divisor = CE->getZExtValue(); + + if (bits64::isPowerOfTwo(divisor)) { + + unsigned bits = bits64::indexOfSingleBit(divisor); + // special case for modding by 1 or else we bvExtract -1:0 + if (bits == 0) { + res = bvZero(*width_out); + construct_both = false; + } + else { + res = evaluate(_solver, concat(bvZero(*width_out - bits), + bvExtract(left_expr, bits - 1, 0))); + construct_both = false; + } + } + + // Use fast division to compute modulo without explicit division for constant divisor. + + if (_optimizeDivides && *width_out == 32) { //only works for 32-bit division + typename SolverContext::result_type quotient = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor); + typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor); + res = evaluate(_solver, bvsub(left_expr, quot_times_divisor)); + construct_both = false; + } + } + + if (construct_both) { + res = evaluate(_solver, bvurem(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::SRem: + { + SRemExpr *de = cast<SRemExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(de->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(de->right, width_out)); + assert(*width_out != 1 && "uncanonicalized srem"); + + bool construct_both = true; + +#if 0 //not faster per first benchmark + + if (_optimizeDivides) { + if (ConstantExpr *cre = de->right->asConstant()) { + uint64_t divisor = cre->asUInt64; + + //use fast division to compute modulo without explicit division for constant divisor + if( *width_out == 32 ) { //only works for 32-bit division + typename SolverContext::result_type quotient = constructSDivByConstant(left, *width_out, divisor); + typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor); + res = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor ); + construct_both = false; + } + } + } + +#endif + + if (construct_both) { + res = evaluate(_solver, bvsrem(left_expr, right_expr)); + } + break; + } + + case Expr::Not: + { + NotExpr *ne = cast<NotExpr>(e); + assert(ne); + + typename SolverContext::result_type child = evaluate(_solver, construct(ne->expr, width_out)); + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Not(child)); + } + else { + res = evaluate(_solver, bvnot(child)); + } + break; + } + + case Expr::And: + { + AndExpr *ae = cast<AndExpr>(e); + assert(ae); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ae->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ae->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvand(left_expr, right_expr)); + } + + break; + } + + case Expr::Or: + { + OrExpr *oe = cast<OrExpr>(e); + assert(oe); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(oe->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(oe->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvor(left_expr, right_expr)); + } + + break; + } + + case Expr::Xor: + { + XorExpr *xe = cast<XorExpr>(e); + assert(xe); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(xe->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(xe->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvxor(left_expr, right_expr)); + } + + break; + } + + case Expr::Shl: + { + ShlExpr *se = cast<ShlExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + assert(*width_out != 1 && "uncanonicalized shl"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) { + res = bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, &shiftWidth)); + res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvshl(left_expr, right_expr)); + } + + break; + } + + case Expr::LShr: + { + LShrExpr *lse = cast<LShrExpr>(e); + assert(lse); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(lse->left, width_out)); + assert(*width_out != 1 && "uncanonicalized lshr"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) { + res = bvRightShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(lse->right, &shiftWidth)); + res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvshr(left_expr, right_expr)); + } + + break; + } + + case Expr::AShr: + { + AShrExpr *ase = cast<AShrExpr>(e); + assert(ase); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ase->left, width_out)); + assert(*width_out != 1 && "uncanonicalized ashr"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) { + unsigned shift = (unsigned) CE->getLimitedValue(); + typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1); + res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ase->right, &shiftWidth)); + res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvashr(left_expr, right_expr)); + } + + break; + } + + case Expr::Eq: + { + EqExpr *ee = cast<EqExpr>(e); + assert(ee); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ee->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ee->right, width_out)); + + if (*width_out==1) { + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) { + if (CE->isTrue()) { + res = right_expr; + } + else { + res = evaluate(_solver, metaSMT::logic::Not(right_expr)); + } + } + else { + res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr)); + } + } // end of *width_out == 1 + else { + *width_out = 1; + res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr)); + } + + break; + } + + case Expr::Ult: + { + UltExpr *ue = cast<UltExpr>(e); + assert(ue); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized ult"); + *width_out = 1; + + res = evaluate(_solver, bvult(left_expr, right_expr)); + break; + } + + case Expr::Ule: + { + UleExpr *ue = cast<UleExpr>(e); + assert(ue); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized ule"); + *width_out = 1; + + res = evaluate(_solver, bvule(left_expr, right_expr)); + break; + } + + case Expr::Slt: + { + SltExpr *se = cast<SltExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized slt"); + *width_out = 1; + + res = evaluate(_solver, bvslt(left_expr, right_expr)); + break; + } + + case Expr::Sle: + { + SleExpr *se = cast<SleExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized sle"); + *width_out = 1; + + res = evaluate(_solver, bvsle(left_expr, right_expr)); + break; + } + + // unused due to canonicalization +#if 0 + case Expr::Ne: + case Expr::Ugt: + case Expr::Uge: + case Expr::Sgt: + case Expr::Sge: +#endif + + default: + assert(false); + break; + + }; + return res; +} + + +} /* end of namespace klee */ + +#endif /* SUPPORT_METASMT */ + +#endif /* METASMTBUILDER_H_ */ diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index e7187fc3..f2e38182 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -74,6 +74,7 @@ void QueryLoggingSolver::flushBuffer() { // we do additional check here to log only timeouts in case // user specified negative value for minQueryTimeToLog param os << logBuffer.str(); + os.flush(); } } diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 3414cda2..22b1545f 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -12,6 +12,7 @@ #include "SolverStats.h" #include "STPBuilder.h" +#include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Expr.h" @@ -20,6 +21,7 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/Internal/Support/Timer.h" +#include "klee/CommandLine.h" #define vc_bvBoolExtract IAMTHESPAWNOFSATAN @@ -45,6 +47,24 @@ IgnoreSolverFailures("ignore-solver-failures", using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + /***/ SolverImpl::~SolverImpl() { @@ -809,3 +829,426 @@ STPSolverImpl::computeInitialValues(const Query &query, SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { return runStatusCode; } + +#ifdef SUPPORT_METASMT + +// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------ + +template<typename SolverContext> +class MetaSMTSolverImpl : public SolverImpl { +private: + + SolverContext _meta_solver; + MetaSMTSolver<SolverContext> *_solver; + MetaSMTBuilder<SolverContext> *_builder; + double _timeout; + bool _useForked; + SolverRunStatus _runStatusCode; + +public: + MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolverImpl(); + + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout) { _timeout = timeout; } + + bool computeTruth(const Query&, bool &isValid); + bool computeValue(const Query&, ref<Expr> &result); + + bool computeInitialValues(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution, + double timeout); + + SolverRunStatus getOperationStatusCode(); + + SolverContext& get_meta_solver() { return(_meta_solver); }; + +}; + + +// ------------------------------------- MetaSMTSolver methods -------------------------------------------- + + +template<typename SolverContext> +MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) + : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides)) +{ + +} + +template<typename SolverContext> +MetaSMTSolver<SolverContext>::~MetaSMTSolver() +{ + +} + +template<typename SolverContext> +char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) { + return(impl->getConstraintLog(query)); +} + +template<typename SolverContext> +void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); +} + + +// ------------------------------------- MetaSMTSolverImpl methods ---------------------------------------- + + + +template<typename SolverContext> +MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides) + : _solver(solver), + _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)), + _timeout(0.0), + _useForked(useForked) +{ + assert(_solver && "unable to create MetaSMTSolver"); + assert(_builder && "unable to create MetaSMTBuilder"); + + if (_useForked) { + shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700); + assert(shared_memory_id >= 0 && "shmget failed"); + shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0); + assert(shared_memory_ptr != (void*) -1 && "shmat failed"); + shmctl(shared_memory_id, IPC_RMID, NULL); + } +} + +template<typename SolverContext> +MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() { + +} + +template<typename SolverContext> +char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) { + const char* msg = "Not supported"; + char *buf = new char[strlen(msg) + 1]; + strcpy(buf, msg); + return(buf); +} + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) { + + bool success = false; + std::vector<const Array*> objects; + std::vector< std::vector<unsigned char> > values; + bool hasSolution; + + if (computeInitialValues(query, objects, values, hasSolution)) { + // query.expr is valid iff !query.expr is not satisfiable + isValid = !hasSolution; + success = true; + } + + return(success); +} + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) { + + bool success = false; + std::vector<const Array*> objects; + std::vector< std::vector<unsigned char> > values; + bool hasSolution; + + // Find the object used in the expression, and compute an assignment for them. + findSymbolicObjects(query.expr, objects); + if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) { + assert(hasSolution && "state has invalid constraint set"); + // Evaluate the expression with the computed assignment. + Assignment a(objects, values); + result = a.evaluate(query.expr); + success = true; + } + + return(success); +} + + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) { + + _runStatusCode = SOLVER_RUN_STATUS_FAILURE; + + TimerStatIncrementer t(stats::queryTime); + assert(_builder); + + /* + * FIXME push() and pop() work for Z3 but not for Boolector. + * If using Z3, use push() and pop() and assert constraints. + * If using Boolector, assume constrainsts instead of asserting them. + */ + //push(_meta_solver); + + if (!_useForked) { + for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { + //assertion(_meta_solver, _builder->construct(*it)); + assumption(_meta_solver, _builder->construct(*it)); + } + } + + ++stats::queries; + ++stats::queryCounterexamples; + + bool success = true; + if (_useForked) { + _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout); + success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode)); + } + else { + _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution); + success = true; + } + + if (success) { + if (hasSolution) { + ++stats::queriesInvalid; + } + else { + ++stats::queriesValid; + } + } + + //pop(_meta_solver); + + return(success); +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) +{ + + // assume the negation of the query + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr))); + hasSolution = solve(_meta_solver); + + if (hasSolution) { + values.reserve(objects.size()); + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + std::vector<unsigned char> data; + data.reserve(array->size); + + for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp); + data.push_back(elem_value); + } + + values.push_back(data); + } + } + + if (true == hasSolution) { + return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE); + } + else { + return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE); + } +} + +static void metaSMTTimeoutHandler(int x) { + _exit(52); +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution, + double timeout) +{ + unsigned char *pos = shared_memory_ptr; + unsigned sum = 0; + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + sum += (*it)->size; + } + // sum += sizeof(uint64_t); + sum += sizeof(stats::queryConstructs); + assert(sum < shared_memory_size && "not enough shared memory for counterexample"); + + fflush(stdout); + fflush(stderr); + int pid = fork(); + if (pid == -1) { + fprintf(stderr, "error: fork failed (for metaSMT)"); + return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED); + } + + if (pid == 0) { + if (timeout) { + ::alarm(0); /* Turn off alarm so we can safely set signal handler */ + ::signal(SIGALRM, metaSMTTimeoutHandler); + ::alarm(std::max(1, (int) timeout)); + } + + for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { + assertion(_meta_solver, _builder->construct(*it)); + //assumption(_meta_solver, _builder->construct(*it)); + } + + + std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs; + if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) { + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + std::vector<typename SolverContext::result_type> aux_arr; + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + aux_arr.push_back(elem_exp); + } + aux_arr_exprs.push_back(aux_arr); + } + assert(aux_arr_exprs.size() == objects.size()); + } + + + // assume the negation of the query + // can be also asserted instead of assumed as we are in a child process + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr))); + unsigned res = solve(_meta_solver); + + if (res) { + + if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) { + + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp); + *pos++ = elem_value; + } + } + } + else { + typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end(); + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) { + const Array *array = *it; + const std::vector<typename SolverContext::result_type>& arr_exp = *eit; + assert(array); + assert(array->size == arr_exp.size()); + + for (unsigned offset = 0; offset < array->size; offset++) { + unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]); + *pos++ = elem_value; + } + } + } + } + assert((uint64_t*) pos); + *((uint64_t*) pos) = stats::queryConstructs; + + _exit(!res); + } + else { + int status; + pid_t res; + + do { + res = waitpid(pid, &status, 0); + } + while (res < 0 && errno == EINTR); + + if (res < 0) { + fprintf(stderr, "error: waitpid() for metaSMT failed"); + return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED); + } + + // From timed_run.py: It appears that linux at least will on + // "occasion" return a status when the process was terminated by a + // signal, so test signal first. + if (WIFSIGNALED(status) || !WIFEXITED(status)) { + fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status)); + return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED); + } + + int exitcode = WEXITSTATUS(status); + if (exitcode == 0) { + hasSolution = true; + } + else if (exitcode == 1) { + hasSolution = false; + } + else if (exitcode == 52) { + fprintf(stderr, "error: metaSMT timed out"); + return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT); + } + else { + fprintf(stderr, "error: metaSMT did not return a recognized code"); + return(SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE); + } + + if (hasSolution) { + values = std::vector< std::vector<unsigned char> >(objects.size()); + unsigned i = 0; + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + const Array *array = *it; + assert(array); + std::vector<unsigned char> &data = values[i++]; + data.insert(data.begin(), pos, pos + array->size); + pos += array->size; + } + } + stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs); + + if (true == hasSolution) { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + else { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + } + } +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() { + return _runStatusCode; +} + +template class MetaSMTSolver< DirectSolver_Context < Boolector> >; +template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >; +template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >; + +#endif /* SUPPORT_METASMT */ + diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp index fb0e349c..909e07da 100644 --- a/lib/Support/Time.cpp +++ b/lib/Support/Time.cpp @@ -10,11 +10,7 @@ #include "klee/Config/Version.h" #include "klee/Internal/System/Time.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif using namespace llvm; using namespace klee; diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp index 35922d4d..c61a90a3 100644 --- a/lib/Support/Timer.cpp +++ b/lib/Support/Timer.cpp @@ -10,11 +10,7 @@ #include "klee/Config/Version.h" #include "klee/Internal/Support/Timer.h" -#if LLVM_VERSION_CODE < LLVM_VERSION(2, 9) -#include "llvm/System/Process.h" -#else #include "llvm/Support/Process.h" -#endif using namespace klee; using namespace llvm; |