Move rounding_mode_identifier() to configt

tautschnig · tautschnig · commit 96dfda9c56b7 · 2025-07-29T18:32:05.000Z
This removes a goto-programs dependency from linking/, which is all
about symbol tables, not goto programs.
diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -9,22 +9,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #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/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{rounding_mode_identifier(), signed_int_type(), ID_C};
+    symbolt symbol{config.rounding_mode_identifier(), signed_int_type(), ID_C};
     symbol.base_name = symbol.name;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/message.h>
 #include <util/suffix.h>
 
-#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_functions.h>
 
@@ -239,7 +238,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())});
 
diff --git a/src/analyses/constant_propagator.cpp b/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>
@@ -663,7 +662,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(), ns))
+  if(!known_values.is_constant(config.rounding_mode_identifier(), ns))
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
 
   return replace_constants_and_simplify(known_values, expr, ns);
@@ -693,7 +692,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))
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 
-#include <goto-programs/adjust_float_expressions.h>
-
 #include <linking/static_lifetime_init.h>
 
 #include "ansi_c_parser.h"
@@ -179,7 +177,7 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
 
     // 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
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
@@ -17,8 +17,6 @@ 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;
@@ -86,7 +84,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
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
@@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "full_slicer.h"
 #include "full_slicer_class.h"
 
+#include <util/config.h>
 #include <util/find_symbols.h>
 
-#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/remove_skip.h>
 
 void full_slicert::add_dependencies(
@@ -248,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()(
diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, 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.
@@ -195,7 +190,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();
 
diff --git a/src/goto-programs/adjust_float_expressions.h b/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
diff --git a/src/linking/module_dependencies.txt b/src/linking/module_dependencies.txt
@@ -1,5 +1,4 @@
 ansi-c
-goto-programs
 langapi # should go away
 linking
 util
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
@@ -19,8 +19,6 @@ Author: Daniel Kroening
 #include <util/std_types.h>
 #include <util/symbol_table_base.h>
 
-#include <goto-programs/adjust_float_expressions.h>
-
 #include "static_lifetime_init.h"
 
 static void get_symbols(
@@ -153,7 +151,7 @@ void remove_internal_symbols(
   special.insert(CPROVER_PREFIX "freeable");
   special.insert(CPROVER_PREFIX "is_freeable");
   special.insert(CPROVER_PREFIX "was_freed");
-  special.insert(rounding_mode_identifier());
+  special.insert(config.rounding_mode_identifier());
   special.insert("__new");
   special.insert("__new_array");
   special.insert("__placement_new");
diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp
@@ -18,7 +18,6 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 #include <util/std_code.h>
 #include <util/symbol_table_base.h>
 
-#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_functions.h>
 
 #include <linking/static_lifetime_init.h>
@@ -142,7 +141,8 @@ generate_statement_list_init_function(symbol_table_baset &symbol_table)
 /// \param [out] symbol_table: Symbol table that should contain the symbol.
 static void generate_rounding_mode(symbol_table_baset &symbol_table)
 {
-  symbolt rounding_mode{rounding_mode_identifier(), signed_int_type(), ID_C};
+  symbolt rounding_mode{
+    config.rounding_mode_identifier(), signed_int_type(), ID_C};
   rounding_mode.is_thread_local = true;
   rounding_mode.is_static_lifetime = true;
   const constant_exprt rounding_val{
diff --git a/src/util/config.cpp b/src/util/config.cpp
@@ -1612,3 +1612,8 @@ mp_integer configt::max_malloc_size() const
   const auto bits_for_positive_offset = offset_bits - 1;
   return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
 }
+
+irep_idt configt::rounding_mode_identifier() const
+{
+  return CPROVER_PREFIX "rounding_mode";
+}
diff --git a/src/util/config.h b/src/util/config.h
@@ -402,6 +402,10 @@ class configt
   static irep_idt this_architecture();
   static irep_idt this_operating_system();
 
+  /// Return the identifier of the program symbol used to
+  /// store the current rounding mode.
+  irep_idt rounding_mode_identifier() const;
+
 private:
   void set_classpath(const std::string &cp);
 };

-Original file line number
+Diff line change
@@ @@ -1,5 +1,4 @@ @@
 ansi-c
 -goto-programs
 langapi # should go away
 linking
 util