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,10 @@
+CORE broken-z3-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Z3 appears to suffer from a similar bug as we previously did.

src/solvers/floatbv/float_utils.cpp

@@ -195,6 +195,7 @@ bvt float_utilst::conversion(
     if(dest_spec.e > spec.e)
     {
       normalization_shift(result.fraction, result.exponent);
+      result.exponent.resize(dest_spec.e);
     }
 
     // the flags get copied
@@ -792,8 +793,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());