Do not read from goto_functiont::type

Future changes will remove this member as it is redundant with the information
stored in the symbol table. We keep writing to it so as not to break any users,
but no longer read it.

Author: tautschnig

src/goto-instrument/code_contracts.cpp

@@ -763,18 +763,15 @@ void code_contractst::add_contract_check(
 {
   PRECONDITION(!dest.instructions.empty());
 
-  goto_functionst::function_mapt::iterator f_it =
-    goto_functions.function_map.find(mangled_fun);
-  PRECONDITION(f_it != goto_functions.function_map.end());
-
-  const goto_functionst::goto_functiont &gf = f_it->second;
+  const symbolt &function_symbol = ns.lookup(mangled_fun);
+  const code_typet &code_type = to_code_type(function_symbol.type);
 
   const exprt &assigns =
-    static_cast<const exprt &>(gf.type.find(ID_C_spec_assigns));
+    static_cast<const exprt &>(code_type.find(ID_C_spec_assigns));
   const exprt &requires =
-    static_cast<const exprt &>(gf.type.find(ID_C_spec_requires));
+    static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
   const exprt &ensures =
-    static_cast<const exprt &>(gf.type.find(ID_C_spec_ensures));
+    static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
   INVARIANT(
     ensures.is_not_nil() || assigns.is_not_nil(),
     "Code contract enforcement is trivial without an ensures or assigns "
@@ -803,15 +800,14 @@ void code_contractst::add_contract_check(
     skip->source_location));
 
   // prepare function call including all declarations
-  const symbolt &function_symbol = ns.lookup(mangled_fun);
   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,
                        wrapper_fun,
                        function_symbol.mode)

src/goto-instrument/generate_function_bodies.cpp

@@ -321,9 +321,10 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       function.body.destructive_append(dest);
     }
 
-    if(function.type.return_type() != empty_typet())
+    const typet &return_type = to_code_type(function_symbol.type).return_type();
+    if(return_type != empty_typet())
     {
-      typet type(function.type.return_type());
+      typet type(return_type);
       type.remove(ID_C_constant);
 
       symbolt &aux_symbol = get_fresh_aux_symbol(
@@ -350,8 +351,8 @@ 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());
+      exprt return_expr =
+        typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type);
 
       add_instruction(goto_programt::make_return(code_returnt(return_expr)));
 

src/goto-instrument/replace_calls.cpp

@@ -112,7 +112,7 @@ void replace_callst::operator()(
     }
 
     // Finally modify the call
-    function.type() = f_it2->second.type;
+    function.type() = ns.lookup(f_it2->first).type;
     se.set_identifier(new_id);
 
     ins.set_function_call(cfc);
@@ -167,7 +167,8 @@ void replace_callst::check_replacement_map(
     auto it1 = goto_functions.function_map.find(p.first);
     if(it1 != goto_functions.function_map.end())
     {
-      if(!base_type_eq(it1->second.type, it2->second.type, ns))
+      if(!base_type_eq(
+           ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns))
         throw invalid_command_line_argument_exceptiont(
           "functions " + id2string(p.first) + " and " + id2string(p.second) +
             " are not type-compatible",

src/goto-programs/goto_convert_functions.cpp

@@ -87,6 +87,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
@@ -133,7 +134,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));
@@ -190,15 +191,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(

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_functions.cpp

@@ -137,5 +137,17 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm)
     }
 
     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");
+      }
+    }
   }
 }

src/goto-programs/link_goto_model.cpp

@@ -100,6 +100,11 @@ static bool link_functions(
         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)

src/goto-programs/remove_function_pointers.cpp

@@ -125,7 +125,7 @@ remove_function_pointerst::remove_function_pointerst(
 
   // build type map
   forall_goto_functions(f_it, goto_functions)
-    type_map.emplace(f_it->first, f_it->second.type);
+    type_map.emplace(f_it->first, to_code_type(ns.lookup(f_it->first).type));
 }
 
 bool remove_function_pointerst::arg_is_type_compatible(

src/goto-programs/remove_returns.cpp

@@ -101,10 +101,11 @@ void remove_returnst::replace_returns(
   const irep_idt &function_id,
   goto_functionst::goto_functiont &function)
 {
-  typet return_type = function.type.return_type();
+  // look up the function symbol
+  symbolt &function_symbol = *symbol_table.get_writeable(function_id);
 
   // returns something but void?
-  if(return_type == empty_typet())
+  if(to_code_type(function_symbol.type).return_type() == empty_typet())
     return;
 
   // add return_value symbol to symbol_table, if not already created:

src/goto-symex/symex_function_call.cpp

@@ -42,8 +42,6 @@ void goto_symext::parameter_assignments(
   statet &state,
   const exprt::operandst &arguments)
 {
-  const code_typet &function_type=goto_function.type;
-
   // iterates over the arguments
   exprt::operandst::const_iterator it1=arguments.begin();
 
@@ -151,7 +149,7 @@ void goto_symext::parameter_assignments(
       it1++;
   }
 
-  if(function_type.has_ellipsis())
+  if(to_code_type(ns.lookup(function_identifier).type).has_ellipsis())
   {
     // These are va_arg arguments; their types may differ from call to call
     for(; it1 != arguments.end(); it1++)