[fix] Fix perfomance bug

UnitTestBot · Nov 3, 2023 · 01ddb65 · 01ddb65
1 parent 8b91d6a
commit 01ddb65
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 50 deletions.
diff --git a/include/klee/Expr/Assignment.h b/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
 

diff --git a/include/klee/Solver/SolverUtil.h b/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(); }

diff --git a/lib/Solver/CexCachingSolver.cpp b/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");