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/Asmgenproof1.v | |
| parent | b096dac760b7d306c85e2b6b9b56779018596916 (diff) | |
| download | compcert-kvx-469a282add58074e2bc1a2822125d18e4dc6a80d.tar.gz compcert-kvx-469a282add58074e2bc1a2822125d18e4dc6a80d.zip | |
removed RA restoration
Diffstat (limited to 'aarch64/Asmgenproof1.v')
| -rw-r--r-- | aarch64/Asmgenproof1.v | 18 |
1 files changed, 17 insertions, 1 deletions
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'. |