division-by-zero on float

This separates the division-by-zero check for floating-point operations from
the division-by-zero check for integers.  The new division-by-zero check for
floating-point operations is off by default, and is enabled by
--float-div-by-zero-check.

The case for doing so is weak.  ISO/IEC 9899:2021 (C21) and predecessors
clealy state (Sec 6.5.5 par 5) "In both operations, if the value of the
second operand is zero, the behavior is undefined."

However, Annex F (IEC 60559 floating-point arithmetic) states that
implementations that define __STDC_IEC_559__ must implement IEC 60559
division, which clearly defines the behavior when dividing floating-point
numbers by zero.  This behavior can be observed on all architectures that we
support.

Author: kroening

doc/man/cbmc.1

@@ -62,7 +62,10 @@ enable array bounds checks
 check shift greater than bit\-width
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-pointer\-primitive\-check\fR
 checks that all pointers in pointer primitives are valid or null

doc/man/goto-analyzer.1

@@ -521,7 +521,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
 explicitly freed before terminating the program.
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-signed\-overflow\-check\fR
 enable signed arithmetic over\- and underflow checks

doc/man/goto-diff.1

@@ -52,7 +52,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
 explicitly freed before terminating the program.
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-signed\-overflow\-check\fR
 enable signed arithmetic over\- and underflow checks

doc/man/goto-instrument.1

@@ -192,7 +192,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
 explicitly freed before terminating the program.
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-signed\-overflow\-check\fR
 enable signed arithmetic over\- and underflow checks

regression/cbmc/Division/floating_point_division1.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  assert(1.0 / 2 == 0.5);
+  assert(1.0 / 0 == INFINITY);
+  assert(-1.0 / 0 == -INFINITY);
+  assert(isnan(NAN / 0));
+  assert(1.0 / INFINITY == 0);
+  assert(isnan(INFINITY / INFINITY));
+}

regression/cbmc/Division/floating_point_division1.desc

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

regression/cbmc/Division/floating_point_division2.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <math.h>
+
+double nondet_double();
+
+int main()
+{
+  double y = nondet_double();
+
+  if(y == 0)
+  {
+    // we expect to catch this with --float-div-by-zero-check
+    double x = 1.0 / y;
+  }
+}

regression/cbmc/Division/floating_point_division2.desc

@@ -0,0 +1,9 @@
+CORE no-new-smt
+floating_point_division2.c
+--float-div-by-zero-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.float-division-by-zero\.1\] line \d+ floating-point division by zero in 1\.0 / y: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/pragma_cprover_enable_all/main.c

@@ -15,7 +15,7 @@ int main()
 #pragma CPROVER check push
 #pragma CPROVER check disable "bounds"
 #pragma CPROVER check disable "pointer"
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "enum-range"
 #pragma CPROVER check disable "signed-overflow"
 #pragma CPROVER check disable "unsigned-overflow"
@@ -52,7 +52,7 @@ int main()
 #pragma CPROVER check push
 #pragma CPROVER check enable "bounds"
 #pragma CPROVER check enable "pointer"
-#pragma CPROVER check enable "div-by-zero"
+#pragma CPROVER check enable "float-div-by-zero"
 #pragma CPROVER check enable "enum-range"
 #pragma CPROVER check enable "signed-overflow"
 #pragma CPROVER check enable "unsigned-overflow"

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -5,7 +5,7 @@ main.c
 ^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
 ^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
-^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
+^\[main\.float-division-by-zero\.\d+\] line 84 floating-point division by zero in x / den: FAILURE
 ^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
 ^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
 ^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
@@ -18,7 +18,7 @@ main.c
 ^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
 ^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
 ^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
-^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
+^\[main\.float-division-by-zero\.\d+\] line 47 floating-point division by zero in x / den: FAILURE
 ^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE
 ^\[main\.enum-range-check\.\d+\] line 48 enum range check in \(ABC\)10: FAILURE
 ^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE