fix for floating-point division for the case of normal / subnormal

Author: kroening

regression/cbmc/Float-div2/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <math.h>
+
+float nondet_float (void);
+
+int main (void) {
+	float f = nondet_float();
+        // Everything in this range hits the bug
+	__CPROVER_assume(f < +INFINITY);
+	__CPROVER_assume(f >= 0x1.0p+107f);
+	__CPROVER_assume(f > 0.0f);
+
+	float g = nondet_float();
+	__CPROVER_assume(g <= 0x1.0p-149f);
+	__CPROVER_assume(g > 0.0f);
+
+	// exponent is >= 107 - -127 = 234 = 255 - 21
+	float div = f / g;
+
+	assert(!(div == 0.0));
+
+	return 1;
+}

regression/cbmc/Float-div2/test.desc

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

src/solvers/floatbv/float_utils.cpp

@@ -632,8 +632,9 @@ bvt float_utilst::div(const bvt &src1, const bvt &src2)
 
   // We will subtract the exponents;
   // to account for overflow, we add a bit.
-  const bvt exponent1=bv_utils.sign_extension(unpacked1.exponent, unpacked1.exponent.size()+1);
-  const bvt exponent2=bv_utils.sign_extension(unpacked2.exponent, unpacked2.exponent.size()+1);
+  // we add a second bit for the adjust by extra fraction bits
+  const bvt exponent1=bv_utils.sign_extension(unpacked1.exponent, unpacked1.exponent.size()+2);
+  const bvt exponent2=bv_utils.sign_extension(unpacked2.exponent, unpacked2.exponent.size()+2);
 
   // subtract exponents
   bvt added_exponent=bv_utils.sub(exponent1, exponent2);