diff options
Diffstat (limited to 'lib/Core/SpecialFunctionHandler.cpp')
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 158 |
1 files changed, 73 insertions, 85 deletions
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); } |