check for introduction of nonnull/align arg attributes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1695,7 +1695,7 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
s.addUB(p.isAligned(argflag.align));
if (argflag.has(ParamAttrs::NonNull))
- s.addUB(!p.isNull());
+ s.addUB(p.isNonZero());
ptr_inputs.emplace_back(StateValue(p.release(), move(value.non_poison)),
argflag.has(ParamAttrs::ByVal),
@@ -1735,15 +1735,18 @@ pack_return(State &s, Type &ty, vector<StateValue> &vals, const FnAttrs &attrs,
return agg->aggregateVals(vs);
}
- auto &ret = vals[idx++];
- if (ty.isFloatType() && attrs.has(FnAttrs::NNaN))
+ auto ret = move(vals[idx++]);
+ if (attrs.has(FnAttrs::NNaN)) {
+ assert(ty.isFloatType());
ret.non_poison &= !ret.value.isNaN();
+ }
bool isDeref = attrs.has(FnAttrs::Dereferenceable);
bool isNonNull = attrs.has(FnAttrs::NonNull);
bool isAlign = attrs.has(FnAttrs::Align);
- if (ty.isPtrType() && (isDeref || isNonNull || isAlign)) {
+ if (isDeref || isNonNull || isAlign) {
+ assert(ty.isPtrType());
Pointer p(s.getMemory(), ret.value);
s.addUB(ret.non_poison);
if (isDeref)
@@ -1751,7 +1754,7 @@ pack_return(State &s, Type &ty, vector<StateValue> &vals, const FnAttrs &attrs,
else if (isAlign)
s.addUB(p.isAligned(attrs.align));
if (isNonNull)
- s.addUB(!p.isNull());
+ s.addUB(p.isNonZero());
}
return ret;
@@ -2418,7 +2421,7 @@ StateValue Return::toSMT(State &s) const {
s.addUB(p.isAligned(attrs.align));
}
if (isNonNull) {
- s.addUB(!p.isNull());
+ s.addUB(p.isNonZero());
}
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1580,11 +1580,6 @@ expr Memory::mkInput(const char *name, const ParamAttrs &attrs) {
Pointer p(*this, name, false, false, false, attr_to_bitvec(attrs));
auto bid = p.getShortBid();
- if (attrs.has(ParamAttrs::NonNull))
- state->addAxiom(p.isNonZero());
- if (attrs.has(ParamAttrs::Align))
- state->addAxiom(p.isAligned(attrs.align));
-
state->addAxiom(bid.ule(max_bid));
AliasSet alias(*this);

MODIFY
ir/value.cpp
ir/value.cpp
@@ -219,7 +219,7 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
}
if (hasAttribute(ParamAttrs::NonNull))
- s.addUB(!Pointer(s.getMemory(), val).isNull());
+ s.addUB(Pointer(s.getMemory(), val).isNonZero());
if (hasAttribute(ParamAttrs::Dereferenceable))
s.addUB(Pointer(s.getMemory(), val)

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

check for introduction of nonnull/align arg attributes