Skip to content

Commit 787d94d

Browse files
committed
Small fix
1 parent add9e41 commit 787d94d

File tree

3 files changed

+35
-17
lines changed

3 files changed

+35
-17
lines changed

include/klee/Expr/Expr.h

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,8 @@ class Expr {
183183

184184
static const Width Fl80 = 80;
185185

186+
static const Width TaintWidth = 64;
187+
186188
enum States { Undefined, True, False };
187189

188190
enum Kind {
@@ -414,6 +416,8 @@ class Expr {
414416
static ref<ConstantExpr> createFalse();
415417

416418
static ref<ConstantExpr> createEmptyTaint();
419+
static ref<Expr> combineTaints(const ref<Expr> &taintL,
420+
const ref<Expr> &taintR);
417421

418422
/// Create a little endian read of the given type at offset 0 of the
419423
/// given object.
@@ -1684,9 +1688,8 @@ class PointerExpr : public NonConstantExpr {
16841688
ref<Expr> value;
16851689
ref<Expr> taint;
16861690

1687-
static ref<Expr>
1688-
alloc(const ref<Expr> &b, const ref<Expr> &v,
1689-
const ref<Expr> &t = createEmptyTaint()) {
1691+
static ref<Expr> alloc(const ref<Expr> &b, const ref<Expr> &v,
1692+
const ref<Expr> &t = createEmptyTaint()) {
16901693
ref<Expr> r(new PointerExpr(b, v, t));
16911694
r->computeHash();
16921695
r->computeHeight();
@@ -1734,8 +1737,8 @@ class PointerExpr : public NonConstantExpr {
17341737

17351738
bool isKnownValue() const { return getBase()->isZero(); }
17361739

1737-
ref<Expr> combineTaints(const ref<PointerExpr> &RHS) {
1738-
return OrExpr::create(getTaint(), RHS->getTaint());
1740+
ref<ConstantExpr> combineTaints(const ref<PointerExpr> &RHS) {
1741+
return Expr::combineTaints(getTaint(), RHS->getTaint());
17391742
}
17401743

17411744
ref<Expr> Add(const ref<PointerExpr> &RHS);
@@ -1783,9 +1786,9 @@ class ConstantPointerExpr : public PointerExpr {
17831786
r->computeHeight();
17841787
return r;
17851788
}
1786-
static ref<Expr>
1787-
create(const ref<ConstantExpr> &b, const ref<ConstantExpr> &v,
1788-
const ref<ConstantExpr> &t = createEmptyTaint());
1789+
static ref<Expr> create(const ref<ConstantExpr> &b,
1790+
const ref<ConstantExpr> &v,
1791+
const ref<ConstantExpr> &t = createEmptyTaint());
17891792

17901793
Kind getKind() const { return Expr::ConstantPointer; }
17911794

lib/Core/SpecialFunctionHandler.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -808,7 +808,8 @@ void SpecialFunctionHandler::handleRealloc(ExecutionState &state,
808808
if (zeroSize.first) { // size == 0
809809
executor.executeFree(*zeroSize.first,
810810
PointerExpr::create(addressPointer->getValue(),
811-
addressPointer->getValue()),
811+
addressPointer->getValue(),
812+
addressPointer->getTaint()),
812813
target);
813814
}
814815
if (zeroSize.second) { // size != 0
@@ -1278,11 +1279,8 @@ void SpecialFunctionHandler::handleTaintHit(klee::ExecutionState &state,
12781279
return;
12791280
}
12801281

1281-
char *end = nullptr;
1282-
size_t rule = strtoul(arguments[0]->toString().c_str(), &end, 10);
1283-
if (*end != '\0' || errno == ERANGE) {
1284-
executor.terminateStateOnUserError(
1285-
state, "Incorrect argument 0 to klee_taint_hit(size_t)");
1286-
}
1287-
executor.terminateStateOnTargetTaintError(state, rule);
1282+
// printf("klee_taint_hit for rule: %s\n", arguments[0]->toString().c_str());
1283+
1284+
executor.terminateStateOnTargetTaintError(
1285+
state, dyn_cast<ConstantExpr>(arguments[0])->getZExtValue());
12881286
}

lib/Expr/Expr.cpp

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -553,6 +553,23 @@ ref<ConstantExpr> Expr::createEmptyTaint() {
553553
return ConstantExpr::create(0, Expr::Int64);
554554
}
555555

556+
ref<Expr> Expr::combineTaints(const ref<Expr> &taintL,
557+
const ref<Expr> &taintR) {
558+
if (SelectExpr *sel = dyn_cast<SelectExpr>(taintL)) {
559+
taintL->dump();
560+
}
561+
if (PointerExpr *sel = dyn_cast<PointerExpr>(taintL)) {
562+
taintR->dump();
563+
}
564+
if (ConstantExpr *sel = dyn_cast<ConstantExpr>(taintL)) {
565+
if (ConstantExpr *ser = dyn_cast<ConstantExpr>(taintR)) {
566+
sel->getAPValue().dump();
567+
ser->getAPValue().dump();
568+
}
569+
}
570+
return OrExpr::create(taintL, taintR);
571+
}
572+
556573
Expr::ByteWidth Expr::getByteWidth() const {
557574
return (getWidth() + CHAR_BIT - 1) / CHAR_BIT;
558575
}
@@ -2974,7 +2991,7 @@ ref<Expr> ConstantPointerExpr::create(const ref<ConstantExpr> &b,
29742991
combineTaints(RHS)); \
29752992
} else { \
29762993
auto value = _e_op::create(getValue(), RHS->getValue()); \
2977-
if (getTaint().isNull() && RHS->getTaint().isNull()) { \
2994+
if (getTaint()->isZero() && RHS->getTaint()->isZero()) { \
29782995
return value; \
29792996
} else { \
29802997
return PointerExpr::create(ConstantExpr::create(0, value->getWidth()), \

0 commit comments

Comments
 (0)