change return_value_identifier() to return_value_symbol

All users of this function either compare the result with a symbol_exprt or
build a symbol_exprt.  This change makes the function return a symbol_exprt
instead of the identifier, which reduces effort at the call site.

Author: Daniel Kroening

src/goto-programs/mm_io.cpp

@@ -56,8 +56,7 @@ void mm_io(
           const code_typet &ct=to_code_type(mm_io_r.type());
 
           irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
-          irep_idt r_identifier = return_value_identifier(identifier, ns);
-          symbol_exprt return_value(r_identifier, ct.return_type());
+          auto return_value = return_value_symbol(identifier, ns);
           if_exprt if_expr(integer_address(d.pointer()), return_value, d);
           if(!replace_expr(d, if_expr, a.rhs()))
             it->set_assign(a);

src/goto-programs/remove_returns.cpp

@@ -64,10 +64,10 @@ optionalt<symbol_exprt>
 remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
 {
   const namespacet ns(symbol_table);
-  const irep_idt symbol_name = return_value_identifier(function_id, ns);
-  const symbolt *existing_symbol = symbol_table.lookup(symbol_name);
-  if(existing_symbol != nullptr)
-    return existing_symbol->symbol_expr();
+  const auto symbol_expr = return_value_symbol(function_id, ns);
+  const auto symbol_name = symbol_expr.get_identifier();
+  if(symbol_table.has_symbol(symbol_name))
+    return symbol_expr;
 
   const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
   const typet &return_type = to_code_type(function_symbol.type).return_type();
@@ -296,7 +296,8 @@ bool remove_returnst::restore_returns(
 
   // do we have X#return_value?
   const namespacet ns(symbol_table);
-  auto rv_name = return_value_identifier(function_id, ns);
+  auto rv_symbol = return_value_symbol(function_id, ns);
+  auto rv_name = rv_symbol.get_identifier();
 
   symbol_tablet::symbolst::const_iterator rv_it=
     symbol_table.symbols.find(rv_name);
@@ -368,12 +369,8 @@ void remove_returnst::undo_function_calls(
 
       const code_assignt &assign = next->get_assign();
 
-      if(assign.rhs().id()!=ID_symbol)
-        continue;
-
-      irep_idt rv_name = return_value_identifier(function_id, ns);
-      const symbol_exprt &rhs=to_symbol_expr(assign.rhs());
-      if(rhs.get_identifier()!=rv_name)
+      const auto rv_symbol = return_value_symbol(function_id, ns);
+      if(assign.rhs() != rv_symbol)
         continue;
 
       // restore the previous assignment
@@ -414,7 +411,10 @@ void restore_returns(goto_modelt &goto_model)
   rr.restore(goto_model.goto_functions);
 }
 
-irep_idt return_value_identifier(const irep_idt &identifier, const namespacet &)
+symbol_exprt
+return_value_symbol(const irep_idt &identifier, const namespacet &ns)
 {
-  return id2string(identifier) + RETURN_VALUE_SUFFIX;
+  const symbolt &function_symbol = ns.lookup(identifier);
+  const typet &return_type = to_code_type(function_symbol.type).return_type();
+  return symbol_exprt(id2string(identifier) + RETURN_VALUE_SUFFIX, return_type);
 }

src/goto-programs/remove_returns.h

@@ -78,8 +78,9 @@ Date:   September 2009
 class goto_functionst;
 class goto_model_functiont;
 class goto_modelt;
-class symbol_table_baset;
 class namespacet;
+class symbol_table_baset;
+class symbol_exprt;
 
 void remove_returns(symbol_table_baset &, goto_functionst &);
 
@@ -94,8 +95,8 @@ void restore_returns(symbol_table_baset &, goto_functionst &);
 
 void restore_returns(goto_modelt &);
 
-/// produces the identifier that is used to store the return
+/// produces the symbol that is used to store the return
 /// value of the function with the given identifier
-irep_idt return_value_identifier(const irep_idt &, const namespacet &);
+symbol_exprt return_value_symbol(const irep_idt &, const namespacet &);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H

src/goto-programs/replace_calls.cpp

@@ -97,16 +97,18 @@ void replace_callst::operator()(
     PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns));
 
     // check that returns have not been removed
-    goto_programt::const_targett next_it = std::next(it);
-    if(next_it != goto_program.instructions.end() && next_it->is_assign())
+    if(to_code_type(f_it1->second.type).return_type().id() != ID_empty)
     {
-      const code_assignt &ca = next_it->get_assign();
-      const exprt &rhs = ca.rhs();
-
-      INVARIANT(
-        rhs.id() != ID_symbol || to_symbol_expr(rhs).get_identifier() !=
-                                   return_value_identifier(id, ns),
-        "returns must not be removed before replacing calls");
+      goto_programt::const_targett next_it = std::next(it);
+      if(next_it != goto_program.instructions.end() && next_it->is_assign())
+      {
+        const code_assignt &ca = next_it->get_assign();
+        const exprt &rhs = ca.rhs();
+
+        INVARIANT(
+          rhs != return_value_symbol(id, ns),
+          "returns must not be removed before replacing calls");
+      }
     }
 
     // Finally modify the call