klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
CexCachingSolver.cpp
Go to the documentation of this file.
1 //===-- CexCachingSolver.cpp ----------------------------------------------===//
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 #include "klee/Solver.h"
11 
12 #include "klee/Constraints.h"
13 #include "klee/Expr.h"
14 #include "klee/SolverImpl.h"
16 #include "klee/util/Assignment.h"
17 #include "klee/util/ExprUtil.h"
18 #include "klee/util/ExprVisitor.h"
20 
21 #include "SolverStats.h"
22 
23 #include "llvm/Support/CommandLine.h"
24 
25 using namespace klee;
26 using namespace llvm;
27 
28 namespace {
29  cl::opt<bool>
30  DebugCexCacheCheckBinding("debug-cex-cache-check-binding");
31 
32  cl::opt<bool>
33  CexCacheTryAll("cex-cache-try-all",
34  cl::desc("try substituting all counterexamples before asking the SMT solver"),
35  cl::init(false));
36 
37  cl::opt<bool>
38  CexCacheExperimental("cex-cache-exp", cl::init(false));
39 
40 }
41 
43 
44 typedef std::set< ref<Expr> > KeyType;
45 
47  bool operator()(const Assignment *a, const Assignment *b) {
48  return a->bindings < b->bindings;
49  }
50 };
51 
52 
53 class CexCachingSolver : public SolverImpl {
54  typedef std::set<Assignment*, AssignmentLessThan> assignmentsTable_ty;
55 
57 
59  // memo table
61 
62  bool searchForAssignment(KeyType &key,
63  Assignment *&result);
64 
65  bool lookupAssignment(const Query& query, KeyType &key, Assignment *&result);
66 
67  bool lookupAssignment(const Query& query, Assignment *&result) {
68  KeyType key;
69  return lookupAssignment(query, key, result);
70  }
71 
72  bool getAssignment(const Query& query, Assignment *&result);
73 
74 public:
75  CexCachingSolver(Solver *_solver) : solver(_solver) {}
77 
78  bool computeTruth(const Query&, bool &isValid);
79  bool computeValidity(const Query&, Solver::Validity &result);
80  bool computeValue(const Query&, ref<Expr> &result);
81  bool computeInitialValues(const Query&,
82  const std::vector<const Array*> &objects,
83  std::vector< std::vector<unsigned char> > &values,
84  bool &hasSolution);
85  SolverRunStatus getOperationStatusCode();
86  char *getConstraintLog(const Query& query);
87  void setCoreSolverTimeout(double timeout);
88 };
89 
91 
93  bool operator()(Assignment *a) const { return !a; }
94 };
95 
97  bool operator()(Assignment *a) const { return a!=0; }
98 };
99 
102 
103  NullOrSatisfyingAssignment(KeyType &_key) : key(_key) {}
104 
105  bool operator()(Assignment *a) const {
106  return !a || a->satisfies(key.begin(), key.end());
107  }
108 };
109 
118  Assignment * const *lookup = cache.lookup(key);
119  if (lookup) {
120  result = *lookup;
121  return true;
122  }
123 
124  if (CexCacheTryAll) {
125  // Look for a satisfying assignment for a superset, which is trivially an
126  // assignment for any subset.
127  Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
128 
129  // Otherwise, look for a subset which is unsatisfiable, see below.
130  if (!lookup)
131  lookup = cache.findSubset(key, NullAssignment());
132 
133  // If either lookup succeeded, then we have a cached solution.
134  if (lookup) {
135  result = *lookup;
136  return true;
137  }
138 
139  // Otherwise, iterate through the set of current assignments to see if one
140  // of them satisfies the query.
141  for (assignmentsTable_ty::iterator it = assignmentsTable.begin(),
142  ie = assignmentsTable.end(); it != ie; ++it) {
143  Assignment *a = *it;
144  if (a->satisfies(key.begin(), key.end())) {
145  result = a;
146  return true;
147  }
148  }
149  } else {
150  // FIXME: Which order? one is sure to be better.
151 
152  // Look for a satisfying assignment for a superset, which is trivially an
153  // assignment for any subset.
154  Assignment **lookup = cache.findSuperset(key, NonNullAssignment());
155 
156  // Otherwise, look for a subset which is unsatisfiable -- if the subset is
157  // unsatisfiable then no additional constraints can produce a valid
158  // assignment. While searching subsets, we also explicitly the solutions for
159  // satisfiable subsets to see if they solve the current query and return
160  // them if so. This is cheap and frequently succeeds.
161  if (!lookup)
162  lookup = cache.findSubset(key, NullOrSatisfyingAssignment(key));
163 
164  // If either lookup succeeded, then we have a cached solution.
165  if (lookup) {
166  result = *lookup;
167  return true;
168  }
169  }
170 
171  return false;
172 }
173 
183  KeyType &key,
184  Assignment *&result) {
185  key = KeyType(query.constraints.begin(), query.constraints.end());
186  ref<Expr> neg = Expr::createIsZero(query.expr);
187  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
188  if (CE->isFalse()) {
189  result = (Assignment*) 0;
191  return true;
192  }
193  } else {
194  key.insert(neg);
195  }
196 
197  bool found = searchForAssignment(key, result);
198  if (found)
201 
202  return found;
203 }
204 
205 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
206  KeyType key;
207  if (lookupAssignment(query, key, result))
208  return true;
209 
210  std::vector<const Array*> objects;
211  findSymbolicObjects(key.begin(), key.end(), objects);
212 
213  std::vector< std::vector<unsigned char> > values;
214  bool hasSolution;
215  if (!solver->impl->computeInitialValues(query, objects, values,
216  hasSolution))
217  return false;
218 
219  Assignment *binding;
220  if (hasSolution) {
221  binding = new Assignment(objects, values);
222 
223  // Memoize the result.
224  std::pair<assignmentsTable_ty::iterator, bool>
225  res = assignmentsTable.insert(binding);
226  if (!res.second) {
227  delete binding;
228  binding = *res.first;
229  }
230 
231  if (DebugCexCacheCheckBinding)
232  assert(binding->satisfies(key.begin(), key.end()));
233  } else {
234  binding = (Assignment*) 0;
235  }
236 
237  result = binding;
238  cache.insert(key, binding);
239 
240  return true;
241 }
242 
244 
246  cache.clear();
247  delete solver;
248  for (assignmentsTable_ty::iterator it = assignmentsTable.begin(),
249  ie = assignmentsTable.end(); it != ie; ++it)
250  delete *it;
251 }
252 
254  Solver::Validity &result) {
256  Assignment *a;
257  if (!getAssignment(query.withFalse(), a))
258  return false;
259  assert(a && "computeValidity() must have assignment");
260  ref<Expr> q = a->evaluate(query.expr);
261  assert(isa<ConstantExpr>(q) &&
262  "assignment evaluation did not result in constant");
263 
264  if (cast<ConstantExpr>(q)->isTrue()) {
265  if (!getAssignment(query, a))
266  return false;
267  result = !a ? Solver::True : Solver::Unknown;
268  } else {
269  if (!getAssignment(query.negateExpr(), a))
270  return false;
271  result = !a ? Solver::False : Solver::Unknown;
272  }
273 
274  return true;
275 }
276 
278  bool &isValid) {
280 
281  // There is a small amount of redundancy here. We only need to know
282  // truth and do not really need to compute an assignment. This means
283  // that we could check the cache to see if we already know that
284  // state ^ query has no assignment. In that case, by the validity of
285  // state, we know that state ^ !query must have an assignment, and
286  // so query cannot be true (valid). This does get hits, but doesn't
287  // really seem to be worth the overhead.
288 
289  if (CexCacheExperimental) {
290  Assignment *a;
291  if (lookupAssignment(query.negateExpr(), a) && !a)
292  return false;
293  }
294 
295  Assignment *a;
296  if (!getAssignment(query, a))
297  return false;
298 
299  isValid = !a;
300 
301  return true;
302 }
303 
305  ref<Expr> &result) {
307 
308  Assignment *a;
309  if (!getAssignment(query.withFalse(), a))
310  return false;
311  assert(a && "computeValue() must have assignment");
312  result = a->evaluate(query.expr);
313  assert(isa<ConstantExpr>(result) &&
314  "assignment evaluation did not result in constant");
315  return true;
316 }
317 
318 bool
320  const std::vector<const Array*>
321  &objects,
322  std::vector< std::vector<unsigned char> >
323  &values,
324  bool &hasSolution) {
326  Assignment *a;
327  if (!getAssignment(query, a))
328  return false;
329  hasSolution = !!a;
330 
331  if (!a)
332  return true;
333 
334  // FIXME: We should use smarter assignment for result so we don't
335  // need redundant copy.
336  values = std::vector< std::vector<unsigned char> >(objects.size());
337  for (unsigned i=0; i < objects.size(); ++i) {
338  const Array *os = objects[i];
339  Assignment::bindings_ty::iterator it = a->bindings.find(os);
340 
341  if (it == a->bindings.end()) {
342  values[i] = std::vector<unsigned char>(os->size, 0);
343  } else {
344  values[i] = it->second;
345  }
346  }
347 
348  return true;
349 }
350 
352  return solver->impl->getOperationStatusCode();
353 }
354 
356  return solver->impl->getConstraintLog(query);
357 }
358 
360  solver->impl->setCoreSolverTimeout(timeout);
361 }
362 
364 
366  return new Solver(new CexCachingSolver(_solver));
367 }
CexCachingSolver(Solver *_solver)
std::set< ref< Expr > > KeyType
constraint_iterator end() const
Definition: Constraints.h:57
MapOfSets< ref< Expr >, Assignment * > cache
Statistic cexCacheTime
bool computeValue(const Query &, ref< Expr > &result)
bool operator()(const Assignment *a, const Assignment *b)
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
bool operator()(Assignment *a) const
unsigned size
Definition: Expr.h:605
ref< Expr > expr
Definition: Solver.h:25
char * getConstraintLog(const Query &query)
bool operator()(Assignment *a) const
ref< Expr > evaluate(const Array *mo, unsigned index) const
Definition: Assignment.h:68
bool lookupAssignment(const Query &query, KeyType &key, Assignment *&result)
Query withFalse() const
withFalse - Return a copy of the query with a false expression.
Definition: Solver.h:37
Statistic queryCexCacheMisses
bool computeValidity(const Query &, Solver::Validity &result)
bool lookupAssignment(const Query &query, Assignment *&result)
bindings_ty bindings
Definition: Assignment.h:27
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
bool computeTruth(const Query &, bool &isValid)
Query negateExpr() const
negateExpr - Return a copy of the query with the expression negated.
Definition: Solver.h:42
assignmentsTable_ty assignmentsTable
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
bool getAssignment(const Query &query, Assignment *&result)
std::set< Assignment *, AssignmentLessThan > assignmentsTable_ty
NullOrSatisfyingAssignment(KeyType &_key)
void findSymbolicObjects(ref< Expr > e, std::vector< const Array * > &results)
Definition: ExprUtil.cpp:118
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
bool searchForAssignment(KeyType &key, Assignment *&result)
bool satisfies(InputIterator begin, InputIterator end)
Definition: Assignment.h:90
void setCoreSolverTimeout(double timeout)
bool operator()(Assignment *a) const
Solver * createCexCachingSolver(Solver *s)
Statistic queryCexCacheHits