klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprEvaluator.cpp
Go to the documentation of this file.
1 //===-- ExprEvaluator.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 
11 
12 using namespace klee;
13 
15  unsigned index) {
16  for (const UpdateNode *un=ul.head; un; un=un->next) {
17  ref<Expr> ui = visit(un->index);
18 
19  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
20  if (CE->getZExtValue() == index)
21  return Action::changeTo(visit(un->value));
22  } else {
23  // update index is unknown, so may or may not be index, we
24  // cannot guarantee value. we can rewrite to read at this
25  // version though (mostly for debugging).
26 
28  ConstantExpr::alloc(index,
29  ul.root->getDomain())));
30  }
31  }
32 
33  if (ul.root->isConstantArray() && index < ul.root->size)
34  return Action::changeTo(ul.root->constantValues[index]);
35 
36  return Action::changeTo(getInitialValue(*ul.root, index));
37 }
38 
40  // Evaluate all constant expressions here, in case they weren't folded in
41  // construction. Don't do this for reads though, because we want them to go to
42  // the normal rewrite path.
43  unsigned N = e.getNumKids();
44  if (!N || isa<ReadExpr>(e))
45  return Action::doChildren();
46 
47  for (unsigned i = 0; i != N; ++i)
48  if (!isa<ConstantExpr>(e.getKid(i)))
49  return Action::doChildren();
50 
51  ref<Expr> Kids[3];
52  for (unsigned i = 0; i != N; ++i) {
53  assert(i < 3);
54  Kids[i] = e.getKid(i);
55  }
56 
57  return Action::changeTo(e.rebuild(Kids));
58 }
59 
61  ref<Expr> v = visit(re.index);
62 
63  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v)) {
64  return evalRead(re.updates, CE->getZExtValue());
65  } else {
66  return Action::doChildren();
67  }
68 }
69 
70 // we need to check for div by zero during partial evaluation,
71 // if this occurs then simply ignore the 0 divisor and use the
72 // original expression.
74  ref<Expr> kids[2] = { visit(e.left),
75  visit(e.right) };
76 
77  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(kids[1]))
78  if (CE->isZero())
79  kids[1] = e.right;
80 
81  if (kids[0]!=e.left || kids[1]!=e.right) {
82  return Action::changeTo(e.rebuild(kids));
83  } else {
84  return Action::skipChildren();
85  }
86 }
87 
89  return protectedDivOperation(e);
90 }
92  return protectedDivOperation(e);
93 }
95  return protectedDivOperation(e);
96 }
98  return protectedDivOperation(e);
99 }
Action visitSRem(const SRemExpr &e)
ref< Expr > left
Definition: Expr.h:494
virtual ref< Expr > rebuild(ref< Expr > kids[]) const =0
virtual unsigned getNumKids() const =0
static Action doChildren()
Definition: ExprVisitor.h:39
unsigned size
Definition: Expr.h:605
Action visitExpr(const Expr &e)
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:499
static Action changeTo(const ref< Expr > &expr)
Definition: ExprVisitor.h:36
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
Class representing a complete list of updates into an array.
Definition: Expr.h:655
UpdateList updates
Definition: Expr.h:687
Class representing symbolic expressions.
Definition: Expr.h:88
Action visitURem(const URemExpr &e)
virtual ref< Expr > getKid(unsigned i) const =0
Action protectedDivOperation(const BinaryExpr &e)
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
Action visitRead(const ReadExpr &re)
Action visitSDiv(const SDivExpr &e)
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
Action evalRead(const UpdateList &ul, unsigned index)
virtual ref< Expr > getInitialValue(const Array &os, unsigned index)=0
ref< Expr > right
Definition: Expr.h:494
Action visitUDiv(const UDivExpr &e)
const UpdateNode * next
Definition: Expr.h:577
bool isConstantArray() const
Definition: Expr.h:642
Expr::Width getDomain() const
Definition: Expr.h:644
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
Class representing a byte update of an array.
Definition: Expr.h:569
static Action skipChildren()
Definition: ExprVisitor.h:40
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:24