Make all methods of dfcc_utilst static

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -188,23 +188,20 @@ dfcct::dfcct(
     to_exclude_from_nondet_static(to_exclude_from_nondet_static),
     message_handler(message_handler),
     log(message_handler),
-    utils(goto_model, message_handler),
-    library(goto_model, utils, message_handler),
+    library(goto_model, message_handler),
     ns(goto_model.symbol_table),
-    spec_functions(goto_model, message_handler, utils, library),
-    contract_clauses_codegen(goto_model, message_handler, utils, library),
+    spec_functions(goto_model, message_handler, library),
+    contract_clauses_codegen(goto_model, message_handler, library),
     instrument(
       goto_model,
       message_handler,
-      utils,
       library,
       spec_functions,
       contract_clauses_codegen),
-    memory_predicates(goto_model, utils, library, instrument, message_handler),
+    memory_predicates(goto_model, library, instrument, message_handler),
     contract_handler(
       goto_model,
       message_handler,
-      utils,
       library,
       instrument,
       memory_predicates,
@@ -213,7 +210,6 @@ dfcct::dfcct(
     swap_and_wrap(
       goto_model,
       message_handler,
-      utils,
       library,
       instrument,
       spec_functions,
@@ -227,15 +223,15 @@ void dfcct::check_transform_goto_model_preconditions()
 {
   // check that harness function exists
   PRECONDITION_WITH_DIAGNOSTICS(
-    utils.function_symbol_with_body_exists(harness_id),
+    dfcc_utilst::function_symbol_with_body_exists(goto_model, harness_id),
     "Harness function '" + id2string(harness_id) +
       "' either not found or has no body");
 
   if(to_check.has_value())
   {
     auto pair = to_check.value();
     PRECONDITION_WITH_DIAGNOSTICS(
-      utils.function_symbol_with_body_exists(pair.first),
+      dfcc_utilst::function_symbol_with_body_exists(goto_model, pair.first),
       "Function to check '" + id2string(pair.first) +
         "' either not found or has no body");
 
@@ -268,7 +264,7 @@ void dfcct::check_transform_goto_model_preconditions()
     // for functions to replace with contracts we don't require the replaced
     // function to have a body because only the contract is actually used
     PRECONDITION_WITH_DIAGNOSTICS(
-      utils.function_symbol_exists(pair.first),
+      dfcc_utilst::function_symbol_exists(goto_model, pair.first),
       "Function to replace '" + id2string(pair.first) + "' not found");
 
     // triggers signature compatibility checking
@@ -454,7 +450,7 @@ void dfcct::wrap_discovered_function_pointer_contracts()
       {
         // we need to swap it with itself
         PRECONDITION_WITH_DIAGNOSTICS(
-          utils.function_symbol_exists(str),
+          dfcc_utilst::function_symbol_exists(goto_model, str),
           "Function pointer contract '" + str + "' not found.");
 
         // triggers signature compatibility checking
@@ -581,7 +577,7 @@ void dfcct::reinitialize_model()
     goto_model.symbol_table.symbols.find(goto_functionst::entry_point()));
   // regenerate the CPROVER start function
   generate_ansi_c_start_function(
-    utils.get_function_symbol(harness_id),
+    dfcc_utilst::get_function_symbol(goto_model.symbol_table, harness_id),
     goto_model.symbol_table,
     message_handler,
     c_object_factory_parameterst(options));

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -41,7 +41,6 @@ Author: Remi Delmas, [email protected]
 #include "dfcc_loop_contract_mode.h"
 #include "dfcc_spec_functions.h"
 #include "dfcc_swap_and_wrap.h"
-#include "dfcc_utils.h"
 
 #include <map>
 #include <set>
@@ -217,7 +216,6 @@ class dfcct
 
   // Singletons that hold the global state of the program transformation
   // (caches etc.)
-  dfcc_utilst utils;
   dfcc_libraryt library;
   namespacet ns;
   dfcc_spec_functionst spec_functions;

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -436,9 +436,8 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   dirtyt &dirty,
   local_may_aliast &local_may_alias,
   message_handlert &message_handler,
-  dfcc_utilst &utils,
   dfcc_libraryt &library,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   std::unordered_set<irep_idt> loop_locals =
     gen_loop_locals_set(loop_nesting_graph, loop_id);
@@ -472,7 +471,8 @@ static dfcc_loop_infot gen_dfcc_loop_info(
 
   auto &loop = loop_nesting_graph[loop_id];
   const auto cbmc_loop_number = loop.latch->loop_number;
-  const auto &language_mode = utils.get_function_symbol(function_id).mode;
+  const auto &language_mode =
+    dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
 
   // Generate "write set" variable
   const auto &write_set_var =
@@ -515,9 +515,8 @@ dfcc_cfg_infot::dfcc_cfg_infot(
   goto_functiont &goto_function,
   const exprt &top_level_write_set,
   const dfcc_loop_contract_modet loop_contract_mode,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  dfcc_utilst &utils,
   dfcc_libraryt &library)
   : function_id(function_id),
     goto_function(goto_function),
@@ -581,7 +580,6 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          dirty,
          local_may_alias,
          message_handler,
-         utils,
          library,
          symbol_table)});
 

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h

@@ -29,7 +29,6 @@ Date: March 2023
 #include <set>
 #include <unordered_set>
 
-class dfcc_utilst;
 class dfcc_libraryt;
 class goto_functiont;
 class message_handlert;
@@ -240,9 +239,8 @@ class dfcc_cfg_infot
     goto_functiont &goto_function,
     const exprt &top_level_write_set,
     const dfcc_loop_contract_modet loop_contract_mode,
-    symbol_tablet &symbol_table,
+    symbol_table_baset &symbol_table,
     message_handlert &message_handler,
-    dfcc_utilst &utils,
     dfcc_libraryt &library);
 
   void output(std::ostream &out) const;

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

@@ -30,12 +30,10 @@ Date: February 2023
 dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  dfcc_utilst &utils,
   dfcc_libraryt &library)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
-    utils(utils),
     library(library),
     ns(goto_model.symbol_table)
 {
@@ -233,7 +231,9 @@ void dfcc_contract_clauses_codegent::encode_freeable_target(
   {
     // A plain `target` becomes `CALL __CPROVER_freeable(target);`
     code_function_callt code_function_call(
-      utils.get_function_symbol(CPROVER_PREFIX "freeable").symbol_expr());
+      dfcc_utilst::get_function_symbol(
+        goto_model.symbol_table, CPROVER_PREFIX "freeable")
+        .symbol_expr());
     auto &arguments = code_function_call.arguments();
     arguments.emplace_back(target);
 
@@ -258,12 +258,14 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
   std::set<irep_idt> recursive_call;
   std::set<irep_idt> not_enough_arguments;
 
-  utils.inline_program(
+  dfcc_utilst::inline_program(
+    goto_model,
     goto_program,
     no_body,
     recursive_call,
     missing_function,
-    not_enough_arguments);
+    not_enough_arguments,
+    message_handler);
 
   // check that the only no body / missing functions are the cprover builtins
   for(const auto &id : no_body)

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h

@@ -28,7 +28,6 @@ Date: February 2023
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
-class dfcc_utilst;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
 
@@ -39,12 +38,10 @@ class dfcc_contract_clauses_codegent
 public:
   /// \param goto_model GOTO model being transformed
   /// \param message_handler Used debug/warning/error messages
-  /// \param utils Utility class for dynamic frames
   /// \param library The contracts instrumentation library
   dfcc_contract_clauses_codegent(
     goto_modelt &goto_model,
     message_handlert &message_handler,
-    dfcc_utilst &utils,
     dfcc_libraryt &library);
 
   /// \brief Generates instructions encoding the \p assigns_clause targets and
@@ -81,7 +78,6 @@ class dfcc_contract_clauses_codegent
   goto_modelt &goto_model;
   message_handlert &message_handler;
   messaget log;
-  dfcc_utilst &utils;
   dfcc_libraryt &library;
   namespacet ns;
 

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp

@@ -26,13 +26,11 @@ Date: August 2022
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_spec_functions.h"
-#include "dfcc_utils.h"
 
 dfcc_contract_functionst::dfcc_contract_functionst(
   const symbolt &pure_contract_symbol,
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  dfcc_utilst &utils,
   dfcc_libraryt &library,
   dfcc_spec_functionst &spec_functions,
   dfcc_contract_clauses_codegent &contract_clauses_codegen,
@@ -48,7 +46,6 @@ dfcc_contract_functionst::dfcc_contract_functionst(
     goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
-    utils(utils),
     library(library),
     spec_functions(spec_functions),
     contract_clauses_codegen(contract_clauses_codegen),
@@ -122,8 +119,11 @@ const std::size_t dfcc_contract_functionst::get_nof_frees_targets() const
 
 void dfcc_contract_functionst::gen_spec_assigns_function()
 {
-  const auto &spec_function_symbol = utils.clone_and_rename_function(
-    pure_contract_symbol.name, spec_assigns_function_id, empty_typet());
+  const auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
+    goto_model,
+    pure_contract_symbol.name,
+    spec_assigns_function_id,
+    empty_typet());
 
   const auto &spec_function_id = spec_function_symbol.name;
 
@@ -171,8 +171,11 @@ void dfcc_contract_functionst::gen_spec_frees_function()
   const auto &code_with_contract =
     to_code_with_contract_type(pure_contract_symbol.type);
 
-  auto &spec_function_symbol = utils.clone_and_rename_function(
-    pure_contract_symbol.name, spec_frees_function_id, empty_typet());
+  auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
+    goto_model,
+    pure_contract_symbol.name,
+    spec_frees_function_id,
+    empty_typet());
 
   const auto &spec_function_id = spec_function_symbol.name;
 

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h

@@ -28,7 +28,6 @@ Date: August 2022
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
-class dfcc_utilst;
 class dfcc_instrumentt;
 class dfcc_spec_functionst;
 class dfcc_contract_clauses_codegent;
@@ -68,7 +67,6 @@ class dfcc_contract_functionst
   /// \param pure_contract_symbol the contract to generate code from
   /// \param goto_model goto model being transformed
   /// \param message_handler used debug/warning/error messages
-  /// \param utils utility class for dynamic frames
   /// \param library the contracts instrumentation library
   /// \param spec_functions provides translation methods for assignable set
   /// \param contract_clauses_codegen provides GOTO code generation methods
@@ -78,7 +76,6 @@ class dfcc_contract_functionst
     const symbolt &pure_contract_symbol,
     goto_modelt &goto_model,
     message_handlert &message_handler,
-    dfcc_utilst &utils,
     dfcc_libraryt &library,
     dfcc_spec_functionst &spec_functions,
     dfcc_contract_clauses_codegent &contract_clauses_codegen,
@@ -126,7 +123,6 @@ class dfcc_contract_functionst
   goto_modelt &goto_model;
   message_handlert &message_handler;
   messaget log;
-  dfcc_utilst &utils;
   dfcc_libraryt &library;
   dfcc_spec_functionst &spec_functions;
   dfcc_contract_clauses_codegent &contract_clauses_codegen;

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp

@@ -30,7 +30,6 @@ Date: August 2022
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_spec_functions.h"
-#include "dfcc_utils.h"
 #include "dfcc_wrapper_program.h"
 
 std::map<irep_idt, dfcc_contract_functionst>
@@ -39,7 +38,6 @@ std::map<irep_idt, dfcc_contract_functionst>
 dfcc_contract_handlert::dfcc_contract_handlert(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  dfcc_utilst &utils,
   dfcc_libraryt &library,
   dfcc_instrumentt &instrument,
   dfcc_lift_memory_predicatest &memory_predicates,
@@ -48,7 +46,6 @@ dfcc_contract_handlert::dfcc_contract_handlert(
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
-    utils(utils),
     library(library),
     instrument(instrument),
     memory_predicates(memory_predicates),
@@ -75,7 +72,6 @@ dfcc_contract_handlert::get_contract_functions(const irep_idt &contract_id)
          get_pure_contract_symbol(contract_id),
          goto_model,
          message_handler,
-         utils,
          library,
          spec_functions,
          contract_clauses_codegen,
@@ -100,13 +96,12 @@ void dfcc_contract_handlert::add_contract_instructions(
 {
   dfcc_wrapper_programt(
     contract_mode,
-    utils.get_function_symbol(wrapper_id),
-    utils.get_function_symbol(wrapped_id),
+    dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id),
+    dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapped_id),
     get_contract_functions(contract_id),
     wrapper_write_set_symbol,
     goto_model,
     message_handler,
-    utils,
     library,
     instrument,
     memory_predicates)
@@ -124,7 +119,8 @@ const symbolt &dfcc_contract_handlert::get_pure_contract_symbol(
     if(function_id_opt.has_value())
     {
       auto function_id = function_id_opt.value();
-      const auto &function_symbol = utils.get_function_symbol(function_id);
+      const auto &function_symbol =
+        dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
       check_signature_compat(
         function_id,
         to_code_type(function_symbol.type),
@@ -145,7 +141,8 @@ const symbolt &dfcc_contract_handlert::get_pure_contract_symbol(
         "to derive a default contract");
 
     auto function_id = function_id_opt.value();
-    const auto &function_symbol = utils.get_function_symbol(function_id);
+    const auto &function_symbol =
+      dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
 
     log.warning() << "Contract '" << contract_id
                   << "' not found, deriving empty pure contract '"

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h

@@ -27,7 +27,6 @@ Date: August 2022
 class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
-class dfcc_utilst;
 class dfcc_instrumentt;
 class dfcc_lift_memory_predicatest;
 class dfcc_spec_functionst;
@@ -69,7 +68,6 @@ class dfcc_contract_handlert
   dfcc_contract_handlert(
     goto_modelt &goto_model,
     message_handlert &message_handler,
-    dfcc_utilst &utils,
     dfcc_libraryt &library,
     dfcc_instrumentt &instrument,
     dfcc_lift_memory_predicatest &memory_predicates,
@@ -119,7 +117,6 @@ class dfcc_contract_handlert
   goto_modelt &goto_model;
   message_handlert &message_handler;
   messaget log;
-  dfcc_utilst &utils;
   dfcc_libraryt &library;
   dfcc_instrumentt &instrument;
   dfcc_lift_memory_predicatest &memory_predicates;