introduce rounding_mode_identifier()

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -18,14 +18,16 @@ Author: Daniel Kroening, [email protected]
 #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, [email protected]
 #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, [email protected]
 
 #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, [email protected]
 
 #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, [email protected]
 #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, [email protected]
 
 #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, [email protected]
 #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);

src/jsil/jsil_internal_additions.cpp

@@ -11,6 +11,8 @@ Author: Michael Tautschnig, [email protected]
 
 #include "jsil_internal_additions.h"
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>
 #include <util/symbol_table.h>
@@ -25,8 +27,8 @@ void jsil_internal_additions(symbol_tablet &dest)
 
   {
     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;

src/linking/remove_internal_symbols.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening
 
 #include "remove_internal_symbols.h"
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/message.h>
@@ -119,7 +121,7 @@ void remove_internal_symbols(
   special.insert(CPROVER_PREFIX "malloc_size");
   special.insert(CPROVER_PREFIX "deallocated");
   special.insert(CPROVER_PREFIX "dead_object");
-  special.insert(CPROVER_PREFIX "rounding_mode");
+  special.insert(rounding_mode_identifier());
   special.insert("__new");
   special.insert("__new_array");
   special.insert("__placement_new");

src/statement-list/statement_list_entry_point.cpp

@@ -11,6 +11,7 @@ Author: Matthias Weiss, [email protected]
 
 #include "statement_list_entry_point.h"
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_functions.h>
 
 #include <linking/static_lifetime_init.h>
@@ -21,9 +22,6 @@ Author: Matthias Weiss, [email protected]
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
-/// Name of the CPROVER-specific variable that specifies the rounding mode.
-#define ROUNDING_MODE_NAME CPROVER_PREFIX "rounding_mode"
-
 /// Postfix for the artificial data block that is created when calling a main
 /// symbol that is a function block.
 #define DB_ENTRY_POINT_POSTFIX "_entry_point"
@@ -146,7 +144,7 @@ static void generate_statement_list_init_function(symbol_tablet &symbol_table)
 static void generate_rounding_mode(symbol_tablet &symbol_table)
 {
   symbolt rounding_mode;
-  rounding_mode.name = ROUNDING_MODE_NAME;
+  rounding_mode.name = rounding_mode_identifier();
   rounding_mode.type = signed_int_type();
   rounding_mode.is_thread_local = true;
   rounding_mode.is_static_lifetime = true;

src/util/ieee_float.h

@@ -19,8 +19,6 @@ Author: Daniel Kroening, [email protected]
 class constant_exprt;
 class floatbv_typet;
 
-const char ID_cprover_rounding_mode_str[] = CPROVER_PREFIX "rounding_mode";
-
 class ieee_float_spect
 {
 public: