Make all methods of dfcc_utilst static

This class has no state, there is no need to instantiate it.

Author: tautschnig

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

@@ -185,22 +185,19 @@ 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),
-    instrument(goto_model, message_handler, utils, library),
-    memory_predicates(goto_model, utils, library, instrument, message_handler),
-    spec_functions(goto_model, message_handler, utils, library, instrument),
+    instrument(goto_model, message_handler, library),
+    memory_predicates(goto_model, library, instrument, message_handler),
+    spec_functions(goto_model, message_handler, library, instrument),
     contract_clauses_codegen(
       goto_model,
       message_handler,
-      utils,
       library,
       spec_functions),
     contract_handler(
       goto_model,
       message_handler,
-      utils,
       library,
       instrument,
       memory_predicates,
@@ -209,7 +206,6 @@ dfcct::dfcct(
     swap_and_wrap(
       goto_model,
       message_handler,
-      utils,
       library,
       instrument,
       spec_functions,
@@ -223,15 +219,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");
 
@@ -264,7 +260,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
@@ -449,7 +445,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
@@ -559,7 +555,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

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

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

@@ -29,13 +29,11 @@ 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,
   dfcc_spec_functionst &spec_functions)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
-    utils(utils),
     library(library),
     spec_functions(spec_functions),
     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 dfcc_spec_functionst;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
@@ -45,7 +44,6 @@ class dfcc_contract_clauses_codegent
   dfcc_contract_clauses_codegent(
     goto_modelt &goto_model,
     message_handlert &message_handler,
-    dfcc_utilst &utils,
     dfcc_libraryt &library,
     dfcc_spec_functionst &spec_functions);
 
@@ -83,7 +81,6 @@ class dfcc_contract_clauses_codegent
   goto_modelt &goto_model;
   message_handlert &message_handler;
   messaget log;
-  dfcc_utilst &utils;
   dfcc_libraryt &library;
   dfcc_spec_functionst &spec_functions;
   namespacet ns;

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

@@ -25,13 +25,11 @@ Date: August 2022
 #include "dfcc_contract_clauses_codegen.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)
@@ -46,7 +44,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),
@@ -97,8 +94,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;
 
@@ -146,8 +146,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_spec_functionst;
 class dfcc_contract_clauses_codegent;
 class code_with_contract_typet;
@@ -74,7 +73,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);
@@ -116,7 +114,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

@@ -31,7 +31,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>
@@ -40,7 +39,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,
@@ -49,7 +47,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),
@@ -76,7 +73,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;