division-by-zero on float

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

@@ -16,6 +16,7 @@ int main()
 #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"
@@ -36,7 +37,7 @@ int main()
     ABC e;
     bool readable;
     char i;
-    signed int j;
+    signed int j, k;
     readable = __CPROVER_r_ok(q, 1);
     q = p + 2000000000000;
     q = r;
@@ -45,14 +46,16 @@ int main()
     else
       den = 1.0;
     y = x / den;
+    j = 10 / 0;
     e = 10;
     i += 1;
-    j += 1;
+    k += 1;
   }
 #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"
@@ -73,7 +76,7 @@ int main()
     ABC e;
     bool readable;
     char i;
-    signed int j;
+    signed int j, k;
     readable = __CPROVER_r_ok(q, 1);
     q = p + 2000000000000;
     q = r;
@@ -82,9 +85,10 @@ int main()
     else
       den = 1.0;
     y = x / den;
+    j = 10 / 0;
     e = 10;
     i += 1;
-    j += 1;
+    k += 1;
   }
 #pragma CPROVER check pop
 #pragma CPROVER check pop

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -1,27 +1,29 @@
 CORE no-new-smt
 main.c
---object-bits 8 --enum-range-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --nan-check
-^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[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\.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
-^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+--object-bits 8 --enum-range-check --div-by-zero-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --float-div-by-zero-check --conversion-check --nan-check
+^\[main\.pointer_primitives\.\d+\] line 80 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_primitives\.\d+\] line 80 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_arithmetic\.\d+\] line 81 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
+^\[main\.NaN\.\d+\] line 87 NaN on / in x / den: FAILURE
+^\[main\.float-division-by-zero\.\d+\] line 87 floating-point division by zero in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 87 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.division-by-zero\.\d+\] line 88 division by zero in 10 / 0: FAILURE$
+^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: FAILURE
+^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: FAILURE
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[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\.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
-^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
+^\[main\.NaN\.\d+\] line 48 NaN on / in x / den: FAILURE
+^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0: FAILURE$
+^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10: FAILURE
+^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1: FAILURE
 --
 This test uses all possible named-checks to maximize coverage.

src/ansi-c/goto_check_c.cpp

@@ -58,6 +58,8 @@ class goto_check_ct
     enable_memory_cleanup_check =
       _options.get_bool_option("memory-cleanup-check");
     enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
+    enable_float_div_by_zero_check =
+      _options.get_bool_option("float-div-by-zero-check");
     enable_enum_range_check = _options.get_bool_option("enum-range-check");
     enable_signed_overflow_check =
       _options.get_bool_option("signed-overflow-check");
@@ -179,6 +181,7 @@ class goto_check_ct
   void bounds_check_index(const index_exprt &, const guardt &);
   void bounds_check_bit_count(const unary_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
+  void float_div_by_zero_check(const div_exprt &, const guardt &);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void mod_overflow_check(const mod_exprt &, const guardt &);
   void enum_range_check(const exprt &, const guardt &);
@@ -262,6 +265,7 @@ class goto_check_ct
   bool enable_memory_leak_check;
   bool enable_memory_cleanup_check;
   bool enable_div_by_zero_check;
+  bool enable_float_div_by_zero_check;
   bool enable_enum_range_check;
   bool enable_signed_overflow_check;
   bool enable_unsigned_overflow_check;
@@ -282,6 +286,7 @@ class goto_check_ct
     {"memory-leak-check", &enable_memory_leak_check},
     {"memory-cleanup-check", &enable_memory_cleanup_check},
     {"div-by-zero-check", &enable_div_by_zero_check},
+    {"float-div-by-zero-check", &enable_float_div_by_zero_check},
     {"enum-range-check", &enable_enum_range_check},
     {"signed-overflow-check", &enable_signed_overflow_check},
     {"unsigned-overflow-check", &enable_unsigned_overflow_check},
@@ -508,6 +513,27 @@ void goto_check_ct::div_by_zero_check(
     guard);
 }
 
+void goto_check_ct::float_div_by_zero_check(
+  const div_exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_float_div_by_zero_check)
+    return;
+
+  // add divison by zero subgoal
+
+  exprt zero = from_integer(0, expr.op1().type());
+  const notequal_exprt inequality(expr.op1(), std::move(zero));
+
+  add_guarded_property(
+    inequality,
+    "floating-point division by zero",
+    "float-division-by-zero",
+    expr.find_source_location(),
+    expr,
+    guard);
+}
+
 void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
 {
   if(!enable_enum_range_check)
@@ -1850,7 +1876,21 @@ void goto_check_ct::check_rec_div(
   const div_exprt &div_expr,
   const guardt &guard)
 {
-  div_by_zero_check(to_div_expr(div_expr), guard);
+  if(
+    div_expr.type().id() == ID_signedbv ||
+    div_expr.type().id() == ID_unsignedbv || div_expr.type().id() == ID_c_bool)
+  {
+    // Division by zero is undefined behavior for all integer types.
+    div_by_zero_check(to_div_expr(div_expr), guard);
+  }
+  else if(div_expr.type().id() == ID_floatbv)
+  {
+    // Division by zero on floating-point numbers may be undefined behavior.
+    // Annex F of the ISO C21 suggests that implementations that
+    // define __STDC_IEC_559__ follow IEEE 754 semantics,
+    // which defines the outcome of division by zero.
+    float_div_by_zero_check(to_div_expr(div_expr), guard);
+  }
 
   if(div_expr.type().id() == ID_signedbv)
     integer_overflow_check(div_expr, guard);

src/ansi-c/goto_check_c.h

@@ -39,7 +39,8 @@ void goto_check_c(
 
 #define OPT_GOTO_CHECK                                                         \
   "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
-  "(div-by-zero-check)(enum-range-check)"                                      \
+  "(div-by-zero-check)(float-div-by-zero-check)"                               \
+  "(enum-range-check)"                                                         \
   "(signed-overflow-check)(unsigned-overflow-check)"                           \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
@@ -61,7 +62,10 @@ void goto_check_c(
   " {y--no-pointer-check} \t disable pointer checks\n"                         \
   " {y--memory-leak-check} \t enable memory leak checks\n"                     \
   " {y--memory-cleanup-check} \t enable memory cleanup checks\n"               \
-  " {y--div-by-zero-check} \t enable division by zero checks (default on)\n"   \
+  " {y--div-by-zero-check} \t "                                                \
+  "enable division by zero checks on integers (default on)\n"                  \
+  " {y--float-div-by-zero-check} \t "                                          \
+  "enable division by zero checks on floating-point numbers (default off)\n"   \
   " {y--no-div-by-zero-check} \t disable division by zero checks\n"            \
   " {y--signed-overflow-check} \t "                                            \
   "enable signed arithmetic over- and underflow checks (default on)\n"         \
@@ -123,6 +127,7 @@ void goto_check_c(
   PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "float-div-by-zero-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \