allow free(zero), with zero != null
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -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.isNull() || ptr_old.isLocal());
+ s.addUB(ptr_old.isNonZero().implies(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.isNull() || ptr.isLocal());
+ s.addUB(ptr.isNonZero().implies(ptr.isLocal()));
}
return {};

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -162,7 +162,8 @@ static expr load_bv(const expr &var, const expr &idx0) {
}
static void store_bv(Pointer &p, const expr &val, expr &local,
- expr &non_local, bool assume_local = false) {
+ expr &non_local, bool assume_local = false,
+ const expr &cond = true) {
auto bid0 = p.getShortBid();
auto set = [&](const expr &var) {
@@ -178,8 +179,8 @@ static void store_bv(Pointer &p, const expr &val, expr &local,
};
auto is_local = p.isLocal() || assume_local;
- local = expr::mkIf(is_local, set(local), local);
- non_local = expr::mkIf(!is_local, set(non_local), non_local);
+ local = mkIf_fold(cond && is_local, set(local), local);
+ non_local = mkIf_fold(cond && !is_local, set(non_local), non_local);
}
namespace IR {
@@ -1520,14 +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();
+
if (!unconstrained)
- state->addUB(p.isNull() || (p.getOffset() == 0 &&
+ state->addUB(nonzero.implies(p.getOffset() == 0 &&
p.isBlockAlive() &&
p.getAllocType() == Pointer::MALLOC));
- if (!p.isNull().isTrue()) {
+
+ if (!nonzero.isFalse()) {
// 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);
+ store_bv(p, false, local_block_liveness, non_local_block_liveness, false,
+ nonzero);
}
}

ADD
tests/alive-tv/memory/free-null2.srctgt.ll
+define void @src(i8* %ptr) {
+ %c = icmp ne i8* %ptr, null
+ br i1 %c, label %then, label %else
+
+then:
+ call void @free(i8* %ptr)
+ br label %else
+
+else:
+ ret void
+}
+
+define void @tgt(i8* %ptr) {
+ call void @free(i8* %ptr)
+ ret void
+}
+
+declare void @free(i8*)

allow free(zero), with zero != null