klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprVisitor.cpp
Go to the documentation of this file.
1 //===-- ExprVisitor.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/Expr.h"
11 #include "klee/util/ExprVisitor.h"
12 
13 #include "llvm/Support/CommandLine.h"
14 
15 namespace {
16  llvm::cl::opt<bool>
17  UseVisitorHash("use-visitor-hash",
18  llvm::cl::desc("Use hash-consing during expr visitation."),
19  llvm::cl::init(true));
20 }
21 
22 using namespace klee;
23 
25  if (!UseVisitorHash || isa<ConstantExpr>(e)) {
26  return visitActual(e);
27  } else {
28  visited_ty::iterator it = visited.find(e);
29 
30  if (it!=visited.end()) {
31  return it->second;
32  } else {
33  ref<Expr> res = visitActual(e);
34  visited.insert(std::make_pair(e, res));
35  return res;
36  }
37  }
38 }
39 
41  if (isa<ConstantExpr>(e)) {
42  return e;
43  } else {
44  Expr &ep = *e.get();
45 
46  Action res = visitExpr(ep);
47  switch(res.kind) {
48  case Action::DoChildren:
49  // continue with normal action
50  break;
52  return e;
53  case Action::ChangeTo:
54  return res.argument;
55  }
56 
57  switch(ep.getKind()) {
58  case Expr::NotOptimized: res = visitNotOptimized(static_cast<NotOptimizedExpr&>(ep)); break;
59  case Expr::Read: res = visitRead(static_cast<ReadExpr&>(ep)); break;
60  case Expr::Select: res = visitSelect(static_cast<SelectExpr&>(ep)); break;
61  case Expr::Concat: res = visitConcat(static_cast<ConcatExpr&>(ep)); break;
62  case Expr::Extract: res = visitExtract(static_cast<ExtractExpr&>(ep)); break;
63  case Expr::ZExt: res = visitZExt(static_cast<ZExtExpr&>(ep)); break;
64  case Expr::SExt: res = visitSExt(static_cast<SExtExpr&>(ep)); break;
65  case Expr::Add: res = visitAdd(static_cast<AddExpr&>(ep)); break;
66  case Expr::Sub: res = visitSub(static_cast<SubExpr&>(ep)); break;
67  case Expr::Mul: res = visitMul(static_cast<MulExpr&>(ep)); break;
68  case Expr::UDiv: res = visitUDiv(static_cast<UDivExpr&>(ep)); break;
69  case Expr::SDiv: res = visitSDiv(static_cast<SDivExpr&>(ep)); break;
70  case Expr::URem: res = visitURem(static_cast<URemExpr&>(ep)); break;
71  case Expr::SRem: res = visitSRem(static_cast<SRemExpr&>(ep)); break;
72  case Expr::Not: res = visitNot(static_cast<NotExpr&>(ep)); break;
73  case Expr::And: res = visitAnd(static_cast<AndExpr&>(ep)); break;
74  case Expr::Or: res = visitOr(static_cast<OrExpr&>(ep)); break;
75  case Expr::Xor: res = visitXor(static_cast<XorExpr&>(ep)); break;
76  case Expr::Shl: res = visitShl(static_cast<ShlExpr&>(ep)); break;
77  case Expr::LShr: res = visitLShr(static_cast<LShrExpr&>(ep)); break;
78  case Expr::AShr: res = visitAShr(static_cast<AShrExpr&>(ep)); break;
79  case Expr::Eq: res = visitEq(static_cast<EqExpr&>(ep)); break;
80  case Expr::Ne: res = visitNe(static_cast<NeExpr&>(ep)); break;
81  case Expr::Ult: res = visitUlt(static_cast<UltExpr&>(ep)); break;
82  case Expr::Ule: res = visitUle(static_cast<UleExpr&>(ep)); break;
83  case Expr::Ugt: res = visitUgt(static_cast<UgtExpr&>(ep)); break;
84  case Expr::Uge: res = visitUge(static_cast<UgeExpr&>(ep)); break;
85  case Expr::Slt: res = visitSlt(static_cast<SltExpr&>(ep)); break;
86  case Expr::Sle: res = visitSle(static_cast<SleExpr&>(ep)); break;
87  case Expr::Sgt: res = visitSgt(static_cast<SgtExpr&>(ep)); break;
88  case Expr::Sge: res = visitSge(static_cast<SgeExpr&>(ep)); break;
89  case Expr::Constant:
90  default:
91  assert(0 && "invalid expression kind");
92  }
93 
94  switch(res.kind) {
95  default:
96  assert(0 && "invalid kind");
97  case Action::DoChildren: {
98  bool rebuild = false;
99  ref<Expr> e(&ep), kids[8];
100  unsigned count = ep.getNumKids();
101  for (unsigned i=0; i<count; i++) {
102  ref<Expr> kid = ep.getKid(i);
103  kids[i] = visit(kid);
104  if (kids[i] != kid)
105  rebuild = true;
106  }
107  if (rebuild) {
108  e = ep.rebuild(kids);
109  if (recursive)
110  e = visit(e);
111  }
112  if (!isa<ConstantExpr>(e)) {
113  res = visitExprPost(*e.get());
114  if (res.kind==Action::ChangeTo)
115  e = res.argument;
116  }
117  return e;
118  }
120  return e;
121  case Action::ChangeTo:
122  return res.argument;
123  }
124  }
125 }
126 
128  return Action::doChildren();
129 }
130 
132  return Action::skipChildren();
133 }
134 
136  return Action::doChildren();
137 }
138 
140  return Action::doChildren();
141 }
142 
144  return Action::doChildren();
145 }
146 
148  return Action::doChildren();
149 }
150 
152  return Action::doChildren();
153 }
154 
156  return Action::doChildren();
157 }
158 
160  return Action::doChildren();
161 }
162 
164  return Action::doChildren();
165 }
166 
168  return Action::doChildren();
169 }
170 
172  return Action::doChildren();
173 }
174 
176  return Action::doChildren();
177 }
178 
180  return Action::doChildren();
181 }
182 
184  return Action::doChildren();
185 }
186 
188  return Action::doChildren();
189 }
190 
192  return Action::doChildren();
193 }
194 
196  return Action::doChildren();
197 }
198 
200  return Action::doChildren();
201 }
202 
204  return Action::doChildren();
205 }
206 
208  return Action::doChildren();
209 }
210 
212  return Action::doChildren();
213 }
214 
216  return Action::doChildren();
217 }
218 
220  return Action::doChildren();
221 }
222 
224  return Action::doChildren();
225 }
226 
228  return Action::doChildren();
229 }
230 
232  return Action::doChildren();
233 }
234 
236  return Action::doChildren();
237 }
238 
240  return Action::doChildren();
241 }
242 
244  return Action::doChildren();
245 }
246 
248  return Action::doChildren();
249 }
250 
252  return Action::doChildren();
253 }
254 
256  return Action::doChildren();
257 }
258 
T * get() const
Definition: Ref.h:69
virtual Action visitMul(const MulExpr &)
virtual Action visitAShr(const AShrExpr &)
virtual ref< Expr > rebuild(ref< Expr > kids[]) const =0
Not used in canonical form.
Definition: Expr.h:151
virtual unsigned getNumKids() const =0
static Action doChildren()
Definition: ExprVisitor.h:39
virtual Action visitUlt(const UltExpr &)
visited_ty visited
Definition: ExprVisitor.h:85
virtual Action visitUle(const UleExpr &)
virtual Action visitConcat(const ConcatExpr &)
virtual Action visitSgt(const SgtExpr &)
virtual Action visitAnd(const AndExpr &)
virtual Action visitEq(const EqExpr &)
Not used in canonical form.
Definition: Expr.h:155
virtual Action visitSlt(const SltExpr &)
virtual Action visitExpr(const Expr &)
Class representing an if-then-else expression.
Definition: Expr.h:726
virtual Action visitRead(const ReadExpr &)
virtual Action visitSelect(const SelectExpr &)
Not used in canonical form.
Definition: Expr.h:154
Class representing symbolic expressions.
Definition: Expr.h:88
Not used in canonical form.
Definition: Expr.h:158
virtual Action visitNot(const NotExpr &)
virtual ref< Expr > getKid(unsigned i) const =0
virtual Action visitSub(const SubExpr &)
virtual Action visitUgt(const UgtExpr &)
virtual Action visitXor(const XorExpr &)
virtual Action visitExtract(const ExtractExpr &)
virtual Action visitSRem(const SRemExpr &)
virtual Action visitAdd(const AddExpr &)
virtual Action visitSge(const SgeExpr &)
virtual Action visitUDiv(const UDivExpr &)
virtual Action visitOr(const OrExpr &)
virtual Action visitSDiv(const SDivExpr &)
virtual Action visitNe(const NeExpr &)
virtual Action visitUge(const UgeExpr &)
virtual Action visitExprPost(const Expr &)
virtual Kind getKind() const =0
Class representing a one byte read from an array.
Definition: Expr.h:681
virtual Action visitNotOptimized(const NotOptimizedExpr &)
Not used in canonical form.
Definition: Expr.h:159
ref< Expr > visitActual(const ref< Expr > &e)
Definition: ExprVisitor.cpp:40
static Action skipChildren()
Definition: ExprVisitor.h:40
virtual Action visitLShr(const LShrExpr &)
virtual Action visitURem(const URemExpr &)
virtual Action visitSExt(const SExtExpr &)
virtual Action visitZExt(const ZExtExpr &)
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:24
virtual Action visitShl(const ShlExpr &)
virtual Action visitSle(const SleExpr &)