util: IEEE-754 sign-aware expression builders (signbit/fabs/copysign)

src/util/ieee_float.cpp

@@ -1403,3 +1403,30 @@ ieee_floatt ieee_floatt::round_to_integral() const
     return result;
   }
 }
+
+exprt ieee_signbit(const exprt &f)
+{
+  PRECONDITION(f.type().id() == ID_floatbv);
+  // sign_exprt on a floating-point operand yields the IEEE sign bit
+  // (see simplify_sign / float_bvt::sign_bit): true for -0.0.
+  return sign_exprt{f};
+}
+
+exprt ieee_fabs(const exprt &f)
+{
+  PRECONDITION(f.type().id() == ID_floatbv);
+  // |f|: if the sign bit is set, negate; else keep. Negating clears the
+  // sign bit for -0.0 (so fabs(-0.0) == +0.0) and for finite negatives.
+  return if_exprt{sign_exprt{f}, unary_minus_exprt{f}, f};
+}
+
+exprt ieee_copysign(const exprt &magnitude, const exprt &sign_source)
+{
+  PRECONDITION(magnitude.type().id() == ID_floatbv);
+  PRECONDITION(sign_source.type().id() == ID_floatbv);
+  // Magnitude of `magnitude`, signed by the sign BIT of `sign_source`.
+  // Using the sign bit (not `sign_source < 0`) is what makes
+  // copysign(1.0, -0.0) == -1.0, matching IEEE-754 / C copysign.
+  const exprt mag = ieee_fabs(magnitude);
+  return if_exprt{sign_exprt{sign_source}, unary_minus_exprt{mag}, mag};
+}

src/util/ieee_float.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "format_spec.h"
 
 class constant_exprt;
+class exprt;
 class floatbv_typet;
 
 class ieee_float_spect
@@ -447,4 +448,26 @@ class ieee_floatt : public ieee_float_valuet
   void align();
 };
 
+// IEEE-754 sign-aware expression builders.
+//
+// These centralise IEEE sign-bit semantics so callers do not re-derive
+// them (and get them subtly wrong). The crucial point is that the sign of
+// a floating-point value is its sign BIT, which is independent of ordering:
+// `-0.0` has the sign bit set yet `-0.0 < 0.0` is false. Building these on
+// `x < 0` therefore mishandles negative zero (copysign(1.0, -0.0) must be
+// -1.0, fabs(-0.0) must be +0.0). They build on `sign_exprt` (ID_sign),
+// whose float semantics are exactly the IEEE sign bit.
+
+/// IEEE-754 signbit as a boolean expression: true iff the sign bit of the
+/// floating-point expression `f` is set (true for `-0.0`, reflects NaN sign).
+exprt ieee_signbit(const exprt &f);
+
+/// IEEE-754 fabs: the magnitude of `f` with the sign bit cleared, so
+/// `fabs(-0.0) == +0.0` and `fabs(-x) == x`.
+exprt ieee_fabs(const exprt &f);
+
+/// IEEE-754 copysign: a value with the magnitude of `magnitude` and the
+/// sign (sign BIT) of `sign_source`, so `copysign(1.0, -0.0) == -1.0`.
+exprt ieee_copysign(const exprt &magnitude, const exprt &sign_source);
+
 #endif // CPROVER_UTIL_IEEE_FLOAT_H

unit/util/ieee_float.cpp

@@ -7,6 +7,10 @@ Author: Daniel Kroening, dkr@amazon.com
 \*******************************************************************/
 
 #include <util/ieee_float.h>
+#include <util/namespace.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include <testing-utils/use_catch.h>
 
@@ -130,6 +134,64 @@ TEST_CASE("round_to_integral", "[unit][util][ieee_float]")
   REQUIRE(round_to_integral(from_double(dmax), away) == dmax);
 }
 
+TEST_CASE("ieee signbit / fabs / copysign", "[core][util][ieee_float]")
+{
+  const auto dp = ieee_float_spect::double_precision();
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+
+  // Build a double-precision floating-point constant expression.
+  auto fc = [&](double d) -> exprt
+  {
+    ieee_floatt v{dp, ieee_floatt::rounding_modet::ROUND_TO_EVEN};
+    v.from_double(d);
+    return v.to_expr();
+  };
+  // Evaluate a float-valued expression to a double via simplification.
+  auto eval = [&](const exprt &e) -> double
+  {
+    exprt s = simplify_expr(e, ns);
+    REQUIRE(s.is_constant());
+    ieee_float_valuet v{to_constant_expr(s)};
+    return v.to_double();
+  };
+  auto eval_bool = [&](const exprt &e) -> bool
+  { return simplify_expr(e, ns).is_true(); };
+
+  SECTION("signbit reflects the sign BIT, not ordering")
+  {
+    REQUIRE(eval_bool(ieee_signbit(fc(-0.0))));      // negative zero
+    REQUIRE_FALSE(eval_bool(ieee_signbit(fc(0.0)))); // positive zero
+    REQUIRE(eval_bool(ieee_signbit(fc(-3.5))));
+    REQUIRE_FALSE(eval_bool(ieee_signbit(fc(3.5))));
+  }
+
+  SECTION("fabs clears the sign bit, incl. negative zero")
+  {
+    REQUIRE(eval(ieee_fabs(fc(-3.5))) == 3.5);
+    REQUIRE(eval(ieee_fabs(fc(3.5))) == 3.5);
+    // fabs(-0.0) == +0.0: value compares equal to 0, and the sign bit
+    // of the result must be clear.
+    REQUIRE(eval(ieee_fabs(fc(-0.0))) == 0.0);
+    REQUIRE_FALSE(eval_bool(ieee_signbit(ieee_fabs(fc(-0.0)))));
+  }
+
+  SECTION("copysign takes the sign from the sign bit of the source")
+  {
+    // The negative-zero cases are the ones a `< 0` implementation gets
+    // wrong: -0.0 is not < 0, yet copysign must treat it as negative.
+    REQUIRE(eval(ieee_copysign(fc(1.0), fc(-0.0))) == -1.0);
+    REQUIRE(eval_bool(ieee_signbit(ieee_copysign(fc(1.0), fc(-0.0)))));
+    REQUIRE(eval(ieee_copysign(fc(1.0), fc(0.0))) == 1.0);
+    REQUIRE_FALSE(eval_bool(ieee_signbit(ieee_copysign(fc(1.0), fc(0.0)))));
+    REQUIRE(eval(ieee_copysign(fc(1.0), fc(-5.0))) == -1.0);
+    REQUIRE(eval(ieee_copysign(fc(-1.0), fc(5.0))) == 1.0);
+    REQUIRE(eval(ieee_copysign(fc(2.0), fc(-3.0))) == -2.0);
+    // Magnitude's own sign is irrelevant; only its absolute value is used.
+    REQUIRE(eval(ieee_copysign(fc(-2.0), fc(3.0))) == 2.0);
+  }
+}
+
 TEST_CASE(
   "ieee_float_valuet to_double / to_float round-trip",
   "[core][util][ieee_float]")