constrained FP ops: mismatch of rounding mode now yields poison
MODIFY
ir/attrs.cpp
ir/attrs.cpp
@@ -221,6 +221,7 @@ smt::expr FpRoundingMode::toSMT() const {
case FpRoundingMode::RTP: return expr::rtp();
case FpRoundingMode::RTN: return expr::rtn();
case FpRoundingMode::RTZ: return expr::rtz();
+ case FpRoundingMode::Default: UNREACHABLE();
}
UNREACHABLE();
}
@@ -234,6 +235,7 @@ ostream& operator<<(std::ostream &os, FpRoundingMode rounding) {
case FpRoundingMode::RTP: str = "upward"; break;
case FpRoundingMode::RTN: str = "downward"; break;
case FpRoundingMode::RTZ: str = "towardzero"; break;
+ case FpRoundingMode::Default: UNREACHABLE();
}
return os << str;
}

MODIFY
ir/attrs.h
ir/attrs.h
@@ -97,10 +97,12 @@ struct FastMathFlags final {
struct FpRoundingMode final {
- enum Mode { Dynamic, RNE, RNA, RTP, RTN, RTZ } mode;
- FpRoundingMode() : mode(RNE) {}
+ enum Mode { RNE, RNA, RTP, RTN, RTZ, Dynamic, Default } mode;
+ FpRoundingMode() : mode(Default) {}
FpRoundingMode(Mode mode) : mode(mode) {}
bool isDynamic() const { return mode == Dynamic; }
+ bool isDefault() const { return mode == Default; }
+ Mode getMode() const { return mode; }
smt::expr toSMT() const;
friend std::ostream& operator<<(std::ostream &os, FpRoundingMode rounding);
};

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -598,8 +598,9 @@ void FpBinOp::print(ostream &os) const {
case FMinimum: str = "fminimum "; break;
case CopySign: str = "copysign "; break;
}
- os << getName() << " = " << str << fmath << *lhs << ", " << rhs->getName()
- << ", rounding=" << rm;
+ os << getName() << " = " << str << fmath << *lhs << ", " << rhs->getName();
+ if (!rm.isDefault())
+ os << ", rounding=" << rm;
}
static expr any_fp_zero(State &s, const expr &v) {
@@ -701,10 +702,15 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
const State &s, FpRoundingMode rm) {
- if (!rm.isDynamic())
- return fn(rm);
+ if (rm.isDefault())
+ return fn(FpRoundingMode::RNE);
auto &var = s.getFpRoundingMode();
+ if (!rm.isDynamic()) {
+ auto [v, np] = fn(rm);
+ return { move(v), np && var == rm.getMode() };
+ }
+
return StateValue::mkIf(var == FpRoundingMode::RNE, fn(FpRoundingMode::RNE),
StateValue::mkIf(var == FpRoundingMode::RNA, fn(FpRoundingMode::RNA),
StateValue::mkIf(var == FpRoundingMode::RTP, fn(FpRoundingMode::RTP),
@@ -712,14 +718,6 @@ static StateValue round_value(const function<StateValue(FpRoundingMode)> &fn,
fn(FpRoundingMode::RTZ)))));
}
-static expr get_fp_rounding(const State &s) {
- auto &var = s.getFpRoundingMode();
- return expr::mkIf(var == FpRoundingMode::RNE, expr::rne(),
- expr::mkIf(var == FpRoundingMode::RNA, expr::rna(),
- expr::mkIf(var == FpRoundingMode::RTP, expr::rtp(),
- expr::mkIf(var == FpRoundingMode::RTN, expr::rtn(), expr::rtz()))));
-}
-
StateValue FpBinOp::toSMT(State &s) const {
function<StateValue(const expr&, const expr&, const expr&, const expr&,
FpRoundingMode)> fn;
@@ -989,7 +987,9 @@ void FpUnaryOp::print(ostream &os) const {
case Sqrt: str = "sqrt "; break;
}
- os << getName() << " = " << str << fmath << *val << ", rounding=" << rm;
+ os << getName() << " = " << str << fmath << *val;
+ if (!rm.isDefault())
+ os << ", rounding=" << rm;
}
StateValue FpUnaryOp::toSMT(State &s) const {
@@ -1260,8 +1260,9 @@ void FpTernaryOp::print(ostream &os) const {
case MulAdd: str = "fmuladd "; break;
}
- os << getName() << " = " << str << fmath << *a << ", " << *b << ", " << *c
- << ", rounding=" << rm;
+ os << getName() << " = " << str << fmath << *a << ", " << *b << ", " << *c;
+ if (!rm.isDefault())
+ os << ", rounding=" << rm;
}
StateValue FpTernaryOp::toSMT(State &s) const {
@@ -1492,8 +1493,9 @@ void FpConversionOp::print(ostream &os) const {
case LRound: str = "lround "; break;
}
- os << getName() << " = " << str << *val << print_type(getType(), " to ", "")
- << ", rounding=" << rm;
+ os << getName() << " = " << str << *val << print_type(getType(), " to ", "");
+ if (!rm.isDefault())
+ os << ", rounding=" << rm;
}
StateValue FpConversionOp::toSMT(State &s) const {
@@ -1516,14 +1518,14 @@ StateValue FpConversionOp::toSMT(State &s) const {
case FPToSInt:
case LRInt:
case LRound:
- fn = [&](auto &val, auto &to_type, auto rm_) -> StateValue {
+ fn = [&](auto &val, auto &to_type, auto rm_in) -> StateValue {
expr rm;
switch (op) {
case FPToSInt:
rm = expr::rtz();
break;
case LRInt:
- rm = get_fp_rounding(s);
+ rm = rm_in.toSMT();
break;
case LRound:
rm = expr::rna();

ADD
tests/alive-tv/fp/fadd3-fail.srctgt.ll
+; ERROR: Target is more poisonous than source
+
+define float @src(float noundef %a) {
+ %x = call float @llvm.experimental.constrained.fsub.f32(float %a, float 0.0, metadata !"round.upward", metadata !"fpexcept.strict")
+ %y = call float @llvm.experimental.constrained.fsub.f32(float %a, float 0.0, metadata !"round.upward", metadata !"fpexcept.strict")
+ %ret = call float @llvm.experimental.constrained.fsub.f32(float %x, float %y, metadata !"round.dynamic", metadata !"fpexcept.strict")
+ ret float %ret
+}
+
+define float @tgt(float noundef %a) {
+ ret float poison
+}
+
+declare float @llvm.experimental.constrained.fsub.f32(float, float, metadata, metadata)

ADD
tests/alive-tv/fp/fadd3.srctgt.ll
+define float @src(float %a) {
+ %x = call float @llvm.experimental.constrained.fsub.f32(float %a, float 0.0, metadata !"round.upward", metadata !"fpexcept.strict")
+ %y = call float @llvm.experimental.constrained.fsub.f32(float %a, float 0.0, metadata !"round.downward", metadata !"fpexcept.strict")
+ %ret = call float @llvm.experimental.constrained.fsub.f32(float %x, float %y, metadata !"round.dynamic", metadata !"fpexcept.strict")
+ ret float %ret
+}
+
+define float @tgt(float %a) {
+ ret float poison
+}
+
+declare float @llvm.experimental.constrained.fsub.f32(float, float, metadata, metadata)

constrained FP ops: mismatch of rounding mode now yields poison