diff options
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 179 |
1 files changed, 107 insertions, 72 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 78ec748..dba445d 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1643,29 +1643,78 @@ Qed. (** Properties of [switch] compilation *) -Remark switch_table_shift: - forall n sl base dfl, - switch_target n (S dfl) (switch_table sl (S base)) = - S (switch_target n dfl (switch_table sl base)). +Inductive lbl_stmt_tail: lbl_stmt -> nat -> lbl_stmt -> Prop := + | lstail_O: forall sl, + lbl_stmt_tail sl O sl + | lstail_S: forall c s sl n sl', + lbl_stmt_tail sl n sl' -> + lbl_stmt_tail (LScons c s sl) (S n) sl'. + +Lemma switch_table_default: + forall sl base, + exists n, + lbl_stmt_tail sl n (select_switch_default sl) + /\ snd (switch_table sl base) = (n + base)%nat. +Proof. + induction sl; simpl; intros. +- exists O; split. constructor. omega. +- destruct o. + + destruct (IHsl (S base)) as (n & P & Q). exists (S n); split. + constructor; auto. + destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. omega. + + exists O; split. constructor. + destruct (switch_table sl (S base)) as [tbl dfl]; simpl in *. auto. +Qed. + +Lemma switch_table_case: + forall i sl base dfl, + match select_switch_case i sl with + | None => + switch_target i dfl (fst (switch_table sl base)) = dfl + | Some sl' => + exists n, + lbl_stmt_tail sl n sl' + /\ switch_target i dfl (fst (switch_table sl base)) = (n + base)%nat + end. Proof. - induction sl; intros; simpl. auto. destruct (Int.eq n i); auto. + induction sl; simpl; intros. +- auto. +- destruct (switch_table sl (S base)) as [tbl1 dfl1] eqn:ST. + destruct o; simpl. + rewrite Int.eq_sym. destruct (Int.eq i i0). + exists O; split; auto. constructor. + specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. + destruct (select_switch_case i sl). + destruct IHsl as (n & P & Q). exists (S n); split. constructor; auto. omega. + auto. + specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. + destruct (select_switch_case i sl). + destruct IHsl as (n & P & Q). exists (S n); split. constructor; auto. omega. + auto. Qed. -Remark length_switch_table: - forall sl base1 base2, - length (switch_table sl base1) = length (switch_table sl base2). +Lemma switch_table_select: + forall i sl, + lbl_stmt_tail sl + (switch_target i (snd (switch_table sl O)) (fst (switch_table sl O))) + (select_switch i sl). Proof. - induction sl; intros; simpl. auto. decEq; auto. + unfold select_switch; intros. + generalize (switch_table_case i sl O (snd (switch_table sl O))). + destruct (select_switch_case i sl) as [sl'|]. + intros (n & P & Q). replace (n + O)%nat with n in Q by omega. congruence. + intros E; rewrite E. + destruct (switch_table_default sl O) as (n & P & Q). + replace (n + O)%nat with n in Q by omega. congruence. Qed. Inductive transl_lblstmt_cont(cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop := - | tlsc_default: forall s k ts, - transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts -> - transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k)) + | tlsc_default: forall k, + transl_lblstmt_cont cenv xenv LSnil k (Kblock (Kseq Sskip k)) | tlsc_case: forall i s ls k ts k', - transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts -> + transl_stmt cenv (switch_env (LScons i s ls) xenv) s = OK ts -> transl_lblstmt_cont cenv xenv ls k k' -> - transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')). + transl_lblstmt_cont cenv xenv (LScons i s ls) k (Kblock (Kseq ts k')). Lemma switch_descent: forall cenv xenv k ls body s, @@ -1676,10 +1725,10 @@ Lemma switch_descent: plus step tge (State f s k sp e m) E0 (State f body k' sp e m)). Proof. induction ls; intros. - monadInv H. econstructor; split. - econstructor; eauto. - intros. eapply plus_left. constructor. apply star_one. constructor. traceEq. - monadInv H. exploit IHls; eauto. intros [k' [A B]]. +- monadInv H. econstructor; split. + econstructor. + intros. eapply plus_two. constructor. constructor. auto. +- monadInv H. exploit IHls; eauto. intros [k' [A B]]. econstructor; split. econstructor; eauto. intros. eapply plus_star_trans. eauto. @@ -1688,27 +1737,21 @@ Proof. Qed. Lemma switch_ascent: - forall f n sp e m cenv xenv k ls k1, - let tbl := switch_table ls O in - let ls' := select_switch n ls in + forall f sp e m cenv xenv ls n ls', + lbl_stmt_tail ls n ls' -> + forall k k1, transl_lblstmt_cont cenv xenv ls k k1 -> exists k2, - star step tge (State f (Sexit (switch_target n (length tbl) tbl)) k1 sp e m) + star step tge (State f (Sexit n) k1 sp e m) E0 (State f (Sexit O) k2 sp e m) /\ transl_lblstmt_cont cenv xenv ls' k k2. Proof. - induction ls; intros; unfold tbl, ls'; simpl. - inv H. econstructor; split. apply star_refl. econstructor; eauto. - simpl in H. inv H. - rewrite Int.eq_sym. destruct (Int.eq i n). - econstructor; split. apply star_refl. econstructor; eauto. - exploit IHls; eauto. intros [k2 [A B]]. - rewrite (length_switch_table ls 1%nat 0%nat). - rewrite switch_table_shift. - econstructor; split. - eapply star_left. constructor. eapply star_left. constructor. eexact A. - reflexivity. traceEq. - exact B. + induction 1; intros. +- exists k1; split; auto. apply star_refl. +- inv H0. exploit IHlbl_stmt_tail; eauto. intros (k2 & P & Q). + exists k2; split; auto. + eapply star_left. constructor. eapply star_left. constructor. eexact P. + eauto. auto. Qed. Lemma switch_match_cont: @@ -1722,22 +1765,6 @@ Proof. inv H0. apply match_Kblock2. eapply match_Kseq2. auto. eauto. Qed. -Lemma transl_lblstmt_suffix: - forall n cenv xenv ls body ts, - transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> - let ls' := select_switch n ls in - exists body', exists ts', - transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'. -Proof. - induction ls; simpl; intros. - monadInv H. - exists body; econstructor. rewrite EQ; eauto. simpl. reflexivity. - monadInv H. - destruct (Int.eq i n). - exists body; econstructor. simpl. rewrite EQ; simpl. rewrite EQ0; simpl. reflexivity. - eauto. -Qed. - Lemma switch_match_states: forall fn k e le m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk' (TRF: transl_funbody cenv sz fn = OK tfn) @@ -1752,14 +1779,22 @@ Lemma switch_match_states: plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e le m) S. Proof. - intros. destruct ls; simpl. - inv TK. econstructor; split. - eapply plus_left. constructor. apply star_one. constructor. traceEq. - eapply match_state; eauto. - inv TK. econstructor; split. - eapply plus_left. constructor. apply star_one. constructor. traceEq. - eapply match_state_seq; eauto. - simpl. eapply switch_match_cont; eauto. + intros. inv TK. +- econstructor; split. eapply plus_two. constructor. constructor. auto. + eapply match_state; eauto. +- econstructor; split. eapply plus_left. constructor. apply star_one. constructor. auto. + simpl. eapply match_state_seq; eauto. simpl. eapply switch_match_cont; eauto. +Qed. + +Lemma transl_lblstmt_suffix: + forall cenv xenv ls n ls', + lbl_stmt_tail ls n ls' -> + forall body ts, transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + exists body', exists ts', transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'. +Proof. + induction 1; intros. +- exists body, ts; auto. +- monadInv H0. eauto. Qed. (** Commutation between [find_label] and compilation *) @@ -1778,10 +1813,9 @@ Lemma transl_lblstmt_find_label_context: find_label lbl ts tk1 = Some (ts', tk'). Proof. induction ls; intros. - monadInv H. inv H0. simpl. simpl in H2. replace x with ts by congruence. rewrite H1. auto. - monadInv H. inv H0. - eapply IHls. eauto. eauto. simpl in H6. replace x with ts0 by congruence. simpl. - rewrite H1. auto. +- monadInv H. inv H0. simpl. rewrite H1. auto. +- monadInv H. inv H0. simpl in H6. eapply IHls; eauto. + replace x with ts0 by congruence. simpl. rewrite H1. auto. Qed. Lemma transl_find_label: @@ -1830,6 +1864,7 @@ Proof. (* block *) apply transl_find_label with (true :: xenv). auto. constructor; auto. (* switch *) + simpl in H. destruct (switch_table l O) as [tbl dfl]. monadInv H. exploit switch_descent; eauto. intros [k' [A B]]. eapply transl_lblstmt_find_label. eauto. eauto. eauto. reflexivity. (* return *) @@ -1840,10 +1875,9 @@ Proof. apply transl_find_label with xenv; auto. intros. destruct ls; monadInv H; simpl. - (* default *) - inv H1. simpl in H3. replace x with ts by congruence. rewrite H2. - eapply transl_find_label; eauto. - (* case *) + (* nil *) + inv H1. rewrite H2. auto. + (* cons *) inv H1. simpl in H7. exploit (transl_find_label s). eauto. eapply switch_match_cont; eauto. destruct (Csharpminor.find_label lbl s (Csharpminor.Kseq (seq_of_lbl_stmt ls) k)) as [[s' k''] | ]. @@ -1851,8 +1885,7 @@ Proof. exists ts'; exists tk'; exists xenv'; intuition. eapply transl_lblstmt_find_label_context; eauto. simpl. replace x with ts0 by congruence. rewrite H2. auto. - intro. - eapply transl_lblstmt_find_label. eauto. auto. eauto. + intro. eapply transl_lblstmt_find_label. eauto. auto. eauto. simpl. replace x with ts0 by congruence. rewrite H2. auto. Qed. @@ -2056,14 +2089,16 @@ Opaque PTree.set. eapply plus_left. constructor. apply plus_star; eauto. traceEq. (* switch *) - monadInv TR. left. + simpl in TR. destruct (switch_table cases O) as [tbl dfl] eqn:STBL. monadInv TR. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. inv VINJ. exploit switch_descent; eauto. intros [k1 [A B]]. - exploit switch_ascent; eauto. intros [k2 [C D]]. - exploit transl_lblstmt_suffix; eauto. simpl. intros [body' [ts' E]]. + exploit switch_ascent; eauto. eapply (switch_table_select n). + rewrite STBL; simpl. intros [k2 [C D]]. + exploit transl_lblstmt_suffix; eauto. eapply (switch_table_select n). + simpl. intros [body' [ts' E]]. exploit switch_match_states; eauto. intros [T2 [F G]]. - exists T2; split. + left; exists T2; split. eapply plus_star_trans. eapply B. eapply star_left. econstructor; eauto. eapply star_trans. eexact C. |