From 8372862b2853c1a2c3f523068b9d7e696deed22d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 May 2018 10:21:41 +0000
Subject: [PATCH 1/3] function-pointer removal: Set the mode of a return symbol

---
 src/goto-programs/remove_function_pointers.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 854a706e5e7..4225ba759ea 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -233,12 +233,15 @@ void remove_function_pointerst::fix_return_type(
        code_type.return_type(), ns))
     return;
 
+  const symbolt &function_symbol =
+    ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
+
   symbolt &tmp_symbol = get_fresh_aux_symbol(
     code_type.return_type(),
     id2string(function_call.source_location().get_function()),
     "tmp_return_val",
     function_call.source_location(),
-    irep_idt(),
+    function_symbol.mode,
     symbol_table);
 
   symbol_exprt tmp_symbol_expr;

From 4f7fade584a116e55bad6bad5a5742278c1bbf5e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 May 2018 10:22:30 +0000
Subject: [PATCH 2/3] Cleanup: use symbolt::symbol_expr

---
 src/goto-programs/remove_function_pointers.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 4225ba759ea..79ea4566c2a 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -244,9 +244,7 @@ void remove_function_pointerst::fix_return_type(
     function_symbol.mode,
     symbol_table);
 
-  symbol_exprt tmp_symbol_expr;
-  tmp_symbol_expr.type()=tmp_symbol.type;
-  tmp_symbol_expr.set_identifier(tmp_symbol.name);
+  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
 
   exprt old_lhs=function_call.lhs();
   function_call.lhs()=tmp_symbol_expr;

From 3b3dc71ff19e827fca0ecd61884cc90175cf9105 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 22 May 2018 10:24:50 +0000
Subject: [PATCH 3/3] Distinct names of return-value symbols

Function-pointer removal spends 43.52% of its time in get_max when
working on the Linux kernel. By avoiding repeated use of the same prefix
for all calls that a function pointer may expand to, the number of calls
to get_max is reduced, resulting in a total runtime reduction from 1457s to
640s.
---
 src/goto-programs/remove_function_pointers.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 79ea4566c2a..419c6d2f3ba 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -239,7 +239,7 @@ void remove_function_pointerst::fix_return_type(
   symbolt &tmp_symbol = get_fresh_aux_symbol(
     code_type.return_type(),
     id2string(function_call.source_location().get_function()),
-    "tmp_return_val",
+    "tmp_return_val_" + id2string(function_symbol.base_name),
     function_call.source_location(),
     function_symbol.mode,
     symbol_table);