1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
//===-- ExprEvaluator.cpp -------------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#include "klee/util/ExprEvaluator.h"
using namespace klee;
ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
unsigned index) {
for (const UpdateNode *un=ul.head; un; un=un->next) {
ref<Expr> ui = visit(un->index);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
if (CE->getConstantValue() == index)
return Action::changeTo(visit(un->value));
} else {
// update index is unknown, so may or may not be index, we
// cannot guarantee value. we can rewrite to read at this
// version though (mostly for debugging).
UpdateList fwd(ul.root, un, 0);
return Action::changeTo(ReadExpr::create(fwd,
ConstantExpr::alloc(index, Expr::Int32)));
}
}
return Action::changeTo(getInitialValue(*ul.root, index));
}
ExprVisitor::Action ExprEvaluator::visitExpr(const Expr &e) {
// Evaluate all constant expressions here, in case they weren't folded in
// construction. Don't do this for reads though, because we want them to go to
// the normal rewrite path.
unsigned N = e.getNumKids();
if (!N || isa<ReadExpr>(e))
return Action::doChildren();
for (unsigned i = 0; i != N; ++i)
if (!isa<ConstantExpr>(e.getKid(i)))
return Action::doChildren();
ref<Expr> Kids[3];
for (unsigned i = 0; i != N; ++i) {
assert(i < 3);
Kids[i] = e.getKid(i);
}
return Action::changeTo(e.rebuild(Kids));
}
ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
ref<Expr> v = visit(re.index);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v)) {
return evalRead(re.updates, CE->getConstantValue());
} else {
return Action::doChildren();
}
}
// we need to check for div by zero during partial evaluation,
// if this occurs then simply ignore the 0 divisor and use the
// original expression.
ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) {
ref<Expr> kids[2] = { visit(e.left),
visit(e.right) };
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(kids[1]))
if (!CE->getConstantValue())
kids[1] = e.right;
if (kids[0]!=e.left || kids[1]!=e.right) {
return Action::changeTo(e.rebuild(kids));
} else {
return Action::skipChildren();
}
}
ExprVisitor::Action ExprEvaluator::visitUDiv(const UDivExpr &e) {
return protectedDivOperation(e);
}
ExprVisitor::Action ExprEvaluator::visitSDiv(const SDivExpr &e) {
return protectedDivOperation(e);
}
ExprVisitor::Action ExprEvaluator::visitURem(const URemExpr &e) {
return protectedDivOperation(e);
}
ExprVisitor::Action ExprEvaluator::visitSRem(const SRemExpr &e) {
return protectedDivOperation(e);
}
|
