Add `AssignmentValidatingSolver`. It's purpose is to check any computed

assignments against the corresponding `Query` object and check the
assignment evaluates correctly.

This can be switched on using `-debug-assignment-validating-solver`
on the command line.

3 files changed, 9 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);