Modest optimization of leaf functions

Leaf functions are functions that do not call any other function.  For leaf functions, it is not necessary to save the LR register on function entry nor to reload LR on function return, since LR contains the correct return address throughout the function's execution.

This commit suppresses the reloading of LR before returning from a leaf function.  LR is still saved on the stack on function entry, because doing otherwise would require extensive changes in the Stacking pass of CompCert.  However, preliminary experiments indicate that we get good speedups by avoiding to reload LR, while avoiding to save LR makes little difference in speed.

To support this optimization and its proof:
- Mach is extended with a `is_leaf_function` Boolean function and a `wf_state` predicate to provide the semantic characterization.
- Asmgenproof* is extended with a `important_preg` Boolean function that means "data register or LR".  A number of lemmas that used to show preservation of data registers now show preservation of LR as well.

1 files changed, 8 insertions, 4 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index fc04b15d..774f58f9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -672,10 +672,14 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       do r <- ireg_of arg;
       OK (Pbtbl r tbl :: k)
   | Mreturn =>
-      OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
-          Pmtlr GPR0 ::
-          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-          Pblr :: k)
+      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)
   end.
 
 (** Translation of a code sequence *)