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)26ref<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)42ref<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 &)129ExprVisitor::Action ExprVisitor::visitExpr(const Expr&) { 130 return Action::doChildren(); 131 } 132 visitExprPost(const Expr &)133ExprVisitor::Action ExprVisitor::visitExprPost(const Expr&) { 134 return Action::skipChildren(); 135 } 136 visitNotOptimized(const NotOptimizedExpr &)137ExprVisitor::Action ExprVisitor::visitNotOptimized(const NotOptimizedExpr&) { 138 return Action::doChildren(); 139 } 140 visitRead(const ReadExpr &)141ExprVisitor::Action ExprVisitor::visitRead(const ReadExpr&) { 142 return Action::doChildren(); 143 } 144 visitSelect(const SelectExpr &)145ExprVisitor::Action ExprVisitor::visitSelect(const SelectExpr&) { 146 return Action::doChildren(); 147 } 148 visitConcat(const ConcatExpr &)149ExprVisitor::Action ExprVisitor::visitConcat(const ConcatExpr&) { 150 return Action::doChildren(); 151 } 152 visitExtract(const ExtractExpr &)153ExprVisitor::Action ExprVisitor::visitExtract(const ExtractExpr&) { 154 return Action::doChildren(); 155 } 156 visitZExt(const ZExtExpr &)157ExprVisitor::Action ExprVisitor::visitZExt(const ZExtExpr&) { 158 return Action::doChildren(); 159 } 160 visitSExt(const SExtExpr &)161ExprVisitor::Action ExprVisitor::visitSExt(const SExtExpr&) { 162 return Action::doChildren(); 163 } 164 visitAdd(const AddExpr &)165ExprVisitor::Action ExprVisitor::visitAdd(const AddExpr&) { 166 return Action::doChildren(); 167 } 168 visitSub(const SubExpr &)169ExprVisitor::Action ExprVisitor::visitSub(const SubExpr&) { 170 return Action::doChildren(); 171 } 172 visitMul(const MulExpr &)173ExprVisitor::Action ExprVisitor::visitMul(const MulExpr&) { 174 return Action::doChildren(); 175 } 176 visitUDiv(const UDivExpr &)177ExprVisitor::Action ExprVisitor::visitUDiv(const UDivExpr&) { 178 return Action::doChildren(); 179 } 180 visitSDiv(const SDivExpr &)181ExprVisitor::Action ExprVisitor::visitSDiv(const SDivExpr&) { 182 return Action::doChildren(); 183 } 184 visitURem(const URemExpr &)185ExprVisitor::Action ExprVisitor::visitURem(const URemExpr&) { 186 return Action::doChildren(); 187 } 188 visitSRem(const SRemExpr &)189ExprVisitor::Action ExprVisitor::visitSRem(const SRemExpr&) { 190 return Action::doChildren(); 191 } 192 visitNot(const NotExpr &)193ExprVisitor::Action ExprVisitor::visitNot(const NotExpr&) { 194 return Action::doChildren(); 195 } 196 visitAnd(const AndExpr &)197ExprVisitor::Action ExprVisitor::visitAnd(const AndExpr&) { 198 return Action::doChildren(); 199 } 200 visitOr(const OrExpr &)201ExprVisitor::Action ExprVisitor::visitOr(const OrExpr&) { 202 return Action::doChildren(); 203 } 204 visitXor(const XorExpr &)205ExprVisitor::Action ExprVisitor::visitXor(const XorExpr&) { 206 return Action::doChildren(); 207 } 208 visitShl(const ShlExpr &)209ExprVisitor::Action ExprVisitor::visitShl(const ShlExpr&) { 210 return Action::doChildren(); 211 } 212 visitLShr(const LShrExpr &)213ExprVisitor::Action ExprVisitor::visitLShr(const LShrExpr&) { 214 return Action::doChildren(); 215 } 216 visitAShr(const AShrExpr &)217ExprVisitor::Action ExprVisitor::visitAShr(const AShrExpr&) { 218 return Action::doChildren(); 219 } 220 visitEq(const EqExpr &)221ExprVisitor::Action ExprVisitor::visitEq(const EqExpr&) { 222 return Action::doChildren(); 223 } 224 visitNe(const NeExpr &)225ExprVisitor::Action ExprVisitor::visitNe(const NeExpr&) { 226 return Action::doChildren(); 227 } 228 visitUlt(const UltExpr &)229ExprVisitor::Action ExprVisitor::visitUlt(const UltExpr&) { 230 return Action::doChildren(); 231 } 232 visitUle(const UleExpr &)233ExprVisitor::Action ExprVisitor::visitUle(const UleExpr&) { 234 return Action::doChildren(); 235 } 236 visitUgt(const UgtExpr &)237ExprVisitor::Action ExprVisitor::visitUgt(const UgtExpr&) { 238 return Action::doChildren(); 239 } 240 visitUge(const UgeExpr &)241ExprVisitor::Action ExprVisitor::visitUge(const UgeExpr&) { 242 return Action::doChildren(); 243 } 244 visitSlt(const SltExpr &)245ExprVisitor::Action ExprVisitor::visitSlt(const SltExpr&) { 246 return Action::doChildren(); 247 } 248 visitSle(const SleExpr &)249ExprVisitor::Action ExprVisitor::visitSle(const SleExpr&) { 250 return Action::doChildren(); 251 } 252 visitSgt(const SgtExpr &)253ExprVisitor::Action ExprVisitor::visitSgt(const SgtExpr&) { 254 return Action::doChildren(); 255 } 256 visitSge(const SgeExpr &)257ExprVisitor::Action ExprVisitor::visitSge(const SgeExpr&) { 258 return Action::doChildren(); 259 } 260 261