klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CachingSolver.cpp
Go to the documentation of this file.
1 //===-- CachingSolver.cpp - Caching expression solver ---------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 
11 #include "klee/Solver.h"
12 
13 #include "klee/Constraints.h"
14 #include "klee/Expr.h"
15 #include "klee/IncompleteSolver.h"
16 #include "klee/SolverImpl.h"
17 
18 #include "SolverStats.h"
19 
20 #include <tr1/unordered_map>
21 
22 using namespace klee;
23 
24 class CachingSolver : public SolverImpl {
25 private:
26  ref<Expr> canonicalizeQuery(ref<Expr> originalQuery,
27  bool &negationUsed);
28 
29  void cacheInsert(const Query& query,
31 
32  bool cacheLookup(const Query& query,
34 
35  struct CacheEntry {
37  : constraints(c), query(q) {}
38 
40  : constraints(ce.constraints), query(ce.query) {}
41 
44 
45  bool operator==(const CacheEntry &b) const {
46  return constraints==b.constraints && *query.get()==*b.query.get();
47  }
48  };
49 
50  struct CacheEntryHash {
51  unsigned operator()(const CacheEntry &ce) const {
52  unsigned result = ce.query->hash();
53 
55  it != ce.constraints.end(); ++it)
56  result ^= (*it)->hash();
57 
58  return result;
59  }
60  };
61 
62  typedef std::tr1::unordered_map<CacheEntry,
65 
68 
69 public:
70  CachingSolver(Solver *s) : solver(s) {}
71  ~CachingSolver() { cache.clear(); delete solver; }
72 
73  bool computeValidity(const Query&, Solver::Validity &result);
74  bool computeTruth(const Query&, bool &isValid);
75  bool computeValue(const Query& query, ref<Expr> &result) {
77  return solver->impl->computeValue(query, result);
78  }
79  bool computeInitialValues(const Query& query,
80  const std::vector<const Array*> &objects,
81  std::vector< std::vector<unsigned char> > &values,
82  bool &hasSolution) {
84  return solver->impl->computeInitialValues(query, objects, values,
85  hasSolution);
86  }
87  SolverRunStatus getOperationStatusCode();
88  char *getConstraintLog(const Query&);
89  void setCoreSolverTimeout(double timeout);
90 };
91 
96  bool &negationUsed) {
97  ref<Expr> negatedQuery = Expr::createIsZero(originalQuery);
98 
99  // select the "smaller" query to the be canonical representation
100  if (originalQuery.compare(negatedQuery) < 0) {
101  negationUsed = false;
102  return originalQuery;
103  } else {
104  negationUsed = true;
105  return negatedQuery;
106  }
107 }
108 
113  bool negationUsed;
114  ref<Expr> canonicalQuery = canonicalizeQuery(query.expr, negationUsed);
115 
116  CacheEntry ce(query.constraints, canonicalQuery);
117  cache_map::iterator it = cache.find(ce);
118 
119  if (it != cache.end()) {
120  result = (negationUsed ?
122  it->second);
123  return true;
124  }
125 
126  return false;
127 }
128 
132  bool negationUsed;
133  ref<Expr> canonicalQuery = canonicalizeQuery(query.expr, negationUsed);
134 
135  CacheEntry ce(query.constraints, canonicalQuery);
136  IncompleteSolver::PartialValidity cachedResult =
137  (negationUsed ? IncompleteSolver::negatePartialValidity(result) : result);
138 
139  cache.insert(std::make_pair(ce, cachedResult));
140 }
141 
143  Solver::Validity &result) {
145  bool tmp, cacheHit = cacheLookup(query, cachedResult);
146 
147  if (cacheHit) {
148  switch(cachedResult) {
150  result = Solver::True;
152  return true;
154  result = Solver::False;
156  return true;
158  result = Solver::Unknown;
160  return true;
163  if (!solver->impl->computeTruth(query, tmp))
164  return false;
165  if (tmp) {
166  cacheInsert(query, IncompleteSolver::MustBeTrue);
167  result = Solver::True;
168  return true;
169  } else {
170  cacheInsert(query, IncompleteSolver::TrueOrFalse);
171  result = Solver::Unknown;
172  return true;
173  }
174  }
177  if (!solver->impl->computeTruth(query.negateExpr(), tmp))
178  return false;
179  if (tmp) {
180  cacheInsert(query, IncompleteSolver::MustBeFalse);
181  result = Solver::False;
182  return true;
183  } else {
184  cacheInsert(query, IncompleteSolver::TrueOrFalse);
185  result = Solver::Unknown;
186  return true;
187  }
188  }
189  default: assert(0 && "unreachable");
190  }
191  }
192 
194 
195  if (!solver->impl->computeValidity(query, result))
196  return false;
197 
198  switch (result) {
199  case Solver::True:
200  cachedResult = IncompleteSolver::MustBeTrue; break;
201  case Solver::False:
202  cachedResult = IncompleteSolver::MustBeFalse; break;
203  default:
204  cachedResult = IncompleteSolver::TrueOrFalse; break;
205  }
206 
207  cacheInsert(query, cachedResult);
208  return true;
209 }
210 
212  bool &isValid) {
214  bool cacheHit = cacheLookup(query, cachedResult);
215 
216  // a cached result of MayBeTrue forces us to check whether
217  // a False assignment exists.
218  if (cacheHit && cachedResult != IncompleteSolver::MayBeTrue) {
220  isValid = (cachedResult == IncompleteSolver::MustBeTrue);
221  return true;
222  }
223 
225 
226  // cache miss: query solver
227  if (!solver->impl->computeTruth(query, isValid))
228  return false;
229 
230  if (isValid) {
231  cachedResult = IncompleteSolver::MustBeTrue;
232  } else if (cacheHit) {
233  // We know a true assignment exists, and query isn't valid, so
234  // must be TrueOrFalse.
235  assert(cachedResult == IncompleteSolver::MayBeTrue);
236  cachedResult = IncompleteSolver::TrueOrFalse;
237  } else {
238  cachedResult = IncompleteSolver::MayBeFalse;
239  }
240 
241  cacheInsert(query, cachedResult);
242  return true;
243 }
244 
246  return solver->impl->getOperationStatusCode();
247 }
248 
250  return solver->impl->getConstraintLog(query);
251 }
252 
254  solver->impl->setCoreSolverTimeout(timeout);
255 }
256 
258 
260  return new Solver(new CachingSolver(_solver));
261 }
T * get() const
Definition: Ref.h:69
int compare(const ref &rhs) const
Definition: Ref.h:102
constraint_iterator end() const
Definition: Constraints.h:57
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
bool computeValidity(const Query &, Solver::Validity &result)
ref< Expr > expr
Definition: Solver.h:25
bool cacheLookup(const Query &query, IncompleteSolver::PartialValidity &result)
bool operator==(const CacheEntry &b) const
virtual unsigned hash() const
Returns the pre-computed hash of the current expression.
Definition: Expr.h:192
CacheEntry(const ConstraintManager &c, ref< Expr > q)
Solver * createCachingSolver(Solver *s)
ref< Expr > canonicalizeQuery(ref< Expr > originalQuery, bool &negationUsed)
The query is provably true.
unsigned operator()(const CacheEntry &ce) const
Statistic queryCacheHits
static PartialValidity negatePartialValidity(PartialValidity pv)
bool computeInitialValues(const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Query negateExpr() const
negateExpr - Return a copy of the query with the expression negated.
Definition: Solver.h:42
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
const ConstraintManager & constraints
Definition: Solver.h:24
constraint_iterator begin() const
Definition: Constraints.h:54
The query is provably false.
char * getConstraintLog(const Query &)
void setCoreSolverTimeout(double timeout)
ConstraintManager constraints
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
The query is known to have both true and false assignments.
bool computeValue(const Query &query, ref< Expr > &result)
Statistic queryCacheMisses
CacheEntry(const CacheEntry &ce)
cache_map cache
bool computeTruth(const Query &, bool &isValid)
void cacheInsert(const Query &query, IncompleteSolver::PartialValidity result)
Inserts the given query, result pair into the cache.
std::vector< ref< Expr > >::const_iterator constraint_iterator
Definition: Constraints.h:38
std::tr1::unordered_map< CacheEntry, IncompleteSolver::PartialValidity, CacheEntryHash > cache_map
CachingSolver(Solver *s)