Use goto_functiont::parameter_identifiers and 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

@@ -253,8 +253,6 @@ void function_call_harness_generatort::implt::
 
   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);
   auto &body = goto_functions->function_map[harness_function_name].body;
   goto_convert(
     static_cast<const codet &>(generated_harness.value),

src/goto-instrument/code_contracts.cpp

@@ -266,16 +266,13 @@ void code_contractst::add_contract_check(
 {
   assert(!dest.instructions.empty());
 
-  goto_functionst::function_mapt::iterator f_it=
-    goto_functions.function_map.find(function);
-  assert(f_it!=goto_functions.function_map.end());
-
-  const goto_functionst::goto_functiont &gf=f_it->second;
+  const symbolt &function_symbol = ns.lookup(function);
+  const code_typet &code_type = to_code_type(function_symbol.type);
 
-  const exprt &requires=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
-  const exprt &ensures=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
+  const exprt &requires =
+    static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
+  const exprt &ensures =
+    static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
   assert(ensures.is_not_nil());
 
   // build:
@@ -302,15 +299,14 @@ void code_contractst::add_contract_check(
     skip->source_location));
 
   // prepare function call including all declarations
-  const symbolt &function_symbol = ns.lookup(function);
   code_function_callt call(function_symbol.symbol_expr());
   replace_symbolt replace;
 
   // decl ret
-  if(gf.type.return_type()!=empty_typet())
+  if(code_type.return_type() != empty_typet())
   {
     symbol_exprt r = new_tmp_symbol(
-                       gf.type.return_type(),
+                       code_type.return_type(),
                        skip->source_location,
                        function,
                        function_symbol.mode)
@@ -324,22 +320,19 @@ void code_contractst::add_contract_check(
   }
 
   // decl parameter1 ...
-  for(code_typet::parameterst::const_iterator
-      p_it=gf.type.parameters().begin();
-      p_it!=gf.type.parameters().end();
-      ++p_it)
+  for(const auto &parameter : code_type.parameters())
   {
     symbol_exprt p =
       new_tmp_symbol(
-        p_it->type(), skip->source_location, function, function_symbol.mode)
+        parameter.type(), skip->source_location, function, function_symbol.mode)
         .symbol_expr();
     check.add(goto_programt::make_decl(p, skip->source_location));
 
     call.arguments().push_back(p);
 
-    if(!p_it->get_identifier().empty())
+    if(!parameter.get_identifier().empty())
     {
-      symbol_exprt cur_p(p_it->get_identifier(), p_it->type());
+      symbol_exprt cur_p(parameter.get_identifier(), parameter.type());
       replace.insert(cur_p, p);
     }
   }

src/goto-instrument/generate_function_bodies.cpp

@@ -68,7 +68,6 @@ void generate_function_bodiest::generate_parameter_names(
 
     ++it;
   }
-  function.type = to_code_type(function_symbol.type);
 }
 
 class assume_false_generate_function_bodiest : public generate_function_bodiest
@@ -215,8 +214,9 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       instruction->source_location = function_symbol.location;
       return instruction;
     };
-    const namespacet ns(symbol_table);
-    for(auto const &parameter : function.type.parameters())
+
+    const code_typet &code_type = to_code_type(function_symbol.type);
+    for(auto const &parameter : code_type.parameters())
     {
       if(
         parameter.type().id() == ID_pointer &&
@@ -269,9 +269,9 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       function.body.destructive_append(dest);
     }
 
-    if(function.type.return_type() != empty_typet())
+    if(code_type.return_type() != empty_typet())
     {
-      typet type(function.type.return_type());
+      typet type(code_type.return_type());
       type.remove(ID_C_constant);
 
       symbolt &aux_symbol = get_fresh_aux_symbol(
@@ -299,7 +299,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       function.body.destructive_append(dest);
 
       exprt return_expr = typecast_exprt::conditional_cast(
-        aux_symbol.symbol_expr(), function.type.return_type());
+        aux_symbol.symbol_expr(), code_type.return_type());
 
       add_instruction(goto_programt::make_return(code_returnt(return_expr)));
 

src/goto-programs/goto_convert_functions.cpp

@@ -86,6 +86,7 @@ bool goto_convert_functionst::hide(const goto_programt &goto_program)
 
 void goto_convert_functionst::add_return(
   goto_functionst::goto_functiont &f,
+  const typet &return_type,
   const source_locationt &source_location)
 {
   #if 0
@@ -132,7 +133,7 @@ void goto_convert_functionst::add_return(
 
   #endif
 
-  side_effect_expr_nondett rhs(f.type.return_type(), source_location);
+  side_effect_expr_nondett rhs(return_type, source_location);
 
   f.body.add(
     goto_programt::make_return(code_returnt(std::move(rhs)), source_location));
@@ -183,16 +184,15 @@ void goto_convert_functionst::convert_function(
 
   targets=targetst();
   targets.set_return(end_function);
-  targets.has_return_value=
-    f.type.return_type().id()!=ID_empty &&
-    f.type.return_type().id()!=ID_constructor &&
-    f.type.return_type().id()!=ID_destructor;
+  targets.has_return_value = code_type.return_type().id() != ID_empty &&
+                             code_type.return_type().id() != ID_constructor &&
+                             code_type.return_type().id() != ID_destructor;
 
   goto_convert_rec(code, f.body, mode);
 
   // add non-det return value, if needed
   if(targets.has_return_value)
-    add_return(f, end_location);
+    add_return(f, code_type.return_type(), end_location);
 
   // handle SV-COMP's __VERIFIER_atomic_
   if(!f.body.instructions.empty() &&

src/goto-programs/goto_convert_functions.h

@@ -58,6 +58,7 @@ class goto_convert_functionst:public goto_convertt
   //
   void add_return(
     goto_functionst::goto_functiont &,
+    const typet &return_type,
     const source_locationt &);
 };
 

src/goto-programs/goto_function.cpp

@@ -21,12 +21,9 @@ void get_local_identifiers(
 {
   goto_function.body.get_decl_identifiers(dest);
 
-  const code_typet::parameterst &parameters = goto_function.type.parameters();
-
   // add parameters
-  for(const auto &param : parameters)
+  for(const auto &identifier : goto_function.parameter_identifiers)
   {
-    const irep_idt &identifier = param.get_identifier();
     if(identifier != "")
       dest.insert(identifier);
   }
@@ -40,27 +37,4 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
   const
 {
   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

@@ -28,63 +28,32 @@ class goto_functiont
 public:
   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 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);
-  }
-
-  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;
   }
 
@@ -93,15 +62,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.h

@@ -149,6 +149,18 @@ class goto_functionst
       }
 
       goto_function.validate(ns, vm);
+
+      // Check that a void function does not contain any RETURN instructions
+      if(to_code_type(function_symbol.type).return_type().id() == ID_empty)
+      {
+        forall_goto_program_instructions(instruction, goto_function.body)
+        {
+          DATA_CHECK(
+            vm,
+            !instruction->is_return(),
+            "void function should not return a value");
+        }
+      }
     }
   }
 };