memory: fix byte ptr encoding when padding is present
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -36,10 +36,11 @@ Byte::Byte(const Pointer &ptr, unsigned i, const expr &non_poison)
unsigned padding = bitsByte() - does_int_mem_access - 1 - bits_for_offset
- bits_for_bid - 3;
- if (does_int_mem_access)
+ if (does_int_mem_access) {
p = expr::mkUInt(1, 1);
if (padding)
p = concat_if(p, expr::mkUInt(0, padding));
+ }
p = concat_if(p, non_poison.toBVBool())
.concat(ptr()).concat(expr::mkUInt(i, 3));
assert(!p.isValid() || p.bits() == bitsByte());
@@ -73,7 +74,7 @@ expr Byte::is_ptr() const {
expr Byte::ptr_nonpoison() const {
if (!does_ptr_mem_access)
return true;
- auto bit = p.bits() - 2;
+ auto bit = bits_for_offset + bits_for_bid + 3;
return p.extract(bit, bit) == 1;
}
@@ -270,6 +271,7 @@ Pointer::Pointer(const Memory &m, const char *var_name, const expr &local,
if (unique_name)
name += '!' + to_string(ptr_next_idx++);
p = local.toBVBool().concat(expr::mkVar(name.c_str(), total_bits() - 1));
+ assert(!p.isValid() || p.bits() == total_bits());
}
Pointer::Pointer(const Memory &m, expr repr) : m(m), p(move(repr)) {
@@ -280,10 +282,13 @@ Pointer::Pointer(const Memory &m, unsigned bid, bool local)
: m(m), p(expr::mkUInt(local, 1).concat(expr::mkUInt(bid, bits_for_bid - 1)
.concat(expr::mkUInt(0, bits_for_offset)))) {
assert((local && bid < num_locals) || (!local && bid < num_nonlocals));
+ assert(!p.isValid() || p.bits() == total_bits());
}
Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset)
- : m(m), p(bid.concat(offset)) {}
+ : m(m), p(bid.concat(offset)) {
+ assert(!p.isValid() || p.bits() == total_bits());
+}
unsigned Pointer::total_bits() {
return bits_for_bid + bits_for_offset;
@@ -743,17 +748,19 @@ Memory::Memory(State &state) : state(&state) {
non_local_block_val =
expr::mkLambda({ idx }, expr::mkIf(is_ptr, ptr_val(), int_val));
- if (state.isSource()) {
- auto bid = ptr_val.ptr().get_bid().extract(bits_for_bid - 2, 0);
- state.addAxiom(expr::mkForAll({ idx }, bid.ule(num_nonlocals - 1)));
- }
+ if (state.isSource())
+ state.addAxiom(expr::mkForAll({ idx },
+ ptr_val.ptr().get_short_bid().ule(num_nonlocals - 1)));
#else
+ if (state.isSource()) {
Byte byte(*this, non_local_block_val.load(idx));
Pointer loadedptr = byte.ptr();
+ expr bid = loadedptr.get_short_bid();
state.addAxiom(
expr::mkForAll({ idx },
byte.is_ptr().implies(!loadedptr.is_local() &&
- loadedptr.get_bid().ult(num_nonlocals))));
+ bid.ule(num_nonlocals - 1))));
+ }
#endif
}
@@ -844,12 +851,10 @@ void Memory::resetLocalBids() {
}
expr Memory::mkInput(const char *name) const {
- unsigned bits = bits_for_bid - 1 + bits_for_offset;
- expr var = expr::mkVar(name, bits);
- expr bid = var.extract(bits - 1, bits_for_offset);
- expr is_local = expr::mkUInt(0, 1);
- state->addAxiom(bid.ule(num_nonlocals - 1));
- return Pointer(*this, is_local.concat(var)).release();
+ expr var = expr::mkVar(name, bits_for_bid - 1 + bits_for_offset);
+ Pointer p(*this, expr::mkUInt(0, 1).concat(var));
+ state->addAxiom(p.get_short_bid().ule(num_nonlocals - 1));
+ return p.release();
}
pair<expr, expr> Memory::mkUndefInput() const {

MODIFY
ir/memory.h
ir/memory.h
@@ -22,10 +22,10 @@ class State;
// A data structure that represents a byte.
// A byte is either a pointer byte or a non-pointer byte.
// Pointer byte's representation:
-// +-+-------+-----------+------------------+----------------+-------------+
-// |1|padding|non-poison?| ptr offset | block id | byte offset |
-// | | |(1 bit) | (bits_for_offset)| (bits_for_bid) | (3 bits) |
-// +-+-------+-----------+------------------+----------------+-------------+
+// +-+-------+-----------+----------------+-------------------+-------------+
+// |1|padding|non-poison?| block id | ptr offset | byte offset |
+// | | |(1 bit) | (bits_for_bid) | (bits_for_offset) | (3 bits) |
+// +-+-------+-----------+----------------+-------------------+-------------+
// Non-pointer byte's representation:
// +-+--------------------------+--------------------+---------------------+
// |0| padding(zero) | non-poison bits? | data |

ADD
tests/alive-tv/memory/ptr-cmp.src.ll
+; ERROR: Target is more poisonous
+
+define i1 @f(i32** %a) {
+ %load = load i32*, i32** %a
+ %integral = ptrtoint i32* %load to i64
+ %cmp = icmp slt i64 %integral, 0
+ ret i1 %cmp
+}

ADD
tests/alive-tv/memory/ptr-cmp.tgt.ll
+define i1 @f(i32** %a) {
+ %load = load i32*, i32** %a, align 8
+ %cmp = icmp slt i32* %load, null
+ ret i1 %cmp
+}
+

MODIFY
tests/alive-tv/memory/store-removal.src.ll
tests/alive-tv/memory/store-removal.src.ll
-; TEST-ARGS: -disable-poison-input
+; TEST-ARGS: -disable-poison-input -disable-undef-input
define void @f(i8* %p) {
%v = load i8, i8* %p

memory: fix byte ptr encoding when padding is present