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

16 files changed, 366 insertions, 207 deletions

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 "@[<v 2>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 "@[<v 2>case %ld:@ %a@]@ %a"
-              (camlint_of_coqint lbl)
+  | LScons(lbl, s, rem) ->
+      fprintf p "@[<v 2>%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 "@[<v 2>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 "@[<v 2>case %ld:@ %a@]@ %a"
-              (camlint_of_coqint lbl)
+  | LScons(lbl, s, rem) ->
+      fprintf p "@[<v 2>%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.