aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp270
-rw-r--r--lib/Core/Executor.h72
-rw-r--r--lib/Core/MergeHandler.cpp2
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp158
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 &current, 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 &current, 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);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-26 09:52:44 +0000