From 53c1757eeb2a76bae796854b9437808ce7ac907e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 7 Apr 2017 14:13:54 +0200
Subject: Modest optimization of leaf functions (continued)

- Avoid reloading LR before a tail call if we're in a leaf function
- Factor out the code that reloads LR if necessary (function Asmgen.transl_epilogue)
- Factor out the corresponding parts of the proof (Asmgenproof1.transl_epilogue_correct, Asmgenproof.step_simulation)
---
 powerpc/Asmgen.v | 31 +++++++++++++++----------------
 1 file changed, 15 insertions(+), 16 deletions(-)

(limited to 'powerpc/Asmgen.v')

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 774f58f9..1c97c5b0 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -621,6 +621,18 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
       Error (msg "Asmgen.transl_store")
   end.
 
+(** Function epilogue: reload return address into register LR and
+    free the stack frame.  No need to reload the return address if
+    this is a tail function. *)
+
+Definition transl_epilogue (f: Mach.function) (k: code) :=
+  if is_leaf_function f then
+    Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
+  else
+    Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
+    Pmtlr GPR0 ::
+    Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k.
+
 (** Translation of a Mach instruction. *)
 
 Definition transl_instr (f: Mach.function) (i: Mach.instruction)
@@ -649,15 +661,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mtailcall sig (inl r) =>
       do r1 <- ireg_of r;
       OK (Pmtctr r1 ::
-          Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
-          Pmtlr GPR0 ::
-          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-          Pbctr sig :: k)
+          transl_epilogue f (Pbctr sig :: k))
   | Mtailcall sig (inr symb) =>
-      OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
-          Pmtlr GPR0 ::
-          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-          Pbs symb sig :: k)
+      OK (transl_epilogue f (Pbs symb sig :: k))
   | Mbuiltin ef args res =>
       OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
   | Mlabel lbl =>
@@ -672,14 +678,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       do r <- ireg_of arg;
       OK (Pbtbl r tbl :: k)
   | Mreturn =>
-      if is_leaf_function f then
-        OK (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-            Pblr :: k)
-      else
-        OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
-            Pmtlr GPR0 ::
-            Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-            Pblr :: k)
+      OK (transl_epilogue f (Pblr :: k))
   end.
 
 (** Translation of a code sequence *)
-- 
cgit