diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e3186bbf7a..325e28ab2f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -288,10 +288,12 @@ cl::list ExitOnErrorType( clEnumValN(Executor::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), cl::ZeroOrMore, @@ -441,8 +443,10 @@ const char *Executor::TerminateReasonNames[] = { [ ReadOnly ] = "readonly", [ ReportError ] = "reporterror", [ User ] = "user", +#ifdef SUPPORT_KLEE_EH_CXX [ UncaughtException ] = "uncaught_exception", [ UnexpectedException ] = "unexpected_exception", +#endif [ Unhandled ] = "xxx", }; @@ -1743,10 +1747,12 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, break; } +#ifdef SUPPORT_KLEE_EH_CXX case Intrinsic::eh_typeid_for: { bindLocal(ki, state, getEhTypeidFor(arguments.at(0))); break; } +#endif case Intrinsic::vaend: // va_end is a noop for the interpreter. @@ -2026,6 +2032,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ++state.pc; } +#ifdef SUPPORT_KLEE_EH_CXX if (ri->getFunction()->getName() == "_klee_eh_cxx_personality") { assert(dyn_cast(result) && "result from personality fn must be a concrete value"); @@ -2059,6 +2066,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // never return normally from the personality fn break; } +#endif // SUPPORT_KLEE_EH_CXX if (!isVoidReturn) { Type *t = caller->getType(); @@ -3152,6 +3160,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { terminateStateOnExecError(state, "Unexpected ShuffleVector instruction"); break; +#ifdef SUPPORT_KLEE_EH_CXX case Instruction::Resume: { auto *cui = dyn_cast_or_null( state.unwindingInformation.get()); @@ -3230,6 +3239,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { break; } +#endif // SUPPORT_KLEE_EH_CXX case Instruction::AtomicRMW: terminateStateOnExecError(state, "Unexpected Atomic instruction, should be " diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 1614a0f927..eb3417ae51 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -110,8 +110,10 @@ class Executor : public Interpreter { ReadOnly, ReportError, User, +#ifdef SUPPORT_KLEE_EH_CXX UncaughtException, UnexpectedException, +#endif Unhandled, }; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index f101a085ad..27ca385cee 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -18,6 +18,7 @@ #include "StatsTracker.h" #include "TimingSolver.h" +#include "klee/Config/config.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/Solver/SolverCmdLine.h" @@ -115,7 +116,11 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("malloc", handleMalloc, true), add("memalign", handleMemalign, true), add("realloc", handleRealloc, true), + +#ifdef SUPPORT_KLEE_EH_CXX add("_klee_eh_Unwind_RaiseException_impl", handleEhUnwindRaiseExceptionImpl, false), + add("klee_eh_typeid_for", handleEhTypeid, true), +#endif // operator delete[](void*) add("_ZdaPv", handleDeleteArray, false), @@ -140,7 +145,6 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("__ubsan_handle_sub_overflow", handleSubOverflow, false), add("__ubsan_handle_mul_overflow", handleMulOverflow, false), add("__ubsan_handle_divrem_overflow", handleDivRemOverflow, false), - add("klee_eh_typeid_for", handleEhTypeid, true), #undef addDNR #undef add @@ -458,6 +462,7 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state, alignment); } +#ifdef SUPPORT_KLEE_EH_CXX void SpecialFunctionHandler::handleEhUnwindRaiseExceptionImpl( ExecutionState &state, KInstruction *target, std::vector> &arguments) { @@ -495,6 +500,7 @@ void SpecialFunctionHandler::handleEhTypeid(ExecutionState &state, executor.bindLocal(target, state, executor.getEhTypeidFor(arguments[0])); } +#endif // SUPPORT_KLEE_EH_CXX void SpecialFunctionHandler::handleAssume(ExecutionState &state, KInstruction *target, diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 3db650d7dc..a9f7100d8c 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -10,6 +10,8 @@ #ifndef KLEE_SPECIALFUNCTIONHANDLER_H #define KLEE_SPECIALFUNCTIONHANDLER_H +#include "klee/Config/config.h" + #include #include #include @@ -109,8 +111,12 @@ namespace klee { HANDLER(handleDefineFixedObject); HANDLER(handleDelete); HANDLER(handleDeleteArray); - HANDLER(handleExit); +#ifdef SUPPORT_KLEE_EH_CXX + HANDLER(handleEhUnwindRaiseExceptionImpl); + HANDLER(handleEhTypeid); +#endif HANDLER(handleErrnoLocation); + HANDLER(handleExit); HANDLER(handleFree); HANDLER(handleGetErrno); HANDLER(handleGetObjSize); @@ -119,8 +125,6 @@ namespace klee { HANDLER(handleMakeSymbolic); HANDLER(handleMalloc); HANDLER(handleMemalign); - HANDLER(handleEhUnwindRaiseExceptionImpl); - HANDLER(handleEhTypeid); HANDLER(handleMarkGlobal); HANDLER(handleOpenMerge); HANDLER(handleCloseMerge); diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index cd93b3ec57..eaec772274 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -363,6 +363,9 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { case Intrinsic::dbg_declare: #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) case Intrinsic::dbg_label: +#endif +#ifndef SUPPORT_KLEE_EH_CXX + case Intrinsic::eh_typeid_for: #endif case Intrinsic::exp2: case Intrinsic::exp: @@ -399,10 +402,12 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { dirty = true; break; +#ifdef SUPPORT_KLEE_EH_CXX case Intrinsic::eh_typeid_for: { // Don't lower this, we need it for exception handling break; } +#endif // Warn about any unrecognized intrinsics. default: { diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 7690d3c73d..1bcdedbbc3 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -782,8 +782,10 @@ static const char *modelledExternals[] = { "klee_warning", "klee_warning_once", "klee_stack_trace", +#ifdef SUPPORT_KLEE_EH_CXX "_klee_eh_Unwind_RaiseException_impl", "klee_eh_typeid_for", +#endif "llvm.dbg.declare", "llvm.dbg.value", "llvm.va_start",