Machblock: Mach language with basic blocks

1 files changed, 749 insertions, 0 deletions

diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v
new file mode 100644
index 00000000..93284b0b
--- /dev/null
+++ b/mppa_k1c/Machblockgen.v
@@ -0,0 +1,749 @@
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Locations.
+Require Import Conventions.
+Require Stacklayout.
+Require Import Mach.
+Require Import Linking.
+Require Import Machblock.
+
+Definition to_basic_inst(i: Mach.instruction): option basic_inst :=
+  match i with
+  | Mgetstack ofs ty dst          => Some (MBgetstack ofs ty dst)
+  | Msetstack src ofs ty          => Some (MBsetstack src ofs ty)
+  | Mgetparam ofs ty dst          => Some (MBgetparam ofs ty dst)
+  | Mop       op args res         => Some (MBop       op args res)
+  | Mload     chunk addr args dst => Some (MBload     chunk addr args dst)
+  | Mstore    chunk addr args src => Some (MBstore    chunk addr args src)
+  | _ => None
+  end.
+
+(* version pas récursive terminale, mais plus facile pour la preuve *)
+Fixpoint to_bblock_body(c: Mach.code): bblock_body * Mach.code :=
+  match c with
+  | nil => (nil,nil)
+  | i::c' => 
+    match to_basic_inst i with
+    | Some bi => 
+       let (p,c'') := to_bblock_body c' in 
+       (bi::p, c'')
+    | None => (nil, c)
+    end
+  end.
+
+Definition to_bblock_header (c: Mach.code): option label * Mach.code :=
+  match c with
+  | (Mlabel l)::c' => (Some l, c')
+  | _ => (None, c)
+  end.
+
+
+Definition to_cfi (i: Mach.instruction): option control_flow_inst :=
+  match i with
+  | Mcall sig ros         => Some (MBcall sig ros)
+  | Mtailcall sig ros     => Some (MBtailcall sig ros)
+  | Mbuiltin ef args res  => Some (MBbuiltin ef args res)
+  | Mgoto lbl             => Some (MBgoto lbl)
+  | Mcond cond args lbl   => Some (MBcond cond args lbl)
+  | Mjumptable arg tbl    => Some (MBjumptable arg tbl)
+  | Mreturn               => Some (MBreturn)
+  | _ => None
+  end.
+
+Definition to_bblock_exit (c: Mach.code): option control_flow_inst * Mach.code :=
+  match c with
+  | nil => (None,nil)
+  | i::c' => 
+    match to_cfi i with
+    | Some bi as o => (o, c')
+    | None => (None, c)
+    end
+  end.
+
+Inductive code_nature: Set := IsEmpty | IsLabel | IsBasicInst | IsCFI.
+
+Definition get_code_nature (c: Mach.code): code_nature :=
+  match c with
+  | nil => IsEmpty
+  | (Mlabel _)::_ => IsLabel
+  | i::_ => match to_basic_inst i with
+         | Some _ => IsBasicInst
+         | None => IsCFI
+         end
+  end.
+
+Ltac Discriminate :=
+  match goal with
+  | [ H: ?a <> ?a |- _ ] => contradict H; auto
+  | _ => discriminate
+  end.
+
+
+Lemma cn_eqdec (cn1 cn2: code_nature): { cn1=cn2 } + {cn1 <> cn2}.
+Proof.
+  decide equality.
+Qed.  
+
+Lemma get_code_nature_nil c: c<>nil -> get_code_nature c <> IsEmpty.
+Proof.
+  intro. unfold get_code_nature. destruct c; try Discriminate.
+  destruct i; discriminate.
+Qed.
+
+Lemma get_code_nature_nil_contra c: get_code_nature c = IsEmpty -> c = nil.
+Proof.
+  intro. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto.
+  intro. contradict H0.
+Qed.
+
+Lemma get_code_nature_basic_inst:
+  forall c a c0,
+  c = a :: c0 ->
+  get_code_nature c = IsBasicInst ->
+  to_basic_inst a <> None.
+Proof.
+  intros. destruct a; discriminate || contradict H0; subst; simpl; discriminate.
+Qed.
+
+Lemma to_bblock_header_not_IsLabel:
+  forall c b c0,
+  get_code_nature c <> IsLabel ->
+  to_bblock_header c = (b, c0) ->
+  c = c0 /\ b=None.
+Proof.
+  intros. destruct c.
+  - simpl in H0; inversion H0; auto.
+  - destruct i; unfold to_bblock_header in H0; inversion H0; auto.
+    simpl in H; contradict H; auto.
+Qed.
+
+
+Lemma to_bblock_header_eq:
+  forall c b c0,
+  get_code_nature c <> IsLabel ->
+  to_bblock_header c = (b, c0) ->
+  c = c0.
+Proof.
+  intros; exploit to_bblock_header_not_IsLabel; intuition eauto.
+Qed.
+
+Lemma to_bblock_header_IsLabel: 
+  forall c c0 b, 
+  get_code_nature c = IsLabel -> 
+  to_bblock_header c = (b, c0) ->
+  exists l, c = (Mlabel l)::c0.
+Proof.
+  intros. destruct c; try discriminate.
+  destruct i; try discriminate.
+  unfold to_bblock_header in H0; inversion H0; eauto.
+Qed.
+
+Lemma to_bblock_header_wf: 
+  forall c b c0, 
+  get_code_nature c = IsLabel -> 
+  to_bblock_header c = (b, c0) ->
+  (length c > length c0)%nat.
+Proof.
+  intros; exploit to_bblock_header_IsLabel; eauto.
+  intros [l H1]; subst; simpl; auto.
+Qed.
+
+Ltac ExploitHeaderEq := 
+  match goal with
+  | [ H: to_bblock_header (?i0 :: ?c) = (?b, ?c0) |- _ ] =>
+      exploit (to_bblock_header_eq (i0::c) b c0); [subst; simpl; discriminate | auto | intro; subst; auto]
+  | _ => idtac
+  end.
+
+Lemma to_bblock_header_wfe:
+  forall c b c0,
+  to_bblock_header c = (b, c0) ->
+  (length c >= length c0)%nat.
+Proof.
+  intros c b c0; destruct (cn_eqdec (get_code_nature c) IsLabel).
+  - intros; exploit to_bblock_header_wf; eauto; omega.
+  - intros; exploit to_bblock_header_eq; eauto. intros; subst; auto.
+Qed.
+
+Lemma to_bblock_body_eq:
+  forall c b c0,
+  get_code_nature c <> IsBasicInst ->
+  to_bblock_body c = (b, c0) ->
+  c = c0.
+Proof.
+  intros. destruct c.
+  - simpl in H0. inversion H0. auto.
+  - destruct i; simpl in *; try Discriminate || inversion H0; subst; auto.
+Qed.
+
+Lemma to_bblock_body_wfe:
+  forall c b c0,
+  to_bblock_body c = (b, c0) ->
+  (length c >= length c0)%nat.
+Proof.
+  induction c.
+  - intros. simpl in H. inversion H. subst. auto.
+  - intros. simpl in H. destruct (to_basic_inst a).
+    + remember (to_bblock_body c) as tbbc. destruct tbbc as [p c''].
+      exploit (IHc p c''); auto. inversion H. subst. simpl. omega.
+    + inversion H; subst; auto.
+Qed.
+
+
+Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop :=
+  Cons_to_bbloc_body i bi c' b': 
+    to_basic_inst i = Some bi
+    -> to_bblock_body c' = (b', c0)
+    -> cons_to_bblock_body c0 (i::c') (bi::b').
+
+Lemma to_bblock_body_IsBasicInst: 
+  forall c b c0, 
+  get_code_nature c = IsBasicInst ->
+  to_bblock_body c = (b, c0) -> 
+  cons_to_bblock_body c0 c b.
+Proof.
+  intros. destruct c; [ contradict H; simpl; discriminate | ].
+  remember (to_basic_inst i) as tbii. destruct tbii.
+  - simpl in H0. rewrite <- Heqtbii in H0.
+    remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1].
+    inversion H0. subst. eapply Cons_to_bbloc_body; eauto.
+  - destruct i; try discriminate.
+Qed.
+
+Lemma to_bblock_body_wf: 
+  forall c b c0, 
+  get_code_nature c = IsBasicInst ->
+  to_bblock_body c = (b, c0) -> 
+  (length c > length c0)%nat.
+Proof.
+  intros; exploit to_bblock_body_IsBasicInst; eauto.
+  intros H1; destruct H1.
+  exploit to_bblock_body_wfe; eauto.
+  simpl; omega.
+Qed.
+
+Lemma to_bblock_exit_eq:
+  forall c b c0,
+  get_code_nature c <> IsCFI ->
+  to_bblock_exit c = (b, c0) ->
+  c = c0.
+Proof.
+  intros. destruct c.
+  - simpl in H0; inversion H0; auto.
+  - destruct i; unfold to_bblock_header in H0; inversion H0; auto;
+    simpl in H; contradict H; auto.
+Qed.
+
+Lemma to_bblock_exit_wf:
+  forall c b c0,
+  get_code_nature c = IsCFI ->
+  to_bblock_exit c = (b, c0) ->
+  (length c > length c0)%nat.
+Proof.
+  intros. destruct c; try discriminate.
+  destruct i; try discriminate;
+  unfold to_bblock_header in H0; inversion H0; auto.
+Qed.
+
+Ltac ExploitExitEq := 
+  match goal with
+  | [ H: to_bblock_exit (?i0 :: ?c) = (?b, ?c0) |- _ ] =>
+      exploit (to_bblock_exit_eq (i0::c) b c0); [subst; simpl; discriminate | auto | intro; subst; auto]
+  | _ => idtac
+  end.
+
+Lemma to_bblock_exit_wfe:
+  forall c b c0,
+  to_bblock_exit c = (b, c0) ->
+  (length c >= length c0)%nat.
+Proof.
+  intros. destruct c. unfold to_bblock_exit in H; inversion H; auto.
+  remember i as i0.
+  destruct i; try ExploitExitEq.
+  all: exploit (to_bblock_exit_wf (i0::c) b c0); [subst; simpl; auto | auto | try omega].
+Qed.
+
+Definition to_bblock(c: Mach.code): bblock * Mach.code :=
+  let (h,c0) := to_bblock_header c in
+  let (bdy, c1) := to_bblock_body c0 in
+  let (ext, c2) := to_bblock_exit c1 in
+  ({| header := h; body := bdy; exit := ext |}, c2)
+  .
+
+Lemma to_bblock_double_label:
+  forall c l,
+  get_code_nature c = IsLabel ->
+  to_bblock (Mlabel l :: c) = ({| header := Some l; body := nil; exit := None |}, c).
+Proof.
+  intros.
+  destruct c; try (contradict H; simpl; discriminate).
+  destruct i; try (contradict H; simpl; discriminate).
+  simpl. auto.
+Qed.
+
+Lemma to_bblock_basic_inst_then_label:
+  forall i c bi,
+  get_code_nature (i::c) = IsBasicInst ->
+  get_code_nature c = IsLabel ->
+  to_basic_inst i = Some bi ->
+  fst (to_bblock (i::c)) = {| header := None; body := bi::nil; exit := None |}.
+Proof.
+  intros.
+  destruct c; try (contradict H; simpl; discriminate).
+  destruct i0; try (contradict H; simpl; discriminate).
+  destruct i; simpl in *; inversion H1; subst; auto.
+Qed.
+
+Lemma to_bblock_cf_inst_then_label:
+  forall i c cfi,
+  get_code_nature (i::c) = IsCFI ->
+  get_code_nature c = IsLabel ->
+  to_cfi i = Some cfi ->
+  fst (to_bblock (i::c)) = {| header := None; body := nil; exit := Some cfi |}.
+Proof.
+  intros.
+  destruct c; try (contradict H; simpl; discriminate).
+  destruct i0; try (contradict H; simpl; discriminate).
+  destruct i; simpl in *; inversion H1; subst; auto.
+Qed.
+
+Lemma to_bblock_single_label:
+  forall c l,
+  get_code_nature c <> IsLabel ->
+  fst (to_bblock (Mlabel l :: c)) = {|
+    header := Some l;
+    body := body (fst (to_bblock c));
+    exit := exit (fst (to_bblock c))
+  |}.
+Proof.
+  intros.
+  destruct c; simpl; auto.
+  apply bblock_eq; simpl.
+(* header *)
+  + destruct i; try (
+      remember (to_bblock _) as bb;
+      unfold to_bblock in *;
+      remember (to_bblock_header _) as tbh;
+      destruct tbh;
+      destruct (to_bblock_body _);
+      destruct (to_bblock_exit _);
+      subst; simpl; inversion Heqtbh; auto; fail
+      ).
+(* body *)
+  + remember i as i0; destruct i0; try (
+      remember (to_bblock _) as bb;
+      unfold to_bblock in *;
+      remember (to_bblock_header _) as tbh; rewrite Heqi0;
+      remember (to_bblock_header (i :: _)) as tbh'; rewrite <- Heqi0 in *;
+      destruct tbh; destruct tbh';
+      inversion Heqtbh; inversion Heqtbh'; subst;
+      destruct (to_bblock_body _);
+      destruct (to_bblock_exit _); auto; fail
+      ). contradict H; simpl; auto.
+(* exit (same proof as body) *)
+  + remember i as i0; destruct i0; try (
+      remember (to_bblock _) as bb;
+      unfold to_bblock in *;
+      remember (to_bblock_header _) as tbh; rewrite Heqi0;
+      remember (to_bblock_header (i :: _)) as tbh'; rewrite <- Heqi0 in *;
+      destruct tbh; destruct tbh';
+      inversion Heqtbh; inversion Heqtbh'; subst;
+      destruct (to_bblock_body _);
+      destruct (to_bblock_exit _); auto; fail
+      ). contradict H; simpl; auto.
+Qed.
+
+Lemma to_bblock_no_label:
+  forall c,
+  get_code_nature c <> IsLabel ->
+  fst (to_bblock c) = {|
+    header := None;
+    body := body (fst (to_bblock c));
+    exit := exit (fst (to_bblock c))
+  |}.
+Proof.
+  intros.
+  destruct c; simpl; auto.
+  apply bblock_eq; simpl;
+  destruct i; (
+      try (
+        remember (to_bblock _) as bb;
+        unfold to_bblock in *;
+        remember (to_bblock_header _) as tbh;
+        destruct tbh;
+        destruct (to_bblock_body _);
+        destruct (to_bblock_exit _);
+        subst; simpl; inversion Heqtbh; auto; fail
+      )
+    || contradict H; simpl; auto ).
+Qed.
+
+Lemma to_bblock_body_nil c c':
+  to_bblock_body c = (nil, c') ->
+  c = c'.
+Proof.
+  intros H.
+  destruct c; [ simpl in *; inversion H; auto |].
+  destruct i; try ( simpl in *; remember (to_bblock_body c) as tbc; destruct tbc as [p c'']; inversion H ).
+  all: auto.
+Qed.
+
+Lemma to_bblock_exit_nil c c':
+  to_bblock_exit c = (None, c') ->
+  c = c'.
+Proof.
+  intros H.
+  destruct c; [ simpl in *; inversion H; auto |].
+  destruct i; try ( simpl in *; remember (to_bblock_exit c) as tbe; destruct tbe as [p c'']; inversion H ).
+  all: auto.
+Qed.
+
+Lemma to_bblock_label b l c c':
+  to_bblock (Mlabel l :: c) = (b, c') ->
+  exists bdy c1, to_bblock_body c = (bdy, c1) /\
+  header b = Some l /\ body b = bdy /\ exit b = fst (to_bblock_exit c1).
+Proof.
+  intros H. 
+  (* destruct b as [bhd bbd bex]. simpl. *)
+  unfold to_bblock in H; simpl in H.
+  remember (to_bblock_body c) as tbbc; destruct tbbc as [bdy' c1'].
+  remember (to_bblock_exit c1') as tbbe; destruct tbbe as [ext c2].
+  esplit; eauto. esplit; eauto. esplit; eauto.
+  inversion H; subst; clear H. simpl.
+  apply (f_equal fst) in Heqtbbe. simpl in Heqtbbe. auto.
+Qed.
+
+Lemma to_bblock_label_then_nil b l c c':
+  to_bblock (Mlabel l :: c) = (b, c') ->
+  body b = nil ->
+  exit b = None ->
+  c = c'.
+Proof.
+  intros TOB BB EB.
+  unfold to_bblock in TOB.
+  remember (to_bblock_header _) as tbh; destruct tbh as [h c0].
+  remember (to_bblock_body _) as tbb; destruct tbb as [bdy c1].
+  remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2].
+  inversion TOB; subst. simpl in *. clear TOB.
+  inversion Heqtbh; subst. clear Heqtbh.
+  exploit to_bblock_body_nil; eauto. intros; subst. clear Heqtbb.
+  exploit to_bblock_exit_nil; eauto.
+Qed.
+
+Lemma to_bblock_basic_inst:
+  forall c i bi,
+  get_code_nature (i::c) = IsBasicInst ->
+  to_basic_inst i = Some bi ->
+  get_code_nature c <> IsLabel ->
+  fst (to_bblock (i::c)) = {|
+    header := None;
+    body := bi :: body (fst (to_bblock c));
+    exit := exit (fst (to_bblock c))
+  |}.
+Proof.
+  intros.
+  destruct c; try (destruct i; inversion H0; subst; simpl; auto; fail).
+  apply bblock_eq; simpl.
+(* header *)
+  + destruct i; simpl; auto; (
+      exploit to_bblock_no_label; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]).
+(* body *)
+(* FIXME - the proof takes some time to prove.. N² complexity :( *)
+  + destruct i; inversion H0; try (
+      destruct i0; try (
+        subst; unfold to_bblock;
+        remember (to_bblock_header _) as tbh; destruct tbh;
+        remember (to_bblock_header (_::c)) as tbh'; destruct tbh';
+        inversion Heqtbh; inversion Heqtbh'; subst;
+
+        remember (to_bblock_body _) as tbb; destruct tbb;
+        remember (to_bblock_body (_::c)) as tbb'; destruct tbb';
+        inversion Heqtbb; inversion Heqtbb'; destruct (to_bblock_body c);
+        inversion H3; inversion H4; subst;
+
+        remember (to_bblock_exit _) as tbc; destruct tbc;
+        simpl; auto );
+      contradict H1; simpl; auto ).
+(* exit - same as body *)
+  + destruct i; inversion H0; try (
+      destruct i0; try (
+        subst; unfold to_bblock;
+        remember (to_bblock_header _) as tbh; destruct tbh;
+        remember (to_bblock_header (_::c)) as tbh'; destruct tbh';
+        inversion Heqtbh; inversion Heqtbh'; subst;
+
+        remember (to_bblock_body _) as tbb; destruct tbb;
+        remember (to_bblock_body (_::c)) as tbb'; destruct tbb';
+        inversion Heqtbb; inversion Heqtbb'; destruct (to_bblock_body c);
+        inversion H3; inversion H4; subst;
+
+        remember (to_bblock_exit _) as tbc; destruct tbc;
+        simpl; auto );
+      contradict H1; simpl; auto ).
+Qed.
+
+Lemma to_bblock_size_single_label:
+  forall c i,
+  get_code_nature (i::c) = IsLabel ->
+  get_code_nature c <> IsLabel ->
+  size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
+Proof.
+  intros.
+  destruct i; try (contradict H; simpl; discriminate).
+  destruct c; simpl; auto.
+  destruct i; try (
+    exploit to_bblock_single_label; eauto; intro; rewrite H1;
+    exploit to_bblock_no_label; eauto; intro; rewrite H2;
+    simpl; auto; fail ).
+  Unshelve. all: auto.
+Qed.
+
+Lemma to_bblock_size_label_neqz:
+  forall c,
+  get_code_nature c = IsLabel ->
+  size (fst (to_bblock c)) <> 0%nat.
+Proof.
+  intros. destruct c; try (contradict H; auto; simpl; discriminate).
+  destruct i; try (contradict H; simpl; discriminate).
+  destruct (get_code_nature c) eqn:gcnc.
+  (* Case gcnc is not IsLabel *)
+  all: try (rewrite to_bblock_size_single_label; auto; rewrite gcnc; discriminate).
+  (* Case gcnc is IsLabel *)
+  rewrite to_bblock_double_label; auto; unfold size; simpl; auto.
+Qed.
+
+Lemma to_bblock_size_basicinst_neqz:
+  forall c,
+  get_code_nature c = IsBasicInst ->
+  size (fst (to_bblock c)) <> 0%nat.
+Proof.
+  intros. destruct c; try (contradict H; auto; simpl; discriminate).
+  destruct i; try (contradict H; simpl; discriminate);
+  (
+    destruct (get_code_nature c) eqn:gcnc;
+    (* Case gcnc is not IsLabel *)
+    try (erewrite to_bblock_basic_inst; eauto; [
+        unfold size; simpl; auto
+      | simpl; auto
+      | rewrite gcnc; discriminate
+    ]);
+    erewrite to_bblock_basic_inst_then_label; eauto; [
+        unfold size; simpl; auto
+      | simpl; auto
+    ]
+  ).
+Qed.
+
+Lemma to_bblock_size_cfi_neqz:
+  forall c,
+  get_code_nature c = IsCFI ->
+  size (fst (to_bblock c)) <> 0%nat.
+Proof.
+  intros. destruct c; try (contradict H; auto; simpl; discriminate).
+  destruct i; discriminate.
+Qed.
+
+Lemma to_bblock_size_single_basicinst:
+  forall c i,
+  get_code_nature (i::c) = IsBasicInst ->
+  get_code_nature c <> IsLabel ->
+  size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))).
+Proof.
+  intros.
+  destruct i; try (contradict H; simpl; discriminate); try (
+    (exploit to_bblock_basic_inst; eauto);
+      [remember (to_basic_inst _) as tbi; destruct tbi; eauto |];
+    intro; rewrite H1; unfold size; simpl;
+    assert ((length_opt (header (fst (to_bblock c)))) = 0%nat);
+      exploit to_bblock_no_label; eauto; intro; rewrite H2; simpl; auto;
+    rewrite H2; auto
+  ).
+Qed.
+
+Lemma to_bblock_wf c b c0:
+  c <> nil -> 
+  to_bblock c = (b, c0) ->
+  (length c > length c0)%nat.
+Proof.
+  intro H; lapply (get_code_nature_nil c); eauto.
+  intro H'; remember (get_code_nature c) as gcn.
+  unfold to_bblock.
+  remember (to_bblock_header c) as p1; eauto.
+  destruct p1 as [h c1].
+  intro H0.
+  destruct gcn. 
+  - contradict H'; auto.
+  - exploit to_bblock_header_wf; eauto.
+    remember (to_bblock_body c1) as p2; eauto.
+    destruct p2 as [h2 c2].
+    exploit to_bblock_body_wfe; eauto.
+    remember (to_bblock_exit c2) as p3; eauto.
+    destruct p3 as [h3 c3].
+    exploit to_bblock_exit_wfe; eauto.
+    inversion H0. omega.
+  - exploit to_bblock_header_eq; eauto. rewrite <- Heqgcn. discriminate.
+    intro; subst.
+    remember (to_bblock_body c1) as p2; eauto.
+    destruct p2 as [h2 c2].
+    exploit to_bblock_body_wf; eauto.
+    remember (to_bblock_exit c2) as p3; eauto.
+    destruct p3 as [h3 c3].
+    exploit to_bblock_exit_wfe; eauto.
+    inversion H0. omega.
+  - exploit to_bblock_header_eq; eauto. rewrite <- Heqgcn. discriminate.
+    intro; subst.
+    remember (to_bblock_body c1) as p2; eauto.
+    destruct p2 as [h2 c2].
+    exploit (to_bblock_body_eq c1 h2 c2); eauto. rewrite <- Heqgcn. discriminate.
+    intro; subst.
+    remember (to_bblock_exit c2) as p3; eauto.
+    destruct p3 as [h3 c3].
+    exploit (to_bblock_exit_wf c2 h3 c3); eauto.
+    inversion H0. omega.
+Qed.
+
+Lemma to_bblock_nonil:
+  forall c i c0,
+  c = i :: c0 -> 
+  size (fst (to_bblock c)) <> 0%nat.
+Proof.
+  intros. remember (get_code_nature c) as gcnc. destruct gcnc.
+  - contradict Heqgcnc. subst. simpl. destruct i; discriminate.
+  - eapply to_bblock_size_label_neqz; auto.
+  - eapply to_bblock_size_basicinst_neqz; auto.
+  - eapply to_bblock_size_cfi_neqz; auto.
+Qed.
+
+Lemma to_bblock_islabel:
+  forall c l,
+  is_label l (fst (to_bblock (Mlabel l :: c))) = true.
+Proof.
+  intros. unfold to_bblock.
+  remember (to_bblock_header _) as tbh; destruct tbh as [h c0].
+  remember (to_bblock_body _) as tbc; destruct tbc as [bdy c1].
+  remember (to_bblock_exit _) as tbe; destruct tbe as [ext c2].
+  simpl. inversion Heqtbh. unfold is_label. simpl.
+  apply peq_true.
+Qed.
+
+Lemma body_fst_to_bblock_label:
+  forall l c,
+  body (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_body c).
+Proof.
+  intros. destruct c as [|i c']; simpl; auto.
+  destruct i; simpl; auto.
+  all: (
+    remember (to_bblock_body c') as tbbc; destruct tbbc as [tc c'']; simpl;
+    unfold to_bblock;
+    remember (to_bblock_header _) as tbh; destruct tbh as [h c0];
+    remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1];
+    remember (to_bblock_exit c1) as tbe; destruct tbe as [ext c2];
+    simpl; simpl in Heqtbh; inversion Heqtbh; subst c0;
+    simpl in Heqtbc; remember (to_bblock_body c') as tbc'; destruct tbc' as [tc' osef];
+    inversion Heqtbc; inversion Heqtbbc; auto
+  ).
+Qed.
+
+Lemma exit_fst_to_bblock_label:
+  forall c c' l,
+  snd (to_bblock_body c) = c' ->
+  exit (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_exit c').
+Proof.
+  intros. destruct c as [|i c]; [simpl in *; subst; auto |].
+  unfold to_bblock.
+  remember (to_bblock_header _) as tbh; destruct tbh as [h c0].
+  remember (to_bblock_body c0) as tbc; destruct tbc as [bdy c1].
+  remember (to_bblock_exit c1) as tbe; destruct tbe as [ext c2].
+  simpl in *. inversion Heqtbh; subst.
+  destruct (to_basic_inst i) eqn:TBI.
+  - remember (to_bblock_body c) as tbbc; destruct tbbc as [p c''].
+    simpl. simpl in Heqtbc. rewrite TBI in Heqtbc. rewrite <- Heqtbbc in Heqtbc.
+    inversion Heqtbc; subst. apply (f_equal fst) in Heqtbe; auto.
+  - simpl. simpl in Heqtbc. rewrite TBI in Heqtbc.
+    inversion Heqtbc; subst. clear Heqtbh Heqtbc. unfold to_bblock_exit in Heqtbe.
+    apply (f_equal fst) in Heqtbe; auto.
+Qed.
+
+Function trans_code (c: Mach.code) { measure length c }: code :=
+  match c with
+  | nil => nil
+  | _ => 
+     let (b, c0) := to_bblock c in
+     b::(trans_code c0)
+  end.
+Proof.
+  intros; eapply to_bblock_wf; eauto. discriminate.
+Qed.
+
+(*
+Functional Scheme trans_code_ind := Induction for trans_code Sort Prop.
+*)
+
+Definition hd_code (bc: code) := (hd {| header := None; body := nil; exit := None |} bc).
+
+Lemma trans_code_nonil:
+  forall c,
+  c <> nil -> trans_code c <> nil.
+Proof.
+  intros.
+  induction c, (trans_code c) using trans_code_ind; simpl; auto. discriminate.
+Qed.
+
+Lemma trans_code_step:
+  forall c b lb0 hb c1 bb c2 eb c3,
+  trans_code c = b :: lb0 ->
+  to_bblock_header c = (hb, c1) ->
+  to_bblock_body c1 = (bb, c2) ->
+  to_bblock_exit c2 = (eb, c3) ->
+  hb = header b /\ bb = body b /\ eb = exit b /\ trans_code c3 = lb0.
+Proof.
+  intros.
+  induction c, (trans_code c) using trans_code_ind. discriminate. clear IHc0.
+  subst. destruct _x as [|i c]; try (contradict y; auto; fail).
+  inversion H; subst. clear H. unfold to_bblock in e0.
+  remember (to_bblock_header (i::c)) as hd. destruct hd as [hb' c1'].
+  remember (to_bblock_body c1') as bd. destruct bd as [bb' c2'].
+  remember (to_bblock_exit c2') as be. destruct be as [eb' c3'].
+  inversion e0. simpl.
+  inversion H0. subst.
+  rewrite <- Heqbd in H1. inversion H1. subst.
+  rewrite <- Heqbe in H2. inversion H2. subst.
+  auto.
+Qed.
+
+Lemma trans_code_cfi:
+  forall i c cfi,
+  to_cfi i = Some cfi ->
+  trans_code (i :: c) = {| header := None ; body := nil ; exit := Some cfi |} :: trans_code c.
+Proof.
+  intros. rewrite trans_code_equation. remember (to_bblock _) as tb; destruct tb as [b c0].
+  destruct i; try (contradict H; discriminate).
+  all: unfold to_bblock in Heqtb; remember (to_bblock_header _) as tbh; destruct tbh as [h c0'];
+      remember (to_bblock_body c0') as tbb; destruct tbb as [bdy c1'];
+      remember (to_bblock_exit c1') as tbe; destruct tbe as [ext c2]; simpl in *;
+      inversion Heqtbh; subst; inversion Heqtbb; subst; inversion Heqtbe; subst;
+      inversion Heqtb; subst; rewrite H; auto.
+Qed.
+
+(* à finir pour passer des Mach.function au function, etc. *)
+Definition trans_function (f: Mach.function) : function :=
+  {| fn_sig:=Mach.fn_sig f; 
+     fn_code:=trans_code (Mach.fn_code f);
+     fn_stacksize := Mach.fn_stacksize f;
+     fn_link_ofs := Mach.fn_link_ofs f;
+     fn_retaddr_ofs := Mach.fn_retaddr_ofs f
+ |}.
+
+Definition trans_fundef (f: Mach.fundef) : fundef :=
+  transf_fundef trans_function f.
+
+Definition trans_prog (src: Mach.program) : program :=
+  transform_program trans_fundef src.