diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Core/Executor.cpp | 270 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 72 | ||||
| -rw-r--r-- | lib/Core/MergeHandler.cpp | 2 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 158 |
4 files changed, 241 insertions, 261 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3d6ea4ae..fdb8e3b8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -267,35 +267,34 @@ cl::opt<std::string> /*** Termination criteria options ***/ -cl::list<Executor::TerminateReason> ExitOnErrorType( +cl::list<StateTerminationType> ExitOnErrorType( "exit-on-error-type", - cl::desc( - "Stop execution after reaching a specified condition (default=false)"), + cl::desc("Stop execution after reaching a specified condition (default=false)"), cl::values( - clEnumValN(Executor::Abort, "Abort", "The program crashed"), - clEnumValN(Executor::Assert, "Assert", "An assertion was hit"), - clEnumValN(Executor::BadVectorAccess, "BadVectorAccess", + clEnumValN(StateTerminationType::Abort, "Abort", + "The program crashed (reached abort()/klee_abort())"), + clEnumValN(StateTerminationType::Assert, "Assert", + "An assertion was hit"), + clEnumValN(StateTerminationType::BadVectorAccess, "BadVectorAccess", "Vector accessed out of bounds"), - clEnumValN(Executor::Exec, "Exec", + clEnumValN(StateTerminationType::Execution, "Execution", "Trying to execute an unexpected instruction"), - clEnumValN(Executor::External, "External", + clEnumValN(StateTerminationType::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", + clEnumValN(StateTerminationType::Free, "Free", + "Freeing invalid memory"), + clEnumValN(StateTerminationType::Model, "Model", + "Memory model limit hit"), + clEnumValN(StateTerminationType::Overflow, "Overflow", + "An overflow occurred"), + clEnumValN(StateTerminationType::Ptr, "Ptr", "Pointer error"), + clEnumValN(StateTerminationType::ReadOnly, "ReadOnly", + "Write to read-only memory"), + clEnumValN(StateTerminationType::ReportError, "ReportError", "klee_report_error called"), - clEnumValN(Executor::User, "User", "Wrong klee_* functions invocation"), -#ifdef SUPPORT_KLEE_EH_CXX - clEnumValN(Executor::UncaughtException, "UncaughtException", - "Exception was not caught"), - clEnumValN(Executor::UnexpectedException, "UnexpectedException", - "An unexpected exception was thrown"), -#endif - clEnumValN(Executor::Unhandled, "Unhandled", - "Unhandled instruction hit") KLEE_LLVM_CL_VAL_END), + clEnumValN(StateTerminationType::User, "User", + "Wrong klee_* functions invocation") + KLEE_LLVM_CL_VAL_END), cl::ZeroOrMore, cl::cat(TerminationCat)); @@ -436,27 +435,6 @@ cl::opt<bool> DebugCheckForImpliedValues( extern "C" unsigned dumpStates, dumpPTree; unsigned dumpStates = 0, dumpPTree = 0; -const char *Executor::TerminateReasonNames[] = { - [ Abort ] = "abort", - [ Assert ] = "assert", - [ BadVectorAccess ] = "bad_vector_access", - [ Exec ] = "exec", - [ External ] = "external", - [ Free ] = "free", - [ Model ] = "model", - [ Overflow ] = "overflow", - [ Ptr ] = "ptr", - [ ReadOnly ] = "readonly", - [ ReportError ] = "reporterror", - [ User ] = "user", -#ifdef SUPPORT_KLEE_EH_CXX - [ UncaughtException ] = "uncaught_exception", - [ UnexpectedException ] = "unexpected_exception", -#endif - [ Unhandled ] = "xxx", -}; - - Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), interpreterHandler(ih), searcher(0), @@ -960,10 +938,10 @@ void Executor::branch(ExecutionState &state, if (OnlyReplaySeeds) { for (unsigned i=0; i<N; ++i) { if (result[i] && !seedMap.count(result[i])) { - terminateState(*result[i]); - result[i] = NULL; + terminateStateEarly(*result[i], "Unseeded path during replay", StateTerminationType::Replay); + result[i] = nullptr; } - } + } } } @@ -1047,7 +1025,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { solver->setTimeout(time::Span()); if (!success) { current.pc = current.prevPC; - terminateStateEarly(current, "Query timed out (fork)."); + terminateStateOnSolverError(current, "Query timed out (fork)."); return StatePair(nullptr, nullptr); } @@ -1210,8 +1188,8 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { // Kinda gross, do we even really still want this option? if (MaxDepth && MaxDepth<=trueState->depth) { - terminateStateEarly(*trueState, "max-depth exceeded."); - terminateStateEarly(*falseState, "max-depth exceeded."); + terminateStateEarly(*trueState, "max-depth exceeded.", StateTerminationType::MaxDepth); + terminateStateEarly(*falseState, "max-depth exceeded.", StateTerminationType::MaxDepth); return StatePair(nullptr, nullptr); } @@ -1489,9 +1467,8 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, } else if (current_clause->isNullValue()) { ti_addr = 0; } else { - terminateStateOnError( - state, "Internal: Clause is not a bitcast or null (catch-all)", - Exec); + terminateStateOnExecError( + state, "Internal: Clause is not a bitcast or null (catch-all)"); stateTerminated = true; return nullptr; } @@ -1515,8 +1492,8 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, if (num_elements >= std::numeric_limits<decltype(serialized_num_elements)>::max()) { - terminateStateOnError( - state, "Internal: too many elements in landingpad filter", Exec); + terminateStateOnExecError( + state, "Internal: too many elements in landingpad filter"); stateTerminated = true; return nullptr; } @@ -1529,10 +1506,9 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, llvm::BitCastOperator const *bitcast = dyn_cast<llvm::BitCastOperator>(v); if (!bitcast) { - terminateStateOnError(state, - "Internal: expected value inside a " - "filter-clause to be a bitcast", - Exec); + terminateStateOnExecError(state, + "Internal: expected value inside a " + "filter-clause to be a bitcast"); stateTerminated = true; return nullptr; } @@ -1540,10 +1516,9 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, llvm::GlobalValue const *clause_value = dyn_cast<GlobalValue>(bitcast->getOperand(0)); if (!clause_value) { - terminateStateOnError(state, - "Internal: expected value inside a " - "filter-clause bitcast to be a GlobalValue", - Exec); + terminateStateOnExecError(state, + "Internal: expected value inside a " + "filter-clause bitcast to be a GlobalValue"); stateTerminated = true; return nullptr; } @@ -1876,7 +1851,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, // well. default: klee_warning("unimplemented intrinsic: %s", f->getName().data()); - terminateStateOnError(state, "unimplemented intrinsic", Unhandled); + terminateStateOnExecError(state, "unimplemented intrinsic"); return; } @@ -1887,7 +1862,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, // Check if maximum stack size was reached. // We currently only count the number of stack frames if (RuntimeMaxStackFrames && state.stack.size() > RuntimeMaxStackFrames) { - terminateStateEarly(state, "Maximum stack size reached."); + terminateStateEarly(state, "Maximum stack size reached.", StateTerminationType::OutOfStackMemory); klee_warning("Maximum stack size reached."); return; } @@ -1913,14 +1888,12 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, 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); + terminateStateOnUserError(state, "calling function with too few arguments"); return; } } else { if (callingArgs < funcArgs) { - terminateStateOnError(state, "calling function with too few arguments", - User); + terminateStateOnUserError(state, "calling function with too few arguments"); return; } @@ -3198,9 +3171,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ConstantExpr *cIdx = dyn_cast<ConstantExpr>(idx); if (cIdx == NULL) { - terminateStateOnError( - state, "InsertElement, support for symbolic index not implemented", - Unhandled); + terminateStateOnExecError( + state, "InsertElement, support for symbolic index not implemented"); return; } uint64_t iIdx = cIdx->getZExtValue(); @@ -3214,7 +3186,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds write terminateStateOnError(state, "Out of bounds write when inserting element", - BadVectorAccess); + StateTerminationType::BadVectorAccess); return; } @@ -3240,9 +3212,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ConstantExpr *cIdx = dyn_cast<ConstantExpr>(idx); if (cIdx == NULL) { - terminateStateOnError( - state, "ExtractElement, support for symbolic index not implemented", - Unhandled); + terminateStateOnExecError( + state, "ExtractElement, support for symbolic index not implemented"); return; } uint64_t iIdx = cIdx->getZExtValue(); @@ -3256,7 +3227,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (iIdx >= vt->getNumElements()) { // Out of bounds read terminateStateOnError(state, "Out of bounds read when extracting element", - BadVectorAccess); + StateTerminationType::BadVectorAccess); return; } @@ -3509,7 +3480,7 @@ bool Executor::checkMemoryUsage() { idx = theRNG.getInt32() % N; std::swap(arr[idx], arr[N - 1]); - terminateStateEarly(*arr[N - 1], "Memory limit exceeded."); + terminateStateEarly(*arr[N - 1], "Memory limit exceeded.", StateTerminationType::OutOfMemory); } return false; @@ -3523,7 +3494,7 @@ void Executor::doDumpStates() { klee_message("halting execution, dumping remaining states"); for (const auto &state : states) - terminateStateEarly(*state, "Execution halting."); + terminateStateEarly(*state, "Execution halting.", StateTerminationType::Interrupted); updateStates(nullptr); } @@ -3707,23 +3678,49 @@ void Executor::terminateState(ExecutionState &state) { } } -void Executor::terminateStateEarly(ExecutionState &state, - const Twine &message) { - if (!OnlyOutputStatesCoveringNew || state.coveredNew || - (AlwaysOutputSeeds && seedMap.count(&state))) - interpreterHandler->processTestCase(state, (message + "\n").str().c_str(), - "early"); - terminateState(state); +static bool shouldWriteTest(const ExecutionState &state) { + return !OnlyOutputStatesCoveringNew || state.coveredNew; } +static std::string terminationTypeFileExtension(StateTerminationType type) { + std::string ret; +#define TTYPE(N,I,S) case StateTerminationType::N: ret = (S); break; +#define MARK(N,I) + switch (type) { + TERMINATION_TYPES + } +#undef TTYPE +#undef MARK + return ret; +}; + void Executor::terminateStateOnExit(ExecutionState &state) { - if (!OnlyOutputStatesCoveringNew || state.coveredNew || - (AlwaysOutputSeeds && seedMap.count(&state))) - interpreterHandler->processTestCase(state, 0, 0); + if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state))) + interpreterHandler->processTestCase( + state, nullptr, + terminationTypeFileExtension(StateTerminationType::Exit).c_str()); + interpreterHandler->incPathsCompleted(); terminateState(state); } +void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, + StateTerminationType terminationType) { + if ((terminationType <= StateTerminationType::EXECERR && + shouldWriteTest(state)) || + (AlwaysOutputSeeds && seedMap.count(&state))) { + interpreterHandler->processTestCase( + state, (message + "\n").str().c_str(), + terminationTypeFileExtension(terminationType).c_str()); + } + + terminateState(state); +} + +void Executor::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) { + terminateStateOnError(state, message, StateTerminationType::User, ""); +} + const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state, Instruction ** lastInstruction) { // unroll the stack of the applications state and find @@ -3767,30 +3764,24 @@ 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; +bool shouldExitOn(StateTerminationType reason) { + auto it = std::find(ExitOnErrorType.begin(), ExitOnErrorType.end(), reason); + return it != ExitOnErrorType.end(); } void Executor::terminateStateOnError(ExecutionState &state, const llvm::Twine &messaget, - enum TerminateReason termReason, - const char *suffix, - const llvm::Twine &info) { + StateTerminationType terminationType, + const llvm::Twine &info, + const char *suffix) { std::string message = messaget.str(); static std::set< std::pair<Instruction*, std::string> > emittedErrors; Instruction * lastInst; const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst); - + if (EmitAllErrors || emittedErrors.insert(std::make_pair(lastInst, message)).second) { - if (ii.file != "") { + if (!ii.file.empty()) { klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str()); } else { klee_message("ERROR: (location information missing) %s", message.c_str()); @@ -3801,7 +3792,7 @@ void Executor::terminateStateOnError(ExecutionState &state, std::string MsgString; llvm::raw_string_ostream msg(MsgString); msg << "Error: " << message << '\n'; - if (ii.file != "") { + if (!ii.file.empty()) { msg << "File: " << ii.file << '\n' << "Line: " << ii.line << '\n' << "assembly.ll line: " << ii.assemblyLine << '\n' @@ -3811,25 +3802,32 @@ void Executor::terminateStateOnError(ExecutionState &state, state.dumpStack(msg); std::string info_str = info.str(); - if (info_str != "") + if (!info_str.empty()) 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); + const std::string ext = terminationTypeFileExtension(terminationType); + // use user provided suffix from klee_report_error() + const char * file_suffix = suffix ? suffix : ext.c_str(); + interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); } - + terminateState(state); - if (shouldExitOn(termReason)) + if (shouldExitOn(terminationType)) haltExecution = true; } +void Executor::terminateStateOnExecError(ExecutionState &state, + const llvm::Twine &message, + const llvm::Twine &info) { + terminateStateOnError(state, message, StateTerminationType::Execution, info); +} + +void Executor::terminateStateOnSolverError(ExecutionState &state, + const llvm::Twine &message) { + terminateStateOnError(state, message, StateTerminationType::Solver, ""); +} + // XXX shoot me static const char *okExternalsList[] = { "printf", "fprintf", @@ -3851,7 +3849,7 @@ void Executor::callExternalFunction(ExecutionState &state, !okExternals.count(function->getName().str())) { klee_warning("Disallowed call to external function: %s\n", function->getName().str().c_str()); - terminateStateOnError(state, "external calls disallowed", User); + terminateStateOnUserError(state, "external calls disallowed"); return; } @@ -3886,8 +3884,8 @@ void Executor::callExternalFunction(ExecutionState &state, ce->toMemory(&args[wordIndex]); wordIndex += (ce->getWidth()+63)/64; } else { - terminateStateOnExecError(state, - "external call with symbolic argument: " + + terminateStateOnExecError(state, + "external call with symbolic argument: " + function->getName()); return; } @@ -3938,13 +3936,13 @@ void Executor::callExternalFunction(ExecutionState &state, bool success = externalDispatcher->executeCall(function, target->inst, args); if (!success) { terminateStateOnError(state, "failed external call: " + function->getName(), - External); + StateTerminationType::External); return; } if (!state.addressSpace.copyInConcretes()) { terminateStateOnError(state, "external modified read-only object", - External); + StateTerminationType::External); return; } @@ -4118,7 +4116,7 @@ void Executor::executeAlloc(ExecutionState &state, info << " concretization : " << example << "\n"; info << " unbound example: " << tmp << "\n"; terminateStateOnError(*hugeSize.second, "concretized symbolic size", - Model, NULL, info.str()); + StateTerminationType::Model, info.str()); } } } @@ -4146,10 +4144,12 @@ 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, NULL, + terminateStateOnError(*it->second, "free of alloca", + StateTerminationType::Free, getAddressInfo(*it->second, address)); } else if (mo->isGlobal) { - terminateStateOnError(*it->second, "free of global", Free, NULL, + terminateStateOnError(*it->second, "free of global", + StateTerminationType::Free, getAddressInfo(*it->second, address)); } else { it->second->addressSpace.unbindObject(mo); @@ -4186,7 +4186,7 @@ void Executor::resolveExact(ExecutionState &state, if (unbound) { terminateStateOnError(*unbound, "memory error: invalid pointer: " + name, - Ptr, NULL, getAddressInfo(*unbound, p)); + StateTerminationType::Ptr, getAddressInfo(*unbound, p)); } } @@ -4236,7 +4236,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, solver->setTimeout(time::Span()); if (!success) { state.pc = state.prevPC; - terminateStateEarly(state, "Query timed out (bounds check)."); + terminateStateOnSolverError(state, "Query timed out (bounds check)."); return; } @@ -4245,7 +4245,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (isWrite) { if (os->readOnly) { terminateStateOnError(state, "memory error: object read only", - ReadOnly); + StateTerminationType::ReadOnly); } else { ObjectState *wos = state.addressSpace.getWriteable(mo, os); wos->write(offset, value); @@ -4289,7 +4289,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, if (isWrite) { if (os->readOnly) { terminateStateOnError(*bound, "memory error: object read only", - ReadOnly); + StateTerminationType::ReadOnly); } else { ObjectState *wos = bound->addressSpace.getWriteable(mo, os); wos->write(mo->getOffsetExpr(address), value); @@ -4308,10 +4308,11 @@ void Executor::executeMemoryOperation(ExecutionState &state, // XXX should we distinguish out of bounds and overlapped cases? if (unbound) { if (incomplete) { - terminateStateEarly(*unbound, "Query timed out (resolve)."); + terminateStateOnSolverError(*unbound, "Query timed out (resolve)."); } else { - terminateStateOnError(*unbound, "memory error: out of bound pointer", Ptr, - NULL, getAddressInfo(*unbound, address)); + terminateStateOnError(*unbound, "memory error: out of bound pointer", + StateTerminationType::Ptr, + getAddressInfo(*unbound, address)); } } } @@ -4346,8 +4347,7 @@ 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); + terminateStateOnUserError(state, "ran out of inputs during seeding"); break; } } else { @@ -4361,7 +4361,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, << " vs " << obj->name << "[" << obj->numBytes << "]" << " in test\n"; - terminateStateOnError(state, msg.str(), User); + terminateStateOnUserError(state, msg.str()); break; } else { std::vector<unsigned char> &values = si.assignment.bindings[array]; @@ -4378,11 +4378,11 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } else { ObjectState *os = bindObjectInState(state, mo, false); if (replayPosition >= replayKTest->numObjects) { - terminateStateOnError(state, "replay count mismatch", User); + terminateStateOnUserError(state, "replay count mismatch"); } else { KTestObject *obj = &replayKTest->objects[replayPosition++]; if (obj->numBytes != mo->size) { - terminateStateOnError(state, "replay size mismatch", User); + terminateStateOnUserError(state, "replay size mismatch"); } else { for (unsigned i=0; i<mo->size; i++) os->write8(i, obj->bytes[i]); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 987edf47..e9763547 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -20,6 +20,7 @@ #include "klee/ADT/RNG.h" #include "klee/Core/Interpreter.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Expr/ArrayCache.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Module/Cell.h" @@ -98,32 +99,10 @@ class Executor : public Interpreter { public: typedef std::pair<ExecutionState*,ExecutionState*> StatePair; - enum TerminateReason { - Abort, - Assert, - BadVectorAccess, - Exec, - External, - Free, - Model, - Overflow, - Ptr, - ReadOnly, - ReportError, - User, -#ifdef SUPPORT_KLEE_EH_CXX - UncaughtException, - UnexpectedException, -#endif - Unhandled, - }; - /// The random number generator. RNG theRNG; private: - static const char *TerminateReasonNames[]; - std::unique_ptr<KModule> kmodule; InterpreterHandler *interpreterHandler; Searcher *searcher; @@ -430,28 +409,41 @@ private: const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, llvm::Instruction** lastInstruction); - bool shouldExitOn(enum TerminateReason termReason); - - // remove state from queue and delete + /// Remove state from queue and delete state void terminateState(ExecutionState &state); - // call exit handler and terminate state - void terminateStateEarly(ExecutionState &state, const llvm::Twine &message); - // call exit handler and terminate state + + /// Call exit handler and terminate state normally + /// (end of execution path) void terminateStateOnExit(ExecutionState &state); - // call error handler and terminate state + + /// Call exit handler and terminate state early + /// (e.g. due to state merging or memory pressure) + void terminateStateEarly(ExecutionState &state, const llvm::Twine &message, + StateTerminationType terminationType); + + /// Call error handler and terminate state in case of program errors + /// (e.g. free()ing globals, out-of-bound accesses) 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 - // unlowered instrinsic, or are unsupported, like inline assembly) - void terminateStateOnExecError(ExecutionState &state, + StateTerminationType terminationType, + const llvm::Twine &longMessage = "", + const char *suffix = nullptr); + + /// Call error handler and terminate state in case of execution errors + /// (things that should not be possible, like illegal instruction or + /// unlowered intrinsic, or unsupported intrinsics, like inline assembly) + void terminateStateOnExecError(ExecutionState &state, const llvm::Twine &message, - const llvm::Twine &info="") { - terminateStateOnError(state, message, Exec, NULL, info); - } + const llvm::Twine &info = ""); + + /// Call error handler and terminate state in case of solver errors + /// (solver error or timeout) + void terminateStateOnSolverError(ExecutionState &state, + const llvm::Twine &message); + + /// Call error handler and terminate state for user errors + /// (e.g. wrong usage of klee.h API) + void terminateStateOnUserError(ExecutionState &state, + const llvm::Twine &message); /// bindModuleConstants - Initialize the module constant table. void bindModuleConstants(); diff --git a/lib/Core/MergeHandler.cpp b/lib/Core/MergeHandler.cpp index 578b1b51..00677541 100644 --- a/lib/Core/MergeHandler.cpp +++ b/lib/Core/MergeHandler.cpp @@ -106,7 +106,7 @@ void MergeHandler::addClosedState(ExecutionState *es, for (auto& mState: cpv) { if (mState->merge(*es)) { - executor->terminateState(*es); + executor->terminateStateEarly(*es, "merged state.", StateTerminationType::Merge); executor->mergingSearcher->inCloseMerge.erase(es); mergedSuccessful = true; break; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 94c4dc3c..5c0246b3 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -246,16 +246,14 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, ObjectPair op; addressExpr = executor.toUnique(state, addressExpr); if (!isa<ConstantExpr>(addressExpr)) { - executor.terminateStateOnError( - state, "Symbolic string pointer passed to one of the klee_ functions", - Executor::TerminateReason::User); + executor.terminateStateOnUserError( + state, "Symbolic string pointer passed to one of the klee_ functions"); return ""; } ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr); if (!state.addressSpace.resolveOne(address, op)) { - executor.terminateStateOnError( - state, "Invalid string pointer passed to one of the klee_ functions", - Executor::TerminateReason::User); + executor.terminateStateOnUserError( + state, "Invalid string pointer passed to one of the klee_ functions"); return ""; } const MemoryObject *mo = op.first; @@ -292,54 +290,57 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, /****/ 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", Executor::Abort); + KInstruction *target, + std::vector<ref<Expr>> &arguments) { + assert(arguments.size() == 0 && "invalid number of arguments to abort"); + executor.terminateStateOnError(state, "abort failure", + StateTerminationType::Abort); } void SpecialFunctionHandler::handleExit(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { - assert(arguments.size()==1 && "invalid number of arguments to exit"); + KInstruction *target, + std::vector<ref<Expr>> &arguments) { + assert(arguments.size() == 1 && "invalid number of arguments to exit"); executor.terminateStateOnExit(state); } -void SpecialFunctionHandler::handleSilentExit(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { - assert(arguments.size()==1 && "invalid number of arguments to exit"); - executor.terminateState(state); +void SpecialFunctionHandler::handleSilentExit( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { + assert(arguments.size() == 1 && "invalid number of arguments to exit"); + executor.terminateStateEarly(state, "", StateTerminationType::SilentExit); } void SpecialFunctionHandler::handleAssert(ExecutionState &state, KInstruction *target, - std::vector<ref<Expr> > &arguments) { - assert(arguments.size()==3 && "invalid number of arguments to _assert"); - executor.terminateStateOnError(state, - "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - Executor::Assert); + std::vector<ref<Expr>> &arguments) { + assert(arguments.size() == 3 && "invalid number of arguments to _assert"); + executor.terminateStateOnError( + state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), + StateTerminationType::Assert); } -void SpecialFunctionHandler::handleAssertFail(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { - assert(arguments.size()==4 && "invalid number of arguments to __assert_fail"); - executor.terminateStateOnError(state, - "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), - Executor::Assert); +void SpecialFunctionHandler::handleAssertFail( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { + assert(arguments.size() == 4 && + "invalid number of arguments to __assert_fail"); + executor.terminateStateOnError( + state, "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]), + StateTerminationType::Assert); } -void SpecialFunctionHandler::handleReportError(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { - assert(arguments.size()==4 && "invalid number of arguments to klee_report_error"); - - // arguments[0], arguments[1] are file, line - executor.terminateStateOnError(state, - readStringAtAddress(state, arguments[2]), - Executor::ReportError, - readStringAtAddress(state, arguments[3]).c_str()); +void SpecialFunctionHandler::handleReportError( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { + assert(arguments.size() == 4 && + "invalid number of arguments to klee_report_error"); + + // arguments[0,1,2,3] are file, line, message, suffix + executor.terminateStateOnError( + state, readStringAtAddress(state, arguments[2]), + StateTerminationType::ReportError, "", + readStringAtAddress(state, arguments[3]).c_str()); } void SpecialFunctionHandler::handleOpenMerge(ExecutionState &state, @@ -431,9 +432,8 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state, KInstruction *target, std::vector<ref<Expr>> &arguments) { if (arguments.size() != 2) { - executor.terminateStateOnError(state, - "Incorrect number of arguments to memalign(size_t alignment, size_t size)", - Executor::User); + executor.terminateStateOnUserError(state, + "Incorrect number of arguments to memalign(size_t alignment, size_t size)"); return; } @@ -444,9 +444,7 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state, auto alignmentConstExpr = dyn_cast<ConstantExpr>(alignmentExpr); if (!alignmentConstExpr) { - executor.terminateStateOnError(state, - "Could not determine size of symbolic alignment", - Executor::User); + executor.terminateStateOnUserError(state, "Could not determine size of symbolic alignment"); return; } @@ -470,10 +468,8 @@ void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl( "invalid number of arguments to _klee_eh_Unwind_RaiseException_impl"); ref<ConstantExpr> exceptionObject = dyn_cast<ConstantExpr>(arguments[0]); - if (!exceptionObject) { - executor.terminateStateOnError(state, - "Internal error: Symbolic exception pointer", - Executor::Unhandled); + if (!exceptionObject.get()) { + executor.terminateStateOnExecError(state, "Internal error: Symbolic exception pointer"); return; } @@ -520,9 +516,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, if (SilentKleeAssume) { executor.terminateState(state); } else { - executor.terminateStateOnError(state, - "invalid klee_assume call (provably false)", - Executor::User); + executor.terminateStateOnUserError( + state, "invalid klee_assume call (provably false)"); } } else { executor.addConstraint(state, e); @@ -579,9 +574,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { state.forkDisabled = CE->isZero(); } else { - executor.terminateStateOnError(state, - "klee_set_forking requires a constant arg", - Executor::User); + executor.terminateStateOnUserError(state, "klee_set_forking requires a constant arg"); } } @@ -678,8 +671,7 @@ void SpecialFunctionHandler::handleGetErrno(ExecutionState &state, bool resolved = state.addressSpace.resolveOne( ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result); if (!resolved) - executor.terminateStateOnError(state, "Could not resolve address for errno", - Executor::User); + executor.terminateStateOnUserError(state, "Could not resolve address for errno"); executor.bindLocal(target, state, result.second->read(0, Expr::Int32)); } @@ -770,16 +762,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, ref<Expr> address = executor.toUnique(state, arguments[0]); ref<Expr> size = executor.toUnique(state, arguments[1]); if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) { - executor.terminateStateOnError(state, - "check_memory_access requires constant args", - Executor::User); + executor.terminateStateOnUserError(state, "check_memory_access requires constant args"); } else { ObjectPair op; if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) { executor.terminateStateOnError(state, "check_memory_access: memory error", - Executor::Ptr, NULL, + StateTerminationType::Ptr, executor.getAddressInfo(state, address)); } else { ref<Expr> chk = @@ -788,7 +778,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, if (!chk->isTrue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", - Executor::Ptr, NULL, + StateTerminationType::Ptr, executor.getAddressInfo(state, address)); } } @@ -827,7 +817,8 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, std::string name; if (arguments.size() != 3) { - executor.terminateStateOnError(state, "Incorrect number of arguments to klee_make_symbolic(void*, size_t, char*)", Executor::User); + executor.terminateStateOnUserError(state, + "Incorrect number of arguments to klee_make_symbolic(void*, size_t, char*)"); return; } @@ -850,8 +841,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, ExecutionState *s = it->second; if (old->readOnly) { - executor.terminateStateOnError(*s, "cannot make readonly object symbolic", - Executor::User); + executor.terminateStateOnUserError(*s, "cannot make readonly object symbolic"); return; } @@ -868,9 +858,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, if (res) { executor.executeMakeSymbolic(*s, mo, name); } else { - executor.terminateStateOnError(*s, - "wrong size given to klee_make_symbolic[_name]", - Executor::User); + executor.terminateStateOnUserError(*s, "wrong size given to klee_make_symbolic[_name]"); } } } @@ -892,30 +880,30 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, } } -void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { +void SpecialFunctionHandler::handleAddOverflow( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { executor.terminateStateOnError(state, "overflow on addition", - Executor::Overflow); + StateTerminationType::Overflow); } -void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { +void SpecialFunctionHandler::handleSubOverflow( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { executor.terminateStateOnError(state, "overflow on subtraction", - Executor::Overflow); + StateTerminationType::Overflow); } -void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { +void SpecialFunctionHandler::handleMulOverflow( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { executor.terminateStateOnError(state, "overflow on multiplication", - Executor::Overflow); + StateTerminationType::Overflow); } -void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { +void SpecialFunctionHandler::handleDivRemOverflow( + ExecutionState &state, KInstruction *target, + std::vector<ref<Expr>> &arguments) { executor.terminateStateOnError(state, "overflow on division or remainder", - Executor::Overflow); + StateTerminationType::Overflow); } |