extract Machgen.trans_code stuff from Asmgenproof

3 files changed, 65 insertions, 99 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.
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 ->