Initial nonlocal val cannot contain ptr to fncall mem blk
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1009,7 +1009,7 @@ static expr mk_liveness_array() {
return expr::mkInt(-1, num_nonlocals);
}
-void Memory::mk_nonlocal_val_axioms(bool skip_consts) {
+void Memory::mkNonlocalValAxioms(bool skip_consts) {
if (!does_ptr_mem_access)
return;
@@ -1021,11 +1021,25 @@ void Memory::mk_nonlocal_val_axioms(bool skip_consts) {
Byte byte(*this, non_local_block_val[i].val.load(offset));
Pointer loadedptr = byte.ptr();
expr bid = loadedptr.getShortBid();
+
+ unsigned upperbid = numNonlocals() - 1;
+ expr bid_cond(true);
+ if (has_fncall) {
+ // initial memory cannot contain a pointer to fncall mem block.
+ if (is_fncall_mem(upperbid)) {
+ upperbid--;
+ } else {
+ assert(!state->isSource()); // target-only glb vars exist
+ bid_cond = bid != get_fncallmem_bid();
+ }
+ }
+ bid_cond &= bid.ule(upperbid);
+
state->addAxiom(
expr::mkForAll({ offset },
byte.isPtr().implies(!loadedptr.isLocal(false) &&
!loadedptr.isNocapture(false) &&
- bid.ule(numNonlocals() - 1))));
+ move(bid_cond))));
}
}
@@ -1048,7 +1062,7 @@ Memory::Memory(State &state) : state(&state), escaped_local_blks(*this) {
// Non-local blocks cannot initially contain pointers to local blocks
// and no-capture pointers.
- mk_nonlocal_val_axioms(false);
+ mkNonlocalValAxioms(false);
// initialize all local blocks as non-pointer, poison value
// This is okay because loading a pointer as non-pointer is also poison.
@@ -1321,7 +1335,7 @@ void Memory::setState(const Memory::CallState &st) {
non_local_block_val[i].undef.clear();
}
non_local_block_liveness = st.non_local_liveness;
- mk_nonlocal_val_axioms(true);
+ mkNonlocalValAxioms(true);
}
static expr disjoint_local_blocks(const Memory &m, const expr &addr,

MODIFY
ir/memory.h
ir/memory.h
@@ -163,7 +163,7 @@ class Memory {
smt::expr isBlockAlive(const smt::expr &bid, bool local) const;
- void mk_nonlocal_val_axioms(bool skip_consts);
+ void mkNonlocalValAxioms(bool skip_consts);
bool mayalias(bool local, unsigned bid, const smt::expr &offset,
unsigned bytes, unsigned align, bool write) const;

ADD
tests/alive-tv/por/issue697.srctgt.ll
+@glb = global i8* null, align 8
+
+define void @src(i8* %p) {
+ %tobool = icmp ne i8* %p, null
+ br i1 %tobool, label %if.then, label %if.end
+
+if.then:
+ call void @g(i8* %p)
+ br label %if.end
+
+if.end:
+ %q = load i8*, i8** @glb, align 8
+ ret void
+}
+
+define void @tgt(i8* %p) {
+ %tobool = icmp ne i8* %p, null
+ br i1 %tobool, label %if.then, label %if.end
+
+if.then:
+ call void @g(i8* %p)
+ br label %if.end
+
+if.end:
+ ;%q = load i8*, i8** @glb, align 8
+ ret void
+}
+
+declare void @g(i8*)

ADD
tests/alive-tv/por/issue697_2.srctgt.ll
+@glb = global i8* null, align 8
+
+define void @src(i8* %p) {
+ %tobool = icmp ne i8* %p, null
+ br i1 %tobool, label %if.then, label %if.end
+
+if.then:
+ call void @g(i8* undef)
+ br label %if.end
+
+if.end:
+ %q = load i8*, i8** @glb, align 8
+ ret void
+}
+
+define void @tgt(i8* %p) {
+ %tobool = icmp ne i8* %p, null
+ br i1 %tobool, label %if.then, label %if.end
+
+if.then:
+ call void @g(i8* undef)
+ br label %if.end
+
+if.end:
+ ;%q = load i8*, i8** @glb, align 8
+ ret void
+}
+
+declare void @g(i8*)

ADD
tests/alive-tv/por/issue697_3.srctgt.ll
+@glb = global i8* null, align 8
+@glb2 = global i8 0, align 8
+
+define void @src() {
+ %tobool = icmp ne i8* undef, null
+ br i1 %tobool, label %if.then, label %if.end
+
+if.then:
+ call void @g()
+ br label %if.end
+
+if.end:
+ %q = load i8*, i8** @glb, align 8
+ ret void
+}
+
+define void @tgt() {
+ %tobool = icmp ne i8* undef, null
+ br i1 %tobool, label %if.then, label %if.end
+
+if.then:
+ call void @g()
+ br label %if.end
+
+if.end:
+ ret void
+}
+
+declare void @g() writeonly

Initial nonlocal val cannot contain ptr to fncall mem blk (#696)