[fix] Symcretes are updating now for new constraints if they had not …

…been assigned before. Changed behaviour of conretization manager.
S1eGa · Dec 27, 2022 · 975eb21 · 975eb21
1 parent 21c3ddd
commit 975eb21
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -1344,7 +1344,12 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
       klee_warning("seeds patched for violating constraint"); 
   }
 
+  ConstraintSet oldCS = state.constraints;
   state.addConstraint(condition);
+  if (cm->get(state.constraints).bindings.empty()) {
+    cm->add(Query(oldCS, condition), Assignment(true));
+  }
+
   if (ivcEnabled)
     doImpliedValueConcretization(state, condition, 
                                  ConstantExpr::alloc(1, Expr::Bool));
@@ -4866,7 +4871,6 @@ void Executor::executeMemoryOperation(ExecutionState &state,
       }
 
       if (bound) {
-        addConstraint(*bound, inBounds);
         bound->addPointerResolution(base, address, mo);
 
         /* FIXME: same as above. Wasting memory. */
@@ -4900,6 +4904,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
         return;
       }
       if (mayBeOutOfBound) {
+        addConstraint(*unbound, checkOutOfBounds);
         terminateStateOnError(*unbound, "memory error: out of bound pointer",
                               StateTerminationType::Ptr,
                               getAddressInfo(*unbound, address));

diff --git a/lib/Solver/ConcretizationManager.cpp b/lib/Solver/ConcretizationManager.cpp
@@ -48,26 +48,25 @@ void ConcretizationManager::add(const ConstraintSet &oldCS,
   }
   delete independent;
 
-  std::set<ref<Expr>> dependentWithNew;
+  ConstraintSet dependentWithNew;
+  ConstraintManager cm(dependentWithNew);
+
   for (auto i : dependent) {
-    dependentWithNew.insert(i);
+    cm.addConstraint(i);
   }
 
   for (auto i : newCS) {
-    dependentWithNew.insert(i);
+    cm.addConstraint(i);
   }
 
   for (auto i : assign.bindings) {
-    newAssign.bindings.insert(i);
+    newAssign.bindings[i.first] = i.second;
   }
 
-  concretizations.insert(dependentWithNew, newAssign);
+  concretizations.insert(dependentWithNew.asSet(), newAssign);
 }
 
 void ConcretizationManager::add(const Query &q, const Assignment &assign) {
-  std::vector<ref<Expr>> dependent;
-  getIndependentConstraints(q, dependent);
-  ConstraintSet newCS(dependent);
-  newCS.push_back(q.expr);
-  add({}, newCS, assign);
+  ConstraintSet newCS(std::vector<ref<Expr>>{q.expr});
+  add(q.constraints, newCS, assign);
 }
diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp
@@ -110,10 +110,6 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) {
   // symcretes until remove all of them or query starts to evaluate
   // to `mayBeFalse`.
 
-  if (isValid) {
-    cm->add(query, assign);
-  }
-
   if (!isValid) {
     cm->add(query.negateExpr(), assign);
   }