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)

1 files changed, 45 insertions, 143 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 68c19db0..0610b242 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -255,6 +255,12 @@ Proof.
   destruct (Int.eq (high_s (Ptrofs.to_int i)) Int.zero); TailNoLabel.
 Qed.
 
+Remark transl_epilogue_label:
+  forall f k, tail_nolabel k (transl_epilogue f k).
+Proof.
+  intros; unfold transl_epilogue; destruct (is_leaf_function f); TailNoLabel.
+Qed.
+
 Lemma transl_instr_label:
   forall f i ep k c,
   transl_instr f i ep k = OK c ->
@@ -269,9 +275,10 @@ Proof.
   destruct m; monadInv H; (eapply tail_nolabel_trans; [eapply transl_memory_access_label; TailNoLabel|TailNoLabel]).
   destruct m; monadInv H; eapply transl_memory_access_label; TailNoLabel.
   destruct s0; monadInv H; TailNoLabel.
-  destruct s0; monadInv H; TailNoLabel.
+  destruct s0; monadInv H; TailNoLabel; (eapply tail_nolabel_trans; [apply transl_epilogue_label | TailNoLabel]). 
   eapply tail_nolabel_trans. eapply transl_cond_label; eauto.
   destruct (snd (crbit_for_cond c0)); TailNoLabel.
+  eapply tail_nolabel_trans; [apply transl_epilogue_label | TailNoLabel]. 
 Qed.
 
 Lemma transl_instr_label':
@@ -657,11 +664,7 @@ Opaque loadind.
   assert (f0 = f) by congruence.  subst f0.
   inversion AT; subst.
   assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-    eapply transf_function_no_overflow; eauto.  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
-  exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]].
-  exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]].
+    eapply transf_function_no_overflow; eauto.
   destruct ros as [rf|fid]; simpl in H; monadInv H7.
 + (* Indirect call *)
   assert (rs rf = Vptr f' Ptrofs.zero).
@@ -669,83 +672,41 @@ Opaque loadind.
     revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence.
   assert (rs0 x0 = Vptr f' Ptrofs.zero).
     exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto.
-  set (rs2 := nextinstr (rs0#CTR <- (Vptr f' Ptrofs.zero))).
-  set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))).
-  set (rs4 := nextinstr (rs3#LR <- (parent_ra s))).
-  set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))).
-  set (rs6 := rs5#PC <- (rs5 CTR)).
-  assert (exec_straight tge tf
-            (Pmtctr x0 :: Plwz GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) GPR1 :: Pmtlr GPR0
-              :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr sig :: x)
+  set (rs1 := nextinstr (rs0#CTR <- (Vptr f' Ptrofs.zero))).
+  assert (AG1: agree rs (Vptr stk soff) rs1). { apply agree_nextinstr. apply agree_set_other; auto. }
+  exploit transl_epilogue_correct; eauto. 
+  intros (rs2 & m2' & A & B & C & D & E & F). 
+  assert (A': exec_straight tge tf
+            (Pmtctr x0 :: transl_epilogue f (Pbctr sig :: x))
             rs0 m'0
-            (Pbctr sig :: x) rs5 m2').
-  apply exec_straight_step with rs2 m'0.
-  simpl. rewrite H9. auto. auto.
-  apply exec_straight_step with rs3 m'0.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  change (rs2 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG).
-  erewrite loadv_offset_ptr by eexact C. auto. congruence. auto.
-  apply exec_straight_step with rs4 m'0.
-  simpl. reflexivity. reflexivity.
-  apply exec_straight_one.
-  simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG).
-  simpl. rewrite A.
-  rewrite E. reflexivity. reflexivity.
-  left; exists (State rs6 m2'); split.
+            (Pbctr sig :: x) rs2 m2').
+  { apply exec_straight_step with rs1 m'0. simpl. rewrite H9. reflexivity. reflexivity. eexact A. }
+  clear A.
+  exploit exec_straight_steps_2; eauto using functions_transl. 
+  intros (ofs' & U & V).
+  set (rs3 := rs2#PC <- (rs2 CTR)).
+  left; exists (State rs3 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor.
-  change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one).
-  rewrite <- H4; simpl. eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail.
-  repeat (eapply code_tail_next_int; auto). eauto.
-  simpl. reflexivity. traceEq.
+  econstructor; eauto using functions_transl, find_instr_tail.
+  traceEq.
   (* match states *)
-  econstructor; eauto.
-Hint Resolve agree_nextinstr agree_set_other: asmgen.
-  assert (AG4: agree rs (Vptr stk soff) rs4).
-    unfold rs4, rs3, rs2; auto 10 with asmgen.
-  assert (AG5: agree rs (parent_sp s) rs5).
-    unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto.
-    eapply parent_sp_def; eauto.
-  unfold rs6, rs5; auto 10 with asmgen.
+  econstructor; eauto. apply agree_set_other; auto. 
+  unfold rs3; Simpl. rewrite F by congruence. reflexivity.
 + (* Direct call *)
-  set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))).
-  set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
-  set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
-  set (rs5 := rs4#PC <- (Vptr f' Ptrofs.zero)).
-  assert (exec_straight tge tf
-            (Plwz GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) GPR1 :: Pmtlr GPR0
-             :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid sig :: x)
-            rs0 m'0
-            (Pbs fid sig :: x) rs4 m2').
-  apply exec_straight_step with rs2 m'0.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  rewrite <- (sp_val _ _ _ AG).  erewrite loadv_offset_ptr by eexact C. auto. congruence. auto.
-  apply exec_straight_step with rs3 m'0.
-  simpl. reflexivity. reflexivity.
-  apply exec_straight_one.
-  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). simpl. rewrite A.
-  rewrite E. reflexivity. reflexivity.
-  left; exists (State rs5 m2'); split.
+  exploit transl_epilogue_correct; eauto. 
+  intros (rs2 & m2' & A & B & C & D & E & F). 
+  exploit exec_straight_steps_2; eauto using functions_transl. 
+  intros (ofs' & U & V).
+  set (rs3 := rs2#PC <- (Vptr f' Ptrofs.zero)).
+  left; exists (State rs3 m2'); split.
   (* execution *)
   eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor.
-  change (rs4 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one).
-  rewrite <- H4; simpl. eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail.
-  repeat (eapply code_tail_next_int; auto). eauto.
-  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. traceEq.
+  econstructor; eauto using functions_transl, find_instr_tail.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved, H. reflexivity.
+  traceEq.
   (* match states *)
-  econstructor; eauto.
-  assert (AG3: agree rs (Vptr stk soff) rs3).
-    unfold rs3, rs2; auto 10 with asmgen.
-  assert (AG4: agree rs (parent_sp s) rs4).
-    unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto.
-    eapply parent_sp_def; eauto.
-  unfold rs5; auto 10 with asmgen.
+  econstructor; eauto. apply agree_set_other; auto. 
 
 - (* Mbuiltin *)
   inv AT. monadInv H4.
@@ -850,79 +811,20 @@ Local Transparent destroyed_by_jumptable.
   inversion AT; subst.
   assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
     eapply transf_function_no_overflow; eauto.
-  rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]].
-  exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]].
-  exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
-  exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]].
-  monadInv H6. destruct (is_leaf_function f) eqn:ISLEAF; monadInv EQ0.
-+ (* leaf function *)
-  set (rs2 := nextinstr (rs0#GPR1 <- (parent_sp s))).
+  monadInv H6.
+  exploit transl_epilogue_correct; eauto. 
+  intros (rs2 & m2' & A & B & C & D & E & F).
+  exploit exec_straight_steps_2; eauto using functions_transl. 
+  intros (ofs' & U & V).
   set (rs3 := rs2#PC <- (parent_ra s)).
-  assert (exec_straight tge tf
-           (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0
-           (Pblr :: x) rs2 m2').
-  simpl. apply exec_straight_one. 
-  simpl. rewrite A.
-  rewrite <- (sp_val _ _ _ AG). rewrite E. auto.
-  auto.
   left; exists (State rs3 m2'); split.
   (* execution *)
-  apply plus_right' with E0 (State rs2 m2') E0.
-  eapply exec_straight_exec; eauto.
-  econstructor.
-  change (rs2 PC) with (Val.offset_ptr (rs0 PC) Ptrofs.one).
-  rewrite <- H3. simpl. eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail.
-  eapply code_tail_next_int; eauto.
-  simpl. change (rs2 LR) with (rs0 LR). rewrite LEAF by auto. reflexivity. 
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor; eauto using functions_transl, find_instr_tail.
+  simpl. rewrite D; reflexivity. 
   traceEq.
   (* match states *)
-  econstructor; eauto.
-  assert (AG2: agree rs (parent_sp s) rs2).
-    unfold rs2. apply agree_nextinstr. eapply agree_change_sp; eauto.
-    eapply parent_sp_def; eauto.
-  unfold rs3; auto with asmgen.
-+ (* non-leaf function *)
-  set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))).
-  set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
-  set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
-  set (rs5 := rs4#PC <- (parent_ra s)).
-  assert (exec_straight tge tf
-           (Plwz GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) GPR1
-           :: Pmtlr GPR0
-           :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0
-           (Pblr :: x) rs4 m2').
-  simpl. apply exec_straight_three with rs2 m'0 rs3 m'0.
-  simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  erewrite loadv_offset_ptr by eexact C. auto. congruence.
-  simpl. auto.
-  simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A.
-  rewrite <- (sp_val _ _ _ AG). rewrite E. auto.
-  auto. auto. auto.
-  left; exists (State rs5 m2'); split.
-  (* execution *)
-  apply plus_right' with E0 (State rs4 m2') E0.
-  eapply exec_straight_exec; eauto.
-  econstructor.
-  change (rs4 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one).
-  rewrite <- H3. simpl. eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail.
-  eapply code_tail_next_int; auto.
-  eapply code_tail_next_int; auto.
-  eapply code_tail_next_int; eauto.
-  reflexivity. traceEq.
-  (* match states *)
-  econstructor; eauto.
-  assert (AG3: agree rs (Vptr stk soff) rs3).
-    unfold rs3, rs2; auto 10 with asmgen.
-  assert (AG4: agree rs (parent_sp s) rs4).
-    unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto.
-    eapply parent_sp_def; eauto.
-  unfold rs5; auto with asmgen.
+  econstructor; eauto. apply agree_set_other; auto. 
 
 - (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.