Add support for llvm.assume with noundef op bundle
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2290,15 +2290,30 @@ void Assume::rauw(const Value &what, Value &with) {
}
void Assume::print(ostream &os) const {
- os << (if_non_poison ? "assume_non_poison " : "assume ") << *cond;
+ switch (kind) {
+ case AndNonPoison: os << "assume "; break;
+ case IfNonPoison: os << "assume_non_poison "; break;
+ case WellDefined: os << "assume_welldefined "; break;
+ }
+ os << *cond;
}
StateValue Assume::toSMT(State &s) const {
+ switch (kind) {
+ case AndNonPoison: {
+ auto &v = s.getAndAddPoisonUB(*cond);
+ s.addUB(v.value != 0);
+ break;
+ }
+ case IfNonPoison: {
auto &[v, np] = s[*cond];
- if (if_non_poison)
s.addUB(np.implies(v != 0));
- else
- s.addUB(np && v != 0);
+ break;
+ }
+ case WellDefined:
+ (void)s.getAndAddPoisonUB(*cond, true);
+ break;
+ }
return {};
}
@@ -2307,7 +2322,7 @@ expr Assume::getTypeConstraints(const Function &f) const {
}
unique_ptr<Instr> Assume::dup(const string &suffix) const {
- return make_unique<Assume>(*cond, if_non_poison);
+ return make_unique<Assume>(*cond, kind);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -392,12 +392,20 @@ public:
class Assume final : public Instr {
+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)
+ };
+
+private:
Value *cond;
- bool if_non_poison; /// cond only needs to hold if non-poison
+ Kind kind;
+
public:
- Assume(Value &cond, bool if_non_poison)
- : Instr(Type::voidTy, "assume"), cond(&cond),
- if_non_poison(if_non_poison) {}
+ Assume(Value &cond, Kind kind)
+ : Instr(Type::voidTy, "assume"), cond(&cond), 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
@@ -175,7 +175,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
// some NOP instruction
assert(i.getType()->isVoidTy());
auto true_val = get_operand(llvm::ConstantInt::getTrue(i.getContext()));
- return make_unique<Assume>(*true_val, false);
+ return make_unique<Assume>(*true_val, Assume::AndNonPoison);
}
public:
@@ -692,15 +692,31 @@ end:
RetTy visitUnreachableInst(llvm::UnreachableInst &i) {
auto fals = get_operand(llvm::ConstantInt::getFalse(i.getContext()));
- return make_unique<Assume>(*fals, /*if_non_poison=*/false);
+ return make_unique<Assume>(*fals, Assume::AndNonPoison);
}
RetTy visitIntrinsicInst(llvm::IntrinsicInst &i) {
switch (i.getIntrinsicID()) {
case llvm::Intrinsic::assume:
{
+ unsigned n = i.getNumOperandBundles();
+ for (unsigned j = 0; j < n; ++j) {
+ auto bundle = i.getOperandBundleAt(j);
+ llvm::StringRef name = bundle.getTagName();
+ if (name == "noundef") {
+ // Currently it is unclear whether noundef bundle takes single op.
+ // 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();
+ BB->addInstr(
+ make_unique<Assume>(*get_operand(v), Assume::WellDefined));
+ }
+ } else {
+ return error(i);
+ }
+ }
PARSE_UNOP();
- return make_unique<Assume>(*val, false);
+ return make_unique<Assume>(*val, Assume::AndNonPoison);
}
case llvm::Intrinsic::sadd_with_overflow:
case llvm::Intrinsic::uadd_with_overflow:
@@ -937,7 +953,7 @@ end:
}
if (range)
- BB->addInstr(make_unique<Assume>(*range, true));
+ BB->addInstr(make_unique<Assume>(*range, Assume::IfNonPoison));
break;
}

ADD
tests/alive-tv/attrs/noundef-bundle.srctgt.ll
+declare void @llvm.assume(i1)
+
+define i32 @src(i32 %x) {
+ %x.fr = freeze i32 %x
+ call void @llvm.assume(i1 1) [ "noundef"(i32 %x) ]
+ ret i32 %x.fr
+}
+
+define i32 @tgt(i32 %x) {
+ ret i32 %x
+}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -1196,7 +1196,8 @@ static unique_ptr<Instr> parse_assume(bool if_non_poison) {
tokenizer.ensure(LPAREN);
auto &val = parse_operand(*int_types[1].get());
tokenizer.ensure(RPAREN);
- return make_unique<Assume>(val, if_non_poison);
+ return make_unique<Assume>(val, if_non_poison ? Assume::IfNonPoison :
+ Assume::AndNonPoison);
}
static unique_ptr<Instr> parse_return() {
@@ -1230,7 +1231,7 @@ static void parse_fn(Function &f) {
}
case UNREACH:
bb->addInstr(make_unique<Assume>(get_constant(0, *int_types[1].get()),
- /*if_non_poison=*/false));
+ Assume::AndNonPoison));
break;
default:
string_view name;

Add support for llvm.assume with noundef op bundle (#506)