diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-25 00:57:57 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-25 00:57:57 +0100 |
commit | 469a282add58074e2bc1a2822125d18e4dc6a80d (patch) | |
tree | bbc8c3527caace03a5a815c1804f822f8c653551 /aarch64 | |
parent | b096dac760b7d306c85e2b6b9b56779018596916 (diff) | |
download | compcert-kvx-469a282add58074e2bc1a2822125d18e4dc6a80d.tar.gz compcert-kvx-469a282add58074e2bc1a2822125d18e4dc6a80d.zip |
removed RA restoration
Diffstat (limited to 'aarch64')
-rw-r--r-- | aarch64/Asmgen.v | 6 | ||||
-rw-r--r-- | aarch64/Asmgenproof.v | 7 | ||||
-rw-r--r-- | aarch64/Asmgenproof1.v | 18 |
3 files changed, 27 insertions, 4 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 875f3fd1..fc083223 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -1050,8 +1050,10 @@ 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). + 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 5f88b99b..90a06144 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. + 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 b851966d..91c5c306 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -2044,6 +2044,7 @@ 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) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> @@ -2058,7 +2059,7 @@ 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. 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'. @@ -2068,6 +2069,21 @@ Proof. 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). + destruct (is_leaf_function f). + { + 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. + } 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'. |