From 0fad63149de9c500641c61907ddaa226d6ce39ec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 23 Jul 2026 11:05:54 +0000 Subject: [PATCH] util: IEEE-754 sign-aware expression builders (signbit/fabs/copysign) Centralise IEEE sign-bit semantics in ieee_signbit/ieee_fabs/ieee_copysign, built on sign_exprt so negative zero is handled correctly (copysign(1,-0.0) == -1.0, fabs(-0.0) == +0.0) -- unlike an 'x < 0' formulation. With a unit test covering signbit/fabs/copysign incl. the negative-zero cases. Co-authored-by: Kiro --- src/util/ieee_float.cpp | 27 +++++++++++++++++ src/util/ieee_float.h | 23 +++++++++++++++ unit/util/ieee_float.cpp | 62 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 112 insertions(+) diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 5f3a0f62587..8dd404c86c5 100644 --- a/src/util/ieee_float.cpp +++ b/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}; +} diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 8af2f9d308c..5d6d1649253 100644 --- a/src/util/ieee_float.h +++ b/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 diff --git a/unit/util/ieee_float.cpp b/unit/util/ieee_float.cpp index 2828944463d..2103b990134 100644 --- a/unit/util/ieee_float.cpp +++ b/unit/util/ieee_float.cpp @@ -7,6 +7,10 @@ Author: Daniel Kroening, dkr@amazon.com \*******************************************************************/ #include +#include +#include +#include +#include #include @@ -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]")