aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp122
-rw-r--r--lib/Core/Executor.h29
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp44
3 files changed, 126 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);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-22 22:43:56 +0000