diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 199 |
1 files changed, 169 insertions, 30 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 069022a2..b2cff8ba 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -47,6 +47,19 @@ #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/System/Time.h" +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) +#include "llvm/IR/Function.h" +#include "llvm/IR/Attributes.h" +#include "llvm/IR/BasicBlock.h" +#include "llvm/IR/Constants.h" +#include "llvm/IR/Function.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/LLVMContext.h" +#include "llvm/IR/Module.h" +#include "llvm/IR/DataLayout.h" +#include "llvm/IR/TypeBuilder.h" +#else #include "llvm/Attributes.h" #include "llvm/BasicBlock.h" #include "llvm/Constants.h" @@ -57,6 +70,13 @@ #include "llvm/LLVMContext.h" #endif #include "llvm/Module.h" +#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) +#include "llvm/Target/TargetData.h" +#else +#include "llvm/DataLayout.h" +#include "llvm/TypeBuilder.h" +#endif +#endif #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CallSite.h" @@ -67,11 +87,6 @@ #else #include "llvm/Support/Process.h" #endif -#if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) -#include "llvm/Target/TargetData.h" -#else -#include "llvm/DataLayout.h" -#endif #include <cassert> #include <algorithm> @@ -90,6 +105,33 @@ using namespace llvm; using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + namespace { cl::opt<bool> DumpStatesOnHalt("dump-states-on-halt", @@ -253,7 +295,41 @@ Executor::Executor(const InterpreterOptions &opts, : std::max(MaxCoreSolverTime,MaxInstructionTime)) { if (coreSolverTimeout) UseForkedCoreSolver = true; - Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + + Solver *coreSolver = NULL; + +#ifdef SUPPORT_METASMT + if (UseMetaSMT != METASMT_BACKEND_NONE) { + + std::string backend; + + switch (UseMetaSMT) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + assert(false); + break; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + } +#else + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#endif /* SUPPORT_METASMT */ + + Solver *solver = constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), @@ -386,10 +462,10 @@ void Executor::initializeGlobals(ExecutionState &state) { if (m->getModuleInlineAsm() != "") klee_warning("executable has module level assembly (ignoring)"); - +#if LLVM_VERSION_CODE < LLVM_VERSION(3, 3) assert(m->lib_begin() == m->lib_end() && "XXX do not support dependent libraries"); - +#endif // represent function globals using the address of the actual llvm function // object. given that we use malloc to allocate memory in states this also // ensures that we won't conflict. we don't need to allocate a memory object @@ -557,20 +633,31 @@ void Executor::branch(ExecutionState &state, unsigned N = conditions.size(); assert(N); - stats::forks += N-1; + if (MaxForks!=~0u && stats::forks >= MaxForks) { + unsigned next = theRNG.getInt32() % N; + for (unsigned i=0; i<N; ++i) { + if (i == next) { + result.push_back(&state); + } else { + result.push_back(NULL); + } + } + } else { + stats::forks += N-1; - // XXX do proper balance or keep random? - result.push_back(&state); - for (unsigned i=1; i<N; ++i) { - ExecutionState *es = result[theRNG.getInt32() % i]; - ExecutionState *ns = es->branch(); - addedStates.insert(ns); - result.push_back(ns); - es->ptreeNode->data = 0; - std::pair<PTree::Node*,PTree::Node*> res = - processTree->split(es->ptreeNode, ns, es); - ns->ptreeNode = res.first; - es->ptreeNode = res.second; + // XXX do proper balance or keep random? + result.push_back(&state); + for (unsigned i=1; i<N; ++i) { + ExecutionState *es = result[theRNG.getInt32() % i]; + ExecutionState *ns = es->branch(); + addedStates.insert(ns); + result.push_back(ns); + es->ptreeNode->data = 0; + std::pair<PTree::Node*,PTree::Node*> res = + processTree->split(es->ptreeNode, ns, es); + ns->ptreeNode = res.first; + es->ptreeNode = res.second; + } } // If necessary redistribute seeds to match conditions, killing @@ -605,12 +692,14 @@ void Executor::branch(ExecutionState &state, if (i==N) i = theRNG.getInt32() % N; - seedMap[result[i]].push_back(*siit); + // Extra check in case we're replaying seeds with a max-fork + if (result[i]) + seedMap[result[i]].push_back(*siit); } if (OnlyReplaySeeds) { for (unsigned i=0; i<N; ++i) { - if (!seedMap.count(result[i])) { + if (result[i] && !seedMap.count(result[i])) { terminateState(*result[i]); result[i] = NULL; } @@ -1380,7 +1469,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { CallSite(cast<CallInst>(caller))); // XXX need to check other param attrs ? -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) bool isSExt = cs.paramHasAttr(0, llvm::Attributes::SExt); #else bool isSExt = cs.paramHasAttr(0, llvm::Attribute::SExt); @@ -1584,7 +1675,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (from != to) { // XXX need to check other param attrs ? -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt); +#elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2) bool isSExt = cs.paramHasAttr(i+1, llvm::Attributes::SExt); #else bool isSExt = cs.paramHasAttr(i+1, llvm::Attribute::SExt); @@ -1982,8 +2075,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FAdd operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.add(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.add(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -1996,9 +2094,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(left->getWidth()) || !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FSub operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.subtract(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.subtract(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2012,8 +2114,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FMul operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.multiply(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.multiply(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2027,8 +2134,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FDiv operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.divide(APFloat(*fpWidthToSemantics(right->getWidth()), right->getAPValue()), APFloat::rmNearestTiesToEven); +#else llvm::APFloat Res(left->getAPValue()); Res.divide(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2041,9 +2153,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(left->getWidth()) || !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FRem operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(left->getWidth()), left->getAPValue()); + Res.remainder(APFloat(*fpWidthToSemantics(right->getWidth()),right->getAPValue())); +#else llvm::APFloat Res(left->getAPValue()); Res.mod(APFloat(right->getAPValue()), APFloat::rmNearestTiesToEven); +#endif bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt())); break; } @@ -2056,7 +2172,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(arg->getWidth()) || resultType > arg->getWidth()) return terminateStateOnExecError(state, "Unsupported FPTrunc operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Res(arg->getAPValue()); +#endif bool losesInfo = false; Res.convert(*fpWidthToSemantics(resultType), llvm::APFloat::rmNearestTiesToEven, @@ -2072,8 +2192,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); if (!fpWidthToSemantics(arg->getWidth()) || arg->getWidth() > resultType) return terminateStateOnExecError(state, "Unsupported FPExt operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Res(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Res(arg->getAPValue()); +#endif bool losesInfo = false; Res.convert(*fpWidthToSemantics(resultType), llvm::APFloat::rmNearestTiesToEven, @@ -2090,7 +2213,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToUI operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Arg(arg->getAPValue()); +#endif uint64_t value = 0; bool isExact = true; Arg.convertToInteger(&value, resultType, false, @@ -2106,8 +2233,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "floating point"); if (!fpWidthToSemantics(arg->getWidth()) || resultType > 64) return terminateStateOnExecError(state, "Unsupported FPToSI operation"); - +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + llvm::APFloat Arg(*fpWidthToSemantics(arg->getWidth()), arg->getAPValue()); +#else llvm::APFloat Arg(arg->getAPValue()); + +#endif uint64_t value = 0; bool isExact = true; Arg.convertToInteger(&value, resultType, true, @@ -2158,8 +2289,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { !fpWidthToSemantics(right->getWidth())) return terminateStateOnExecError(state, "Unsupported FCmp operation"); +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + APFloat LHS(*fpWidthToSemantics(left->getWidth()),left->getAPValue()); + APFloat RHS(*fpWidthToSemantics(right->getWidth()),right->getAPValue()); +#else APFloat LHS(left->getAPValue()); APFloat RHS(right->getAPValue()); +#endif APFloat::cmpResult CmpRes = LHS.compare(RHS); bool Result = false; @@ -2470,8 +2606,11 @@ void Executor::run(ExecutionState &initialState) { // We need to avoid calling GetMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) + unsigned mbs = sys::Process::GetMallocUsage() >> 20; +#else unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20; - +#endif if (mbs > MaxMemory) { if (mbs > MaxMemory + 100) { // just guess at how many to kill |