Make all methods of dfcc_utilst static

This class has no state, there is no need to instantiate it. Also remove
functions from the interface that are only used by one of the members,
and remove those that are not used at all.

Author: tautschnig

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;