Skip to content

Commit 238fa5e

Browse files
committed
Add taint to lazy object init and small methods
1 parent 202f6cf commit 238fa5e

File tree

8 files changed

+35
-16
lines changed

8 files changed

+35
-16
lines changed

include/klee/Core/BranchTypes.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,8 @@
2525
BTYPE(Realloc, 8U) \
2626
BTYPE(Free, 9U) \
2727
BTYPE(GetVal, 10U) \
28-
BMARK(END, 10U)
28+
BTYPE(Taint, 11U) \
29+
BMARK(END, 11U)
2930
/// \endcond
3031

3132
/** @enum BranchType

include/klee/Expr/Expr.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -416,6 +416,7 @@ class Expr {
416416
static ref<ConstantExpr> createFalse();
417417

418418
static ref<ConstantExpr> createEmptyTaint();
419+
static ref<ConstantExpr> createTaintBySource(uint64_t source);
419420
static ref<Expr> combineTaints(const ref<Expr> &taintL,
420421
const ref<Expr> &taintR);
421422

lib/Core/AddressSpace.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99

1010
#include "AddressSpace.h"
1111

12+
#include <utility>
13+
1214
#include "ExecutionState.h"
1315
#include "Memory.h"
1416
#include "TimingSolver.h"
@@ -80,19 +82,21 @@ ObjectPair AddressSpace::findObject(const MemoryObject *mo) const {
8082
: ObjectPair(nullptr, nullptr);
8183
}
8284

83-
RefObjectPair AddressSpace::lazyInitializeObject(const MemoryObject *mo) const {
84-
return RefObjectPair(mo, new ObjectState(mo, mo->content, mo->type));
85+
RefObjectPair AddressSpace::lazyInitializeObject(const MemoryObject *mo,
86+
ref<Expr> taint) const {
87+
return RefObjectPair(
88+
mo, new ObjectState(mo, mo->content, mo->type, std::move(taint)));
8589
}
8690

87-
RefObjectPair
88-
AddressSpace::findOrLazyInitializeObject(const MemoryObject *mo) const {
91+
RefObjectPair AddressSpace::findOrLazyInitializeObject(const MemoryObject *mo,
92+
ref<Expr> taint) const {
8993
ObjectPair op = findObject(mo);
9094
if (op.first && op.second) {
9195
return RefObjectPair(op.first, op.second);
9296
}
9397
assert(!op.first && !op.second);
9498
if (mo->isLazyInitialized) {
95-
return lazyInitializeObject(mo);
99+
return lazyInitializeObject(mo, std::move(taint));
96100
}
97101
return RefObjectPair(nullptr, nullptr);
98102
}

lib/Core/AddressSpace.h

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,8 +136,11 @@ class AddressSpace {
136136

137137
/// Lookup a binding from a MemoryObject.
138138
ObjectPair findObject(const MemoryObject *mo) const;
139-
RefObjectPair lazyInitializeObject(const MemoryObject *mo) const;
140-
RefObjectPair findOrLazyInitializeObject(const MemoryObject *mo) const;
139+
RefObjectPair lazyInitializeObject(const MemoryObject *mo,
140+
ref<Expr> taint) const;
141+
RefObjectPair
142+
findOrLazyInitializeObject(const MemoryObject *mo,
143+
ref<Expr> taint = Expr::createEmptyTaint()) const;
141144

142145
/// Copy the concrete values of all managed ObjectStates into the
143146
/// actual system memory location they were allocated at.

lib/Core/Executor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5985,7 +5985,7 @@ bool Executor::resolveMemoryObjects(
59855985
state, basePointer, target, baseTargetType, minObjectSize, sizeExpr,
59865986
false, checkOutOfBounds, UseSymbolicSizeLazyInit);
59875987
RefObjectPair op = state.addressSpace.findOrLazyInitializeObject(
5988-
idLazyInitialization.get());
5988+
idLazyInitialization.get(), address->getTaint());
59895989
state.addressSpace.bindObject(op.first, op.second.get());
59905990
mayBeResolvedMemoryObjects.push_back(idLazyInitialization);
59915991
}

lib/Core/Memory.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -106,22 +106,26 @@ std::string MemoryObject::getAllocInfo() const {
106106

107107
/***/
108108

109-
ObjectState::ObjectState(const MemoryObject *mo, const Array *array, KType *dt)
109+
ObjectState::ObjectState(const MemoryObject *mo, const Array *array, KType *dt,
110+
ref<Expr> defaultTaintValue)
110111
: copyOnWriteOwner(0), object(mo), valueOS(ObjectStage(array, nullptr)),
111112
baseOS(ObjectStage(array->size, Expr::createPointer(0), false,
112113
Context::get().getPointerWidth())),
113-
taintOS(ObjectStage(array->size, Expr::createEmptyTaint(), false, Expr::TaintWidth)),
114+
taintOS(
115+
ObjectStage(array->size, defaultTaintValue, false, Expr::TaintWidth)),
114116
lastUpdate(nullptr), size(array->size), dynamicType(dt), readOnly(false) {
115117
baseOS.initializeToZero();
116118
taintOS.initializeToZero();
117119
}
118120

119-
ObjectState::ObjectState(const MemoryObject *mo, KType *dt)
121+
ObjectState::ObjectState(const MemoryObject *mo, KType *dt,
122+
ref<Expr> defaultTaintValue)
120123
: copyOnWriteOwner(0), object(mo),
121124
valueOS(ObjectStage(mo->getSizeExpr(), nullptr)),
122125
baseOS(ObjectStage(mo->getSizeExpr(), Expr::createPointer(0), false,
123126
Context::get().getPointerWidth())),
124-
taintOS(ObjectStage(mo->getSizeExpr(), Expr::createEmptyTaint(), false, Expr::TaintWidth)),
127+
taintOS(ObjectStage(mo->getSizeExpr(), defaultTaintValue, false,
128+
Expr::TaintWidth)),
125129
lastUpdate(nullptr), size(mo->getSizeExpr()), dynamicType(dt),
126130
readOnly(false) {
127131
baseOS.initializeToZero();

lib/Core/Memory.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -310,8 +310,10 @@ class ObjectState {
310310

311311
/// Create a new object state for the given memory
312312
// For objects in memory
313-
ObjectState(const MemoryObject *mo, const Array *array, KType *dt);
314-
ObjectState(const MemoryObject *mo, KType *dt);
313+
ObjectState(const MemoryObject *mo, const Array *array, KType *dt,
314+
ref<Expr> defaultTaintValue = Expr::createEmptyTaint());
315+
ObjectState(const MemoryObject *mo, KType *dt,
316+
ref<Expr> defaultTaintValue = Expr::createEmptyTaint());
315317

316318
// For symbolic objects not in memory (hack)
317319

lib/Expr/Expr.cpp

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

556+
ref<ConstantExpr> Expr::createTaintBySource(uint64_t source) {
557+
return ConstantExpr::create((1 << source), Expr::Int64);
558+
}
559+
556560
ref<Expr> Expr::combineTaints(const ref<Expr> &taintL,
557561
const ref<Expr> &taintR) {
558562
if (SelectExpr *sel = dyn_cast<SelectExpr>(taintL)) {
@@ -2991,7 +2995,7 @@ ref<Expr> ConstantPointerExpr::create(const ref<ConstantExpr> &b,
29912995
combineTaints(RHS)); \
29922996
} else { \
29932997
auto value = _e_op::create(getValue(), RHS->getValue()); \
2994-
if (getTaint()->isZero() && RHS->getTaint()->isZero()) { \
2998+
if (getTaint()->isZero() && RHS->getTaint()->isZero()) { \
29952999
return value; \
29963000
} else { \
29973001
return PointerExpr::create(ConstantExpr::create(0, value->getWidth()), \

0 commit comments

Comments
 (0)