diff options
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/AddressSpace.cpp | 2 | ||||
| -rw-r--r-- | lib/Core/ExecutionState.cpp | 4 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 413 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 34 | ||||
| -rw-r--r-- | lib/Core/ExecutorTimers.cpp | 6 | ||||
| -rw-r--r-- | lib/Core/MemoryManager.cpp | 143 | ||||
| -rw-r--r-- | lib/Core/MemoryManager.h | 57 | ||||
| -rw-r--r-- | lib/Core/Searcher.cpp | 124 | ||||
| -rw-r--r-- | lib/Core/Searcher.h | 56 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 44 | ||||
| -rw-r--r-- | lib/Core/StatsTracker.cpp | 76 |
11 files changed, 645 insertions, 314 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 25418c13..811e52c3 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -58,6 +58,8 @@ bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr, if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) { const MemoryObject *mo = res->first; + // Check if the provided address is between start and end of the object + // [mo->address, mo->address + mo->size) or the object is a 0-sized object. if ((mo->size==0 && address==mo->address) || (address - mo->address < mo->size)) { result = *res; diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 6aeaa833..30d20266 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -370,8 +370,8 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const { out << ai->getName().str(); // XXX should go through function - ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; - if (isa<ConstantExpr>(value)) + ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; + if (value.get() && isa<ConstantExpr>(value)) out << "=" << value; } out << ")"; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ff346487..d755403f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -89,6 +89,10 @@ #include "llvm/IR/CallSite.h" #endif +#ifdef HAVE_ZLIB_H +#include "klee/Internal/Support/CompressionStream.h" +#endif + #include <cassert> #include <algorithm> #include <iomanip> @@ -158,6 +162,11 @@ namespace { "[inst_id]"), clEnumValEnd), llvm::cl::CommaSeparated); +#ifdef HAVE_ZLIB_H + cl::opt<bool> DebugCompressInstructions( + "debug-compress-instructions", cl::init(false), + cl::desc("Compress the logged instructions in gzip format.")); +#endif cl::opt<bool> DebugCheckForImpliedValues("debug-check-for-implied-values"); @@ -267,6 +276,25 @@ namespace { cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"), cl::init(0)); + cl::list<Executor::TerminateReason> + ExitOnErrorType("exit-on-error-type", + cl::desc("Stop execution after reaching a specified condition. (default=off)"), + cl::values( + clEnumValN(Executor::Abort, "Abort", "The program crashed"), + clEnumValN(Executor::Assert, "Assert", "An assertion was hit"), + clEnumValN(Executor::Exec, "Exec", "Trying to execute an unexpected instruction"), + clEnumValN(Executor::External, "External", "External objects referenced"), + clEnumValN(Executor::Free, "Free", "Freeing invalid memory"), + clEnumValN(Executor::Model, "Model", "Memory model limit hit"), + clEnumValN(Executor::Overflow, "Overflow", "An overflow occurred"), + clEnumValN(Executor::Ptr, "Ptr", "Pointer error"), + clEnumValN(Executor::ReadOnly, "ReadOnly", "Write to read-only memory"), + clEnumValN(Executor::ReportError, "ReportError", "klee_report_error called"), + clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"), + clEnumValN(Executor::Unhandled, "Unhandled", "Unhandled instruction hit"), + clEnumValEnd), + cl::ZeroOrMore); + cl::opt<unsigned int> StopAfterNInstructions("stop-after-n-instructions", cl::desc("Stop execution after specified number of instructions (default=0 (off))"), @@ -298,6 +326,21 @@ namespace klee { RNG theRNG; } +const char *Executor::TerminateReasonNames[] = { + [ Abort ] = "abort", + [ Assert ] = "assert", + [ Exec ] = "exec", + [ External ] = "external", + [ Free ] = "free", + [ Model ] = "model", + [ Overflow ] = "overflow", + [ Ptr ] = "ptr", + [ ReadOnly ] = "readonly", + [ ReportError ] = "reporterror", + [ User ] = "user", + [ Unhandled ] = "xxx", +}; + Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), kmodule(0), interpreterHandler(ih), searcher(0), externalDispatcher(new ExternalDispatcher()), statsTracker(0), @@ -332,6 +375,10 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) std::string debug_file_name = interpreterHandler->getOutputFilename("instructions.txt"); std::string ErrorInfo; +#ifdef HAVE_ZLIB_H + if (!DebugCompressInstructions) { +#endif + #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), @@ -339,6 +386,16 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) debugInstFile = new llvm::raw_fd_ostream(debug_file_name.c_str(), ErrorInfo); #endif +#ifdef HAVE_ZLIB_H + } else { + debugInstFile = new compressed_fd_ostream( + (debug_file_name + ".gz").c_str(), ErrorInfo); + } +#endif + if (ErrorInfo != "") { + klee_error("Could not open file %s : %s", debug_file_name.c_str(), + ErrorInfo.c_str()); + } } } @@ -364,7 +421,7 @@ const Module *Executor::setModule(llvm::Module *module, kmodule->prepare(opts, interpreterHandler); specialFunctionHandler->bind(); - if (StatsTracker::useStatistics()) { + if (StatsTracker::useStatistics() || userSearcherRequiresMD2U()) { statsTracker = new StatsTracker(*this, interpreterHandler->getOutputFilename("assembly.ll"), @@ -539,7 +596,13 @@ void Executor::initializeGlobals(ExecutionState &state) { // hack where we check the object file information. LLVM_TYPE_Q Type *ty = i->getType()->getElementType(); - uint64_t size = kmodule->targetData->getTypeStoreSize(ty); + uint64_t size = 0; + if (ty->isSized()) { + size = kmodule->targetData->getTypeStoreSize(ty); + } else { + klee_warning("Type for %.*s is not sized", (int)i->getName().size(), + i->getName().data()); + } // XXX - DWD - hardcode some things until we decide how to fix. #ifndef WINDOWS @@ -553,9 +616,8 @@ void Executor::initializeGlobals(ExecutionState &state) { #endif if (size == 0) { - llvm::errs() << "Unable to find size for global variable: " - << i->getName() - << " (use will result in out of bounds access)\n"; + klee_warning("Unable to find size for global variable: %.*s (use will result in out of bounds access)", + (int)i->getName().size(), i->getName().data()); } MemoryObject *mo = memory->allocate(size, false, true, i); @@ -642,7 +704,7 @@ void Executor::branch(ExecutionState &state, for (unsigned i=1; i<N; ++i) { ExecutionState *es = result[theRNG.getInt32() % i]; ExecutionState *ns = es->branch(); - addedStates.insert(ns); + addedStates.push_back(ns); result.push_back(ns); es->ptreeNode->data = 0; std::pair<PTree::Node*,PTree::Node*> res = @@ -860,7 +922,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { ++stats::forks; falseState = trueState->branch(); - addedStates.insert(falseState); + addedStates.push_back(falseState); if (RandomizeFork && theRNG.getBool()) std::swap(trueState, falseState); @@ -1212,8 +1274,10 @@ void Executor::executeCall(ExecutionState &state, // ExecutionState::varargs case Intrinsic::vastart: { StackFrame &sf = state.stack.back(); - assert(sf.varargs && - "vastart called in function with no vararg object"); + + // varargs can be zero if no varargs were provided + if (!sf.varargs) + return; // FIXME: This is really specific to the architecture, not the pointer // size. This happens to work fir x86-32 and x86-64, however. @@ -1270,13 +1334,13 @@ void Executor::executeCall(ExecutionState &state, KFunction *kf = kmodule->functionMap[f]; state.pushFrame(state.prevPC, kf); state.pc = kf->instructions; - + if (statsTracker) statsTracker->framePushed(state, &state.stack[state.stack.size()-2]); - + // TODO: support "byval" parameter attribute // TODO: support zeroext, signext, sret attributes - + unsigned callingArgs = arguments.size(); unsigned funcArgs = f->arg_size(); if (!f->isVarArg()) { @@ -1284,68 +1348,76 @@ void Executor::executeCall(ExecutionState &state, klee_warning_once(f, "calling %s with extra arguments.", f->getName().data()); } else if (callingArgs < funcArgs) { - terminateStateOnError(state, "calling function with too few arguments", - "user.err"); + terminateStateOnError(state, "calling function with too few arguments", + User); return; } } else { Expr::Width WordSize = Context::get().getPointerWidth(); if (callingArgs < funcArgs) { - terminateStateOnError(state, "calling function with too few arguments", - "user.err"); + terminateStateOnError(state, "calling function with too few arguments", + User); return; } - + StackFrame &sf = state.stack.back(); unsigned size = 0; + bool requires16ByteAlignment = false; for (unsigned i = funcArgs; i < callingArgs; i++) { // FIXME: This is really specific to the architecture, not the pointer - // size. This happens to work fir x86-32 and x86-64, however. + // size. This happens to work for x86-32 and x86-64, however. if (WordSize == Expr::Int32) { size += Expr::getMinBytesForWidth(arguments[i]->getWidth()); } else { Expr::Width argWidth = arguments[i]->getWidth(); - // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a 16 - // byte boundary if alignment needed by type exceeds 8 byte boundary. + // AMD64-ABI 3.5.7p5: Step 7. Align l->overflow_arg_area upwards to a + // 16 byte boundary if alignment needed by type exceeds 8 byte + // boundary. // // Alignment requirements for scalar types is the same as their size if (argWidth > Expr::Int64) { size = llvm::RoundUpToAlignment(size, 16); + requires16ByteAlignment = true; } size += llvm::RoundUpToAlignment(argWidth, WordSize) / 8; } } - MemoryObject *mo = sf.varargs = memory->allocate(size, true, false, - state.prevPC->inst); - if (!mo) { + MemoryObject *mo = sf.varargs = + memory->allocate(size, true, false, state.prevPC->inst, + (requires16ByteAlignment ? 16 : 8)); + if (!mo && size) { terminateStateOnExecError(state, "out of memory (varargs)"); return; } - if ((WordSize == Expr::Int64) && (mo->address & 15)) { - // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes. - klee_warning_once(0, "While allocating varargs: malloc did not align to 16 bytes."); - } + if (mo) { + if ((WordSize == Expr::Int64) && (mo->address & 15) && + requires16ByteAlignment) { + // Both 64bit Linux/Glibc and 64bit MacOSX should align to 16 bytes. + klee_warning_once( + 0, "While allocating varargs: malloc did not align to 16 bytes."); + } - ObjectState *os = bindObjectInState(state, mo, true); - unsigned offset = 0; - for (unsigned i = funcArgs; i < callingArgs; i++) { - // FIXME: This is really specific to the architecture, not the pointer - // size. This happens to work fir x86-32 and x86-64, however. - if (WordSize == Expr::Int32) { - os->write(offset, arguments[i]); - offset += Expr::getMinBytesForWidth(arguments[i]->getWidth()); - } else { - assert(WordSize == Expr::Int64 && "Unknown word size!"); + ObjectState *os = bindObjectInState(state, mo, true); + unsigned offset = 0; + for (unsigned i = funcArgs; i < callingArgs; i++) { + // FIXME: This is really specific to the architecture, not the pointer + // size. This happens to work for x86-32 and x86-64, however. + if (WordSize == Expr::Int32) { + os->write(offset, arguments[i]); + offset += Expr::getMinBytesForWidth(arguments[i]->getWidth()); + } else { + assert(WordSize == Expr::Int64 && "Unknown word size!"); - Expr::Width argWidth = arguments[i]->getWidth(); - if (argWidth > Expr::Int64) { - offset = llvm::RoundUpToAlignment(offset, 16); + Expr::Width argWidth = arguments[i]->getWidth(); + if (argWidth > Expr::Int64) { + offset = llvm::RoundUpToAlignment(offset, 16); + } + os->write(offset, arguments[i]); + offset += llvm::RoundUpToAlignment(argWidth, WordSize) / 8; } - os->write(offset, arguments[i]); - offset += llvm::RoundUpToAlignment(argWidth, WordSize) / 8; } } } @@ -1586,58 +1658,108 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { #endif transferToBasicBlock(si->getSuccessor(index), si->getParent(), state); } else { - std::map<BasicBlock*, ref<Expr> > targets; - ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool); -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); - i != e; ++i) { + // Handle possible different branch targets + + // We have the following assumptions: + // - each case value is mutual exclusive to all other values including the + // default value + // - order of case branches is based on the order of the expressions of + // the scase values, still default is handled last + std::vector<BasicBlock *> bbOrder; + std::map<BasicBlock *, ref<Expr> > branchTargets; + + std::map<ref<Expr>, BasicBlock *> expressionOrder; + + // Iterate through all non-default cases and order them by expressions +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + for (SwitchInst::CaseIt i = si->case_begin(), e = si->case_end(); i != e; + ++i) { ref<Expr> value = evalConstant(i.getCaseValue()); #else - for (unsigned i=1, cases = si->getNumCases(); i<cases; ++i) { + for (unsigned i = 1, cases = si->getNumCases(); i < cases; ++i) { ref<Expr> value = evalConstant(si->getCaseValue(i)); #endif - ref<Expr> match = EqExpr::create(cond, value); - isDefault = AndExpr::create(isDefault, Expr::createIsZero(match)); + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) + BasicBlock *caseSuccessor = i.getCaseSuccessor(); +#else + BasicBlock *caseSuccessor = si->getSuccessor(i); +#endif + expressionOrder.insert(std::make_pair(value, caseSuccessor)); + } + + // Track default branch values + ref<Expr> defaultValue = ConstantExpr::alloc(1, Expr::Bool); + + // iterate through all non-default cases but in order of the expressions + for (std::map<ref<Expr>, BasicBlock *>::iterator + it = expressionOrder.begin(), + itE = expressionOrder.end(); + it != itE; ++it) { + ref<Expr> match = EqExpr::create(cond, it->first); + + // Make sure that the default value does not contain this target's value + defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match)); + + // Check if control flow could take this case bool result; bool success = solver->mayBeTrue(state, match, result); assert(success && "FIXME: Unhandled solver failure"); (void) success; if (result) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) - BasicBlock *caseSuccessor = i.getCaseSuccessor(); -#else - BasicBlock *caseSuccessor = si->getSuccessor(i); -#endif - std::map<BasicBlock*, ref<Expr> >::iterator it = - targets.insert(std::make_pair(caseSuccessor, - ConstantExpr::alloc(0, Expr::Bool))).first; - - it->second = OrExpr::create(match, it->second); + BasicBlock *caseSuccessor = it->second; + + // Handle the case that a basic block might be the target of multiple + // switch cases. + // Currently we generate an expression containing all switch-case + // values for the same target basic block. We spare us forking too + // many times but we generate more complex condition expressions + // TODO Add option to allow to choose between those behaviors + std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> res = + branchTargets.insert(std::make_pair( + caseSuccessor, ConstantExpr::alloc(0, Expr::Bool))); + + res.first->second = OrExpr::create(match, res.first->second); + + // Only add basic blocks which have not been target of a branch yet + if (res.second) { + bbOrder.push_back(caseSuccessor); + } } } + + // Check if control could take the default case bool res; - bool success = solver->mayBeTrue(state, isDefault, res); + bool success = solver->mayBeTrue(state, defaultValue, res); assert(success && "FIXME: Unhandled solver failure"); (void) success; - if (res) - targets.insert(std::make_pair(si->getDefaultDest(), isDefault)); - + if (res) { + std::pair<std::map<BasicBlock *, ref<Expr> >::iterator, bool> ret = + branchTargets.insert( + std::make_pair(si->getDefaultDest(), defaultValue)); + if (ret.second) { + bbOrder.push_back(si->getDefaultDest()); + } + } + + // Fork the current state with each state having one of the possible + // successors of this switch std::vector< ref<Expr> > conditions; - for (std::map<BasicBlock*, ref<Expr> >::iterator it = - targets.begin(), ie = targets.end(); - it != ie; ++it) - conditions.push_back(it->second); - + for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(), + ie = bbOrder.end(); + it != ie; ++it) { + conditions.push_back(branchTargets[*it]); + } std::vector<ExecutionState*> branches; branch(state, conditions, branches); - + std::vector<ExecutionState*>::iterator bit = branches.begin(); - for (std::map<BasicBlock*, ref<Expr> >::iterator it = - targets.begin(), ie = targets.end(); + for (std::vector<BasicBlock *>::iterator it = bbOrder.begin(), + ie = bbOrder.end(); it != ie; ++it) { ExecutionState *es = *bit; if (es) - transferToBasicBlock(it->first, bb, *es); + transferToBasicBlock(*it, bb, *es); ++bit; } } @@ -2428,7 +2550,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { case Instruction::InsertElement: case Instruction::ShuffleVector: terminateStateOnError(state, "XXX vector instructions unhandled", - "xxx.err"); + Unhandled); break; default: @@ -2444,9 +2566,9 @@ void Executor::updateStates(ExecutionState *current) { states.insert(addedStates.begin(), addedStates.end()); addedStates.clear(); - - for (std::set<ExecutionState*>::iterator - it = removedStates.begin(), ie = removedStates.end(); + + for (std::vector<ExecutionState *>::iterator it = removedStates.begin(), + ie = removedStates.end(); it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::iterator it2 = states.find(es); @@ -2531,7 +2653,9 @@ void Executor::checkMemoryUsage() { // We need to avoid calling GetTotalMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. - unsigned mbs = util::GetTotalMallocUsage() >> 20; + unsigned mbs = (util::GetTotalMallocUsage() >> 20) + + (memory->getUsedDeterministicSize() >> 20); + if (mbs > MaxMemory) { if (mbs > MaxMemory + 100) { // just guess at how many to kill @@ -2557,6 +2681,20 @@ void Executor::checkMemoryUsage() { } } +void Executor::doDumpStates() { + if (!DumpStatesOnHalt || states.empty()) + return; + klee_message("halting execution, dumping remaining states"); + for (std::set<ExecutionState *>::iterator it = states.begin(), + ie = states.end(); + it != ie; ++it) { + ExecutionState &state = **it; + stepInstruction(state); // keep stats rolling + terminateStateEarly(state, "Execution halting."); + } + updateStates(0); +} + void Executor::run(ExecutionState &initialState) { bindModuleConstants(); @@ -2577,7 +2715,10 @@ void Executor::run(ExecutionState &initialState) { double lastTime, startTime = lastTime = util::getWallTime(); ExecutionState *lastState = 0; while (!seedMap.empty()) { - if (haltExecution) goto dump; + if (haltExecution) { + doDumpStates(); + return; + } std::map<ExecutionState*, std::vector<SeedInfo> >::iterator it = seedMap.upper_bound(lastState); @@ -2626,13 +2767,16 @@ void Executor::run(ExecutionState &initialState) { (*it)->weight = 1.; } - if (OnlySeed) - goto dump; + if (OnlySeed) { + doDumpStates(); + return; + } } searcher = constructUserSearcher(*this); - searcher->update(0, states, std::set<ExecutionState*>()); + std::vector<ExecutionState *> newStates(states.begin(), states.end()); + searcher->update(0, newStates, std::vector<ExecutionState *>()); while (!states.empty() && !haltExecution) { ExecutionState &state = searcher->selectState(); @@ -2649,19 +2793,8 @@ void Executor::run(ExecutionState &initialState) { delete searcher; searcher = 0; - - dump: - if (DumpStatesOnHalt && !states.empty()) { - llvm::errs() << "KLEE: halting execution, dumping remaining states\n"; - for (std::set<ExecutionState*>::iterator - it = states.begin(), ie = states.end(); - it != ie; ++it) { - ExecutionState &state = **it; - stepInstruction(state); // keep stats rolling - terminateStateEarly(state, "Execution halting."); - } - updateStates(0); - } + + doDumpStates(); } std::string Executor::getAddressInfo(ExecutionState &state, @@ -2722,11 +2855,12 @@ void Executor::terminateState(ExecutionState &state) { interpreterHandler->incPathsExplored(); - std::set<ExecutionState*>::iterator it = addedStates.find(&state); + std::vector<ExecutionState *>::iterator it = + std::find(addedStates.begin(), addedStates.end(), &state); if (it==addedStates.end()) { state.pc = state.prevPC; - removedStates.insert(&state); + removedStates.push_back(&state); } else { // never reached searcher, just delete immediately std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it3 = @@ -2797,8 +2931,21 @@ const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const Execut } return *ii; } + +bool Executor::shouldExitOn(enum TerminateReason termReason) { + std::vector<TerminateReason>::iterator s = ExitOnErrorType.begin(); + std::vector<TerminateReason>::iterator e = ExitOnErrorType.end(); + + for (; s != e; ++s) + if (termReason == *s) + return true; + + return false; +} + void Executor::terminateStateOnError(ExecutionState &state, const llvm::Twine &messaget, + enum TerminateReason termReason, const char *suffix, const llvm::Twine &info) { std::string message = messaget.str(); @@ -2831,10 +2978,20 @@ void Executor::terminateStateOnError(ExecutionState &state, if (info_str != "") msg << "Info: \n" << info_str; + std::string suffix_buf; + if (!suffix) { + suffix_buf = TerminateReasonNames[termReason]; + suffix_buf += ".err"; + suffix = suffix_buf.c_str(); + } + interpreterHandler->processTestCase(state, msg.str().c_str(), suffix); } terminateState(state); + + if (shouldExitOn(termReason)) + haltExecution = true; } // XXX shoot me @@ -2857,7 +3014,7 @@ void Executor::callExternalFunction(ExecutionState &state, if (NoExternals && !okExternals.count(function->getName())) { llvm::errs() << "KLEE:ERROR: Calling not-OK external function : " << function->getName().str() << "\n"; - terminateStateOnError(state, "externals disallowed", "user.err"); + terminateStateOnError(state, "externals disallowed", User); return; } @@ -2915,13 +3072,13 @@ void Executor::callExternalFunction(ExecutionState &state, bool success = externalDispatcher->executeCall(function, target->inst, args); if (!success) { terminateStateOnError(state, "failed external call: " + function->getName(), - "external.err"); + External); return; } if (!state.addressSpace.copyInConcretes()) { terminateStateOnError(state, "external modified read-only object", - "external.err"); + External); return; } @@ -3075,10 +3232,8 @@ void Executor::executeAlloc(ExecutionState &state, ExprPPrinter::printOne(info, " size expr", size); info << " concretization : " << example << "\n"; info << " unbound example: " << tmp << "\n"; - terminateStateOnError(*hugeSize.second, - "concretized symbolic size", - "model.err", - info.str()); + terminateStateOnError(*hugeSize.second, "concretized symbolic size", + Model, NULL, info.str()); } } } @@ -3105,14 +3260,10 @@ void Executor::executeFree(ExecutionState &state, ie = rl.end(); it != ie; ++it) { const MemoryObject *mo = it->first.first; if (mo->isLocal) { - terminateStateOnError(*it->second, - "free of alloca", - "free.err", + terminateStateOnError(*it->second, "free of alloca", Free, NULL, getAddressInfo(*it->second, address)); } else if (mo->isGlobal) { - terminateStateOnError(*it->second, - "free of global", - "free.err", + terminateStateOnError(*it->second, "free of global", Free, NULL, getAddressInfo(*it->second, address)); } else { it->second->addressSpace.unbindObject(mo); @@ -3147,10 +3298,8 @@ void Executor::resolveExact(ExecutionState &state, } if (unbound) { - terminateStateOnError(*unbound, - "memory error: invalid pointer: " + name, - "ptr.err", - getAddressInfo(*unbound, p)); + terminateStateOnError(*unbound, "memory error: invalid pointer: " + name, + Ptr, NULL, getAddressInfo(*unbound, p)); } } @@ -3205,9 +3354,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, const ObjectState *os = op.second; if (isWrite) { if (os->readOnly) { - terminateStateOnError(state, - "memory error: object read only", - "readonly.err"); + terminateStateOnError(state, "memory error: object read only", + ReadOnly); } else { ObjectState *wos = state.addressSpace.getWriteable(mo, os); wos->write(offset, value); @@ -3249,9 +3397,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (bound) { if (isWrite) { if (os->readOnly) { - terminateStateOnError(*bound, - "memory error: object read only", - "readonly.err"); + terminateStateOnError(*bound, "memory error: object read only", + ReadOnly); } else { ObjectState *wos = bound->addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), value); @@ -3272,10 +3419,8 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (incomplete) { terminateStateEarly(*unbound, "Query timed out (resolve)."); } else { - terminateStateOnError(*unbound, - "memory error: out of bound pointer", - "ptr.err", - getAddressInfo(*unbound, address)); + terminateStateOnError(*unbound, "memory error: out of bound pointer", Ptr, + NULL, getAddressInfo(*unbound, address)); } } } @@ -3310,9 +3455,8 @@ void Executor::executeMakeSymbolic(ExecutionState &state, std::vector<unsigned char> &values = si.assignment.bindings[array]; values = std::vector<unsigned char>(mo->size, '\0'); } else if (!AllowSeedExtension) { - terminateStateOnError(state, - "ran out of inputs during seeding", - "user.err"); + terminateStateOnError(state, "ran out of inputs during seeding", + User); break; } } else { @@ -3326,9 +3470,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, << " vs " << obj->name << "[" << obj->numBytes << "]" << " in test\n"; - terminateStateOnError(state, - msg.str(), - "user.err"); + terminateStateOnError(state, msg.str(), User); break; } else { std::vector<unsigned char> &values = si.assignment.bindings[array]; @@ -3345,11 +3487,11 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } else { ObjectState *os = bindObjectInState(state, mo, false); if (replayPosition >= replayKTest->numObjects) { - terminateStateOnError(state, "replay count mismatch", "user.err"); + terminateStateOnError(state, "replay count mismatch", User); } else { KTestObject *obj = &replayKTest->objects[replayPosition++]; if (obj->numBytes != mo->size) { - terminateStateOnError(state, "replay size mismatch", "user.err"); + terminateStateOnError(state, "replay size mismatch", User); } else { for (unsigned i=0; i<mo->size; i++) os->write8(i, obj->bytes[i]); @@ -3390,7 +3532,10 @@ void Executor::runFunctionAsMain(Function *f, if (++ai!=ae) { argvMO = memory->allocate((argc+1+envc+1+1) * NumPtrBytes, false, true, f->begin()->begin()); - + + if (!argvMO) + klee_error("Could not allocate memory for function arguments"); + arguments.push_back(argvMO->getBaseExpr()); if (++ai!=ae) { @@ -3430,6 +3575,8 @@ void Executor::runFunctionAsMain(Function *f, int j, len = strlen(s); MemoryObject *arg = memory->allocate(len+1, false, true, state->pc->inst); + if (!arg) + klee_error("Could not allocate memory for function arguments"); ObjectState *os = bindObjectInState(*state, arg, false); for (j=0; j<len+1; j++) os->write8(j, s[j]); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 600c7b90..93d1443e 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -101,7 +101,24 @@ public: typedef std::pair<ExecutionState*,ExecutionState*> StatePair; + enum TerminateReason { + Abort, + Assert, + Exec, + External, + Free, + Model, + Overflow, + Ptr, + ReadOnly, + ReportError, + User, + Unhandled + }; + private: + static const char *TerminateReasonNames[]; + class TimerInfo; KModule *kmodule; @@ -122,12 +139,12 @@ private: /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> addedStates; + std::vector<ExecutionState *> addedStates; /// Used to track states that have been removed during the current /// instructions step. /// \invariant \ref removedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> removedStates; + std::vector<ExecutionState *> removedStates; /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order @@ -362,6 +379,8 @@ private: const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction** lastInstruction); + bool shouldExitOn(enum TerminateReason termReason); + // remove state from queue and delete void terminateState(ExecutionState &state); // call exit handler and terminate state @@ -369,10 +388,10 @@ private: // call exit handler and terminate state void terminateStateOnExit(ExecutionState &state); // call error handler and terminate state - void terminateStateOnError(ExecutionState &state, - const llvm::Twine &message, - const char *suffix, - const llvm::Twine &longMessage=""); + void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, + enum TerminateReason termReason, + const char *suffix = NULL, + const llvm::Twine &longMessage = ""); // call error handler and terminate state, for execution errors // (things that should not be possible, like illegal instruction or @@ -380,7 +399,7 @@ private: void terminateStateOnExecError(ExecutionState &state, const llvm::Twine &message, const llvm::Twine &info="") { - terminateStateOnError(state, message, "exec.err", info); + terminateStateOnError(state, message, Exec, NULL, info); } /// bindModuleConstants - Initialize the module constant table. @@ -412,6 +431,7 @@ private: double maxInstTime); void checkMemoryUsage(); void printDebugInstructions(ExecutionState &state); + void doDumpStates(); public: Executor(const InterpreterOptions &opts, InterpreterHandler *ie); diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index b8ea97c2..f1c45105 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -52,7 +52,7 @@ public: ~HaltTimer() {} void run() { - llvm::errs() << "KLEE: HaltTimer invoked\n"; + klee_message("HaltTimer invoked"); executor->setHaltExecution(true); } }; @@ -179,7 +179,9 @@ void Executor::processTimers(ExecutionState *current, dumpStates = 0; } - if (maxInstTime>0 && current && !removedStates.count(current)) { + if (maxInstTime > 0 && current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) { if (timerTicks*kSecondsPerTick > maxInstTime) { klee_warning("max-instruction-time exceeded: %.2fs", timerTicks*kSecondsPerTick); diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index 7c76d480..f9f4b105 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -11,37 +11,135 @@ #include "Memory.h" #include "MemoryManager.h" -#include "klee/ExecutionState.h" #include "klee/Expr.h" -#include "klee/Solver.h" #include "klee/Internal/Support/ErrorHandling.h" #include "llvm/Support/CommandLine.h" +#include "llvm/Support/MathExtras.h" +#include <sys/mman.h> using namespace klee; +namespace { +llvm::cl::opt<bool> DeterministicAllocation( + "allocate-determ", + llvm::cl::desc("Allocate memory deterministically(default=off)"), + llvm::cl::init(false)); + +llvm::cl::opt<unsigned> DeterministicAllocationSize( + "allocate-determ-size", + llvm::cl::desc( + "Preallocated memory for deterministic allocation in MB (default=100)"), + llvm::cl::init(100)); + +llvm::cl::opt<bool> + NullOnZeroMalloc("return-null-on-zero-malloc", + llvm::cl::desc("Returns NULL in case malloc(size) was " + "called with size 0 (default=off)."), + llvm::cl::init(false)); + +llvm::cl::opt<unsigned> RedZoneSpace( + "red-zone-space", + llvm::cl::desc("Set the amount of free space between allocations. This is " + "important to detect out-of-bound accesses (default=10)."), + llvm::cl::init(10)); + +llvm::cl::opt<unsigned long long> DeterministicStartAddress( + "allocate-determ-start-address", + llvm::cl::desc("Start address for deterministic allocation. Has to be page " + "aligned (default=0x7ff30000000)."), + llvm::cl::init(0x7ff30000000)); +} + /***/ +MemoryManager::MemoryManager(ArrayCache *_arrayCache) + : arrayCache(_arrayCache), deterministicSpace(0), nextFreeSlot(0), + spaceSize(DeterministicAllocationSize.getValue() * 1024 * 1024) { + if (DeterministicAllocation) { + // Page boundary + void *expectedAddress = (void *)DeterministicStartAddress.getValue(); + + char *newSpace = + (char *)mmap(expectedAddress, spaceSize, PROT_READ | PROT_WRITE, + MAP_ANONYMOUS | MAP_PRIVATE, -1, 0); -MemoryManager::~MemoryManager() { + if (newSpace == MAP_FAILED) { + klee_error("Couldn't mmap() memory for deterministic allocations"); + } + if (expectedAddress != newSpace && expectedAddress != 0) { + klee_error("Could not allocate memory deterministically"); + } + + klee_message("Deterministic memory allocation starting from %p", newSpace); + deterministicSpace = newSpace; + nextFreeSlot = newSpace; + } +} + +MemoryManager::~MemoryManager() { while (!objects.empty()) { MemoryObject *mo = *objects.begin(); - if (!mo->isFixed) + if (!mo->isFixed && !DeterministicAllocation) free((void *)mo->address); objects.erase(mo); delete mo; } + + if (DeterministicAllocation) + munmap(deterministicSpace, spaceSize); } -MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, +MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, bool isGlobal, - const llvm::Value *allocSite) { - if (size>10*1024*1024) - klee_warning_once(0, "Large alloc: %u bytes. KLEE may run out of memory.", (unsigned) size); - - uint64_t address = (uint64_t) (unsigned long) malloc((unsigned) size); + const llvm::Value *allocSite, + size_t alignment) { + if (size > 10 * 1024 * 1024) + klee_warning_once(0, "Large alloc: %lu bytes. KLEE may run out of memory.", + size); + + // Return NULL if size is zero, this is equal to error during allocation + if (NullOnZeroMalloc && size == 0) + return 0; + + if (!llvm::isPowerOf2_64(alignment)) { + klee_warning("Only alignment of power of two is supported"); + return 0; + } + + uint64_t address = 0; + if (DeterministicAllocation) { + + address = llvm::RoundUpToAlignment((uint64_t)nextFreeSlot + alignment - 1, + alignment); + + // Handle the case of 0-sized allocations as 1-byte allocations. + // This way, we make sure we have this allocation between its own red zones + size_t alloc_size = std::max(size, (uint64_t)1); + if ((char *)address + alloc_size < deterministicSpace + spaceSize) { + nextFreeSlot = (char *)address + alloc_size + RedZoneSpace; + } else { + klee_warning_once( + 0, + "Couldn't allocate %lu bytes. Not enough deterministic space left.", + size); + address = 0; + } + } else { + // Use malloc for the standard case + if (alignment <= 8) + address = (uint64_t)malloc(size); + else { + int res = posix_memalign((void **)&address, alignment, size); + if (res < 0) { + klee_warning("Allocating aligned memory failed."); + address = 0; + } + } + } + if (!address) return 0; - + ++stats::allocations; MemoryObject *res = new MemoryObject(address, size, isLocal, isGlobal, false, allocSite, this); @@ -52,30 +150,31 @@ MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, MemoryObject *MemoryManager::allocateFixed(uint64_t address, uint64_t size, const llvm::Value *allocSite) { #ifndef NDEBUG - for (objects_ty::iterator it = objects.begin(), ie = objects.end(); - it != ie; ++it) { + for (objects_ty::iterator it = objects.begin(), ie = objects.end(); it != ie; + ++it) { MemoryObject *mo = *it; - if (address+size > mo->address && address < mo->address+mo->size) + if (address + size > mo->address && address < mo->address + mo->size) klee_error("Trying to allocate an overlapping object"); } #endif ++stats::allocations; - MemoryObject *res = new MemoryObject(address, size, false, true, true, - allocSite, this); + MemoryObject *res = + new MemoryObject(address, size, false, true, true, allocSite, this); objects.insert(res); return res; } -void MemoryManager::deallocate(const MemoryObject *mo) { - assert(0); -} +void MemoryManager::deallocate(const MemoryObject *mo) { assert(0); } void MemoryManager::markFreed(MemoryObject *mo) { - if (objects.find(mo) != objects.end()) - { - if (!mo->isFixed) + if (objects.find(mo) != objects.end()) { + if (!mo->isFixed && !DeterministicAllocation) free((void *)mo->address); objects.erase(mo); } } + +size_t MemoryManager::getUsedDeterministicSize() { + return nextFreeSlot - deterministicSpace; +} diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h index 01683443..fc77b476 100644 --- a/lib/Core/MemoryManager.h +++ b/lib/Core/MemoryManager.h @@ -14,31 +14,44 @@ #include <stdint.h> namespace llvm { - class Value; +class Value; } namespace klee { - class MemoryObject; - class ArrayCache; - - class MemoryManager { - private: - typedef std::set<MemoryObject*> objects_ty; - objects_ty objects; - ArrayCache *const arrayCache; - - public: - MemoryManager(ArrayCache *arrayCache) : arrayCache(arrayCache) {} - ~MemoryManager(); - - MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal, - const llvm::Value *allocSite); - MemoryObject *allocateFixed(uint64_t address, uint64_t size, - const llvm::Value *allocSite); - void deallocate(const MemoryObject *mo); - void markFreed(MemoryObject *mo); - ArrayCache *getArrayCache() const { return arrayCache; } - }; +class MemoryObject; +class ArrayCache; + +class MemoryManager { +private: + typedef std::set<MemoryObject *> objects_ty; + objects_ty objects; + ArrayCache *const arrayCache; + + char *deterministicSpace; + char *nextFreeSlot; + size_t spaceSize; + +public: + MemoryManager(ArrayCache *arrayCache); + ~MemoryManager(); + + /** + * Returns memory object which contains a handle to real virtual process + * memory. + */ + MemoryObject *allocate(uint64_t size, bool isLocal, bool isGlobal, + const llvm::Value *allocSite, size_t alignment = 8); + MemoryObject *allocateFixed(uint64_t address, uint64_t size, + const llvm::Value *allocSite); + void deallocate(const MemoryObject *mo); + void markFreed(MemoryObject *mo); + ArrayCache *getArrayCache() const { return arrayCache; } + + /* + * Returns the size used by deterministic allocation in bytes + */ + size_t getUsedDeterministicSize(); +}; } // End klee namespace diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index cbb88727..973057c3 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -67,13 +67,14 @@ ExecutionState &DFSSearcher::selectState() { } void DFSSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.back()) { states.pop_back(); @@ -101,13 +102,14 @@ ExecutionState &BFSSearcher::selectState() { } void BFSSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; if (es == states.front()) { states.pop_front(); @@ -134,14 +136,16 @@ ExecutionState &RandomSearcher::selectState() { return *states[theRNG.getInt32()%states.size()]; } -void RandomSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +RandomSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { states.insert(states.end(), addedStates.begin(), addedStates.end()); - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; bool ok = false; @@ -224,20 +228,24 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { } } -void WeightedRandomSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { - if (current && updateWeights && !removedStates.count(current)) +void WeightedRandomSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + if (current && updateWeights && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end()) states->update(current, getWeight(current)); - - for (std::set<ExecutionState*>::const_iterator it = addedStates.begin(), - ie = addedStates.end(); it != ie; ++it) { + + for (std::vector<ExecutionState *>::const_iterator it = addedStates.begin(), + ie = addedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; states->insert(es, getWeight(es)); } - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + for (std::vector<ExecutionState *>::const_iterator it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { states->remove(*it); } } @@ -277,9 +285,10 @@ ExecutionState &RandomPathSearcher::selectState() { return *n->data; } -void RandomPathSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +RandomPathSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { } bool RandomPathSearcher::empty() { @@ -358,9 +367,9 @@ entry: } } -void BumpMergingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void BumpMergingSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { baseSearcher->update(current, addedStates, removedStates); } @@ -472,18 +481,21 @@ ExecutionState &MergingSearcher::selectState() { return selectState(); } -void MergingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void +MergingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { if (!removedStates.empty()) { - std::set<ExecutionState *> alt = removedStates; - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + std::vector<ExecutionState *> alt = removedStates; + for (std::vector<ExecutionState *>::const_iterator + it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::const_iterator it2 = statesAtMerge.find(es); if (it2 != statesAtMerge.end()) { statesAtMerge.erase(it2); - alt.erase(alt.find(es)); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -529,10 +541,12 @@ ExecutionState &BatchingSearcher::selectState() { } } -void BatchingSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { - if (removedStates.count(lastState)) +void +BatchingSearcher::update(ExecutionState *current, + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { + if (std::find(removedStates.begin(), removedStates.end(), lastState) != + removedStates.end()) lastState = 0; baseSearcher->update(current, addedStates, removedStates); } @@ -554,20 +568,22 @@ ExecutionState &IterativeDeepeningTimeSearcher::selectState() { return res; } -void IterativeDeepeningTimeSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void IterativeDeepeningTimeSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { double elapsed = util::getWallTime() - startTime; if (!removedStates.empty()) { - std::set<ExecutionState *> alt = removedStates; - for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(), - ie = removedStates.end(); it != ie; ++it) { + std::vector<ExecutionState *> alt = removedStates; + for (std::vector<ExecutionState *>::const_iterator + it = removedStates.begin(), + ie = removedStates.end(); + it != ie; ++it) { ExecutionState *es = *it; std::set<ExecutionState*>::const_iterator it2 = pausedStates.find(es); if (it2 != pausedStates.end()) { - pausedStates.erase(it); - alt.erase(alt.find(es)); + pausedStates.erase(it2); + alt.erase(std::remove(alt.begin(), alt.end(), es), alt.end()); } } baseSearcher->update(current, addedStates, alt); @@ -575,7 +591,10 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, baseSearcher->update(current, addedStates, removedStates); } - if (current && !removedStates.count(current) && elapsed>time) { + if (current && + std::find(removedStates.begin(), removedStates.end(), current) == + removedStates.end() && + elapsed > time) { pausedStates.insert(current); baseSearcher->removeState(current); } @@ -583,7 +602,8 @@ void IterativeDeepeningTimeSearcher::update(ExecutionState *current, if (baseSearcher->empty()) { time *= 2; llvm::errs() << "KLEE: increasing time budget to: " << time << "\n"; - baseSearcher->update(0, pausedStates, std::set<ExecutionState*>()); + std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end()); + baseSearcher->update(0, ps, std::vector<ExecutionState *>()); pausedStates.clear(); } } @@ -607,9 +627,9 @@ ExecutionState &InterleavedSearcher::selectState() { return s->selectState(); } -void InterleavedSearcher::update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) { +void InterleavedSearcher::update( + ExecutionState *current, const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) { for (std::vector<Searcher*>::const_iterator it = searchers.begin(), ie = searchers.end(); it != ie; ++it) (*it)->update(current, addedStates, removedStates); diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index d866f521..4ede3640 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -35,8 +35,8 @@ namespace klee { virtual ExecutionState &selectState() = 0; virtual void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) = 0; + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) = 0; virtual bool empty() = 0; @@ -55,15 +55,15 @@ namespace klee { // utility functions void addState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, tmp, std::set<ExecutionState*>()); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, tmp, std::vector<ExecutionState *>()); } void removeState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, std::set<ExecutionState*>(), tmp); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, std::vector<ExecutionState *>(), tmp); } enum CoreSearchType { @@ -86,8 +86,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; @@ -100,8 +100,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; @@ -114,8 +114,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; @@ -146,8 +146,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "WeightedRandomSearcher::"; @@ -172,8 +172,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; @@ -195,8 +195,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; @@ -218,8 +218,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; @@ -243,8 +243,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty(); } void printName(llvm::raw_ostream &os) { os << "<BatchingSearcher> timeBudget: " << timeBudget @@ -266,8 +266,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; @@ -286,8 +286,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return searchers[0]->empty(); } void printName(llvm::raw_ostream &os) { os << "<InterleavedSearcher> containing " diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 542d7f5b..0ecbdd07 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -281,7 +281,7 @@ void SpecialFunctionHandler::handleAbort(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { assert(arguments.size()==0 && "invalid number of arguments to abort"); - executor.terminateStateOnError(state, "abort failure", "abort.err"); + executor.terminateStateOnError(state, "abort failure", Executor::Abort); } void SpecialFunctionHandler::handleExit(ExecutionState &state, @@ -318,7 +318,7 @@ void SpecialFunctionHandler::handleAssert(ExecutionState &state, assert(arguments.size()==3 && "invalid number of arguments to _assert"); executor.terminateStateOnError(state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - "assert.err"); + Executor::Assert); } void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, @@ -327,7 +327,7 @@ void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, assert(arguments.size()==4 && "invalid number of arguments to __assert_fail"); executor.terminateStateOnError(state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - "assert.err"); + Executor::Assert); } void SpecialFunctionHandler::handleReportError(ExecutionState &state, @@ -338,6 +338,7 @@ void SpecialFunctionHandler::handleReportError(ExecutionState &state, // arguments[0], arguments[1] are file, line executor.terminateStateOnError(state, readStringAtAddress(state, arguments[2]), + Executor::ReportError, readStringAtAddress(state, arguments[3]).c_str()); } @@ -410,7 +411,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, } else { executor.terminateStateOnError(state, "invalid klee_assume call (provably false)", - "user.err"); + Executor::User); } } else { executor.addConstraint(state, e); @@ -475,7 +476,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, } else { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", - "user.err"); + Executor::User); } } @@ -634,14 +635,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) { executor.terminateStateOnError(state, "check_memory_access requires constant args", - "user.err"); + Executor::User); } else { ObjectPair op; if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) { executor.terminateStateOnError(state, "check_memory_access: memory error", - "ptr.err", + Executor::Ptr, NULL, executor.getAddressInfo(state, address)); } else { ref<Expr> chk = @@ -650,7 +651,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!chk->isTrue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", - "ptr.err", + Executor::Ptr, NULL, executor.getAddressInfo(state, address)); } } @@ -711,9 +712,8 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, ExecutionState *s = it->second; if (old->readOnly) { - executor.terminateStateOnError(*s, - "cannot make readonly object symbolic", - "user.err"); + executor.terminateStateOnError(*s, "cannot make readonly object symbolic", + Executor::User); return; } @@ -732,7 +732,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, } else { executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", - "user.err"); + Executor::User); } } } @@ -757,31 +757,27 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned addition", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned addition", + Executor::Overflow); } void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned subtraction", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned subtraction", + Executor::Overflow); } void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on unsigned multiplication", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on unsigned multiplication", + Executor::Overflow); } void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { - executor.terminateStateOnError(state, - "overflow on division or remainder", - "overflow.err"); + executor.terminateStateOnError(state, "overflow on division or remainder", + Executor::Overflow); } diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 5e77172e..97ed26ea 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -86,17 +86,20 @@ namespace { cl::init(1.), cl::desc("Approximate number of seconds between stats writes (default=1.0s)")); + cl::opt<unsigned> StatsWriteAfterInstructions( + "stats-write-after-instructions", cl::init(0), + cl::desc("Write statistics after each n instructions, 0 to disable " + "(default=0)")); + cl::opt<double> IStatsWriteInterval("istats-write-interval", cl::init(10.), cl::desc("Approximate number of seconds between istats writes (default: 10.0s)")); - /* - cl::opt<double> - BranchCovCountsWriteInterval("branch-cov-counts-write-interval", - cl::desc("Approximate number of seconds between run.branches writes (default: 5.0s)"), - cl::init(5.)); - */ + cl::opt<unsigned> IStatsWriteAfterInstructions( + "istats-write-after-instructions", cl::init(0), + cl::desc("Write istats after each n instructions, 0 to disable " + "(default=0)")); // XXX I really would like to have dynamic rate control for something like this. cl::opt<double> @@ -185,6 +188,18 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, fullBranches(0), partialBranches(0), updateMinDistToUncovered(_updateMinDistToUncovered) { + + if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0) + klee_error("Both options --stats-write-interval and " + "--stats-write-after-instructions cannot be enabled at the same " + "time."); + + if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0) + klee_error( + "Both options --istats-write-interval and " + "--istats-write-after-instructions cannot be enabled at the same " + "time."); + KModule *km = executor.kmodule; if (!sys::path::is_absolute(objectFilename)) { @@ -235,19 +250,22 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, writeStatsHeader(); writeStatsLine(); - executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + if (StatsWriteInterval > 0) + executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + } - if (updateMinDistToUncovered) { - computeReachableUncovered(); - executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval); - } + // Add timer to calculate uncovered instructions if needed by the solver + if (updateMinDistToUncovered) { + computeReachableUncovered(); + executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval); } if (OutputIStats) { istatsFile = executor.interpreterHandler->openOutputFile("run.istats"); assert(istatsFile && "unable to open istats file"); - executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); + if (IStatsWriteInterval > 0) + executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); } } @@ -261,8 +279,12 @@ StatsTracker::~StatsTracker() { void StatsTracker::done() { if (statsFile) writeStatsLine(); - if (OutputIStats) + + if (OutputIStats) { + if (updateMinDistToUncovered) + computeReachableUncovered(); writeIStats(); + } } void StatsTracker::stepInstruction(ExecutionState &es) { @@ -310,6 +332,14 @@ void StatsTracker::stepInstruction(ExecutionState &es) { } } } + + if (statsFile && StatsWriteAfterInstructions && + stats::instructions % StatsWriteAfterInstructions.getValue() == 0) + writeStatsLine(); + + if (istatsFile && IStatsWriteAfterInstructions && + stats::instructions % IStatsWriteAfterInstructions.getValue() == 0) + writeIStats(); } /// @@ -327,15 +357,17 @@ void StatsTracker::framePushed(ExecutionState &es, StackFrame *parentFrame) { sf.callPathNode = cp; cp->count++; } + } - if (updateMinDistToUncovered) { - uint64_t minDistAtRA = 0; - if (parentFrame) - minDistAtRA = parentFrame->minDistToUncoveredOnReturn; - - sf.minDistToUncoveredOnReturn = sf.caller ? - computeMinDistToUncovered(sf.caller, minDistAtRA) : 0; - } + if (updateMinDistToUncovered) { + StackFrame &sf = es.stack.back(); + + uint64_t minDistAtRA = 0; + if (parentFrame) + minDistAtRA = parentFrame->minDistToUncoveredOnReturn; + + sf.minDistToUncoveredOnReturn = + sf.caller ? computeMinDistToUncovered(sf.caller, minDistAtRA) : 0; } } @@ -406,7 +438,7 @@ void StatsTracker::writeStatsLine() { << "," << numBranches << "," << util::getUserTime() << "," << executor.states.size() - << "," << util::GetTotalMallocUsage() + << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize() << "," << stats::queries << "," << stats::queryConstructs << "," << 0 // was numObjects |