fix support for undef const globals
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -291,6 +291,15 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
Pointer p(mem, val.value);
unsigned bytesize = bits_program_pointer / bits_byte;
+ // constant global can't store pointers that alias with local blocks
+ if (s->isInitializationPhase() && !p.isLocal().isFalse()) {
+ expr bid = expr::mkUInt(0, 1).concat(p.getShortBid());
+ expr off = p.getOffset();
+ expr attr = p.getAttrs();
+ p.~Pointer();
+ new (&p) Pointer(mem, bid, off, attr);
+ }
+
for (unsigned i = 0; i < bytesize; ++i)
bytes.emplace_back(p, i, val.non_poison);
} else {
@@ -2007,7 +2016,7 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
for (unsigned i = num_nonlocals_src; i < numNonlocals(); ++i) {
I->second.setMayAlias(false, i);
}
- state->addAxiom(islocal || bid.ule(*max_bid) ||
+ state->addPre(islocal || bid.ule(*max_bid) ||
(num_extra_nonconst_tgt ? bid.uge(num_nonlocals_src)
: false));
}

ADD
tests/alive-tv/memory/glb-undef-2.srctgt.ll
+@g = internal unnamed_addr constant i8* undef, align 8
+
+define i1 @src() {
+ %a = alloca i8, align 8
+ %v = load i8*, i8** @g
+ %c = icmp eq i8* %a, %v
+ ret i1 %c
+}
+
+define i1 @tgt() {
+ ret i1 false
+}

ADD
tests/alive-tv/memory/glb-undef.srctgt.ll
+@g = internal unnamed_addr constant i8* undef, align 8
+
+define i8 @src() {
+ %a = alloca i8, align 8
+ %v = load i8*, i8** @g
+ ret i8 0
+}
+
+define i8 @tgt() {
+ ret i8 0
+}

fix #645: support for undef const globals