diff options
Diffstat (limited to 'mppa_k1c/Machblockgen.v')
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 693 |
1 files changed, 161 insertions, 532 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 1d5555df..4dfc309e 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -15,552 +15,77 @@ Require Import Mach. Require Import Linking. Require Import Machblock. +Inductive Machblock_inst: Type := +| MB_label (lbl: label) +| MB_basic (bi: basic_inst) +| MB_cfi (cfi: control_flow_inst). -Fixpoint to_bblock_header (c: Mach.code): list label * Mach.code := - match c with - | (Mlabel l)::c' => - let (h, c'') := to_bblock_header c' in - (l::h, c'') - | _ => (nil, c) - end. - -Definition to_basic_inst(i: Mach.instruction): option basic_inst := +Definition trans_inst (i:Mach.instruction) : Machblock_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 + | Mcall sig ros => MB_cfi (MBcall sig ros) + | Mtailcall sig ros => MB_cfi (MBtailcall sig ros) + | Mbuiltin ef args res => MB_cfi (MBbuiltin ef args res) + | Mgoto lbl => MB_cfi (MBgoto lbl) + | Mcond cond args lbl => MB_cfi (MBcond cond args lbl) + | Mjumptable arg tbl => MB_cfi (MBjumptable arg tbl) + | Mreturn => MB_cfi (MBreturn) + | Mgetstack ofs ty dst => MB_basic (MBgetstack ofs ty dst) + | Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty) + | Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst) + | Mop op args res => MB_basic (MBop op args res) + | Mload chunk addr args dst => MB_basic (MBload chunk addr args dst) + | Mstore chunk addr args src => MB_basic (MBstore chunk addr args src) + | Mlabel l => MB_label l end. -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 empty_bblock:={| header := nil; body := nil; exit := None |}. +Extraction Inline empty_bblock. +Definition add_label l bb:={| header := l::(header bb); body := (body bb); exit := (exit bb) |}. +Extraction Inline add_label. -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 add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}. +Extraction Inline add_basic. -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 cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}. +Extraction Inline cfi_bblock. -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 +Definition add_to_new_bblock (i:Machblock_inst) : bblock := + match i with + | MB_label l => add_label l empty_bblock + | MB_basic i => add_basic i empty_bblock + | MB_cfi i => cfi_bblock i 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. - intros H. unfold get_code_nature. - destruct c; try (contradict H; auto; fail). - destruct i; discriminate. -Qed. - -Lemma get_code_nature_empty c: get_code_nature c = IsEmpty -> c = nil. -Proof. - intros H. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto. - intro F. contradict F. -Qed. - -Lemma to_bblock_header_noLabel c: - get_code_nature c <> IsLabel -> - to_bblock_header c = (nil, c). -Proof. - intros H. destruct c as [|i c]; auto. - destruct i; simpl; auto. - contradict H; simpl; auto. -Qed. - -Lemma to_bblock_header_wfe c: - forall h c0, - to_bblock_header c = (h, c0) -> - (length c >= length c0)%nat. -Proof. - induction c as [ |i c]; simpl; intros h c' H. - - inversion H; subst; clear H; simpl; auto. - - destruct i; try (inversion H; subst; simpl; auto; fail). - remember (to_bblock_header c) as bhc; destruct bhc as [h0 c0]. - inversion H; subst. - lapply (IHc h0 c'); auto. -Qed. - -Lemma to_bblock_header_wf c b c0: - get_code_nature c = IsLabel -> - to_bblock_header c = (b, c0) -> - (length c > length c0)%nat. -Proof. - intros H1 H2; destruct c; [ contradict H1; simpl; discriminate | ]. - destruct i; try discriminate. - simpl in H2. - remember (to_bblock_header c) as bh; destruct bh as [h c'']. - inversion H2; subst. - exploit to_bblock_header_wfe; eauto. - simpl; omega. -Qed. - -Lemma to_bblock_body_noBasic c: - get_code_nature c <> IsBasicInst -> - to_bblock_body c = (nil, c). -Proof. - intros H. destruct c as [|i c]; simpl; auto. - destruct i; simpl; auto. - all: contradict H; simpl; auto. -Qed. - -Lemma to_bblock_body_wfe c b c0: - to_bblock_body c = (b, c0) -> - (length c >= length c0)%nat. -Proof. - generalize b c0; clear b c0. - induction c as [|i c]. - - intros b c0 H. simpl in H. inversion H; subst; auto. - - intros b c0 H. simpl in H. destruct (to_basic_inst i). - + 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. - -(** Attempt to eliminate cons_to_bblock_body *) -(* -Lemma to_bblock_body_basic c: - get_code_nature c = IsBasicInst -> - exists i bi b c', - to_basic_inst i = Some bi - /\ c = i :: c' - /\ to_bblock_body c = (bi::b, snd (to_bblock_body c')). -Proof. - intros H. - destruct c as [|i c]; try (contradict H; simpl; discriminate). - destruct i eqn:I; try (contradict H; simpl; discriminate). - all: simpl; destruct (to_bblock_body c) as [p c''] eqn:TBBC; repeat (eapply ex_intro); (repeat split); - simpl; eauto; rewrite TBBC; simpl; eauto. -Qed. - -Lemma to_bblock_body_wf c b c0: - get_code_nature c = IsBasicInst -> - to_bblock_body c = (b, c0) -> - (length c > length c0)%nat. -Proof. - intros H1 H2; exploit to_bblock_body_basic; eauto. - intros X. destruct X as (i & bi & b' & c' & X1 & X2 & X3). - exploit to_bblock_body_wfe. eauto. subst. simpl. - rewrite X3 in H2. inversion H2; clear H2; subst. - simpl; omega. -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 c b c0: - get_code_nature c = IsBasicInst -> - to_bblock_body c = (b, c0) -> - cons_to_bblock_body c0 c b. -Proof. - intros H1 H2. destruct c; [ contradict H1; simpl; discriminate | ]. - remember (to_basic_inst i) as tbii. destruct tbii. - - simpl in H2. rewrite <- Heqtbii in H2. - remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1]. - inversion H2. subst. eapply Cons_to_bbloc_body; eauto. - - destruct i; try discriminate. -Qed. - -Lemma to_bblock_body_wf c b c0: - get_code_nature c = IsBasicInst -> - to_bblock_body c = (b, c0) -> - (length c > length c0)%nat. -Proof. - intros H1 H2; exploit to_bblock_body_IsBasicInst; eauto. - intros X. destruct X. - exploit to_bblock_body_wfe; eauto. subst. simpl. - simpl; omega. -Qed. - -Lemma to_bblock_exit_noCFI c: - get_code_nature c <> IsCFI -> - to_bblock_exit c = (None, c). -Proof. - intros H. destruct c as [|i c]; simpl; auto. - destruct i; simpl; auto. - all: contradict H; simpl; auto. -Qed. - -Lemma to_bblock_exit_wf c b c0: - get_code_nature c = IsCFI -> - to_bblock_exit c = (b, c0) -> - (length c > length c0)%nat. -Proof. - intros H1 H2. destruct c as [|i c]; try discriminate. - destruct i; try discriminate; - unfold to_bblock_header in H2; inversion H2; auto. -Qed. - -Lemma to_bblock_exit_wfe c b c0: - to_bblock_exit c = (b, c0) -> - (length c >= length c0)%nat. -Proof. - intros H. destruct c as [|i c]. - - simpl in H. inversion H; subst; clear H; auto. - - destruct i; try ( simpl in H; inversion H; subst; clear H; auto ). - all: simpl; auto. -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_acc_label c l b c': - to_bblock c = (b, c') -> - to_bblock (Mlabel l :: c) = ({| header := l::(header b); body := (body b); exit := (exit b) |}, c'). -Proof. - unfold to_bblock; simpl. - remember (to_bblock_header c) as bhc; destruct bhc as [h c0]. - remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1]. - remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2]. - intros H; inversion H; subst; clear H; simpl; auto. -Qed. - -Lemma to_bblock_basic_then_label 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 := nil; body := bi::nil; exit := None |}. -Proof. - intros H1 H2 H3. - destruct c as [|i' c]; try (contradict H1; simpl; discriminate). - destruct i'; try (contradict H1; simpl; discriminate). - destruct i; simpl in *; inversion H3; subst; auto. -Qed. - -Lemma to_bblock_CFI i c cfi: - get_code_nature (i::c) = IsCFI -> - to_cfi i = Some cfi -> - fst (to_bblock (i::c)) = {| header := nil; body := nil; exit := Some cfi |}. -Proof. - intros H1 H2. - destruct i; try discriminate. - all: subst; rewrite <- H2; simpl; auto. -Qed. - -Lemma to_bblock_noLabel c: - get_code_nature c <> IsLabel -> - fst (to_bblock c) = {| - header := nil; - body := body (fst (to_bblock c)); - exit := exit (fst (to_bblock c)) - |}. -Proof. - intros H. - destruct c as [|i 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 as [|i 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 as [|i 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') -> - (header b) = l::(tail (header b)) /\ to_bblock c = ({| header:=tail (header b); body := body b; exit := exit b |}, c'). -Proof. - unfold to_bblock; simpl. - remember (to_bblock_header c) as bhc; destruct bhc as [h c0]. - remember (to_bblock_body c0) as bbc; destruct bbc as [bdy c1]. - remember (to_bblock_exit c1) as bbc; destruct bbc as [ext c2]. - intros H; inversion H; subst; clear H; simpl; auto. -Qed. - -Lemma to_bblock_basic 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 := nil; - 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_noLabel; [rewrite H; discriminate | intro; rewrite H2; simpl; auto]). -(* body *) -(* FIXME - the proof takes some time to prove.. N² complexity :( *) - + unfold to_bblock. - remember (to_bblock_header _) as tbh; destruct tbh. - remember (to_bblock_body _) as tbb; destruct tbb. - remember (to_bblock_exit _) as tbe; destruct tbe. - simpl. - destruct i; destruct i0. - all: try (simpl in H1; contradiction). - all: try discriminate. - all: try ( - simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst; - simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc; - inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1; - inversion H0; clear H0; subst; destruct (to_bblock_body c); - inversion Heqtbbc; clear Heqtbbc; subst; - destruct (to_bblock_exit c1); simpl; auto; fail). -(* exit *) - + unfold to_bblock. - remember (to_bblock_header _) as tbh; destruct tbh. - remember (to_bblock_body _) as tbb; destruct tbb. - remember (to_bblock_exit _) as tbe; destruct tbe. - simpl. - destruct i; destruct i0. - all: try (simpl in H1; contradiction). - all: try discriminate. - all: try ( - simpl in Heqtbh; inversion Heqtbh; clear Heqtbh; subst; - simpl in Heqtbb; remember (to_bblock_body c) as tbbc; destruct tbbc; - inversion Heqtbb; clear Heqtbb; subst; simpl in *; clear H H1; - inversion H0; clear H0; subst; destruct (to_bblock_body c) eqn:TBBC; - inversion Heqtbbc; clear Heqtbbc; subst; - destruct (to_bblock_exit c1) eqn:TBBE; simpl; - inversion Heqtbe; clear Heqtbe; subst; auto; fail). -Qed. - -Lemma to_bblock_size_single_label c i: - get_code_nature (i::c) = IsLabel -> - size (fst (to_bblock (i::c))) = Datatypes.S (size (fst (to_bblock c))). -Proof. - intros H. - destruct i; try discriminate. - remember (to_bblock c) as bl. destruct bl as [b c']. - erewrite to_bblock_acc_label; eauto. - unfold size; simpl. - auto. -Qed. - -Lemma to_bblock_size_label_neqz c: - get_code_nature c = IsLabel -> - size (fst (to_bblock c)) <> 0%nat. -Proof. - destruct c as [ |i c]; try discriminate. - intros; rewrite to_bblock_size_single_label; auto. -Qed. - -Lemma to_bblock_size_basic_neqz c: - get_code_nature c = IsBasicInst -> - size (fst (to_bblock c)) <> 0%nat. -Proof. - intros H. destruct c as [|i 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; eauto; [ - unfold size; simpl; auto - | simpl; auto - | rewrite gcnc; discriminate - ]); - erewrite to_bblock_basic_then_label; eauto; [ - unfold size; simpl; auto - | simpl; auto - ] - ). -Qed. - -Lemma to_bblock_size_cfi_neqz c: - get_code_nature c = IsCFI -> - size (fst (to_bblock c)) <> 0%nat. -Proof. - intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate). - destruct i; discriminate. -Qed. - -Lemma to_bblock_size_single_basic 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; eauto); - [remember (to_basic_inst _) as tbi; destruct tbi; eauto |]; - intro; rewrite H1; unfold size; simpl; - assert ((length (header (fst (to_bblock c)))) = 0%nat); - exploit to_bblock_noLabel; 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_noLabel; eauto. rewrite <- Heqgcn. discriminate. - intro. rewrite H1 in Heqp1. inversion Heqp1. clear Heqp1. subst. - remember (to_bblock_body c) 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_noLabel; eauto. rewrite <- Heqgcn. discriminate. - intro. rewrite H1 in Heqp1. inversion Heqp1; clear Heqp1; subst. - remember (to_bblock_body c) as p2; eauto. - destruct p2 as [h2 c2]. - exploit (to_bblock_body_noBasic c); eauto. rewrite <- Heqgcn. discriminate. - intros H2; rewrite H2 in Heqp2; inversion Heqp2; clear Heqp2; subst. - remember (to_bblock_exit c) as p3; eauto. - destruct p3 as [h3 c3]. - exploit (to_bblock_exit_wf c h3 c3); eauto. - inversion H0. omega. -Qed. - -Lemma to_bblock_nonil i c0: - size (fst (to_bblock (i :: c0))) <> 0%nat. -Proof. - intros H. remember (i::c0) as c. remember (get_code_nature c) as gcnc. destruct gcnc. - - contradict Heqgcnc. subst. simpl. destruct i; discriminate. - - eapply to_bblock_size_label_neqz; eauto. - - eapply to_bblock_size_basic_neqz; eauto. - - eapply to_bblock_size_cfi_neqz; eauto. -Qed. - -Function trans_code (c: Mach.code) { measure length c }: code := +(* ajout d'une instruction en début d'une liste de blocks *) +(* Soit /1\ ajout en tête de block, soit /2\ ajout dans un nouveau block*) +(* bl est vide -> /2\ *) +(* cfi -> /2\ (ajout dans exit)*) +(* basic -> /1\ si header vide, /2\ si a un header *) +(* label -> /1\ (dans header)*) +Definition add_to_code (i:Machblock_inst) (bl:code) : code := + match bl with + | bh::bl0 => match i with + | MB_label l => add_label l bh::bl0 + | MB_cfi i0 => cfi_bblock i0::bl + | MB_basic i0 => match header bh with + |_::_ => add_basic i0 empty_bblock::bl + | nil => add_basic i0 bh::bl0 + end + end + | _ => add_to_new_bblock i::nil + end. + +Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := match c with - | nil => nil - | _ => - let (b, c0) := to_bblock c in - b::(trans_code c0) + | nil => bl + | i::c0 => + trans_code_rev c0 (add_to_code (trans_inst i) bl) end. -Proof. - intros; eapply to_bblock_wf; eauto. discriminate. -Qed. - -Lemma trans_code_nonil c: - c <> nil -> trans_code c <> nil. -Proof. - intros H. - induction c, (trans_code c) using trans_code_ind; simpl; auto. discriminate. -Qed. -Lemma trans_code_step 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. +Function trans_code (c: Mach.code) : code := + trans_code_rev (List.rev_append c nil) nil. -Lemma trans_code_cfi i c cfi: - to_cfi i = Some cfi -> - trans_code (i :: c) = {| header := nil ; 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 transf_function (f: Mach.function) : function := @@ -576,3 +101,107 @@ Definition transf_fundef (f: Mach.fundef) : fundef := Definition transf_program (src: Mach.program) : program := transform_program transf_fundef src. + + +(** Abstraction de trans_code *) + +Inductive is_end_block: Machblock_inst -> code -> Prop := + | End_empty mbi: is_end_block mbi nil + | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl) + | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. + +Local Hint Resolve End_empty End_basic End_cfi. + +Inductive is_trans_code: Mach.code -> code -> Prop := + | Tr_nil: is_trans_code nil nil + | Tr_end_block i c bl: + is_trans_code c bl -> + is_end_block (trans_inst i) bl -> + is_trans_code (i::c) (add_to_new_bblock (trans_inst i)::bl) + | Tr_add_label i l bh c bl: + is_trans_code c (bh::bl) -> + i = Mlabel l -> + is_trans_code (i::c) (add_label l bh::bl) + | Tr_add_basic i bi bh c bl: + is_trans_code c (bh::bl) -> + trans_inst i = MB_basic bi -> + header bh = nil -> + is_trans_code (i::c) (add_basic bi bh::bl). + +Local Hint Resolve Tr_nil Tr_end_block. + +Lemma add_to_code_is_trans_code i c bl: + is_trans_code c bl -> + is_trans_code (i::c) (add_to_code (trans_inst i) bl). +Proof. + destruct bl as [|bh0 bl]; simpl. + - intro H. inversion H. subst. eauto. + - remember (trans_inst i) as ti. + destruct ti as [l|bi|cfi]. + + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence. + + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. + * eapply Tr_add_basic; eauto. + * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. + rewrite Heqti; eapply Tr_end_block; eauto. + rewrite <- Heqti. eapply End_basic. congruence. + + intros. + cutrewrite (cfi_bblock cfi = add_to_new_bblock (MB_cfi cfi)); auto. + rewrite Heqti. eapply Tr_end_block; eauto. + rewrite <- Heqti. eapply End_cfi. congruence. +Qed. + +Local Hint Resolve add_to_code_is_trans_code. + +Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, + is_trans_code c2 mbi -> + is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi). +Proof. + induction c1 as [| i c1]; simpl; auto. +Qed. + +Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c). +Proof. + unfold trans_code. + rewrite <- rev_alt. + rewrite <- (rev_involutive c) at 1. + rewrite rev_alt at 1. + apply trans_code_is_trans_code_rev; auto. +Qed. + +Lemma add_to_code_is_trans_code_inv i c bl: + is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0. +Proof. + intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto. + + (* case Tr_end_block *) inversion H3; subst; simpl; auto. + * destruct (header bh); congruence. + * destruct bl0; simpl; congruence. + + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence. +Qed. + +Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, + is_trans_code (rev_append c1 c2) mbi -> + exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0. +Proof. + induction c1 as [| i c1]; simpl; eauto. + intros; exploit IHc1; eauto. + intros (mbi0 & H1 & H2); subst. + exploit add_to_code_is_trans_code_inv; eauto. + intros. destruct H0 as [mbi1 [H2 H3]]. + exists mbi1. split; congruence. +Qed. + +Local Hint Resolve trans_code_is_trans_code. + +Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c). +Proof. + constructor; intros; subst; auto. + unfold trans_code. + exploit (trans_code_is_trans_code_rev_inv (rev_append c nil) nil bl); eauto. + * rewrite <- rev_alt. + rewrite <- rev_alt. + rewrite (rev_involutive c). + apply H. + * intros. + destruct H0 as [mbi [H0 H1]]. + inversion H0. subst. reflexivity. +Qed. |