adjust_float_expressions can now take a rounding mode argument

Author: Daniel Kroening

src/goto-programs/adjust_float_expressions.cpp

@@ -20,9 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 #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))
+      type.subtype().id()==ID_floatbv))
   {
     if(expr.id()==ID_plus || expr.id()==ID_minus ||
        expr.id()==ID_mult || expr.id()==ID_div ||
@@ -69,7 +67,7 @@ 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;
@@ -79,25 +77,21 @@ static bool have_to_adjust_float_expressions(
 /// vectors and complex numbers.
 void adjust_float_expressions(
   exprt &expr,
-  const namespacet &ns)
+  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))
+      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 +122,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 +168,23 @@ 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)

src/goto-programs/adjust_float_expressions.h

@@ -22,6 +22,10 @@ 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);