fix semantics of mem accessing instructions for undef ptrs
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -59,7 +59,7 @@ ostream& operator<<(ostream &os, const FnAttrs &attr) {
}
bool ParamAttrs::undefImpliesUB() const {
- bool ub = has(NoUndef);
+ bool ub = has(NoUndef) || has(Dereferenceable) || has(ByVal);
assert(!ub || poisonImpliesUB());
return ub;
}
@@ -79,7 +79,7 @@ bool FnAttrs::poisonImpliesUB() const {
}
bool FnAttrs::undefImpliesUB() const {
- bool ub = has(NoUndef);
+ bool ub = has(NoUndef) || has(Dereferenceable);
assert(!ub || poisonImpliesUB());
return ub;
}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -3061,7 +3061,7 @@ void Load::print(ostream &os) const {
}
StateValue Load::toSMT(State &s) const {
- auto &p = s.getAndAddPoisonUB(*ptr).value;
+ auto &p = s.getAndAddPoisonUB(*ptr, true).value;
check_can_load(s, p);
auto [sv, ub] = s.getMemory().load(p, getType(), align);
s.addUB(move(ub));
@@ -3112,7 +3112,7 @@ StateValue Store::toSMT(State &s) const {
return {};
}
- auto &p = s.getAndAddPoisonUB(*ptr).value;
+ auto &p = s.getAndAddPoisonUB(*ptr, true).value;
check_can_store(s, p);
auto &v = s[*val];
s.getMemory().store(p, v, val->getType(), align, s.getUndefVars());
@@ -3159,15 +3159,17 @@ void Memset::print(ostream &os) const {
}
StateValue Memset::toSMT(State &s) const {
- auto &vbytes = s.getAndAddPoisonUB(*bytes).value;
+ auto &vbytes = s.getAndAddPoisonUB(*bytes, true).value;
uint64_t n;
expr vptr;
if (vbytes.isUInt(n) && n > 0) {
- vptr = s.getAndAddPoisonUB(*ptr).value;
+ vptr = s.getAndAddPoisonUB(*ptr, true).value;
} else {
auto &sv_ptr = s[*ptr];
- s.addUB((vbytes != 0).implies(sv_ptr.non_poison));
+ auto &sv_ptr2 = s[*ptr];
+ s.addUB((vbytes != 0).implies(
+ sv_ptr.non_poison && (sv_ptr.value == sv_ptr2.value)));
vptr = sv_ptr.value;
}
check_can_store(s, vptr);
@@ -3223,17 +3225,20 @@ void Memcpy::print(ostream &os) const {
}
StateValue Memcpy::toSMT(State &s) const {
- auto &vbytes = s.getAndAddPoisonUB(*bytes).value;
+ auto &vbytes = s.getAndAddPoisonUB(*bytes, true).value;
uint64_t n;
expr vsrc, vdst;
if (vbytes.isUInt(n) && n > 0) {
- vdst = s.getAndAddPoisonUB(*dst).value;
- vsrc = s.getAndAddPoisonUB(*src).value;
+ vdst = s.getAndAddPoisonUB(*dst, true).value;
+ vsrc = s.getAndAddPoisonUB(*src, true).value;
} else {
auto &sv_dst = s[*dst];
+ auto &sv_dst2 = s[*dst];
auto &sv_src = s[*src];
- s.addUB((vbytes != 0).implies(sv_dst.non_poison && sv_src.non_poison));
+ auto &sv_src2 = s[*src];
+ s.addUB((vbytes != 0).implies(sv_dst.non_poison && sv_src.non_poison &&
+ (sv_dst.value == sv_dst2.value && sv_src.value == sv_src2.value)));
vdst = sv_dst.value;
vsrc = sv_src.value;
}

MODIFY
tests/alive-tv/undef/load-undefidx.srctgt.ll
tests/alive-tv/undef/load-undefidx.srctgt.ll
-; Relevant patch: https://reviews.llvm.org/D87994
+; https://reviews.llvm.org/D95238
define i8 @src() {
ret i8 0
@@ -12,3 +12,5 @@ define i8 @tgt() {
%v = load i8, i8* %p2
ret i8 %v
}
+
+; ERROR: Source is more defined than target

fix semantics of mem accessing instructions for undef ptrs (#674)