klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Constraints.cpp
Go to the documentation of this file.
1 //===-- Constraints.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/Constraints.h"
11 
12 #include "klee/util/ExprPPrinter.h"
13 #include "klee/util/ExprVisitor.h"
14 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
15 #include "llvm/IR/Function.h"
16 #else
17 #include "llvm/Function.h"
18 #endif
19 #include "llvm/Support/CommandLine.h"
21 
22 #include <map>
23 
24 using namespace klee;
25 
27 private:
28  ref<Expr> src, dst;
29 
30 public:
31  ExprReplaceVisitor(ref<Expr> _src, ref<Expr> _dst) : src(_src), dst(_dst) {}
32 
33  Action visitExpr(const Expr &e) {
34  if (e == *src.get()) {
35  return Action::changeTo(dst);
36  } else {
37  return Action::doChildren();
38  }
39  }
40 
42  if (e == *src.get()) {
43  return Action::changeTo(dst);
44  } else {
45  return Action::doChildren();
46  }
47  }
48 };
49 
51 private:
52  const std::map< ref<Expr>, ref<Expr> > &replacements;
53 
54 public:
55  ExprReplaceVisitor2(const std::map< ref<Expr>, ref<Expr> > &_replacements)
56  : ExprVisitor(true),
57  replacements(_replacements) {}
58 
60  std::map< ref<Expr>, ref<Expr> >::const_iterator it =
61  replacements.find(ref<Expr>(const_cast<Expr*>(&e)));
62  if (it!=replacements.end()) {
63  return Action::changeTo(it->second);
64  } else {
65  return Action::doChildren();
66  }
67  }
68 };
69 
72  bool changed = false;
73 
74  constraints.swap(old);
75  for (ConstraintManager::constraints_ty::iterator
76  it = old.begin(), ie = old.end(); it != ie; ++it) {
77  ref<Expr> &ce = *it;
78  ref<Expr> e = visitor.visit(ce);
79 
80  if (e!=ce) {
81  addConstraintInternal(e); // enable further reductions
82  changed = true;
83  } else {
84  constraints.push_back(ce);
85  }
86  }
87 
88  return changed;
89 }
90 
92  // XXX
93 }
94 
96  if (isa<ConstantExpr>(e))
97  return e;
98 
99  std::map< ref<Expr>, ref<Expr> > equalities;
100 
101  for (ConstraintManager::constraints_ty::const_iterator
102  it = constraints.begin(), ie = constraints.end(); it != ie; ++it) {
103  if (const EqExpr *ee = dyn_cast<EqExpr>(*it)) {
104  if (isa<ConstantExpr>(ee->left)) {
105  equalities.insert(std::make_pair(ee->right,
106  ee->left));
107  } else {
108  equalities.insert(std::make_pair(*it,
110  }
111  } else {
112  equalities.insert(std::make_pair(*it,
114  }
115  }
116 
117  return ExprReplaceVisitor2(equalities).visit(e);
118 }
119 
121  // rewrite any known equalities
122 
123  // XXX should profile the effects of this and the overhead.
124  // traversing the constraints looking for equalities is hardly the
125  // slowest thing we do, but it is probably nicer to have a
126  // ConstraintSet ADT which efficiently remembers obvious patterns
127  // (byte-constant comparison).
128 
129  switch (e->getKind()) {
130  case Expr::Constant:
131  assert(cast<ConstantExpr>(e)->isTrue() &&
132  "attempt to add invalid (false) constraint");
133  break;
134 
135  // split to enable finer grained independence and other optimizations
136  case Expr::And: {
137  BinaryExpr *be = cast<BinaryExpr>(e);
140  break;
141  }
142 
143  case Expr::Eq: {
144  BinaryExpr *be = cast<BinaryExpr>(e);
145  if (isa<ConstantExpr>(be->left)) {
146  ExprReplaceVisitor visitor(be->right, be->left);
147  rewriteConstraints(visitor);
148  }
149  constraints.push_back(e);
150  break;
151  }
152 
153  default:
154  constraints.push_back(e);
155  break;
156  }
157 }
158 
160  e = simplifyExpr(e);
162 }
ExprReplaceVisitor2(const std::map< ref< Expr >, ref< Expr > > &_replacements)
Definition: Constraints.cpp:55
ref< Expr > left
Definition: Expr.h:494
bool rewriteConstraints(ExprVisitor &visitor)
Definition: Constraints.cpp:70
void addConstraint(ref< Expr > e)
ExprReplaceVisitor(ref< Expr > _src, ref< Expr > _dst)
Definition: Constraints.cpp:31
void addConstraintInternal(ref< Expr > e)
Class representing symbolic expressions.
Definition: Expr.h:88
Action visitExprPost(const Expr &e)
Definition: Constraints.cpp:41
std::vector< ref< Expr > > constraints
Definition: Constraints.h:69
std::vector< ref< Expr > > constraints_ty
Definition: Constraints.h:25
void simplifyForValidConstraint(ref< Expr > e)
Definition: Constraints.cpp:91
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
const std::map< ref< Expr >, ref< Expr > > & replacements
Definition: Constraints.cpp:52
ref< Expr > right
Definition: Expr.h:494
ref< Expr > simplifyExpr(ref< Expr > e) const
Definition: Constraints.cpp:95
virtual Kind getKind() const =0
static const Width Bool
Definition: Expr.h:97
Action visitExpr(const Expr &e)
Definition: Constraints.cpp:33
Action visitExprPost(const Expr &e)
Definition: Constraints.cpp:59
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:24