add noundef support to FpConversionOp
MODIFY
ir/attrs.h
ir/attrs.h
@@ -203,6 +203,7 @@ struct FpExceptionMode final {
FpExceptionMode() : mode(Ignore) {}
FpExceptionMode(Mode mode) : mode(mode) {}
Mode getMode() const { return mode; }
+ bool ignore() const { return mode == Ignore; }
friend std::ostream& operator<<(std::ostream &os, FpExceptionMode ex);
};

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -475,8 +475,8 @@ StateValue BinOp::toSMT(State &s) const {
};
}
- auto &a = noundef ? s.getAndAddPoisonUB(*lhs) : s[*lhs];
- auto &b = (isDivOrRem() || noundef) ? s.getAndAddPoisonUB(*rhs) : s[*rhs];
+ auto &a = s.getVal(*lhs, noundef);
+ auto &b = s.getVal(*rhs, isDivOrRem() || noundef);
if (lhs->getType().isVectorType()) {
auto retty = getType().getAsAggregateType();
@@ -616,6 +616,7 @@ void FpBinOp::print(ostream &os) const {
os << getName() << " = " << str << fmath << *lhs << ", " << rhs->getName();
if (!rm.isDefault())
os << ", rounding=" << rm;
+ if (!ex.ignore())
os << ", exceptions=" << ex;
}
@@ -1059,6 +1060,7 @@ void FpUnaryOp::print(ostream &os) const {
os << getName() << " = " << str << fmath << *val;
if (!rm.isDefault())
os << ", rounding=" << rm;
+ if (!ex.ignore())
os << ", exceptions=" << ex;
}
@@ -1343,6 +1345,7 @@ void FpTernaryOp::print(ostream &os) const {
os << getName() << " = " << str << fmath << *a << ", " << *b << ", " << *c;
if (!rm.isDefault())
os << ", rounding=" << rm;
+ if (!ex.ignore())
os << ", exceptions=" << ex;
}
@@ -1662,11 +1665,15 @@ void FpConversionOp::print(ostream &os) const {
os << getName() << " = " << str << *val << print_type(getType(), " to ", "");
if (!rm.isDefault())
os << ", rounding=" << rm;
+ if (!ex.ignore())
os << ", exceptions=" << ex;
+ if (flags & NoUndef)
+ os << ", !noundef";
}
StateValue FpConversionOp::toSMT(State &s) const {
- auto &v = s[*val];
+ bool noundef = flags & NoUndef;
+ auto &v = s.getVal(*val, noundef);
function<StateValue(const expr &, const Type &, FpRoundingMode)> fn;
switch (op) {
@@ -1750,11 +1757,16 @@ StateValue FpConversionOp::toSMT(State &s) const {
StateValue ret = to_type.isFloatType() ? round_value(s, rm, np, fn_rm)
: fn(val, to_type, rm);
+ np.add(std::move(ret.non_poison));
+
+ if (noundef) {
+ s.addUB(np());
+ np.reset();
+ }
return { to_type.isFloatType()
? to_type.getAsFloatType()->fromFloat(s, ret.value)
- : std::move(ret.value),
- np() && ret.non_poison};
+ : std::move(ret.value), np()};
};
if (getType().isVectorType()) {

MODIFY
ir/instr.h
ir/instr.h
@@ -278,16 +278,21 @@ public:
enum Op { SIntToFP, UIntToFP, FPToSInt, FPToUInt, FPExt, FPTrunc, LRInt,
LRound };
+ enum Flags { None = 0, NoUndef = 1<<0 };
+
private:
Value *val;
Op op;
FpRoundingMode rm;
FpExceptionMode ex;
+ unsigned flags;
public:
FpConversionOp(Type &type, std::string &&name, Value &val, Op op,
- FpRoundingMode rm = {}, FpExceptionMode ex = {})
- : Instr(type, std::move(name)), val(&val), op(op), rm(rm), ex(ex) {}
+ FpRoundingMode rm = {}, FpExceptionMode ex = {},
+ unsigned flags = None)
+ : Instr(type, std::move(name)), val(&val), op(op), rm(rm), ex(ex),
+ flags(flags) {}
std::vector<Value*> operands() const override;
bool propagatesPoison() const override;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -595,6 +595,10 @@ State::getAndAddPoisonUB(const Value &val, bool undef_ub_too,
sv.non_poison.isBool() ? true : expr::mkInt(-1, sv.non_poison) };
}
+const StateValue& State::getVal(const Value &val, bool is_poison_ub) {
+ return is_poison_ub ? getAndAddPoisonUB(val) : (*this)[val];
+}
+
const expr& State::getWellDefinedPtr(const Value &val) {
return getAndAddPoisonUB(val, true, true).value;
}

MODIFY
ir/state.h
ir/state.h
@@ -204,6 +204,7 @@ public:
// If undef_ub is true, UB is also added when val was undef
const StateValue& getAndAddPoisonUB(const Value &val, bool undef_ub = false,
bool ptr_compare = false);
+ const StateValue& getVal(const Value &val, bool is_poison_ub);
const smt::expr& getWellDefinedPtr(const Value &val);
const ValTy& at(const Value &val) const;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -1035,6 +1035,7 @@ public:
case llvm::Intrinsic::experimental_constrained_fptosi:
case llvm::Intrinsic::experimental_constrained_fptoui:
case llvm::Intrinsic::experimental_constrained_fpext:
+ case llvm::Intrinsic::fptrunc_round:
case llvm::Intrinsic::experimental_constrained_fptrunc:
case llvm::Intrinsic::lrint:
case llvm::Intrinsic::experimental_constrained_lrint:
@@ -1053,6 +1054,7 @@ public:
case llvm::Intrinsic::experimental_constrained_fptosi: op = FpConversionOp::FPToSInt; break;
case llvm::Intrinsic::experimental_constrained_fptoui: op = FpConversionOp::FPToUInt; break;
case llvm::Intrinsic::experimental_constrained_fpext: op = FpConversionOp::FPExt; break;
+ case llvm::Intrinsic::fptrunc_round:
case llvm::Intrinsic::experimental_constrained_fptrunc: op = FpConversionOp::FPTrunc; break;
case llvm::Intrinsic::lrint:
case llvm::Intrinsic::experimental_constrained_lrint:
@@ -1064,9 +1066,15 @@ public:
case llvm::Intrinsic::experimental_constrained_llround: op = FpConversionOp::LRound; break;
default: UNREACHABLE();
}
+ FnAttrs attrs;
+ parse_fn_attrs(i, attrs);
+ unsigned flags = FpConversionOp::None;
+ if (attrs.has(FnAttrs::NoUndef))
+ flags |= FpConversionOp::NoUndef;
RETURN_IDENTIFIER(make_unique<FpConversionOp>(*ty, value_name(i), *val,
op, parse_rounding(i),
- parse_exceptions(i)));
+ parse_exceptions(i),
+ flags));
}
case llvm::Intrinsic::is_fpclass:
{

add noundef support to FpConversionOp