Move rounding_mode_identifier() to configt

This removes a goto-programs dependency from linking/, which is all
about symbol tables, not goto programs.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -9,24 +9,23 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_internal_additions.h"
 
 // For INFLIGHT_EXCEPTION_VARIABLE_NAME
-#include "java_types.h"
-#include "remove_exceptions.h"
-
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
 #include <util/std_types.h>
 #include <util/symbol_table_base.h>
 
-#include <goto-programs/adjust_float_expressions.h>
+#include "java_types.h"
+#include "remove_exceptions.h"
 
 void java_internal_additions(symbol_table_baset &dest)
 {
   // add __CPROVER_rounding_mode
 
   {
     symbolt symbol;
-    symbol.name = rounding_mode_identifier();
+    symbol.name = config.rounding_mode_identifier();
     symbol.base_name = symbol.name;
     symbol.type=signed_int_type();
     symbol.mode=ID_C;

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/journalling_symbol_table.h>
 #include <util/suffix.h>
 
-#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
@@ -240,7 +239,7 @@ void java_static_lifetime_init(
   code_blockt code_block;
 
   const symbol_exprt rounding_mode =
-    symbol_table.lookup_ref(rounding_mode_identifier()).symbol_expr();
+    symbol_table.lookup_ref(config.rounding_mode_identifier()).symbol_expr();
   code_block.add(code_frontend_assignt{rounding_mode,
                                        from_integer(0, rounding_mode.type())});
 

src/analyses/constant_propagator.cpp

@@ -11,15 +11,14 @@ Author: Peter Schrammel
 
 #include "constant_propagator.h"
 
-#include <goto-programs/adjust_float_expressions.h>
-
 #ifdef DEBUG
 #include <iostream>
 #include <util/format_expr.h>
 #endif
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/ieee_float.h>
@@ -658,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(rounding_mode_identifier()))
+  if(!known_values.is_constant(config.rounding_mode_identifier()))
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
 
   return replace_constants_and_simplify(known_values, expr, ns);
@@ -688,7 +687,7 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(
   {
     valuest tmp_values = known_values;
     tmp_values.set_to(
-      symbol_exprt(rounding_mode_identifier(), integer_typet()),
+      symbol_exprt(config.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,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/static_lifetime_init.h>
 
-#include <goto-programs/adjust_float_expressions.h>
-
 const char gcc_builtin_headers_types[] =
   "#line 1 \"gcc_builtin_headers_types.h\"\n"
 #include "gcc_builtin_headers_types.inc"
@@ -196,7 +194,7 @@ void ansi_c_internal_additions(std::string &code)
 
     // float stuff
     "int " CPROVER_PREFIX "thread_local " +
-      id2string(rounding_mode_identifier()) + '='+
+      id2string(config.rounding_mode_identifier()) + '='+
       std::to_string(config.ansi_c.rounding_mode)+";\n"
 
     // pipes, write, read, close

src/cpp/cpp_internal_additions.cpp

@@ -17,8 +17,6 @@ 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;
@@ -109,7 +107,7 @@ void cpp_internal_additions(std::ostream &out)
 
   // float
   // TODO: should be thread_local
-  out << "int " << rounding_mode_identifier() << " = "
+  out << "int " << config.rounding_mode_identifier() << " = "
       << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
 
   // pipes, write, read, close

src/goto-instrument/full_slicer.cpp

@@ -12,10 +12,9 @@ Author: Daniel Kroening, [email protected]
 #include "full_slicer.h"
 #include "full_slicer_class.h"
 
+#include <util/config.h>
 #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(
@@ -249,7 +248,7 @@ static bool implicit(goto_programt::const_targett target)
 
   const symbol_exprt &s = to_symbol_expr(a_lhs);
 
-  return s.get_identifier() == rounding_mode_identifier();
+  return s.get_identifier() == config.rounding_mode_identifier();
 }
 
 void full_slicert::operator()(

src/goto-programs/adjust_float_expressions.cpp

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "adjust_float_expressions.h"
 
 #include <util/arith_tools.h>
-#include <util/cprover_prefix.h>
+#include <util/config.h>
 #include <util/expr_util.h>
 #include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
@@ -21,11 +21,6 @@ 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.
@@ -193,7 +188,7 @@ void adjust_float_expressions(exprt &expr, const namespacet &ns)
     return;
 
   symbol_exprt rounding_mode =
-    ns.lookup(rounding_mode_identifier()).symbol_expr();
+    ns.lookup(config.rounding_mode_identifier()).symbol_expr();
 
   rounding_mode.add_source_location() = expr.source_location();
 

src/goto-programs/adjust_float_expressions.h

@@ -56,8 +56,4 @@ 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

@@ -18,7 +18,6 @@ Author: Michael Tautschnig, [email protected]
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
-#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_functions.h>
 
 #include <linking/static_lifetime_init.h>
@@ -37,7 +36,7 @@ static void create_initialize(symbol_tablet &symbol_table)
   namespacet ns(symbol_table);
 
   symbol_exprt rounding_mode =
-    ns.lookup(rounding_mode_identifier()).symbol_expr();
+    ns.lookup(config.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,14 +11,11 @@ Author: Michael Tautschnig, [email protected]
 
 #include "jsil_internal_additions.h"
 
-#include <goto-programs/adjust_float_expressions.h>
-
+#include <util/c_types.h>
+#include <util/config.h>
 #include <util/std_types.h>
-#include <util/cprover_prefix.h>
 #include <util/symbol_table.h>
 
-#include <util/c_types.h>
-
 #include "jsil_types.h"
 
 void jsil_internal_additions(symbol_tablet &dest)
@@ -27,7 +24,7 @@ void jsil_internal_additions(symbol_tablet &dest)
 
   {
     symbolt symbol;
-    symbol.name = rounding_mode_identifier();
+    symbol.name = config.rounding_mode_identifier();
     symbol.base_name = symbol.name;
     symbol.type=signed_int_type();
     symbol.mode=ID_C;