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