Skip to content

Commit add9e41

Browse files
mamaria-kmamaria-k
committed
Add taint for PointerExpr
1 parent 036c02e commit add9e41

File tree

2 files changed

+115
-43
lines changed

2 files changed

+115
-43
lines changed

‎include/klee/Expr/Expr.h‎

Lines changed: 40 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -413,6 +413,8 @@ class Expr {
413413
static ref<ConstantExpr> createTrue();
414414
static ref<ConstantExpr> createFalse();
415415

416+
static ref<ConstantExpr> createEmptyTaint();
417+
416418
/// Create a little endian read of the given type at offset 0 of the
417419
/// given object.
418420
static ref<Expr> createTempRead(const Array *array, Expr::Width w,
@@ -1676,25 +1678,33 @@ class ConstantExpr : public Expr {
16761678
class PointerExpr : public NonConstantExpr {
16771679
public:
16781680
static const Kind kind = Expr::Pointer;
1679-
static const unsigned numKids = 2;
1681+
static const unsigned numKids = 3;
1682+
16801683
ref<Expr> base;
16811684
ref<Expr> value;
1682-
static ref<Expr> alloc(const ref<Expr> &b, const ref<Expr> &v) {
1683-
ref<Expr> r(new PointerExpr(b, v));
1685+
ref<Expr> taint;
1686+
1687+
static ref<Expr>
1688+
alloc(const ref<Expr> &b, const ref<Expr> &v,
1689+
const ref<Expr> &t = createEmptyTaint()) {
1690+
ref<Expr> r(new PointerExpr(b, v, t));
16841691
r->computeHash();
16851692
r->computeHeight();
16861693
return r;
16871694
}
1688-
static ref<Expr> create(const ref<Expr> &b, const ref<Expr> &o);
1689-
static ref<Expr> create(const ref<Expr> &v);
1695+
static ref<Expr> create(const ref<Expr> &b, const ref<Expr> &v,
1696+
const ref<Expr> &t = createEmptyTaint());
1697+
static ref<Expr> create(const ref<Expr> &expr);
16901698
static ref<Expr> createSymbolic(const ref<Expr> &expr,
16911699
const ref<ReadExpr> &pointer,
16921700
const ref<Expr> &off);
16931701

16941702
Width getWidth() const { return value->getWidth(); }
16951703
Kind getKind() const { return Expr::Pointer; }
1704+
16961705
ref<Expr> getBase() const { return base; }
16971706
ref<Expr> getValue() const { return value; }
1707+
ref<Expr> getTaint() const { return taint; }
16981708
ref<Expr> getOffset() const {
16991709
assert(value->getWidth() == base->getWidth() &&
17001710
"Invalid getOffset() call!");
@@ -1707,12 +1717,14 @@ class PointerExpr : public NonConstantExpr {
17071717
return base;
17081718
if (i == 1)
17091719
return value;
1720+
if (i == 2)
1721+
return taint;
17101722
return 0;
17111723
}
17121724

17131725
int compareContents(const Expr &b) const { return 0; }
17141726
virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
1715-
return create(kids[0], kids[1]);
1727+
return create(kids[0], kids[1], kids[2]);
17161728
}
17171729
static bool classof(const Expr *E) {
17181730
return E->getKind() == Expr::Pointer ||
@@ -1722,6 +1734,10 @@ class PointerExpr : public NonConstantExpr {
17221734

17231735
bool isKnownValue() const { return getBase()->isZero(); }
17241736

1737+
ref<Expr> combineTaints(const ref<PointerExpr> &RHS) {
1738+
return OrExpr::create(getTaint(), RHS->getTaint());
1739+
}
1740+
17251741
ref<Expr> Add(const ref<PointerExpr> &RHS);
17261742
ref<Expr> Sub(const ref<PointerExpr> &RHS);
17271743
ref<Expr> Mul(const ref<PointerExpr> &RHS);
@@ -1750,40 +1766,49 @@ class PointerExpr : public NonConstantExpr {
17501766
ref<Expr> Not();
17511767

17521768
protected:
1753-
PointerExpr(const ref<Expr> &b, const ref<Expr> &v) : base(b), value(v) {}
1769+
PointerExpr(const ref<Expr> &b, const ref<Expr> &v, const ref<Expr> &t)
1770+
: base(b), value(v), taint(t) {}
17541771
};
17551772

17561773
class ConstantPointerExpr : public PointerExpr {
17571774
public:
17581775
static const Kind kind = Expr::ConstantPointer;
1759-
static const unsigned numKids = 2;
1760-
static ref<ConstantPointerExpr> alloc(const ref<ConstantExpr> &b,
1761-
const ref<ConstantExpr> &o) {
1762-
ref<ConstantPointerExpr> r = new ConstantPointerExpr(b, o);
1776+
static const unsigned numKids = 3;
1777+
1778+
static ref<ConstantPointerExpr>
1779+
alloc(const ref<ConstantExpr> &b, const ref<ConstantExpr> &v,
1780+
const ref<ConstantExpr> &t = createEmptyTaint()) {
1781+
ref<ConstantPointerExpr> r = new ConstantPointerExpr(b, v, t);
17631782
r->computeHash();
17641783
r->computeHeight();
17651784
return r;
17661785
}
1767-
static ref<Expr> create(const ref<ConstantExpr> &b,
1768-
const ref<ConstantExpr> &o);
1786+
static ref<Expr>
1787+
create(const ref<ConstantExpr> &b, const ref<ConstantExpr> &v,
1788+
const ref<ConstantExpr> &t = createEmptyTaint());
17691789

17701790
Kind getKind() const { return Expr::ConstantPointer; }
1791+
17711792
ref<ConstantExpr> getConstantBase() const { return cast<ConstantExpr>(base); }
17721793
ref<ConstantExpr> getConstantOffset() const {
17731794
return getConstantValue()->Sub(getConstantBase());
17741795
}
17751796
ref<ConstantExpr> getConstantValue() const {
17761797
return cast<ConstantExpr>(value);
17771798
}
1799+
ref<ConstantExpr> getConstantTaint() const {
1800+
return cast<ConstantExpr>(taint);
1801+
}
17781802

17791803
static bool classof(const Expr *E) {
17801804
return E->getKind() == Expr::ConstantPointer;
17811805
}
17821806
static bool classof(const ConstantPointerExpr *) { return true; }
17831807

17841808
private:
1785-
ConstantPointerExpr(const ref<ConstantExpr> &b, const ref<ConstantExpr> &v)
1786-
: PointerExpr(b, v) {}
1809+
ConstantPointerExpr(const ref<ConstantExpr> &b, const ref<ConstantExpr> &v,
1810+
const ref<ConstantExpr> &t)
1811+
: PointerExpr(b, v, t) {}
17871812
};
17881813

17891814
// Implementations

‎lib/Expr/Expr.cpp‎

Lines changed: 75 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -549,6 +549,10 @@ ref<ConstantExpr> Expr::createFalse() {
549549
return ConstantExpr::create(0, Expr::Bool);
550550
}
551551

552+
ref<ConstantExpr> Expr::createEmptyTaint() {
553+
return ConstantExpr::create(0, Expr::Int64);
554+
}
555+
552556
Expr::ByteWidth Expr::getByteWidth() const {
553557
return (getWidth() + CHAR_BIT - 1) / CHAR_BIT;
554558
}
@@ -1694,7 +1698,25 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
16941698
SelectExpr::create(c, truePointer->getBase(), falsePointer->getBase());
16951699
ref<Expr> value = SelectExpr::create(c, truePointer->getValue(),
16961700
falsePointer->getValue());
1697-
return PointerExpr::create(base, value);
1701+
ref<Expr> taint = SelectExpr::create(c, truePointer->getTaint(),
1702+
falsePointer->getTaint());
1703+
return PointerExpr::create(base, value, taint);
1704+
} else if (isa<PointerExpr>(t) && !isa<PointerExpr>(f)) {
1705+
ref<PointerExpr> truePointer = cast<PointerExpr>(t);
1706+
ref<Expr> base = SelectExpr::create(c, truePointer->getBase(),
1707+
ConstantExpr::create(0, f->getWidth()));
1708+
ref<Expr> value = SelectExpr::create(c, truePointer->getValue(), f);
1709+
ref<Expr> taint =
1710+
SelectExpr::create(c, truePointer->getTaint(), createEmptyTaint());
1711+
return PointerExpr::create(base, value, taint);
1712+
} else if (!isa<PointerExpr>(t) && isa<PointerExpr>(f)) {
1713+
ref<PointerExpr> falsePointer = cast<PointerExpr>(f);
1714+
ref<Expr> base = SelectExpr::create(
1715+
c, ConstantExpr::create(0, t->getWidth()), falsePointer->getBase());
1716+
ref<Expr> value = SelectExpr::create(c, t, falsePointer->getValue());
1717+
ref<Expr> taint =
1718+
SelectExpr::create(c, createEmptyTaint(), falsePointer->getTaint());
1719+
return PointerExpr::create(base, value, taint);
16981720
} else if (!isa<ConstantExpr>(t) && isa<ConstantExpr>(f)) {
16991721
return SelectExpr::alloc(Expr::createIsZero(c), f, t);
17001722
}
@@ -1797,7 +1819,8 @@ ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
17971819
if (PointerExpr *ee_right = dyn_cast<PointerExpr>(r)) {
17981820
return PointerExpr::create(
17991821
convolution(ee_left->getBase(), ee_right->getBase()),
1800-
ConcatExpr::create(ee_left->getValue(), ee_right->getValue()));
1822+
ConcatExpr::create(ee_left->getValue(), ee_right->getValue()),
1823+
ee_left->combineTaints(ee_right));
18011824
}
18021825
}
18031826

@@ -1849,7 +1872,8 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
18491872
return CE->Extract(off, w);
18501873
} else if (PointerExpr *pe = dyn_cast<PointerExpr>(expr)) {
18511874
return PointerExpr::create(pe->getBase(),
1852-
ExtractExpr::create(pe->getValue(), off, w));
1875+
ExtractExpr::create(pe->getValue(), off, w),
1876+
pe->getTaint());
18531877
} else {
18541878
// Extract(Concat)
18551879
if (ConcatExpr *ce = dyn_cast<ConcatExpr>(expr)) {
@@ -1916,8 +1940,8 @@ ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
19161940
} else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
19171941
return CE->ZExt(w);
19181942
} else if (PointerExpr *pe = dyn_cast<PointerExpr>(e)) {
1919-
return PointerExpr::create(pe->getBase(),
1920-
ZExtExpr::create(pe->getValue(), w));
1943+
return PointerExpr::create(
1944+
pe->getBase(), ZExtExpr::create(pe->getValue(), w), pe->getTaint());
19211945
} else if (SelectExpr *se = dyn_cast<SelectExpr>(e)) {
19221946
if (isa<ConstantExpr>(se->trueExpr)) {
19231947
return SelectExpr::create(se->cond, ZExtExpr::create(se->trueExpr, w),
@@ -1937,8 +1961,8 @@ ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
19371961
} else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
19381962
return CE->SExt(w);
19391963
} else if (PointerExpr *pe = dyn_cast<PointerExpr>(e)) {
1940-
return PointerExpr::create(pe->getBase(),
1941-
SExtExpr::create(pe->getValue(), w));
1964+
return PointerExpr::create(
1965+
pe->getBase(), SExtExpr::create(pe->getValue(), w), pe->getTaint());
19421966
} else if (SelectExpr *se = dyn_cast<SelectExpr>(e)) {
19431967
if (isa<ConstantExpr>(se->trueExpr)) {
19441968
return SelectExpr::create(se->cond, SExtExpr::create(se->trueExpr, w),
@@ -2049,7 +2073,8 @@ static ref<Expr> AddExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
20492073
}
20502074

20512075
static ref<Expr> AddExpr_createPointerR(const ref<PointerExpr> &pl, Expr *r) {
2052-
return PointerExpr::create(pl->getBase(), AddExpr::create(pl->getValue(), r));
2076+
return PointerExpr::create(pl->getBase(), AddExpr::create(pl->getValue(), r),
2077+
pl->getTaint());
20532078
}
20542079

20552080
static ref<Expr> AddExpr_createPointer(Expr *l, const ref<PointerExpr> &pr) {
@@ -2110,11 +2135,13 @@ static ref<Expr> SubExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
21102135
}
21112136

21122137
static ref<Expr> SubExpr_createPointerR(const ref<PointerExpr> &pl, Expr *r) {
2113-
return PointerExpr::create(pl->getBase(), SubExpr::create(pl->getValue(), r));
2138+
return PointerExpr::create(pl->getBase(), SubExpr::create(pl->getValue(), r),
2139+
pl->getTaint());
21142140
}
21152141

21162142
static ref<Expr> SubExpr_createPointer(Expr *l, const ref<PointerExpr> &pr) {
2117-
return PointerExpr::create(pr->getBase(), SubExpr::create(l, pr->getValue()));
2143+
return PointerExpr::create(pr->getBase(), SubExpr::create(l, pr->getValue()),
2144+
pr->getTaint());
21182145
}
21192146

21202147
static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
@@ -2174,7 +2201,8 @@ static ref<Expr> MulExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
21742201
}
21752202

21762203
static ref<Expr> MulExpr_createPointerR(const ref<PointerExpr> &pl, Expr *r) {
2177-
return PointerExpr::create(pl->getBase(), MulExpr::create(pl->getValue(), r));
2204+
return PointerExpr::create(pl->getBase(), MulExpr::create(pl->getValue(), r),
2205+
pl->getTaint());
21782206
}
21792207

21802208
static ref<Expr> MulExpr_createPointer(Expr *l, const ref<PointerExpr> &pr) {
@@ -2205,7 +2233,8 @@ static ref<Expr> AndExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
22052233
}
22062234

22072235
static ref<Expr> AndExpr_createPointerR(const ref<PointerExpr> &pl, Expr *r) {
2208-
return PointerExpr::create(pl->getBase(), AndExpr::create(pl->getValue(), r));
2236+
return PointerExpr::create(pl->getBase(), AndExpr::create(pl->getValue(), r),
2237+
pl->getTaint());
22092238
}
22102239

22112240
static ref<Expr> AndExpr_createPointer(Expr *l, const ref<PointerExpr> &pr) {
@@ -2233,7 +2262,8 @@ static ref<Expr> OrExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
22332262
}
22342263

22352264
static ref<Expr> OrExpr_createPointerR(const ref<PointerExpr> &pl, Expr *r) {
2236-
return PointerExpr::create(pl->getBase(), OrExpr::create(pl->getValue(), r));
2265+
return PointerExpr::create(pl->getBase(), OrExpr::create(pl->getValue(), r),
2266+
pl->getTaint());
22372267
}
22382268

22392269
static ref<Expr> OrExpr_createPointer(Expr *l, const ref<PointerExpr> &pr) {
@@ -2262,7 +2292,8 @@ static ref<Expr> XorExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
22622292
}
22632293

22642294
static ref<Expr> XorExpr_createPointerR(const ref<PointerExpr> &pl, Expr *r) {
2265-
return PointerExpr::create(pl->getBase(), XorExpr::create(pl->getValue(), r));
2295+
return PointerExpr::create(pl->getBase(), XorExpr::create(pl->getValue(), r),
2296+
pl->getTaint());
22662297
}
22672298

22682299
static ref<Expr> XorExpr_createPointer(Expr *l, const ref<PointerExpr> &pr) {
@@ -2424,9 +2455,11 @@ static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
24242455
if (PointerExpr *pl = dyn_cast<PointerExpr>(l)) { \
24252456
if (PointerExpr *pr = dyn_cast<PointerExpr>(r)) \
24262457
return pl->_op(pr); \
2427-
return _e_op::create(pl->getValue(), r); \
2458+
return PointerExpr::create( \
2459+
pl->getBase(), _e_op::create(pl->getValue(), r), pl->getTaint()); \
24282460
} else if (PointerExpr *pr = dyn_cast<PointerExpr>(r)) { \
2429-
return _e_op::create(l, pr->getValue()); \
2461+
return PointerExpr::create( \
2462+
pr->getBase(), _e_op::create(l, pr->getValue()), pr->getTaint()); \
24302463
} \
24312464
if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) \
24322465
if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
@@ -2864,14 +2897,17 @@ ref<Expr> IsSubnormalExpr::either(const ref<Expr> &e0, const ref<Expr> &e1) {
28642897

28652898
/***/
28662899

2867-
ref<Expr> PointerExpr::create(const ref<Expr> &b, const ref<Expr> &v) {
2900+
ref<Expr> PointerExpr::create(const ref<Expr> &b, const ref<Expr> &v,
2901+
const ref<Expr> &t) {
28682902
assert(!isa<PointerExpr>(b));
28692903
assert(!isa<PointerExpr>(v));
2870-
if (isa<ConstantExpr>(b) && isa<ConstantExpr>(v)) {
2871-
return ConstantPointerExpr::create(cast<ConstantExpr>(b),
2872-
cast<ConstantExpr>(v));
2904+
assert(!isa<PointerExpr>(t));
2905+
2906+
if (isa<ConstantExpr>(b) && isa<ConstantExpr>(v) && isa<ConstantExpr>(t)) {
2907+
return ConstantPointerExpr::create(
2908+
cast<ConstantExpr>(b), cast<ConstantExpr>(v), cast<ConstantExpr>(t));
28732909
} else {
2874-
return PointerExpr::alloc(b, v);
2910+
return PointerExpr::alloc(b, v, t);
28752911
}
28762912
}
28772913

@@ -2913,10 +2949,12 @@ ref<Expr> PointerExpr::create(const ref<Expr> &expr) {
29132949
}
29142950

29152951
ref<Expr> ConstantPointerExpr::create(const ref<ConstantExpr> &b,
2916-
const ref<ConstantExpr> &v) {
2952+
const ref<ConstantExpr> &v,
2953+
const ref<ConstantExpr> &t) {
29172954
assert(!isa<PointerExpr>(b));
29182955
assert(!isa<PointerExpr>(v));
2919-
return ConstantPointerExpr::alloc(b, v);
2956+
assert(!isa<PointerExpr>(t));
2957+
return ConstantPointerExpr::alloc(b, v, t);
29202958
}
29212959

29222960
#define BCREATE_P(_e_op, _op) \
@@ -2926,14 +2964,22 @@ ref<Expr> ConstantPointerExpr::create(const ref<ConstantExpr> &b,
29262964
if (!RHS->isKnownValue()) { \
29272965
return _e_op::create(getValue(), RHS->getValue()); \
29282966
} else { \
2929-
return PointerExpr::create( \
2930-
getBase(), _e_op::create(getValue(), RHS->getValue())); \
2967+
return PointerExpr::create(getBase(), \
2968+
_e_op::create(getValue(), RHS->getValue()), \
2969+
combineTaints(RHS)); \
29312970
} \
29322971
} else if (!RHS->isKnownValue()) { \
29332972
return PointerExpr::create(RHS->getBase(), \
2934-
_e_op::create(getValue(), RHS->getValue())); \
2973+
_e_op::create(getValue(), RHS->getValue()), \
2974+
combineTaints(RHS)); \
29352975
} else { \
2936-
return _e_op::create(getValue(), RHS->getValue()); \
2976+
auto value = _e_op::create(getValue(), RHS->getValue()); \
2977+
if (getTaint().isNull() && RHS->getTaint().isNull()) { \
2978+
return value; \
2979+
} else { \
2980+
return PointerExpr::create(ConstantExpr::create(0, value->getWidth()), \
2981+
value, combineTaints(RHS)); \
2982+
} \
29372983
} \
29382984
}
29392985

@@ -2952,7 +2998,8 @@ BCREATE_P(LShrExpr, LShr)
29522998
BCREATE_P(AShrExpr, AShr)
29532999

29543000
ref<Expr> PointerExpr::Not() {
2955-
return PointerExpr::create(getBase(), NotExpr::create(getValue()));
3001+
return PointerExpr::create(getBase(), NotExpr::create(getValue()),
3002+
getTaint());
29563003
}
29573004

29583005
ref<Expr> PointerExpr::Eq(const ref<PointerExpr> &RHS) {

0 commit comments

Comments
 (0)