Add support for align, nonnull assume operand bundle
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2433,12 +2433,29 @@ unique_ptr<Instr> Return::dup(const string &suffix) const {
}
+Assume::Assume(Value &cond, Kind kind)
+ : Instr(Type::voidTy, "assume"), args({&cond}), kind(kind) {
+ assert(kind == AndNonPoison || kind == IfNonPoison || kind == WellDefined ||
+ kind == NonNull);
+}
+
+Assume::Assume(vector<Value *> &&args0, Kind kind)
+ : Instr(Type::voidTy, "assume"), args(move(args0)), kind(kind) {
+ if (args.size() == 1)
+ assert(kind == AndNonPoison || kind == IfNonPoison || kind == WellDefined ||
+ kind == NonNull);
+ else {
+ assert(kind == Align && args.size() == 2);
+ }
+}
+
vector<Value*> Assume::operands() const {
- return { cond };
+ return args;
}
void Assume::rauw(const Value &what, Value &with) {
- RAUW(cond);
+ for (auto &arg: args)
+ RAUW(arg);
}
void Assume::print(ostream &os) const {
@@ -2446,37 +2463,66 @@ void Assume::print(ostream &os) const {
case AndNonPoison: os << "assume"; break;
case IfNonPoison: os << "assume_non_poison"; break;
case WellDefined: os << "assume_welldefined"; break;
+ case Align: os << "assume_align"; break;
+ case NonNull: os << "assume_nonnull"; break;
}
- os << *cond;
+ for (auto &arg: args)
+ os << ' ' << *arg;
}
StateValue Assume::toSMT(State &s) const {
switch (kind) {
case AndNonPoison: {
- auto &v = s.getAndAddPoisonUB(*cond);
+ auto &v = s.getAndAddPoisonUB(*args[0]);
s.addUB(v.value != 0);
break;
}
case IfNonPoison: {
- auto &[v, np] = s[*cond];
+ auto &[v, np] = s[*args[0]];
s.addUB(np.implies(v != 0));
break;
}
case WellDefined:
- (void)s.getAndAddPoisonUB(*cond, true);
+ (void)s.getAndAddPoisonUB(*args[0], true);
+ break;
+ case Align: {
+ // assume(ptr, align)
+ const auto &vptr = s.getAndAddPoisonUB(*args[0]);
+ uint64_t align = *dynamic_cast<IntConst *>(args[1])->getInt();
+
+ Pointer ptr(s.getMemory(), vptr.value);
+ s.addUB(ptr.isAligned(align));
+ break;
+ }
+ case NonNull: {
+ // assume(ptr)
+ const auto &vptr = s.getAndAddPoisonUB(*args[0]);
+ Pointer ptr(s.getMemory(), vptr.value);
+ s.addUB(ptr.isNonZero());
break;
}
+ }
return {};
}
expr Assume::getTypeConstraints(const Function &f) const {
- if (kind == WellDefined)
+ switch (kind) {
+ case WellDefined:
return true;
- return cond->getType().enforceIntType();
+ case AndNonPoison:
+ case IfNonPoison:
+ return args[0]->getType().enforceIntType();
+ case Align:
+ return args[0]->getType().enforcePtrType() &&
+ args[1]->getType().enforceIntType();
+ case NonNull:
+ return args[0]->getType().enforcePtrType();
+ }
+ return {};
}
unique_ptr<Instr> Assume::dup(const string &suffix) const {
- return make_unique<Assume>(*cond, kind);
+ return make_unique<Assume>(vector<Value *>(args), kind);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -407,16 +407,18 @@ public:
enum Kind {
AndNonPoison, /// cond should be non-poison and hold
IfNonPoison, /// cond only needs to hold if non-poison
- WellDefined /// cond only needs to be well defined (can be false)
+ WellDefined, /// cond only needs to be well defined (can be false)
+ Align, /// args[0] satisfies alignment args[1]
+ NonNull /// args[0] is a nonnull pointer
};
private:
- Value *cond;
+ std::vector<Value*> args;
Kind kind;
public:
- Assume(Value &cond, Kind kind)
- : Instr(Type::voidTy, "assume"), cond(&cond), kind(kind) {}
+ Assume(Value &cond, Kind kind);
+ Assume(std::vector<Value *> &&args, Kind kind);
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -741,9 +741,30 @@ public:
// Be conservative & simply assume it can take arbitrary num of ops.
for (unsigned j = 0; j < bundle.Inputs.size(); ++j) {
llvm::Value *v = bundle.Inputs[j].get();
+ auto *av = get_operand(v);
+ if (!av)
+ return error(i);
+
BB->addInstr(
- make_unique<Assume>(*get_operand(v), Assume::WellDefined));
+ make_unique<Assume>(*av, Assume::WellDefined));
}
+ } else if (name == "align") {
+ llvm::Value *ptr = bundle.Inputs[0].get();
+ llvm::Value *align = bundle.Inputs[1].get();
+ auto *aptr = get_operand(ptr), *aalign = get_operand(align);
+ if (!aptr || !aalign)
+ return error(i);
+
+ vector<Value *> args = {aptr, aalign};
+ BB->addInstr(make_unique<Assume>(move(args), Assume::Align));
+ } else if (name == "nonnull") {
+ llvm::Value *ptr = bundle.Inputs[0].get();
+ auto *aptr = get_operand(ptr);
+ if (!aptr)
+ return error(i);
+
+ BB->addInstr(
+ make_unique<Assume>(*aptr, Assume::NonNull));
} else {
return error(i);
}

ADD
tests/alive-tv/assume/align.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* align(4)) ; has no noundef
+
+define void @src(i8* %ptr) {
+ call void @f(i8* %ptr)
+ ret void
+}
+
+define void @tgt(i8* %ptr) {
+ call void @f(i8* %ptr)
+ call void @llvm.assume(i1 1) [ "align"(i8* %ptr, i64 4) ]
+ ret void
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/assume/align2.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* align(4) noundef)
+
+define void @src(i8* %ptr) {
+ call void @f(i8* %ptr)
+ ret void
+}
+
+define void @tgt(i8* %ptr) {
+ call void @f(i8* %ptr)
+ call void @llvm.assume(i1 1) [ "align"(i8* %ptr, i64 4) ]
+ ret void
+}

ADD
tests/alive-tv/assume/align3.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* align(4) dereferenceable(1)) ; dereferenceable implies noundef
+
+define void @src(i8* %ptr) {
+ call void @f(i8* %ptr)
+ ret void
+}
+
+define void @tgt(i8* %ptr) {
+ call void @f(i8* %ptr)
+ call void @llvm.assume(i1 1) [ "align"(i8* %ptr, i64 4) ]
+ ret void
+}

ADD
tests/alive-tv/assume/nonnull-twovars.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* noundef nonnull)
+
+define void @src(i8* %ptr, i8* %ptr2) {
+ call void @f(i8* %ptr)
+ call void @f(i8* %ptr2)
+ ret void
+}
+
+define void @tgt(i8* %ptr, i8* %ptr2) {
+ call void @f(i8* %ptr)
+ call void @f(i8* %ptr2)
+ call void @llvm.assume(i1 1) [ "nonnull"(i8* %ptr), "nonnull"(i8* %ptr2) ]
+ ret void
+}

ADD
tests/alive-tv/assume/nonnull-twovars2.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* nonnull) ; has no noundef
+
+define void @src(i8* %ptr, i8* %ptr2) {
+ call void @f(i8* %ptr)
+ call void @f(i8* noundef %ptr2)
+ ret void
+}
+
+define void @tgt(i8* %ptr, i8* %ptr2) {
+ call void @f(i8* %ptr)
+ call void @f(i8* noundef %ptr2)
+ call void @llvm.assume(i1 1) [ "nonnull"(i8* %ptr), "nonnull"(i8* %ptr2) ]
+ ret void
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/assume/nonnull.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* nonnull) ; has no noundef
+
+define void @src(i8* %ptr) {
+ call void @f(i8* %ptr)
+ ret void
+}
+
+define void @tgt(i8* %ptr) {
+ call void @f(i8* %ptr)
+ call void @llvm.assume(i1 1) [ "nonnull"(i8* %ptr) ]
+ ret void
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/assume/nonnull2.srctgt.ll
+declare void @llvm.assume(i1)
+
+declare void @f(i8* nonnull noundef)
+
+define void @src(i8* %ptr) {
+ call void @f(i8* %ptr)
+ ret void
+}
+
+define void @tgt(i8* %ptr) {
+ call void @f(i8* %ptr)
+ call void @llvm.assume(i1 1) [ "nonnull"(i8* %ptr) ]
+ ret void
+}

RENAME
tests/alive-tv/attrs/noundef-bundle.srctgt.ll
tests/alive-tv/assume/noundef.srctgt.ll
Add support for align, nonnull assume operand bundle (#600)