Ignore sign difference between two NaNs

ir/type.cpp

@@ -525,6 +525,22 @@ expr FloatType::isNaN(const expr &v, bool signalling) const {
   }
 }
 
+smt::expr FloatType::toInt(State &s, smt::expr v) const {
+  expr isnan = v.BV2float(getDummyFloat()).isNaN();
+
+  if (isnan.isFalse())
+    return v;
+
+  expr sign = s.getFreshNondetVar("#sign", expr::mkUInt(0, 1));
+  expr nan = sign.concat(v.trunc(bits() - 1));
+
+  return expr::mkIf(isnan, nan, v);
+}
+
+IR::StateValue FloatType::toInt(State &s, IR::StateValue v) const {
+  return Type::toInt(s, std::move(v));
+}
+
 unsigned FloatType::bits() const {
   assert(fpType != Unknown);
   return float_sizes[fpType].first;
@@ -611,8 +627,13 @@ pair<expr, expr>
 FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
                    const StateValue &tgt) const {
   expr non_poison = src.non_poison && tgt.non_poison;
-  return { src.non_poison.implies(tgt.non_poison),
-           (src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
+  expr equal_payload =
+      src.value.trunc(fractionBits()) == tgt.value.trunc(fractionBits());
+  expr equal = src.value == tgt.value;
+  return {src.non_poison.implies(tgt.non_poison),
+          non_poison.implies(expr::mkIf(getFloat(src.value).isNaN() &&
+                                            getFloat(tgt.value).isNaN(),
+                                        equal_payload, equal))};
 }
 
 expr FloatType::mkInput(State &s, const char *name,

ir/type.h

@@ -207,6 +207,8 @@ class FloatType final : public Type {
                       unsigned nary, const smt::expr &a,
                       const smt::expr &b = {}, const smt::expr &c = {}) const;
   smt::expr isNaN(const smt::expr &v, bool signalling) const;
+  smt::expr toInt(State &s, smt::expr v) const override;
+  IR::StateValue toInt(State &s, IR::StateValue v) const override;
 
   IR::StateValue getDummyValue(bool non_poison) const override;
   smt::expr getTypeConstraints() const override;

tests/alive-tv/fp/fabs-fmf.srctgt.ll

@@ -9,5 +9,31 @@ define float @tgt() {
   ret float undef
 }
 
+; Ignore sign difference between two NaNs
+define half @src1(half noundef %x) {
+  %gtzero = fcmp ugt half %x, 0xH8000
+  %negx = fsub nnan ninf half 0xH0000, %x
+  %fabs = select ninf i1 %gtzero, half %x, half %negx
+  ret half %fabs
+}
+
+define half @tgt1(half noundef %x) {
+  %fabs = call ninf half @llvm.fabs(half %x)
+  ret half %fabs
+}
+
+define i16 @src2(half noundef %x) {
+  %gtzero = fcmp ugt half %x, 0xH8000
+  %negx = fsub nnan ninf half 0xH0000, %x
+  %fabs = select ninf i1 %gtzero, half %x, half %negx
+  %cast = bitcast half %fabs to i16
+  ret i16 %cast
+}
+
+define i16 @tgt2(half noundef %x) {
+  %fabs = call ninf half @llvm.fabs(half %x)
+  %cast = bitcast half %fabs to i16
+  ret i16 %cast
+}
 
 declare float @llvm.fabs.f32(float)

tests/alive-tv/fp/sign-nan.ll

@@ -0,0 +1,18 @@
+define half @src1(half nofpclass(norm sub inf zero) noundef %x) {
+  %fneg = fneg half %x
+  ret half %fneg
+}
+
+define half @tgt1(half noundef %x) {
+  ret half %x
+}
+
+define i1 @src2(half nofpclass(norm sub inf zero) noundef %x) {
+  %cast = bitcast half %x to i16
+  %cmp = icmp sgt i16 %cast, -1
+  ret i1 %cmp
+}
+
+define i1 @tgt2(half noundef %x) {
+  ret i1 true
+}