From 36ee65612f9264eeb2a0255e504112e7e9213a3f Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 11 Apr 2023 19:17:40 +0300 Subject: [PATCH] [feat] Add mocks --- .github/workflows/build.yaml | 2 +- include/klee/Core/TerminationTypes.h | 3 +- lib/Core/ExecutionState.cpp | 4 + lib/Core/Executor.cpp | 430 ++++++++++++++++++--------- lib/Core/Executor.h | 14 +- lib/Core/PForest.cpp | 2 +- lib/Core/Searcher.cpp | 1 + lib/Core/SpecialFunctionHandler.cpp | 32 +- lib/Core/SpecialFunctionHandler.h | 1 + 9 files changed, 332 insertions(+), 157 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 58ad51bafa..b905595881 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -52,7 +52,7 @@ jobs: "Latest klee-uclibc", "Asserts enabled", "No TCMalloc, optimised runtime", - ] + ] include: - name: "LLVM 13" env: diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 7ea2f01ee6..2735c4eb3c 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -33,7 +33,8 @@ TTYPE(ReadOnly, 17U, "read_only.err") \ TTYPE(ReportError, 18U, "report_error.err") \ TTYPE(UndefinedBehavior, 19U, "undefined_behavior.err") \ - MARK(PROGERR, 19U) \ + TTYPE(InternalOutOfMemory, 20U, "out_of_memory.er") \ + MARK(PROGERR, 20U) \ TTYPE(User, 23U, "user.err") \ MARK(USERERR, 23U) \ TTYPE(Execution, 25U, "exec.err") \ diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index ef8def246c..8dcf8b7554 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -87,6 +87,7 @@ ExecutionState::ExecutionState(KFunction *kf) : initPC(kf->instructions), pc(initPC), prevPC(pc), roundingMode(llvm::APFloat::rmNearestTiesToEven) { pushFrame(nullptr, kf); + setID(); } ExecutionState::ExecutionState(KFunction *kf, KBlock *kb) @@ -346,6 +347,7 @@ bool ExecutionState::merge(const ExecutionState &b) { std::set> aConstraints(constraints.begin(), constraints.end()); std::set> bConstraints(b.constraints.begin(), b.constraints.end()); + std::set> commonConstraints, aSuffix, bSuffix; std::set_intersection( aConstraints.begin(), aConstraints.end(), bConstraints.begin(), @@ -357,6 +359,7 @@ bool ExecutionState::merge(const ExecutionState &b) { std::set_difference(bConstraints.begin(), bConstraints.end(), commonConstraints.begin(), commonConstraints.end(), std::inserter(bSuffix, bSuffix.end())); + if (DebugLogStateMerge) { llvm::errs() << "\tconstraint prefix: ["; for (std::set>::iterator it = commonConstraints.begin(), @@ -472,6 +475,7 @@ bool ExecutionState::merge(const ExecutionState &b) { constraints = ConstraintSet(); ConstraintManager m(constraints); + for (const auto &constraint : commonConstraints) m.addConstraint(constraint); m.addConstraint(OrExpr::create(inA, inB)); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 15723c5fce..f553c9b0c0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -160,25 +160,50 @@ cl::opt "Use plain type system from LLVM"), clEnumValN(TypeSystemKind::CXX, "CXX", "Use type system from CXX")), - cl::init(TypeSystemKind::LLVM)); + cl::init(TypeSystemKind::LLVM), cl::cat(ExecCat)); cl::opt UseTBAA("use-tbaa", cl::desc("Turns on restrictions based on types compatibility for " "symbolic pointers (default=false)"), - cl::init(false)); + cl::init(false), cl::cat(ExecCat)); cl::opt AlignSymbolicPointers("align-symbolic-pointers", cl::desc("Makes symbolic pointers aligned according" "to the used type system (default=true)"), - cl::init(true)); + cl::init(true), cl::cat(ExecCat)); cl::opt OutOfMemAllocs("out-of-mem-allocs", cl::desc("Model malloc behavior, i.e. model NULL on 0 " "or huge symbolic allocations."), - cl::init(false)); + cl::init(false), cl::cat(ExecCat)); + +cl::opt + ExternCallsCanReturnNull("extern-calls-can-return-null", cl::init(false), + cl::desc("Enable case when extern call can crash " + "and return null (default=false)"), + cl::cat(ExecCat)); + +enum class MockMutableGlobalsPolicy { + None, + PrimitiveFields, + All, +}; + +cl::opt MockMutableGlobals( + "mock-mutable-globals", + cl::values(clEnumValN(MockMutableGlobalsPolicy::None, "none", + "No mutable global object are allowed o mock except " + "external (default)"), + clEnumValN(MockMutableGlobalsPolicy::PrimitiveFields, + "primitive-fields", + "Only primitive fileds of mutable global objects are " + "allowed to mock."), + clEnumValN(MockMutableGlobalsPolicy::All, "all", + "All mutable global object are allowed o mock.")), + cl::init(MockMutableGlobalsPolicy::None), cl::cat(ExecCat)); } // namespace klee namespace { @@ -201,12 +226,6 @@ cl::opt EmitAllErrors( "(default=false, i.e. one per (error,instruction) pair)"), cl::cat(TestGenCat)); -cl::opt SkipNotLazyAndSymbolicPointers( - "skip-not-lazy-and-symbolic-pointers", cl::init(false), - cl::desc("Set pointers only on lazy and make_symbolic variables " - "(default=false)"), - cl::cat(TestGenCat)); - /* Constraint solving options */ cl::opt MaxSymArraySize( @@ -263,6 +282,18 @@ cl::opt AllExternalWarnings( "as opposed to once per function (default=false)"), cl::cat(ExtCallsCat)); +cl::opt + MockExternalCalls("mock-external-calls", cl::init(false), + cl::desc("If true, failed external calls are mocked, " + "i.e. return values are made symbolic " + "and then added to generated test cases. " + "If false, fails on externall calls."), + cl::cat(ExtCallsCat)); + +cl::opt MockAllExternals("mock-all-externals", cl::init(false), + cl::desc("If true, all externals are mocked."), + cl::cat(ExtCallsCat)); + /*** Seeding options ***/ cl::opt AlwaysOutputSeeds( @@ -854,6 +885,7 @@ void Executor::allocateGlobalObjects(ExecutionState &state) { /*alignment=*/globalObjectAlignment); if (!mo) klee_error("out of memory"); + globalObjects.emplace(&v, mo); globalAddresses.emplace(&v, mo->getBaseConstantExpr()); } @@ -919,12 +951,17 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { } else { addr = externalDispatcher->resolveSymbol(v.getName().str()); } - if (!addr) { + if (MockAllExternals && !addr) { + executeMakeSymbolic( + state, mo, typeSystemManager->getWrappedType(v.getType()), + "mocked_extern", SourceBuilder::irreproducible(), false); + } else if (!addr) { klee_error("Unable to load symbol(%.*s) while initializing globals", static_cast(v.getName().size()), v.getName().data()); - } - for (unsigned offset = 0; offset < mo->size; offset++) { - os->write8(offset, static_cast(addr)[offset]); + } else { + for (unsigned offset = 0; offset < mo->size; offset++) { + os->write8(offset, static_cast(addr)[offset]); + } } } else if (v.hasInitializer()) { initializeGlobalObject(state, os, v.getInitializer(), 0); @@ -2406,6 +2443,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref cond = eval(ki, 0, state).value; cond = optimizer.optimizeExpr(cond, false); + Executor::StatePair branches = fork(state, cond, false, BranchType::ConditionalBranch); @@ -2733,45 +2771,53 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } else { ref v = eval(ki, 0, state).value; - ExecutionState *free = &state; - bool hasInvalid = false, first = true; - - /* XXX This is wasteful, no need to do a full evaluate since we - have already got a value. But in the end the caches should - handle it for us, albeit with some overhead. */ - do { - v = optimizer.optimizeExpr(v, true); - ref value; - bool success = - solver->getValue(free->constraints, v, value, free->queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - StatePair res = - fork(*free, EqExpr::create(v, value), true, BranchType::Call); - if (res.first) { - uint64_t addr = value->getZExtValue(); - auto it = legalFunctions.find(addr); - if (it != legalFunctions.end()) { - f = it->second; - - // Don't give warning on unique resolution - if (res.second || !first) - klee_warning_once(reinterpret_cast(addr), - "resolved symbolic function pointer to: %s", - f->getName().data()); - - executeCall(*res.first, ki, f, arguments); - } else { - if (!hasInvalid) { - terminateStateOnExecError(state, "invalid function pointer"); - hasInvalid = true; + if (!isa(v) && MockExternalCalls) { + if (ki->inst->getType()->isSized()) { + prepareSymbolicValue(state, ki, "mocked_extern", + SourceBuilder::irreproducible()); + } + } else { + ExecutionState *free = &state; + bool hasInvalid = false, first = true; + + /* XXX This is wasteful, no need to do a full evaluate since we + have already got a value. But in the end the caches should + handle it for us, albeit with some overhead. */ + do { + v = optimizer.optimizeExpr(v, true); + ref value; + bool success = solver->getValue(free->constraints, v, value, + free->queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); + (void)success; + StatePair res = + fork(*free, EqExpr::create(v, value), true, BranchType::Call); + if (res.first) { + uint64_t addr = value->getZExtValue(); + auto it = legalFunctions.find(addr); + if (it != legalFunctions.end()) { + f = it->second; + + // Don't give warning on unique resolution + if (res.second || !first) + klee_warning_once(reinterpret_cast(addr), + "resolved symbolic function pointer to: %s", + f->getName().data()); + + executeCall(*res.first, ki, f, arguments); + } else { + if (!hasInvalid) { + terminateStateOnExecError(state, "invalid function pointer"); + hasInvalid = true; + } } } - } - first = false; - free = res.second; - } while (free && !haltExecution); + first = false; + free = res.second; + timers.invoke(); + } while (free && !haltExecution); + } } break; } @@ -4375,11 +4421,12 @@ bool shouldExitOn(StateTerminationType reason) { void Executor::reportStateOnTargetError(ExecutionState &state, ReachWithError error) { if (guidanceKind == GuidanceKind::ErrorGuidance) { - bool reportedTruePositive = - targetedExecutionManager.reportTruePositive(state, error); - if (!reportedTruePositive) { - targetedExecutionManager.reportFalseNegative(state, error); - } + // TODO: uncomment when `targetedExecutionManager` will be added + // bool reportedTruePositive = + // targetedExecutionManager.reportTruePositive(state, error); + // if (!reportedTruePositive) { + // targetedExecutionManager.reportFalseNegative(state, error); + // } } } @@ -4510,6 +4557,29 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, return; } + if (ExternalCalls == ExternalCallPolicy::All && MockAllExternals) { + std::string TmpStr; + llvm::raw_string_ostream os(TmpStr); + os << "calling external: " << callable->getName().str() << "("; + for (unsigned i = 0; i < arguments.size(); i++) { + os << arguments[i]; + if (i != arguments.size() - 1) + os << ", "; + } + os << ") at " << state.pc->getSourceLocation(); + + if (AllExternalWarnings) + klee_warning("%s", os.str().c_str()); + else if (!SuppressExternalWarnings) + klee_warning_once(callable->getValue(), "%s", os.str().c_str()); + + if (target->inst->getType()->isSized()) { + prepareSymbolicValue(state, target, "mocked_extern", + SourceBuilder::irreproducible()); + } + return; + } + // normal external function handling path // allocate 128 bits for each argument (+return value) to support fp80's; // we could iterate through all the arguments first and determine the exact @@ -4634,8 +4704,16 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, roundingMode); if (!success) { - terminateStateOnError(state, "failed external call: " + callable->getName(), - StateTerminationType::External); + if (MockExternalCalls) { + if (target->inst->getType()->isSized()) { + prepareSymbolicValue(state, target, "mocked_extern", + SourceBuilder::irreproducible()); + } + } else { + terminateStateOnError(state, + "failed external call: " + callable->getName(), + StateTerminationType::External); + } return; } @@ -4656,6 +4734,18 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, if (resultType != Type::getVoidTy(kmodule->module->getContext())) { ref e = ConstantExpr::fromMemory((void *)args, getWidthForLLVMType(resultType)); + if (ExternCallsCanReturnNull && + e->getWidth() == Context::get().getPointerWidth()) { + const Array *symExternCallsCanReturnNull = makeArray( + state, Expr::createPointer(1), "symExternCallsCanReturnNull", + SourceBuilder::irreproducible()); + + ref symExternCallsCanReturnNullExpr = + Expr::createTempRead(symExternCallsCanReturnNull, Expr::Bool); + e = SelectExpr::create( + symExternCallsCanReturnNullExpr, + ConstantExpr::alloc(0, Context::get().getPointerWidth()), e); + } bindLocal(target, state, e); } } @@ -4689,6 +4779,16 @@ ref Executor::replaceReadWithSymbolic(ExecutionState &state, return res; } +ref Executor::mockValue(ExecutionState &state, ref result) { + static unsigned id; + const Array *array = makeArray( + state, Expr::createPointer(Expr::getMinBytesForWidth(result->getWidth())), + "mockedGlobalValue" + llvm::utostr(++id), + SourceBuilder::irreproducible()); + result = Expr::createTempRead(array, result->getWidth()); + return result; +} + ObjectState *Executor::bindObjectInState(ExecutionState &state, const MemoryObject *mo, KType *dynamicType, bool isLocal, @@ -4710,7 +4810,7 @@ ObjectState *Executor::bindObjectInState(ExecutionState &state, void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, KInstruction *target, KType *type, bool zeroMemory, const ObjectState *reallocFrom, - size_t allocationAlignment) { + size_t allocationAlignment, bool checkOutOfMemory) { const llvm::Value *allocSite = state.prevPC->inst; if (allocationAlignment == 0) { allocationAlignment = getAllocationAlignment(allocSite); @@ -4737,7 +4837,20 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, } else { os->initializeToRandom(); } - bindLocal(target, *bound, mo->getBaseExpr()); + + ref address = mo->getBaseExpr(); + if (checkOutOfMemory) { + const Array *symCheckOutOfMemory = + makeArray(state, Expr::createPointer(1), "symCheckOutOfMemory", + SourceBuilder::irreproducible()); + + ref symCheckOutOfMemoryExpr = + Expr::createTempRead(symCheckOutOfMemory, Expr::Bool); + address = SelectExpr::create( + symCheckOutOfMemoryExpr, + Expr::createPointer(0), address); + } + bindLocal(target, state, address); if (reallocFrom) { unsigned count = std::min(reallocFrom->size, os->size); @@ -5079,6 +5192,14 @@ void Executor::executeMemoryOperation( if (interpreterOpts.MakeConcreteSymbolic) result = replaceReadWithSymbolic(state, result); + if (MockMutableGlobals != MockMutableGlobalsPolicy::None && + mo->isGlobal && !wos->readOnly && !isa(result) && + (MockMutableGlobals != MockMutableGlobalsPolicy::PrimitiveFields || + !targetType->getRawType()->isPointerTy())) { + result = mockValue(state, result); + wos->write(offset, result); + } + bindLocal(target, state, result); } @@ -5104,90 +5225,105 @@ void Executor::executeMemoryOperation( ResolutionList rl; ResolutionList rlSkipped; - solver->setTimeout(coreSolverTimeout); - bool incomplete = state.addressSpace.resolve( - state, solver, address, targetType, rl, rlSkipped, 0, coreSolverTimeout); - solver->setTimeout(time::Span()); + bool incomplete = false; + ExecutionState *unbound = &state; + ref checkOutOfBounds = ConstantExpr::create(1, Expr::Bool); + if (guidanceKind != GuidanceKind::ErrorGuidance) { + solver->setTimeout(coreSolverTimeout); + incomplete = + state.addressSpace.resolve(state, solver, address, targetType, rl, + rlSkipped, 0, coreSolverTimeout); + solver->setTimeout(time::Span()); - // XXX there is some query wasteage here. who cares? + // XXX there is some query wasteage here. who cares? - ref checkOutOfBounds = ConstantExpr::create(1, Expr::Bool); - ref canLazyInitialize = ConstantExpr::create(1, Expr::Bool); + checkOutOfBounds = ConstantExpr::create(1, Expr::Bool); - std::vector> resolveConditions; - std::vector resolvedMemoryObjects; + std::vector> resolveConditions; + std::vector resolvedMemoryObjects; - for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) { - const MemoryObject *mo = state.addressSpace.findObject(*i).first; - ref inBounds = mo->getBoundsCheckPointer(address, bytes); - ref outOfBound = NotExpr::create(inBounds); - canLazyInitialize = AndExpr::create(outOfBound, canLazyInitialize); - if (state.isGEPExpr(address)) { - inBounds = AndExpr::create(inBounds, mo->getBoundsCheckPointer(base, 1)); - inBounds = - AndExpr::create(inBounds, mo->getBoundsCheckPointer(base, size)); - outOfBound = AndExpr::create(outOfBound, mo->getBoundsCheckPointer(base)); - } + for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) { + const MemoryObject *mo = state.addressSpace.findObject(*i).first; + ref inBounds = mo->getBoundsCheckPointer(address, bytes); + ref outOfBound = NotExpr::create(inBounds); + if (state.isGEPExpr(address)) { + inBounds = + AndExpr::create(inBounds, mo->getBoundsCheckPointer(base, 1)); + inBounds = + AndExpr::create(inBounds, mo->getBoundsCheckPointer(base, size)); + outOfBound = + AndExpr::create(outOfBound, mo->getBoundsCheckPointer(base)); + } - bool mayBeInBounds; - solver->setTimeout(coreSolverTimeout); - bool success = solver->mayBeTrue(state.constraints, inBounds, mayBeInBounds, - state.queryMetaData); - solver->setTimeout(time::Span()); - if (!success) { - terminateStateOnSolverError(state, "Query timed out (resolve)"); - return; - } + bool mayBeInBounds; + solver->setTimeout(coreSolverTimeout); + bool success = solver->mayBeTrue(state.constraints, inBounds, + mayBeInBounds, state.queryMetaData); + solver->setTimeout(time::Span()); + if (!success) { + terminateStateOnSolverError(state, "Query timed out (resolve)"); + return; + } - if (mayBeInBounds) { - resolveConditions.push_back(inBounds); - resolvedMemoryObjects.push_back(mo->id); + if (mayBeInBounds) { + resolveConditions.push_back(inBounds); + resolvedMemoryObjects.push_back(mo->id); + } + checkOutOfBounds = AndExpr::create(outOfBound, checkOutOfBounds); } - checkOutOfBounds = AndExpr::create(outOfBound, checkOutOfBounds); - } - // Fictive condition just to keep state for unbound case. - resolveConditions.push_back(ConstantExpr::create(1, Expr::Bool)); + // Fictive condition just to keep state for unbound case. + resolveConditions.push_back(ConstantExpr::create(1, Expr::Bool)); - std::vector statesForMemoryOperation; - branch(state, resolveConditions, statesForMemoryOperation, BranchType::MemOp); + std::vector statesForMemoryOperation; + branch(state, resolveConditions, statesForMemoryOperation, + BranchType::MemOp); - for (unsigned int i = 0; i < resolvedMemoryObjects.size(); ++i) { - ExecutionState *bound = statesForMemoryOperation[i]; - ObjectPair op = bound->addressSpace.findObject(resolvedMemoryObjects[i]); - const MemoryObject *mo = op.first; - const ObjectState *os = op.second; - - bound->addPointerResolution(base, address, mo); - - /* FIXME: Notice, that here we are creating a new instance of object - for every memory operation in order to handle type changes. This might - waste too much memory as we do now always modify something. To fix this - we can ask memory if we will make anything, and create a copy if - required. */ - ObjectState *wos = bound->addressSpace.getWriteable(mo, os); - - if (isWrite) { - wos->getDynamicType()->handleMemoryAccess( - targetType, mo->getOffsetExpr(address), - ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); - if (wos->readOnly) { - terminateStateOnError(*bound, "memory error: object read only", - StateTerminationType::ReadOnly); + for (unsigned int i = 0; i < resolvedMemoryObjects.size(); ++i) { + ExecutionState *bound = statesForMemoryOperation[i]; + ObjectPair op = bound->addressSpace.findObject(resolvedMemoryObjects[i]); + const MemoryObject *mo = op.first; + const ObjectState *os = op.second; + + bound->addPointerResolution(base, address, mo); + + /* FIXME: Notice, that here we are creating a new instance of object + for every memory operation in order to handle type changes. This might + waste too much memory as we do now always modify something. To fix this + we can ask memory if we will make anything, and create a copy if + required. */ + ObjectState *wos = bound->addressSpace.getWriteable(mo, os); + + if (isWrite) { + wos->getDynamicType()->handleMemoryAccess( + targetType, mo->getOffsetExpr(address), + ConstantExpr::alloc(size, Context::get().getPointerWidth()), true); + if (wos->readOnly) { + terminateStateOnError(*bound, "memory error: object read only", + StateTerminationType::ReadOnly); + } else { + wos->write(mo->getOffsetExpr(address), value); + } } else { - wos->write(mo->getOffsetExpr(address), value); + wos->getDynamicType()->handleMemoryAccess( + targetType, mo->getOffsetExpr(address), + ConstantExpr::alloc(size, Context::get().getPointerWidth()), false); + ref result = wos->read(mo->getOffsetExpr(address), type); + + if (MockMutableGlobals != MockMutableGlobalsPolicy::None && + mo->isGlobal && !wos->readOnly && !isa(result) && + (MockMutableGlobals != MockMutableGlobalsPolicy::PrimitiveFields || + !targetType->getRawType()->isPointerTy())) { + result = mockValue(state, result); + wos->write(mo->getOffsetExpr(address), result); + } + + bindLocal(target, *bound, result); } - } else { - wos->getDynamicType()->handleMemoryAccess( - targetType, mo->getOffsetExpr(address), - ConstantExpr::alloc(size, Context::get().getPointerWidth()), false); - ref result = wos->read(mo->getOffsetExpr(address), type); - bindLocal(target, *bound, result); } + unbound = statesForMemoryOperation.back(); } - ExecutionState *unbound = statesForMemoryOperation.back(); - // XXX should we distinguish out of bounds and overlapped cases? if (unbound) { ref baseUniqueExpr = toUnique(*unbound, base); @@ -5565,6 +5701,7 @@ ExecutionState *Executor::formState(Function *f, int argc, char **argv, /*allocSite=*/state->pc->inst, /*alignment=*/8); if (!arg) klee_error("Could not allocate memory for function arguments"); + ObjectState *os = bindObjectInState( *state, arg, typeSystemManager->getWrappedType(argumentType), false); @@ -5592,13 +5729,13 @@ void Executor::clearMemory() { memory = new MemoryManager(NULL); } -void Executor::prepareSymbolicValue(ExecutionState &state, - KInstruction *target) { +void Executor::prepareSymbolicValue(ExecutionState &state, KInstruction *target, + std::string name, + ref source) { Instruction *allocSite = target->inst; uint64_t size = kmodule->targetData->getTypeStoreSize(allocSite->getType()); uint64_t width = kmodule->targetData->getTypeSizeInBits(allocSite->getType()); - ref result = - makeSymbolicValue(allocSite, state, size, width, "symbolic_value"); + ref result = makeSymbolic(allocSite, state, size, width, name, source); bindLocal(target, state, result); if (isa(allocSite)) { AllocaInst *ai = cast(allocSite); @@ -5636,24 +5773,28 @@ void Executor::prepareSymbolicArgs(ExecutionState &state, KFunction *kf) { } } -ref Executor::makeSymbolicValue(Value *value, ExecutionState &state, - uint64_t size, Expr::Width width, - const std::string &name) { - MemoryObject *mo = memory->allocate(size, true, - /*isGlobal=*/false, value, +ref Executor::makeSymbolic(Value *value, ExecutionState &state, + uint64_t size, Expr::Width width, + const std::string &name, + ref source) { + MemoryObject *mo = memory->allocate(size, true, /*isGlobal=*/false, value, /*allocationAlignment=*/8); - const Array *array = makeArray(state, Expr::createPointer(size), name, - SourceBuilder::symbolicValue()); + const Array *array = + makeArray(state, Expr::createPointer(size), name, source); state.addSymbolic(mo, array, typeSystemManager->getWrappedType(value->getType())); assert(value && "Attempted to make symbolic value from nullptr Value"); - ObjectState *os = bindObjectInState( - state, mo, typeSystemManager->getWrappedType(value->getType()), false, - array); - ref result = os->read(0, width); + ref result = Expr::createTempRead(array, width); return result; } +ref Executor::makeSymbolicValue(Value *value, ExecutionState &state, + uint64_t size, Expr::Width width, + const std::string &name) { + return makeSymbolic(value, state, size, width, name, + SourceBuilder::symbolicValue()); +} + void Executor::runFunctionAsMain(Function *f, int argc, char **argv, char **envp) { if (guidanceKind == GuidanceKind::ErrorGuidance && @@ -5734,7 +5875,7 @@ ExecutionState *Executor::prepareStateForPOSIX(KInstIterator &caller, ExecutionState *state) { Function *mainFn = kmodule->module->getFunction("__klee_posix_wrapped_main"); - assert(mainFn && "klee_posix_wrapped_main not found"); + assert(mainFn && "__klee_posix_wrapped_main not found"); KBlock *target = kmodule->functionMap[mainFn]->entryKBlock; if (pathWriter) @@ -5886,7 +6027,6 @@ void Executor::setInitializationGraph(const ExecutionState &state, continue; } ref constantAddress = cast(addressInModel); - ref mo; IDType idResult; if (state.resolveOnSymbolics(constantAddress, idResult)) { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 00a7e41a0f..56975f73e4 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -318,7 +318,8 @@ class Executor : public Interpreter { void executeAlloc(ExecutionState &state, ref size, bool isLocal, KInstruction *target, KType *type, bool zeroMemory = false, const ObjectState *reallocFrom = 0, - size_t allocationAlignment = 0); + size_t allocationAlignment = 0, + bool checkOutOfMemory = false); /// Free the given address with checking for errors. If target is /// given it will be bound to 0 in the resulting states (this is a @@ -384,6 +385,8 @@ class Executor : public Interpreter { // Used for testing. ref replaceReadWithSymbolic(ExecutionState &state, ref e); + ref mockValue(ExecutionState &state, ref result); + const Cell &eval(KInstruction *ki, unsigned index, ExecutionState &state, bool isSymbolic = true); @@ -584,13 +587,20 @@ class Executor : public Interpreter { void clearMemory(); - void prepareSymbolicValue(ExecutionState &state, KInstruction *targetW); + void prepareSymbolicValue( + ExecutionState &state, KInstruction *targetW, + std::string name = "symbolic_value", + ref source = SourceBuilder::symbolicValue()); void prepareSymbolicRegister(ExecutionState &state, StackFrame &sf, unsigned index); void prepareSymbolicArgs(ExecutionState &state, KFunction *kf); + ref makeSymbolic(llvm::Value *value, ExecutionState &state, + uint64_t size, Expr::Width width, + const std::string &name, ref source); + ref makeSymbolicValue(llvm::Value *value, ExecutionState &state, uint64_t size, Expr::Width width, const std::string &name); diff --git a/lib/Core/PForest.cpp b/lib/Core/PForest.cpp index 8a97410510..d1374f7be4 100644 --- a/lib/Core/PForest.cpp +++ b/lib/Core/PForest.cpp @@ -1,4 +1,4 @@ -//===-- PForest.cpp -------------------------------------------------------===// +//===-- PForest.cpp-------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index cb8abf08f6..bf4deca0dd 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -768,6 +768,7 @@ bool GuidedSearcher::isReached(ref history, ref target) { return reachedTargets.count(target) != 0; } + bool GuidedSearcher::tryAddTarget(ref history, ref target) { if (isReached(history, target)) { diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index a4e3307046..24caa37e49 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -57,6 +57,11 @@ cl::opt "condition given to klee_assume() rather than " "emitting an error (default=false)"), cl::cat(TerminationCat)); + +cl::opt CheckOutOfMemory("check-out-of-memory", cl::init(false), + cl::desc("Enable out-of-memory checking during " + "memory allocation (default=false)"), + cl::cat(ExecCat)); } // namespace /// \todo Almost all of the demands in this file should be replaced @@ -87,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("calloc", handleCalloc, true), add("free", handleFree, false), add("klee_assume", handleAssume, false), + add("klee_sleep", handleSleep, false), add("klee_check_memory_access", handleCheckMemoryAccess, false), add("klee_get_valuef", handleGetValue, true), add("klee_get_valued", handleGetValue, true), @@ -479,7 +485,8 @@ void SpecialFunctionHandler::handleNew(ExecutionState &state, // XXX should type check args assert(arguments.size() == 1 && "invalid number of arguments to new"); executor.executeAlloc(state, arguments[0], false, target, - executor.typeSystemManager->handleAlloc(arguments[0])); + executor.typeSystemManager->handleAlloc(arguments[0]), + false, nullptr, 0, CheckOutOfMemory); } void SpecialFunctionHandler::handleDelete(ExecutionState &state, @@ -499,7 +506,8 @@ void SpecialFunctionHandler::handleNewArray(ExecutionState &state, // XXX should type check args assert(arguments.size() == 1 && "invalid number of arguments to new[]"); executor.executeAlloc(state, arguments[0], false, target, - executor.typeSystemManager->handleAlloc(arguments[0])); + executor.typeSystemManager->handleAlloc(arguments[0]), + false, nullptr, 0, CheckOutOfMemory); } void SpecialFunctionHandler::handleNewNothrowArray( @@ -510,7 +518,8 @@ void SpecialFunctionHandler::handleNewNothrowArray( "invalid number of arguments to new[](unsigned long, std::nothrow_t " "const&)"); executor.executeAlloc(state, arguments[0], false, target, - executor.typeSystemManager->handleAlloc(arguments[0])); + executor.typeSystemManager->handleAlloc(arguments[0]), + false, nullptr, 0, CheckOutOfMemory); } void SpecialFunctionHandler::handleDeleteArray( @@ -527,7 +536,8 @@ void SpecialFunctionHandler::handleMalloc(ExecutionState &state, // XXX should type check args assert(arguments.size() == 1 && "invalid number of arguments to malloc"); executor.executeAlloc(state, arguments[0], false, target, - executor.typeSystemManager->handleAlloc(arguments[0])); + executor.typeSystemManager->handleAlloc(arguments[0]), + false, nullptr, 0, CheckOutOfMemory); } void SpecialFunctionHandler::handleMemalign(ExecutionState &state, @@ -604,6 +614,12 @@ void SpecialFunctionHandler::handleEhTypeid(ExecutionState &state, } #endif // SUPPORT_KLEE_EH_CXX +void SpecialFunctionHandler::handleSleep(ExecutionState &state, + KInstruction *target, + std::vector> &arguments) { + nanosleep((const struct timespec[]){{1, 0}}, NULL); +} + void SpecialFunctionHandler::handleAssume(ExecutionState &state, KInstruction *target, std::vector> &arguments) { @@ -825,7 +841,8 @@ void SpecialFunctionHandler::handleCalloc(ExecutionState &state, ref size = MulExpr::create(arguments[0], arguments[1]); executor.executeAlloc(state, size, false, target, - executor.typeSystemManager->handleAlloc(size), true); + executor.typeSystemManager->handleAlloc(size), true, + nullptr, 0, CheckOutOfMemory); } void SpecialFunctionHandler::handleRealloc(ExecutionState &state, @@ -849,7 +866,8 @@ void SpecialFunctionHandler::handleRealloc(ExecutionState &state, if (zeroPointer.first) { // address == 0 executor.executeAlloc(*zeroPointer.first, size, false, target, - executor.typeSystemManager->handleAlloc(size)); + executor.typeSystemManager->handleAlloc(size), + false, nullptr, 0, CheckOutOfMemory); } if (zeroPointer.second) { // address != 0 Executor::ExactResolutionList rl; @@ -865,7 +883,7 @@ void SpecialFunctionHandler::handleRealloc(ExecutionState &state, executor.executeAlloc(*it->second, size, false, target, executor.typeSystemManager->handleRealloc( os->getDynamicType(), size), - false, os); + false, os, 0, CheckOutOfMemory); } } } diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 6769febe25..10ec81217a 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -103,6 +103,7 @@ class SpecialFunctionHandler { HANDLER(handleAbort); HANDLER(handleAssert); HANDLER(handleAssertFail); + HANDLER(handleSleep); HANDLER(handleAssume); HANDLER(handleCalloc); HANDLER(handleCheckMemoryAccess);