Merge pull request diffblue#2584 from diffblue/fp-constant-folding

kroening · web-flow · commit 64a63a0d8530 · 2018-07-19T11:27:16.000+01:00
ANSI-C: Floating-point constant folding
diff --git a/regression/cbmc/switch7/main.c b/regression/cbmc/switch7/main.c
@@ -0,0 +1,23 @@
+// These need to be constant-folded at compile time
+
+#define C1 (int)(0. / 1. + 0.5)
+#define C2 (int)(1. / 1. + 0.5)
+
+int nondet_int();
+
+int main(void)
+{
+  int i = nondet_int();
+
+  switch(i)
+  {
+  case C1:
+    break;
+
+  case C2:
+    break;
+
+  default:
+    break;
+  }
+}
diff --git a/regression/cbmc/switch7/test.desc b/regression/cbmc/switch7/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #include "builtin_factory.h"
 #include "c_typecast.h"
 #include "c_qualifiers.h"
@@ -3372,6 +3374,13 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
 
 void c_typecheck_baset::make_constant(exprt &expr)
 {
+  // Floating-point expressions may require a rounding mode.
+  // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
+  // Some compilers have command-line options to override.
+  const auto rounding_mode =
+    from_integer(ieee_floatt::ROUND_TO_EVEN, signed_int_type());
+  adjust_float_expressions(expr, rounding_mode);
+
   simplify(expr, *this);
 
   if(!expr.is_constant() &&
diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp
@@ -20,9 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_model.h"
 
-static bool have_to_adjust_float_expressions(
-  const exprt &expr,
-  const namespacet &ns)
+static bool have_to_adjust_float_expressions(const exprt &expr)
 {
   if(expr.id()==ID_floatbv_plus ||
      expr.id()==ID_floatbv_minus ||
@@ -33,11 +31,11 @@ static bool have_to_adjust_float_expressions(
      expr.id()==ID_floatbv_typecast)
     return false;
 
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
-  if(type.id()==ID_floatbv ||
-     (type.id()==ID_complex &&
-      ns.follow(type.subtype()).id()==ID_floatbv))
+  if(
+    type.id() == ID_floatbv ||
+    (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
   {
     if(expr.id()==ID_plus || expr.id()==ID_minus ||
        expr.id()==ID_mult || expr.id()==ID_div ||
@@ -69,35 +67,29 @@ static bool have_to_adjust_float_expressions(
   }
 
   forall_operands(it, expr)
-    if(have_to_adjust_float_expressions(*it, ns))
+    if(have_to_adjust_float_expressions(*it))
       return true;
 
   return false;
 }
 
 /// This adds the rounding mode to floating-point operations, including those in
 /// vectors and complex numbers.
-void adjust_float_expressions(
-  exprt &expr,
-  const namespacet &ns)
+void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
 {
-  if(!have_to_adjust_float_expressions(expr, ns))
+  if(!have_to_adjust_float_expressions(expr))
     return;
 
-  Forall_operands(it, expr)
-    adjust_float_expressions(*it, ns);
+  // recursive call
+  for(auto &op : expr.operands())
+    adjust_float_expressions(op, rounding_mode);
 
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
-  if(type.id()==ID_floatbv ||
-     (type.id()==ID_complex &&
-      ns.follow(type.subtype()).id()==ID_floatbv))
+  if(
+    type.id() == ID_floatbv ||
+    (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
   {
-    symbol_exprt rounding_mode=
-      ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
-
-    rounding_mode.add_source_location()=expr.source_location();
-
     if(expr.id()==ID_plus || expr.id()==ID_minus ||
        expr.id()==ID_mult || expr.id()==ID_div ||
        expr.id()==ID_rem)
@@ -128,11 +120,6 @@ void adjust_float_expressions(
     const typet &src_type=typecast_expr.op().type();
     const typet &dest_type=typecast_expr.type();
 
-    symbol_exprt rounding_mode=
-      ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
-
-    rounding_mode.add_source_location()=expr.source_location();
-
     if(dest_type.id()==ID_floatbv &&
        src_type.id()==ID_floatbv)
     {
@@ -179,6 +166,21 @@ void adjust_float_expressions(
   }
 }
 
+/// This adds the rounding mode to floating-point operations, including those in
+/// vectors and complex numbers.
+void adjust_float_expressions(exprt &expr, const namespacet &ns)
+{
+  if(!have_to_adjust_float_expressions(expr))
+    return;
+
+  symbol_exprt rounding_mode =
+    ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
+
+  rounding_mode.add_source_location() = expr.source_location();
+
+  adjust_float_expressions(expr, rounding_mode);
+}
+
 void adjust_float_expressions(
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns)
diff --git a/src/goto-programs/adjust_float_expressions.h b/src/goto-programs/adjust_float_expressions.h
@@ -22,6 +22,8 @@ void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns);
 
+void adjust_float_expressions(exprt &expr, const exprt &rounding_mode);
+
 void adjust_float_expressions(
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns);
