Add undefImpliesUB, poisonImpliesUB
MODIFY
ir/attrs.h
ir/attrs.h
@@ -24,6 +24,14 @@ public:
bool has(Attribute a) const { return (bits & a) != 0; }
void set(Attribute a) { bits |= (unsigned)a; }
+ // Returns true if it's UB for the argument to be poison / have a poison elem.
+ bool poisonImpliesUB() const
+ { return has(NonNull) || has(Dereferenceable) || has(NoUndef) || has(ByVal); }
+
+ // Returns true if it is UB for the argument to be (partially) undef.
+ bool undefImpliesUB() const
+ { return has(NoUndef); }
+
friend std::ostream& operator<<(std::ostream &os, const ParamAttrs &attr);
};
@@ -45,6 +53,14 @@ public:
uint64_t getDerefBytes() const { return derefBytes; }
void setDerefBytes(uint64_t bytes) { derefBytes = bytes; }
+ // Returns true if returning poison or an aggregate having a poison is UB
+ bool poisonImpliesUB() const
+ { return has(NonNull) || has(Dereferenceable) || has(NoUndef); }
+
+ // Returns true if returning (partially) undef is UB
+ bool undefImpliesUB() const
+ { return has(NoUndef); }
+
friend std::ostream& operator<<(std::ostream &os, const FnAttrs &attr);
};

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1606,26 +1606,6 @@ static expr eq_except_padding(const Type &ty, const expr &e1, const expr &e2) {
return result;
}
-static expr not_poison_except_padding(const Type &ty, const expr &np) {
- const auto *aty = ty.getAsAggregateType();
- if (!aty) {
- assert(!np.isValid() || np.isBool());
- return np;
- }
-
- StateValue sv{expr(), expr(np)};
- expr result = true;
-
- for (unsigned i = 0; i < aty->numElementsConst(); ++i) {
- if (aty->isPadding(i))
- continue;
-
- result &= not_poison_except_padding(aty->getChild(i),
- aty->extract(sv, i).non_poison);
- }
- return result;
-}
-
static bool isUndefMask(const expr &e, const expr &var) {
auto ty_name = e.fn_name();
auto var_name = var.fn_name();
@@ -1690,14 +1670,7 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
inputs, ptr_inputs);
}
} else {
- bool is_deref = argflag.has(ParamAttrs::Dereferenceable);
- bool is_nonnull = argflag.has(ParamAttrs::NonNull);
- bool is_noundef = argflag.has(ParamAttrs::NoUndef);
-
- if (is_deref || is_nonnull || is_noundef)
- s.addUB(not_poison_except_padding(ty, value.non_poison));
-
- if (is_noundef) {
+ if (argflag.undefImpliesUB()) {
auto [val, not_undef] = strip_undef(s, argv, value.value);
value.value = move(val);
s.addUB(move(not_undef));
@@ -1706,11 +1679,11 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
if (ty.isPtrType()) {
Pointer p(s.getMemory(), move(value.value));
p.stripAttrs();
- if (is_deref)
+ if (argflag.has(ParamAttrs::Dereferenceable))
s.addUB(
p.isDereferenceable(argflag.derefBytes, bits_byte / 8, false));
- if (is_nonnull)
+ if (argflag.has(ParamAttrs::NonNull))
s.addUB(p.isNonZero());
ptr_inputs.emplace_back(StateValue(p.release(), move(value.non_poison)),
@@ -1780,7 +1753,13 @@ StateValue FnCall::toSMT(State &s) const {
ostringstream fnName_mangled;
fnName_mangled << fnName;
for (auto &[arg, flags] : args) {
- unpack_inputs(s, *arg, arg->getType(), flags, s[*arg], inputs, ptr_inputs);
+ StateValue sv;
+ if (flags.poisonImpliesUB())
+ sv = s.getAndAddPoisonUB(*arg);
+ else
+ sv = s[*arg];
+
+ unpack_inputs(s, *arg, arg->getType(), flags, sv, inputs, ptr_inputs);
fnName_mangled << '#' << arg->getType();
}
fnName_mangled << '!' << getType();
@@ -2326,16 +2305,21 @@ static void addUBForNoCaptureRet(State &s, const StateValue &svret,
StateValue Return::toSMT(State &s) const {
// Encode nocapture semantics.
- auto retval = s[*val];
+ StateValue retval;
+
+ auto &attrs = s.getFn().getFnAttrs();
+ if (attrs.poisonImpliesUB())
+ retval = s.getAndAddPoisonUB(*val);
+ else
+ retval = s[*val];
+
s.addUB(s.getMemory().checkNocapture());
addUBForNoCaptureRet(s, retval, val->getType());
- auto &attrs = s.getFn().getFnAttrs();
bool isDeref = attrs.has(FnAttrs::Dereferenceable);
bool isNonNull = attrs.has(FnAttrs::NonNull);
- bool isNoUndef = attrs.has(FnAttrs::NoUndef);
- if (isNoUndef) {
+ if (attrs.undefImpliesUB()) {
auto [value, not_undef] = strip_undef(s, *val, retval.value);
retval.value = move(value);
s.addUB(move(not_undef));
@@ -2355,10 +2339,6 @@ StateValue Return::toSMT(State &s) const {
}
}
- if (isDeref || isNonNull || isNoUndef) {
- s.addUB(not_poison_except_padding(val->getType(), retval.non_poison));
- }
-
s.addReturn(move(retval));
return {};
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -123,6 +123,26 @@ const StateValue& State::getAndAddUndefs(const Value &val) {
return v;
}
+static expr not_poison_except_padding(const Type &ty, const expr &np) {
+ const auto *aty = ty.getAsAggregateType();
+ if (!aty) {
+ assert(!np.isValid() || np.isBool());
+ return np;
+ }
+
+ StateValue sv{expr(), expr(np)};
+ expr result = true;
+
+ for (unsigned i = 0; i < aty->numElementsConst(); ++i) {
+ if (aty->isPadding(i))
+ continue;
+
+ result &= not_poison_except_padding(aty->getChild(i),
+ aty->extract(sv, i).non_poison);
+ }
+ return result;
+}
+
const StateValue& State::getAndAddPoisonUB(const Value &val) {
auto &v = (*this)[val];
if (!analysis.non_poison_vals.insert(&val).second)
@@ -148,7 +168,7 @@ const StateValue& State::getAndAddPoisonUB(const Value &val) {
}
// If val is an aggregate, all elements should be non-poison
- addUB(v.non_poison.isBool() ? v.non_poison : v.non_poison == 0);
+ addUB(not_poison_except_padding(val.getType(), v.non_poison));
assert(i_tmp_values < tmp_values.size());
return tmp_values[i_tmp_values++] = { expr(v.value),
v.non_poison.isBool() ? true : expr::mkUInt(0, v.non_poison.bits()) };

MODIFY
ir/value.cpp
ir/value.cpp
@@ -198,8 +198,6 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
bool has_byval = hasAttribute(ParamAttrs::ByVal);
bool has_deref = hasAttribute(ParamAttrs::Dereferenceable);
- bool has_nonnull = hasAttribute(ParamAttrs::NonNull);
- bool has_noundef = hasAttribute(ParamAttrs::NoUndef);
expr val;
if (has_byval) {
@@ -227,8 +225,7 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
s.addAxiom(p.isDereferenceable(attrs.derefBytes, bits_byte/8, false));
}
- bool never_poison = config::disable_poison_input || has_byval || has_deref ||
- has_nonnull || has_noundef;
+ bool never_poison = config::disable_poison_input || attrs.poisonImpliesUB();
string np_name = "np_" + getSMTName(child);
return { move(val), never_poison ? true : expr::mkBoolVar(np_name.c_str()) };
@@ -239,10 +236,12 @@ StateValue Input::toSMT(State &s) const {
}
expr Input::getUndefVar(const Type &ty, unsigned child) const {
+ // TODO: Clarify whether byval/dereferenceable accept partially undefined
+ // pointers
if (config::disable_undef_input ||
hasAttribute(ParamAttrs::ByVal) ||
hasAttribute(ParamAttrs::Dereferenceable) ||
- hasAttribute(ParamAttrs::NoUndef))
+ attrs.undefImpliesUB())
return {};
string tyname = "isundef_" + getSMTName(child);

Add undefImpliesUB, poisonImpliesUB (#486)