From 7dca5905e7921b72634c31ae8de1bd08b3ff2e2e Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 26 Jun 2018 14:09:33 +0200 Subject: Machblock: some cleaning --- lib/Coqlib.v | 7 -- mppa_k1c/Machblock.v | 11 +- mppa_k1c/Machblockgen.v | 281 +++++++++++++++++-------------------------- mppa_k1c/Machblockgenproof.v | 50 ++++---- 4 files changed, 146 insertions(+), 203 deletions(-) diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 86bfa248..3fe1ea2e 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -90,13 +90,6 @@ Ltac exploit x := || refine (modusponens _ _ (x _ _) _) || refine (modusponens _ _ (x _) _). -Ltac totologize H := - match type of H with - | ( ?id = _ ) => - let Hassert := fresh "Htoto" in ( - assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert) - end. - (** * Definitions and theorems over the type [positive] *) Definition peq: forall (x y: positive), {x = y} + {x <> y} := Pos.eq_dec. diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v index 9b36fc43..6d28844b 100644 --- a/mppa_k1c/Machblock.v +++ b/mppa_k1c/Machblock.v @@ -55,7 +55,7 @@ Proof. Qed. Definition length_opt {A} (o: option A) : nat := - match o with + match o with | Some o => 1 | None => 0 end. @@ -110,10 +110,11 @@ Qed. Local Open Scope nat_scope. +(* FIXME - avoir une définition un peu plus simple, au prix de la preuve Mach -> Machblock ? *) Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := match c with | nil => None - | bb1 :: bbl => if is_label lbl bb1 + | bb1 :: bbl => if is_label lbl bb1 then let bb' := {| header := None ; body := body bb1 ; exit := exit bb1 |} in ( Some (match size bb' with | O => bbl @@ -191,7 +192,7 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m: | exec_MBsetstack: forall src ofs ty m' rs', store_stack m sp ty ofs (rs src) = Some m' -> - rs' = undef_regs (destroyed_by_setstack ty) rs -> + rs' = undef_regs (destroyed_by_setstack ty) rs -> basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m' | exec_MBgetparam: forall ofs ty dst v rs' f, @@ -225,8 +226,8 @@ Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> re forall rs m, body_step s f sp nil rs m rs m | exec_cons_body: - forall rs m bi p rs' m' rs'' m'', - basic_step s f sp rs m bi rs' m' -> + forall rs m bi p rs' m' rs'' m'', + basic_step s f sp rs m bi rs' m' -> body_step s f sp p rs' m' rs'' m'' -> body_step s f sp (bi::p) rs m rs'' m'' . diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 93284b0b..039e6c6e 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -26,14 +26,13 @@ Definition to_basic_inst(i: Mach.instruction): option basic_inst := | _ => 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' => + | i::c' => match to_basic_inst i with - | Some bi => - let (p,c'') := to_bblock_body c' in + | Some bi => + let (p,c'') := to_bblock_body c' in (bi::p, c'') | None => (nil, c) end @@ -61,7 +60,7 @@ Definition to_cfi (i: Mach.instruction): option control_flow_inst := Definition to_bblock_exit (c: Mach.code): option control_flow_inst * Mach.code := match c with | nil => (None,nil) - | i::c' => + | i::c' => match to_cfi i with | Some bi as o => (o, c') | None => (None, c) @@ -80,195 +79,162 @@ Definition get_code_nature (c: Mach.code): code_nature := 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. +Qed. Lemma get_code_nature_nil c: c<>nil -> get_code_nature c <> IsEmpty. Proof. - intro. unfold get_code_nature. destruct c; try Discriminate. + intros H. unfold get_code_nature. + destruct c; try (contradict H; auto; fail). 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. + intros H. destruct c; auto. exploit (get_code_nature_nil (i::c)); discriminate || auto. + intro F. contradict F. Qed. -Lemma get_code_nature_basic_inst: - forall c a c0, +Lemma get_code_nature_basic_inst 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. + intros H1 H2. destruct a; discriminate || contradict H2; subst; simpl; discriminate. Qed. -Lemma to_bblock_header_not_IsLabel: - forall c b c0, +Lemma to_bblock_header_not_IsLabel 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. + intros H1 H2. destruct c. + - simpl in H2; inversion H2; auto. + - destruct i; unfold to_bblock_header in H2; inversion H2; auto. + simpl in H1; contradict H1; auto. Qed. - -Lemma to_bblock_header_eq: - forall c b c0, +Lemma to_bblock_header_eq 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. + intros H1 H2; exploit to_bblock_header_not_IsLabel; intuition eauto. Qed. -Lemma to_bblock_header_IsLabel: - forall c c0 b, - get_code_nature c = IsLabel -> +Lemma to_bblock_header_IsLabel 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. + intros H1 H2. destruct c; try discriminate. destruct i; try discriminate. - unfold to_bblock_header in H0; inversion H0; eauto. + unfold to_bblock_header in H2; inversion H2; eauto. Qed. -Lemma to_bblock_header_wf: - forall c b c0, - get_code_nature c = IsLabel -> +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; exploit to_bblock_header_IsLabel; eauto. - intros [l H1]; subst; simpl; auto. + intros H1 H2; exploit to_bblock_header_IsLabel; eauto. + intros [l X]; 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, +Lemma to_bblock_header_wfe 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). + 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, +Lemma to_bblock_body_eq 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. + intros H1 H2. destruct c. + - simpl in H2. inversion H2. auto. + - destruct i; try ( simpl in *; destruct H1; auto; fail ). + all: simpl in *; inversion H2; subst; clear H2; auto. Qed. -Lemma to_bblock_body_wfe: - forall c b c0, +Lemma to_bblock_body_wfe 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. + 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. - Inductive cons_to_bblock_body c0: Mach.code -> bblock_body -> Prop := - Cons_to_bbloc_body i bi c' b': + 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, +Lemma to_bblock_body_IsBasicInst c b c0: get_code_nature c = IsBasicInst -> - to_bblock_body c = (b, c0) -> + to_bblock_body c = (b, c0) -> cons_to_bblock_body c0 c b. Proof. - intros. destruct c; [ contradict H; simpl; discriminate | ]. + intros H1 H2. destruct c; [ contradict H1; simpl; discriminate | ]. remember (to_basic_inst i) as tbii. destruct tbii. - - simpl in H0. rewrite <- Heqtbii in H0. + - simpl in H2. rewrite <- Heqtbii in H2. remember (to_bblock_body c) as tbbc. destruct tbbc as [p1 c1]. - inversion H0. subst. eapply Cons_to_bbloc_body; eauto. + inversion H2. subst. eapply Cons_to_bbloc_body; eauto. - destruct i; try discriminate. Qed. -Lemma to_bblock_body_wf: - forall c b c0, +Lemma to_bblock_body_wf c b c0: get_code_nature c = IsBasicInst -> - to_bblock_body c = (b, c0) -> + to_bblock_body c = (b, c0) -> (length c > length c0)%nat. Proof. - intros; exploit to_bblock_body_IsBasicInst; eauto. - intros H1; destruct H1. + intros H1 H2; exploit to_bblock_body_IsBasicInst; eauto. + intros X; destruct X. exploit to_bblock_body_wfe; eauto. simpl; omega. Qed. -Lemma to_bblock_exit_eq: - forall c b c0, +Lemma to_bblock_exit_eq 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. + intros H1 H2. destruct c as [|i c]. + - simpl in H2; inversion H2; auto. + - destruct i; unfold to_bblock_header in H2; inversion H2; auto; + simpl in H1; contradict H1; auto. Qed. -Lemma to_bblock_exit_wf: - forall c b c0, +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. destruct c; try discriminate. + intros H1 H2. destruct c as [|i c]; try discriminate. destruct i; try discriminate; - unfold to_bblock_header in H0; inversion H0; auto. + unfold to_bblock_header in H2; inversion H2; 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, +Lemma to_bblock_exit_wfe 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]. + 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 := @@ -278,45 +244,41 @@ Definition to_bblock(c: Mach.code): bblock * Mach.code := ({| header := h; body := bdy; exit := ext |}, c2) . -Lemma to_bblock_double_label: - forall c l, +Lemma to_bblock_double_label 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). + intros H. + destruct c as [|i c]; try (contradict H; simpl; discriminate). destruct i; try (contradict H; simpl; discriminate). - simpl. auto. + auto. Qed. -Lemma to_bblock_basic_inst_then_label: - forall i c bi, +Lemma to_bblock_basic_inst_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 := 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. + 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_cf_inst_then_label: - forall i c cfi, +Lemma to_bblock_cf_inst_then_label 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. + 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_single_label: - forall c l, +Lemma to_bblock_single_label c l: get_code_nature c <> IsLabel -> fst (to_bblock (Mlabel l :: c)) = {| header := Some l; @@ -324,8 +286,8 @@ Lemma to_bblock_single_label: exit := exit (fst (to_bblock c)) |}. Proof. - intros. - destruct c; simpl; auto. + intros H. + destruct c as [|i c]; simpl; auto. apply bblock_eq; simpl. (* header *) + destruct i; try ( @@ -361,8 +323,7 @@ Proof. ). contradict H; simpl; auto. Qed. -Lemma to_bblock_no_label: - forall c, +Lemma to_bblock_no_label c: get_code_nature c <> IsLabel -> fst (to_bblock c) = {| header := None; @@ -370,8 +331,8 @@ Lemma to_bblock_no_label: exit := exit (fst (to_bblock c)) |}. Proof. - intros. - destruct c; simpl; auto. + intros H. + destruct c as [|i c]; simpl; auto. apply bblock_eq; simpl; destruct i; ( try ( @@ -391,7 +352,7 @@ Lemma to_bblock_body_nil c c': c = c'. Proof. intros H. - destruct c; [ simpl in *; inversion H; auto |]. + 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. @@ -401,7 +362,7 @@ Lemma to_bblock_exit_nil c c': c = c'. Proof. intros H. - destruct c; [ simpl in *; inversion H; auto |]. + 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. @@ -411,8 +372,7 @@ Lemma to_bblock_label b l c 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. *) + intros H. 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]. @@ -438,8 +398,7 @@ Proof. exploit to_bblock_exit_nil; eauto. Qed. -Lemma to_bblock_basic_inst: - forall c i bi, +Lemma to_bblock_basic_inst c i bi: get_code_nature (i::c) = IsBasicInst -> to_basic_inst i = Some bi -> get_code_nature c <> IsLabel -> @@ -490,8 +449,7 @@ Proof. contradict H1; simpl; auto ). Qed. -Lemma to_bblock_size_single_label: - forall c i, +Lemma to_bblock_size_single_label 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))). @@ -506,12 +464,11 @@ Proof. Unshelve. all: auto. Qed. -Lemma to_bblock_size_label_neqz: - forall c, +Lemma to_bblock_size_label_neqz c: get_code_nature c = IsLabel -> size (fst (to_bblock c)) <> 0%nat. Proof. - intros. destruct c; try (contradict H; auto; simpl; discriminate). + 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 *) @@ -520,12 +477,11 @@ Proof. rewrite to_bblock_double_label; auto; unfold size; simpl; auto. Qed. -Lemma to_bblock_size_basicinst_neqz: - forall c, +Lemma to_bblock_size_basicinst_neqz c: get_code_nature c = IsBasicInst -> size (fst (to_bblock c)) <> 0%nat. Proof. - intros. destruct c; try (contradict H; auto; simpl; discriminate). + 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; @@ -542,17 +498,15 @@ Proof. ). Qed. -Lemma to_bblock_size_cfi_neqz: - forall c, +Lemma to_bblock_size_cfi_neqz c: get_code_nature c = IsCFI -> size (fst (to_bblock c)) <> 0%nat. Proof. - intros. destruct c; try (contradict H; auto; simpl; discriminate). + intros H. destruct c as [|i c]; try (contradict H; auto; simpl; discriminate). destruct i; discriminate. Qed. -Lemma to_bblock_size_single_basicinst: - forall c i, +Lemma to_bblock_size_single_basicinst 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))). @@ -569,7 +523,7 @@ Proof. Qed. Lemma to_bblock_wf c b c0: - c <> nil -> + c <> nil -> to_bblock c = (b, c0) -> (length c > length c0)%nat. Proof. @@ -579,7 +533,7 @@ Proof. remember (to_bblock_header c) as p1; eauto. destruct p1 as [h c1]. intro H0. - destruct gcn. + destruct gcn. - contradict H'; auto. - exploit to_bblock_header_wf; eauto. remember (to_bblock_body c1) as p2; eauto. @@ -610,23 +564,21 @@ Proof. inversion H0. omega. Qed. -Lemma to_bblock_nonil: - forall c i c0, - c = i :: c0 -> +Lemma to_bblock_nonil c i c0: + c = i :: c0 -> size (fst (to_bblock c)) <> 0%nat. Proof. - intros. remember (get_code_nature c) as gcnc. destruct gcnc. + intros H. 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, +Lemma to_bblock_islabel c l: is_label l (fst (to_bblock (Mlabel l :: c))) = true. Proof. - intros. unfold to_bblock. + 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]. @@ -634,11 +586,10 @@ Proof. apply peq_true. Qed. -Lemma body_fst_to_bblock_label: - forall l c, +Lemma body_fst_to_bblock_label l c: body (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_body c). Proof. - intros. destruct c as [|i c']; simpl; auto. + 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; @@ -652,12 +603,11 @@ Proof. ). Qed. -Lemma exit_fst_to_bblock_label: - forall c c' l, +Lemma exit_fst_to_bblock_label 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 |]. + intros H. 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]. @@ -675,7 +625,7 @@ 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. @@ -683,22 +633,16 @@ 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, +Lemma trans_code_nonil c: c <> nil -> trans_code c <> nil. Proof. - intros. + intros H. 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, +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) -> @@ -719,8 +663,7 @@ Proof. auto. Qed. -Lemma trans_code_cfi: - forall i c cfi, +Lemma trans_code_cfi i c cfi: to_cfi i = Some cfi -> trans_code (i :: c) = {| header := None ; body := nil ; exit := Some cfi |} :: trans_code c. Proof. @@ -735,7 +678,7 @@ Qed. (* à finir pour passer des Mach.function au function, etc. *) Definition trans_function (f: Mach.function) : function := - {| fn_sig:=Mach.fn_sig f; + {| 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; diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 838f7977..b53af131 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -17,12 +17,11 @@ Require Import Machblock. Require Import Machblockgen. Require Import ForwardSimulationBlock. -(* FIXME: put this section somewhere else. - In "Smallstep" ? - -TODO: also move "starN_last_step" in the same section ? - -*) +(** FIXME: put this section somewhere else. + * In "Smallstep" ? + * + * also move "starN_last_step" in the same section ? + *) Section starN_lemma. (* Auxiliary Lemma on starN *) @@ -35,16 +34,16 @@ Variable L: semantics. Local Hint Resolve starN_refl starN_step Eapp_assoc. -Lemma starN_split n s t s': +Lemma starN_split n s t s': starN (step L) (globalenv L) n s t s' -> - forall m k, n=m+k -> + forall m k, n=m+k -> exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. Proof. induction 1; simpl. + intros m k H; assert (X: m=0); try omega. assert (X0: k=0); try omega. subst; repeat (eapply ex_intro); intuition eauto. - + intros m; destruct m as [| m']; simpl. + + intros m; destruct m as [| m']; simpl. - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. - intros k H2. inversion H2. exploit (IHstarN m' k); eauto. intro. @@ -104,7 +103,7 @@ Proof (Genv.senv_match TRANSF). Lemma init_mem_preserved: forall m, - Genv.init_mem prog = Some m -> + Genv.init_mem prog = Some m -> Genv.init_mem tprog = Some m. Proof (Genv.init_mem_transf TRANSF). @@ -174,7 +173,7 @@ Proof. Qed. Lemma Mach_find_label_split l i c c': - Mach.find_label l (i :: c) = Some c' -> + Mach.find_label l (i :: c) = Some c' -> (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c'). Proof. intros H. @@ -270,7 +269,7 @@ Proof. symmetry. destruct i; try (simpl; auto). assert (l0 <> l); [ intro; subst; contradict H1; auto |]. rewrite peq_false; auto. -Qed. +Qed. Lemma to_bblock_body_find_label c2 bdy l c1: (bdy, c2) = to_bblock_body c1 -> @@ -376,6 +375,13 @@ Ltac ExploitDistEndBlockCode := | _ => idtac end. +Ltac totologize H := + match type of H with + | ( ?id = _ ) => + let Hassert := fresh "Htoto" in ( + assert (id = id) as Hassert; auto; rewrite H in Hassert at 2; simpl in Hassert; rewrite H in Hassert) + end. + (* FIXME - refactoriser avec get_code_nature pour que ce soit plus joli *) Lemma dist_end_block_code_simu_mid_block i c: dist_end_block_code (i::c) <> 0%nat -> @@ -420,7 +426,7 @@ Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. Proof. - destruct i; simpl in * |-; + destruct i; simpl in * |-; (discriminate || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. @@ -435,14 +441,14 @@ Proof. Qed. -Lemma star_step_simu_body_step s f sp c: +Lemma star_step_simu_body_step s f sp c: forall (p:bblock_body) c' rs m t s', to_bblock_body c = (p, c') -> - starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' -> + starN (Mach.step (inv_trans_rao rao)) ge (length p) (Mach.State s f sp c rs m) t s' -> exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp p rs m rs' m'. Proof. - induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H. - * (* nil *) + induction c as [ | i0 c0 Hc0]; simpl; intros p c' rs m t s' H. + * (* nil *) inversion_clear H; simpl; intros X; inversion_clear X. eapply ex_intro; eapply ex_intro; intuition eauto. * (* cons *) @@ -510,10 +516,10 @@ Lemma simu_end_block: step rao tge (trans_state s1) t (trans_state s1'). Proof. destruct s1; simpl. - + (* State *) + + (* State *) (* c cannot be nil *) - destruct c as [|i c]; simpl; try ( (* nil => absurd *) - unfold dist_end_block_code; simpl; + destruct c as [|i c]; simpl; try ( (* nil => absurd *) + unfold dist_end_block_code; simpl; intros t s1' H; inversion_clear H; inversion_clear H0; fail ). @@ -526,7 +532,7 @@ Proof. ( exploit (trans_code_nonil c0); subst; auto; try discriminate; intro H0; contradict H0 ). assert (X: Datatypes.S (dist_end_block_code c0) = (size (fst (to_bblock c0)))). - { + { unfold dist_end_block_code. remember (size _) as siz. assert (siz <> 0%nat). rewrite Heqsiz; apply to_bblock_nonil with (c0 := c) (i := i) (c := c0); auto. omega. @@ -587,7 +593,7 @@ Proof. - simpl in H3. inversion H3; subst. simpl. destruct c2 as [|ei c2']; inversion Heqexb; subst; try eapply exec_None_exit. clear H3. destruct (to_cfi ei) as [cfi|] eqn:TOCFI; inversion H0. - subst. eapply exec_None_exit. + subst. eapply exec_None_exit. + (* Callstate *) intros t s1' H; inversion_clear H. -- cgit