Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ci

3 files changed, 44 insertions, 5 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 46dd875d..024c9a17 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -1061,8 +1061,13 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) :=
 (** Function epilogue *)
 
 Definition make_epilogue (f: Mach.function) (k: code) :=
-  loadptr XSP f.(fn_retaddr_ofs) RA
-    (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+  (* FIXME
+     Cannot be used because memcpy destroys X30;
+     issue being discussed with X. Leroy *)
+  (* if is_leaf_function f
+  then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
+  else*) loadptr XSP f.(fn_retaddr_ofs) RA
+         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
   
 (** Translation of a Mach instruction. *)
 
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 03a3be60..6831509f 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -337,7 +337,12 @@ Qed.
 Remark make_epilogue_label:
   forall f k, tail_nolabel k (make_epilogue f k).
 Proof.
-  unfold make_epilogue; intros. eapply tail_nolabel_trans. apply loadptr_label. TailNoLabel.
+  unfold make_epilogue; intros.
+  (* FIXME destruct is_leaf_function.
+  { TailNoLabel. } *)
+  eapply tail_nolabel_trans.
+  apply loadptr_label.
+  TailNoLabel.
 Qed.
 
 Lemma transl_instr_label:
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index fe7f0ed6..0e36bd05 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -2068,8 +2068,9 @@ Qed.
 
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,
+  (is_leaf_function f = true -> rs # (IR RA) = parent_ra cs) ->
   load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
-  load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
+  ((* FIXME is_leaf_function f = false -> *) load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs)) ->
   Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
   agree ms (Vptr stk soff) rs ->
   Mem.extends m tm ->
@@ -2082,16 +2083,44 @@ Lemma make_epilogue_correct:
   /\ rs'#SP = parent_sp cs
   /\ (forall r, r <> PC -> r <> SP -> r <> RA -> r <> X16 -> rs'#r = rs#r).
 Proof.
-  intros until tm; intros LP LRA FREE AG MEXT MCS.
+  intros until tm; intros LEAF_RA LP LRA FREE AG MEXT MCS.
+
+  (* FIXME
+  Cannot be used at this point
+  destruct (is_leaf_function f) eqn:IS_LEAF.
+  {
+  exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
+  exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
+  exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
+  unfold make_epilogue.
+  rewrite IS_LEAF.
+
+  econstructor; econstructor; split.
+  apply exec_straight_one. simpl.
+  rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. 
+    rewrite FREE'. eauto. auto. 
+  split. apply agree_nextinstr. apply agree_set_other; auto.
+  apply agree_change_sp with (Vptr stk soff).
+  apply agree_exten with rs; auto.
+  eapply parent_sp_def; eauto.
+  split. auto.
+  split. Simpl.
+  split. Simpl.
+  intros. Simpl.
+  }
+  lapply LRA. 2: reflexivity.
+  clear LRA. intro LRA. *)
   exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP').
   exploit Mem.loadv_extends. eauto. eexact LRA. auto. simpl. intros (ra' & LRA' & LDRA').
   exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'.
   exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'.
   exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
   unfold make_epilogue.
+  (* FIXME rewrite IS_LEAF. *)
   exploit (loadptr_correct XSP (fn_retaddr_ofs f)).
     instantiate (2 := rs). simpl. rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; congruence.
   intros (rs1 & A1 & B1 & C1).
+
   econstructor; econstructor; split.
   eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. 
     simpl; rewrite (C1 SP) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'.