- Support "switch" statements over 64-bit integers

  (in CompCert C to Cminor, included)
- Translation of "switch" to decision trees or jumptables made generic
  over the sizes of integers and moved to the Cminor->CminorSel pass
  instead of CminorSel->RTL as before.
- CminorSel: add "exitexpr" to support the above.
- ValueDomain: more precise analysis of comparisons against an integer
  literal.  E.g. "x >=u 0" is always true.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

15 files changed, 102 insertions, 57 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 6ee217c..702fcf2 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -765,8 +765,6 @@ let rec convertStmt ploc env s =
   | C.Scontinue ->
       Scontinue
   | C.Sswitch(e, s1) ->
-      if is_longlong env e.etyp then
-        unsupported "'switch' on an argument of type 'long long'";
       let (init, cases) = groupSwitch (flattenSwitch s1) in
       if cases = [] then
         unsupported "ill-formed 'switch' statement";
@@ -810,7 +808,7 @@ and convertSwitch ploc env = function
             match Ceval.integer_expr env e with
             | None -> unsupported "'case' label is not a compile-time integer";
                       None
-            | Some v -> Some (convertInt v)
+            | Some v -> Some (Z.of_uint64 v)
       in
       LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env rem)
 
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index eea1997..0e07093 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -1980,10 +1980,8 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
             do m' <- Mem.free_list m (blocks_of_env e);
             ret (Returnstate v' (call_cont k) m')
         | Kswitch1 sl k =>
-            match v with
-            | Vint n => ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
-            | _ => nil
-            end
+            do n <- sem_switch_arg v ty;
+            ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
         | _ => nil
         end
 
@@ -2089,7 +2087,6 @@ Proof with try (left; right; econstructor; eauto; fail).
   (* expression is a value *)
   rewrite (is_val_inv _ _ _ Heqo).
   destruct k; myinv...
-  destruct v; myinv...
   (* expression reduces *)
   intros. exploit list_in_map_inv; eauto. intros [[C rd] [A B]].
   generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q].
@@ -2189,6 +2186,7 @@ Proof with (unfold ret; auto with coqlib).
   rewrite H0...
   rewrite H0; rewrite H1...
   rewrite H1. red in H0. destruct k; try contradiction...
+  rewrite H0...
   destruct H0; subst x...
   rewrite H0...
 
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index d9fb650..40206d3 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -111,7 +111,7 @@ Inductive statement : Type :=
 
 with labeled_statements : Type :=            (**r cases of a [switch] *)
   | LSnil: labeled_statements
-  | LScons: option int -> statement -> labeled_statements -> labeled_statements.
+  | LScons: option Z -> statement -> labeled_statements -> labeled_statements.
                       (**r [None] is [default], [Some x] is [case x] *)
 
 (** The C loops are derived forms. *)
@@ -312,14 +312,14 @@ Fixpoint select_switch_default (sl: labeled_statements): labeled_statements :=
   | LScons (Some i) s sl' => select_switch_default sl'
   end.
 
-Fixpoint select_switch_case (n: int) (sl: labeled_statements): option labeled_statements :=
+Fixpoint select_switch_case (n: Z) (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'
+  | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl'
   end.
 
-Definition select_switch (n: int) (sl: labeled_statements): labeled_statements :=
+Definition select_switch (n: Z) (sl: labeled_statements): labeled_statements :=
   match select_switch_case n sl with
   | Some sl' => sl'
   | None => select_switch_default sl
@@ -614,8 +614,9 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f Sskip k e le m)
         E0 (Returnstate Vundef k m')
 
-  | step_switch: forall f a sl k e le m n,
-      eval_expr e le m a (Vint n) ->
+  | step_switch: forall f a sl k e le m v n,
+      eval_expr e le m a v ->
+      sem_switch_arg v (typeof a) = Some n ->
       step (State f (Sswitch a sl) k e le m)
         E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e le m)
   | step_skip_break_switch: forall f x k e le m,
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index f7a0e18..d61e4ee 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -151,8 +151,9 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
       exec_stmt e le2 m2 (Sloop s1 s2) t3 le3 m3 out ->
       exec_stmt e le m (Sloop s1 s2)
                 (t1**t2**t3) le3 m3 out
-  | exec_Sswitch:   forall e le m a t n sl le1 m1 out,
-      eval_expr ge e le m a (Vint n) ->
+  | exec_Sswitch:   forall e le m a t v n sl le1 m1 out,
+      eval_expr ge e le m a v ->
+      sem_switch_arg v (typeof a) = Some n ->
       exec_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t le1 m1 out ->
       exec_stmt e le m (Sswitch a sl)
                 t le1 m1 (outcome_switch out)
@@ -220,8 +221,9 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro
       exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal ->
       execinf_stmt e le2 m2 (Sloop s1 s2) t3 ->
       execinf_stmt e le m (Sloop s1 s2) (t1***t2***t3)
-  | execinf_Sswitch:   forall e le m a t n sl,
-      eval_expr ge e le m a (Vint n) ->
+  | execinf_Sswitch:   forall e le m a t v n sl,
+      eval_expr ge e le m a v ->
+      sem_switch_arg v (typeof a) = Some n ->
       execinf_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t ->
       execinf_stmt e le m (Sswitch a sl) t
 
@@ -427,7 +429,7 @@ Proof.
   auto.
 
 (* switch *)
-  destruct (H1 f (Kswitch k)) as [S1 [A1 B1]].
+  destruct (H2 f (Kswitch k)) as [S1 [A1 B1]].
   set (S2 :=
     match out with
     | Out_normal => State f Sskip k e le1 m1
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index ae6ec56..82509b0 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -138,7 +138,7 @@ 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) * nat :=
+Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (Z * nat) * nat :=
   match ls with
   | LSnil =>
       (nil, k)
@@ -193,10 +193,10 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
       OK (Sblock ts)
   | Csharpminor.Sexit n =>
       OK (Sexit (shift_exit xenv n))
-  | Csharpminor.Sswitch e ls =>
+  | Csharpminor.Sswitch long e ls =>
       let (tbl, dfl) := switch_table ls O in
       do te <- transl_expr cenv e;
-      transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te tbl dfl)
+      transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch long te tbl dfl)
   | Csharpminor.Sreturn None =>
       OK (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 3bf790c..7cb604e 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1697,15 +1697,15 @@ Proof.
 - auto.
 - destruct (switch_table sl (S base)) as [tbl1 dfl1] eqn:ST. 
   destruct o; simpl.
-  rewrite Int.eq_sym. destruct (Int.eq i i0). 
+  rewrite dec_eq_sym. destruct (zeq i z).
   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. 
+  destruct IHsl as (x & P & Q). exists (S x); 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. 
+  destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. 
   auto.
 Qed.
 
@@ -2107,7 +2107,8 @@ Opaque PTree.set.
 (* switch *)
   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.
+  assert (SA: switch_argument islong tv n).
+  { inv H0; inv VINJ; constructor. }
   exploit switch_descent; eauto. intros [k1 [A B]].
   exploit switch_ascent; eauto. eapply (switch_table_select n).
   rewrite STBL; simpl. intros [k2 [C D]].
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index ff43cbd..a5d4c66 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -936,7 +936,7 @@ Definition sem_cmp (c:comparison)
 
 (** ** Function applications *)
 
-Inductive classify_fun_cases : Type:=
+Inductive classify_fun_cases : Type :=
   | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (**r (pointer to) function *)
   | fun_default.
 
@@ -947,6 +947,30 @@ Definition classify_fun (ty: type) :=
   | _ => fun_default
   end.
 
+(** ** Argument of a [switch] statement *)
+
+Inductive classify_switch_cases : Type :=
+  | switch_case_i
+  | switch_case_l
+  | switch_default.
+
+Definition classify_switch (ty: type) :=
+  match ty with
+  | Tint _ _ _ => switch_case_i
+  | Tlong _ _ => switch_case_l
+  | _ => switch_default
+  end.
+
+Definition sem_switch_arg (v: val) (ty: type): option Z :=
+  match classify_switch ty with
+  | switch_case_i =>
+      match v with Vint n => Some(Int.unsigned n) | _ => None end
+  | switch_case_l =>
+      match v with Vlong n => Some(Int64.unsigned n) | _ => None end
+  | switch_default =>
+      None
+  end.
+
 (** * Combined semantics of unary and binary operators *)
 
 Definition sem_unary_operation
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index a43ee00..55c37c9 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -155,14 +155,14 @@ Fixpoint select_switch_default (sl: labeled_statements): labeled_statements :=
   | LScons (Some i) s sl' => select_switch_default sl'
   end.
 
-Fixpoint select_switch_case (n: int) (sl: labeled_statements): option labeled_statements :=
+Fixpoint select_switch_case (n: Z) (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'
+  | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl'
   end.
 
-Definition select_switch (n: int) (sl: labeled_statements): labeled_statements :=
+Definition select_switch (n: Z) (sl: labeled_statements): labeled_statements :=
   match select_switch_case n sl with
   | Some sl' => sl'
   | None => select_switch_default sl
@@ -715,8 +715,9 @@ Inductive sstep: state -> trace -> state -> Prop :=
   | step_switch: forall f x sl k e m,
       sstep (State f (Sswitch x sl) k e m)
          E0 (ExprState f x (Kswitch1 sl k) e m)
-  | step_expr_switch: forall f n ty sl k e m,
-      sstep (ExprState f (Eval (Vint n) ty) (Kswitch1 sl k) e m)
+  | step_expr_switch: forall f ty sl k e m v n,
+      sem_switch_arg v ty = Some n ->
+      sstep (ExprState f (Eval v ty) (Kswitch1 sl k) e m)
          E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
   | step_skip_break_switch: forall f x k e m,
       x = Sskip \/ x = Sbreak ->
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index d37fa81..c34b10a 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -21,6 +21,7 @@ Require Import Values.
 Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Switch.
 Require Cminor.
 Require Import Smallstep.
 
@@ -67,14 +68,14 @@ Inductive stmt : Type :=
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
-  | Sswitch: expr -> lbl_stmt -> stmt
+  | Sswitch: bool -> expr -> lbl_stmt -> stmt
   | Sreturn: option expr -> stmt
   | Slabel: label -> stmt -> stmt
   | Sgoto: label -> stmt
 
 with lbl_stmt : Type :=
   | LSnil: lbl_stmt
-  | LScons: option int -> stmt -> lbl_stmt -> lbl_stmt.
+  | LScons: option Z -> 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,
@@ -191,14 +192,14 @@ Fixpoint select_switch_default (sl: lbl_stmt): lbl_stmt :=
   | LScons (Some i) s sl' => select_switch_default sl'
   end.
 
-Fixpoint select_switch_case (n: int) (sl: lbl_stmt): option lbl_stmt :=
+Fixpoint select_switch_case (n: Z) (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'
+  | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl'
   end.
 
-Definition select_switch (n: int) (sl: lbl_stmt): lbl_stmt :=
+Definition select_switch (n: Z) (sl: lbl_stmt): lbl_stmt :=
   match select_switch_case n sl with
   | Some sl' => sl'
   | None => select_switch_default sl
@@ -230,7 +231,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
       find_label lbl s1 (Kseq (Sloop s1) k)
   | Sblock s1 =>
       find_label lbl s1 (Kblock k)
-  | Sswitch a sl =>
+  | Sswitch long a sl =>
       find_label_ls lbl sl k
   | Slabel lbl' s' =>
       if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
@@ -423,9 +424,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sexit (S n)) (Kblock k) e le m)
         E0 (State f (Sexit n) k e le m)
 
-  | step_switch: forall f a cases k e le m n,
-      eval_expr e le m a (Vint n) ->
-      step (State f (Sswitch a cases) k e le m)
+  | step_switch: forall f islong a cases k e le m v n,
+      eval_expr e le m a v ->
+      switch_argument islong v n ->
+      step (State f (Sswitch islong a cases) k e le m)
         E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e le m)
 
   | step_return_0: forall f k e le m m',
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index cedfd8b..3b23a54 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -589,7 +589,11 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
   | Clight.Sswitch a sl =>
       do ta <- transl_expr a;
       do tsl <- transl_lbl_stmt tyret 0%nat (S ncnt) sl;
-      OK (Sblock (Sswitch ta tsl))
+      match classify_switch (typeof a) with
+      | switch_case_i => OK (Sblock (Sswitch false ta tsl))
+      | switch_case_l => OK (Sblock (Sswitch true ta tsl))
+      | switch_default => Error(msg "Cshmgen.transl_stmt(switch)")
+      end
   | Clight.Slabel lbl s =>
       do ts <- transl_statement tyret nbrk ncnt s;
       OK (Slabel lbl ts)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index a977e0f..fdf5b06 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -118,7 +118,7 @@ Proof.
   {
     induction sl; simpl; intros.
     inv H; auto. 
-    monadInv H; simpl. destruct o. destruct (Int.eq i n). 
+    monadInv H; simpl. destruct o. destruct (zeq z n).
     econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto.
     apply IHsl; auto.
     apply IHsl; auto.
@@ -1188,6 +1188,9 @@ Proof.
 (* return *)
   simpl in TR. destruct o; monadInv TR. auto. auto. 
 (* switch *)
+  assert (exists b, ts = Sblock (Sswitch b x x0)).
+  { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. }
+  destruct H as [b EQ3]; rewrite EQ3; simpl.
   eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. 
 (* label *)
   destruct (ident_eq lbl l). 
@@ -1394,10 +1397,15 @@ Proof.
 
 (* switch *)
   monadInv TR.
+  assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n).
+  { unfold sem_switch_arg in H0.
+    destruct (classify_switch (typeof a)); inv EQ2; econstructor; split; eauto;
+    destruct v; inv H0; constructor. }
+  destruct E as (b & A & B). subst ts. 
   exploit transl_expr_correct; eauto. intro EV.
   econstructor; split.
   eapply star_plus_trans. eapply match_transl_step; eauto.
-  apply plus_one. econstructor. eauto. traceEq. 
+  apply plus_one. econstructor; eauto. traceEq. 
   econstructor; eauto.
   apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. 
   constructor.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index b6d1c87..676f3fa 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -1881,8 +1881,9 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
       exec_stmt e m3 (Sfor Sskip a2 a3 s) t4 m4 out ->
       exec_stmt e m (Sfor Sskip a2 a3 s)
                 (t1 ** t2 ** t3 ** t4) m4 out
-  | exec_Sswitch:   forall e m a sl t1 m1 n t2 m2 out,
-      eval_expression e m a t1 m1 (Vint n) ->
+  | exec_Sswitch:   forall e m a sl t1 m1 v n t2 m2 out,
+      eval_expression e m a t1 m1 v ->
+      sem_switch_arg v (typeof a) = Some n ->
       exec_stmt e m1 (seq_of_labeled_statement (select_switch n sl)) t2 m2 out ->
       exec_stmt e m (Sswitch a sl)
                 (t1 ** t2) m2 (outcome_switch out)
@@ -2104,8 +2105,9 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop :=
   | execinf_Sswitch_expr:   forall e m a sl t1,
       evalinf_expr e m RV a t1 ->
       execinf_stmt e m (Sswitch a sl) t1
-  | execinf_Sswitch_body:   forall e m a sl t1 m1 n t2,
-      eval_expression e m a t1 m1 (Vint n) ->
+  | execinf_Sswitch_body:   forall e m a sl t1 m1 v n t2,
+      eval_expression e m a t1 m1 v ->
+      sem_switch_arg v (typeof a) = Some n ->
       execinf_stmt e m1 (seq_of_labeled_statement (select_switch n sl)) t2 ->
       execinf_stmt e m (Sswitch a sl) (t1***t2)
 
@@ -2573,7 +2575,7 @@ Proof.
   auto.
 
 (* switch *)
-  destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]].
+  destruct (H3 f (Kswitch2 k)) as [S1 [A1 B1]].
   set (S2 :=
     match out with
     | Out_normal => State f Sskip k e m2
@@ -2584,7 +2586,7 @@ Proof.
   exists S2; split.
   eapply star_left. right; eapply step_switch.
   eapply star_trans. apply H0. 
-  eapply star_left. right; eapply step_expr_switch.
+  eapply star_left. right; eapply step_expr_switch. eauto. 
   eapply star_trans. eexact A1. 
   unfold S2; inv B1.
     apply star_one. right; constructor. auto. 
@@ -3013,7 +3015,7 @@ Proof.
   eapply forever_N_plus.
   eapply plus_left. right; constructor. 
   eapply star_right. eapply eval_expression_to_steps; eauto. 
-  right; constructor. 
+  right; constructor. eauto. 
   reflexivity. reflexivity. 
   eapply COS; eauto. traceEq. 
 
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ea1bd86..a926bc3 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -166,7 +166,7 @@ Inductive statement : Type :=
 
 with labeled_statements : Type :=            (**r cases of a [switch] *)
   | LSnil: labeled_statements
-  | LScons: option int -> statement -> labeled_statements -> labeled_statements.
+  | LScons: option Z -> statement -> labeled_statements -> labeled_statements.
                       (**r [None] is [default], [Some x] is [case x] *)
 (** ** Functions *)
 
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 0a77b19..c907f77 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -1003,7 +1003,7 @@ Proof.
       end).
   { induction 1; simpl; intros. 
     auto.
-    destruct c; auto. destruct (Int.eq i n); auto. 
+    destruct c; auto. destruct (zeq z n); auto. 
     econstructor; split; eauto. constructor; auto. }
   intros. unfold Csem.select_switch, select_switch.
   specialize (CASE n ls tls H). 
@@ -2113,7 +2113,7 @@ Proof.
   left; eapply plus_left. constructor. apply push_seq. traceEq.
   econstructor; eauto. constructor; auto. 
 (* expr switch *)
-  inv H7. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
+  inv H8. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst.
   econstructor; split.
   left; eapply plus_two. constructor. econstructor; eauto. traceEq.
   econstructor; eauto.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 6024de4..67a7e62 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1798,7 +1798,7 @@ Proof.
     induction ls; simpl; intros; monadInv H; simpl.
     auto.
     destruct o. 
-    destruct (Int.eq i n).
+    destruct (zeq z n).
     econstructor; split; eauto. simpl; rewrite EQ, EQ1; auto.
     apply IHls. auto. 
     apply IHls. auto.
@@ -1840,7 +1840,7 @@ Proof.
   {
     induction ls; simpl; intros.
     discriminate.
-    destruct o. destruct (Int.eq i n). inv H0. auto. eauto with compat. 
+    destruct o. destruct (zeq z n). inv H0. auto. eauto with compat. 
     eauto with compat.
   }
   intros. specialize (CASE ls). unfold select_switch. 
@@ -2104,8 +2104,12 @@ Proof.
   intros. apply match_cont_change_cenv with (cenv_for f); auto. eapply match_cont_free_env; eauto.
 
 (* switch *)
-  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. inv B.
+  exploit eval_simpl_expr; eauto with compat. intros [tv [A B]].
   econstructor; split. apply plus_one. econstructor; eauto.
+  rewrite typeof_simpl_expr. instantiate (1 := n). 
+  unfold sem_switch_arg in *;
+  destruct (classify_switch (typeof a)); try discriminate;
+  inv B; inv H0; auto.
   econstructor; eauto. 
   erewrite simpl_seq_of_labeled_statement. reflexivity.
   eapply simpl_select_switch; eauto.