Add support for the noundef attribute
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -19,6 +19,8 @@ ostream& operator<<(ostream &os, const ParamAttrs &attr) {
os << "readnone ";
if (attr.has(ParamAttrs::Dereferenceable))
os << "dereferenceable(" << attr.derefBytes << ") ";
+ if (attr.has(ParamAttrs::NoUndef))
+ os << "noundef ";
return os;
}
@@ -40,6 +42,8 @@ ostream& operator<<(ostream &os, const FnAttrs &attr) {
os << " nonnull";
if (attr.has(FnAttrs::NoFree))
os << " nofree";
+ if (attr.has(FnAttrs::NoUndef))
+ os << " noundef";
return os;
}

MODIFY
ir/attrs.h
ir/attrs.h
@@ -13,7 +13,8 @@ class ParamAttrs final {
public:
enum Attribute { None = 0, NonNull = 1<<0, ByVal = 1<<1, NoCapture = 1<<2,
- ReadOnly = 1<<3, ReadNone = 1<<4, Dereferenceable = 1<<5 };
+ ReadOnly = 1<<3, ReadNone = 1<<4, Dereferenceable = 1<<5,
+ NoUndef = 1<<6 };
ParamAttrs(unsigned bits = None) : bits(bits) {}
@@ -34,7 +35,7 @@ public:
enum Attribute { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1,
ArgMemOnly = 1 << 2, NNaN = 1 << 3, NoReturn = 1 << 4,
Dereferenceable = 1 << 5, NonNull = 1 << 6,
- NoFree = 1 << 7 };
+ NoFree = 1 << 7, NoUndef = 1 << 8 };
FnAttrs(unsigned bits = None) : bits(bits) {}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1451,27 +1451,60 @@ void FnCall::print(ostream &os) const {
os << "\t; WARNING: unknown known function";
}
-static void unpack_inputs(State&s, Type &ty, const ParamAttrs &argflag,
+static pair<expr,expr> // <extracted value, not_undef>
+strip_undef(State &s, const Value &val, const expr &e) {
+ if (s.isUndef(e))
+ return { expr::mkUInt(0, e.bits()), false };
+
+ expr c, a, b, lhs, rhs, ty;
+ unsigned h, l;
+
+ // (ite (= ((_ extract 0 0) ty_%var) #b0) %var undef!0)
+ if (e.isIf(c, a, b) && s.isUndef(b) && c.isEq(lhs, rhs)) {
+ if (lhs.isZero())
+ swap(lhs, rhs);
+
+ if (rhs.isZero() &&
+ lhs.isExtract(ty, h, l) && h == 0 && l == 0 && isTyVar(ty, a))
+ return { move(a), move(c) };
+ }
+
+ return { e, e == s[val].value };
+}
+
+static void unpack_inputs(State &s, Value *argv, Type &ty,
+ const ParamAttrs &argflag,
const StateValue &value, vector<StateValue> &inputs,
vector<Memory::PtrInput> &ptr_inputs) {
if (auto agg = ty.getAsAggregateType()) {
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
- unpack_inputs(s, agg->getChild(i), argflag, agg->extract(value, i),
+ unpack_inputs(s, argv, agg->getChild(i), argflag, agg->extract(value, i),
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(value.non_poison);
+
+ if (is_noundef) {
+ // TODO: noundef for aggregate should be supported.
+ assert(!argv->getType().isAggregateType());
+ s.addUB(strip_undef(s, *argv, value.value).second);
+ }
+
if (ty.isPtrType()) {
Pointer p(s.getMemory(), value.value);
p.stripAttrs();
- if (argflag.has(ParamAttrs::Dereferenceable)) {
- s.addUB(value.non_poison);
+ if (is_deref)
s.addUB(
p.isDereferenceable(argflag.getDerefBytes(), bits_byte / 8, false));
- }
- if (argflag.has(ParamAttrs::NonNull)) {
- s.addUB(value.non_poison);
+
+ if (is_nonnull)
s.addUB(p.isNonZero());
- }
+
ptr_inputs.emplace_back(StateValue(p.release(), expr(value.non_poison)),
argflag.has(ParamAttrs::ByVal),
argflag.has(ParamAttrs::NoCapture));
@@ -1533,7 +1566,7 @@ StateValue FnCall::toSMT(State &s) const {
ostringstream fnName_mangled;
fnName_mangled << fnName;
for (auto &[arg, flags] : args) {
- unpack_inputs(s, arg->getType(), flags, s[*arg], inputs, ptr_inputs);
+ unpack_inputs(s, arg, arg->getType(), flags, s[*arg], inputs, ptr_inputs);
fnName_mangled << '#' << arg->getType();
}
fnName_mangled << '!' << getType();
@@ -1940,32 +1973,10 @@ void Branch::print(ostream &os) const {
os << ", label " << dst_false->getName();
}
-static pair<expr,expr> // <condition, not_undef>
-jump_undef_condition(State &s, const Value &val, const expr &e) {
- if (s.isUndef(e))
- return { expr::mkUInt(0, 1), false };
-
- expr c, a, b, lhs, rhs, ty;
- unsigned h, l;
- uint64_t n;
-
- // (ite (= ((_ extract 0 0) ty_%var) #b0) %var undef!0)
- if (e.isIf(c, a, b) && s.isUndef(b) && c.isEq(lhs, rhs)) {
- if (lhs.isUInt(n))
- swap(lhs, rhs);
-
- if (rhs.isUInt(n) && n == 0 &&
- lhs.isExtract(ty, h, l) && h == 0 && l == 0 && isTyVar(ty, a))
- return { move(a), c };
- }
-
- return { e, e == s[val].value };
-}
-
StateValue Branch::toSMT(State &s) const {
if (cond) {
auto &c = s[*cond];
- auto [cond_val, not_undef] = jump_undef_condition(s, *cond, c.value);
+ auto [cond_val, not_undef] = strip_undef(s, *cond, c.value);
s.addUB(c.non_poison);
s.addUB(move(not_undef));
s.addCondJump(cond_val, dst_true, *dst_false);
@@ -2021,7 +2032,7 @@ StateValue Switch::toSMT(State &s) const {
auto &val = s[*value];
expr default_cond(true);
- auto [cond_val, not_undef] = jump_undef_condition(s, *value, val.value);
+ auto [cond_val, not_undef] = strip_undef(s, *value, val.value);
s.addUB(val.non_poison);
s.addUB(move(not_undef));
@@ -2094,10 +2105,11 @@ StateValue Return::toSMT(State &s) const {
auto &attrs = s.getFn().getFnAttrs();
bool isDeref = attrs.has(FnAttrs::Dereferenceable);
bool isNonNull = attrs.has(FnAttrs::NonNull);
+ bool isNoUndef = attrs.has(FnAttrs::NoUndef);
+
if (isDeref || isNonNull) {
assert(val->getType().isPtrType());
Pointer p(s.getMemory(), retval.value);
- s.addUB(retval.non_poison);
if (isDeref) {
s.addUB(p.isDereferenceable(attrs.getDerefBytes()));
@@ -2108,6 +2120,14 @@ StateValue Return::toSMT(State &s) const {
}
}
+ if (isDeref || isNonNull || isNoUndef)
+ s.addUB(retval.non_poison);
+ if (isNoUndef) {
+ // TODO: noundef for aggregates should be supported.
+ assert(!val->getType().isAggregateType());
+ s.addUB(strip_undef(s, *val, retval.value).second);
+ }
+
s.addReturn(retval);
return {};
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -229,6 +229,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
bool reads_memory = !attrs.has(FnAttrs::NoRead);
bool writes_memory = !attrs.has(FnAttrs::NoWrite);
bool argmemonly = attrs.has(FnAttrs::ArgMemOnly);
+ bool noundef = attrs.has(FnAttrs::NoUndef);
bool all_valid = true;
for (auto &v : inputs) {
@@ -257,10 +258,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
auto mk_val = [&](const Type &t, const string &name) {
if (t.isPtrType())
- return memory.mkFnRet(name.c_str(), I->first.args_ptr);
+ return memory.mkFnRet(name.c_str(), I->first.args_ptr).first;
- auto v = expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
- return make_pair(v, v);
+ return expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
};
if (inserted) {
@@ -268,8 +268,8 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
string valname = name + "#val";
string npname = name + "#np";
for (auto t : out_types) {
- values.emplace_back(mk_val(*t, valname).first,
- expr::mkFreshVar(npname.c_str(), false));
+ expr np = noundef ? expr(true) : expr::mkFreshVar(npname.c_str(), false);
+ values.emplace_back(mk_val(*t, valname), move(np));
}
string ub_name = name + "#ub";

MODIFY
ir/value.cpp
ir/value.cpp
@@ -192,8 +192,10 @@ StateValue Input::toSMT(State &s) const {
bool has_deref = hasAttribute(ParamAttrs::Dereferenceable);
bool has_nonnull = hasAttribute(ParamAttrs::NonNull);
+ bool has_noundef = hasAttribute(ParamAttrs::NoUndef);
- if (!config::disable_undef_input && !has_deref) {
+ bool never_undef = config::disable_undef_input || has_deref || has_noundef;
+ if (!never_undef) {
auto [undef, vars] = getType().mkUndefInput(s, attrs);
for (auto &v : vars) {
s.addUndefVar(move(v));
@@ -214,9 +216,10 @@ StateValue Input::toSMT(State &s) const {
expr poison = getType().getDummyValue(false).non_poison;
expr non_poison = getType().getDummyValue(true).non_poison;
+ bool never_poison = config::disable_poison_input || has_deref || has_noundef;
return { move(val),
- config::disable_poison_input || has_deref
+ never_poison
? move(non_poison)
: expr::mkIf(type.extract(1, 1) == 0, non_poison, poison) };
}

ADD
tests/alive-tv/attrs/noundef-callsite.srctgt.ll
+declare void @f(i1)
+
+define i32 @src(i1 %cond) {
+ call void @f(i1 noundef %cond)
+ %f = freeze i1 %cond
+ br i1 %f, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}
+
+define i32 @tgt(i1 %cond) {
+ call void @f(i1 noundef %cond)
+ br i1 %cond, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}

ADD
tests/alive-tv/attrs/noundef-fndef.srctgt.ll
+declare void @f(i1 noundef)
+
+define i32 @src(i1 %cond) {
+ call void @f(i1 %cond)
+ %f = freeze i1 %cond
+ br i1 %f, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}
+
+define i32 @tgt(i1 %cond) {
+ call void @f(i1 %cond)
+ br i1 %cond, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}

ADD
tests/alive-tv/attrs/noundef-ret-callsite.srctgt.ll
+declare i1 @f()
+
+define i32 @src() {
+ %cond = call noundef i1 @f()
+ %f = freeze i1 %cond
+ br i1 %f, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}
+
+define i32 @tgt() {
+ %cond = call noundef i1 @f()
+ br i1 %cond, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}

ADD
tests/alive-tv/attrs/noundef-ret-fndef.srctgt.ll
+declare noundef i1 @f()
+
+define i32 @src() {
+ %cond = call i1 @f()
+ %f = freeze i1 %cond
+ br i1 %f, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}
+
+define i32 @tgt() {
+ %cond = call i1 @f()
+ br i1 %cond, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}

ADD
tests/alive-tv/attrs/noundef-ret.srctgt.ll
+define noundef i32 @src() {
+ ret i32 undef
+}
+
+define noundef i32 @tgt() {
+ unreachable
+}

ADD
tests/alive-tv/attrs/noundef-ret2.srctgt.ll
+define noundef i32 @src() {
+ ret i32 0
+}
+
+define noundef i32 @tgt() {
+ unreachable
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/attrs/noundef-ret3.srctgt.ll
+define noundef i32 @src(i32 %x) {
+ ret i32 %x
+}
+
+define noundef i32 @tgt(i32 %x) {
+ unreachable
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/attrs/noundef-ret4.srctgt.ll
+define noundef i32 @src() {
+ %a = add nsw i32 2147483647, 1
+ ret i32 %a
+}
+
+define noundef i32 @tgt() {
+ unreachable
+}

ADD
tests/alive-tv/attrs/noundef.srctgt.ll
+define i32 @src(i1 noundef %cond) {
+ %f = freeze i1 %cond
+ br i1 %f, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}
+
+define i32 @tgt(i1 noundef %cond) {
+ br i1 %cond, label %A, label %B
+A:
+ ret i32 0
+B:
+ ret i32 1
+}

ADD
tests/alive-tv/attrs/noundef2.srctgt.ll
+declare void @f(i1)
+
+; show that neither a or b is undef
+define void @src(i1 %a, i1 %b) {
+ %c = add i1 %a, %b
+ call void @f(i1 noundef %c)
+ ret void
+}
+
+define void @tgt(i1 %a, i1 %b) {
+ %c = add i1 %a, %b
+ call void @f(i1 noundef %c)
+ br i1 %a, label %A, label %B
+A:
+ br i1 %b, label %B, label %C
+B:
+ ret void
+C:
+ ret void
+}

Add support for the noundef attribute (#453)