7 files changed, 191 insertions, 0 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index cc186db7..6a72692d 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -29,6 +29,8 @@ extern llvm::cl::opt<bool> UseForkedCoreSolver;
 
 extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
+extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
+
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
 {
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 2f613992..32c8cf9e 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -268,6 +268,12 @@ namespace klee {
   /// \param oracle - The solver to check query results against.
   Solver *createValidatingSolver(Solver *s, Solver *oracle);
 
+  /// createAssignmentValidatingSolver - Create a solver that when requested
+  /// for an assignment will check that the computed assignment satisfies
+  /// the Query.
+  /// \param s - The underlying solver to use.
+  Solver *createAssignmentValidatingSolver(Solver *s);
+
   /// createCachingSolver - Create a solver which will cache the queries in
   /// memory (without eviction).
   ///
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 5d8aa1ab..55e681de 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -46,6 +46,7 @@ namespace klee {
     
     ref<Expr> evaluate(const Array *mo, unsigned index) const;
     ref<Expr> evaluate(ref<Expr> e);
+    void createConstraintsFromAssignment(std::vector<ref<Expr> > &out) const;
 
     template<typename InputIterator>
     bool satisfies(InputIterator begin, InputIterator end);
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index e55c4550..82cb01b2 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -82,6 +82,10 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     llvm::cl::CommaSeparated
 );
 
+llvm::cl::opt<bool>
+    UseAssignmentValidatingSolver("debug-assignment-validating-solver",
+                                  llvm::cl::init(false));
+
 #ifdef ENABLE_METASMT
 
 #ifdef METASMT_DEFAULT_BACKEND_IS_BTOR
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 68e1b08b..d00fcec1 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -37,6 +37,9 @@ Solver *constructSolverChain(Solver *coreSolver,
                  baseSolverQuerySMT2LogPath.c_str());
   }
 
+  if (UseAssignmentValidatingSolver)
+    solver = createAssignmentValidatingSolver(solver);
+
   if (UseFastCexSolver)
     solver = createFastCexSolver(solver);
 
diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp
index 635362d4..d788785a 100644
--- a/lib/Expr/Assigment.cpp
+++ b/lib/Expr/Assigment.cpp
@@ -22,4 +22,21 @@ void Assignment::dump() {
     llvm::errs() << "]\n";
   }
 }
+
+void Assignment::createConstraintsFromAssignment(
+    std::vector<ref<Expr> > &out) const {
+  assert(out.size() == 0 && "out should be empty");
+  for (bindings_ty::const_iterator it = bindings.begin(), ie = bindings.end();
+       it != ie; ++it) {
+    const Array *array = it->first;
+    const std::vector<unsigned char> &values = it->second;
+    for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) {
+      unsigned char value = values[arrayIndex];
+      out.push_back(EqExpr::create(
+          ReadExpr::create(UpdateList(array, 0),
+                           ConstantExpr::alloc(arrayIndex, array->getDomain())),
+          ConstantExpr::alloc(value, array->getRange())));
+    }
+  }
+}
 }
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
new file mode 100644
index 00000000..a4d97f54
--- /dev/null
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -0,0 +1,158 @@
+//===-- AssignmentValidatingSolver.cpp ------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include "klee/util/Assignment.h"
+#include "klee/Constraints.h"
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+#include <vector>
+
+namespace klee {
+
+class AssignmentValidatingSolver : public SolverImpl {
+private:
+  Solver *solver;
+  void dumpAssignmentQuery(const Query &query, const Assignment &assignment);
+
+public:
+  AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {}
+  ~AssignmentValidatingSolver() { delete solver; }
+
+  bool computeValidity(const Query &, Solver::Validity &result);
+  bool computeTruth(const Query &, bool &isValid);
+  bool computeValue(const Query &, ref<Expr> &result);
+  bool computeInitialValues(const Query &,
+                            const std::vector<const Array *> &objects,
+                            std::vector<std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+  SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query &);
+  void setCoreSolverTimeout(double timeout);
+};
+
+// TODO: use computeInitialValues for all queries for more stress testing
+bool AssignmentValidatingSolver::computeValidity(const Query &query,
+                                                 Solver::Validity &result) {
+  return solver->impl->computeValidity(query, result);
+}
+bool AssignmentValidatingSolver::computeTruth(const Query &query,
+                                              bool &isValid) {
+  return solver->impl->computeTruth(query, isValid);
+}
+bool AssignmentValidatingSolver::computeValue(const Query &query,
+                                              ref<Expr> &result) {
+  return solver->impl->computeValue(query, result);
+}
+
+bool AssignmentValidatingSolver::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+  bool success =
+      solver->impl->computeInitialValues(query, objects, values, hasSolution);
+  if (!hasSolution)
+    return success;
+
+  // Use `_allowFreeValues` so that if we are missing an assignment
+  // we can't compute a constant and flag this as a problem.
+  Assignment assignment(objects, values, /*_allowFreeValues=*/true);
+  // Check computed assignment satisfies query
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                         ie = query.constraints.end();
+       it != ie; ++it) {
+    ref<Expr> constraint = *it;
+    ref<Expr> constraintEvaluated = assignment.evaluate(constraint);
+    ConstantExpr *CE = dyn_cast<ConstantExpr>(constraintEvaluated);
+    if (CE == NULL) {
+      llvm::errs() << "Constraint did not evalaute to a constant:\n";
+      llvm::errs() << "Constraint:\n" << constraint << "\n";
+      llvm::errs() << "Evaluated Constraint:\n" << constraintEvaluated << "\n";
+      llvm::errs() << "Assignment:\n";
+      assignment.dump();
+      dumpAssignmentQuery(query, assignment);
+      abort();
+    }
+    if (CE->isFalse()) {
+      llvm::errs() << "Constraint evaluated to false when using assignment\n";
+      llvm::errs() << "Constraint:\n" << constraint << "\n";
+      llvm::errs() << "Assignment:\n";
+      assignment.dump();
+      dumpAssignmentQuery(query, assignment);
+      abort();
+    }
+  }
+
+  ref<Expr> queryExprEvaluated = assignment.evaluate(query.expr);
+  ConstantExpr *CE = dyn_cast<ConstantExpr>(queryExprEvaluated);
+  if (CE == NULL) {
+    llvm::errs() << "Query expression did not evalaute to a constant:\n";
+    llvm::errs() << "Expression:\n" << query.expr << "\n";
+    llvm::errs() << "Evaluated expression:\n" << queryExprEvaluated << "\n";
+    llvm::errs() << "Assignment:\n";
+    assignment.dump();
+    dumpAssignmentQuery(query, assignment);
+    abort();
+  }
+  // KLEE queries are validity queries. A counter example to
+  // ∀ x constraints(x) → query(x)
+  // exists therefore
+  // ¬∀ x constraints(x) → query(x)
+  // Which is equivalent to
+  // ∃ x constraints(x) ∧ ¬ query(x)
+  // This means for the assignment we get back query expression should evaluate
+  // to false.
+  if (CE->isTrue()) {
+    llvm::errs()
+        << "Query Expression evaluated to true when using assignment\n";
+    llvm::errs() << "Expression:\n" << query.expr << "\n";
+    llvm::errs() << "Assignment:\n";
+    assignment.dump();
+    dumpAssignmentQuery(query, assignment);
+    abort();
+  }
+
+  return success;
+}
+
+void AssignmentValidatingSolver::dumpAssignmentQuery(
+    const Query &query, const Assignment &assignment) {
+  // Create a Query that is augmented with constraints that
+  // enforce the given assignment.
+  std::vector<ref<Expr> > constraints;
+  assignment.createConstraintsFromAssignment(constraints);
+  // Add Constraints from `query`
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                         ie = query.constraints.end();
+       it != ie; ++it) {
+    constraints.push_back(*it);
+  }
+  ConstraintManager augmentedConstraints(constraints);
+  Query augmentedQuery(augmentedConstraints, query.expr);
+
+  // Ask the solver for the log for this query.
+  char *logText = solver->getConstraintLog(augmentedQuery);
+  llvm::errs() << "Query with assignment as constraints:\n" << logText << "\n";
+  free(logText);
+}
+
+SolverImpl::SolverRunStatus
+AssignmentValidatingSolver::getOperationStatusCode() {
+  return solver->impl->getOperationStatusCode();
+}
+
+char *AssignmentValidatingSolver::getConstraintLog(const Query &query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) {
+  return solver->impl->setCoreSolverTimeout(timeout);
+}
+
+Solver *createAssignmentValidatingSolver(Solver *s) {
+  return new Solver(new AssignmentValidatingSolver(s));
+}
+}