From 7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sun, 7 Apr 2019 08:06:23 +0200 Subject: extract Machgen.trans_code stuff from Asmgenproof --- mppa_k1c/Asmgenproof.v | 79 ---------------------------------------- mppa_k1c/Machblockgenproof.v | 69 ++++++++++++++++++++++++++++++++--- mppa_k1c/lib/Asmblockgenproof0.v | 16 +------- 3 files changed, 65 insertions(+), 99 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 8eb0b693..b0e7619d 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -45,85 +45,6 @@ Qed. Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs. - -(* TODO: put this proof in Machblocgen ? (it is specific to Machblocgen) *) -Lemma trans_code_monotonic c i b l: - trans_code c = b::l -> - exists l', exists b', trans_code (i::c) = l' ++ (b'::l). -Proof. - destruct c as [|i' c]. { rewrite trans_code_equation; intros; congruence. } - destruct (get_code_nature (i :: i':: c)) eqn:GCNIC. - - apply get_code_nature_empty in GCNIC. discriminate. - - (* i=label *) - destruct i; try discriminate. - rewrite! trans_code_equation; - remember (to_bblock (Mlabel l0 :: i' :: c)) as b0. - destruct b0 as [b0 c0]. - exploit to_bblock_label; eauto. - intros (H1 & H2). rewrite H2; simpl; clear H2. - intros H2; inversion H2; subst. - exists nil; simpl; eauto. - - (*i=basic *) - rewrite! trans_code_equation; destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate]. - destruct (cn_eqdec (get_code_nature (i':: c)) IsLabel). - + (* i'=label *) remember (to_bblock (i :: i' :: c)) as b1. - destruct b1 as [b1 c1]. - assert (X: c1 = i'::c). - { generalize Heqb1; clear Heqb1. - unfold to_bblock. - erewrite to_bblock_header_noLabel; try congruence. - destruct i'; try discriminate. - destruct i; try discriminate; simpl; - intro X; inversion X; auto. - } - subst c1. - rewrite !trans_code_equation. intro H1; rewrite H1. - exists (b1 :: nil). simpl; eauto. - + (* i'<>label *) remember (to_bblock (i :: i' :: c)) as b1. - destruct b1 as [b1 c1]. - remember (to_bblock (i' :: c)) as b2. - destruct b2 as [b2 c2]. - intro H1; assert (X: c1=c2). - { generalize Heqb1, Heqb2; clear Heqb1 Heqb2. - unfold to_bblock. - erewrite to_bblock_header_noLabel; try congruence. - destruct i'; simpl in * |- ; try congruence; - destruct i; try discriminate; simpl; - try (destruct (to_bblock_body c) as [xx yy], (to_bblock_exit yy); - intros X1 X2; inversion X1; inversion X2; auto). - } - subst; inversion H1. - exists nil; simpl; eauto. - - (* i=cfi *) - remember (to_cfi i) as cfi. - intros H. destruct cfi. - + erewrite trans_code_cfi; eauto. - rewrite H. - refine (ex_intro _ (_::nil) _). simpl; eauto. - + destruct i; simpl in * |-; try congruence. -Qed. - -Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> - exists b, (* Machblock.exit b = Some (Machblock.MBcall sg ros) /\ *) - is_tail (b :: trans_code c) (trans_code c2). -Proof. - intro H; induction 1. - - intros; subst. - rewrite (trans_code_equation (Mcall sg ros :: c)). - simpl. - eapply ex_intro; eauto with coqlib. - - intros; exploit IHis_tail; eauto. clear IHis_tail. - intros (b & Hb). - + inversion Hb; clear Hb. - * exploit (trans_code_monotonic c2 i); eauto. - intros (l' & b' & Hl'); rewrite Hl'. - simpl; eauto with coqlib. - * exploit (trans_code_monotonic c2 i); eauto. - intros (l' & b' & Hl'); rewrite Hl'. - simpl; eapply ex_intro. - eapply is_tail_trans; eauto with coqlib. -Qed. - Lemma return_address_exists: forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> exists ra, return_address_offset f c ra. diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 07ec9d08..11c3db6d 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -17,6 +17,11 @@ Require Import Machblock. Require Import Machblockgen. Require Import ForwardSimulationBlock. +Ltac subst_is_trans_code H := + rewrite is_trans_code_inv in H; + rewrite <- H in * |- *; + rewrite <- is_trans_code_inv in H. + Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) := rao (transf_function f) (trans_code c). @@ -199,11 +204,6 @@ Definition concat (h: list label) (c: code): code := | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c' end. -Ltac subst_is_trans_code H := - rewrite is_trans_code_inv in H; - rewrite <- H in * |- *; - rewrite <- is_trans_code_inv in H. - Lemma find_label_transcode_preserved: forall l c c', Mach.find_label l c = Some c' -> @@ -650,3 +650,62 @@ Proof. Qed. End PRESERVATION. + +(** Auxiliary lemmas used in [Asmgenproof.return_address_exists] *) + +Lemma is_trans_code_monotonic i c b l: + is_trans_code c (b::l) -> + exists l' b', is_trans_code (i::c) (l' ++ (b'::l)). +Proof. + intro H; destruct c as [|i' c]. { inversion H. } + remember (trans_inst i) as ti. + destruct ti as [lbl|bi|cfi]. + - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2:{ destruct i; simpl in * |- *; try congruence. } + exists nil; simpl; eexists. eapply Tr_add_label; eauto. +Admitted. (* A FINIR *) + +Lemma trans_code_monotonic i c b l: + (b::l) = trans_code c -> + exists l' b', trans_code (i::c) = (l' ++ (b'::l)). +Proof. + intro H; rewrite <- is_trans_code_inv in H. + destruct (is_trans_code_monotonic i c b l H) as (l' & b' & H0). + subst_is_trans_code H0. + eauto. +Qed. + +(* FIXME: these two lemma should go into [Coqlib.v] *) +Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). +Proof. + induction l1; simpl; auto with coqlib. +Qed. +Hint Resolve is_tail_app: coqlib. + +Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. +Proof. + induction l1; simpl; auto with coqlib. + intros l2 l3 H; inversion H; eauto with coqlib. +Qed. +Hint Resolve is_tail_app_inv: coqlib. + + +Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> + exists b, is_tail (b :: trans_code c) (trans_code c2). +Proof. + intros H; induction 1. + - intros; subst. + remember (trans_code (Mcall _ _::c)) as tc2. + rewrite <- is_trans_code_inv in Heqtc2. + inversion Heqtc2; simpl in * |- *; subst; try congruence. + subst_is_trans_code H1. + eapply ex_intro; eauto with coqlib. + - intros; exploit IHis_tail; eauto. clear IHis_tail. + intros (b & Hb). inversion Hb; clear Hb. + * exploit (trans_code_monotonic i c2); eauto. + intros (l' & b' & Hl'); rewrite Hl'. + exists b'; simpl; eauto with coqlib. + * exploit (trans_code_monotonic i c2); eauto. + intros (l' & b' & Hl'); rewrite Hl'. + simpl; eapply ex_intro. + eapply is_tail_trans; eauto with coqlib. +Qed. diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 443e8757..86c81c8d 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -14,6 +14,7 @@ Require Import Machblock. Require Import Asmblock. Require Import Asmblockgen. Require Import Conventions1. +Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) Module MB:=Machblock. Module AB:=Asmblock. @@ -571,21 +572,6 @@ Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : P transl_blocks f c false = OK tc -> code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc. -(* NB: these two lemma should go into [Coqlib.v] *) -Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). -Proof. - induction l1; simpl; auto with coqlib. -Qed. -Hint Resolve is_tail_app: coqlib. - -Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. -Proof. - induction l1; simpl; auto with coqlib. - intros l2 l3 H; inversion H; eauto with coqlib. -Qed. -Hint Resolve is_tail_app_inv: coqlib. - - Lemma transl_blocks_tail: forall f c1 c2, is_tail c1 c2 -> forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 -> -- cgit