Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 313 insertions, 0 deletions

diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
new file mode 100644
index 00000000..79bc985d
--- /dev/null
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -0,0 +1,313 @@
+//===-- CexCachingSolver.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/Solver.h"
+
+#include "klee/Constraints.h"
+#include "klee/Expr.h"
+#include "klee/SolverImpl.h"
+#include "klee/TimerStatIncrementer.h"
+#include "klee/util/Assignment.h"
+#include "klee/util/ExprUtil.h"
+#include "klee/util/ExprVisitor.h"
+#include "klee/Internal/ADT/MapOfSets.h"
+
+#include "SolverStats.h"
+
+#include "llvm/Support/CommandLine.h"
+
+using namespace klee;
+using namespace llvm;
+
+namespace {
+  cl::opt<bool>
+  DebugCexCacheCheckBinding("debug-cex-cache-check-binding");
+
+  cl::opt<bool>
+  CexCacheTryAll("cex-cache-try-all",
+                 cl::desc("try substituting all counterexamples before asking STP"),
+                 cl::init(false));
+
+  cl::opt<bool>
+  CexCacheExperimental("cex-cache-exp", cl::init(false));
+
+}
+
+///
+
+typedef std::set< ref<Expr> > KeyType;
+
+struct AssignmentLessThan {
+  bool operator()(const Assignment *a, const Assignment *b) {
+    return a->bindings < b->bindings;
+  }
+};
+
+
+class CexCachingSolver : public SolverImpl {
+  typedef std::set<Assignment*, AssignmentLessThan> assignmentsTable_ty;
+
+  Solver *solver;
+  
+  MapOfSets<ref<Expr>, Assignment*> cache;
+  // memo table
+  assignmentsTable_ty assignmentsTable;
+
+  bool searchForAssignment(KeyType &key, 
+                           Assignment *&result);
+  
+  bool lookupAssignment(const Query& query, Assignment *&result);
+
+  bool getAssignment(const Query& query, Assignment *&result);
+  
+public:
+  CexCachingSolver(Solver *_solver) : solver(_solver) {}
+  ~CexCachingSolver();
+  
+  bool computeTruth(const Query&, bool &isValid);
+  bool computeValidity(const Query&, Solver::Validity &result);
+  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);
+};
+
+///
+
+struct NullAssignment {
+  bool operator()(Assignment *a) const { return !a; }
+};
+
+struct NonNullAssignment {
+  bool operator()(Assignment *a) const { return a!=0; }
+};
+
+struct NullOrSatisfyingAssignment {
+  KeyType &key;
+  
+  NullOrSatisfyingAssignment(KeyType &_key) : key(_key) {}
+
+  bool operator()(Assignment *a) const { 
+    return !a || a->satisfies(key.begin(), key.end()); 
+  }
+};
+
+bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
+  Assignment * const *lookup = cache.lookup(key);
+  if (lookup) {
+    result = *lookup;
+    return true;
+  }
+
+  if (CexCacheTryAll) {
+    Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
+    if (!lookup) lookup = cache.findSubset(key, NullAssignment());
+    if (lookup) {
+      result = *lookup;
+      return true;
+    }
+    for (assignmentsTable_ty::iterator it = assignmentsTable.begin(), 
+           ie = assignmentsTable.end(); it != ie; ++it) {
+      Assignment *a = *it;
+      if (a->satisfies(key.begin(), key.end())) {
+        result = a;
+        return true;
+      }
+    }
+  } else {
+    // XXX which order? one is sure to be better
+    Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
+    if (!lookup) lookup = cache.findSubset(key, NullOrSatisfyingAssignment(key));
+    if (lookup) {
+      result = *lookup;
+      return true;
+    }
+  }
+  
+  return false;
+}
+
+bool CexCachingSolver::lookupAssignment(const Query &query, 
+                                        Assignment *&result) {
+  KeyType key(query.constraints.begin(), query.constraints.end());
+  ref<Expr> neg = Expr::createNot(query.expr);
+  if (neg.isConstant()) {
+    if (!neg.getConstantValue()) {
+      result = (Assignment*) 0;
+      return true;
+    }
+  } else {
+    key.insert(neg);
+  }
+
+  return searchForAssignment(key, result);
+}
+
+bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
+  KeyType key(query.constraints.begin(), query.constraints.end());
+  ref<Expr> neg = Expr::createNot(query.expr);
+  if (neg.isConstant()) {
+    if (!neg.getConstantValue()) {
+      result = (Assignment*) 0;
+      return true;
+    }
+  } else {
+    key.insert(neg);
+  }
+
+  if (!searchForAssignment(key, result)) {
+    // need to solve
+    
+    std::vector<const Array*> objects;
+    findSymbolicObjects(key.begin(), key.end(), objects);
+
+    std::vector< std::vector<unsigned char> > values;
+    bool hasSolution;
+    if (!solver->impl->computeInitialValues(query, objects, values, 
+                                            hasSolution))
+      return false;
+    
+    Assignment *binding;
+    if (hasSolution) {
+      binding = new Assignment(objects, values);
+
+      // memoization
+      std::pair<assignmentsTable_ty::iterator, bool>
+        res = assignmentsTable.insert(binding);
+      if (!res.second) {
+        delete binding;
+        binding = *res.first;
+      }
+
+      if (DebugCexCacheCheckBinding)
+        assert(binding->satisfies(key.begin(), key.end()));
+    } else {
+      binding = (Assignment*) 0;
+    }
+
+    result = binding;
+    cache.insert(key, binding);
+  }
+
+  return true;
+}
+
+///
+
+CexCachingSolver::~CexCachingSolver() {
+  cache.clear();
+  delete solver;
+  for (assignmentsTable_ty::iterator it = assignmentsTable.begin(), 
+         ie = assignmentsTable.end(); it != ie; ++it)
+    delete *it;
+}
+
+bool CexCachingSolver::computeValidity(const Query& query,
+                                       Solver::Validity &result) {
+  TimerStatIncrementer t(stats::cexCacheTime);
+  Assignment *a;
+  if (!getAssignment(query.withFalse(), a))
+    return false;
+  assert(a && "computeValidity() must have assignment");
+  ref<Expr> q = a->evaluate(query.expr);
+  assert(q.isConstant() && "assignment evaluation did not result in constant");
+
+  if (q.getConstantValue()) {
+    if (!getAssignment(query, a))
+      return false;
+    result = !a ? Solver::True : Solver::Unknown;
+  } else {
+    if (!getAssignment(query.negateExpr(), a))
+      return false;
+    result = !a ? Solver::False : Solver::Unknown;
+  }
+  
+  return true;
+}
+
+bool CexCachingSolver::computeTruth(const Query& query,
+                                    bool &isValid) {
+  TimerStatIncrementer t(stats::cexCacheTime);
+
+  // There is a small amount of redundancy here. We only need to know
+  // truth and do not really need to compute an assignment. This means
+  // that we could check the cache to see if we already know that
+  // state ^ query has no assignment. In that case, by the validity of
+  // state, we know that state ^ !query must have an assignment, and
+  // so query cannot be true (valid). This does get hits, but doesn't
+  // really seem to be worth the overhead.
+
+  if (CexCacheExperimental) {
+    Assignment *a;
+    if (lookupAssignment(query.negateExpr(), a) && !a)
+      return false;
+  }
+
+  Assignment *a;
+  if (!getAssignment(query, a))
+    return false;
+
+  isValid = !a;
+
+  return true;
+}
+
+bool CexCachingSolver::computeValue(const Query& query,
+                                    ref<Expr> &result) {
+  TimerStatIncrementer t(stats::cexCacheTime);
+
+  Assignment *a;
+  if (!getAssignment(query.withFalse(), a))
+    return false;
+  assert(a && "computeValue() must have assignment");
+  result = a->evaluate(query.expr);  
+  assert(result.isConstant() && 
+         "assignment evaluation did not result in constant");
+  return true;
+}
+
+bool 
+CexCachingSolver::computeInitialValues(const Query& query,
+                                       const std::vector<const Array*> 
+                                         &objects,
+                                       std::vector< std::vector<unsigned char> >
+                                         &values,
+                                       bool &hasSolution) {
+  TimerStatIncrementer t(stats::cexCacheTime);
+  Assignment *a;
+  if (!getAssignment(query, a))
+    return false;
+  hasSolution = !!a;
+  
+  if (!a)
+    return true;
+
+  // FIXME: We should use smarter assignment for result so we don't
+  // need redundant copy.
+  values = std::vector< std::vector<unsigned char> >(objects.size());
+  for (unsigned i=0; i < objects.size(); ++i) {
+    const Array *os = objects[i];
+    Assignment::bindings_ty::iterator it = a->bindings.find(os);
+    
+    if (it == a->bindings.end()) {
+      values[i] = std::vector<unsigned char>(os->size, 0);
+    } else {
+      values[i] = it->second;
+    }
+  }
+  
+  return true;
+}
+
+///
+
+Solver *klee::createCexCachingSolver(Solver *_solver) {
+  return new Solver(new CexCachingSolver(_solver));
+}