From 1cd385f3b354a78ae8d02333f40cd065073c9b19 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 21 Dec 2013 17:00:43 +0000 Subject: Support "default" cases in the middle of a "switch", not just at the end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 28 ++++--- cfrontend/Clight.v | 34 +++++--- cfrontend/Cminorgen.v | 26 ++++--- cfrontend/Cminorgenproof.v | 179 ++++++++++++++++++++++++++----------------- cfrontend/Csem.v | 29 +++++-- cfrontend/Csharpminor.v | 32 +++++--- cfrontend/Cshmgen.v | 9 +-- cfrontend/Cshmgenproof.v | 43 +++++++++-- cfrontend/Csyntax.v | 6 +- cfrontend/PrintClight.ml | 24 +++--- cfrontend/PrintCsyntax.ml | 24 +++--- cfrontend/SimplExpr.v | 9 +-- cfrontend/SimplExprproof.v | 38 +++++---- cfrontend/SimplExprspec.v | 9 +-- cfrontend/SimplLocals.v | 13 ++-- cfrontend/SimplLocalsproof.v | 70 ++++++++++++++--- 16 files changed, 366 insertions(+), 207 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 850682e..f12efa3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -742,22 +742,20 @@ let rec convertStmt ploc env s = and convertSwitch ploc env = function | [] -> - LSdefault Sskip - | [Default, s] -> - LSdefault (convertStmt ploc env s) - | (Default, s) :: _ -> + LSnil + | (lbl, s) :: rem -> updateLoc s.sloc; - unsupported "'default' case must occur last"; - LSdefault Sskip - | (Case e, s) :: rem -> - updateLoc s.sloc; - let v = - match Ceval.integer_expr env e with - | None -> unsupported "'case' label is not a compile-time integer"; 0L - | Some v -> v in - LScase(convertInt v, - convertStmt ploc env s, - convertSwitch s.sloc env rem) + let lbl' = + match lbl with + | Default -> + None + | Case e -> + match Ceval.integer_expr env e with + | None -> unsupported "'case' label is not a compile-time integer"; + None + | Some v -> Some (convertInt v) + in + LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env rem) (** Function definitions *) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 6a57999..137decc 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -108,8 +108,9 @@ Inductive statement : Type := | Sgoto : label -> statement with labeled_statements : Type := (**r cases of a [switch] *) - | LSdefault: statement -> labeled_statements - | LScase: int -> statement -> labeled_statements -> labeled_statements. + | LSnil: labeled_statements + | LScons: option int -> statement -> labeled_statements -> labeled_statements. + (**r [None] is [default], [Some x] is [case x] *) (** The C loops are derived forms. *) @@ -301,19 +302,32 @@ Definition set_opttemp (optid: option ident) (v: val) (le: temp_env) := (** Selection of the appropriate case of a [switch], given the value [n] of the selector expression. *) -Fixpoint select_switch (n: int) (sl: labeled_statements) - {struct sl}: labeled_statements := +Fixpoint select_switch_default (sl: labeled_statements): labeled_statements := match sl with - | LSdefault _ => sl - | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + | LSnil => sl + | LScons None s sl' => sl + | LScons (Some i) s sl' => select_switch_default sl' + end. + +Fixpoint select_switch_case (n: int) (sl: labeled_statements): option labeled_statements := + match sl with + | LSnil => None + | LScons None s sl' => select_switch_case n sl' + | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl' + end. + +Definition select_switch (n: int) (sl: labeled_statements): labeled_statements := + match select_switch_case n sl with + | Some sl' => sl' + | None => select_switch_default sl end. (** Turn a labeled statement into a sequence *) Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := match sl with - | LSdefault s => s - | LScase c s sl' => Ssequence s (seq_of_labeled_statement sl') + | LSnil => Sskip + | LScons _ s sl' => Ssequence s (seq_of_labeled_statement sl') end. Section SEMANTICS. @@ -507,8 +521,8 @@ Fixpoint find_label (lbl: label) (s: statement) (k: cont) with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) {struct sl}: option (statement * cont) := match sl with - | LSdefault s => find_label lbl s k - | LScase _ s sl' => + | LSnil => None + | LScons _ s sl' => match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with | Some sk => Some sk | None => find_label_ls lbl sl' k diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 3b902c5..724e80c 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -140,16 +140,20 @@ Fixpoint shift_exit (e: exit_env) (n: nat) {struct e} : nat := | true :: e', S m => S (shift_exit e' m) end. -Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (int * nat) := +Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (int * nat) * nat := match ls with - | LSdefault _ => nil - | LScase ni _ rem => (ni, k) :: switch_table rem (S k) + | LSnil => + (nil, k) + | LScons None _ rem => + let (tbl, dfl) := switch_table rem (S k) in (tbl, k) + | LScons (Some ni) _ rem => + let (tbl, dfl) := switch_table rem (S k) in ((ni, k) :: tbl, dfl) end. Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env := match ls with - | LSdefault _ => e - | LScase _ _ ls' => false :: switch_env ls' e + | LSnil => e + | LScons _ _ ls' => false :: switch_env ls' e end. (** Translation of statements. The nonobvious part is @@ -192,10 +196,9 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) | Csharpminor.Sexit n => OK (Sexit (shift_exit xenv n)) | Csharpminor.Sswitch e ls => - let cases := switch_table ls O in - let default := length cases in + let (tbl, dfl) := switch_table ls O in do te <- transl_expr cenv e; - transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default) + transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te tbl dfl) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => @@ -210,10 +213,9 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) with transl_lblstmt (cenv: compilenv) (xenv: exit_env) (ls: Csharpminor.lbl_stmt) (body: stmt) {struct ls}: res stmt := match ls with - | Csharpminor.LSdefault s => - do ts <- transl_stmt cenv xenv s; - OK (Sseq (Sblock body) ts) - | Csharpminor.LScase _ s ls' => + | Csharpminor.LSnil => + OK (Sseq (Sblock body) Sskip) + | Csharpminor.LScons _ s ls' => do ts <- transl_stmt cenv xenv s; transl_lblstmt cenv (List.tail xenv) ls' (Sseq (Sblock body) ts) end. 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. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 5d94c53..be3ee4b 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -148,19 +148,32 @@ Definition blocks_of_env (e: env) : list (block * Z * Z) := (** Selection of the appropriate case of a [switch], given the value [n] of the selector expression. *) -Fixpoint select_switch (n: int) (sl: labeled_statements) - {struct sl}: labeled_statements := +Fixpoint select_switch_default (sl: labeled_statements): labeled_statements := match sl with - | LSdefault _ => sl - | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + | LSnil => sl + | LScons None s sl' => sl + | LScons (Some i) s sl' => select_switch_default sl' + end. + +Fixpoint select_switch_case (n: int) (sl: labeled_statements): option labeled_statements := + match sl with + | LSnil => None + | LScons None s sl' => select_switch_case n sl' + | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl' + end. + +Definition select_switch (n: int) (sl: labeled_statements): labeled_statements := + match select_switch_case n sl with + | Some sl' => sl' + | None => select_switch_default sl end. (** Turn a labeled statement into a sequence *) Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := match sl with - | LSdefault s => s - | LScase c s sl' => Ssequence s (seq_of_labeled_statement sl') + | LSnil => Sskip + | LScons _ s sl' => Ssequence s (seq_of_labeled_statement sl') end. (** Extract the values from a list of function arguments *) @@ -559,8 +572,8 @@ Fixpoint find_label (lbl: label) (s: statement) (k: cont) with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) {struct sl}: option (statement * cont) := match sl with - | LSdefault s => find_label lbl s k - | LScase _ s sl' => + | LSnil => None + | LScons _ s sl' => match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with | Some sk => Some sk | None => find_label_ls lbl sl' k diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 718daa1..6ae33a6 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -72,8 +72,8 @@ Inductive stmt : Type := | Sgoto: label -> stmt with lbl_stmt : Type := - | LSdefault: stmt -> lbl_stmt - | LScase: int -> stmt -> lbl_stmt -> lbl_stmt. + | LSnil: lbl_stmt + | LScons: option int -> stmt -> lbl_stmt -> lbl_stmt. (** Functions are composed of a return type, a list of parameter names, a list of local variables with their sizes, a list of temporary variables, @@ -183,16 +183,30 @@ Definition is_call_cont (k: cont) : Prop := (** Resolve [switch] statements. *) -Fixpoint select_switch (n: int) (sl: lbl_stmt) {struct sl} : lbl_stmt := +Fixpoint select_switch_default (sl: lbl_stmt): lbl_stmt := match sl with - | LSdefault _ => sl - | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + | LSnil => sl + | LScons None s sl' => sl + | LScons (Some i) s sl' => select_switch_default sl' + end. + +Fixpoint select_switch_case (n: int) (sl: lbl_stmt): option lbl_stmt := + match sl with + | LSnil => None + | LScons None s sl' => select_switch_case n sl' + | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl' + end. + +Definition select_switch (n: int) (sl: lbl_stmt): lbl_stmt := + match select_switch_case n sl with + | Some sl' => sl' + | None => select_switch_default sl end. Fixpoint seq_of_lbl_stmt (sl: lbl_stmt) : stmt := match sl with - | LSdefault s => s - | LScase c s sl' => Sseq s (seq_of_lbl_stmt sl') + | LSnil => Sskip + | LScons c s sl' => Sseq s (seq_of_lbl_stmt sl') end. (** Find the statement and manufacture the continuation @@ -225,8 +239,8 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont) with find_label_ls (lbl: label) (sl: lbl_stmt) (k: cont) {struct sl}: option (stmt * cont) := match sl with - | LSdefault s => find_label lbl s k - | LScase _ s sl' => + | LSnil => None + | LScons _ s sl' => match find_label lbl s (Kseq (seq_of_lbl_stmt sl') k) with | Some sk => Some sk | None => find_label_ls lbl sl' k diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index f37e8c7..0ed008f 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -534,13 +534,12 @@ with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat) (sl: Clight.labeled_statements) {struct sl}: res lbl_stmt := match sl with - | Clight.LSdefault s => - do ts <- transl_statement tyret nbrk ncnt s; - OK (LSdefault ts) - | Clight.LScase n s sl' => + | Clight.LSnil => + OK LSnil + | Clight.LScons n s sl' => do ts <- transl_statement tyret nbrk ncnt s; do tsl' <- transl_lbl_stmt tyret nbrk ncnt sl'; - OK (LScase n ts tsl') + OK (LScons n ts tsl') end. (*** Translation of functions *) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 851e3f2..220d907 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -100,10 +100,37 @@ Lemma transl_lbl_stmt_1: transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl). Proof. - induction sl; intros. - monadInv H. simpl. rewrite EQ. auto. - generalize H; intro TR. monadInv TR. simpl. - destruct (Int.eq i n). auto. auto. + intros until n. + assert (DFL: forall sl tsl, + transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> + transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)). + { + induction sl; simpl; intros. + inv H; auto. + monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. + } + assert (CASE: forall sl tsl, + transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> + match Clight.select_switch_case n sl with + | None => + select_switch_case n tsl = None + | Some sl' => + exists tsl', + select_switch_case n tsl = Some tsl' + /\ transl_lbl_stmt tyret nbrk ncnt sl' = OK tsl' + end). + { + induction sl; simpl; intros. + inv H; auto. + monadInv H; simpl. destruct o. destruct (Int.eq i n). + econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. + apply IHsl; auto. + apply IHsl; auto. + } + intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch. + destruct (Clight.select_switch_case n sl) as [sl'|]. + destruct CASE as [tsl' [P Q]]. rewrite P, Q. auto. + rewrite CASE. auto. Qed. Lemma transl_lbl_stmt_2: @@ -112,7 +139,7 @@ Lemma transl_lbl_stmt_2: transl_statement tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). Proof. induction sl; intros. - monadInv H. simpl. auto. + monadInv H. auto. monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto. Qed. @@ -1140,9 +1167,9 @@ Proof. auto. intro ls; case ls; intros; monadInv TR; simpl. -(* default *) - eapply transl_find_label; eauto. -(* case *) +(* nil *) + auto. +(* cons *) exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto. econstructor; eauto. apply transl_lbl_stmt_2; eauto. destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ]. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 6c333aa..8b98556 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -165,9 +165,9 @@ Inductive statement : Type := | Sgoto : label -> statement with labeled_statements : Type := (**r cases of a [switch] *) - | LSdefault: statement -> labeled_statements - | LScase: int -> statement -> labeled_statements -> labeled_statements. - + | LSnil: labeled_statements + | LScons: option int -> statement -> labeled_statements -> labeled_statements. + (**r [None] is [default], [Some x] is [case x] *) (** ** Functions *) (** A function definition is composed of its return type ([fn_return]), diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 8f0bfbf..78ab7fc 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -179,20 +179,22 @@ let rec print_stmt p s = and print_cases p cases = match cases with - | LSdefault Sskip -> + | LSnil -> () - | LSdefault s -> - fprintf p "@[default:@ %a@]" print_stmt s - | LScase(lbl, Sskip, rem) -> - fprintf p "case %ld:@ %a" - (camlint_of_coqint lbl) + | LScons(lbl, Sskip, rem) -> + fprintf p "%a:@ %a" + print_case_label lbl print_cases rem - | LScase(lbl, s, rem) -> - fprintf p "@[case %ld:@ %a@]@ %a" - (camlint_of_coqint lbl) + | LScons(lbl, s, rem) -> + fprintf p "@[%a:@ %a@]@ %a" + print_case_label lbl print_stmt s print_cases rem +and print_case_label p = function + | None -> fprintf p "default" + | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl) + and print_stmt_for p s = match s with | Sskip -> @@ -295,8 +297,8 @@ let rec collect_stmt = function | Sgoto lbl -> () and collect_cases = function - | LSdefault s -> collect_stmt s - | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem + | LSnil -> () + | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem let collect_function f = collect_type f.fn_return; diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index fc60f33..4db8976 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -324,20 +324,22 @@ let rec print_stmt p s = and print_cases p cases = match cases with - | LSdefault Sskip -> + | LSnil -> () - | LSdefault s -> - fprintf p "@[default:@ %a@]" print_stmt s - | LScase(lbl, Sskip, rem) -> - fprintf p "case %ld:@ %a" - (camlint_of_coqint lbl) + | LScons(lbl, Sskip, rem) -> + fprintf p "%a:@ %a" + print_case_label lbl print_cases rem - | LScase(lbl, s, rem) -> - fprintf p "@[case %ld:@ %a@]@ %a" - (camlint_of_coqint lbl) + | LScons(lbl, s, rem) -> + fprintf p "@[%a:@ %a@]@ %a" + print_case_label lbl print_stmt s print_cases rem +and print_case_label p = function + | None -> fprintf p "default" + | Some lbl -> fprintf p "case %ld" (camlint_of_coqint lbl) + and print_stmt_for p s = match s with | Sskip -> @@ -539,8 +541,8 @@ let rec collect_stmt = function | Sgoto lbl -> () and collect_cases = function - | LSdefault s -> collect_stmt s - | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem + | LSnil -> () + | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem let collect_function f = collect_type f.fn_return; diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 854d345..1ead0ae 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -488,13 +488,12 @@ Fixpoint transl_stmt (s: Csyntax.statement) : mon statement := with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements := match ls with - | Csyntax.LSdefault s => - do ts <- transl_stmt s; - ret (LSdefault ts) - | Csyntax.LScase n s ls1 => + | Csyntax.LSnil => + ret LSnil + | Csyntax.LScons c s ls1 => do ts <- transl_stmt s; do tls1 <- transl_lblstmt ls1; - ret (LScase n ts tls1) + ret (LScons c ts tls1) end. (** Translation of a function *) diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index dfe1c8a..b3c861e 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1003,9 +1003,27 @@ Lemma tr_select_switch: tr_lblstmts ls tls -> tr_lblstmts (Csem.select_switch n ls) (select_switch n tls). Proof. - induction 1; simpl. - constructor; auto. - destruct (Int.eq n0 n). constructor; auto. auto. + assert (DFL: forall ls tls, + tr_lblstmts ls tls -> + tr_lblstmts (Csem.select_switch_default ls) (select_switch_default tls)). + { induction 1; simpl. constructor. destruct c; auto. constructor; auto. } + assert (CASE: forall n ls tls, + tr_lblstmts ls tls -> + match Csem.select_switch_case n ls with + | None => + select_switch_case n tls = None + | Some ls' => + exists tls', select_switch_case n tls = Some tls' /\ tr_lblstmts ls' tls' + end). + { induction 1; simpl; intros. + auto. + destruct c; auto. destruct (Int.eq i n); auto. + econstructor; split; eauto. constructor; auto. } + intros. unfold Csem.select_switch, select_switch. + specialize (CASE n ls tls H). + destruct (Csem.select_switch_case n ls) as [ls'|]. + destruct CASE as [tls' [P Q]]. rewrite P. auto. + rewrite CASE. apply DFL; auto. Qed. Lemma tr_seq_of_labeled_statement: @@ -1013,7 +1031,7 @@ Lemma tr_seq_of_labeled_statement: tr_lblstmts ls tls -> tr_stmt (Csem.seq_of_labeled_statement ls) (seq_of_labeled_statement tls). Proof. - induction 1; simpl. auto. constructor; auto. + induction 1; simpl; constructor; auto. Qed. (** Commutation between translation and the "find label" operation. *) @@ -1086,14 +1104,6 @@ Proof. destruct dst; simpl; intros. auto. auto. apply nolabel_do_set. Qed. -(* -Lemma nolabel_dest_cast: - forall ty dst, nolabel_dest dst -> nolabel_dest (cast_destination ty dst). -Proof. - unfold nolabel_dest; intros; destruct dst; auto. -Qed. -*) - Ltac NoLabelTac := match goal with | [ |- nolabel_list nil ] => exact I @@ -1255,8 +1265,8 @@ Proof. auto. induction s; intros; inversion TR; subst; clear TR; simpl. -(* default *) - apply tr_find_label; auto. +(* nil *) + auto. (* case *) exploit (tr_find_label s (Csem.Kseq (Csem.seq_of_labeled_statement s0) k)); eauto. econstructor; eauto. apply tr_seq_of_labeled_statement; eauto. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index a424261..9dfa42e 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -479,13 +479,12 @@ Inductive tr_stmt: Csyntax.statement -> statement -> Prop := tr_stmt (Csyntax.Sgoto lbl) (Sgoto lbl) with tr_lblstmts: Csyntax.labeled_statements -> labeled_statements -> Prop := - | tr_default: forall s ts, - tr_stmt s ts -> - tr_lblstmts (Csyntax.LSdefault s) (LSdefault ts) - | tr_case: forall n s ls ts tls, + | tr_ls_nil: + tr_lblstmts Csyntax.LSnil LSnil + | tr_ls_cons: forall c s ls ts tls, tr_stmt s ts -> tr_lblstmts ls tls -> - tr_lblstmts (Csyntax.LScase n s ls) (LScase n ts tls). + tr_lblstmts (Csyntax.LScons c s ls) (LScons c ts tls). (** * Correctness proof with respect to the specification. *) diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index edcd5fe..95ff9ed 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -129,13 +129,12 @@ Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement := with simpl_lblstmt (cenv: compilenv) (ls: labeled_statements) : res labeled_statements := match ls with - | LSdefault s => - do s' <- simpl_stmt cenv s; - OK (LSdefault s') - | LScase n s ls1 => + | LSnil => + OK LSnil + | LScons c s ls1 => do s' <- simpl_stmt cenv s; do ls1' <- simpl_lblstmt cenv ls1; - OK (LScase n s' ls1') + OK (LScons c s' ls1') end. (** Function parameters that are not lifted to temporaries must be @@ -198,8 +197,8 @@ Fixpoint addr_taken_stmt (s: statement) : VSet.t := with addr_taken_lblstmt (ls: labeled_statements) : VSet.t := match ls with - | LSdefault s => addr_taken_stmt s - | LScase n s ls' => VSet.union (addr_taken_stmt s) (addr_taken_lblstmt ls') + | LSnil => VSet.empty + | LScons c s ls' => VSet.union (addr_taken_stmt s) (addr_taken_lblstmt ls') end. (** The compilation environment for a function is the set of local variables diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 8a26b08..552c991 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1747,11 +1747,37 @@ Remark simpl_select_switch: simpl_lblstmt cenv ls = OK tls -> simpl_lblstmt cenv (select_switch n ls) = OK (select_switch n tls). Proof. - induction ls; simpl; intros. - monadInv H. rewrite EQ; auto. - monadInv H. simpl. destruct (Int.eq i n). - simpl. rewrite EQ; rewrite EQ1. auto. - eauto. + intros cenv n. + assert (DFL: + forall ls tls, + simpl_lblstmt cenv ls = OK tls -> + simpl_lblstmt cenv (select_switch_default ls) = OK (select_switch_default tls)). + { + induction ls; simpl; intros; monadInv H. + auto. + simpl. destruct o. eauto. simpl; rewrite EQ, EQ1. auto. + } + assert (CASE: + forall ls tls, + simpl_lblstmt cenv ls = OK tls -> + match select_switch_case n ls with + | None => select_switch_case n tls = None + | Some ls' => + exists tls', select_switch_case n tls = Some tls' /\ simpl_lblstmt cenv ls' = OK tls' + end). + { + induction ls; simpl; intros; monadInv H; simpl. + auto. + destruct o. + destruct (Int.eq i n). + econstructor; split; eauto. simpl; rewrite EQ, EQ1; auto. + apply IHls. auto. + apply IHls. auto. + } + intros; unfold select_switch. + specialize (CASE _ _ H). destruct (select_switch_case n ls) as [ls'|]. + destruct CASE as [tls' [P Q]]. rewrite P, Q. auto. + rewrite CASE. apply DFL; auto. Qed. Remark simpl_seq_of_labeled_statement: @@ -1759,9 +1785,9 @@ Remark simpl_seq_of_labeled_statement: simpl_lblstmt cenv ls = OK tls -> simpl_stmt cenv (seq_of_labeled_statement ls) = OK (seq_of_labeled_statement tls). Proof. - induction ls; simpl; intros. - monadInv H. auto. - monadInv H. rewrite EQ; simpl. erewrite IHls; eauto. simpl. auto. + induction ls; simpl; intros; monadInv H; simpl. + auto. + rewrite EQ; simpl. erewrite IHls; eauto. simpl. auto. Qed. Remark compat_cenv_select_switch: @@ -1769,7 +1795,27 @@ Remark compat_cenv_select_switch: compat_cenv (addr_taken_lblstmt ls) cenv -> compat_cenv (addr_taken_lblstmt (select_switch n ls)) cenv. Proof. - induction ls; simpl; intros. auto. destruct (Int.eq i n); simpl; eauto with compat. + intros cenv n. + assert (DFL: forall ls, + compat_cenv (addr_taken_lblstmt ls) cenv -> + compat_cenv (addr_taken_lblstmt (select_switch_default ls)) cenv). + { + induction ls; simpl; intros. + eauto with compat. + destruct o; simpl; eauto with compat. + } + assert (CASE: forall ls ls', + compat_cenv (addr_taken_lblstmt ls) cenv -> + select_switch_case n ls = Some ls' -> + compat_cenv (addr_taken_lblstmt ls') cenv). + { + induction ls; simpl; intros. + discriminate. + destruct o. destruct (Int.eq i n). inv H0. auto. eauto with compat. + eauto with compat. + } + intros. specialize (CASE ls). unfold select_switch. + destruct (select_switch_case n ls) as [ls'|]; eauto. Qed. Remark addr_taken_seq_of_labeled_statement: @@ -1868,9 +1914,9 @@ Proof. monadInv TS; auto. induction ls; simpl; intros. - (* default *) - monadInv H. apply simpl_find_label; auto. - (* case *) + (* nil *) + monadInv H. auto. + (* cons *) monadInv H. exploit (simpl_find_label s (Kseq (seq_of_labeled_statement ls) k)). eauto. constructor. eapply simpl_seq_of_labeled_statement; eauto. eauto. -- cgit v1.2.3