Add support for nonnull attribute
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -36,6 +36,8 @@ ostream& operator<<(ostream &os, const FnAttrs &attr) {
os << " noreturn";
if (attr.has(FnAttrs::Dereferenceable))
os << " dereferenceable(" << attr.derefBytes << ")";
+ if (attr.has(FnAttrs::NonNull))
+ os << " nonnull";
return os;
}

MODIFY
ir/attrs.h
ir/attrs.h
@@ -33,7 +33,7 @@ class FnAttrs final {
public:
enum Attribute { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1,
ArgMemOnly = 1 << 2, NNaN = 1 << 3, NoReturn = 1 << 4,
- Dereferenceable = 1 << 5 };
+ Dereferenceable = 1 << 5, NonNull = 1 << 6 };
FnAttrs(unsigned bits = None) : bits(bits) {}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1342,6 +1342,10 @@ static void unpack_inputs(State&s, Type &ty, const ParamAttrs &argflag,
s.addUB(
p.isDereferenceable(argflag.getDerefBytes(), bits_byte / 8, false));
}
+ if (argflag.has(ParamAttrs::NonNull)) {
+ s.addUB(value.non_poison);
+ s.addUB(p.isNonZero());
+ }
ptr_inputs.emplace_back(StateValue(p.release(), expr(value.non_poison)),
argflag.has(ParamAttrs::ByVal));
} else {
@@ -1374,11 +1378,18 @@ pack_return(State &s, Type &ty, vector<StateValue> &vals, const FnAttrs &attrs,
auto &ret = vals[idx++];
if (ty.isFloatType() && attrs.has(FnAttrs::NNaN))
ret.non_poison &= !ret.value.isNaN();
- if (ty.isPtrType() && attrs.has(FnAttrs::Dereferenceable)) {
+
+ bool isDeref = attrs.has(FnAttrs::Dereferenceable);
+ bool isNonNull = attrs.has(FnAttrs::NonNull);
+ if (ty.isPtrType() && (isDeref || isNonNull)) {
Pointer p(s.getMemory(), ret.value);
s.addUB(ret.non_poison);
+ if (isDeref)
s.addUB(p.isDereferenceable(attrs.getDerefBytes()));
+ if (isNonNull)
+ s.addUB(p.isNonZero());
}
+
return ret;
}
@@ -1943,13 +1954,21 @@ StateValue Return::toSMT(State &s) const {
addUBForNoCaptureRet(s, retval, val->getType());
auto &attrs = s.getFn().getFnAttrs();
- if (attrs.has(FnAttrs::Dereferenceable)) {
+ bool isDeref = attrs.has(FnAttrs::Dereferenceable);
+ bool isNonNull = attrs.has(FnAttrs::NonNull);
+ 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()));
s.addUB(p.getAllocType() != Pointer::STACK || !has_alloca);
}
+ if (isNonNull) {
+ s.addUB(p.isNonZero());
+ }
+ }
s.addReturn(retval);
return {};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -190,7 +190,9 @@ StateValue Input::toSMT(State &s) const {
val = getType().mkInput(s, smt_name.c_str(), attrs);
}
- const bool has_deref = hasAttribute(ParamAttrs::Dereferenceable);
+ bool has_deref = hasAttribute(ParamAttrs::Dereferenceable);
+ bool has_nonnull = hasAttribute(ParamAttrs::NonNull);
+
if (!config::disable_undef_input && !has_deref) {
auto [undef, vars] = getType().mkUndefInput(s, attrs);
for (auto &v : vars) {
@@ -199,10 +201,15 @@ StateValue Input::toSMT(State &s) const {
val = expr::mkIf(type.extract(0, 0) == 0, val, undef);
}
- if (has_deref) {
+ if (has_deref || has_nonnull) {
Pointer p(s.getMemory(), val);
- s.addAxiom(p.isDereferenceable(attrs.getDerefBytes(), bits_byte/8, false));
+ if (has_deref) {
s.addAxiom(type == 0);
+ s.addAxiom(p.isDereferenceable(attrs.getDerefBytes(), bits_byte/8, false));
+ }
+ if (has_nonnull && !has_deref) {
+ s.addAxiom(type.extract(1, 1) == 0);
+ }
}
expr poison = getType().getDummyValue(false).non_poison;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -272,6 +272,8 @@ public:
attrs.set(FnAttrs::Dereferenceable);
attrs.setDerefBytes(b);
}
+ if (i.hasRetAttr(llvm::Attribute::NonNull))
+ attrs.set(FnAttrs::NonNull);
string fn_name = '@' + fn->getName().str();
auto call =
@@ -304,6 +306,9 @@ public:
if (i.paramHasAttr(argidx, llvm::Attribute::ByVal))
attr.set(ParamAttrs::ByVal);
+ if (i.paramHasAttr(argidx, llvm::Attribute::NonNull))
+ attr.set(ParamAttrs::NonNull);
+
if (i.paramHasAttr(argidx, llvm::Attribute::Returned)) {
auto call2
= make_unique<FnCall>(Type::voidTy, "", string(call->getFnName()),
@@ -917,6 +922,8 @@ public:
attrs.set(FnAttrs::Dereferenceable);
attrs.setDerefBytes(b);
}
+ if (f.hasAttribute(ridx, llvm::Attribute::NonNull))
+ attrs.set(FnAttrs::NonNull);
// create all BBs upfront in topological order
vector<pair<BasicBlock*, llvm::BasicBlock*>> sorted_bbs;

ADD
tests/alive-tv/attrs/nonnull-callsite.srctgt.ll
+define i1 @src(i8* %p) {
+ call void @f(i8* nonnull %p)
+ %c = icmp eq i8* %p, null
+ ret i1 %c
+}
+
+define i1 @tgt(i8* %p) {
+ call void @f(i8* nonnull %p)
+ ret i1 0
+}
+
+declare void @f(i8*)

ADD
tests/alive-tv/attrs/nonnull-callsite2.srctgt.ll
+define i1 @src(i8* %p) {
+ call void @f(i8* %p)
+ %c = icmp eq i8* %p, null
+ ret i1 %c
+}
+
+define i1 @tgt(i8* %p) {
+ call void @f(i8* %p)
+ ret i1 0
+}
+
+declare void @f(i8* nonnull)

ADD
tests/alive-tv/attrs/nonnull-callsite3.srctgt.ll
+define void @src(i8* %p) {
+ %c = icmp ne i8* %p, null
+ br i1 %c, label %A, label %B
+A:
+ call void @f(i8* %p)
+ ret void
+B:
+ ret void
+}
+
+define void @tgt(i8* %p) {
+ %c = icmp ne i8* %p, null
+ br i1 %c, label %A, label %B
+A:
+ call void @f(i8* nonnull %p)
+ ret void
+B:
+ ret void
+}
+
+declare void @f(i8*)

ADD
tests/alive-tv/attrs/nonnull-callsite4.srctgt.ll
+define void @src(i8* %p) {
+ call void @f(i8* null)
+ ret void
+}
+
+define void @tgt(i8* %p) {
+ unreachable
+}
+
+declare void @f(i8* nonnull)

ADD
tests/alive-tv/attrs/nonnull-callsite5.srctgt.ll
+define void @src(i8* %p) {
+ call void @f(i8* undef)
+ ret void
+}
+
+define void @tgt(i8* %p) {
+ unreachable
+}
+
+declare void @f(i8* nonnull)

ADD
tests/alive-tv/attrs/nonnull-fndef.srctgt.ll
+define nonnull i8* @src(i8* nonnull %p) {
+ ret i8* %p
+}
+
+define nonnull i8* @tgt(i8* nonnull %p) {
+ unreachable
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/attrs/nonnull-fndef2.srctgt.ll
+define nonnull i8* @src(i8* %p) {
+ ret i8* null
+}
+
+define nonnull i8* @tgt(i8* %p) {
+ unreachable
+}

ADD
tests/alive-tv/attrs/nonnull-ret-callsite.srctgt.ll
+define nonnull i8* @src() {
+ %p = call i8* @f()
+ ret i8* %p
+}
+
+define nonnull i8* @tgt() {
+ unreachable
+}
+
+; ERROR: Source is more defined than target
+
+declare nonnull i8* @f()

Add support for nonnull attribute (#389)