Floating-point normalization must not overflow

We need to extend the exponent to compute a new exponent without
overflow; subsequent denormalization and rounding will ensure the
exponent fits into the target format.

Fixes: #7616

Author: tautschnig

regression/cbmc/Float-rounding2/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+
+int main()
+{
+#if 0
+  // examples of constants that previously exhibited wrong behaviour
+  union U
+  {
+    double d;
+    uint64_t b;
+  };
+  union U u = {
+    .b = 0b0000000000000011111111111111111111111110000001000000000000000000};
+  union U u2 = {
+    .b = 0b0000000000000000000000000000001111111111111111111111111000000000};
+  double d = u.d;
+#else
+  double d;
+#endif
+  float f;
+  if(d > 0.0 && d < 1.0)
+  {
+    f = d;
+    assert(f <= 1.0f);
+  }
+  return 0;
+}

regression/cbmc/Float-rounding2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/floatbv/float_utils.cpp

@@ -792,8 +792,9 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
   PRECONDITION(!fraction.empty());
   std::size_t depth = address_bits(fraction.size() - 1);
 
-  if(exponent.size()<depth)
-    exponent=bv_utils.sign_extension(exponent, depth);
+  // sign-extend to ensure the arithmetic below cannot result in overflow/underflow
+  exponent =
+    bv_utils.sign_extension(exponent, std::max(depth, exponent.size() + 1));
 
   bvt exponent_delta=bv_utils.zeros(exponent.size());