Store identifiers of parameters in goto_functiont::parameter_identifiers

This is to enable a transition towards #4167.

Author: Daniel Kroening

src/goto-instrument/generate_function_bodies.cpp

@@ -35,9 +35,14 @@ void generate_function_bodiest::generate_parameter_names(
   symbol_tablet &symbol_table,
   const irep_idt &function_name) const
 {
-  const namespacet ns(symbol_table);
+  auto &function_symbol = symbol_table.get_writeable_ref(function_name);
+  auto &parameters = to_code_type(function_symbol.type).parameters();
+
+  PRECONDITION(parameters.size() == function.parameter_identifiers.size());
+
   int param_counter = 0;
-  for(auto &parameter : function.type.parameters())
+  auto it = function.parameter_identifiers.begin();
+  for(auto &parameter : parameters)
   {
     if(parameter.get_identifier().empty())
     {
@@ -53,15 +58,17 @@ void generate_function_bodiest::generate_parameter_names(
       new_param_sym.name = new_param_identifier;
       new_param_sym.type = parameter.type();
       new_param_sym.base_name = param_base_name;
-      auto const &function_symbol = symbol_table.lookup_ref(function_name);
       new_param_sym.mode = function_symbol.mode;
       new_param_sym.module = function_symbol.module;
       new_param_sym.location = function_symbol.location;
       symbol_table.add(new_param_sym);
+
+      *it = new_param_identifier;
     }
+
+    ++it;
   }
-  auto &function_symbol = symbol_table.get_writeable_ref(function_name);
-  function_symbol.type = function.type;
+  function.type = to_code_type(function_symbol.type);
 }
 
 class assume_false_generate_function_bodiest : public generate_function_bodiest

src/goto-programs/goto_convert_functions.cpp

@@ -151,7 +151,13 @@ void goto_convert_functionst::convert_function(
   // make tmp variables local to function
   tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
 
-  f.type=to_code_type(symbol.type);
+  // store the parameter identifiers in the goto functions
+  const code_typet &code_type = to_code_type(symbol.type);
+  f.type = code_type;
+  f.parameter_identifiers.clear();
+  f.parameter_identifiers.reserve(code_type.parameters().size());
+  for(const auto &parameter : code_type.parameters())
+    f.parameter_identifiers.push_back(parameter.get_identifier());
 
   if(symbol.value.is_nil() ||
      symbol.is_compiled()) /* goto_inline may have removed the body */

src/goto-programs/goto_function.h

@@ -29,33 +29,35 @@ class goto_functiont
   goto_programt body;
 
   /// The type of the function, indicating the return type and parameter types
+  /// This is deprecated; get the type from the namespace instead.
   code_typet type;
 
   typedef std::vector<irep_idt> parameter_identifierst;
 
   /// The identifiers of the parameters of this function
   ///
-  /// Note: This variable is currently unused and the vector is thus always
-  /// empty. In the future the code base may be refactored to fill in the
-  /// parameter identifiers here when creating a `goto_functiont`. For now the
-  /// parameter identifiers should be retrieved from the type (`code_typet`).
+  /// 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
   {
     return !body.instructions.empty();
   }
 
+  /// This is deprecated; get the type from the namespace instead.
   bool is_inlined() const
   {
     return type.get_bool(ID_C_inlined);
   }
 
+  /// This is deprecated; get the type from the namespace instead.
   bool is_hidden() const
   {
     return type.get_bool(ID_C_hide);
   }
 
+  /// This is deprecated; modify the type in the namespace instead.
   void make_hidden()
   {
     type.set(ID_C_hide, true);

src/goto-programs/goto_functions.h

@@ -117,6 +117,9 @@ class goto_functionst
     {
       const goto_functiont &goto_function = entry.second;
       const auto &function_name = entry.first;
+      const symbolt &function_symbol = ns.lookup(function_name);
+      const code_typet::parameterst &parameters =
+        to_code_type(function_symbol.type).parameters();
 
       DATA_CHECK(
         vm,
@@ -125,6 +128,26 @@ class goto_functionst
           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(),
+        id2string(function_name) + " parameter count inconsistency\n" +
+          "goto program: " +
+          std::to_string(goto_function.parameter_identifiers.size()) +
+          "\nsymbol table: " + std::to_string(parameters.size()));
+
+      auto it = goto_function.parameter_identifiers.begin();
+      for(const auto &parameter : parameters)
+      {
+        DATA_CHECK(
+          vm,
+          it->empty() || ns.lookup(*it).type == parameter.type(),
+          id2string(function_name) + " parameter type inconsistency\n" +
+            "goto program: " + ns.lookup(*it).type.id_string() +
+            "\nsymbol table: " + parameter.type().id_string());
+        ++it;
+      }
+
       goto_function.validate(ns, vm);
     }
   }

src/goto-programs/link_goto_model.cpp

@@ -27,6 +27,13 @@ static void rename_symbols_in_function(
   irep_idt &new_function_name,
   const rename_symbolt &rename_symbol)
 {
+  for(auto &identifier : function.parameter_identifiers)
+  {
+    auto entry = rename_symbol.expr_map.find(identifier);
+    if(entry != rename_symbol.expr_map.end())
+      identifier = entry->second;
+  }
+
   goto_programt &program=function.body;
   rename_symbol(function.type);
 

src/goto-programs/read_bin_goto_object.cpp

@@ -72,10 +72,16 @@ static bool read_bin_goto_object(
 
     if(!sym.is_type && sym.type.id()==ID_code)
     {
-      // makes sure there is an empty function
-      // for every function symbol and fixes
-      // the function types.
-      functions.function_map[sym.name].type=to_code_type(sym.type);
+      // 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.parameter_identifiers.reserve(
+        code_type.parameters().size());
+      for(const auto &parameter : code_type.parameters())
+        entry.first->second.parameter_identifiers.push_back(
+          parameter.get_identifier());
     }
 
     symbol_table.add(sym);

src/goto-programs/string_abstraction.cpp

@@ -166,31 +166,30 @@ void string_abstractiont::add_str_arguments(
 {
   symbolt &fct_symbol=*symbol_table.get_writeable(name);
 
-  code_typet::parameterst &parameters=
-    to_code_type(fct.type).parameters();
   code_typet::parameterst str_args;
 
-  for(code_typet::parameterst::iterator
-      it=parameters.begin();
-      it!=parameters.end();
-      ++it)
+  for(const auto &identifier : fct.parameter_identifiers)
   {
-    const typet &abstract_type=build_abstraction_type(it->type());
-    if(abstract_type.is_nil())
-      continue;
-
-    const irep_idt &identifier=it->get_identifier();
     if(identifier=="")
       continue; // ignore
 
-    add_argument(str_args, fct_symbol, abstract_type,
-        id2string(it->get_base_name())+arg_suffix,
-        id2string(identifier)+arg_suffix);
+    const symbolt &param_symbol = ns.lookup(identifier);
+    const typet &abstract_type = build_abstraction_type(param_symbol.type);
+    if(abstract_type.is_nil())
+      continue;
+
+    add_argument(
+      str_args,
+      fct_symbol,
+      abstract_type,
+      id2string(param_symbol.base_name) + arg_suffix,
+      id2string(identifier) + arg_suffix);
 
     current_args.insert(identifier);
   }
 
-  parameters.insert(parameters.end(), str_args.begin(), str_args.end());
+  for(const auto &new_param : str_args)
+    fct.parameter_identifiers.push_back(new_param.get_identifier());
   code_typet::parameterst &symb_parameters=
     to_code_type(fct_symbol.type).parameters();
   symb_parameters.insert(