Remove goto_functiont::type

Having two function type definitions (one in the symbol table and one in
goto_functiont) is just prone to become inconsistent. Instead, always look at
the symbol table when we do need type information. If all we care about are the
identifiers we can still use goto_functiont::parameter_identifiers.

Author: tautschnig

src/assembler/remove_asm.cpp

@@ -122,14 +122,14 @@ void remove_asmt::gcc_asm_function_call(
     symbol.mode = ID_C;
 
     symbol_table.add(symbol);
-  }
 
-  if(
-    goto_functions.function_map.find(function_identifier) ==
-    goto_functions.function_map.end())
+    goto_functions.function_map.emplace(function_identifier, goto_functiont());
+  }
+  else
   {
-    auto &f = goto_functions.function_map[function_identifier];
-    f.type = fkt_type;
+    DATA_INVARIANT(
+      symbol_table.lookup_ref(function_identifier).type == fkt_type,
+      "function types should match");
   }
 }
 
@@ -171,14 +171,14 @@ void remove_asmt::msc_asm_function_call(
     symbol.mode = ID_C;
 
     symbol_table.add(symbol);
-  }
 
-  if(
-    goto_functions.function_map.find(function_identifier) ==
-    goto_functions.function_map.end())
+    goto_functions.function_map.emplace(function_identifier, goto_functiont());
+  }
+  else
   {
-    auto &f = goto_functions.function_map[function_identifier];
-    f.type = fkt_type;
+    DATA_INVARIANT(
+      symbol_table.lookup_ref(function_identifier).type == fkt_type,
+      "function types should match");
   }
 }
 

src/goto-harness/function_call_harness_generator.cpp

@@ -453,10 +453,6 @@ void function_call_harness_generatort::implt::
 
   symbol_table->insert(harness_function_symbol);
 
-  auto const &generated_harness =
-    symbol_table->lookup_ref(harness_function_name);
-  goto_functions->function_map[harness_function_name].type =
-    to_code_type(generated_harness.type);
   goto_convert(*symbol_table, *goto_functions, *message_handler);
 }
 

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -322,7 +322,6 @@ void memory_snapshot_harness_generatort::
   CHECK_RETURN(function_iterator_pair.second);
 
   goto_functiont &harness_function = function_iterator_pair.first->second;
-  harness_function.type = to_code_type(function.type);
 
   goto_convert(
     goto_model.symbol_table, goto_model.goto_functions, message_handler);

src/goto-harness/recursive_initialization.cpp

@@ -366,8 +366,6 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
     expr_name,
     is_nullable);
 
-  goto_model.goto_functions.function_map[function_symbol.name].type =
-    to_code_type(function_symbol.type);
   return type_constructor_names.at(key);
 }
 

src/goto-instrument/code_contracts.cpp

@@ -749,8 +749,6 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
 
   goto_functiont &wrapper = goto_functions.function_map[original];
   wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
-  if(mangled_fun->second.type.is_not_nil())
-    wrapper.type = mangled_fun->second.type;
   wrapper.body.add(goto_programt::make_end_function(sl));
   add_contract_check(original, mangled, wrapper.body);
   return false;

src/goto-instrument/generate_function_bodies.cpp

@@ -64,7 +64,6 @@ void generate_function_bodiest::generate_parameter_names(
       symbol_table.add(new_param_sym);
     }
   }
-  function.type = to_code_type(function_symbol.type);
   function.set_parameter_identifiers(to_code_type(function_symbol.type));
 }
 
@@ -591,8 +590,6 @@ void generate_function_bodies(
     model.symbol_table.lookup_ref(havoc_function_symbol.name);
 
   // convert to get the function stub to goto-model
-  model.goto_functions.function_map[havoc_function_symbol.name].type =
-    to_code_type(generated_havoc.type);
   goto_convert(model.symbol_table, model.goto_functions, message_handler);
 
   // now generate body as above

src/goto-instrument/replace_calls.cpp

@@ -94,8 +94,6 @@ void replace_callst::operator()(
     auto f_it2 = goto_functions.function_map.find(new_id);
     PRECONDITION(f_it2 != goto_functions.function_map.end());
 
-    PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns));
-
     // check that returns have not been removed
     if(to_code_type(function.type()).return_type().id() != ID_empty)
     {

src/goto-programs/goto_convert_functions.cpp

@@ -155,7 +155,6 @@ void goto_convert_functionst::convert_function(
 
   // store the parameter identifiers in the goto functions
   const code_typet &code_type = to_code_type(symbol.type);
-  f.type = code_type;
   f.set_parameter_identifiers(code_type);
 
   if(
@@ -227,10 +226,7 @@ void goto_convert_functionst::convert_function(
   f.body.update();
 
   if(hide(f.body))
-  {
-    f.make_hidden();
     symbol_table.get_writeable_ref(identifier).set_hidden();
-  }
 
   lifetime = parent_lifetime;
 }

src/goto-programs/goto_function.cpp

@@ -46,27 +46,4 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
   }
 
   body.validate(ns, vm);
-
-  find_symbols_sett typetags;
-  find_type_symbols(type, typetags);
-  const symbolt *symbol;
-  for(const auto &identifier : typetags)
-  {
-    DATA_CHECK(
-      vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
-  }
-
-  // Check that a void function does not contain any RETURN instructions
-  if(to_code_type(type).return_type().id() == ID_empty)
-  {
-    forall_goto_program_instructions(instruction, body)
-    {
-      DATA_CHECK(
-        vm,
-        !instruction->is_return(),
-        "void function should not return a value");
-    }
-  }
-
-  validate_full_type(type, ns, vm);
 }

src/goto-programs/goto_function.h

@@ -22,23 +22,15 @@ Date: May 2018
 
 #include "goto_program.h"
 
-/// A goto function, consisting of function type (see #type), function body (see
-/// #body), and parameter identifiers (see #parameter_identifiers).
+/// A goto function, consisting of function body (see #body) and parameter
+/// identifiers (see #parameter_identifiers).
 class goto_functiont
 {
 public:
   goto_programt body;
 
-  /// The type of the function, indicating the return type and parameter types
-  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
-  code_typet type;
-
   typedef std::vector<irep_idt> parameter_identifierst;
-
   /// The identifiers of the parameters of this function
-  ///
-  /// Note: This is now the preferred way of getting the identifiers of the
-  /// parameters. The identifiers in the type will go away.
   parameter_identifierst parameter_identifiers;
 
   bool body_available() const
@@ -54,46 +46,23 @@ class goto_functiont
       parameter_identifiers.push_back(parameter.get_identifier());
   }
 
-  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
-  bool is_inlined() const
-  {
-    return type.get_bool(ID_C_inlined);
-  }
-
-  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
-  bool is_hidden() const
-  {
-    return type.get_bool(ID_C_hide);
-  }
-
-  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
-  void make_hidden()
-  {
-    type.set(ID_C_hide, true);
-  }
-
-  goto_functiont() : body(), type({}, empty_typet())
-  {
-  }
+  goto_functiont() = default;
 
   void clear()
   {
     body.clear();
-    type.clear();
     parameter_identifiers.clear();
   }
 
   void swap(goto_functiont &other)
   {
     body.swap(other.body);
-    type.swap(other.type);
     parameter_identifiers.swap(other.parameter_identifiers);
   }
 
   void copy_from(const goto_functiont &other)
   {
     body.copy_from(other.body);
-    type = other.type;
     parameter_identifiers = other.parameter_identifiers;
   }
 
@@ -102,15 +71,13 @@ class goto_functiont
 
   goto_functiont(goto_functiont &&other)
     : body(std::move(other.body)),
-      type(std::move(other.type)),
       parameter_identifiers(std::move(other.parameter_identifiers))
   {
   }
 
   goto_functiont &operator=(goto_functiont &&other)
   {
     body = std::move(other.body);
-    type = std::move(other.type);
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }

src/goto-programs/goto_functions.cpp

@@ -109,13 +109,6 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm)
     const code_typet::parameterst &parameters =
       to_code_type(function_symbol.type).parameters();
 
-    DATA_CHECK(
-      vm,
-      goto_function.type == ns.lookup(function_name).type,
-      id2string(function_name) + " type inconsistency\ngoto program type: " +
-        goto_function.type.id_string() +
-        "\nsymbol table type: " + ns.lookup(function_name).type.id_string());
-
     DATA_CHECK(
       vm,
       goto_function.parameter_identifiers.size() == parameters.size(),

src/goto-programs/link_goto_model.cpp

@@ -35,7 +35,6 @@ static void rename_symbols_in_function(
   }
 
   goto_programt &program=function.body;
-  rename_symbol(function.type);
 
   Forall_goto_program_instructions(iit, program)
   {
@@ -99,12 +98,6 @@ static bool link_functions(
         in_dest_symbol_table.body.swap(src_func.body);
         in_dest_symbol_table.parameter_identifiers.swap(
           src_func.parameter_identifiers);
-        in_dest_symbol_table.type=src_func.type;
-        // the linking code will have ensured that types match
-        INVARIANT(
-          base_type_eq(
-            dest_symbol_table.lookup_ref(final_id).type, src_func.type, ns),
-          "linking ensures that types match");
       }
       else if(src_func.body.instructions.empty() ||
               src_ns.lookup(src_it->first).is_weak)
@@ -115,13 +108,6 @@ static bool link_functions(
       {
         // ok, we silently ignore
       }
-      else
-      {
-        // the linking code will have ensured that types match
-        rename_symbol(src_func.type);
-        INVARIANT(base_type_eq(in_dest_symbol_table.type, src_func.type, ns),
-                  "linking ensures that types match");
-      }
     }
   }
 

src/goto-programs/read_bin_goto_object.cpp

@@ -74,10 +74,7 @@ static bool read_bin_goto_object(
     {
       // makes sure there is an empty function for every function symbol
       auto entry = functions.function_map.emplace(sym.name, goto_functiont());
-
-      const code_typet &code_type = to_code_type(sym.type);
-      entry.first->second.type = code_type;
-      entry.first->second.set_parameter_identifiers(code_type);
+      entry.first->second.set_parameter_identifiers(to_code_type(sym.type));
     }
 
     symbol_table.add(sym);
@@ -161,7 +158,6 @@ static bool read_bin_goto_object(
 
     if(hidden)
     {
-      f.make_hidden();
       // can be removed with the next goto-binary version update as the
       // information is guaranteed to be stored in the symbol table
 #if GOTO_BINARY_VERSION > 5

src/goto-programs/remove_complex.cpp

@@ -283,8 +283,6 @@ void remove_complex(symbol_tablet &symbol_table)
 static void remove_complex(
   goto_functionst::goto_functiont &goto_function)
 {
-  remove_complex(goto_function.type);
-
   for(auto &i : goto_function.body.instructions)
     i.transform([](exprt e) -> optionalt<exprt> {
       if(have_to_remove_complex(e))

src/goto-programs/remove_vector.cpp

@@ -217,8 +217,6 @@ static void remove_vector(symbol_tablet &symbol_table)
 /// removes vector data type
 void remove_vector(goto_functionst::goto_functiont &goto_function)
 {
-  remove_vector(goto_function.type);
-
   for(auto &i : goto_function.body.instructions)
     i.transform([](exprt e) -> optionalt<exprt> {
       if(have_to_remove_vector(e))

unit/Makefile

@@ -23,7 +23,6 @@ SRC += analyses/ai/ai.cpp \
        goto-checker/report_util/is_property_less_than.cpp \
        goto-instrument/cover_instrument.cpp \
        goto-instrument/cover/cover_only.cpp \
-       goto-programs/goto_model_function_type_consistency.cpp \
        goto-programs/goto_program_assume.cpp \
        goto-programs/goto_program_dead.cpp \
        goto-programs/goto_program_declaration.cpp \