klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
IndependentSolver.cpp
Go to the documentation of this file.
1 //===-- IndependentSolver.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/Expr.h"
13 #include "klee/Constraints.h"
14 #include "klee/SolverImpl.h"
15 
16 #include "klee/util/ExprUtil.h"
17 
18 #define DEBUG_TYPE "independent-solver"
19 #include "llvm/Support/Debug.h"
20 #include "llvm/Support/raw_ostream.h"
21 #include <map>
22 #include <vector>
23 #include <ostream>
24 
25 using namespace klee;
26 using namespace llvm;
27 
28 template<class T>
29 class DenseSet {
30  typedef std::set<T> set_ty;
32 
33 public:
34  DenseSet() {}
35 
36  void add(T x) {
37  s.insert(x);
38  }
39  void add(T start, T end) {
40  for (; start<end; start++)
41  s.insert(start);
42  }
43 
44  // returns true iff set is changed by addition
45  bool add(const DenseSet &b) {
46  bool modified = false;
47  for (typename set_ty::const_iterator it = b.s.begin(), ie = b.s.end();
48  it != ie; ++it) {
49  if (modified || !s.count(*it)) {
50  modified = true;
51  s.insert(*it);
52  }
53  }
54  return modified;
55  }
56 
57  bool intersects(const DenseSet &b) {
58  for (typename set_ty::iterator it = s.begin(), ie = s.end();
59  it != ie; ++it)
60  if (b.s.count(*it))
61  return true;
62  return false;
63  }
64 
65  void print(llvm::raw_ostream &os) const {
66  bool first = true;
67  os << "{";
68  for (typename set_ty::iterator it = s.begin(), ie = s.end();
69  it != ie; ++it) {
70  if (first) {
71  first = false;
72  } else {
73  os << ",";
74  }
75  os << *it;
76  }
77  os << "}";
78  }
79 };
80 
81 template <class T>
82 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
83  const ::DenseSet<T> &dis) {
84  dis.print(os);
85  return os;
86 }
87 
89  typedef std::map<const Array*, ::DenseSet<unsigned> > elements_ty;
91  std::set<const Array*> wholeObjects;
92 
93 public:
96  std::vector< ref<ReadExpr> > reads;
97  findReads(e, /* visitUpdates= */ true, reads);
98  for (unsigned i = 0; i != reads.size(); ++i) {
99  ReadExpr *re = reads[i].get();
100  const Array *array = re->updates.root;
101 
102  // Reads of a constant array don't alias.
103  if (re->updates.root->isConstantArray() &&
104  !re->updates.head)
105  continue;
106 
107  if (!wholeObjects.count(array)) {
108  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
109  ::DenseSet<unsigned> &dis = elements[array];
110  dis.add((unsigned) CE->getZExtValue(32));
111  } else {
112  elements_ty::iterator it2 = elements.find(array);
113  if (it2!=elements.end())
114  elements.erase(it2);
115  wholeObjects.insert(array);
116  }
117  }
118  }
119  }
121  elements(ies.elements),
122  wholeObjects(ies.wholeObjects) {}
123 
125  elements = ies.elements;
126  wholeObjects = ies.wholeObjects;
127  return *this;
128  }
129 
130  void print(llvm::raw_ostream &os) const {
131  os << "{";
132  bool first = true;
133  for (std::set<const Array*>::iterator it = wholeObjects.begin(),
134  ie = wholeObjects.end(); it != ie; ++it) {
135  const Array *array = *it;
136 
137  if (first) {
138  first = false;
139  } else {
140  os << ", ";
141  }
142 
143  os << "MO" << array->name;
144  }
145  for (elements_ty::const_iterator it = elements.begin(), ie = elements.end();
146  it != ie; ++it) {
147  const Array *array = it->first;
148  const ::DenseSet<unsigned> &dis = it->second;
149 
150  if (first) {
151  first = false;
152  } else {
153  os << ", ";
154  }
155 
156  os << "MO" << array->name << " : " << dis;
157  }
158  os << "}";
159  }
160 
161  // more efficient when this is the smaller set
163  for (std::set<const Array*>::iterator it = wholeObjects.begin(),
164  ie = wholeObjects.end(); it != ie; ++it) {
165  const Array *array = *it;
166  if (b.wholeObjects.count(array) ||
167  b.elements.find(array) != b.elements.end())
168  return true;
169  }
170  for (elements_ty::iterator it = elements.begin(), ie = elements.end();
171  it != ie; ++it) {
172  const Array *array = it->first;
173  if (b.wholeObjects.count(array))
174  return true;
175  elements_ty::const_iterator it2 = b.elements.find(array);
176  if (it2 != b.elements.end()) {
177  if (it->second.intersects(it2->second))
178  return true;
179  }
180  }
181  return false;
182  }
183 
184  // returns true iff set is changed by addition
185  bool add(const IndependentElementSet &b) {
186  bool modified = false;
187  for (std::set<const Array*>::const_iterator it = b.wholeObjects.begin(),
188  ie = b.wholeObjects.end(); it != ie; ++it) {
189  const Array *array = *it;
190  elements_ty::iterator it2 = elements.find(array);
191  if (it2!=elements.end()) {
192  modified = true;
193  elements.erase(it2);
194  wholeObjects.insert(array);
195  } else {
196  if (!wholeObjects.count(array)) {
197  modified = true;
198  wholeObjects.insert(array);
199  }
200  }
201  }
202  for (elements_ty::const_iterator it = b.elements.begin(),
203  ie = b.elements.end(); it != ie; ++it) {
204  const Array *array = it->first;
205  if (!wholeObjects.count(array)) {
206  elements_ty::iterator it2 = elements.find(array);
207  if (it2==elements.end()) {
208  modified = true;
209  elements.insert(*it);
210  } else {
211  if (it2->second.add(it->second))
212  modified = true;
213  }
214  }
215  }
216  return modified;
217  }
218 };
219 
220 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
221  const IndependentElementSet &ies) {
222  ies.print(os);
223  return os;
224 }
225 
226 static
228  std::vector< ref<Expr> > &result) {
229  IndependentElementSet eltsClosure(query.expr);
230  std::vector< std::pair<ref<Expr>, IndependentElementSet> > worklist;
231 
233  ie = query.constraints.end(); it != ie; ++it)
234  worklist.push_back(std::make_pair(*it, IndependentElementSet(*it)));
235 
236  // XXX This should be more efficient (in terms of low level copy stuff).
237  bool done = false;
238  do {
239  done = true;
240  std::vector< std::pair<ref<Expr>, IndependentElementSet> > newWorklist;
241  for (std::vector< std::pair<ref<Expr>, IndependentElementSet> >::iterator
242  it = worklist.begin(), ie = worklist.end(); it != ie; ++it) {
243  if (it->second.intersects(eltsClosure)) {
244  if (eltsClosure.add(it->second))
245  done = false;
246  result.push_back(it->first);
247  } else {
248  newWorklist.push_back(*it);
249  }
250  }
251  worklist.swap(newWorklist);
252  } while (!done);
253 
254 DEBUG(
255  std::set< ref<Expr> > reqset(result.begin(), result.end());
256  errs() << "--\n";
257  errs() << "Q: " << query.expr << "\n";
258  errs() << "\telts: " << IndependentElementSet(query.expr) << "\n";
259  int i = 0;
261  ie = query.constraints.end(); it != ie; ++it) {
262  errs() << "C" << i++ << ": " << *it;
263  errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
264  errs() << "\telts: " << IndependentElementSet(*it) << "\n";
265  }
266  errs() << "elts closure: " << eltsClosure << "\n";
267  );
268 
269 
270  return eltsClosure;
271 }
272 
274 private:
276 
277 public:
279  : solver(_solver) {}
280  ~IndependentSolver() { delete solver; }
281 
282  bool computeTruth(const Query&, bool &isValid);
283  bool computeValidity(const Query&, Solver::Validity &result);
284  bool computeValue(const Query&, ref<Expr> &result);
285  bool computeInitialValues(const Query& query,
286  const std::vector<const Array*> &objects,
287  std::vector< std::vector<unsigned char> > &values,
288  bool &hasSolution) {
289  return solver->impl->computeInitialValues(query, objects, values,
290  hasSolution);
291  }
292  SolverRunStatus getOperationStatusCode();
293  char *getConstraintLog(const Query&);
294  void setCoreSolverTimeout(double timeout);
295 };
296 
298  Solver::Validity &result) {
299  std::vector< ref<Expr> > required;
300  IndependentElementSet eltsClosure =
301  getIndependentConstraints(query, required);
302  ConstraintManager tmp(required);
303  return solver->impl->computeValidity(Query(tmp, query.expr),
304  result);
305 }
306 
307 bool IndependentSolver::computeTruth(const Query& query, bool &isValid) {
308  std::vector< ref<Expr> > required;
309  IndependentElementSet eltsClosure =
310  getIndependentConstraints(query, required);
311  ConstraintManager tmp(required);
312  return solver->impl->computeTruth(Query(tmp, query.expr),
313  isValid);
314 }
315 
316 bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
317  std::vector< ref<Expr> > required;
318  IndependentElementSet eltsClosure =
319  getIndependentConstraints(query, required);
320  ConstraintManager tmp(required);
321  return solver->impl->computeValue(Query(tmp, query.expr), result);
322 }
323 
325  return solver->impl->getOperationStatusCode();
326 }
327 
329  return solver->impl->getConstraintLog(query);
330 }
331 
333  solver->impl->setCoreSolverTimeout(timeout);
334 }
335 
337  return new Solver(new IndependentSolver(s));
338 }
constraint_iterator end() const
Definition: Constraints.h:57
void setCoreSolverTimeout(double timeout)
char * getConstraintLog(const Query &)
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
std::set< T > set_ty
bool intersects(const DenseSet &b)
ref< Expr > expr
Definition: Solver.h:25
void print(llvm::raw_ostream &os) const
llvm::raw_ostream & operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
bool add(const IndependentElementSet &b)
IndependentElementSet(const IndependentElementSet &ies)
constraints_ty::const_iterator const_iterator
Definition: Constraints.h:27
UpdateList updates
Definition: Expr.h:687
IndependentSolver(Solver *_solver)
std::map< const Array *,::DenseSet< unsigned > > elements_ty
bool computeValidity(const Query &, Solver::Validity &result)
void add(T start, T end)
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
const ConstraintManager & constraints
Definition: Solver.h:24
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
bool intersects(const IndependentElementSet &b)
void findReads(ref< Expr > e, bool visitUpdates, std::vector< ref< ReadExpr > > &result)
Definition: ExprUtil.cpp:21
constraint_iterator begin() const
Definition: Constraints.h:54
bool computeValue(const Query &, ref< Expr > &result)
const std::string name
Definition: Expr.h:603
bool computeTruth(const Query &, bool &isValid)
Solver * createIndependentSolver(Solver *s)
static IndependentElementSet getIndependentConstraints(const Query &query, std::vector< ref< Expr > > &result)
IndependentElementSet & operator=(const IndependentElementSet &ies)
bool isConstantArray() const
Definition: Expr.h:642
const Array * root
Definition: Expr.h:659
Class representing a one byte read from an array.
Definition: Expr.h:681
ref< Expr > index
Definition: Expr.h:688
bool add(const DenseSet &b)
void add(T x)
void print(llvm::raw_ostream &os) const
IndependentElementSet(ref< Expr > e)
std::set< const Array * > wholeObjects
bool computeInitialValues(const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)