switch semantics of range metadata to yield poison rather than UB on failure
LLVM 16 adjusted the semantics
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -3042,15 +3042,13 @@ unique_ptr<Instr> Return::dup(Function &f, 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);
+ assert(kind == AndNonPoison || kind == WellDefined || kind == NonNull);
}
Assume::Assume(vector<Value *> &&args0, Kind kind)
: Instr(Type::voidTy, "assume"), args(std::move(args0)), kind(kind) {
if (args.size() == 1)
- assert(kind == AndNonPoison || kind == IfNonPoison || kind == WellDefined ||
- kind == NonNull);
+ assert(kind == AndNonPoison || kind == WellDefined || kind == NonNull);
else {
assert(kind == Align && args.size() == 2);
}
@@ -3069,7 +3067,6 @@ void Assume::print(ostream &os) const {
const char *str = nullptr;
switch (kind) {
case AndNonPoison: str = "assume "; break;
- case IfNonPoison: str = "assume_non_poison "; break;
case WellDefined: str = "assume_welldefined "; break;
case Align: str = "assume_align "; break;
case NonNull: str = "assume_nonnull "; break;
@@ -3092,11 +3089,6 @@ StateValue Assume::toSMT(State &s) const {
s.addUB(v.value != 0);
break;
}
- case IfNonPoison: {
- auto &[v, np] = s[*args[0]];
- s.addUB(np.implies(v != 0));
- break;
- }
case WellDefined:
(void)s.getAndAddPoisonUB(*args[0], true);
break;
@@ -3128,7 +3120,6 @@ expr Assume::getTypeConstraints(const Function &f) const {
case WellDefined:
return true;
case AndNonPoison:
- case IfNonPoison:
return args[0]->getType().enforceIntType();
case Align:
return args[0]->getType().enforcePtrType() &&
@@ -3144,6 +3135,81 @@ unique_ptr<Instr> Assume::dup(Function &f, const string &suffix) const {
}
+AssumeVal::AssumeVal(Type &type, string &&name, Value &val,
+ vector<Value *> &&args0, Kind kind)
+ : Instr(type, std::move(name)), val(&val), args(std::move(args0)),
+ kind(kind) {
+ if (kind == Range) {
+ assert((args.size() & 1) == 0);
+ }
+}
+
+vector<Value*> AssumeVal::operands() const {
+ auto ret = args;
+ ret.emplace_back(val);
+ return ret;
+}
+
+void AssumeVal::rauw(const Value &what, Value &with) {
+ RAUW(val);
+ for (auto &arg: args)
+ RAUW(arg);
+}
+
+void AssumeVal::print(ostream &os) const {
+ const char *str = nullptr;
+ switch (kind) {
+ case Range: str = "range "; break;
+ }
+
+ os << getName() << " = " << str << *val;
+
+ for (auto &arg: args) {
+ os << ", " << *arg;
+ }
+}
+
+StateValue AssumeVal::toSMT(State &s) const {
+ auto &v = s[*val];
+
+ switch (kind) {
+ case Range: { // val in [l1, h1) U ... U [ln, hn) (signed)
+ OrExpr inrange;
+ for (unsigned i = 0, e = args.size(); i != e; i += 2) {
+ auto &lb = s[*args[i]].value;
+ auto &hb = s[*args[i+1]].value;
+ auto l = v.value.sge(lb);
+ auto h = v.value.slt(hb);
+
+ if (lb.sgt(hb).isTrue()) { // wrapping interval
+ inrange.add(std::move(l));
+ inrange.add(std::move(h));
+ } else {
+ inrange.add(l && h);
+ }
+ }
+ return { expr(v.value), v.non_poison && std::move(inrange)() };
+ }
+ }
+ UNREACHABLE();
+}
+
+expr AssumeVal::getTypeConstraints(const Function &f) const {
+ switch (kind) {
+ case Range:
+ return getType() == val->getType() &&
+ args[0]->getType().enforceIntType() &&
+ args[1]->getType().enforceIntType();
+ }
+ UNREACHABLE();
+}
+
+unique_ptr<Instr> AssumeVal::dup(Function &f, const string &suffix) const {
+ return make_unique<AssumeVal>(getType(), getName() + suffix, *val,
+ vector<Value*>(args), kind);
+}
+
+
MemInstr::ByteAccessInfo MemInstr::ByteAccessInfo::intOnly(unsigned bytesz) {
ByteAccessInfo info;
info.byteSize = bytesz;

MODIFY
ir/instr.h
ir/instr.h
@@ -562,7 +562,6 @@ 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)
Align, /// args[0] satisfies alignment args[1]
NonNull /// args[0] is a nonnull pointer
@@ -586,6 +585,32 @@ public:
};
+// yields poison if invalid
+class AssumeVal final : public Instr {
+public:
+ enum Kind {
+ Range,
+ };
+
+private:
+ Value *val;
+ std::vector<Value*> args;
+ Kind kind;
+
+public:
+ AssumeVal(Type &type, std::string &&name, Value &val,
+ std::vector<Value *> &&args, Kind kind);
+
+ std::vector<Value*> operands() const override;
+ void rauw(const Value &what, Value &with) override;
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr>
+ dup(Function &f, const std::string &suffix) const override;
+};
+
+
class MemInstr : public Instr {
public:
MemInstr(Type &type, std::string &&name) : Instr(type, std::move(name)) {}

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -1193,7 +1193,7 @@ public:
return {};
}
- bool handleMetadata(llvm::Instruction &llvm_i, Instr &i) {
+ bool handleMetadata(Function &Fn, llvm::Instruction &llvm_i, Instr &i) {
llvm::SmallVector<pair<unsigned, llvm::MDNode*>, 8> MDs;
llvm_i.getAllMetadataOtherThanDebugLoc(MDs);
@@ -1201,48 +1201,20 @@ public:
switch (ID) {
case LLVMContext::MD_range:
{
- Value *range = nullptr;
- auto &boolTy = get_int_type(1);
+ vector<Value*> args;
for (unsigned op = 0, e = Node->getNumOperands(); op < e; ++op) {
- auto *low =
- llvm::mdconst::extract<llvm::ConstantInt>(Node->getOperand(op));
- auto *high =
- llvm::mdconst::extract<llvm::ConstantInt>(Node->getOperand(++op));
-
- auto op_name = to_string(op / 2);
- auto l = make_unique<ICmp>(boolTy,
- "%range_l#" + op_name + value_name(llvm_i),
- ICmp::SGE, i, *get_operand(low));
-
- auto h = make_unique<ICmp>(boolTy,
- "%range_h#" + op_name + value_name(llvm_i),
- ICmp::SLT, i, *get_operand(high));
-
- bool wrap = low->getValue().sgt(high->getValue());
- auto r = make_unique<BinOp>(boolTy,
- "%range#" + op_name + value_name(llvm_i),
- *l.get(), *h.get(),
- wrap ? BinOp::Or : BinOp::And);
-
- auto r_ptr = r.get();
- BB->addInstr(std::move(l));
- BB->addInstr(std::move(h));
- BB->addInstr(std::move(r));
-
- if (range) {
- auto range_or = make_unique<BinOp>(boolTy,
- "$rangeOR$" + op_name +
- value_name(llvm_i),
- *range, *r_ptr, BinOp::Or);
- range = range_or.get();
- BB->addInstr(std::move(range_or));
- } else {
- range = r_ptr;
- }
- }
-
- if (range)
- BB->addInstr(make_unique<Assume>(*range, Assume::IfNonPoison));
+ args.emplace_back(get_operand(
+ llvm::mdconst::extract<llvm::ConstantInt>(Node->getOperand(op))));
+ args.emplace_back(get_operand(
+ llvm::mdconst::extract<llvm::ConstantInt>(Node->getOperand(++op))));
+ }
+
+ auto assume
+ = make_unique<AssumeVal>(i.getType(), i.getName() + "_range", i,
+ std::move(args), AssumeVal::Range);
+ Fn.rauw(i, *assume);
+ replace_identifier(llvm_i, *assume);
+ BB->addInstr(std::move(assume));
break;
}
@@ -1646,7 +1618,7 @@ public:
BB->addInstr(std::move(I));
if (i.hasMetadataOtherThanDebugLoc() &&
- !handleMetadata(i, *alive_i))
+ !handleMetadata(Fn, i, *alive_i))
return {};
} else
return {};

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -409,6 +409,10 @@ void add_identifier(const llvm::Value &llvm, Value &v) {
value_cache.emplace(&llvm, &v);
}
+void replace_identifier(const llvm::Value &llvm, Value &v) {
+ value_cache[&llvm] = &v;
+}
+
#define PRINT(T) \
ostream& operator<<(ostream &os, const T &x) { \

MODIFY
llvm_util/utils.h
llvm_util/utils.h
@@ -45,6 +45,7 @@ IR::Value* get_operand(llvm::Value *v,
std::function<IR::Value*(IR::AggregateValue *)> copy_inserter);
void add_identifier(const llvm::Value &llvm, IR::Value &v);
+void replace_identifier(const llvm::Value &llvm, IR::Value &v);
#define PRINT(T) std::ostream& operator<<(std::ostream &os, const T &x);
PRINT(llvm::Type)

MODIFY
tests/unit/call-error6.opt
tests/unit/call-error6.opt
@@ -11,8 +11,8 @@ assume(%eq2)
%eq3 = icmp ule i8 %c1, 9
%eq4 = icmp ule i8 %c2, 9
-assume_non_poison(%eq3)
-assume_non_poison(%eq4)
+assume(%eq3)
+assume(%eq4)
%d = add i8 %c1, %c2
ret i8 %d

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -301,7 +301,6 @@ space+ {
"ninf" { return NINF; }
"nsz" { return NSZ; }
"assume" { return ASSUME; }
-"assume_non_poison" { return ASSUME_NON_POISON; }
"unreachable" { return UNREACH; }
"memory" { return MEMORY; }
"read" { return READ; }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -1294,12 +1294,11 @@ static unique_ptr<Instr> parse_instr(string_view name) {
UNREACHABLE();
}
-static unique_ptr<Instr> parse_assume(bool if_non_poison) {
+static unique_ptr<Instr> parse_assume() {
tokenizer.ensure(LPAREN);
auto &val = parse_operand(*int_types[1].get());
tokenizer.ensure(RPAREN);
- return make_unique<Assume>(val, if_non_poison ? Assume::IfNonPoison :
- Assume::AndNonPoison);
+ return make_unique<Assume>(val, Assume::AndNonPoison);
}
static unique_ptr<Instr> parse_return() {
@@ -1316,10 +1315,7 @@ static void parse_fn(Function &f) {
while (true) {
switch (auto t = *tokenizer) {
case ASSUME:
- bb->addInstr(parse_assume(false));
- break;
- case ASSUME_NON_POISON:
- bb->addInstr(parse_assume(true));
+ bb->addInstr(parse_assume());
break;
case LABEL:
bb = &f.getBB(yylval.str);

MODIFY
tools/tokens.h
tools/tokens.h
@@ -9,7 +9,6 @@ TOKEN(ARRAY_TYPE_PREFIX)
TOKEN(ARROW)
TOKEN(ASHR)
TOKEN(ASSUME)
-TOKEN(ASSUME_NON_POISON)
TOKEN(BAND)
TOKEN(BITCAST)
TOKEN(BITREVERSE)

switch semantics of range metadata to yield poison rather than UB on failure
LLVM 16 adjusted the semantics