remove_returns now preserves signature

This simplifies removal, and removes the need to query the 'original' return
type.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2089,16 +2089,14 @@ void java_bytecode_convert_methodt::convert_invoke(
   // less accurate.
   if(method_symbol != symbol_table.symbols.end())
   {
-    const auto &restored_type =
-      original_return_type(symbol_table, invoked_method_id);
     // Note the number of parameters might change here due to constructors using
     // invokespecial will have zero arguments (the `this` is added below)
     // but the symbol for the <init> will have the this parameter.
     INVARIANT(
       to_java_method_type(arg0.type()).return_type().id() ==
-        restored_type.return_type().id(),
+        to_code_type(method_symbol->second.type).return_type().id(),
       "Function return type must not change in kind");
-    arg0.type() = restored_type;
+    arg0.type() = method_symbol->second.type;
   }
 
   // Note arg0 and arg0.type() are subject to many side-effects in this method,

src/goto-checker/symex_coverage.cpp

@@ -160,9 +160,8 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   // </method>
   xml.set_attribute("name", id2string(gf_it->first));
 
-  code_typet sig_type =
-    original_return_type(ns.get_symbol_table(), gf_it->first);
-  xml.set_attribute("signature", from_type(ns, gf_it->first, sig_type));
+  xml.set_attribute(
+    "signature", from_type(ns, gf_it->first, gf_it->second.type));
 
   xml.set_attribute("line-rate", rate_detailed(lines_covered, lines_total));
   xml.set_attribute("branch-rate", rate(branches_covered, branches_total));

src/goto-programs/goto_program.cpp

@@ -713,37 +713,24 @@ void goto_programt::instructiont::validate(
             !symbol_expr_type_matches_symbol_table &&
             table_symbol->type.id() == ID_code)
           {
-            // Return removal sets the return type of a function symbol table
-            // entry to 'void', but some callsites still expect the original
-            // type (e.g. if a function is passed as a parameter)
-            symbol_expr_type_matches_symbol_table =
-              goto_symbol_expr.type() ==
-              original_return_type(ns.get_symbol_table(), goto_id);
-
+            // If a function declaration and its definition are in different
+            // translation units they may have different return types.
+            // Thus, the return type in the symbol table may differ
+            // from the return type in the symbol expr.
             if(
-              !symbol_expr_type_matches_symbol_table &&
-              goto_symbol_expr.type().id() == ID_code)
+              goto_symbol_expr.type().source_location().get_file() !=
+              table_symbol->type.source_location().get_file())
             {
-              // If a function declaration and its definition are in different
-              // translation units they may have different return types,
-              // which remove_returns patches up with a typecast. If thats
-              // the case, then the return type in the symbol table may differ
-              // from the return type in the symbol expr
-              if(
-                goto_symbol_expr.type().source_location().get_file() !=
-                table_symbol->type.source_location().get_file())
-              {
-                // temporarily fixup the return types
-                auto goto_symbol_expr_type =
-                  to_code_type(goto_symbol_expr.type());
-                auto table_symbol_type = to_code_type(table_symbol->type);
-
-                goto_symbol_expr_type.return_type() =
-                  table_symbol_type.return_type();
-
-                symbol_expr_type_matches_symbol_table =
-                  base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
-              }
+              // temporarily fixup the return types
+              auto goto_symbol_expr_type =
+                to_code_type(goto_symbol_expr.type());
+              auto table_symbol_type = to_code_type(table_symbol->type);
+
+              goto_symbol_expr_type.return_type() =
+                table_symbol_type.return_type();
+
+              symbol_expr_type_matches_symbol_table =
+                base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
             }
           }
 

src/goto-programs/remove_returns.cpp

@@ -106,13 +106,6 @@ void remove_returnst::replace_returns(
   // add return_value symbol to symbol_table, if not already created:
   const auto return_symbol = get_or_create_return_value_symbol(function_id);
 
-  // look up the function symbol
-  symbolt &function_symbol = *symbol_table.get_writeable(function_id);
-
-  // make the return type 'void'
-  function.type.return_type() = empty_typet();
-  function_symbol.type = function.type;
-
   goto_programt &goto_program = function.body;
 
   Forall_goto_program_instructions(i_it, goto_program)
@@ -164,73 +157,56 @@ bool remove_returnst::do_function_calls(
       const irep_idt function_id =
         to_symbol_expr(function_call.function()).get_identifier();
 
-      optionalt<symbol_exprt> return_value;
-      typet old_return_type;
-      bool is_stub = function_is_stub(function_id);
-
-      if(is_stub)
-      {
-        old_return_type =
-          to_code_type(function_call.function().type()).return_type();
-      }
-      else
-      {
-        // The callee may or may not already have been transformed by this pass,
-        // so its symbol-table entry may already have void return type.
-        // To simplify matters, create its return-value global now (if not
-        // already done), and use that to determine its true return type.
-        return_value = get_or_create_return_value_symbol(function_id);
-        if(!return_value.has_value()) // really void-typed?
-          continue;
-        old_return_type = return_value->type();
-      }
-
       // Do we return anything?
-      if(old_return_type != empty_typet())
+      if(
+        to_code_type(function_call.function().type()).return_type() !=
+          empty_typet() &&
+        function_call.lhs().is_not_nil())
       {
         // replace "lhs=f(...)" by
         // "f(...); lhs=f#return_value; DEAD f#return_value;"
 
-        // fix the type
-        to_code_type(function_call.function().type()).return_type()=
-          empty_typet();
+        exprt rhs;
+
+        bool is_stub = function_is_stub(function_id);
+        optionalt<symbol_exprt> return_value;
+
+        if(!is_stub)
+        {
+          return_value = get_or_create_return_value_symbol(function_id);
+          CHECK_RETURN(return_value.has_value());
+
+          // The return type in the definition of the function may differ
+          // from the return type in the declaration.  We therefore do a
+          // cast.
+          rhs = typecast_exprt::conditional_cast(
+            *return_value, function_call.lhs().type());
+        }
+        else
+        {
+          rhs = side_effect_expr_nondett(
+            function_call.lhs().type(), i_it->source_location);
+        }
+
+        goto_programt::targett t_a = goto_program.insert_after(
+          i_it,
+          goto_programt::make_assignment(
+            code_assignt(function_call.lhs(), rhs), i_it->source_location));
+
+        // fry the previous assignment
+        function_call.lhs().make_nil();
 
-        if(function_call.lhs().is_not_nil())
+        if(!is_stub)
         {
-          exprt rhs;
-
-          if(!is_stub)
-          {
-            // The return type in the definition of the function may differ
-            // from the return type in the declaration.  We therefore do a
-            // cast.
-            rhs = typecast_exprt::conditional_cast(
-              *return_value, function_call.lhs().type());
-          }
-          else
-            rhs = side_effect_expr_nondett(
-              function_call.lhs().type(), i_it->source_location);
-
-          goto_programt::targett t_a = goto_program.insert_after(
-            i_it,
-            goto_programt::make_assignment(
-              code_assignt(function_call.lhs(), rhs), i_it->source_location));
-
-          // fry the previous assignment
-          function_call.lhs().make_nil();
-
-          if(!is_stub)
-          {
-            goto_program.insert_after(
-              t_a,
-              goto_programt::make_dead(*return_value, i_it->source_location));
-          }
-
-          requires_update = true;
+          goto_program.insert_after(
+            t_a,
+            goto_programt::make_dead(*return_value, i_it->source_location));
         }
 
         // update the call
         i_it->set_function_call(function_call);
+
+        requires_update = true;
       }
     }
   }
@@ -309,31 +285,6 @@ void remove_returns(goto_modelt &goto_model)
   rr(goto_model.goto_functions);
 }
 
-/// Get code type of a function that has had remove_returns run upon it
-/// \param symbol_table: global symbol table
-/// \param function_id: function to get the type of
-/// \return the function's type with its `return_type()` restored to its
-///   original value
-code_typet original_return_type(
-  const symbol_table_baset &symbol_table,
-  const irep_idt &function_id)
-{
-  // look up the function symbol
-  const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
-  code_typet type = to_code_type(function_symbol.type);
-
-  // do we have X#return_value?
-  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
-
-  symbol_tablet::symbolst::const_iterator rv_it=
-    symbol_table.symbols.find(rv_name);
-
-  if(rv_it != symbol_table.symbols.end())
-    type.return_type() = rv_it->second.type;
-
-  return type;
-}
-
 /// turns an assignment to fkt#return_value back into 'return x'
 bool remove_returnst::restore_returns(
   goto_functionst::function_mapt::iterator f_it)
@@ -349,13 +300,6 @@ bool remove_returnst::restore_returns(
   if(rv_it==symbol_table.symbols.end())
     return true;
 
-  // look up the function symbol
-  symbolt &function_symbol=*symbol_table.get_writeable(function_id);
-
-  // restore the return type
-  f_it->second.type=original_return_type(symbol_table, function_id);
-  function_symbol.type=f_it->second.type;
-
   // remove the return_value symbol from the symbol_table
   irep_idt rv_name_id=rv_it->second.name;
   symbol_table.erase(rv_it);
@@ -407,12 +351,6 @@ void remove_returnst::undo_function_calls(
       const irep_idt function_id=
         to_symbol_expr(function_call.function()).get_identifier();
 
-      const symbolt &function_symbol=ns.lookup(function_id);
-
-      // fix the type
-      to_code_type(function_call.function().type()).return_type()=
-        to_code_type(function_symbol.type).return_type();
-
       // find "f(...); lhs=f#return_value; DEAD f#return_value;"
       // and revert to "lhs=f(...);"
       goto_programt::instructionst::iterator next = std::next(i_it);

src/goto-programs/remove_returns.h

@@ -66,18 +66,7 @@ Date:   September 2009
 /// r = func#return_value;
 ///
 /// ```
-///
-/// As `return` instructions are removed, the return types of the function types
-/// are set to void as well (represented by the type `empty_typet`). This
-/// applies both to the functions (i.e., the member `type` of `goto_functiont`)
-/// and to the call sites (i.e., the type
-/// `to_code_function_call(code).function().type()` with `code` being the code
-/// member of the `instructiont` instance that represents the function call).
-///
-/// The types of function pointer expressions in the goto program are however
-/// not changed. For example, in an assignment where `func` is assigned to a
-/// function pointer, such as `int (*f)(void) = func`, the function types
-/// appearing in the lhs and rhs both retain the integer return type.
+/// `remove_returns()` does not change the signature of the function.
 
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
@@ -106,8 +95,4 @@ void restore_returns(symbol_table_baset &, goto_functionst &);
 
 void restore_returns(goto_modelt &);
 
-code_typet original_return_type(
-  const symbol_table_baset &symbol_table,
-  const irep_idt &function_id);
-
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H

src/goto-programs/validate_goto_model.cpp

@@ -133,13 +133,7 @@ void validate_goto_modelt::check_returns_removed()
         DATA_CHECK(
           vm,
           function_call.lhs().is_nil(),
-          "function call return should be nil");
-
-        const auto &callee = to_code_type(function_call.function().type());
-        DATA_CHECK(
-          vm,
-          callee.return_type().id() == ID_empty,
-          "called function must have empty return type");
+          "function call lhs return should be nil");
       }
     }
   }