diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 96e6507dfa..e865de6a31 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -42,7 +42,8 @@ MARK(EXECERR, 26U) \ TTYPE(Replay, 27U, "") \ TTYPE(SilentExit, 28U, "") \ - MARK(END, 28U) + TTYPE(MissedAllTargets, 29U, "") \ + MARK(END, 29U) ///@brief Reason an ExecutionState got terminated. enum class StateTerminationType : std::uint8_t { diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h index fd43f27023..92fdd3c424 100644 --- a/include/klee/Module/Target.h +++ b/include/klee/Module/Target.h @@ -96,6 +96,11 @@ struct Target { bool isTheSameAsIn(KInstruction *instr) const; + /// returns true if we cannot use CFG reachability checks + /// from instr children to this target + /// to avoid solver calls + bool mustVisitForkBranches(KInstruction *instr) const; + unsigned getId() const { return id; } std::string toString() const; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2e8d475edf..2fd22d3e67 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1062,9 +1062,26 @@ ref Executor::maxStaticPctChecks(ExecutionState ¤t, return condition; } +bool Executor::canReachSomeTargetFromBlock(ExecutionState &es, KBlock *block) { + if (interpreterOpts.Guidance != GuidanceKind::ErrorGuidance) + return true; + auto nextInstr = block->getFirstInstruction(); + for (const auto &p : *es.targetForest.getTargets()) { + auto target = p.first; + if (target->mustVisitForkBranches(es.prevPC)) + return true; + auto dist = distanceCalculator->getDistance(nextInstr, es.prevPC, es.initPC, + es.stack, es.error, target); + if (dist.result != WeightResult::Miss) + return true; + } + return false; +} + Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, - bool isInternal, BranchType reason) { - PartialValidity res; + KBlock *ifTrueBlock, KBlock *ifFalseBlock, + BranchType reason) { + bool isInternal = ifTrueBlock == ifFalseBlock; std::map>::iterator it = seedMap.find(¤t); bool isSeeding = it != seedMap.end(); @@ -1076,8 +1093,46 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, if (isSeeding) timeout *= static_cast(it->second.size()); solver->setTimeout(timeout); - bool success = solver->evaluate(current.constraints.cs(), condition, res, - current.queryMetaData); + + bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true; + if (!isInternal) { + shouldCheckTrueBlock = canReachSomeTargetFromBlock(current, ifTrueBlock); + shouldCheckFalseBlock = canReachSomeTargetFromBlock(current, ifFalseBlock); + } + PartialValidity res = PartialValidity::None; + bool terminateEverything = false, success = false; + if (!shouldCheckTrueBlock) { + assert(shouldCheckFalseBlock && + "current state cannot reach any targets itself!"); + // only solver->check-sat(!condition) + bool mayBeFalse; + success = solver->mayBeFalse(current.constraints.cs(), condition, + mayBeFalse, current.queryMetaData); + if (success && !mayBeFalse) + terminateEverything = true; + else + res = PartialValidity::MayBeFalse; + } else if (!shouldCheckFalseBlock) { + // only solver->check-sat(condition) + bool mayBeTrue; + success = solver->mayBeTrue(current.constraints.cs(), condition, mayBeTrue, + current.queryMetaData); + if (success && !mayBeTrue) + terminateEverything = true; + else + res = PartialValidity::MayBeTrue; + } + if (terminateEverything) { + current.pc = current.prevPC; + terminateStateEarly(current, "State missed all it's targets.", + StateTerminationType::MissedAllTargets); + return StatePair(nullptr, nullptr); + } + if (res != PartialValidity::None) + success = true; + else + success = solver->evaluate(current.constraints.cs(), condition, res, + current.queryMetaData); solver->setTimeout(time::Span()); if (!success) { current.pc = current.prevPC; @@ -1266,6 +1321,12 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, } } +Executor::StatePair Executor::forkInternal(ExecutionState ¤t, + ref condition, + BranchType reason) { + return fork(current, condition, nullptr, nullptr, reason); +} + void Executor::addConstraint(ExecutionState &state, ref condition) { condition = Simplificator::simplifyExpr(state.constraints.cs(), condition).simplified; @@ -2279,8 +2340,7 @@ void Executor::checkNullCheckAfterDeref(ref cond, ExecutionState &state, void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Instruction *i = ki->inst; - if (guidanceKind == GuidanceKind::ErrorGuidance && - state.prevPC->inst->isTerminator()) { + if (guidanceKind == GuidanceKind::ErrorGuidance) { for (auto kvp : state.targetForest) { auto target = kvp.first; if (target->isThatError(ReachWithError::Reachable) && @@ -2415,8 +2475,12 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { cond = optimizer.optimizeExpr(cond, false); + KFunction *kf = state.stack.back().kf; + auto ifTrueBlock = kf->blockMap[bi->getSuccessor(0)]; + auto ifFalseBlock = kf->blockMap[bi->getSuccessor(1)]; Executor::StatePair branches = - fork(state, cond, false, BranchType::ConditionalBranch); + fork(state, cond, ifTrueBlock, ifFalseBlock, + BranchType::ConditionalBranch); // NOTE: There is a hidden dependency here, markBranchVisited // requires that we still be in the context of the branch @@ -2461,12 +2525,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref errorCase = ConstantExpr::alloc(1, Expr::Bool); SmallPtrSet destinations; + KFunction *kf = state.stack.back().kf; // collect and check destinations from label list for (unsigned k = 0; k < numDestinations; ++k) { // filter duplicates const auto d = bi->getDestination(k); if (destinations.count(d)) continue; + if (!canReachSomeTargetFromBlock(state, kf->blockMap[d])) + continue; destinations.insert(d); // create address expression @@ -2553,12 +2620,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Track default branch values ref defaultValue = ConstantExpr::alloc(1, Expr::Bool); + KFunction *kf = state.stack.back().kf; + // iterate through all non-default cases but in order of the expressions for (std::map, BasicBlock *>::iterator it = expressionOrder.begin(), itE = expressionOrder.end(); it != itE; ++it) { ref match = EqExpr::create(cond, it->first); + BasicBlock *caseSuccessor = it->second; // skip if case has same successor basic block as default case // (should work even with phi nodes as a switch is a single terminating @@ -2569,6 +2639,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Make sure that the default value does not contain this target's value defaultValue = AndExpr::create(defaultValue, Expr::createIsZero(match)); + if (!canReachSomeTargetFromBlock(state, kf->blockMap[caseSuccessor])) + continue; + // Check if control flow could take this case bool result; match = optimizer.optimizeExpr(match, false); @@ -2577,8 +2650,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { assert(success && "FIXME: Unhandled solver failure"); (void)success; if (result) { - BasicBlock *caseSuccessor = it->second; - // Handle the case that a basic block might be the target of multiple // switch cases. // Currently we generate an expression containing all switch-case @@ -2598,19 +2669,21 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } } - // Check if control could take the default case - defaultValue = optimizer.optimizeExpr(defaultValue, false); - bool res; - bool success = solver->mayBeTrue(state.constraints.cs(), defaultValue, - res, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res) { - std::pair>::iterator, bool> ret = - branchTargets.insert( - std::make_pair(si->getDefaultDest(), defaultValue)); - if (ret.second) { - bbOrder.push_back(si->getDefaultDest()); + auto defaultDest = si->getDefaultDest(); + if (canReachSomeTargetFromBlock(state, kf->blockMap[defaultDest])) { + // Check if control could take the default case + defaultValue = optimizer.optimizeExpr(defaultValue, false); + bool res; + bool success = solver->mayBeTrue(state.constraints.cs(), defaultValue, + res, state.queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); + (void)success; + if (res) { + std::pair>::iterator, bool> ret = + branchTargets.insert(std::make_pair(defaultDest, defaultValue)); + if (ret.second) { + bbOrder.push_back(defaultDest); + } } } @@ -2741,7 +2814,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { assert(success && "FIXME: Unhandled solver failure"); (void)success; StatePair res = - fork(*free, EqExpr::create(v, value), true, BranchType::Call); + forkInternal(*free, EqExpr::create(v, value), BranchType::Call); if (res.first) { uint64_t addr = value->getZExtValue(); auto it = legalFunctions.find(addr); @@ -4899,7 +4972,7 @@ void Executor::executeFree(ExecutionState &state, ref address, KInstruction *target) { address = optimizer.optimizeExpr(address, true); StatePair zeroPointer = - fork(state, Expr::createIsZero(address), true, BranchType::Free); + forkInternal(state, Expr::createIsZero(address), BranchType::Free); if (zeroPointer.first) { if (target) bindLocal(target, *zeroPointer.first, Expr::createPointer(0)); @@ -4963,7 +5036,7 @@ bool Executor::resolveExact(ExecutionState &estate, ref address, uniqueBase = toUnique(estate, uniqueBase); StatePair branches = - fork(estate, Expr::createIsZero(base), true, BranchType::MemOp); + forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp); ExecutionState *bound = branches.first; if (bound) { if (!isReadFromSymbolicArray(uniqueBase) || @@ -5001,7 +5074,7 @@ bool Executor::resolveExact(ExecutionState &estate, ref address, inBounds = EqExpr::create(address, mo->getBaseExpr()); } StatePair branches = - fork(*unbound, inBounds, true, BranchType::ResolvePointer); + forkInternal(*unbound, inBounds, BranchType::ResolvePointer); if (branches.first) results.push_back(std::make_pair(rl.at(i), branches.first)); @@ -5600,7 +5673,7 @@ void Executor::executeMemoryOperation( uniqueBase = toUnique(estate, uniqueBase); StatePair branches = - fork(estate, Expr::createIsZero(base), true, BranchType::MemOp); + forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp); ExecutionState *bound = branches.first; if (bound) { if (!isReadFromSymbolicArray(uniqueBase) || @@ -5791,8 +5864,9 @@ void Executor::executeMemoryOperation( ObjectState *wos = state->addressSpace.getWriteable(mo, os); if (wos->readOnly) { - branches = fork(*state, Expr::createIsZero(unboundConditions[i]), - true, BranchType::MemOp); + branches = + forkInternal(*state, Expr::createIsZero(unboundConditions[i]), + BranchType::MemOp); assert(branches.first); terminateStateOnError(*branches.first, "memory error: object read only", @@ -6304,11 +6378,11 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, prepareTargetedExecution(initialState, whitelist); states.push_back(initialState); } - } else { - ExecutionState *initialState = state->copy(); - states.push_back(initialState); delete state; + } else { + states.push_back(state); } + state = nullptr; TreeOStream pathOS; TreeOStream symPathOS; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index b12e5e7f62..0fe7a1f0d7 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -414,6 +414,10 @@ class Executor : public Interpreter { void updateStateWithSymcretes(ExecutionState &state, const Assignment &assignment); + /// Assume that `current` state stepped to `block`. + /// Can we reach at least one target of `current` from there? + bool canReachSomeTargetFromBlock(ExecutionState ¤t, KBlock *block); + /// Create a new state where each input condition has been added as /// a constraint and return the results. The input state is included /// as one of the results. Note that the output vector may include @@ -424,8 +428,11 @@ class Executor : public Interpreter { /// Fork current and return states in which condition holds / does /// not hold, respectively. One of the states is necessarily the /// current state, and one of the states may be null. - StatePair fork(ExecutionState ¤t, ref condition, bool isInternal, - BranchType reason); + /// if ifTrueBlock == ifFalseBlock, then fork is internal + StatePair fork(ExecutionState ¤t, ref condition, + KBlock *ifTrueBlock, KBlock *ifFalseBlock, BranchType reason); + StatePair forkInternal(ExecutionState ¤t, ref condition, + BranchType reason); // If the MaxStatic*Pct limits have been reached, concretize the condition and // return it. Otherwise, return the unmodified condition. diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index ee85de1d58..4302977607 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -39,7 +39,6 @@ class DistanceCalculator; template class DiscretePDF; template class WeightedQueue; class ExecutionState; -class Executor; class TargetCalculator; class TargetForest; class TargetReachability; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 1a77e09687..0ecb4e2fa2 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -813,16 +813,15 @@ void SpecialFunctionHandler::handleRealloc(ExecutionState &state, ref address = arguments[0]; ref size = arguments[1]; - Executor::StatePair zeroSize = - executor.fork(state, Expr::createIsZero(size), true, BranchType::Realloc); + Executor::StatePair zeroSize = executor.forkInternal( + state, Expr::createIsZero(size), BranchType::Realloc); if (zeroSize.first) { // size == 0 executor.executeFree(*zeroSize.first, address, target); } if (zeroSize.second) { // size != 0 - Executor::StatePair zeroPointer = - executor.fork(*zeroSize.second, Expr::createIsZero(address), true, - BranchType::Realloc); + Executor::StatePair zeroPointer = executor.forkInternal( + *zeroSize.second, Expr::createIsZero(address), BranchType::Realloc); if (zeroPointer.first) { // address == 0 executor.executeAlloc(*zeroPointer.first, size, false, target, diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp index 08b7feca25..99673cfcdb 100644 --- a/lib/Module/Target.cpp +++ b/lib/Module/Target.cpp @@ -79,6 +79,15 @@ bool Target::isTheSameAsIn(KInstruction *instr) const { instr->info->column <= *errLoc.endColumn)); } +bool Target::mustVisitForkBranches(KInstruction *instr) const { + // null check after deref error is checked after fork + // but reachability of this target from instr children + // will always give false, so we need to force visiting + // fork branches here + return isTheSameAsIn(instr) && + isThatError(ReachWithError::NullCheckAfterDerefException); +} + int Target::compare(const Target &other) const { if (errors != other.errors) { return errors < other.errors ? -1 : 1; diff --git a/test/Feature/NotCallingUnreachableBranchesInForkErrorGuided.c b/test/Feature/NotCallingUnreachableBranchesInForkErrorGuided.c new file mode 100644 index 0000000000..784c0151e2 --- /dev/null +++ b/test/Feature/NotCallingUnreachableBranchesInForkErrorGuided.c @@ -0,0 +1,15 @@ +// RUN: %clang %s -emit-llvm -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --analysis-reproduce=%s.json %t1.bc +// RUN: FileCheck -input-file=%t.klee-out/info %s +// CHECK: KLEE: done: total queries = 1 +#include "assert.h" +#include "klee/klee.h" + +int main(int x) { + if (x > 0) { + return 0; + } + x = 42; + return 0; +} diff --git a/test/Feature/NotCallingUnreachableBranchesInForkErrorGuided.c.json b/test/Feature/NotCallingUnreachableBranchesInForkErrorGuided.c.json new file mode 100644 index 0000000000..ec8403ab45 --- /dev/null +++ b/test/Feature/NotCallingUnreachableBranchesInForkErrorGuided.c.json @@ -0,0 +1,65 @@ +{ + "runs": [ + { + "tool": { + "driver": { + "name": "SecB" + } + }, + "results": [ + { + "codeFlows": [ + { + "threadFlows": [ + { + "locations": [ + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "/tmp/NotCallingUnreachableBranchesInForkErrorGuided.c" + }, + "region": { + "startLine": 9, + "startColumn": 14 + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "/tmp/NotCallingUnreachableBranchesInForkErrorGuided.c" + }, + "region": { + "startLine": 13, + "startColumn": 5 + } + } + } + } + ] + } + ] + } + ], + "ruleId": "Reached", + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "/tmp/NotCallingUnreachableBranchesInForkErrorGuided.c" + }, + "region": { + "startLine": 13, + "startColumn": 5 + } + } + } + ] + } + ] + } + ] +} \ No newline at end of file