Merge pull request #6289 from diffblue/rounding_mode_identifier

introduce rounding_mode_identifier()

Author: kroening

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -18,14 +18,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/symbol_table_base.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 void java_internal_additions(symbol_table_baset &dest)
 {
   // add __CPROVER_rounding_mode
 
   {
     symbolt symbol;
-    symbol.base_name = CPROVER_PREFIX "rounding_mode";
-    symbol.name=CPROVER_PREFIX "rounding_mode";
+    symbol.name = rounding_mode_identifier();
+    symbol.base_name = symbol.name;
     symbol.type=signed_int_type();
     symbol.mode=ID_C;
     symbol.is_lvalue=true;

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/nondet.h>
 #include <util/suffix.h>
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
@@ -120,7 +121,7 @@ void java_static_lifetime_init(
   code_blockt code_block;
 
   const symbol_exprt rounding_mode =
-    symbol_table.lookup_ref(CPROVER_PREFIX "rounding_mode").symbol_expr();
+    symbol_table.lookup_ref(rounding_mode_identifier()).symbol_expr();
   code_block.add(
     code_assignt{rounding_mode, from_integer(0, rounding_mode.type())});
 

src/analyses/constant_propagator.cpp

@@ -11,6 +11,8 @@ Author: Peter Schrammel
 
 #include "constant_propagator.h"
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #ifdef DEBUG
 #include <iostream>
 #include <util/format_expr.h>
@@ -655,7 +657,7 @@ bool constant_propagator_domaint::partial_evaluate(
   // if the current rounding mode is top we can
   // still get a non-top result by trying all rounding
   // modes and checking if the results are all the same
-  if(!known_values.is_constant(ID_cprover_rounding_mode_str))
+  if(!known_values.is_constant(rounding_mode_identifier()))
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
 
   return replace_constants_and_simplify(known_values, expr, ns);
@@ -685,7 +687,7 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(
   {
     valuest tmp_values = known_values;
     tmp_values.set_to(
-      symbol_exprt(ID_cprover_rounding_mode_str, integer_typet()),
+      symbol_exprt(rounding_mode_identifier(), integer_typet()),
       from_integer(rounding_modes[i], integer_typet()));
     exprt result = expr;
     if(replace_constants_and_simplify(tmp_values, result, ns))

src/ansi-c/ansi_c_internal_additions.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <linking/static_lifetime_init.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 const char gcc_builtin_headers_types[]=
 "# 1 \"gcc_builtin_headers_types.h\"\n"
 #include "gcc_builtin_headers_types.inc"
@@ -205,7 +207,8 @@ void ansi_c_internal_additions(std::string &code)
       CPROVER_PREFIX "constant_infinity_uint];\n"
 
     // float stuff
-    "int " CPROVER_PREFIX "thread_local " CPROVER_PREFIX "rounding_mode="+
+    "int " CPROVER_PREFIX "thread_local " +
+      id2string(rounding_mode_identifier()) + '='+
       std::to_string(config.ansi_c.rounding_mode)+";\n"
 
     // pipes, write, read, close

src/cpp/cpp_internal_additions.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <linking/static_lifetime_init.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 std::string c2cpp(const std::string &s)
 {
   std::string result;
@@ -108,7 +110,7 @@ void cpp_internal_additions(std::ostream &out)
 
   // float
   // TODO: should be thread_local
-  out << "int " CPROVER_PREFIX "rounding_mode = "
+  out << "int " << rounding_mode_identifier() << " = "
       << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
 
   // pipes, write, read, close

src/cpp/module_dependencies.txt

@@ -1,5 +1,6 @@
 ansi-c
 cpp
+goto-programs
 langapi # should go away
 linking
 util

src/goto-instrument/full_slicer.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/find_symbols.h>
 #include <util/cprover_prefix.h>
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/remove_skip.h>
 
 void full_slicert::add_dependencies(
@@ -248,7 +249,7 @@ static bool implicit(goto_programt::const_targett target)
 
   const symbol_exprt &s=to_symbol_expr(a.lhs());
 
-  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
+  return s.get_identifier() == rounding_mode_identifier();
 }
 
 void full_slicert::operator()(

src/goto-programs/adjust_float_expressions.cpp

@@ -21,6 +21,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_model.h"
 
+irep_idt rounding_mode_identifier()
+{
+  return CPROVER_PREFIX "rounding_mode";
+}
+
 /// Iterate over an expression and check it or any of its subexpressions are
 /// floating point operations that haven't been adjusted with a rounding mode
 /// yet.
@@ -186,7 +191,7 @@ void adjust_float_expressions(exprt &expr, const namespacet &ns)
     return;
 
   symbol_exprt rounding_mode =
-    ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
+    ns.lookup(rounding_mode_identifier()).symbol_expr();
 
   rounding_mode.add_source_location() = expr.source_location();
 

src/goto-programs/adjust_float_expressions.h

@@ -56,4 +56,8 @@ void adjust_float_expressions(
 /// \see adjust_float_expressions(goto_functionst &, const namespacet &)
 void adjust_float_expressions(goto_modelt &goto_model);
 
+/// Return the identifier of the program symbol used to
+/// store the current rounding mode.
+irep_idt rounding_mode_identifier();
+
 #endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H

src/jsil/jsil_entry_point.cpp

@@ -16,6 +16,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 #include <util/message.h>
 #include <util/range.h>
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_functions.h>
 
 #include <linking/static_lifetime_init.h>
@@ -33,8 +34,8 @@ static void create_initialize(symbol_tablet &symbol_table)
 
   namespacet ns(symbol_table);
 
-  symbol_exprt rounding_mode=
-    ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
+  symbol_exprt rounding_mode =
+    ns.lookup(rounding_mode_identifier()).symbol_expr();
 
   code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
   init_code.add(a);