Reach fork optimization

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 {

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;

lib/Core/Executor.cpp

@@ -1062,9 +1062,26 @@ ref<Expr> Executor::maxStaticPctChecks(ExecutionState &current,
   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 &current, ref<Expr> condition,
-                                   bool isInternal, BranchType reason) {
-  PartialValidity res;
+                                   KBlock *ifTrueBlock, KBlock *ifFalseBlock,
+                                   BranchType reason) {
+  bool isInternal = ifTrueBlock == ifFalseBlock;
   std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
       seedMap.find(&current);
   bool isSeeding = it != seedMap.end();
@@ -1076,8 +1093,46 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
   if (isSeeding)
     timeout *= static_cast<unsigned>(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 &current, ref<Expr> condition,
   }
 }
 
+Executor::StatePair Executor::forkInternal(ExecutionState &current,
+                                           ref<Expr> condition,
+                                           BranchType reason) {
+  return fork(current, condition, nullptr, nullptr, reason);
+}
+
 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
   condition =
       Simplificator::simplifyExpr(state.constraints.cs(), condition).simplified;
@@ -2279,8 +2340,7 @@ void Executor::checkNullCheckAfterDeref(ref<Expr> 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<Expr> errorCase = ConstantExpr::alloc(1, Expr::Bool);
     SmallPtrSet<BasicBlock *, 5> 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<Expr> 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<ref<Expr>, BasicBlock *>::iterator
                it = expressionOrder.begin(),
                itE = expressionOrder.end();
            it != itE; ++it) {
         ref<Expr> 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<std::map<BasicBlock *, ref<Expr>>::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<std::map<BasicBlock *, ref<Expr>>::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<Expr> 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<Expr> 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<Expr> 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;

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 &current, 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 &current, ref<Expr> condition, bool isInternal,
-                 BranchType reason);
+  /// if ifTrueBlock == ifFalseBlock, then fork is internal
+  StatePair fork(ExecutionState &current, ref<Expr> condition,
+                 KBlock *ifTrueBlock, KBlock *ifFalseBlock, BranchType reason);
+  StatePair forkInternal(ExecutionState &current, ref<Expr> condition,
+                         BranchType reason);
 
   // If the MaxStatic*Pct limits have been reached, concretize the condition and
   // return it. Otherwise, return the unmodified condition.

lib/Core/Searcher.h

@@ -39,7 +39,6 @@ class DistanceCalculator;
 template <class T, class Comparator> class DiscretePDF;
 template <class T, class Comparator> class WeightedQueue;
 class ExecutionState;
-class Executor;
 class TargetCalculator;
 class TargetForest;
 class TargetReachability;

lib/Core/SpecialFunctionHandler.cpp

@@ -813,16 +813,15 @@ void SpecialFunctionHandler::handleRealloc(ExecutionState &state,
   ref<Expr> address = arguments[0];
   ref<Expr> 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,

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;

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;
+}