Fix several bugs

include/klee/Expr/Assignment.h

@@ -25,6 +25,7 @@ class ConstraintSet;
 
 typedef std::set<ref<Symcrete>, SymcreteLess> SymcreteOrderedSet;
 using symcretes_ty = SymcreteOrderedSet;
+typedef std::function<bool(ref<Expr>)> ExprPredicate;
 
 class Assignment {
 public:
@@ -57,11 +58,14 @@ class Assignment {
   ref<Expr> evaluate(ref<Expr> e, bool allowFreeValues = true) const;
   constraints_ty createConstraintsFromAssignment() const;
 
+  template <typename InputIterator>
+  bool satisfies(InputIterator begin, InputIterator end,
+                 ExprPredicate predicate, bool allowFreeValues = true);
   template <typename InputIterator>
   bool satisfies(InputIterator begin, InputIterator end,
                  bool allowFreeValues = true);
   template <typename InputIterator>
-  bool satisfiesNonBoolean(InputIterator begin, InputIterator end,
+  bool satisfiesOrConstant(InputIterator begin, InputIterator end,
                            bool allowFreeValues = true);
   void dump() const;
 
@@ -115,28 +119,43 @@ inline ref<Expr> Assignment::evaluate(ref<Expr> e, bool allowFreeValues) const {
   return v.visit(e);
 }
 
+struct isTrueBoolean {
+  bool operator()(ref<Expr> e) const {
+    return e->getWidth() == Expr::Bool && e->isTrue();
+  }
+};
+
+struct isTrueBooleanOrConstantNotBoolean {
+  bool operator()(ref<Expr> e) const {
+    return (e->getWidth() == Expr::Bool && e->isTrue()) ||
+           ((isa<ConstantExpr>(e) && e->getWidth() != Expr::Bool));
+  }
+};
+
 template <typename InputIterator>
 inline bool Assignment::satisfies(InputIterator begin, InputIterator end,
+                                  ExprPredicate predicate,
                                   bool allowFreeValues) {
   AssignmentEvaluator v(*this, allowFreeValues);
   for (; begin != end; ++begin) {
-    assert((*begin)->getWidth() == Expr::Bool && "constraints must be boolean");
-    if (!v.visit(*begin)->isTrue())
+    if (!predicate(v.visit(*begin)))
       return false;
   }
   return true;
 }
 
 template <typename InputIterator>
-inline bool Assignment::satisfiesNonBoolean(InputIterator begin,
+inline bool Assignment::satisfies(InputIterator begin, InputIterator end,
+                                  bool allowFreeValues) {
+  return satisfies(begin, end, isTrueBoolean(), allowFreeValues);
+}
+
+template <typename InputIterator>
+inline bool Assignment::satisfiesOrConstant(InputIterator begin,
                                             InputIterator end,
                                             bool allowFreeValues) {
-  AssignmentEvaluator v(*this, allowFreeValues);
-  for (; begin != end; ++begin) {
-    if (!isa<ConstantExpr>(v.visit(*begin)))
-      return false;
-  }
-  return true;
+  return satisfies(begin, end, isTrueBooleanOrConstantNotBoolean(),
+                   allowFreeValues);
 }
 } // namespace klee
 

include/klee/Solver/SolverUtil.h

@@ -299,26 +299,12 @@ class InvalidResponse : public SolverResponse {
   }
 
   bool satisfies(const std::set<ref<Expr>> &key, bool allowFreeValues = true) {
-    std::set<ref<Expr>> booleanKey;
-    std::set<ref<Expr>> nonBooleanKey;
-
-    for (auto i : key) {
-      if (i->getWidth() == Expr::Bool) {
-        booleanKey.insert(i);
-      } else {
-        nonBooleanKey.insert(i);
-      }
-    }
-
-    return result.satisfies(booleanKey.begin(), booleanKey.end(),
-                            allowFreeValues) &&
-           result.satisfiesNonBoolean(nonBooleanKey.begin(),
-                                      nonBooleanKey.end(), allowFreeValues);
+    return result.satisfies(key.begin(), key.end(), allowFreeValues);
   }
 
-  bool satisfiesNonBoolean(const std::set<ref<Expr>> &key,
+  bool satisfiesOrConstant(const std::set<ref<Expr>> &key,
                            bool allowFreeValues = true) {
-    return result.satisfiesNonBoolean(key.begin(), key.end(), allowFreeValues);
+    return result.satisfiesOrConstant(key.begin(), key.end(), allowFreeValues);
   }
 
   void dump() { result.dump(); }

lib/Core/ExecutionState.h

@@ -509,9 +509,9 @@ class ExecutionState {
   }
 
   inline bool isStuck(unsigned long long bound) const {
-    if (depth == 1)
+    if (depth == 0)
       return false;
-    return isCycled(bound) && depth > klee::util::ulog2(bound);
+    return isCycled(bound) && klee::util::ulog2(depth) > bound;
   }
 
   bool isCoveredNew() const {

lib/Core/Executor.cpp

@@ -4415,7 +4415,7 @@ void Executor::executeStep(ExecutionState &state) {
   if (targetManager->isTargeted(state) && state.targets().empty()) {
     terminateStateEarlyAlgorithm(state, "State missed all it's targets.",
                                  StateTerminationType::MissedAllTargets);
-  } else if (state.isStuck(MaxCycles)) {
+  } else if (state.isCycled(MaxCycles)) {
     terminateStateEarly(state, "max-cycles exceeded.",
                         StateTerminationType::MaxCycles);
   } else {
@@ -7167,7 +7167,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
   // also make understanding individual test cases much easier.
   const size_t cexPreferencesBound = 16;
   if (state.cexPreferences.size() > cexPreferencesBound) {
-    klee_warning_once(0, "skipping cex preffering (size of restrictons > %d).",
+    klee_warning_once(0, "skipping cex preffering (size of restrictons > %zu).",
                       cexPreferencesBound);
   } else {
     for (auto &pi : state.cexPreferences) {

lib/Core/TargetCalculator.cpp

@@ -92,8 +92,7 @@ void TargetCalculator::update(const ExecutionState &state) {
             }
             if (!fnsTaken.count(calledKFunction) &&
                 fullyCoveredFunctions.count(calledKFunction) == 0 &&
-                calledKFunction->numInstructions != 0 &&
-                !getCoverageTargets(calledKFunction).empty()) {
+                calledKFunction->numInstructions != 0) {
               fns.push_back(calledKFunction);
             }
           }

lib/Core/TargetManager.cpp

@@ -135,7 +135,7 @@ void TargetManager::updateReached(ExecutionState &state) {
 
 void TargetManager::updateTargets(ExecutionState &state) {
   if (guidance == Interpreter::GuidanceKind::CoverageGuidance) {
-    if (targets(state).empty() && state.isCycled(MaxCyclesBeforeStuck)) {
+    if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) {
       state.setTargeted(true);
     }
     if (isTargeted(state) && targets(state).empty()) {

lib/Solver/CexCachingSolver.cpp

@@ -169,25 +169,14 @@ bool CexCachingSolver::searchForResponse(KeyType &key,
       return true;
     }
 
-    KeyType booleanKey;
-    KeyType nonBooleanKey;
-    for (auto i : key) {
-      if (i->getWidth() == Expr::Bool) {
-        booleanKey.insert(i);
-      } else {
-        nonBooleanKey.insert(i);
-      }
-    }
-
     // Otherwise, iterate through the set of current solver responses to see if
     // one of them satisfies the query.
     for (responseTable_ty::iterator it = responseTable.begin(),
                                     ie = responseTable.end();
          it != ie; ++it) {
       ref<SolverResponse> a = *it;
       if (isa<InvalidResponse>(a) &&
-          cast<InvalidResponse>(a)->satisfies(booleanKey) &&
-          cast<InvalidResponse>(a)->satisfiesNonBoolean(nonBooleanKey)) {
+          cast<InvalidResponse>(a)->satisfiesOrConstant(key)) {
         result = a;
         return true;
       }
@@ -272,17 +261,7 @@ bool CexCachingSolver::getResponse(const Query &query,
     }
 
     if (DebugCexCacheCheckBinding) {
-      KeyType booleanKey;
-      KeyType nonBooleanKey;
-      for (auto i : key) {
-        if (i->getWidth() == Expr::Bool) {
-          booleanKey.insert(i);
-        } else {
-          nonBooleanKey.insert(i);
-        }
-      }
-      if (!cast<InvalidResponse>(result)->satisfies(booleanKey) ||
-          !cast<InvalidResponse>(result)->satisfiesNonBoolean(nonBooleanKey)) {
+      if (!cast<InvalidResponse>(result)->satisfiesOrConstant(key)) {
         query.dump();
         result->dump();
         klee_error("Generated assignment doesn't match query");