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

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
+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

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--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"); \