Add lazy calculation of constraint dsu

UnitTestBot · Nov 15, 2023 · f1c3dc2 · f1c3dc2
1 parent 9f054a9
commit f1c3dc2
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 25 deletions.
diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
@@ -86,7 +86,7 @@ class ConstraintSet {
   constraints_ty _constraints;
   symcretes_ty _symcretes;
   Assignment _concretization;
-  IndependentConstraintSetUnion _independentElements;
+  mutable IndependentConstraintSetUnion _independentElements;
 };
 
 class PathConstraints {

diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h
@@ -12,18 +12,22 @@ class IndependentConstraintSetUnion
                               ExprEitherSymcreteHash, ExprEitherSymcreteCmp> {
 public:
   Assignment concretization;
+  std::vector<ref<ExprEitherSymcrete>> constraintQueue;
+  Assignment updateQueue;
+  Assignment removeQueue;
 
 public:
   ExprHashMap<ref<Expr>> concretizedExprs;
 
 public:
-  void updateConcretization(const Assignment &c);
+  void updateConcretization(const Assignment &delta);
   void removeConcretization(const Assignment &remove);
+  void calculateUpdateConcretizationQueue();
+  void calculateRemoveConcretizationQueue();
   void reEvaluateConcretization(const Assignment &newConcretization);
 
-  IndependentConstraintSetUnion getConcretizedVersion() const;
-  IndependentConstraintSetUnion
-  getConcretizedVersion(const Assignment &c) const;
+  IndependentConstraintSetUnion getConcretizedVersion();
+  IndependentConstraintSetUnion getConcretizedVersion(const Assignment &c);
 
   IndependentConstraintSetUnion();
   IndependentConstraintSetUnion(const constraints_ty &is,
@@ -35,14 +39,13 @@ class IndependentConstraintSetUnion
   addIndependentConstraintSetUnion(const IndependentConstraintSetUnion &icsu);
 
   void getAllDependentConstraintSets(
-      ref<Expr> e,
-      std::vector<ref<const IndependentConstraintSet>> &result) const;
+      ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result);
   void getAllIndependentConstraintSets(
-      ref<Expr> e,
-      std::vector<ref<const IndependentConstraintSet>> &result) const;
+      ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result);
 
   void addExpr(ref<Expr> e);
   void addSymcrete(ref<Symcrete> s);
+  void calculateQueue();
 };
 } // namespace klee
 

diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp
@@ -49,32 +49,50 @@ void IndependentConstraintSetUnion::addIndependentConstraintSetUnion(
     const IndependentConstraintSetUnion &icsu) {
   add(icsu);
   concretization.addIndependentAssignment(icsu.concretization);
+  updateQueue.addIndependentAssignment(icsu.updateQueue);
+  removeQueue.addIndependentAssignment(icsu.removeQueue);
+  constraintQueue.insert(constraintQueue.begin(), icsu.constraintQueue.begin(),
+                         icsu.constraintQueue.end());
 }
 
-void IndependentConstraintSetUnion::updateConcretization(
-    const Assignment &delta) {
+void IndependentConstraintSetUnion::updateConcretization(const Assignment &delta) {
+  for (auto &it : delta.bindings) {
+    updateQueue.bindings.replace({it.first, it.second});
+    removeQueue.bindings.remove(it.first);
+  }
+}
+
+void IndependentConstraintSetUnion::removeConcretization(const Assignment &remove) {
+  for (auto &it : remove.bindings) {
+    removeQueue.bindings.replace({it.first, it.second});
+    updateQueue.bindings.remove(it.first);
+  }
+}
+
+void IndependentConstraintSetUnion::calculateUpdateConcretizationQueue() {
   for (auto &e : roots) {
     ref<const IndependentConstraintSet> ics = disjointSets.at(e);
-    Assignment part = delta.part(ics->getSymcretes());
+    Assignment part = updateQueue.part(ics->getSymcretes());
     ics = ics->updateConcretization(part, concretizedExprs);
     disjointSets.insert_or_assign(e, ics);
   }
-  for (auto &it : delta.bindings) {
+  for (auto &it : updateQueue.bindings) {
     concretization.bindings.replace({it.first, it.second});
   }
+  updateQueue.bindings = Assignment::bindings_ty();
 }
 
-void IndependentConstraintSetUnion::removeConcretization(
-    const Assignment &remove) {
+void IndependentConstraintSetUnion::calculateRemoveConcretizationQueue() {
   for (auto &e : roots) {
     ref<const IndependentConstraintSet> ics = disjointSets.at(e);
-    Assignment part = remove.part(ics->getSymcretes());
+    Assignment part = removeQueue.part(ics->getSymcretes());
     ics = ics->removeConcretization(part, concretizedExprs);
     disjointSets.insert_or_assign(e, ics);
   }
-  for (auto &it : remove.bindings) {
+  for (auto &it : removeQueue.bindings) {
     concretization.bindings.remove(it.first);
   }
+  removeQueue.bindings = Assignment::bindings_ty();
 }
 
 void IndependentConstraintSetUnion::reEvaluateConcretization(
@@ -93,8 +111,8 @@ void IndependentConstraintSetUnion::reEvaluateConcretization(
 }
 
 void IndependentConstraintSetUnion::getAllIndependentConstraintSets(
-    ref<Expr> e,
-    std::vector<ref<const IndependentConstraintSet>> &result) const {
+    ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result) {
+  calculateQueue();
   ref<const IndependentConstraintSet> compare =
       new IndependentConstraintSet(new ExprEitherSymcrete::left(e));
   for (auto &r : roots) {
@@ -106,8 +124,8 @@ void IndependentConstraintSetUnion::getAllIndependentConstraintSets(
 }
 
 void IndependentConstraintSetUnion::getAllDependentConstraintSets(
-    ref<Expr> e,
-    std::vector<ref<const IndependentConstraintSet>> &result) const {
+    ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result) {
+  calculateQueue();
   ref<const IndependentConstraintSet> compare =
       new IndependentConstraintSet(new ExprEitherSymcrete::left(e));
   for (auto &r : roots) {
@@ -119,15 +137,16 @@ void IndependentConstraintSetUnion::getAllDependentConstraintSets(
 }
 
 void IndependentConstraintSetUnion::addExpr(ref<Expr> e) {
-  addValue(new ExprEitherSymcrete::left(e));
+  constraintQueue.push_back(new ExprEitherSymcrete::left(e));
 }
 
 void IndependentConstraintSetUnion::addSymcrete(ref<Symcrete> s) {
-  addValue(new ExprEitherSymcrete::right(s));
+  constraintQueue.push_back(new ExprEitherSymcrete::right(s));
 }
 
 IndependentConstraintSetUnion
-IndependentConstraintSetUnion::getConcretizedVersion() const {
+IndependentConstraintSetUnion::getConcretizedVersion() {
+  calculateQueue();
   IndependentConstraintSetUnion icsu;
   for (auto &i : roots) {
     ref<const IndependentConstraintSet> root = disjointSets.at(i);
@@ -141,14 +160,26 @@ IndependentConstraintSetUnion::getConcretizedVersion() const {
     icsu.concretization.addIndependentAssignment(root->concretization);
   }
   icsu.concretizedExprs = concretizedExprs;
+  icsu.calculateQueue();
   return icsu;
 }
 
 IndependentConstraintSetUnion
 IndependentConstraintSetUnion::getConcretizedVersion(
-    const Assignment &newConcretization) const {
+    const Assignment &newConcretization) {
+  calculateQueue();
   IndependentConstraintSetUnion icsu = *this;
   icsu.reEvaluateConcretization(newConcretization);
+  icsu.calculateQueue();
   return icsu.getConcretizedVersion();
 }
+
+void IndependentConstraintSetUnion::calculateQueue() {
+  while (!constraintQueue.empty()) {
+    addValue(constraintQueue[constraintQueue.size() - 1]);
+    constraintQueue.pop_back();
+  }
+  calculateUpdateConcretizationQueue();
+  calculateRemoveConcretizationQueue();
+}
 } // namespace klee