[fix]

UnitTestBot · Nov 10, 2023 · 7e89b7e · 7e89b7e
1 parent b09470c
commit 7e89b7e
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 14 deletions.
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -6506,6 +6506,17 @@ void Executor::updateStateWithSymcretes(ExecutionState &state,
   }
 
   for (const ref<SizeSymcrete> &sizeSymcrete : updatedSizeSymcretes) {
+    auto evaluated = assignment.evaluate(sizeSymcrete->symcretized);
+    if (!isa<ConstantExpr>(evaluated)) {
+      assignment.dump();
+      sizeSymcrete->symcretized->dump();
+      llvm::errs() << "\n";
+      evaluated->dump();
+      llvm::errs() << "\n";
+      klee_error(
+          "Concretization must evaluate symretized expression to constant!\n");
+    }
+
     uint64_t newSize =
         cast<ConstantExpr>(assignment.evaluate(sizeSymcrete->symcretized))
             ->getZExtValue();

diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
@@ -209,7 +209,7 @@ ConstraintSet::ConstraintSet() {}
 void ConstraintSet::addConstraint(ref<Expr> e, const Assignment &delta) {
   _constraints.insert(e);
   // Update bindings
-  for (auto i : delta.bindings) {
+  for (auto &i : delta.bindings) {
     _concretization.bindings.replace({i.first, i.second});
   }
   _independentElements.updateConcretization(delta);
@@ -333,15 +333,15 @@ void PathConstraints::advancePath(KInstruction *ki) { _path.advance(ki); }
 ExprHashSet PathConstraints::addConstraint(ref<Expr> e, const Assignment &delta,
                                            Path::PathIndex currIndex) {
   auto expr = Simplificator::simplifyExpr(constraints, e);
-  if (auto ce = dyn_cast<ConstantExpr>(expr.simplified)) {
+  if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(expr.simplified)) {
     assert(ce->isTrue() && "Attempt to add invalid constraint");
     return {};
   }
   ExprHashSet added;
   std::vector<ref<Expr>> exprs;
   Expr::splitAnds(expr.simplified, exprs);
   for (auto expr : exprs) {
-    if (auto ce = dyn_cast<ConstantExpr>(expr)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(expr)) {
       assert(ce->isTrue() && "Expression simplified to false");
     } else {
       _original.insert(expr);

diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp
@@ -23,13 +23,13 @@ IndependentConstraintSet::updateConcretization(
   if (delta.bindings.size() == 0) {
     return ics;
   }
-  for (auto i : delta.bindings) {
+  for (auto &i : delta.bindings) {
     ics->concretization.bindings.replace({i.first, i.second});
   }
   InnerSetUnion DSU;
   for (ref<Expr> i : exprs) {
     ref<Expr> e = ics->concretization.evaluate(i);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
       assert(ce->isTrue() && "Attempt to add invalid constraint");
       continue;
     }
@@ -39,7 +39,7 @@ IndependentConstraintSet::updateConcretization(
   for (ref<Symcrete> s : symcretes) {
     ref<Expr> e = EqExpr::create(ics->concretization.evaluate(s->symcretized),
                                  s->symcretized);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
       assert(ce->isTrue() && "Attempt to add invalid constraint");
       continue;
     }
@@ -48,7 +48,7 @@ IndependentConstraintSet::updateConcretization(
   auto concretizationConstraints =
       ics->concretization.createConstraintsFromAssignment();
   for (ref<Expr> e : concretizationConstraints) {
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
       assert(ce->isTrue() && "Attempt to add invalid constraint");
       continue;
     }
@@ -65,13 +65,13 @@ IndependentConstraintSet::removeConcretization(
   if (delta.bindings.size() == 0) {
     return ics;
   }
-  for (auto i : delta.bindings) {
+  for (auto &i : delta.bindings) {
     ics->concretization.bindings.remove(i.first);
   }
   InnerSetUnion DSU;
   for (ref<Expr> i : exprs) {
     ref<Expr> e = ics->concretization.evaluate(i);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
       assert(ce->isTrue() && "Attempt to add invalid constraint");
       continue;
     }
@@ -81,7 +81,7 @@ IndependentConstraintSet::removeConcretization(
   for (ref<Symcrete> s : symcretes) {
     ref<Expr> e = EqExpr::create(ics->concretization.evaluate(s->symcretized),
                                  s->symcretized);
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
       assert(ce->isTrue() && "Attempt to add invalid constraint");
       continue;
     }
@@ -90,7 +90,7 @@ IndependentConstraintSet::removeConcretization(
   auto concretizationConstraints =
       ics->concretization.createConstraintsFromAssignment();
   for (ref<Expr> e : concretizationConstraints) {
-    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+    if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
       assert(ce->isTrue() && "Attempt to add invalid constraint");
       continue;
     }
@@ -346,7 +346,7 @@ IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
     InnerSetUnion DSU;
     for (ref<Expr> i : a->exprs) {
       ref<Expr> e = a->concretization.evaluate(i);
-      if (auto ce = dyn_cast<ConstantExpr>(e)) {
+      if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
         assert(ce->isTrue() && "Attempt to add invalid constraint");
         continue;
       }
@@ -355,7 +355,7 @@ IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
     for (ref<Symcrete> s : a->symcretes) {
       ref<Expr> e = EqExpr::create(a->concretization.evaluate(s->symcretized),
                                    s->symcretized);
-      if (auto ce = dyn_cast<ConstantExpr>(e)) {
+      if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
         assert(ce->isTrue() && "Attempt to add invalid constraint");
         continue;
       }
@@ -364,7 +364,7 @@ IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
     auto concretizationConstraints =
         a->concretization.createConstraintsFromAssignment();
     for (ref<Expr> e : concretizationConstraints) {
-      if (auto ce = dyn_cast<ConstantExpr>(e)) {
+      if (ref<ConstantExpr> ce = dyn_cast<ConstantExpr>(e)) {
         assert(ce->isTrue() && "Attempt to add invalid constraint");
         continue;
       }