constrained FP ops: mismatch of rounding mode now yields poison

Author: nunoplopes

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;
 }

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);
 };

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,25 +702,22 @@ 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),
          StateValue::mkIf(var == FpRoundingMode::RTN, fn(FpRoundingMode::RTN),
                           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();

tests/alive-tv/fp/fadd3-fail.srctgt.ll

@@ -0,0 +1,14 @@
+; 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)

tests/alive-tv/fp/fadd3.srctgt.ll

@@ -0,0 +1,12 @@
+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)