fix undefined pointer detection for memory instructions when ptrs have attributes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -3277,7 +3277,7 @@ void StartLifetime::print(ostream &os) const {
}
StateValue StartLifetime::toSMT(State &s) const {
- auto &p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &p = s.getWellDefinedPtr(*ptr);
s.getMemory().startLifetime(p);
return {};
}
@@ -3309,7 +3309,7 @@ void EndLifetime::print(ostream &os) const {
}
StateValue EndLifetime::toSMT(State &s) const {
- auto &p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &p = s.getWellDefinedPtr(*ptr);
s.getMemory().free(p, true);
return {};
}
@@ -3494,7 +3494,7 @@ void Load::print(ostream &os) const {
}
StateValue Load::toSMT(State &s) const {
- auto &p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &p = s.getWellDefinedPtr(*ptr);
check_can_load(s, p);
auto [sv, ub] = s.getMemory().load(p, getType(), align);
s.addUB(std::move(ub));
@@ -3544,7 +3544,7 @@ StateValue Store::toSMT(State &s) const {
return {};
}
- auto &p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &p = s.getWellDefinedPtr(*ptr);
check_can_store(s, p);
auto &v = s[*val];
s.getMemory().store(p, v, val->getType(), align, s.getUndefVars());
@@ -3595,7 +3595,7 @@ StateValue Memset::toSMT(State &s) const {
uint64_t n;
expr vptr;
if (vbytes.isUInt(n) && n > 0) {
- vptr = s.getAndAddPoisonUB(*ptr, true).value;
+ vptr = s.getWellDefinedPtr(*ptr);
} else {
auto &sv_ptr = s[*ptr];
auto &sv_ptr2 = s[*ptr];
@@ -3656,7 +3656,7 @@ void MemsetPattern::print(ostream &os) const {
}
StateValue MemsetPattern::toSMT(State &s) const {
- auto &vptr = s.getAndAddPoisonUB(*ptr, false).value;
+ auto &vptr = s.getWellDefinedPtr(*ptr);
auto &vpattern = s.getAndAddPoisonUB(*pattern, false).value;
auto &vbytes = s.getAndAddPoisonUB(*bytes, true).value;
check_can_store(s, vptr);
@@ -3700,7 +3700,7 @@ void FillPoison::print(ostream &os) const {
}
StateValue FillPoison::toSMT(State &s) const {
- auto &vptr = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &vptr = s.getWellDefinedPtr(*ptr);
Memory &m = s.getMemory();
m.fillPoison(Pointer(m, vptr).getBid());
return {};
@@ -3756,7 +3756,7 @@ StateValue Memcpy::toSMT(State &s) const {
uint64_t n;
expr vsrc, vdst;
if (align_dst || (vbytes.isUInt(n) && n > 0)) {
- vdst = s.getAndAddPoisonUB(*dst, true).value;
+ vdst = s.getWellDefinedPtr(*dst);
} else {
auto &sv_dst = s[*dst];
auto &sv_dst2 = s[*dst];
@@ -3766,7 +3766,7 @@ StateValue Memcpy::toSMT(State &s) const {
}
if (align_src || (vbytes.isUInt(n) && n > 0)) {
- vsrc = s.getAndAddPoisonUB(*src, true).value;
+ vsrc = s.getWellDefinedPtr(*src);
} else {
auto &sv_src = s[*src];
auto &sv_src2 = s[*src];
@@ -3935,7 +3935,7 @@ void Strlen::print(ostream &os) const {
}
StateValue Strlen::toSMT(State &s) const {
- auto &eptr = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &eptr = s.getWellDefinedPtr(*ptr);
check_can_load(s, eptr);
Pointer p(s.getMemory(), eptr);
@@ -3982,7 +3982,7 @@ StateValue VaStart::toSMT(State &s) const {
s.addUB(expr(s.getFn().isVarArgs()));
auto &data = s.getVarArgsData();
- auto &raw_p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &raw_p = s.getWellDefinedPtr(*ptr);
expr zero = expr::mkUInt(0, VARARG_BITS);
expr num_args = expr::mkVar("num_va_args", VARARG_BITS);
@@ -4057,7 +4057,7 @@ static void ensure_varargs_ptr(D &data, State &s, const expr &arg_ptr) {
StateValue VaEnd::toSMT(State &s) const {
auto &data = s.getVarArgsData();
- auto &raw_p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &raw_p = s.getWellDefinedPtr(*ptr);
s.addUB(Pointer(s.getMemory(), raw_p).isBlockAlive());
@@ -4095,8 +4095,8 @@ void VaCopy::print(ostream &os) const {
StateValue VaCopy::toSMT(State &s) const {
auto &data = s.getVarArgsData();
- auto &dst_raw = s.getAndAddPoisonUB(*dst, true).value;
- auto &src_raw = s.getAndAddPoisonUB(*src, true).value;
+ auto &dst_raw = s.getWellDefinedPtr(*dst);
+ auto &src_raw = s.getWellDefinedPtr(*src);
Pointer dst(s.getMemory(), dst_raw);
Pointer src(s.getMemory(), src_raw);
@@ -4151,7 +4151,7 @@ void VaArg::print(ostream &os) const {
StateValue VaArg::toSMT(State &s) const {
auto &data = s.getVarArgsData();
- auto &raw_p = s.getAndAddPoisonUB(*ptr, true).value;
+ auto &raw_p = s.getWellDefinedPtr(*ptr);
s.addUB(Pointer(s.getMemory(), raw_p).isBlockAlive());

MODIFY
ir/state.cpp
ir/state.cpp
@@ -211,7 +211,11 @@ const State::ValTy& State::exec(const Value &v) {
return get<1>(values.back());
}
-static expr eq_except_padding(const Type &ty, const expr &e1, const expr &e2) {
+static expr eq_except_padding(const Memory &m, const Type &ty, const expr &e1,
+ const expr &e2, bool ptr_compare) {
+ if (ptr_compare && ty.isPtrType())
+ return Pointer(m, e1) == Pointer(m, e2);
+
const auto *aty = ty.getAsAggregateType();
if (!aty)
return e1 == e2;
@@ -224,13 +228,14 @@ static expr eq_except_padding(const Type &ty, const expr &e1, const expr &e2) {
if (aty->isPadding(i))
continue;
- result &= eq_except_padding(aty->getChild(i), aty->extract(sv1, i).value,
- aty->extract(sv2, i).value);
+ result &= eq_except_padding(m, aty->getChild(i), aty->extract(sv1, i).value,
+ aty->extract(sv2, i).value, ptr_compare);
}
return result;
}
-expr State::strip_undef_and_add_ub(const Value &val, const expr &e) {
+expr State::strip_undef_and_add_ub(const Value &val, const expr &e,
+ bool ptr_compare) {
if (isUndef(e)) {
addUB(expr(false));
return expr::mkUInt(0, e);
@@ -422,7 +427,8 @@ expr State::strip_undef_and_add_ub(const Value &val, const expr &e) {
addQuantVar(newv);
repls.emplace_back(undef, std::move(newv));
}
- addUB(eq_except_padding(val.getType(), e, e.subst(repls)));
+ addUB(eq_except_padding(getMemory(), val.getType(), e, e.subst(repls),
+ ptr_compare));
return e;
}
@@ -526,7 +532,8 @@ static expr not_poison_except_padding(const Type &ty, const expr &np) {
}
const StateValue&
-State::getAndAddPoisonUB(const Value &val, bool undef_ub_too) {
+State::getAndAddPoisonUB(const Value &val, bool undef_ub_too,
+ bool ptr_compare) {
auto &sv = (*this)[val];
bool poison_already_added = !analysis.non_poison_vals.insert(&val).second;
@@ -540,7 +547,7 @@ State::getAndAddPoisonUB(const Value &val, bool undef_ub_too) {
if (I != analysis.non_undef_vals.end()) {
v = I->second;
} else {
- v = strip_undef_and_add_ub(val, v);
+ v = strip_undef_and_add_ub(val, v, ptr_compare);
analysis.non_undef_vals.emplace(&val, v);
}
}
@@ -575,6 +582,10 @@ State::getAndAddPoisonUB(const Value &val, bool undef_ub_too) {
sv.non_poison.isBool() ? true : expr::mkInt(-1, sv.non_poison) };
}
+const expr& State::getWellDefinedPtr(const Value &val) {
+ return getAndAddPoisonUB(val, true, true).value;
+}
+
const State::ValTy& State::at(const Value &val) const {
return get<1>(values[values_map.at(&val)]);
}

MODIFY
ir/state.h
ir/state.h
@@ -201,7 +201,9 @@ public:
const StateValue& operator[](const Value &val);
const StateValue& getAndAddUndefs(const Value &val);
// If undef_ub is true, UB is also added when val was undef
- const StateValue& getAndAddPoisonUB(const Value &val, bool undef_ub = false);
+ const StateValue& getAndAddPoisonUB(const Value &val, bool undef_ub = false,
+ bool ptr_compare = false);
+ const smt::expr& getWellDefinedPtr(const Value &val);
const ValTy& at(const Value &val) const;
bool isUndef(const smt::expr &e) const;
@@ -295,7 +297,8 @@ public:
void mkAxioms(State &tgt);
private:
- smt::expr strip_undef_and_add_ub(const Value &val, const smt::expr &e);
+ smt::expr strip_undef_and_add_ub(const Value &val, const smt::expr &e,
+ bool isptr);
void addJump(const BasicBlock &dst, smt::expr &&cond, bool last_jump = false);
};

ADD
tests/alive-tv/attrs/null_is_valid_nocapture.srctgt.ll
+define i8 @src(i1 %C, ptr %P) null_pointer_is_valid {
+ %P2 = select i1 %C, ptr %P, ptr null
+ %V = load i8, ptr %P2
+ ret i8 %V
+}
+
+define i8 @tgt(i1 %C, ptr nocapture %P) null_pointer_is_valid {
+ %P2 = select i1 %C, ptr %P, ptr null
+ %V = load i8, ptr %P2, align 1
+ ret i8 %V
+}

fix undefined pointer detection for memory instructions when ptrs have attributes