Apply adjust_float_expressions, rewrite_union just once per expression

These should be applied once across all goto functions instead of possibly
applying them multiple times to the same source expression during symbolic
execution.

Signed-off-by: Michael Tautschnig <[email protected]>

Author: tautschnig

src/cbmc/cbmc_parse_options.cpp

@@ -39,6 +39,9 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/show_goto_functions.h>
 
+#include <goto-symex/rewrite_union.h>
+#include <goto-symex/adjust_float_expressions.h>
+
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
@@ -891,10 +894,13 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_returns(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
     remove_complex(symbol_table, goto_functions);
+    rewrite_union(goto_functions, ns);
 
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
     goto_check(ns, options, goto_functions);
+    // checks don't know about adjusted float expressions
+    adjust_float_expressions(goto_functions, ns);
 
     // ignore default/user-specified initialization
     // of variables with static lifetime

src/goto-symex/adjust_float_expressions.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_model.h>
+
 #include "adjust_float_expressions.h"
 
 /*******************************************************************\
@@ -32,6 +34,15 @@ void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns)
 {
+  if(expr.id()==ID_floatbv_plus ||
+     expr.id()==ID_floatbv_minus ||
+     expr.id()==ID_floatbv_mult ||
+     expr.id()==ID_floatbv_div ||
+     expr.id()==ID_floatbv_div ||
+     expr.id()==ID_floatbv_rem ||
+     expr.id()==ID_floatbv_typecast)
+    return;
+
   Forall_operands(it, expr)
     adjust_float_expressions(*it, ns);
 
@@ -126,3 +137,64 @@ void adjust_float_expressions(
     }
   }
 }
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+static void adjust_float_expressions(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
+{
+  Forall_goto_program_instructions(it, goto_function.body)
+  {
+    adjust_float_expressions(it->code, ns);
+    adjust_float_expressions(it->guard, ns);
+  }
+}
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void adjust_float_expressions(
+  goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  Forall_goto_functions(it, goto_functions)
+    adjust_float_expressions(it->second, ns);
+}
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void adjust_float_expressions(goto_modelt &goto_model)
+{
+  namespacet ns(goto_model.symbol_table);
+  adjust_float_expressions(goto_model.goto_functions, ns);
+}

src/goto-symex/adjust_float_expressions.h

@@ -9,11 +9,18 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 #define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 
-#include <util/expr.h>
-#include <util/namespace.h>
+class exprt;
+class namespacet;
+class goto_functionst;
+class goto_modelt;
 
 void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns);
 
+void adjust_float_expressions(
+  goto_functionst &goto_functions,
+  const namespacet &ns);
+void adjust_float_expressions(goto_modelt &goto_model);
+
 #endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H

src/goto-symex/rewrite_union.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/byte_operators.h>
 
+#include <goto-programs/goto_model.h>
+
 #include <ansi-c/c_types.h>
 
 #include "rewrite_union.h"
@@ -57,3 +59,64 @@ void rewrite_union(
     expr=tmp;
   }
 }
+
+/*******************************************************************\
+
+Function: rewrite_union
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+static void rewrite_union(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
+{
+  Forall_goto_program_instructions(it, goto_function.body)
+  {
+    rewrite_union(it->code, ns);
+    rewrite_union(it->guard, ns);
+  }
+}
+
+/*******************************************************************\
+
+Function: rewrite_union
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void rewrite_union(
+  goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  Forall_goto_functions(it, goto_functions)
+    rewrite_union(it->second, ns);
+}
+
+/*******************************************************************\
+
+Function: rewrite_union
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void rewrite_union(goto_modelt &goto_model)
+{
+  namespacet ns(goto_model.symbol_table);
+  rewrite_union(goto_model.goto_functions, ns);
+}

src/goto-symex/rewrite_union.h

@@ -9,11 +9,20 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_REWRITE_UNION_H
 #define CPROVER_GOTO_SYMEX_REWRITE_UNION_H
 
-#include <util/expr.h>
-#include <util/namespace.h>
+#include <goto-programs/goto_functions.h>
+
+class exprt;
+class namespacet;
+class goto_functionst;
+class goto_modelt;
 
 void rewrite_union(
   exprt &expr,
   const namespacet &ns);
 
+void rewrite_union(
+  goto_functionst &goto_functions,
+  const namespacet &ns);
+void rewrite_union(goto_modelt &goto_model);
+
 #endif // CPROVER_GOTO_SYMEX_REWRITE_UNION_H

src/goto-symex/symex_clean_expr.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_types.h>
 
-#include "adjust_float_expressions.h"
-#include "rewrite_union.h"
 #include "goto_symex.h"
 
 /*******************************************************************\
@@ -199,9 +197,7 @@ void goto_symext::clean_expr(
   statet &state,
   const bool write)
 {
-  rewrite_union(expr, ns);
   replace_nondet(expr);
   dereference(expr, state, write);
   replace_array_equal(expr);
-  adjust_float_expressions(expr, ns);
 }

src/path-symex/path_symex_state_read.cpp

@@ -11,9 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <pointer-analysis/dereference.h>
 
-#include <goto-symex/adjust_float_expressions.h>
-#include <goto-symex/rewrite_union.h>
-
 #include "path_symex_state.h"
 
 //#define DEBUG
@@ -41,21 +38,13 @@ exprt path_symex_statet::read(const exprt &src, bool propagate)
   //std::cout << "path_symex_statet::read " << src.pretty() << std::endl;
   #endif
 
-  // This has five phases!
-  // 1. Floating-point expression adjustment (rounding mode)
-  // 2. Rewrite unions into byte operators
-  // 3. Dereferencing, including propagation of pointers.
-  // 4. Rewriting to SSA symbols
-  // 5. Simplifier
-
-  exprt tmp1=src;
-  adjust_float_expressions(tmp1, var_map.ns);
-
-  exprt tmp2=tmp1;
-  rewrite_union(tmp2, var_map.ns);
+  // This has three phases!
+  // 1. Dereferencing, including propagation of pointers.
+  // 2. Rewriting to SSA symbols
+  // 3. Simplifier
 
   // we force propagation for dereferencing
-  exprt tmp3=dereference_rec(tmp2, true);
+  exprt tmp3=dereference_rec(src, true);
 
   exprt tmp4=instantiate_rec(tmp3, propagate);
 

src/symex/symex_parse_options.cpp

@@ -33,6 +33,9 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 
+#include <goto-symex/rewrite_union.h>
+#include <goto-symex/adjust_float_expressions.h>
+
 #include <goto-instrument/cover.h>
 
 #include <langapi/mode.h>
@@ -359,6 +362,8 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     remove_complex(goto_model);
     remove_vector(goto_model);
     remove_virtual_functions(goto_model);
+    rewrite_union(goto_model);
+    adjust_float_expressions(goto_model);
 
     // recalculate numbers, etc.
     goto_model.goto_functions.update();