Use FastCexSolver for simple equalities

include/klee/ADT/DisjointSetUnion.h

@@ -150,6 +150,27 @@ class DisjointSetUnion {
     }
   }
 
+  void getAllDependentSets(ValueType value,
+                           std::vector<ref<const SetType>> &result) const {
+    ref<const SetType> compare = new SetType(value);
+    for (auto &r : roots) {
+      ref<const SetType> ics = disjointSets.at(r);
+      if (SetType::intersects(ics, compare)) {
+        result.push_back(ics);
+      }
+    }
+  }
+  void getAllIndependentSets(ValueType value,
+                             std::vector<ref<const SetType>> &result) const {
+    ref<const SetType> compare = new SetType(value);
+    for (auto &r : roots) {
+      ref<const SetType> ics = disjointSets.at(r);
+      if (!SetType::intersects(ics, compare)) {
+        result.push_back(ics);
+      }
+    }
+  }
+
   DisjointSetUnion() {}
 
   DisjointSetUnion(const internalStorage_ty &is) {

include/klee/Expr/ExprRangeEvaluator.h

@@ -13,6 +13,8 @@
 #include "klee/ADT/Bits.h"
 #include "klee/Expr/Expr.h"
 
+#include "llvm/ADT/APInt.h"
+
 namespace klee {
 
 /*
@@ -90,7 +92,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul, T index) {
 template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
   switch (e->getKind()) {
   case Expr::Constant:
-    return T(cast<ConstantExpr>(e));
+    return T(cast<ConstantExpr>(e)->getAPValue());
 
   case Expr::NotOptimized:
     break;
@@ -109,9 +111,9 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     const SelectExpr *se = cast<SelectExpr>(e);
     T cond = evaluate(se->cond);
 
-    if (cond.mustEqual(1)) {
+    if (cond.mustEqual(llvm::APInt(se->cond->getWidth(), 1))) {
       return evaluate(se->trueExpr);
-    } else if (cond.mustEqual(0)) {
+    } else if (cond.mustEqual(llvm::APInt(se->cond->getWidth(), 0))) {
       return evaluate(se->falseExpr);
     } else {
       return evaluate(se->trueExpr).set_union(evaluate(se->falseExpr));
@@ -120,11 +122,9 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
 
     // XXX these should be unrolled to ensure nice inline
   case Expr::Concat: {
-    const Expr *ep = e.get();
-    T res(0);
-    for (unsigned i = 0; i < ep->getNumKids(); i++)
-      res = res.concat(evaluate(ep->getKid(i)), 8);
-    return res;
+    ref<ConcatExpr> ce = cast<ConcatExpr>(e);
+    return evaluate(ce->getLeft())
+        .concat(evaluate(ce->getRight()), ce->getRight()->getWidth());
   }
 
     // Arithmetic
@@ -206,9 +206,9 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     T right = evaluate(be->right);
 
     if (left.mustEqual(right)) {
-      return T(1);
+      return T(llvm::APInt(Expr::Bool, 1));
     } else if (!left.mayEqual(right)) {
-      return T(0);
+      return T(llvm::APInt(Expr::Bool, 0));
     }
     break;
   }
@@ -218,10 +218,10 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     T left = evaluate(be->left);
     T right = evaluate(be->right);
 
-    if (left.max() < right.min()) {
-      return T(1);
-    } else if (left.min() >= right.max()) {
-      return T(0);
+    if (left.max().ult(right.min())) {
+      return T(llvm::APInt(Expr::Bool, 1));
+    } else if (left.min().uge(right.max())) {
+      return T(llvm::APInt(Expr::Bool, 0));
     }
     break;
   }
@@ -230,10 +230,10 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     T left = evaluate(be->left);
     T right = evaluate(be->right);
 
-    if (left.max() <= right.min()) {
-      return T(1);
-    } else if (left.min() > right.max()) {
-      return T(0);
+    if (left.max().ule(right.min())) {
+      return T(llvm::APInt(Expr::Bool, 1));
+    } else if (left.min().ugt(right.max())) {
+      return T(llvm::APInt(Expr::Bool, 0));
     }
     break;
   }
@@ -243,10 +243,10 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     T right = evaluate(be->right);
     unsigned bits = be->left->getWidth();
 
-    if (left.maxSigned(bits) < right.minSigned(bits)) {
-      return T(1);
-    } else if (left.minSigned(bits) >= right.maxSigned(bits)) {
-      return T(0);
+    if (left.maxSigned(bits).ult(right.minSigned(bits))) {
+      return T(llvm::APInt(Expr::Bool, 1));
+    } else if (left.minSigned(bits).uge(right.maxSigned(bits))) {
+      return T(llvm::APInt(Expr::Bool, 0));
     }
     break;
   }
@@ -256,13 +256,21 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     T right = evaluate(be->right);
     unsigned bits = be->left->getWidth();
 
-    if (left.maxSigned(bits) <= right.minSigned(bits)) {
-      return T(1);
-    } else if (left.minSigned(bits) > right.maxSigned(bits)) {
-      return T(0);
+    if (left.maxSigned(bits).ule(right.minSigned(bits))) {
+      return T(llvm::APInt(Expr::Bool, 1));
+    } else if (left.minSigned(bits).ugt(right.maxSigned(bits))) {
+      return T(llvm::APInt(Expr::Bool, 0));
     }
     break;
   }
+  case Expr::ZExt: {
+    ref<CastExpr> ce = cast<CastExpr>(e);
+    return evaluate(e->getKid(0)).zextOrTrunc(ce->getWidth());
+  }
+  case Expr::SExt: {
+    ref<CastExpr> ce = cast<CastExpr>(e);
+    return evaluate(e->getKid(0)).sextOrTrunc(ce->getWidth());
+  }
 
   case Expr::Ne:
   case Expr::Ugt:
@@ -275,7 +283,8 @@ template <class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
     break;
   }
 
-  return T(0, bits64::maxValueOfNBits(e->getWidth()));
+  return T(llvm::APInt(e->getWidth(), 0),
+           llvm::APInt::getAllOnesValue(e->getWidth()));
 }
 
 } // namespace klee

include/klee/Solver/IncompleteSolver.h

@@ -58,14 +58,18 @@ class IncompleteSolver {
 /// StagedSolver - Adapter class for staging an incomplete solver with
 /// a complete secondary solver, to form an (optimized) complete
 /// solver.
+
+typedef std::function<bool(const Query &)> QueryPredicate;
+
 class StagedSolverImpl : public SolverImpl {
 private:
   std::unique_ptr<IncompleteSolver> primary;
   std::unique_ptr<Solver> secondary;
+  QueryPredicate predicate;
 
 public:
   StagedSolverImpl(std::unique_ptr<IncompleteSolver> primary,
-                   std::unique_ptr<Solver> secondary);
+                   std::unique_ptr<Solver> secondary, QueryPredicate predicate);
 
   bool computeTruth(const Query &, bool &isValid);
   bool computeValidity(const Query &, PartialValidity &result);

lib/ADT/SparseStorage.cpp

@@ -35,7 +35,7 @@ void SparseStorage<unsigned char>::print(llvm::raw_ostream &os,
     }
     os << "] default: ";
   }
-  os << defaultValue;
+  os << ((unsigned)defaultValue);
 }
 
 template <>

lib/Core/Executor.cpp

@@ -7180,7 +7180,6 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
   }
   bool success = solver->getInitialValues(extendedConstraints.cs(), objects,
                                           values, state.queryMetaData);
-  Assignment assignment(objects, values);
   solver->setTimeout(time::Span());
   if (!success) {
     klee_warning("unable to compute initial values (invalid constraints?)!");

lib/Expr/IndependentConstraintSetUnion.cpp

@@ -95,27 +95,13 @@ void IndependentConstraintSetUnion::reEvaluateConcretization(
 void IndependentConstraintSetUnion::getAllIndependentConstraintSets(
     ref<Expr> e,
     std::vector<ref<const IndependentConstraintSet>> &result) const {
-  ref<const IndependentConstraintSet> compare =
-      new IndependentConstraintSet(new ExprEitherSymcrete::left(e));
-  for (auto &r : roots) {
-    ref<const IndependentConstraintSet> ics = disjointSets.at(r);
-    if (!IndependentConstraintSet::intersects(ics, compare)) {
-      result.push_back(ics);
-    }
-  }
+  getAllIndependentSets(new ExprEitherSymcrete::left(e), result);
 }
 
 void IndependentConstraintSetUnion::getAllDependentConstraintSets(
     ref<Expr> e,
     std::vector<ref<const IndependentConstraintSet>> &result) const {
-  ref<const IndependentConstraintSet> compare =
-      new IndependentConstraintSet(new ExprEitherSymcrete::left(e));
-  for (auto &r : roots) {
-    ref<const IndependentConstraintSet> ics = disjointSets.at(r);
-    if (IndependentConstraintSet::intersects(ics, compare)) {
-      result.push_back(ics);
-    }
-  }
+  getAllDependentSets(new ExprEitherSymcrete::left(e), result);
 }
 
 void IndependentConstraintSetUnion::addExpr(ref<Expr> e) {

lib/Module/KModule.cpp

@@ -282,16 +282,6 @@ void KModule::optimiseAndPrepare(
     pm.run(*module);
   }
 
-  if (opts.Optimize)
-    Optimize(module.get(), preservedFunctions);
-
-  // Add internal functions which are not used to check if instructions
-  // have been already visited
-  if (opts.CheckDivZero)
-    addInternalFunction("klee_div_zero_check");
-  if (opts.CheckOvershift)
-    addInternalFunction("klee_overshift_check");
-
   // Use KLEE's internal float classification functions if requested.
   if (opts.WithFPRuntime) {
     if (UseKleeFloatInternals) {
@@ -304,6 +294,16 @@ void KModule::optimiseAndPrepare(
     }
   }
 
+  if (opts.Optimize)
+    Optimize(module.get(), preservedFunctions);
+
+  // Add internal functions which are not used to check if instructions
+  // have been already visited
+  if (opts.CheckDivZero)
+    addInternalFunction("klee_div_zero_check");
+  if (opts.CheckOvershift)
+    addInternalFunction("klee_overshift_check");
+
   // Needs to happen after linking (since ctors/dtors can be modified)
   // and optimization (since global optimization can rewrite lists).
   injectStaticConstructorsAndDestructors(module.get(), opts.EntryPoint);