about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-09-15 12:09:23 +0100
committerDan Liew <delcypher@gmail.com>2017-03-23 21:46:41 +0000
commit4530447c21353b5596b66a9fbb642409cda56f73 (patch)
tree094a516168e39166898887984cdb2cbed6762965 /include
parenta40818cab8e1b2315ac40d2c2cb125fc422e8ed7 (diff)
downloadklee-4530447c21353b5596b66a9fbb642409cda56f73.tar.gz
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.
Diffstat (limited to 'include')
-rw-r--r--include/klee/CommandLine.h2
-rw-r--r--include/klee/Solver.h6
-rw-r--r--include/klee/util/Assignment.h1
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);