Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-work

Conflicts:
	mppa_k1c/lib/Asmblockgenproof0.v

1 files changed, 4 insertions, 86 deletions

diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 588019a2..e7e21a18 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -45,96 +45,15 @@ Qed.
 
 (** Return Address Offset *)
 
-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.
+Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
+  Mach_return_address_offset Asmblockgenproof.return_address_offset.
 
 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.
 Proof.
-  intros.
-  exploit Mach_Machblock_tail; eauto.
-  destruct 1.
-  eapply Asmblockgenproof.return_address_exists; eauto.
+  intros; unfold return_address_offset; eapply Mach_return_address_exists; eauto.
+  intros; eapply Asmblockgenproof.return_address_exists; eauto.
 Qed.
 
 
@@ -154,7 +73,6 @@ Proof.
   eapply compose_forward_simulations. 
   exploit Machblockgenproof.transf_program_correct; eauto.
   unfold Machblockgenproof.inv_trans_rao. 
-  intros X; apply X.
   eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
   eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
   apply Asm.transf_program_correct. eauto.