diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 122 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 29 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 44 | ||||
| -rw-r--r-- | test/Feature/ExitOnErrorType.c | 15 |
4 files changed, 141 insertions, 69 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index acd02c67..d755403f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -276,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))"), @@ -307,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), @@ -1314,16 +1348,16 @@ 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; } @@ -2516,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: @@ -2897,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(); @@ -2931,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 @@ -2957,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; } @@ -3015,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; } @@ -3175,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()); } } } @@ -3205,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); @@ -3247,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)); } } @@ -3305,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); @@ -3349,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); @@ -3372,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)); } } } @@ -3410,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 { @@ -3426,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]; @@ -3445,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]); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 92edc364..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; @@ -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. diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index caec5e39..b44b0e1b 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -273,7 +273,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, @@ -310,7 +310,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, @@ -319,7 +319,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, @@ -330,6 +330,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()); } @@ -402,7 +403,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); @@ -467,7 +468,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, } else { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", - "user.err"); + Executor::User); } } @@ -623,14 +624,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 = @@ -639,7 +640,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)); } } @@ -700,9 +701,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; } @@ -721,7 +721,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, } else { executor.terminateStateOnError(*s, "wrong size given to klee_make_symbolic[_name]", - "user.err"); + Executor::User); } } } @@ -746,31 +746,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/test/Feature/ExitOnErrorType.c b/test/Feature/ExitOnErrorType.c new file mode 100644 index 00000000..a68a92e0 --- /dev/null +++ b/test/Feature/ExitOnErrorType.c @@ -0,0 +1,15 @@ +// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -exit-on-error-type Assert %t1.bc 2>&1 + +#include <assert.h> +#include <klee/klee.h> + +int main() { + assert(klee_int("assert")); + + while (1) { + } + + return 0; +} |