use State::s.getAndAddPoisonUB() in more places
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2363,12 +2363,10 @@ void Alloc::print(std::ostream &os) const {
}
StateValue Alloc::toSMT(State &s) const {
- auto [sz, np] = s[*size];
- s.addUB(move(np));
+ auto sz = s.getAndAddPoisonUB(*size, true).value;
if (mul) {
- auto &[mul_e, mul_np] = s[*mul];
- s.addUB(mul_np);
+ auto &mul_e = s.getAndAddPoisonUB(*mul, true).value;
sz = sz.zextOrTrunc(bits_size_t);
auto m = mul_e.zextOrTrunc(bits_size_t);
s.addUB(sz.mul_no_uoverflow(m));
@@ -2769,9 +2767,6 @@ void Load::print(std::ostream &os) const {
}
StateValue Load::toSMT(State &s) const {
- // NOTE: We neeed clarification whether loading a partially undefined pointer
- // is UB. Memory sanitizer has an option (detecting a partially undef pointer)
- // for this, so worth discussing it.
auto &p = s.getAndAddPoisonUB(*ptr, true).value;
auto [sv, ub] = s.getMemory().load(p, getType(), align);
s.addUB(move(ub));
@@ -2814,9 +2809,6 @@ void Store::print(std::ostream &os) const {
}
StateValue Store::toSMT(State &s) const {
- // NOTE: We neeed clarification whether store to a partially undefined pointer
- // is UB. Memory sanitizer has an option (detecting a partially undef pointer)
- // for this, so worth discussing it.
auto &p = s.getAndAddPoisonUB(*ptr, true).value;
auto &v = s[*val];
s.getMemory().store(p, v, val->getType(), align, s.getUndefVars());
@@ -2864,9 +2856,8 @@ void Memset::print(ostream &os) const {
StateValue Memset::toSMT(State &s) const {
auto &[vptr, np_ptr] = s[*ptr];
- auto &[vbytes, np_bytes] = s[*bytes];
+ auto &vbytes = s.getAndAddPoisonUB(*bytes).value;
s.addUB((vbytes != 0).implies(np_ptr));
- s.addUB(np_bytes);
s.getMemory().memset(vptr, s[*val].zextOrTrunc(8), vbytes, align,
s.getUndefVars());
return {};
@@ -2921,7 +2912,7 @@ void Memcpy::print(ostream &os) const {
StateValue Memcpy::toSMT(State &s) const {
auto &[vdst, np_dst] = s[*dst];
auto &[vsrc, np_src] = s[*src];
- auto &vbytes = s.getAndAddPoisonUB(*bytes, true).value;
+ auto &vbytes = s.getAndAddPoisonUB(*bytes).value;
s.addUB((vbytes != 0).implies(np_dst && np_src));
if (vbytes.bits() > bits_size_t)

MODIFY
ir/state.cpp
ir/state.cpp
@@ -163,11 +163,11 @@ static expr strip_undef_and_add_ub(State &s, const Value &val, const expr &e) {
if (e.isIf(c, a, b) && a.isConst() && b.isConst()) {
if (c.isEq(lhs, rhs)) {
expr val, not_undef;
- if (is_if_undef(lhs, val, not_undef)) {
+ if (rhs.isConst() && is_if_undef(lhs, val, not_undef)) {
s.addUB(move(not_undef));
return expr::mkIf(val == rhs, a, b);
}
- if (is_if_undef(rhs, val, not_undef)) {
+ if (lhs.isConst() && is_if_undef(rhs, val, not_undef)) {
s.addUB(move(not_undef));
return expr::mkIf(lhs == val, a, b);
}
@@ -483,7 +483,8 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
// TODO: this doesn't need to compare the full memory, just a subset of fields
auto call_data_pair
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
- analysis.ranges_fn_calls, memory,
+ analysis.ranges_fn_calls,
+ reads_memory ? memory : Memory(*this),
reads_memory, argmemonly });
auto &I = call_data_pair.first;
bool inserted = call_data_pair.second;
@@ -664,13 +665,11 @@ void State::mkAxioms(State &tgt) {
// need to be compared
auto &[ptr_in, is_byval, is_nocapture] = ptr_ins[i];
auto &[ptr_in2, is_byval2, is_nocapture2] = ptr_ins2[i];
- (void)is_nocapture;
- (void)is_nocapture2;
- if (!is_byval && is_byval2) {
- // byval is added at target; this is not supported yet.
+ if (is_byval != is_byval2 || is_nocapture != is_nocapture2) {
refines = false;
break;
}
+
expr eq_val = Pointer(mem, ptr_in.value)
.fninputRefined(Pointer(mem2, ptr_in2.value),
undef_vars, is_byval2);

use State::s.getAndAddPoisonUB() in more places