refactor pointer isNull & remove all uses of isNonZero
we cannot distinguish those anymore
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -96,14 +96,14 @@ encodePtrAttrs(const State &s, const expr &ptrvalue,
Pointer p(s.getMemory(), ptrvalue);
if (nonnull)
- non_poison &= p.isNonZero();
+ non_poison &= !p.isNull();
if (derefBytes || derefOrNullBytes) {
// dereferenceable, byval (ParamAttrs), dereferenceable_or_null
if (derefBytes)
UB.add(p.isDereferenceable(derefBytes, align));
if (derefOrNullBytes)
- UB.add(p.isDereferenceable(derefOrNullBytes, align)() || !p.isNonZero());
+ UB.add(p.isDereferenceable(derefOrNullBytes, align)() || p.isNull());
} else if (align != 1)
// align
non_poison &= p.isAligned(align);

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2510,7 +2510,7 @@ StateValue Assume::toSMT(State &s) const {
// assume(ptr)
const auto &vptr = s.getAndAddPoisonUB(*args[0]);
Pointer ptr(s.getMemory(), vptr.value);
- s.addUB(ptr.isNonZero());
+ s.addUB(!ptr.isNull());
break;
}
}
@@ -2755,7 +2755,7 @@ StateValue Malloc::toSMT(State &s) const {
Pointer ptr_old(m, p);
if (s.getFn().getFnAttrs().has(FnAttrs::NoFree))
- s.addUB(ptr_old.isNonZero().implies(ptr_old.isLocal()));
+ s.addUB(ptr_old.isNull() || ptr_old.isLocal());
m.copy(ptr_old, Pointer(m, p_new));
@@ -2905,7 +2905,7 @@ StateValue Free::toSMT(State &s) const {
if (s.getFn().getFnAttrs().has(FnAttrs::NoFree) && heaponly) {
Pointer ptr(s.getMemory(), p);
- s.addUB(ptr.isNonZero().implies(ptr.isLocal()));
+ s.addUB(ptr.isNull() || ptr.isLocal());
}
return {};

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1521,18 +1521,18 @@ void Memory::startLifetime(const expr &ptr_local) {
void Memory::free(const expr &ptr, bool unconstrained) {
assert(!memory_unused() && (has_free || has_dead_allocas));
Pointer p(*this, ptr);
- expr nonzero = p.isNonZero();
+ expr isnnull = p.isNull();
if (!unconstrained)
- state->addUB(nonzero.implies(p.getOffset() == 0 &&
+ state->addUB(isnnull || (p.getOffset() == 0 &&
p.isBlockAlive() &&
p.getAllocType() == Pointer::MALLOC));
- if (!nonzero.isFalse()) {
+ if (!isnnull.isTrue()) {
// A nonlocal block for encoding fn calls' side effects cannot be freed.
ensure_non_fncallmem(p);
store_bv(p, false, local_block_liveness, non_local_block_liveness, false,
- nonzero);
+ !isnnull);
}
}

MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -560,17 +560,13 @@ Pointer Pointer::mkNullPointer(const Memory &m) {
}
expr Pointer::isNull() const {
+ if (Memory::observesAddresses())
+ return getAddress() == 0;
if (!has_null_block)
return false;
return *this == mkNullPointer(m);
}
-expr Pointer::isNonZero() const {
- if (Memory::observesAddresses())
- return getAddress() != 0;
- return !isNull();
-}
-
void Pointer::resetGlobals() {
ptr_next_idx = 0;
}

MODIFY
ir/pointer.h
ir/pointer.h
@@ -116,7 +116,6 @@ public:
static Pointer mkNullPointer(const Memory &m);
smt::expr isNull() const;
- smt::expr isNonZero() const;
static void resetGlobals();

refactor pointer isNull & remove all uses of isNonZero
we cannot distinguish those anymore