memory: fix encoding of poison bytes
there was a mismatch in the interpretation of the poison bits (0 vs 1)
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1334,7 +1334,7 @@ StateValue ConversionOp::toSMT(State &s) const {
// turn poison data into boolean
if (op == BitCast)
- v.non_poison = v.non_poison == 0;
+ v.non_poison = v.non_poison == expr::mkInt(-1, v.non_poison);
return scalar(move(v), getType());
}
@@ -2403,7 +2403,6 @@ check_ret_attributes(State &s, StateValue &sv, const Type &t,
}
StateValue Return::toSMT(State &s) const {
- // Encode nocapture semantics.
StateValue retval;
auto &attrs = s.getFn().getFnAttrs();

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -184,8 +184,8 @@ Byte::Byte(const Memory &m, const StateValue &ptr, unsigned i) : m(m) {
if (byte_has_ptr_bit())
p = expr::mkUInt(1, 1);
p = concat_if(p,
- expr::mkIf(ptr.non_poison, expr::mkUInt(0, 1),
- expr::mkUInt(1, 1)))
+ expr::mkIf(ptr.non_poison, expr::mkUInt(1, 1),
+ expr::mkUInt(0, 1)))
.concat(ptr.value);
if (bits_ptr_byte_offset())
p = p.concat(expr::mkUInt(i, bits_ptr_byte_offset()));
@@ -206,8 +206,9 @@ Byte::Byte(const Memory &m, const StateValue &v) : m(m) {
if (byte_has_ptr_bit())
p = expr::mkUInt(0, 1);
expr np = v.non_poison.isBool()
- ? expr::mkIf(v.non_poison, expr::mkUInt(0, bits_poison_per_byte),
- expr::mkUInt(1, bits_poison_per_byte))
+ ? expr::mkIf(v.non_poison,
+ expr::mkInt(-1, bits_poison_per_byte),
+ expr::mkUInt(0, bits_poison_per_byte))
: v.non_poison;
p = concat_if(p, np.concat(v.value).concat_zeros(padding_nonptr_byte()));
assert(!p.isValid() || p.bits() == bitsByte());
@@ -230,7 +231,7 @@ expr Byte::ptrNonpoison() const {
if (!does_ptr_mem_access)
return true;
auto bit = p.bits() - 1 - byte_has_ptr_bit();
- return p.extract(bit, bit) == 0;
+ return p.extract(bit, bit) == 1;
}
Pointer Byte::ptr() const {
@@ -269,14 +270,13 @@ expr Byte::nonptrValue() const {
return p.extract(start + bits_byte - 1, start);
}
-expr Byte::isPoison(bool fullbit) const {
+expr Byte::isPoison() const {
expr np = nonptrNonpoison();
if (byte_has_ptr_bit() && bits_poison_per_byte == 1) {
- assert(!np.isValid() || ptrNonpoison().eq(np == 0));
- return np == 1;
+ assert(!np.isValid() || ptrNonpoison().eq(np == 1));
+ return np == 0;
}
- return expr::mkIf(isPtr(), !ptrNonpoison(),
- fullbit ? np == -1ull : np != 0);
+ return expr::mkIf(isPtr(), !ptrNonpoison(), np != expr::mkInt(-1, np));
}
expr Byte::isZero() const {
@@ -295,7 +295,7 @@ expr Byte::refined(const Byte &other) const {
expr int_cnstr;
if (bits_poison_per_byte == bits_byte) {
- int_cnstr = (np2 | np1) == np1 && (v1 | np1) == (v2 | np1);
+ int_cnstr = (np2 & np1) == np1 && (v1 & np1) == (v2 & np1);
}
else if (bits_poison_per_byte > 1) {
assert((bits_byte % bits_poison_per_byte) == 0);
@@ -307,10 +307,11 @@ expr Byte::refined(const Byte &other) const {
expr enp1 = np1.extract(i, i);
expr enp2 = np2.extract(i, i);
int_cnstr
- &= enp1 == 1 || ((enp1.eq(enp2) ? true : enp2 == 0) && ev1 == ev2);
+ &= enp1 == 0 || ((enp1.eq(enp2) ? true : enp2 == 1) && ev1 == ev2);
}
} else {
- int_cnstr = np1 == 1 || ((np1.eq(np2) ? true : np2 == 0) && v1 == v2);
+ assert(!np1.isValid() || np1.bits() == 1);
+ int_cnstr = np1 == 0 || ((np1.eq(np2) ? true : np2 == 1) && v1 == v2);
}
// fast path: if we didn't do any ptr store, then all ptrs in memory were
@@ -454,7 +455,7 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
expr::mkIf(is_ptr,
b.ptrByteoffset() == i && ptr_value == loaded_ptr,
b.nonptrValue() == 0);
- non_poison &= !b.isPoison(false);
+ non_poison &= !b.isPoison();
}
// if bits of loaded ptr are a subset of the non-ptr value,

MODIFY
ir/memory.h
ir/memory.h
@@ -61,7 +61,7 @@ public:
smt::expr ptrByteoffset() const;
smt::expr nonptrNonpoison() const;
smt::expr nonptrValue() const;
- smt::expr isPoison(bool fullbit = true) const;
+ smt::expr isPoison() const;
smt::expr isZero() const; // zero or null
smt::expr&& operator()() && { return std::move(p); }

MODIFY
ir/state.cpp
ir/state.cpp
@@ -495,7 +495,7 @@ State::getAndAddPoisonUB(const Value &val, bool undef_ub_too) {
assert(i_tmp_values < tmp_values.size());
return tmp_values[i_tmp_values++] = { move(v),
- sv.non_poison.isBool() ? true : expr::mkUInt(0, sv.non_poison) };
+ sv.non_poison.isBool() ? true : expr::mkInt(-1, sv.non_poison) };
}
const State::ValTy& State::at(const Value &val) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -215,10 +215,9 @@ expr Type::toBV(expr e) const {
}
StateValue Type::toBV(StateValue v) const {
- expr val = toBV(move(v.value));
auto bw = np_bits();
- return { move(val),
- expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
+ return { toBV(move(v.value)),
+ expr::mkIf(v.non_poison, expr::mkInt(-1, bw), expr::mkUInt(0, bw)) };
}
expr Type::fromBV(expr e) const {
@@ -226,7 +225,8 @@ expr Type::fromBV(expr e) const {
}
StateValue Type::fromBV(StateValue v) const {
- return { fromBV(move(v.value)), v.non_poison == 0 };
+ return { fromBV(move(v.value)),
+ v.non_poison == expr::mkInt(-1, v.non_poison) };
}
expr Type::toInt(State &s, expr v) const {
@@ -234,10 +234,9 @@ expr Type::toInt(State &s, expr v) const {
}
StateValue Type::toInt(State &s, StateValue v) const {
- expr val = toInt(s, move(v.value));
auto bw = np_bits();
- return { move(val),
- expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
+ return { toInt(s, move(v.value)),
+ expr::mkIf(v.non_poison, expr::mkInt(-1, bw), expr::mkUInt(0, bw)) };
}
expr Type::fromInt(expr e) const {
@@ -246,12 +245,14 @@ expr Type::fromInt(expr e) const {
StateValue Type::fromInt(StateValue v) const {
return { fromInt(move(v.value)),
- v.non_poison.isBool() ? expr(v.non_poison) : v.non_poison == 0 };
+ v.non_poison.isBool()
+ ? expr(v.non_poison)
+ : v.non_poison == expr::mkInt(-1, v.non_poison) };
}
expr Type::combine_poison(const expr &boolean, const expr &orig) const {
return
- expr::mkIf(boolean, expr::mkInt(0, orig), expr::mkInt(-1, orig)) | orig;
+ expr::mkIf(boolean, expr::mkInt(-1, orig), expr::mkInt(0, orig)) & orig;
}
pair<expr, expr> Type::mkUndefInput(State &s, const ParamAttrs &attrs) const {
@@ -738,7 +739,7 @@ StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
assert(vals.size() + numPaddingsConst() == elements);
// structs can be empty
if (elements == 0)
- return { expr::mkUInt(0, 1), expr::mkUInt(1, 1) };
+ return { expr::mkUInt(0, 1), expr::mkUInt(0, 1) };
StateValue v;
bool first = true;

ADD
tests/alive-tv/memory/uninit-ptr-mem.srctgt.ll
+define i32* @src() {
+ %retval = alloca i32*, align 8
+ %v = load i32*, i32** %retval, align 8
+ ret i32* %v
+}
+
+define i32* @tgt() {
+ ret i32* undef
+}

memory: fix encoding of poison bytes
there was a mismatch in the interpretation of the poison bits (0 vs 1)