memory: add fast-path for block_size() of null pointers
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -211,10 +211,15 @@ expr Pointer::get_address() const {
return offset + get_value("blk_addr", local_blk_addr, offset);
}
-expr Pointer::block_size() const {
+expr Pointer::block_size(bool simplify) const {
// ASSUMPTION: programs can only allocate up to half of address space
// so the first bit of size is always zero.
// We need this assumption to support negative offsets.
+
+ // fast path for null ptrs
+ if (simplify && (get_bid() == 0).isTrue())
+ return expr::mkUInt(0, m.bits_size_t);
+
expr range = expr::mkUInt(0, m.bits_size_t - 1);
return expr::mkUInt(0, 1)
.concat(get_value("blk_size", local_blk_size, range));
@@ -434,7 +439,7 @@ Memory::Memory(State &state, bool little_endian)
if (state.isSource()) {
auto nullPtr = Pointer::mkNullPointer(*this);
state.addAxiom(nullPtr.get_address() == 0);
- state.addAxiom(nullPtr.block_size() == 0);
+ state.addAxiom(nullPtr.block_size(false) == 0);
}
assert(bits_for_offset <= bits_size_t);

MODIFY
ir/memory.h
ir/memory.h
@@ -51,7 +51,7 @@ public:
smt::expr get_offset() const;
smt::expr get_address() const;
- smt::expr block_size() const;
+ smt::expr block_size(bool simplify = true) const;
const smt::expr& operator()() const { return p; }
smt::expr short_ptr() const;

MODIFY
tests/alive-tv/memory/punning-intptr.tgt.ll
tests/alive-tv/memory/punning-intptr.tgt.ll
@@ -2,9 +2,6 @@ target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
define i8* @int_ptr_punning(i8* %ptr, i64 %n) {
store i8 1, i8* %ptr
- %n2 = and i64 %n, 7
- %n3 = sub i64 0, %n2
- %ptr_2 = getelementptr i8, i8* %ptr, i64 %n3
- %pptr = bitcast i8* %ptr_2 to i8**
- ret i8* undef
+ %poison = getelementptr inbounds i8, i8* null, i64 1
+ ret i8* %poison
}

memory: add fast-path for block_size() of null pointers