diff options
-rw-r--r-- | driver/ForwardSimulationBlock.v | 30 | ||||
-rw-r--r-- | mppa_k1c/Machblockgen.v | 294 | ||||
-rw-r--r-- | mppa_k1c/Machblockgenproof.v | 71 |
3 files changed, 159 insertions, 236 deletions
diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index a9569e08..dc8beb29 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -42,7 +42,7 @@ Proof. intuition eauto. subst. auto. Qed. -Lemma starN_last_step n s t1 s': +Lemma starN_tailstep n s t1 s': starN (step L) (globalenv L) n s t1 s' -> forall (t t2:trace) s'', Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. @@ -95,31 +95,31 @@ Hypothesis simu_end_block: Local Hint Resolve starN_refl starN_step. -Definition star_in_block (head current: state L1): Prop := +Definition follows_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. -Lemma star_in_block_step (head previous next: state L1): - forall t, star_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> star_in_block head next. +Lemma follows_in_block_step (head previous next: state L1): + forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next. Proof. intros t [H1 H2] H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. + omega. + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). - - eapply starN_last_step; eauto. + - eapply starN_tailstep; eauto. - omega. Qed. -Lemma star_in_block_init (head current: state L1): - forall t, Step L1 head t current -> (dist_end_block head)<>0 -> star_in_block head current. +Lemma follows_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current. Proof. intros t H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. + omega. + cutrewrite (dist_end_block head - dist_end_block current = 1). - - eapply starN_last_step; eauto. + - eapply starN_tailstep; eauto. - omega. Qed. @@ -127,7 +127,7 @@ Qed. Record memostate := { real: state L1; memorized: option (state L1); - memo_star: forall head, memorized = Some head -> star_in_block head real; + memo_star: forall head, memorized = Some head -> follows_in_block head real; memo_final: forall r, final_state L1 real r -> memorized = None }. @@ -137,7 +137,7 @@ Definition head (s: memostate): state L1 := | Some s' => s' end. -Lemma head_star (s: memostate): star_in_block (head s) (real s). +Lemma head_followed (s: memostate): follows_in_block (head s) (real s). Proof. destruct s as [rs ms Hs]. simpl. destruct ms as [ms|]; unfold head; simpl; auto. @@ -204,10 +204,10 @@ Proof. * intros; discriminate. * intros; auto. * intros head X; injection X; clear X; intros; subst. - eapply star_in_block_step; eauto. + eapply follows_in_block_step; eauto. * intros r X; erewrite final_states_end_block in H3; intuition eauto. * intros head X; injection X; clear X; intros; subst. - eapply star_in_block_init; eauto. + eapply follows_in_block_init; eauto. * intros r X; erewrite final_states_end_block in H3; intuition eauto. Qed. @@ -244,9 +244,9 @@ Proof. - (* EndBloc *) constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. - * destruct (head_star s1) as [H4 H3]. + * destruct (head_followed s1) as [H4 H3]. cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. - eapply starN_last_step; eauto. + eapply starN_tailstep; eauto. * unfold head; rewrite H2; simpl. intuition eauto. Qed. @@ -319,4 +319,4 @@ Proof. inversion_clear H1. eauto. Qed. -End ForwardSimuBlock_TRANS.
\ No newline at end of file +End ForwardSimuBlock_TRANS. diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 0601f5b9..aa54e8a2 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -94,51 +94,21 @@ Proof. destruct i; discriminate. Qed. -Lemma get_code_nature_nil_contra c: get_code_nature c = IsEmpty -> c = nil. +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 get_code_nature_basic_inst c a c0: - c = a :: c0 -> - get_code_nature c = IsBasicInst -> - to_basic_inst a <> None. -Proof. - intros H1 H2. destruct a; discriminate || contradict H2; subst; simpl; discriminate. -Qed. - -Lemma to_bblock_header_not_IsLabel c h c0: - get_code_nature c <> IsLabel -> - to_bblock_header c = (h, c0) -> - c = c0 /\ h=nil. -Proof. - 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 c h c0: +Lemma to_bblock_header_noLabel c: get_code_nature c <> IsLabel -> - to_bblock_header c = (h, c0) -> - c = c0. + to_bblock_header c = (nil, c). Proof. - intros H1 H2; exploit to_bblock_header_not_IsLabel; intuition eauto. + intros H. destruct c as [|i c]; auto. + destruct i; simpl; auto. + contradict H; simpl; auto. Qed. -(* -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 H1 H2. destruct c; try discriminate. - destruct i; try discriminate. - unfold to_bblock_header in H2; inversion H2; eauto. -Qed. -*) - Lemma to_bblock_header_wfe c: forall h c0, to_bblock_header c = (h, c0) -> @@ -166,15 +136,13 @@ Proof. simpl; omega. Qed. -Lemma to_bblock_body_eq c b c0: +Lemma to_bblock_body_noBasic c: get_code_nature c <> IsBasicInst -> - to_bblock_body c = (b, c0) -> - c = c0. + to_bblock_body c = (nil, c). Proof. - 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. + 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: @@ -190,7 +158,35 @@ Proof. + inversion H; subst; auto. Qed. -(* pas vraiment utile: à éliminer *) +(** 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 @@ -216,20 +212,18 @@ Lemma to_bblock_body_wf 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. + intros X. destruct X. + exploit to_bblock_body_wfe; eauto. subst. simpl. simpl; omega. Qed. -Lemma to_bblock_exit_eq c b c0: +Lemma to_bblock_exit_noCFI c: get_code_nature c <> IsCFI -> - to_bblock_exit c = (b, c0) -> - c = c0. + to_bblock_exit c = (None, c). Proof. - 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. + 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: @@ -270,7 +264,7 @@ Proof. intros H; inversion H; subst; clear H; simpl; auto. Qed. -Lemma to_bblock_basic_inst_then_label i c bi: +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 -> @@ -282,19 +276,17 @@ Proof. destruct i; simpl in *; inversion H3; subst; auto. Qed. -Lemma to_bblock_cf_inst_then_label i c cfi: +Lemma to_bblock_CFI 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 := nil; body := nil; exit := Some cfi |}. 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. + intros H1 H2. + destruct i; try discriminate. + all: subst; rewrite <- H2; simpl; auto. Qed. -Lemma to_bblock_no_label c: +Lemma to_bblock_noLabel c: get_code_nature c <> IsLabel -> fst (to_bblock c) = {| header := nil; @@ -349,26 +341,7 @@ Proof. intros H; inversion H; subst; clear H; simpl; 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 c i bi: +Lemma to_bblock_basic c i bi: get_code_nature (i::c) = IsBasicInst -> to_basic_inst i = Some bi -> get_code_nature c <> IsLabel -> @@ -383,40 +356,41 @@ Proof. apply bblock_eq; simpl. (* header *) + destruct i; simpl; auto; ( - exploit to_bblock_no_label; [rewrite H; discriminate | intro; rewrite H2; 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 :( *) - + 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 ). + + 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: @@ -439,7 +413,7 @@ Proof. intros; rewrite to_bblock_size_single_label; auto. Qed. -Lemma to_bblock_size_basicinst_neqz c: +Lemma to_bblock_size_basic_neqz c: get_code_nature c = IsBasicInst -> size (fst (to_bblock c)) <> 0%nat. Proof. @@ -448,12 +422,12 @@ Proof. ( destruct (get_code_nature c) eqn:gcnc; (* Case gcnc is not IsLabel *) - try (erewrite to_bblock_basic_inst; eauto; [ + try (erewrite to_bblock_basic; eauto; [ unfold size; simpl; auto | simpl; auto | rewrite gcnc; discriminate ]); - erewrite to_bblock_basic_inst_then_label; eauto; [ + erewrite to_bblock_basic_then_label; eauto; [ unfold size; simpl; auto | simpl; auto ] @@ -468,18 +442,18 @@ Proof. destruct i; discriminate. Qed. -Lemma to_bblock_size_single_basicinst c i: +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_inst; eauto); + (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_no_label; eauto; intro; rewrite H2; simpl; auto; + exploit to_bblock_noLabel; eauto; intro; rewrite H2; simpl; auto; rewrite H2; auto ). Qed. @@ -505,87 +479,37 @@ Proof. 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. + - 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_eq; eauto. rewrite <- Heqgcn. discriminate. - intro; subst. - remember (to_bblock_body c1) as p2; eauto. + - 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_eq c1 h2 c2); eauto. rewrite <- Heqgcn. discriminate. - intro; subst. - remember (to_bblock_exit c2) as p3; eauto. + 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 c2 h3 c3); eauto. + exploit (to_bblock_exit_wf c h3 c3); eauto. inversion H0. omega. Qed. -Lemma to_bblock_nonil c i c0: - c = i :: c0 -> - size (fst (to_bblock c)) <> 0%nat. +Lemma to_bblock_nonil i c0: + size (fst (to_bblock (i :: c0))) <> 0%nat. Proof. - intros H. remember (get_code_nature c) as gcnc. destruct gcnc. + 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; auto. - - eapply to_bblock_size_basicinst_neqz; auto. - - eapply to_bblock_size_cfi_neqz; auto. + - eapply to_bblock_size_label_neqz; eauto. + - eapply to_bblock_size_basic_neqz; eauto. + - eapply to_bblock_size_cfi_neqz; eauto. Qed. -(* -Lemma to_bblock_islabel c l: - is_label l (fst (to_bblock (Mlabel l :: c))) = true. -Proof. - 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 l c: - body (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_body c). -Proof. - 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 c c' l: - snd (to_bblock_body c) = c' -> - exit (fst (to_bblock (Mlabel l :: c))) = fst (to_bblock_exit c'). -Proof. - 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]. - 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 diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 0efd4586..62391792 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -328,7 +328,7 @@ Ltac ExploitDistEndBlockCode := | [ H : dist_end_block_code (Mlabel ?l :: ?c) <> 0%nat |- _ ] => exploit (to_bblock_size_single_label c (Mlabel l)); eauto | [ H : dist_end_block_code (?i0 :: ?c) <> 0%nat |- _ ] => - exploit (to_bblock_size_single_basicinst c i0); eauto + exploit (to_bblock_size_single_basic c i0); eauto | _ => idtac end. @@ -339,45 +339,44 @@ Ltac totologize H := 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 -> (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)). Proof. intros H. - remember (get_code_nature c) as gcnc; destruct gcnc. - (* when c is nil *) - - contradict H; rewrite get_code_nature_nil_contra with (c := c); auto. destruct i; simpl; auto. - (* when c is IsLabel *) - - remember i as i0; remember (to_basic_inst i) as sbi; remember (to_cfi i) as scfi; - remember (get_code_nature (i::c)) as gcnic; - destruct i. - (* when i is a basic instruction *) - 1-6: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_basic_inst_then_label; eauto; - [ totologize Heqgcnic; eapply Htoto - | totologize Heqsbi; try eapply Htoto - | intro; subst; rewrite H; simpl; auto - ] ); fail). - (* when i is a control flow instruction *) - 1-8: try (( contradict H; unfold dist_end_block_code; exploit to_bblock_cf_inst_then_label; eauto; - [ totologize Heqgcnic; eapply Htoto - | totologize Heqscfi; try eapply Htoto - | intro; subst; rewrite H; simpl; auto - ] ); fail). - (* when i is a label *) - unfold dist_end_block_code in * |- *. subst i0. - rewrite (to_bblock_size_single_label c (Mlabel l)) in * |- *; simpl in * |- *; auto. omega. - (* when c is IsBasicInst or IsCFI *) - -(* - - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) - ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | - unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). - - destruct i; try (contradict H; auto; fail); (* getting rid of the non basic inst *) - ( ExploitDistEndBlockCode; [ rewrite <- Heqgcnc; discriminate | - unfold dist_end_block_code in *; intro; rewrite H0 in *; omega ] ). -*) -Admitted. + unfold dist_end_block_code. + destruct (get_code_nature (i::c)) eqn:GCNIC. + - apply get_code_nature_empty in GCNIC. discriminate. + - rewrite to_bblock_size_single_label; auto. + destruct c as [|i' c]. + + contradict H. destruct i; simpl; auto. + + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. omega. + - destruct (get_code_nature c) eqn:GCNC. + + apply get_code_nature_empty in GCNC. subst. contradict H. destruct i; simpl; auto. + + contradict H. destruct c as [|i' c]; try discriminate. + destruct i'; try discriminate. + destruct i; try discriminate. all: simpl; auto. + + destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate]. + erewrite to_bblock_basic; eauto; [| rewrite GCNC; discriminate ]. + simpl. destruct c as [|i' c]; try discriminate. + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. + cutrewrite (Datatypes.S (size (fst (to_bblock (i'::c))) - 1) = size (fst (to_bblock (i'::c)))). + unfold size. cutrewrite (length (header (fst (to_bblock (i' :: c)))) = 0). simpl. omega. + rewrite to_bblock_noLabel. simpl; auto. + rewrite GCNC. discriminate. + omega. + + destruct (to_basic_inst i) eqn:TBI; [| destruct i; discriminate]. + erewrite to_bblock_basic; eauto; [| rewrite GCNC; discriminate ]. + simpl. destruct c as [|i' c]; try discriminate. + assert (size (fst (to_bblock (i'::c))) <> 0). apply to_bblock_nonil. + cutrewrite (Datatypes.S (size (fst (to_bblock (i'::c))) - 1) = size (fst (to_bblock (i'::c)))). + unfold size. cutrewrite (length (header (fst (to_bblock (i' :: c)))) = 0). simpl. omega. + rewrite to_bblock_noLabel. simpl; auto. + rewrite GCNC. discriminate. + omega. + - contradict H. destruct i; try discriminate. + all: unfold dist_end_block_code; erewrite to_bblock_CFI; eauto; simpl; eauto. +Qed. Local Hint Resolve dist_end_block_code_simu_mid_block. @@ -543,7 +542,7 @@ Proof. 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. + assert (siz <> 0%nat). rewrite Heqsiz; subst; apply to_bblock_nonil with (c0 := c) (i := i); auto. omega. } |