diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 249 |
1 files changed, 183 insertions, 66 deletions
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 |