switch to bitwise poison tracking in memory
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1545,6 +1545,7 @@ StateValue Memset::toSMT(State &s) const {
expr Memset::getTypeConstraints(const Function &f) const {
return ptr->getType().enforcePtrType() &&
+ val->getType().enforceIntType(8) &&
bytes->getType().enforceIntType();
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -201,7 +201,7 @@ string Memory::mkName(const char *str) const {
expr Memory::mk_val_array(const char *name) const {
unsigned bits_bids = bits_for_local_bid + bits_for_nonlocal_bid;
return expr::mkArray(name, expr::mkUInt(0, bits_bids + bits_for_offset),
- expr::mkUInt(0, 8 + 1)); // val+poison bit
+ expr::mkUInt(0, 2 * 8)); // val + poison bits
}
expr Memory::mk_liveness_uf() const {
@@ -215,7 +215,7 @@ Memory::Memory(State &state) : state(&state) {
{
// initialize all local blocks as poison
Pointer idx(*this, "#idx0");
- expr poison = expr::mkUInt(0, 9);
+ expr poison = expr::mkUInt(0, 16);
expr val = expr::mkIf(idx.is_local(), poison, blocks_val.load(idx()));
blocks_val = expr::mkLambda({ idx() }, move(val));
}
@@ -264,7 +264,7 @@ void Memory::free(const expr &ptr) {
void Memory::store(const expr &p, const StateValue &v, Type &type,
unsigned align) {
StateValue val = type.toBV(v);
- unsigned bits = val.value.bits();
+ unsigned bits = val.bits();
unsigned bytes = divide_up(bits, 8);
val.value = val.value.zext(bytes * 8 - bits);
@@ -275,8 +275,8 @@ void Memory::store(const expr &p, const StateValue &v, Type &type,
for (unsigned i = 0; i < bytes; ++i) {
// FIXME: right now we store in little-endian; consider others?
expr data = val.value.extract((i + 1) * 8 - 1, i * 8);
- auto p = (ptr + i).release();
- blocks_val = blocks_val.store(p, val.non_poison.concat(data));
+ expr np = val.non_poison.extract((i + 1) * 8 - 1, i * 8);
+ blocks_val = blocks_val.store((ptr + i).release(), np.concat(data));
}
}
@@ -292,16 +292,11 @@ StateValue Memory::load(const expr &p, Type &type, unsigned align) {
for (unsigned i = 0; i < bytes; ++i) {
auto ptr_i = (ptr + i).release();
expr pair = blocks_val.load(ptr_i);
- expr v = pair.extract(8-1, 0);
- expr p = pair.extract(8, 8);
+ expr v = pair.extract(7, 0);
+ expr p = pair.extract(15, 8);
- if (first) {
- val.value = move(v);
- val.non_poison = move(p);
- } else {
- val.value = v.concat(val.value);
- val.non_poison = p | val.non_poison;
- }
+ val.value = first ? move(v) : v.concat(val.value);
+ val.non_poison = first ? move(p) : p.concat(val.non_poison);
first = false;
}
@@ -311,9 +306,11 @@ StateValue Memory::load(const expr &p, Type &type, unsigned align) {
void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,
unsigned align) {
+ assert(val.bits() == 8);
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes, align);
- expr store_val = val.non_poison.toBVBool().concat(val.value);
+ auto valbv = IntType("", 8).toBV(val);
+ expr store_val = valbv.non_poison.concat(valbv.value);
uint64_t n;
if (bytes.isUInt(n) && n <= 4) {

MODIFY
ir/memory.h
ir/memory.h
@@ -47,7 +47,7 @@ public:
smt::expr block_size() const;
const smt::expr& operator()() const { return p; }
- smt::expr&& release() { return std::move(p); }
+ smt::expr release() { return std::move(p); }
unsigned bits() const { return p.bits(); }
Pointer operator+(unsigned) const;

MODIFY
ir/state_value.h
ir/state_value.h
@@ -20,6 +20,8 @@ struct StateValue {
static StateValue mkIf(const smt::expr &cond, const StateValue &then,
const StateValue &els);
+ auto bits() const { return value.bits(); }
+
StateValue concat(const StateValue &other) const;
smt::expr both() const { return value && non_poison; }

MODIFY
ir/type.cpp
ir/type.cpp
@@ -165,7 +165,10 @@ expr Type::toBV(expr e) const {
}
StateValue Type::toBV(StateValue v) const {
- return { toBV(v.value), v.non_poison.toBVBool() };
+ expr val = toBV(v.value);
+ auto bw = val.bits();
+ return { move(val),
+ expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
}
expr Type::fromBV(expr e) const {
@@ -173,7 +176,7 @@ expr Type::fromBV(expr e) const {
}
StateValue Type::fromBV(StateValue v) const {
- return { fromBV(v.value), v.non_poison == 1 };
+ return { fromBV(v.value), v.non_poison == 0 };
}
ostream& operator<<(ostream &os, const Type &t) {
@@ -536,11 +539,11 @@ StateValue AggregateType::extract(const StateValue &val, unsigned index) const {
total_till_now += children[i]->bits();
}
unsigned high = val.value.bits() - total_till_now;
- unsigned poison_idx = children.size() - index - 1;
+ unsigned h = high - 1;
+ unsigned l = high - children[index]->bits();
- return children[index]->fromBV({
- val.value.extract(high - 1, high - children[index]->bits()),
- val.non_poison.extract(poison_idx, poison_idx) });
+ return children[index]->fromBV({ val.value.extract(h, l),
+ val.non_poison.extract(h, l) });
}
StateValue AggregateType::extract(const StateValue &val,
@@ -551,11 +554,14 @@ StateValue AggregateType::extract(const StateValue &val,
}
unsigned bw_elem = elementTy.bits();
unsigned bw_val = val.value.bits();
- expr idx = index.zextOrTrunc(bw_val);
- expr v = val.value << (idx * expr::mkUInt(bw_elem, bw_val));
- return elementTy.fromBV({
- v.extract(elements * bw_elem - 1, (elements - 1) * bw_elem),
- (val.non_poison << idx).extract(elements-1, elements-1) });
+ assert(bw_val == val.non_poison.bits());
+ expr idx = index.zextOrTrunc(bw_val) * expr::mkUInt(bw_elem, bw_val);
+
+ unsigned h = elements * bw_elem - 1;
+ unsigned l = (elements - 1) * bw_elem;
+
+ return elementTy.fromBV({ (val.value << idx).extract(h, l),
+ (val.non_poison << idx).extract(h, l) });
}
unsigned AggregateType::bits() const {

switch to bitwise poison tracking in memory