From 96dfda9c56b71f54068b81d65e87f9e85d9448cc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Dec 2021 17:33:10 +0000 Subject: [PATCH] Move rounding_mode_identifier() to configt This removes a goto-programs dependency from linking/, which is all about symbol tables, not goto programs. --- .../java_bytecode/java_bytecode_internal_additions.cpp | 9 ++++----- jbmc/src/java_bytecode/java_entry_point.cpp | 3 +-- src/analyses/constant_propagator.cpp | 7 +++---- src/ansi-c/ansi_c_internal_additions.cpp | 4 +--- src/cpp/cpp_internal_additions.cpp | 4 +--- src/goto-instrument/full_slicer.cpp | 4 ++-- src/goto-programs/adjust_float_expressions.cpp | 9 ++------- src/goto-programs/adjust_float_expressions.h | 4 ---- src/linking/module_dependencies.txt | 1 - src/linking/remove_internal_symbols.cpp | 4 +--- src/statement-list/statement_list_entry_point.cpp | 4 ++-- src/util/config.cpp | 5 +++++ src/util/config.h | 4 ++++ 13 files changed, 26 insertions(+), 36 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp index 84f9a4c7da9..a1f5c37964b 100644 --- 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 +#include #include #include #include -#include +#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 index fa074554c8e..b7d934ef0f2 100644 --- 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 #include -#include #include #include @@ -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 index 80b9c778a45..2a35f6186fe 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -11,8 +11,6 @@ Author: Peter Schrammel #include "constant_propagator.h" -#include - #ifdef DEBUG #include #include @@ -20,6 +18,7 @@ Author: Peter Schrammel #include #include +#include #include #include #include @@ -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 index 0f0e11c759a..e7175e839d6 100644 --- 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 #include -#include - #include #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 index d8c862206a2..06f4da91141 100644 --- 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 -#include - 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 index f8b8c8a6414..f47476ff5f2 100644 --- 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 #include -#include #include 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 index eafea9ed5a3..e1dd5769bbe 100644 --- 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 -#include +#include #include #include #include @@ -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 index 80401edcd0b..43d9cb6c607 100644 --- 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 index 713bdb74bf3..4a2e5bb66d8 100644 --- 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 index ce8401a0699..c5700071425 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -19,8 +19,6 @@ Author: Daniel Kroening #include #include -#include - #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 index 7bb7b1b1cef..a67faa33131 100644 --- 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 #include -#include #include #include @@ -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 index da70a3b9888..6dee28a18f7 100644 --- 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 index e1cdc3eb99c..b9ce87e7593 100644 --- 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); };