diff options
| -rw-r--r-- | aarch64/Asmgen.v | 7 | ||||
| -rw-r--r-- | aarch64/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | aarch64/Asmgenproof1.v | 9 |
3 files changed, 13 insertions, 7 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index f4446696..024c9a17 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -1061,9 +1061,12 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := (** Function epilogue *) Definition make_epilogue (f: Mach.function) (k: code) := - if is_leaf_function f + (* 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 + 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 0d3179d4..6831509f 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -338,8 +338,8 @@ Remark make_epilogue_label: forall f k, tail_nolabel k (make_epilogue f k). Proof. unfold make_epilogue; intros. - destruct is_leaf_function. - { TailNoLabel. } + (* FIXME destruct is_leaf_function. + { TailNoLabel. } *) eapply tail_nolabel_trans. apply loadptr_label. TailNoLabel. diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 2b89723f..0e36bd05 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -2070,7 +2070,7 @@ 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) -> - (is_leaf_function f = false -> 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 -> @@ -2084,6 +2084,9 @@ Lemma make_epilogue_correct: /\ (forall r, r <> PC -> r <> SP -> r <> RA -> r <> X16 -> rs'#r = rs#r). Proof. 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'). @@ -2106,14 +2109,14 @@ Proof. intros. Simpl. } lapply LRA. 2: reflexivity. - clear LRA. intro LRA. + 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. - rewrite IS_LEAF. + (* 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). |