diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-07 14:13:54 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-04-28 15:00:03 +0200 |
| commit | 53c1757eeb2a76bae796854b9437808ce7ac907e (patch) | |
| tree | 9cb8cdb2a3c70496e883bccaed681595529de735 /powerpc/Asmgen.v | |
| parent | 2b3e1f021b2131917cc7a2cf6d3d0d2db9d41ecc (diff) | |
| download | compcert-kvx-53c1757eeb2a76bae796854b9437808ce7ac907e.tar.gz compcert-kvx-53c1757eeb2a76bae796854b9437808ce7ac907e.zip | |
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)
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 31 |
1 files changed, 15 insertions, 16 deletions
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 *) |