rewrite_union, adjust_float_expressions: modify expressions only when necessary

Author: tautschnig

src/goto-symex/adjust_float_expressions.cpp

@@ -19,19 +19,18 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
-Function: adjust_float_expressions
+Function: have_to_adjust_float_expressions
 
   Inputs:
 
  Outputs:
 
- Purpose: This adds the rounding mode to floating-point operations,
-          including those in vectors and complex numbers.
+ Purpose:
 
 \*******************************************************************/
 
-void adjust_float_expressions(
-  exprt &expr,
+static bool have_to_adjust_float_expressions(
+  const exprt &expr,
   const namespacet &ns)
 {
   if(expr.id()==ID_floatbv_plus ||
@@ -41,6 +40,68 @@ void adjust_float_expressions(
      expr.id()==ID_floatbv_div ||
      expr.id()==ID_floatbv_rem ||
      expr.id()==ID_floatbv_typecast)
+    return false;
+
+  const typet &type=ns.follow(expr.type());
+
+  if(type.id()==ID_floatbv ||
+     (type.id()==ID_complex &&
+      ns.follow(type.subtype()).id()==ID_floatbv))
+  {
+    if(expr.id()==ID_plus || expr.id()==ID_minus ||
+       expr.id()==ID_mult || expr.id()==ID_div ||
+       expr.id()==ID_rem)
+      return true;
+  }
+
+  if(expr.id()==ID_typecast)
+  {
+    const typecast_exprt &typecast_expr=to_typecast_expr(expr);
+
+    const typet &src_type=typecast_expr.op().type();
+    const typet &dest_type=typecast_expr.type();
+
+    if(dest_type.id()==ID_floatbv &&
+       src_type.id()==ID_floatbv)
+      return true;
+    else if(dest_type.id()==ID_floatbv &&
+            (src_type.id()==ID_c_bool ||
+             src_type.id()==ID_signedbv ||
+             src_type.id()==ID_unsignedbv ||
+             src_type.id()==ID_c_enum_tag))
+      return true;
+    else if((dest_type.id()==ID_signedbv ||
+             dest_type.id()==ID_unsignedbv ||
+             dest_type.id()==ID_c_enum_tag) &&
+             src_type.id()==ID_floatbv)
+      return true;
+  }
+
+  forall_operands(it, expr)
+    if(have_to_adjust_float_expressions(*it, ns))
+      return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 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, ns))
     return;
 
   Forall_operands(it, expr)

src/goto-symex/rewrite_union.cpp

@@ -19,6 +19,40 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
+Function: have_to_rewrite_union
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static bool have_to_rewrite_union(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  if(expr.id()==ID_member)
+  {
+    const exprt &op=to_member_expr(expr).struct_op();
+    const typet &op_type=ns.follow(op.type());
+
+    if(op_type.id()==ID_union)
+      return true;
+  }
+  else if(expr.id()==ID_union)
+    return true;
+
+  forall_operands(it, expr)
+    if(have_to_rewrite_union(*it, ns))
+      return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
 Function: rewrite_union
 
   Inputs:
@@ -34,6 +68,9 @@ void rewrite_union(
   exprt &expr,
   const namespacet &ns)
 {
+  if(!have_to_rewrite_union(expr, ns))
+    return;
+
   Forall_operands(it, expr)
     rewrite_union(*it, ns);