diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-07 08:06:23 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-07 08:06:23 +0200 |
commit | 7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2 (patch) | |
tree | 2951ff922c42f813e621181d13cb8f93102e7f2d /mppa_k1c/Asmgenproof.v | |
parent | 7946ed0e9130e164c39e137115419ea0ed158c9f (diff) | |
download | compcert-kvx-7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2.tar.gz compcert-kvx-7b2b50c23765dd4c18f1afe3a1e2936d31a93fa2.zip |
extract Machgen.trans_code stuff from Asmgenproof
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 79 |
1 files changed, 0 insertions, 79 deletions
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. |