- 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

32 files changed, 1220 insertions, 709 deletions

diff --git a/Changelog b/Changelog
index 8a2af33..c497f68 100644
--- a/Changelog
+++ b/Changelog
@@ -26,6 +26,12 @@
   pseudo-instructions so that it does not need to be re-done in
   cchecklink.  Updated the cchecklink validator accordingly.
 
+- Language features: support "switch" statements over an argument of
+  type "long long".
+
+- Value analysis and constant propagation: more precise treatment of
+  comparisons against an integer constant.
+
 
 Release 2.3pl2, 2014-05-15
 ==========================
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index d1926fd..7ed5b4a 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -149,6 +149,7 @@ rule token = parse
   | "*f"    { STARF }
   | "*l"    { STARL }
   | "switch"    { SWITCH }
+  | "switchl"    { SWITCHL }
   | "tailcall"  { TAILCALL }
   | "~"    { TILDE }
   | "~l"    { TILDEL }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 8c3769a..ad92a12 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -188,14 +188,14 @@ let longconst n =
 
 let exitnum n = Nat.of_int32 n
 
-let mkswitch expr (cases, dfl) =
+let mkswitch islong convert expr (cases, dfl) =
   convert_accu := [];
   let c = convert_rexpr expr in
   let rec mktable = function
   | [] -> []
   | (key, exit) :: rem ->
-      (coqint_of_camlint key, exitnum exit) :: mktable rem in
-  prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
+      (convert key, exitnum exit) :: mktable rem in
+  prepend_seq !convert_accu (Sswitch(islong, c, mktable cases, exitnum dfl))
 
 (***
    match (a) { case 0: s0; case 1: s1; case 2: s2; }  --->
@@ -222,7 +222,7 @@ let mkmatch_aux expr cases =
         (coqint_of_camlint key, Nat.of_int n)
         :: mktable (n + 1) rem in
   let sw =
-    Sswitch(expr, mktable 0 cases, Nat.of_int (ncases - 1)) in
+    Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in
   let rec mkblocks body n = function
     | [] -> assert false
     | [key, action] ->
@@ -366,6 +366,7 @@ let mkmatch expr cases =
 %token STARL
 %token <string> STRINGLIT
 %token SWITCH
+%token SWITCHL
 %token TILDE
 %token TILDEL
 %token TAILCALL
@@ -531,7 +532,9 @@ stmt:
   | RETURN SEMICOLON                            { Sreturn None }
   | RETURN expr SEMICOLON                       { mkreturn_some $2 }
   | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE
-                                                { mkswitch $3 $6 }
+                                         { mkswitch false Z.of_uint32 $3 $6 }
+  | SWITCHL LPAREN expr RPAREN LBRACE switchl_cases RBRACE
+                                         { mkswitch true Z.of_uint64 $3 $6 }
   | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE
                                                 { mkmatch $3 $6 }
   | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON
@@ -558,6 +561,13 @@ switch_cases:
            { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
 ;
 
+switchl_cases:
+    DEFAULT COLON EXIT INTLIT SEMICOLON
+           { ([], $4) }
+  | CASE LONGLIT COLON EXIT INTLIT SEMICOLON switchl_cases
+           { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
+;
+
 match_cases:
     /* empty */                                 { [] }
   | CASE INTLIT COLON stmt_list match_cases     { ($2, $4) :: $5 }
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 02c3f21..aacbf86 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -313,8 +313,8 @@ let rec type_stmt env blk ret s =
   | Sexit n ->
       if Nat.to_int n >= blk then
         raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n)))
-  | Sswitch(e, cases, deflt) ->
-      unify (type_expr env [] e) tint
+  | Sswitch(islong, e, cases, deflt) ->
+      unify (type_expr env [] e) (if islong then tlong else tint)
   | Sreturn None ->
       begin match ret with
       | None -> ()
diff --git a/backend/Cminor.v b/backend/Cminor.v
index bf20de2..7ac23bf 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -148,7 +148,7 @@ Inductive stmt : Type :=
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
-  | Sswitch: expr -> list (int * nat) -> nat -> stmt
+  | Sswitch: bool -> expr -> list (Z * nat) -> nat -> stmt
   | Sreturn: option expr -> stmt
   | Slabel: label -> stmt -> stmt
   | Sgoto: label -> stmt.
@@ -510,9 +510,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sexit (S n)) (Kblock k) sp e m)
         E0 (State f (Sexit n) k sp e m)
 
-  | step_switch: forall f a cases default k sp e m n,
-      eval_expr sp e m a (Vint n) ->
-      step (State f (Sswitch a cases default) k sp e m)
+  | step_switch: forall f islong a cases default k sp e m v n,
+      eval_expr sp e m a v ->
+      switch_argument islong v n ->
+      step (State f (Sswitch islong a cases default) k sp e m)
         E0 (State f (Sexit (switch_target n default cases)) k sp e m)
 
   | step_return_0: forall f k sp e m m',
@@ -733,9 +734,10 @@ with exec_stmt:
       forall f sp e m n,
       exec_stmt f sp e m (Sexit n) E0 e m (Out_exit n)
   | exec_Sswitch:
-      forall f sp e m a cases default n,
-      eval_expr ge sp e m a (Vint n) ->
-      exec_stmt f sp e m (Sswitch a cases default)
+      forall f sp e m islong a cases default v n,
+      eval_expr ge sp e m a v ->
+      switch_argument islong v n ->
+      exec_stmt f sp e m (Sswitch islong a cases default)
                 E0 e m (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
       forall f sp e m,
@@ -1051,8 +1053,7 @@ Proof.
 
 (* switch *)
   econstructor; split.
-  apply star_one. econstructor; eauto. 
-  constructor.
+  apply star_one. econstructor; eauto. constructor.
 
 (* return none *)
   econstructor; split. apply star_refl. constructor; auto.
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index db414a2..03ef092 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -22,7 +22,6 @@ Require Import Memory.
 Require Import Cminor.
 Require Import Op.
 Require Import Globalenvs.
-Require Import Switch.
 Require Import Smallstep.
 
 (** * Abstract syntax *)
@@ -57,10 +56,21 @@ with condexpr : Type :=
 
 Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope.
 
+(** Conditional expressions [condexpr] are expressions that are evaluated
+  not for their exact value, but for their [true]/[false] Boolean value.
+  Likewise, exit expressions [exitexpr] are expressions that evaluate
+  to an exit number.  They are used to compile the [Sswitch] statement
+  of Cminor. *)
+
+Inductive exitexpr : Type :=
+  | XEexit: nat -> exitexpr
+  | XEjumptable: expr -> list nat -> exitexpr
+  | XEcondition: condexpr -> exitexpr -> exitexpr -> exitexpr
+  | XElet: expr -> exitexpr -> exitexpr.
+
 (** Statements are as in Cminor, except that the [Sifthenelse]
-  construct uses a machine-dependent condition (with multiple
-  arguments), and the [Sstore] construct uses a machine-dependent
-  addressing mode. *)
+  construct uses a conditional expression, and the [Sstore] construct
+  uses a machine-dependent addressing mode. *)
 
 Inductive stmt : Type :=
   | Sskip: stmt
@@ -74,7 +84,7 @@ Inductive stmt : Type :=
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
-  | Sswitch: expr -> list (int * nat) -> nat -> stmt
+  | Sswitch: exitexpr -> stmt
   | Sreturn: option expr -> stmt
   | Slabel: label -> stmt -> stmt
   | Sgoto: label -> stmt.
@@ -214,6 +224,22 @@ Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop
   with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop
   with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop.
 
+Inductive eval_exitexpr: letenv -> exitexpr -> nat -> Prop :=
+  | eval_XEexit: forall le x,
+      eval_exitexpr le (XEexit x) x
+  | eval_XEjumptable: forall le a tbl n x,
+      eval_expr le a (Vint n) ->
+      list_nth_z tbl (Int.unsigned n) = Some x ->
+      eval_exitexpr le (XEjumptable a tbl) x
+  | eval_XEcondition: forall le a b c va x,
+      eval_condexpr le a va ->
+      eval_exitexpr le (if va then b else c) x ->
+      eval_exitexpr le (XEcondition a b c) x
+  | eval_XElet: forall le a b v x,
+      eval_expr le a v ->
+      eval_exitexpr (v :: le) b x ->
+      eval_exitexpr le (XElet a b) x.
+
 Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
   | eval_eos_e: forall le e v,
       eval_expr le e v ->
@@ -344,10 +370,10 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sexit (S n)) (Kblock k) sp e m)
         E0 (State f (Sexit n) k sp e m)
 
-  | step_switch: forall f a cases default k sp e m n,
-      eval_expr sp e m nil a (Vint n) ->
-      step (State f (Sswitch a cases default) k sp e m)
-        E0 (State f (Sexit (switch_target n default cases)) k sp e m)
+  | step_switch: forall f a k sp e m n,
+      eval_exitexpr sp e m nil a n ->
+      step (State f (Sswitch a) k sp e m)
+        E0 (State f (Sexit n) k sp e m)
 
   | step_return_0: forall f k sp e m m',
       Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
@@ -517,4 +543,3 @@ Proof.
 Qed.
 
 Hint Resolve eval_lift: evalexpr.
-
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 51a45b2..19f4c83 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -272,12 +272,15 @@ let rec print_stmt p s =
               print_stmt s
   | Sexit n ->
       fprintf p "exit %d;" (Nat.to_int n)
-  | Sswitch(e, cases, dfl) ->
-      fprintf p "@[<v 2>switch (%a) {" print_expr e;
+  | Sswitch(long, e, cases, dfl) ->
+      fprintf p "@[<v 2>switch%s (%a) {"
+        (if long then "l" else "") print_expr e;
       List.iter
         (fun (n, x) ->
-           fprintf p "@ case %ld: exit %d;" 
-                     (camlint_of_coqint n) (Nat.to_int x))
+           fprintf p "@ case %s%s: exit %d;" 
+                     (Z.to_string n)
+                     (if long then "LL" else "")
+                     (Nat.to_int x))
         cases;
       fprintf p "@ default: exit %d;\n" (Nat.to_int dfl);
       fprintf p "@;<0 -2>}@]"
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 193702e..26f51e3 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -455,19 +455,7 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node)
          transl_expr map b r nc
   end.
 
-(** Auxiliary for branch prediction.  When compiling an if/then/else
-  statement, we have a choice between translating the ``then'' branch
-  first or the ``else'' branch first.  Linearization of RTL control-flow
-  graph, performed later, will exploit this choice as a hint about
-  which branch is most frequently executed.  However, this choice has
-  no impact on program correctness.  We delegate the choice to an
-  external heuristic (written in OCaml), declared below.  *)
-
-Parameter more_likely: condexpr -> stmt -> stmt -> bool.
-
-(** Auxiliary for translating [Sswitch] statements. *)
-
-Parameter compile_switch: nat -> table -> comptree.
+(** Auxiliary for translating exit expressions. *)
 
 Definition transl_exit (nexits: list node) (n: nat) : mon node :=
   match nth_error nexits n with
@@ -484,29 +472,39 @@ Fixpoint transl_jumptable (nexits: list node) (tbl: list nat) : mon (list node)
       ret (n1 :: nl)
   end.
 
-Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
-                       {struct t} : mon node :=
-  match t with
-  | CTaction act =>
-      transl_exit nexits act
-  | CTifeq key act t' =>
-      do ncont <- transl_switch r nexits t';
-      do nfound <- transl_exit nexits act;
-      add_instr (Icond (Ccompimm Ceq key) (r :: nil) nfound ncont)
-  | CTiflt key t1 t2 =>
-      do n2 <- transl_switch r nexits t2;
-      do n1 <- transl_switch r nexits t1;
-      add_instr (Icond (Ccompuimm Clt key) (r :: nil) n1 n2)
-  | CTjumptable ofs sz tbl t' =>
-      do rt <- new_reg;
-      do ttbl <- transl_jumptable nexits tbl;
-      do n1 <- add_instr (Ijumptable rt ttbl);
-      do n2 <- transl_switch r nexits t';
-      do n3 <- add_instr (Icond (Ccompuimm Clt sz) (rt :: nil) n1 n2);
-      let op := if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs) in
-      add_instr (Iop op (r :: nil) rt n3)
+(** Translation of an exit expression.  Branches to the node corresponding
+  to the exit number denoted by the expression. *)
+
+Fixpoint transl_exitexpr (map: mapping) (a: exitexpr) (nexits: list node)
+                         {struct a} : mon node :=
+  match a with
+  | XEexit n =>
+      transl_exit nexits n
+  | XEjumptable a tbl =>
+      do r <- alloc_reg map a;
+      do tbl' <- transl_jumptable nexits tbl;
+      do n1 <- add_instr (Ijumptable r tbl');
+         transl_expr map a r n1
+  | XEcondition a b c =>
+      do nc <- transl_exitexpr map c nexits;
+      do nb <- transl_exitexpr map b nexits;
+         transl_condexpr map a nb nc
+  | XElet a b =>
+      do r  <- new_reg;
+      do n1 <- transl_exitexpr (add_letvar map r) b nexits;
+         transl_expr map a r n1
   end.
 
+(** Auxiliary for branch prediction.  When compiling an if/then/else
+  statement, we have a choice between translating the ``then'' branch
+  first or the ``else'' branch first.  Linearization of RTL control-flow
+  graph, performed later, will exploit this choice as a hint about
+  which branch is most frequently executed.  However, this choice has
+  no impact on program correctness.  We delegate the choice to an
+  external heuristic (written in OCaml), declared below.  *)
+
+Parameter more_likely: condexpr -> stmt -> stmt -> bool.
+
 (** Translation of statements.  [transl_stmt map s nd nexits nret rret]
   enriches the current CFG with the RTL instructions necessary to
   execute the CminorSel statement [s], and returns the node of the first
@@ -581,14 +579,8 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       transl_stmt map sbody nd (nd :: nexits) ngoto nret rret
   | Sexit n =>
       transl_exit nexits n
-  | Sswitch a cases default =>
-      let t := compile_switch default cases in
-      if validate_switch default cases t then
-        (do r <- alloc_reg map a;
-         do ns <- transl_switch r nexits t;
-         transl_expr map a r ns)
-      else
-        error (Errors.msg "RTLgen: wrong switch")
+  | Sswitch a =>
+      transl_exitexpr map a nexits
   | Sreturn opt_a =>
       match opt_a, rret with
       | None, _ => ret nret
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 7590102..27a4908 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -48,6 +48,14 @@ and size_condexpr = function
   | CElet(a, c) ->
       size_expr a + size_condexpr c
 
+let rec size_exitexpr = function
+  | XEexit n -> 0
+  | XEjumptable(arg, tbl) -> 2 + size_expr arg
+  | XEcondition(c1, c2, c3) ->
+      1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3
+  | XElet(a, c) ->
+      size_expr a + size_exitexpr c
+
 let rec length_exprs = function
   | Enil -> 0
   | Econs(e1, el) -> 1 + length_exprs el
@@ -71,7 +79,7 @@ let rec size_stmt = function
   | Sloop s -> 1 + 4 * size_stmt s
   | Sblock s -> size_stmt s
   | Sexit n -> 1
-  | Sswitch(arg, tbl, dfl) -> 2 + size_expr arg
+  | Sswitch xe -> size_exitexpr xe
   | Sreturn None -> 2
   | Sreturn (Some arg) -> 2 + size_expr arg
   | Slabel(lbl, s) -> size_stmt s
@@ -80,95 +88,3 @@ let rec size_stmt = function
 let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = 
   size_stmt ifso > size_stmt ifnot
 
-(* Compiling a switch table into a decision tree *)
-
-module IntOrd =
-  struct
-    type t = Integers.Int.int
-    let compare x y =
-      if Integers.Int.eq x y then 0 else
-      if Integers.Int.ltu x y then -1 else 1
-  end
-
-module IntSet = Set.Make(IntOrd)
-
-let normalize_table tbl =
-  let rec norm keys accu = function
-  | [] -> (accu, keys)
-  | (key, act) :: rem ->
-      if IntSet.mem key keys
-      then norm keys accu rem
-      else norm (IntSet.add key keys) ((key, act) :: accu) rem
-  in norm IntSet.empty [] tbl
-
-let compile_switch_as_tree default tbl =
-  let sw = Array.of_list tbl in
-  Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw;
-  let rec build lo hi minval maxval =
-    match hi - lo with
-    | 0 ->
-       CTaction default
-    | 1 ->
-       let (key, act) = sw.(lo) in
-       if Integers.Int.sub maxval minval = Integers.Int.zero
-       then CTaction act
-       else CTifeq(key, act, CTaction default)
-    | 2 ->
-       let (key1, act1) = sw.(lo)
-       and (key2, act2) = sw.(lo+1) in
-       CTifeq(key1, act1,
-         if Integers.Int.sub maxval minval = Integers.Int.one
-         then CTaction act2
-         else CTifeq(key2, act2, CTaction default))
-    | 3 ->
-       let (key1, act1) = sw.(lo)
-       and (key2, act2) = sw.(lo+1)
-       and (key3, act3) = sw.(lo+2) in
-       CTifeq(key1, act1, 
-        CTifeq(key2, act2,
-          if Integers.Int.sub maxval minval = coqint_of_camlint 2l
-          then CTaction act3
-          else CTifeq(key3, act3, CTaction default)))
-    | _ ->
-       let mid = (lo + hi) / 2 in
-       let (pivot, _) = sw.(mid) in
-       CTiflt(pivot,
-              build lo mid minval (Integers.Int.sub pivot Integers.Int.one),
-              build mid hi pivot maxval)
-  in build 0 (Array.length sw) Integers.Int.zero Integers.Int.max_unsigned
-
-let uint64_of_coqint n = (* force unsigned interpretation *)
-  Int64.logand (Int64.of_int32 (camlint_of_coqint n)) 0xFFFF_FFFFL
-
-let compile_switch_as_jumptable default cases minkey maxkey =
-  let tblsize = 1 + Int64.to_int (Int64.sub maxkey minkey) in
-  assert (tblsize >= 0 && tblsize <= Sys.max_array_length);
-  let tbl = Array.make tblsize default in
-  List.iter
-    (fun (key, act) ->
-       let pos = Int64.to_int (Int64.sub (uint64_of_coqint key) minkey) in
-       tbl.(pos) <- act)
-    cases;
-  CTjumptable(coqint_of_camlint (Int64.to_int32 minkey), 
-              coqint_of_camlint (Int32.of_int tblsize),
-              Array.to_list tbl,
-              CTaction default)
-
-let dense_enough (numcases: int) (minkey: int64) (maxkey: int64) =
-  let span = Int64.sub maxkey minkey in
-  assert (span >= 0L);
-  let tree_size = Int64.mul 4L (Int64.of_int numcases)
-  and table_size = Int64.add 8L span in
-  numcases >= 7           (* really small jump tables are less efficient *)
-  && span < Int64.of_int Sys.max_array_length
-  && table_size <= tree_size
-
-let compile_switch default table =
-  let (tbl, keys) = normalize_table table in
-  if IntSet.is_empty keys then CTaction default else begin
-    let minkey = uint64_of_coqint (IntSet.min_elt keys)
-    and maxkey = uint64_of_coqint (IntSet.max_elt keys) in
-    if dense_enough (List.length tbl) minkey maxkey
-    then compile_switch_as_jumptable default tbl minkey maxkey
-    else compile_switch_as_tree default tbl
-  end
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 51f1f27..2aa5ab9 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -414,71 +414,6 @@ Proof.
   split. apply Regmap.gss. intros; apply Regmap.gso; auto.
 Qed.
 
-(** Correctness of the translation of [switch] statements *)
-
-Lemma transl_switch_correct:
-  forall cs sp e m f map r nexits t ns,
-  tr_switch f.(fn_code) map r nexits t ns ->
-  forall rs i act,
-  rs#r = Vint i ->
-  map_wf map ->
-  match_env map e nil rs ->
-  comptree_match i t = Some act ->
-  exists nd, exists rs',
-  star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\
-  nth_error nexits act = Some nd /\
-  match_env map e nil rs'.
-Proof.
-  Opaque Int.sub.
-  induction 1; simpl; intros.
-(* action *)
-  inv H3. exists n; exists rs; intuition.
-  apply star_refl.
-(* ifeq *)
-  caseEq (Int.eq i key); intro EQ; rewrite EQ in H5.
-  inv H5. exists nfound; exists rs; intuition.
-  apply star_one. eapply exec_Icond with (b := true); eauto. 
-  simpl. rewrite H2. simpl. congruence.
-  exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
-  exists nd1; exists rs1; intuition.
-  eapply star_step. eapply exec_Icond with (b := false); eauto. 
-  simpl. rewrite H2. simpl. congruence. eexact EX. traceEq.
-(* iflt *)
-  caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5.
-  exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
-  exists nd1; exists rs1; intuition.
-  eapply star_step. eapply exec_Icond with (b := true); eauto. 
-  simpl. rewrite H2. simpl. congruence. eexact EX. traceEq.
-  exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
-  exists nd1; exists rs1; intuition.
-  eapply star_step. eapply exec_Icond with (b := false); eauto. 
-  simpl. rewrite H2. simpl. congruence. eexact EX. traceEq.
-(* jumptable *)
-  set (rs1 := rs#rt <- (Vint(Int.sub i ofs))).
-  assert (ME1: match_env map e nil rs1).
-    unfold rs1. eauto with rtlg.
-  assert (EX1: step tge (State cs f sp n rs m) E0 (State cs f sp n1 rs1 m)).
-    eapply exec_Iop; eauto. 
-    predSpec Int.eq Int.eq_spec ofs Int.zero; simpl.
-    rewrite H10. rewrite Int.sub_zero_l. congruence.
-    rewrite H6. simpl. rewrite <- Int.sub_add_opp. auto. 
-  caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9.
-  exploit H5; eauto. intros [nd [A B]].
-  exists nd; exists rs1; intuition. 
-  eapply star_step. eexact EX1.
-  eapply star_step. eapply exec_Icond with (b := true); eauto. 
-  simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. 
-  apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss. 
-  reflexivity. traceEq.
-  exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto.
-  intros [nd [rs' [EX [NTH ME]]]].
-  exists nd; exists rs'; intuition.
-  eapply star_step. eexact EX1.
-  eapply star_step. eapply exec_Icond with (b := false); eauto. 
-  simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence.
-  eexact EX. reflexivity. traceEq.
-Qed.
-
 (** ** Semantic preservation for the translation of expressions *)
 
 Section CORRECTNESS_EXPR.
@@ -560,10 +495,10 @@ Definition transl_condexpr_prop
   /\ Mem.extends m tm'.
 
 (** The correctness of the translation is a huge induction over
-  the Cminor evaluation derivation for the source program.  To keep
+  the CminorSel evaluation derivation for the source program.  To keep
   the proof manageable, we put each case of the proof in a separate
-  lemma.  There is one lemma for each Cminor evaluation rule.
-  It takes as hypotheses the premises of the Cminor evaluation rule,
+  lemma.  There is one lemma for each CminorSel evaluation rule.
+  It takes as hypotheses the premises of the CminorSel evaluation rule,
   plus the induction hypotheses, that is, the [transl_expr_prop], etc,
   corresponding to the evaluations of sub-expressions or sub-statements. *)
 
@@ -978,6 +913,58 @@ Proof
      transl_condexpr_CEcondition_correct
      transl_condexpr_CElet_correct).
 
+(** Exit expressions. *)
+
+Definition transl_exitexpr_prop 
+     (le: letenv) (a: exitexpr) (x: nat) : Prop :=
+  forall tm cs f map ns nexits rs
+    (MWF: map_wf map)
+    (TE: tr_exitexpr f.(fn_code) map a ns nexits)
+    (ME: match_env map e le rs)
+    (EXT: Mem.extends m tm),
+  exists nd, exists rs', exists tm',
+     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
+  /\ nth_error nexits x = Some nd
+  /\ match_env map e le rs'
+  /\ Mem.extends m tm'.
+
+Theorem transl_exitexpr_correct:
+  forall le a x,
+  eval_exitexpr ge sp e m le a x ->
+  transl_exitexpr_prop le a x.
+Proof.
+  induction 1; red; intros; inv TE.
+- (* XEexit *)
+  exists ns, rs, tm.
+  split. apply star_refl.
+  auto.
+- (* XEjumptable *)
+  exploit H3; eauto. intros (nd & A & B).
+  exploit transl_expr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & PRES1 & EXT1).
+  exists nd, rs1, tm1.
+  split. eapply star_right. eexact EXEC1. eapply exec_Ijumptable; eauto. inv RES1; auto. traceEq.
+  auto.
+- (* XEcondition *)
+  exploit transl_condexpr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & EXT1).
+  exploit IHeval_exitexpr; eauto. 
+  instantiate (2 := if va then n2 else n3). destruct va; eauto.
+  intros (nd & rs2 & tm2 & EXEC2 & EXIT2 & ME2 & EXT2).
+  exists nd, rs2, tm2. 
+  split. eapply star_trans. apply plus_star. eexact EXEC1. eexact EXEC2. traceEq.
+  auto.
+- (* XElet *)
+  exploit transl_expr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & PRES1 & EXT1).
+  assert (map_wf (add_letvar map r)).
+    eapply add_letvar_wf; eauto. 
+  exploit IHeval_exitexpr; eauto. eapply match_env_bind_letvar; eauto.
+  intros (nd & rs2 & tm2 & EXEC2 & EXIT2 & ME2 & EXT2).
+  exists nd, rs2, tm2.
+  split. eapply star_trans. eexact EXEC1. eexact EXEC2. traceEq. 
+  split. auto. 
+  split. eapply match_env_unbind_letvar; eauto.
+  auto.
+Qed.
+
 End CORRECTNESS_EXPR.
 
 (** ** Measure over CminorSel states *)
@@ -1357,15 +1344,11 @@ Proof.
 
   (* switch *)
   inv TS.
-  exploit validate_switch_correct; eauto. intro CTM.
-  exploit transl_expr_correct; eauto. 
-  intros [rs' [tm' [A [B [C [D X]]]]]].
-  exploit transl_switch_correct; eauto. inv C. auto.
-  intros [nd [rs'' [E [F G]]]].
+  exploit transl_exitexpr_correct; eauto. 
+  intros (nd & rs' & tm' & A & B & C & D). 
   econstructor; split.
-  right; split. eapply star_trans. eexact A. eexact E.  traceEq. Lt_state. 
-  econstructor; eauto.
-  constructor. auto.
+  right; split. eexact A. Lt_state. 
+  econstructor; eauto. constructor; auto. 
 
   (* return none *)
   inv TS.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index c82c051..32f35bb 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -673,7 +673,7 @@ Hint Resolve reg_map_ok_novar: rtlg.
 
 (** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the
-  value of the Cminor expression [expr] and deposit this value in
+  value of the CminorSel expression [expr] and deposit this value in
   register [rd].  [map] is a mapping from Cminor variables to the
   corresponding RTL registers.  [pr] is a list of RTL registers whose
   values must be preserved during this computation.  All registers
@@ -730,9 +730,9 @@ Inductive tr_expr (c: code):
       tr_expr c map pr (Eexternal id sg al) ns nd rd dst
 
 
-(** [tr_condition c map pr a ns ntrue nfalse rd] holds if the graph [c],
+(** [tr_condition c map pr a ns ntrue nfalse] holds if the graph [c],
   starting at node [ns], contains instructions that compute the truth
-  value of the Cminor conditional expression [a] and terminate
+  value of the CminorSel conditional expression [a] and terminate
   on node [ntrue] if the condition holds and on node [nfalse] otherwise. *)
 
 with tr_condition (c: code): 
@@ -754,7 +754,7 @@ with tr_condition (c: code):
 
 (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the values
-  of the list of Cminor expression [exprlist] and deposit these values
+  of the list of CminorSel expression [exprlist] and deposit these values
   in registers [rds]. *)
 
 with tr_exprlist (c: code): 
@@ -773,31 +773,32 @@ Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) :
   list_nth_z tbl v = Some act ->
   exists n, list_nth_z ttbl v = Some n /\ nth_error nexits act = Some n.
 
-Inductive tr_switch
-     (c: code) (map: mapping) (r: reg) (nexits: list node):
-     comptree -> node -> Prop :=
-  | tr_switch_action: forall act n,
-      nth_error nexits act = Some n ->
-      tr_switch c map r nexits (CTaction act) n
-  | tr_switch_ifeq: forall key act t' n ncont nfound,
-      tr_switch c map r nexits t' ncont ->
-      nth_error nexits act = Some nfound ->
-      c!n = Some(Icond (Ccompimm Ceq key) (r :: nil) nfound ncont) ->
-      tr_switch c map r nexits (CTifeq key act t') n
-  | tr_switch_iflt: forall key t1 t2 n n1 n2,
-      tr_switch c map r nexits t1 n1 ->
-      tr_switch c map r nexits t2 n2 ->
-      c!n = Some(Icond (Ccompuimm Clt key) (r :: nil) n1 n2) ->
-      tr_switch c map r nexits (CTiflt key t1 t2) n
-  | tr_switch_jumptable: forall ofs sz tbl t n n1 n2 n3 rt ttbl,
-      ~reg_in_map map rt -> rt <> r ->
-      c!n = Some(Iop (if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs))
-                     (r ::nil) rt n1) ->
-      c!n1 = Some(Icond (Ccompuimm Clt sz) (rt :: nil) n2 n3) ->
-      c!n2 = Some(Ijumptable rt ttbl) ->
-      tr_switch c map r nexits t n3 ->
-      tr_jumptable nexits tbl ttbl ->
-      tr_switch c map r nexits (CTjumptable ofs sz tbl t) n.
+(** [tr_exitexpr c map pr a ns nexits] holds if the graph [c],
+  starting at node [ns], contains instructions that compute the exit
+  number of the CminorSel exit expression [a] and terminate
+  on the node corresponding to this exit number according to the
+  mapping [nexits]. *)
+
+Inductive tr_exitexpr (c: code): 
+       mapping -> exitexpr -> node -> list node -> Prop :=
+  | tr_XEcond: forall map x n nexits,
+      nth_error nexits x = Some n ->
+      tr_exitexpr c map (XEexit x) n nexits
+  | tr_XEjumptable: forall map a tbl ns nexits n1 r tbl',
+      tr_jumptable nexits tbl tbl' ->
+      tr_expr c map nil a ns n1 r None ->
+      c!n1 = Some (Ijumptable r tbl') ->
+      tr_exitexpr c map (XEjumptable a tbl) ns nexits
+  | tr_XEcondition: forall map a1 a2 a3 ns nexits n2 n3,
+      tr_condition c map nil a1 ns n2 n3 ->
+      tr_exitexpr c map a2 n2 nexits ->
+      tr_exitexpr c map a3 n3 nexits ->
+      tr_exitexpr c map (XEcondition a1 a2 a3) ns nexits
+  | tr_XElet: forall map a b ns nexits r n1,
+      ~reg_in_map map r ->
+      tr_expr c map nil a ns n1 r None ->
+      tr_exitexpr c (add_letvar map r) b n1 nexits ->
+      tr_exitexpr c map (XElet a b) ns nexits.
 
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
@@ -866,11 +867,9 @@ Inductive tr_stmt (c: code) (map: mapping):
   | tr_Sexit: forall n ns nd nexits ngoto nret rret,
      nth_error nexits n = Some ns ->
      tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret
-  | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t,
-     validate_switch default cases t = true ->
-     tr_expr c map nil a ns n r None ->
-     tr_switch c map r nexits t n ->
-     tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret
+  | tr_Sswitch: forall a ns nd nexits ngoto nret rret,
+     tr_exitexpr c map a ns nexits ->
+     tr_stmt c map (Sswitch a) ns nd nexits ngoto nret rret
   | tr_Sreturn_none: forall nret nd nexits ngoto rret,
      tr_stmt c map (Sreturn None) nret nd nexits ngoto nret rret
   | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret,
@@ -1126,13 +1125,15 @@ Proof.
   constructor. eapply new_reg_not_in_map; eauto.
 Qed.
 
-Lemma tr_switch_incr:
+Lemma tr_exitexpr_incr:
   forall s1 s2, state_incr s1 s2 ->
-  forall map r nexits t ns,
-  tr_switch s1.(st_code) map r nexits t ns ->
-  tr_switch s2.(st_code) map r nexits t ns.
+  forall map a ns nexits,
+  tr_exitexpr s1.(st_code) map a ns nexits ->
+  tr_exitexpr s2.(st_code) map a ns nexits.
 Proof.
-  induction 2; econstructor; eauto with rtlg.
+  intros s1 s2 EXT.
+  generalize tr_expr_incr tr_condition_incr; intros I1 I2.
+  induction 1; econstructor; eauto with rtlg.
 Qed.
 
 Lemma tr_stmt_incr:
@@ -1142,10 +1143,9 @@ Lemma tr_stmt_incr:
   tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret.
 Proof.
   intros s1 s2 EXT.
-  generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3.
+  generalize tr_expr_incr tr_condition_incr tr_exprlist_incr tr_exitexpr_incr; intros I1 I2 I3 I4.
   pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
-  induction 1; try (econstructor; eauto; fail).
-  econstructor; eauto. eapply tr_switch_incr; eauto.
+  induction 1; econstructor; eauto.
 Qed.
 
 Lemma transl_exit_charact:
@@ -1170,35 +1170,31 @@ Proof.
   congruence.
 Qed.
 
-Lemma transl_switch_charact:
-  forall map r nexits t s ns s' incr,
-  map_valid map s -> reg_valid r s ->
-  transl_switch r nexits t s = OK ns s' incr ->
-  tr_switch s'.(st_code) map r nexits t ns.
+Lemma transl_exitexpr_charact:
+  forall nexits a map s ns s' INCR
+     (TR: transl_exitexpr map a nexits s = OK ns s' INCR)
+     (WF: map_valid map s),
+  tr_exitexpr s'.(st_code) map a ns nexits.
 Proof.
-  induction t; simpl; intros; saturateTrans.
-
+  induction a; simpl; intros; try (monadInv TR); saturateTrans.
+- (* XEexit *)
   exploit transl_exit_charact; eauto. intros [A B].
-  econstructor; eauto.
-
-  monadInv H1.
-  exploit transl_exit_charact; eauto. intros [A B]. subst s1.
-  econstructor; eauto 2 with rtlg. 
-  apply tr_switch_incr with s0; eauto with rtlg.
-
-  monadInv H1.
-  econstructor; eauto 2 with rtlg. 
-  apply tr_switch_incr with s1; eauto with rtlg.
-  apply tr_switch_incr with s0; eauto with rtlg.
-
-  monadInv H1.
-  exploit transl_jumptable_charact; eauto. intros [A B]. subst s1.
-  econstructor. eauto with rtlg.
-  apply sym_not_equal. apply valid_fresh_different with s; eauto with rtlg.
-  eauto with rtlg. eauto with rtlg. eauto with rtlg. 
-  apply tr_switch_incr with s3. eauto with rtlg.
-  eapply IHt with (s := s2); eauto with rtlg.
-  auto.
+  econstructor; eauto. 
+- (* XEjumptable *)
+  exploit transl_jumptable_charact; eauto. intros [A B].
+  econstructor; eauto. 
+  eapply transl_expr_charact; eauto with rtlg. 
+  eauto with rtlg.
+- (* XEcondition *)
+  econstructor. 
+  eapply transl_condexpr_charact; eauto with rtlg.
+  apply tr_exitexpr_incr with s1; eauto with rtlg. 
+  apply tr_exitexpr_incr with s0; eauto with rtlg.
+- (* XElet *)
+  econstructor; eauto with rtlg.
+  eapply transl_expr_charact; eauto with rtlg.
+  apply tr_exitexpr_incr with s1; auto. eapply IHa; eauto with rtlg.
+  apply add_letvar_valid; eauto with rtlg.
 Qed.
  
 Lemma transl_stmt_charact:
@@ -1285,15 +1281,7 @@ Proof.
   exploit transl_exit_charact; eauto. intros [A B].
   econstructor. eauto.
   (* Sswitch *)
-  generalize TR; clear TR.
-  set (t := compile_switch n l).
-  caseEq (validate_switch n l t); intro VALID; intros.
-  monadInv TR.
-  econstructor; eauto with rtlg.
-  eapply transl_expr_charact; eauto with rtlg.
-  apply tr_switch_incr with s1; auto with rtlg.
-  eapply transl_switch_charact with (s := s0); eauto with rtlg.
-  monadInv TR. 
+  econstructor. eapply transl_exitexpr_charact; eauto. 
   (* Sreturn *)
   destruct o. 
   destruct rret; inv TR. inv OK. 
diff --git a/backend/Selection.v b/backend/Selection.v
index 9bd37ef..cd17b9f 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -27,6 +27,7 @@ Require Import AST.
 Require Import Errors.
 Require Import Integers.
 Require Import Globalenvs.
+Require Import Switch.
 Require Cminor.
 Require Import Op.
 Require Import CminorSel.
@@ -34,7 +35,8 @@ Require Import SelectOp.
 Require Import SelectDiv.
 Require Import SelectLong.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
+Local Open Scope error_monad_scope.
 
 (** Conversion of conditions *)
 
@@ -203,60 +205,119 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind :=
       end
   end.
 
+(** Conversion of Cminor [switch] statements to decision trees. *)
+
+Parameter compile_switch: Z -> nat -> table -> comptree.
+
+Section SEL_SWITCH.
+
+Variable make_cmp_eq: expr -> Z -> expr.
+Variable make_cmp_ltu: expr -> Z -> expr.
+Variable make_sub: expr -> Z -> expr.
+Variable make_to_int: expr -> expr.
+
+Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr :=
+  match t with
+  | CTaction act =>
+      XEexit act
+  | CTifeq key act t' =>
+      XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key))
+                  (XEexit act)
+                  (sel_switch arg t')
+  | CTiflt key t1 t2 =>
+      XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key))
+                  (sel_switch arg t1)
+                  (sel_switch arg t2)
+  | CTjumptable ofs sz tbl t' =>
+      XElet (make_sub (Eletvar arg) ofs)
+        (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz))
+                     (XEjumptable (make_to_int (Eletvar O)) tbl)
+                     (sel_switch (S arg) t'))
+  end.
+
+End SEL_SWITCH.
+
+Definition sel_switch_int :=
+  sel_switch
+    (fun arg n => comp Ceq arg (Eop (Ointconst (Int.repr n)) Enil))
+    (fun arg n => compu Clt arg (Eop (Ointconst (Int.repr n)) Enil))
+    (fun arg ofs => sub arg (Eop (Ointconst (Int.repr ofs)) Enil))
+    (fun arg => arg).
+
+Definition sel_switch_long :=
+  sel_switch
+    (fun arg n => cmpl Ceq arg (longconst (Int64.repr n)))
+    (fun arg n => cmplu Clt arg (longconst (Int64.repr n)))
+    (fun arg ofs => subl hf arg (longconst (Int64.repr ofs)))
+    lowlong.
+
 (** Conversion from Cminor statements to Cminorsel statements. *)
 
-Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt :=
+Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt :=
   match s with
-  | Cminor.Sskip => Sskip
-  | Cminor.Sassign id e => Sassign id (sel_expr e)
-  | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
+  | Cminor.Sskip => OK Sskip
+  | Cminor.Sassign id e => OK (Sassign id (sel_expr e))
+  | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs))
   | Cminor.Scall optid sg fn args =>
-      match classify_call ge fn with
+      OK (match classify_call ge fn with
       | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)
       | Call_imm id  => Scall optid sg (inr _ id) (sel_exprlist args)
       | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args)
-      end
+      end)
   | Cminor.Sbuiltin optid ef args =>
-      Sbuiltin optid ef (sel_exprlist args)
+      OK (Sbuiltin optid ef (sel_exprlist args))
   | Cminor.Stailcall sg fn args => 
-      match classify_call ge fn with
+      OK (match classify_call ge fn with
       | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)
       | _            => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args)
-      end
-  | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2)
+      end)
+  | Cminor.Sseq s1 s2 =>
+      do s1' <- sel_stmt ge s1; do s2' <- sel_stmt ge s2;
+      OK (Sseq s1' s2')
   | Cminor.Sifthenelse e ifso ifnot =>
-      Sifthenelse (condexpr_of_expr (sel_expr e))
-                  (sel_stmt ge ifso) (sel_stmt ge ifnot)
-  | Cminor.Sloop body => Sloop (sel_stmt ge body)
-  | Cminor.Sblock body => Sblock (sel_stmt ge body)
-  | Cminor.Sexit n => Sexit n
-  | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl
-  | Cminor.Sreturn None => Sreturn None
-  | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e))
-  | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body)
-  | Cminor.Sgoto lbl => Sgoto lbl
+      do ifso' <- sel_stmt ge ifso; do ifnot' <- sel_stmt ge ifnot;
+      OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot')
+  | Cminor.Sloop body =>
+      do body' <- sel_stmt ge body; OK (Sloop body')
+  | Cminor.Sblock body =>
+      do body' <- sel_stmt ge body; OK (Sblock body')
+  | Cminor.Sexit n => OK (Sexit n)
+  | Cminor.Sswitch false e cases dfl =>
+      let t := compile_switch Int.modulus dfl cases in
+      if validate_switch Int.modulus dfl cases t
+      then OK (Sswitch (XElet (sel_expr e) (sel_switch_int O t)))
+      else Error (msg "Selection: bad switch (int)")
+  | Cminor.Sswitch true e cases dfl =>
+      let t := compile_switch Int64.modulus dfl cases in
+      if validate_switch Int64.modulus dfl cases t
+      then OK (Sswitch (XElet (sel_expr e) (sel_switch_long O t)))
+      else Error (msg "Selection: bad switch (long)")
+  | Cminor.Sreturn None => OK (Sreturn None)
+  | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e)))
+  | Cminor.Slabel lbl body =>
+      do body' <- sel_stmt ge body; OK (Slabel lbl body')
+  | Cminor.Sgoto lbl => OK (Sgoto lbl)
   end.
 
 End SELECTION.
 
 (** Conversion of functions. *)
 
-Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : function :=
-  mkfunction
-    f.(Cminor.fn_sig)
-    f.(Cminor.fn_params)
-    f.(Cminor.fn_vars)
-    f.(Cminor.fn_stackspace)
-    (sel_stmt hf ge f.(Cminor.fn_body)).
+Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : res function :=
+  do body' <- sel_stmt hf ge f.(Cminor.fn_body);
+  OK (mkfunction
+        f.(Cminor.fn_sig)
+        f.(Cminor.fn_params)
+        f.(Cminor.fn_vars)
+        f.(Cminor.fn_stackspace)
+        body').
 
-Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : fundef :=
-  transf_fundef (sel_function hf ge) f.
+Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : res fundef :=
+  transf_partial_fundef (sel_function hf ge) f.
 
 (** Conversion of programs. *)
 
-Local Open Scope error_monad_scope.
-
 Definition sel_program (p: Cminor.program) : res program :=
   let ge := Genv.globalenv p in
-  do hf <- get_helpers ge; OK (transform_program (sel_fundef hf ge) p).
+  do hf <- get_helpers ge; transform_partial_program (sel_fundef hf ge) p.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 55977b4..658e660 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -22,6 +22,7 @@ Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
 Require Import Smallstep.
+Require Import Switch.
 Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
@@ -33,7 +34,8 @@ Require Import SelectOpproof.
 Require Import SelectDivproof.
 Require Import SelectLongproof.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
+Local Open Scope error_monad_scope.
 
 
 (** * Correctness of the instruction selection functions for expressions *)
@@ -41,50 +43,54 @@ Open Local Scope cminorsel_scope.
 Section PRESERVATION.
 
 Variable prog: Cminor.program.
+Variable tprog: CminorSel.program.
 Let ge := Genv.globalenv prog.
-Variable hf: helper_functions.
-Let tprog := transform_program (sel_fundef hf ge) prog.
 Let tge := Genv.globalenv tprog.
+Variable hf: helper_functions.
 Hypothesis HELPERS: i64_helpers_correct tge hf.
+Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
-  intros; unfold ge, tge, tprog. apply Genv.find_symbol_transf.
+  intros. eapply Genv.find_symbol_transf_partial; eauto. 
 Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (sel_fundef hf ge f).
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf.
 Proof.  
-  intros. 
-  exact (Genv.find_funct_ptr_transf (sel_fundef hf ge) _ _ H).
+  intros. eapply Genv.find_funct_ptr_transf_partial; eauto.
 Qed.
 
 Lemma functions_translated:
   forall (v v': val) (f: Cminor.fundef),
   Genv.find_funct ge v = Some f ->
   Val.lessdef v v' ->
-  Genv.find_funct tge v' = Some (sel_fundef hf ge f).
+  exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf.
 Proof.  
   intros. inv H0.
-  exact (Genv.find_funct_transf (sel_fundef hf ge) _ _ H).
+  eapply Genv.find_funct_transf_partial; eauto.
   simpl in H. discriminate.
 Qed.
 
 Lemma sig_function_translated:
-  forall f,
-  funsig (sel_fundef hf ge f) = Cminor.funsig f.
+  forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f.
+Proof.
+  intros. destruct f; monadInv H; auto. monadInv EQ. auto. 
+Qed.
+
+Lemma stackspace_function_translated:
+  forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
 Proof.
-  intros. destruct f; reflexivity.
+  intros. monadInv H. auto. 
 Qed.
 
 Lemma varinfo_preserved:
   forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
 Proof.
-  intros; unfold ge, tge, tprog, sel_program. 
-  apply Genv.find_var_info_transf.
+  intros; eapply Genv.find_var_info_transf_partial; eauto.
 Qed.
 
 Lemma helper_implements_preserved:
@@ -93,7 +99,7 @@ Lemma helper_implements_preserved:
   helper_implements tge id sg vargs vres.
 Proof.
   intros. destruct H as (b & ef & A & B & C & D).
-  exploit function_ptr_translated; eauto. simpl. intros. 
+  exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. 
   exists b; exists ef. 
   split. rewrite symbols_preserved. auto.
   split. auto.
@@ -306,6 +312,176 @@ Proof.
   auto.
 Qed.
 
+(** Translation of [switch] statements *)
+
+Inductive Rint: Z -> val -> Prop :=
+  | Rint_intro: forall n, Rint (Int.unsigned n) (Vint n).
+
+Inductive Rlong: Z -> val -> Prop :=
+  | Rlong_intro: forall n, Rlong (Int64.unsigned n) (Vlong n).
+
+Section SEL_SWITCH.
+
+Variable make_cmp_eq: expr -> Z -> expr.
+Variable make_cmp_ltu: expr -> Z -> expr.
+Variable make_sub: expr -> Z -> expr.
+Variable make_to_int: expr -> expr.
+Variable modulus: Z.
+Variable R: Z -> val -> Prop.
+
+Hypothesis eval_make_cmp_eq: forall sp e m le a v i n,
+  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
+  eval_expr tge sp e m le (make_cmp_eq a n) (Val.of_bool (zeq i n)).
+Hypothesis eval_make_cmp_ltu: forall sp e m le a v i n,
+  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
+  eval_expr tge sp e m le (make_cmp_ltu a n) (Val.of_bool (zlt i n)).
+Hypothesis eval_make_sub: forall sp e m le a v i n,
+  eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus ->
+  exists v', eval_expr tge sp e m le (make_sub a n) v' /\ R ((i - n) mod modulus) v'.
+Hypothesis eval_make_to_int: forall sp e m le a v i,
+  eval_expr tge sp e m le a v -> R i v ->
+  exists v', eval_expr tge sp e m le (make_to_int a) v' /\ Rint (i mod Int.modulus) v'.
+
+Lemma sel_switch_correct_rec:
+  forall sp e m varg i x,
+  R i varg ->
+  forall t arg le,
+  wf_comptree modulus t ->
+  nth_error le arg = Some varg ->
+  comptree_match modulus i t = Some x ->
+  eval_exitexpr tge sp e m le (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t) x.
+Proof.
+  intros until x; intros Ri. induction t; simpl; intros until le; intros WF ARG MATCH.
+- (* base case *)
+  inv MATCH. constructor.
+- (* eq test *)
+  inv WF.
+  assert (eval_expr tge sp e m le (make_cmp_eq (Eletvar arg) key) (Val.of_bool (zeq i key))).
+  { eapply eval_make_cmp_eq; eauto. constructor; auto. }
+  eapply eval_XEcondition with (va := zeq i key). 
+  eapply eval_condexpr_of_expr; eauto. destruct (zeq i key); constructor; auto. 
+  destruct (zeq i key); simpl. 
+  + inv MATCH. constructor.
+  + eapply IHt; eauto.
+- (* lt test *)
+  inv WF.
+  assert (eval_expr tge sp e m le (make_cmp_ltu (Eletvar arg) key) (Val.of_bool (zlt i key))).
+  { eapply eval_make_cmp_ltu; eauto. constructor; auto. }
+  eapply eval_XEcondition with (va := zlt i key). 
+  eapply eval_condexpr_of_expr; eauto. destruct (zlt i key); constructor; auto. 
+  destruct (zlt i key); simpl. 
+  + eapply IHt1; eauto.
+  + eapply IHt2; eauto.
+- (* jump table *)
+  inv WF.
+  exploit (eval_make_sub sp e m le). eapply eval_Eletvar. eauto. eauto.
+  instantiate (1 := ofs). auto.
+  intros (v' & A & B).
+  set (i' := (i - ofs) mod modulus) in *.
+  assert (eval_expr tge sp e m (v' :: le) (make_cmp_ltu (Eletvar O) sz) (Val.of_bool (zlt i' sz))).
+  { eapply eval_make_cmp_ltu; eauto. constructor; auto. }
+  econstructor. eauto. 
+  eapply eval_XEcondition with (va := zlt i' sz).
+  eapply eval_condexpr_of_expr; eauto. destruct (zlt i' sz); constructor; auto.
+  destruct (zlt i' sz); simpl.
+  + exploit (eval_make_to_int sp e m (v' :: le) (Eletvar O)).
+    constructor. simpl; eauto. eauto. intros (v'' & C & D). inv D. 
+    econstructor; eauto. congruence. 
+  + eapply IHt; eauto.
+Qed.
+
+Lemma sel_switch_correct:
+  forall dfl cases arg sp e m varg i t le,
+  validate_switch modulus dfl cases t = true ->
+  eval_expr tge sp e m le arg varg ->
+  R i varg ->
+  0 <= i < modulus ->
+  eval_exitexpr tge sp e m le
+     (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
+     (switch_target i dfl cases).
+Proof.
+  intros. exploit validate_switch_correct; eauto. omega. intros [A B].
+  econstructor. eauto. eapply sel_switch_correct_rec; eauto.
+Qed.
+
+End SEL_SWITCH.
+
+Lemma sel_switch_int_correct:
+  forall dfl cases arg sp e m i t le,
+  validate_switch Int.modulus dfl cases t = true ->
+  eval_expr tge sp e m le arg (Vint i) ->
+  eval_exitexpr tge sp e m le (XElet arg (sel_switch_int O t)) (switch_target (Int.unsigned i) dfl cases).
+Proof.
+  assert (INTCONST: forall n sp e m le, 
+            eval_expr tge sp e m le (Eop (Ointconst n) Enil) (Vint n)).
+  { intros. econstructor. constructor. auto. } 
+  intros. eapply sel_switch_correct with (R := Rint); eauto.
+- intros until n; intros EVAL R RANGE.
+  exploit eval_comp. eexact EVAL. apply (INTCONST (Int.repr n)).  
+  instantiate (1 := Ceq). intros (vb & A & B). 
+  inv R. unfold Val.cmp in B. simpl in B. revert B. 
+  predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B. 
+  rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto. 
+  unfold Int.max_unsigned; omega.
+  unfold proj_sumbool; rewrite zeq_false; auto.
+  red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence.
+- intros until n; intros EVAL R RANGE.
+  exploit eval_compu. eexact EVAL. apply (INTCONST (Int.repr n)).  
+  instantiate (1 := Clt). intros (vb & A & B). 
+  inv R. unfold Val.cmpu in B. simpl in B.
+  unfold Int.ltu in B. rewrite Int.unsigned_repr in B. 
+  destruct (zlt (Int.unsigned n0) n); inv B; auto. 
+  unfold Int.max_unsigned; omega.
+- intros until n; intros EVAL R RANGE.
+  exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B).
+  inv R. simpl in B. inv B. econstructor; split; eauto. 
+  replace ((Int.unsigned n0 - n) mod Int.modulus)
+     with (Int.unsigned (Int.sub n0 (Int.repr n))).
+  constructor.
+  unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal. 
+  apply Int.unsigned_repr. unfold Int.max_unsigned; omega.
+- intros until i0; intros EVAL R. exists v; split; auto. 
+  inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor.
+- constructor. 
+- apply Int.unsigned_range.
+Qed.
+
+Lemma sel_switch_long_correct:
+  forall dfl cases arg sp e m i t le,
+  validate_switch Int64.modulus dfl cases t = true ->
+  eval_expr tge sp e m le arg (Vlong i) ->
+  eval_exitexpr tge sp e m le (XElet arg (sel_switch_long hf O t)) (switch_target (Int64.unsigned i) dfl cases).
+Proof.
+  intros. eapply sel_switch_correct with (R := Rlong); eauto.
+- intros until n; intros EVAL R RANGE.
+  eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
+  inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq. 
+  rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. 
+  unfold Int64.max_unsigned; omega.
+- intros until n; intros EVAL R RANGE. 
+  eapply eval_cmplu. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
+  inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. 
+  rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. 
+  unfold Int64.max_unsigned; omega.
+- intros until n; intros EVAL R RANGE.
+  exploit eval_subl. eexact HELPERS. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
+  intros (vb & A & B).
+  inv R. simpl in B. inv B. econstructor; split; eauto. 
+  replace ((Int64.unsigned n0 - n) mod Int64.modulus)
+     with (Int64.unsigned (Int64.sub n0 (Int64.repr n))).
+  constructor.
+  unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal. 
+  apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega.
+- intros until i0; intros EVAL R. 
+  exploit eval_lowlong. eexact EVAL. intros (vb & A & B). 
+  inv R. simpl in B. inv B. econstructor; split; eauto.
+  replace (Int64.unsigned n mod Int.modulus) with (Int.unsigned (Int64.loword n)).
+  constructor.
+  unfold Int64.loword. apply Int.unsigned_repr_eq. 
+- constructor. 
+- apply Int64.unsigned_range.
+Qed.
+
 (** Compatibility of evaluation functions with the "less defined than" relation. *)
 
 Ltac TrivialExists :=
@@ -433,56 +609,62 @@ Qed.
 Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
   | match_cont_stop:
       match_cont Cminor.Kstop Kstop
-  | match_cont_seq: forall s k k',
+  | match_cont_seq: forall s s' k k',
+      sel_stmt hf ge s = OK s' ->
       match_cont k k' ->
-      match_cont (Cminor.Kseq s k) (Kseq (sel_stmt hf ge s) k')
+      match_cont (Cminor.Kseq s k) (Kseq s' k')
   | match_cont_block: forall k k',
       match_cont k k' ->
       match_cont (Cminor.Kblock k) (Kblock k')
-  | match_cont_call: forall id f sp e k e' k',
+  | match_cont_call: forall id f sp e k f' e' k',
+      sel_function hf ge f = OK f' ->
       match_cont k k' -> env_lessdef e e' ->
-      match_cont (Cminor.Kcall id f sp e k) (Kcall id (sel_function hf ge f) sp e' k').
+      match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
 
 Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
-  | match_state: forall f s k s' k' sp e m e' m',
-      s' = sel_stmt hf ge s ->
-      match_cont k k' ->
-      env_lessdef e e' ->
-      Mem.extends m m' ->
+  | match_state: forall f f' s k s' k' sp e m e' m'
+        (TF: sel_function hf ge f = OK f')
+        (TS: sel_stmt hf ge s = OK s')
+        (MC: match_cont k k')
+        (LD: env_lessdef e e')
+        (ME: Mem.extends m m'),
       match_states
         (Cminor.State f s k sp e m)
-        (State (sel_function hf ge f) s' k' sp e' m')
-  | match_callstate: forall f args args' k k' m m',
-      match_cont k k' ->
-      Val.lessdef_list args args' ->
-      Mem.extends m m' ->
+        (State f' s' k' sp e' m')
+  | match_callstate: forall f f' args args' k k' m m'
+        (TF: sel_fundef hf ge f = OK f')
+        (MC: match_cont k k')
+        (LD: Val.lessdef_list args args')
+        (ME: Mem.extends m m'),
       match_states
         (Cminor.Callstate f args k m)
-        (Callstate (sel_fundef hf ge f) args' k' m')
-  | match_returnstate: forall v v' k k' m m',
-      match_cont k k' ->
-      Val.lessdef v v' ->
-      Mem.extends m m' ->
+        (Callstate f' args' k' m')
+  | match_returnstate: forall v v' k k' m m'
+        (MC: match_cont k k')
+        (LD: Val.lessdef v v')
+        (ME: Mem.extends m m'),
       match_states
         (Cminor.Returnstate v k m)
         (Returnstate v' k' m')
-  | match_builtin_1: forall ef args args' optid f sp e k m al e' k' m',
-      match_cont k k' ->
-      Val.lessdef_list args args' ->
-      env_lessdef e e' ->
-      Mem.extends m m' ->
-      eval_exprlist tge sp e' m' nil al args' ->
+  | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m'
+        (TF: sel_function hf ge f = OK f')
+        (MC: match_cont k k')
+        (LDA: Val.lessdef_list args args')
+        (LDE: env_lessdef e e')
+        (ME: Mem.extends m m')
+        (EA: eval_exprlist tge sp e' m' nil al args'),
       match_states
         (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
-        (State (sel_function hf ge f) (Sbuiltin optid ef al) k' sp e' m')
-  | match_builtin_2: forall v v' optid f sp e k m e' m' k',
-      match_cont k k' ->
-      Val.lessdef v v' ->
-      env_lessdef e e' ->
-      Mem.extends m m' ->
+        (State f' (Sbuiltin optid ef al) k' sp e' m')
+  | match_builtin_2: forall v v' optid f sp e k m f' e' m' k'
+        (TF: sel_function hf ge f = OK f')
+        (MC: match_cont k k')
+        (LDV: Val.lessdef v v')
+        (LDE: env_lessdef e e')
+        (ME: Mem.extends m m'),
       match_states
         (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
-        (State (sel_function hf ge f) Sskip k' sp (set_optvar optid v' e') m').
+        (State f' Sskip k' sp (set_optvar optid v' e') m').
 
 Remark call_cont_commut:
   forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k').
@@ -491,15 +673,16 @@ Proof.
 Qed.
 
 Remark find_label_commut:
-  forall lbl s k k',
+  forall lbl s k s' k',
   match_cont k k' ->
-  match Cminor.find_label lbl s k, find_label lbl (sel_stmt hf ge s) k' with
+  sel_stmt hf ge s = OK s' ->
+  match Cminor.find_label lbl s k, find_label lbl s' k' with
   | None, None => True
-  | Some(s1, k1), Some(s1', k1') => s1' = sel_stmt hf ge s1 /\ match_cont k1 k1'
+  | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1'
   | _, _ => False
   end.
 Proof.
-  induction s; intros; simpl; auto.
+  induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto.
 (* store *)
   unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto.
 (* call *)
@@ -507,21 +690,27 @@ Proof.
 (* tailcall *)
   destruct (classify_call ge e); simpl; auto.
 (* seq *)
-  exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. 
+  exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.  
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
-  destruct (find_label lbl (sel_stmt hf ge s1) (Kseq (sel_stmt hf ge s2) k')) as [[sy ky] | ];
+  destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ];
   intuition. apply IHs2; auto.
 (* ifthenelse *)
   exploit (IHs1 k); eauto. 
   destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
-  destruct (find_label lbl (sel_stmt hf ge s1) k') as [[sy ky] | ];
+  destruct (find_label lbl x k') as [[sy ky] | ];
   intuition. apply IHs2; auto.
 (* loop *)
-  apply IHs. constructor; auto.
+  apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto.
 (* block *)
-  apply IHs. constructor; auto.
+  apply IHs. constructor; auto. auto.
+(* switch *)
+  destruct b. 
+  destruct (validate_switch Int64.modulus n l (compile_switch Int64.modulus n l)); inv SE.
+  simpl; auto.
+  destruct (validate_switch Int.modulus n l (compile_switch Int.modulus n l)); inv SE.
+  simpl; auto.
 (* return *)
-  destruct o; simpl; auto. 
+  destruct o; inv SE; simpl; auto.
 (* label *)
   destruct (ident_eq lbl l). auto. apply IHs; auto.
 Qed.
@@ -539,64 +728,68 @@ Lemma sel_step_correct:
   (exists T2, step tge T1 t T2 /\ match_states S2 T2)
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
 Proof.
-  induction 1; intros T1 ME; inv ME; simpl.
-  (* skip seq *)
-  inv H7. left; econstructor; split. econstructor. constructor; auto.
-  (* skip block *)
-  inv H7. left; econstructor; split. econstructor. constructor; auto.
-  (* skip call *)
+  induction 1; intros T1 ME; inv ME; try (monadInv TS).
+- (* skip seq *)
+  inv MC. left; econstructor; split. econstructor. constructor; auto.
+- (* skip block *)
+  inv MC. left; econstructor; split. econstructor. constructor; auto.
+- (* skip call *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   left; econstructor; split. 
-  econstructor. inv H9; simpl in H; simpl; auto. 
+  econstructor. inv MC; simpl in H; simpl; auto. 
   eauto. 
+  erewrite stackspace_function_translated; eauto. 
   constructor; auto.
-  (* assign *)
+- (* assign *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split.
   econstructor; eauto.
   constructor; auto. apply set_var_lessdef; auto.
-  (* store *)
+- (* store *)
   exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]].
   exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]].
   exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
   left; econstructor; split.
   eapply eval_store; eauto.
   constructor; auto.
-  (* Scall *)
+- (* Scall *)
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
   exploit classify_call_correct; eauto. 
   destruct (classify_call ge a) as [ | id | ef].
-  (* indirect *)
++ (* indirect *)
   exploit sel_expr_correct; eauto. intros [vf' [A B]].
+  exploit functions_translated; eauto. intros (fd' & U & V).
   left; econstructor; split.
   econstructor; eauto. econstructor; eauto. 
-  eapply functions_translated; eauto. 
-  apply sig_function_translated.
+  apply sig_function_translated; auto.
   constructor; auto. constructor; auto.
-  (* direct *)
++ (* direct *)
   intros [b [U V]]. 
+  exploit functions_translated; eauto. intros (fd' & X & Y).
   left; econstructor; split.
-  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto.
-  eapply functions_translated; eauto. subst vf; auto. 
-  apply sig_function_translated.
+  econstructor; eauto.
+  subst vf. econstructor; eauto. rewrite symbols_preserved; eauto.
+  apply sig_function_translated; auto.
   constructor; auto. constructor; auto.
-  (* turned into Sbuiltin *)
++ (* turned into Sbuiltin *)
   intros EQ. subst fd. 
-  right; split. omega. split. auto. 
+  right; split. simpl. omega. split. auto. 
   econstructor; eauto.
-  (* Stailcall *)
+- (* Stailcall *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
+  erewrite <- stackspace_function_translated in P by eauto.
   exploit sel_expr_correct; eauto. intros [vf' [A B]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
+  exploit functions_translated; eauto. intros [fd' [E F]].
   left; econstructor; split.
   exploit classify_call_correct; eauto. 
   destruct (classify_call ge a) as [ | id | ef]; intros. 
-  econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated.
-  destruct H2 as [b [U V]].
-  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply functions_translated; eauto. subst vf; auto. apply sig_function_translated.
-  econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated.
+  econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto.
+  destruct H2 as [b [U V]]. subst vf. inv B. 
+  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. apply sig_function_translated; auto.
+  econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto.
   constructor; auto. apply call_cont_commut; auto.
-  (* Sbuiltin *)
+- (* Sbuiltin *)
   exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]].
   exploit external_call_mem_extends; eauto. 
   intros [vres' [m2 [A [B [C D]]]]].
@@ -605,77 +798,96 @@ Proof.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
   destruct optid; simpl; auto. apply set_var_lessdef; auto.
-  (* Seq *)
-  left; econstructor; split. constructor. constructor; auto. constructor; auto.
-  (* Sifthenelse *)
+- (* Seq *)
+  left; econstructor; split.
+  constructor. constructor; auto. constructor; auto.
+- (* Sifthenelse *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   assert (Val.bool_of_val v' b). inv B. auto. inv H0.
-  left; exists (State (sel_function hf ge f) (if b then sel_stmt hf ge s1 else sel_stmt hf ge s2) k' sp e' m'); split.
+  left; exists (State f' (if b then x else x0) k' sp e' m'); split.
   econstructor; eauto. eapply eval_condexpr_of_expr; eauto. 
   constructor; auto. destruct b; auto.
-  (* Sloop *)
-  left; econstructor; split. constructor. constructor; auto. constructor; auto.
-  (* Sblock *)
+- (* Sloop *)
+  left; econstructor; split. constructor. constructor; auto.
+  constructor; auto. simpl; rewrite EQ; auto.
+- (* Sblock *)
   left; econstructor; split. constructor. constructor; auto. constructor; auto.
-  (* Sexit seq *)
-  inv H7. left; econstructor; split. constructor. constructor; auto.
-  (* Sexit0 block *)
-  inv H7. left; econstructor; split. constructor. constructor; auto.
-  (* SexitS block *)
-  inv H7. left; econstructor; split. constructor. constructor; auto.
-  (* Sswitch *)
+- (* Sexit seq *)
+  inv MC. left; econstructor; split. constructor. constructor; auto.
+- (* Sexit0 block *)
+  inv MC. left; econstructor; split. constructor. constructor; auto.
+- (* SexitS block *)
+  inv MC. left; econstructor; split. constructor. constructor; auto.
+- (* Sswitch *)
+  inv H0; simpl in TS.
++ set (ct := compile_switch Int.modulus default cases) in *.
+  destruct (validate_switch Int.modulus default cases ct) eqn:VALID; inv TS.
+  exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
+  left; econstructor; split. 
+  econstructor. eapply sel_switch_int_correct; eauto. 
+  constructor; auto.
++ set (ct := compile_switch Int64.modulus default cases) in *.
+  destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS.
   exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
-  left; econstructor; split. econstructor; eauto. constructor; auto.
-  (* Sreturn None *)
+  left; econstructor; split.
+  econstructor. eapply sel_switch_long_correct; eauto. 
+  constructor; auto.
+- (* Sreturn None *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
+  erewrite <- stackspace_function_translated in P by eauto.
   left; econstructor; split. 
   econstructor. simpl; eauto. 
   constructor; auto. apply call_cont_commut; auto.
-  (* Sreturn Some *)
+- (* Sreturn Some *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
+  erewrite <- stackspace_function_translated in P by eauto.
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split. 
   econstructor; eauto.
   constructor; auto. apply call_cont_commut; auto.
-  (* Slabel *)
+- (* Slabel *)
   left; econstructor; split. constructor. constructor; auto.
-  (* Sgoto *)
+- (* Sgoto *)
+  assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')).
+  { monadInv TF; simpl; auto. }
   exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)).
-    apply call_cont_commut; eauto.
+    apply call_cont_commut; eauto. eauto.
   rewrite H. 
-  destruct (find_label lbl (sel_stmt hf ge (Cminor.fn_body f)) (call_cont k'0))
+  destruct (find_label lbl (fn_body f') (call_cont k'0))
   as [[s'' k'']|] eqn:?; intros; try contradiction.
-  destruct H0. 
+  destruct H1. 
   left; econstructor; split.
   econstructor; eauto. 
   constructor; auto.
-  (* internal function *)
+- (* internal function *)
+  monadInv TF. generalize EQ; intros TF; monadInv TF.
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
   intros [m2' [A B]].
   left; econstructor; split.
-  econstructor; eauto.
-  constructor; auto. apply set_locals_lessdef. apply set_params_lessdef; auto.
-  (* external call *)
+  econstructor; simpl; eauto.
+  constructor; simpl; auto. apply set_locals_lessdef. apply set_params_lessdef; auto.
+- (* external call *)
+  monadInv TF.
   exploit external_call_mem_extends; eauto. 
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
   econstructor. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
-  (* external call turned into a Sbuiltin *)
+- (* external call turned into a Sbuiltin *)
   exploit external_call_mem_extends; eauto. 
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
   econstructor. eauto. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
-  (* return *)
-  inv H2. 
+- (* return *)
+  inv MC. 
   left; econstructor; split. 
   econstructor. 
   constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
-  (* return of an external call turned into a Sbuiltin *)
-  right; split. omega. split. auto. constructor; auto. 
+- (* return of an external call turned into a Sbuiltin *)
+  right; split. simpl; omega. split. auto. constructor; auto. 
   destruct optid; simpl; auto. apply set_var_lessdef; auto.
 Qed.
 
@@ -684,11 +896,13 @@ Lemma sel_initial_states:
   exists R, initial_state tprog R /\ match_states S R.
 Proof.
   induction 1.
+  exploit function_ptr_translated; eauto. intros (f' & A & B).
   econstructor; split.
   econstructor.
-  apply Genv.init_mem_transf; eauto.
-  simpl. fold tge. rewrite symbols_preserved. eexact H0.
-  apply function_ptr_translated. eauto. 
+  eapply Genv.init_mem_transf_partial; eauto.
+  simpl. fold tge. rewrite symbols_preserved.
+  erewrite transform_partial_program_main by eauto. eexact H0.
+  eauto.
   rewrite <- H2. apply sig_function_translated; auto.
   constructor; auto. constructor. apply Mem.extends_refl.
 Qed.
@@ -697,7 +911,7 @@ Lemma sel_final_states:
   forall S R r,
   match_states S R -> Cminor.final_state S r -> final_state R r.
 Proof.
-  intros. inv H0. inv H. inv H3. inv H5. constructor.
+  intros. inv H0. inv H. inv MC. inv LD. constructor.
 Qed.
 
 End PRESERVATION.
@@ -712,10 +926,9 @@ Theorem transf_program_correct:
 Proof.
   intros. unfold sel_program in H. 
   destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate.
-  inv H.
-  eapply forward_simulation_opt.
-  apply symbols_preserved.
-  apply sel_initial_states.
-  apply sel_final_states.
-  apply sel_step_correct. apply helpers_correct_preserved. apply get_helpers_correct. auto.
+  apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). 
+  eapply symbols_preserved; eauto.
+  apply sel_initial_states; auto.
+  apply sel_final_states; auto.
+  apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto.
 Qed.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 75dd9d2..92004a2 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1933,17 +1933,184 @@ Proof.
   destruct 1; simpl; auto with va.
 Qed.
 
+(** Comparisons and variation intervals *)
+
+Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool :=
+  let (lo, hi) := i in
+  match c with
+  | Ceq => if zlt n lo || zlt hi n then Maybe false else Btop
+  | Cne => Btop
+  | Clt => if zlt hi n then Maybe true else if zle n lo then Maybe false else Btop
+  | Cle => if zle hi n then Maybe true else if zlt n lo then Maybe false else Btop
+  | Cgt => if zlt n lo then Maybe true else if zle hi n then Maybe false else Btop
+  | Cge => if zle n lo then Maybe true else if zlt hi n then Maybe false else Btop
+  end.
+
+Definition zcmp (c: comparison) (n1 n2: Z) : bool :=
+  match c with
+  | Ceq => zeq n1 n2
+  | Cne => negb (zeq n1 n2)
+  | Clt => zlt n1 n2
+  | Cle => zle n1 n2
+  | Cgt => zlt n2 n1
+  | Cge => zle n2 n1
+  end.
+
+Lemma zcmp_intv_sound:
+  forall c i x n,
+  fst i <= x <= snd i ->
+  cmatch (Some (zcmp c x n)) (cmp_intv c i n).
+Proof.
+  intros c [lo hi] x n; simpl; intros R.
+  destruct c; unfold zcmp, proj_sumbool.
+- (* eq *)
+  destruct (zlt n lo). rewrite zeq_false by omega. constructor. 
+  destruct (zlt hi n). rewrite zeq_false by omega. constructor.
+  constructor.
+- (* ne *)
+  constructor.
+- (* lt *)
+  destruct (zlt hi n). rewrite zlt_true by omega. constructor.
+  destruct (zle n lo). rewrite zlt_false by omega. constructor.
+  constructor.
+- (* le *)
+  destruct (zle hi n). rewrite zle_true by omega. constructor.
+  destruct (zlt n lo). rewrite zle_false by omega. constructor.
+  constructor.
+- (* gt *)
+  destruct (zlt n lo). rewrite zlt_true by omega. constructor.
+  destruct (zle hi n). rewrite zlt_false by omega. constructor.
+  constructor.
+- (* ge *)
+  destruct (zle n lo). rewrite zle_true by omega. constructor.
+  destruct (zlt hi n). rewrite zle_false by omega. constructor.
+  constructor.
+Qed.
+
+Lemma cmp_intv_None:
+  forall c i n, cmatch None (cmp_intv c i n).
+Proof.
+  unfold cmp_intv; intros. destruct i as [lo hi].
+  destruct c.
+- (* eq *)
+  destruct (zlt n lo). constructor. destruct (zlt hi n); constructor.
+- (* ne *)
+  constructor.
+- (* lt *)
+  destruct (zlt hi n). constructor. destruct (zle n lo); constructor.
+- (* le *)
+  destruct (zle hi n). constructor. destruct (zlt n lo); constructor.
+- (* gt *)
+  destruct (zlt n lo). constructor. destruct (zle hi n); constructor.
+- (* ge *)
+  destruct (zle n lo). constructor. destruct (zlt hi n); constructor.
+Qed.
+
+Definition uintv (v: aval) : Z * Z :=
+  match v with
+  | I n => (Int.unsigned n, Int.unsigned n)
+  | Uns n => if zlt n Int.zwordsize then (0, two_p n - 1) else (0, Int.max_unsigned)
+  | _ => (0, Int.max_unsigned)
+  end.
+
+Lemma uintv_sound:
+  forall n v, vmatch (Vint n) v -> fst (uintv v) <= Int.unsigned n <= snd (uintv v).
+Proof.
+  intros. inv H; simpl; try (apply Int.unsigned_range_2).
+- omega.
+- destruct (zlt n0 Int.zwordsize); simpl.
++ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega. 
+  exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. omega.
++ apply Int.unsigned_range_2.
+Qed.
+
+Lemma cmpu_intv_sound:
+  forall valid c n1 v1 n2,
+  vmatch (Vint n1) v1 ->
+  cmatch (Val.cmpu_bool valid c (Vint n1) (Vint n2)) (cmp_intv c (uintv v1) (Int.unsigned n2)).
+Proof.
+  intros. simpl. replace (Int.cmpu c n1 n2) with (zcmp c (Int.unsigned n1) (Int.unsigned n2)).
+  apply zcmp_intv_sound; apply uintv_sound; auto.
+  destruct c; simpl; auto.
+  unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
+  unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
+Qed.
+
+Lemma cmpu_intv_sound_2:
+  forall valid c n1 v1 n2,
+  vmatch (Vint n1) v1 ->
+  cmatch (Val.cmpu_bool valid c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (uintv v1) (Int.unsigned n2)).
+Proof.
+  intros. rewrite <- Val.swap_cmpu_bool. apply cmpu_intv_sound; auto. 
+Qed.
+
+Definition sintv (v: aval) : Z * Z :=
+  match v with
+  | I n => (Int.signed n, Int.signed n)
+  | Uns n =>
+      if zlt n Int.zwordsize then (0, two_p n - 1) else (Int.min_signed, Int.max_signed)
+  | Sgn n =>
+      if zlt n Int.zwordsize
+      then (let x := two_p (n-1) in (-x, x-1))
+      else (Int.min_signed, Int.max_signed)
+  | _ => (Int.min_signed, Int.max_signed)
+  end.
+
+Lemma sintv_sound:
+  forall n v, vmatch (Vint n) v -> fst (sintv v) <= Int.signed n <= snd (sintv v).
+Proof.
+  intros. inv H; simpl; try (apply Int.signed_range).
+- omega.
+- destruct (zlt n0 Int.zwordsize); simpl.
++ rewrite is_uns_zero_ext in H2. rewrite <- H2. 
+  assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; omega).
+  exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros.
+  replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)).
+  rewrite H. omega. 
+  unfold Int.signed. rewrite zlt_true. auto. 
+  assert (two_p n0 <= Int.half_modulus). 
+  { change Int.half_modulus with (two_p (Int.zwordsize - 1)). 
+    apply two_p_monotone. omega. }
+  omega.  
++ apply Int.signed_range.
+- destruct (zlt n0 (Int.zwordsize)); simpl.
++ rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2. 
+  exploit (Int.sign_ext_range n0 n). omega. omega. 
++ apply Int.signed_range.
+Qed.
+
+Lemma cmp_intv_sound:
+  forall c n1 v1 n2,
+  vmatch (Vint n1) v1 ->
+  cmatch (Val.cmp_bool c (Vint n1) (Vint n2)) (cmp_intv c (sintv v1) (Int.signed n2)).
+Proof.
+  intros. simpl. replace (Int.cmp c n1 n2) with (zcmp c (Int.signed n1) (Int.signed n2)).
+  apply zcmp_intv_sound; apply sintv_sound; auto.
+  destruct c; simpl; rewrite ? Int.eq_signed; auto.
+  unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
+  unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega.
+Qed.
+
+Lemma cmp_intv_sound_2:
+  forall c n1 v1 n2,
+  vmatch (Vint n1) v1 ->
+  cmatch (Val.cmp_bool c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (sintv v1) (Int.signed n2)).
+Proof.
+  intros. rewrite <- Val.swap_cmp_bool. apply cmp_intv_sound; auto. 
+Qed. 
+
 (** Comparisons *)
 
 Definition cmpu_bool (c: comparison) (v w: aval) : abool :=
   match v, w with
   | I i1, I i2 => Just (Int.cmpu c i1 i2)
-(* there are cute things to do with Uns/Sgn compared against an integer *)
   | Ptr _, (I _ | Uns _ | Sgn _) => cmp_different_blocks c
   | (I _ | Uns _ | Sgn _), Ptr _ => cmp_different_blocks c
   | Ptr p1, Ptr p2 => pcmp c p1 p2
   | Ptr p1, Ifptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c)
   | Ifptr p1, Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c)
+  | _, I i => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c)
+  | I i, _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c)
   | _, _ => Btop
   end.
 
@@ -1961,22 +2128,28 @@ Proof.
   {
     intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none.
   }
-  unfold cmpu_bool; inv H; inv H0;
+  unfold cmpu_bool; inversion H; subst; inversion H0; subst;
   auto using cmatch_top, cmp_different_blocks_none, pcmp_none,
-             cmatch_lub_l, cmatch_lub_r, pcmp_sound.
+             cmatch_lub_l, cmatch_lub_r, pcmp_sound,
+             cmpu_intv_sound, cmpu_intv_sound_2, cmp_intv_None.
 - constructor.
 Qed.
 
 Definition cmp_bool (c: comparison) (v w: aval) : abool :=
   match v, w with
   | I i1, I i2 => Just (Int.cmp c i1 i2)
+  | _, I i => cmp_intv c (sintv v) (Int.signed i)
+  | I i, _ => cmp_intv (swap_comparison c) (sintv w) (Int.signed i)
   | _, _ => Btop
   end.
 
 Lemma cmp_bool_sound:
   forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmp_bool c v w) (cmp_bool c x y).
 Proof.
-  intros. inv H; try constructor; inv H0; constructor. 
+  intros. 
+  unfold cmp_bool; inversion H; subst; inversion H0; subst;
+  auto using cmatch_top, cmp_intv_sound, cmp_intv_sound_2, cmp_intv_None.
+- constructor.
 Qed.
 
 Definition cmpf_bool (c: comparison) (v w: aval) : abool :=
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. 
diff --git a/common/Switch.v b/common/Switch.v
index 3e25851..4723f50 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -20,45 +20,27 @@ Require Import EqNat.
 Require Import Coqlib.
 Require Import Maps.
 Require Import Integers.
-
-Module IntIndexed <: INDEXED_TYPE.
-
-  Definition t := int.
-
-  Definition index (n: int) : positive :=
-    match Int.unsigned n with
-    | Z0 => xH
-    | Zpos p => xO p
-    | Zneg p => xI p  (**r never happens *)
-    end.
-
-  Lemma index_inj: forall n m, index n = index m -> n = m.
-  Proof.
-    unfold index; intros. 
-    rewrite <- (Int.repr_unsigned n). rewrite <- (Int.repr_unsigned m).
-    f_equal. 
-    destruct (Int.unsigned n); destruct (Int.unsigned m); congruence.
-  Qed.
-
-  Definition eq := Int.eq_dec.
-
-End IntIndexed.
-
-Module IntMap := IMap(IntIndexed).
+Require Import Values.
 
 (** A multi-way branch is composed of a list of (key, action) pairs,
   plus a default action.  *)
 
-Definition table : Type := list (int * nat).
+Definition table : Type := list (Z * nat).
 
-Fixpoint switch_target (n: int) (dfl: nat) (cases: table)
+Fixpoint switch_target (n: Z) (dfl: nat) (cases: table)
                        {struct cases} : nat :=
   match cases with
   | nil => dfl
   | (key, action) :: rem =>
-      if Int.eq n key then action else switch_target n dfl rem
+      if zeq n key then action else switch_target n dfl rem
   end.
 
+Inductive switch_argument: bool -> val -> Z -> Prop :=
+  | switch_argument_32: forall i,
+      switch_argument false (Vint i) (Int.unsigned i)
+  | switch_argument_64: forall i,
+      switch_argument true (Vlong i) (Int64.unsigned i).
+
 (** Multi-way branches are translated to comparison trees.
     Each node of the tree performs either
 - an equality against one of the keys;
@@ -66,21 +48,27 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table)
 - or a computed branch (jump table) against a range of key values. *)
 
 Inductive comptree : Type :=
-  | CTaction: nat -> comptree
-  | CTifeq: int -> nat -> comptree -> comptree
-  | CTiflt: int -> comptree -> comptree -> comptree
-  | CTjumptable: int -> int -> list nat -> comptree -> comptree.
+  | CTaction (act: nat)
+  | CTifeq (key: Z) (act: nat) (cne: comptree)
+  | CTiflt (key: Z) (clt: comptree) (cge: comptree)
+  | CTjumptable (ofs: Z) (sz: Z) (acts: list nat) (cother: comptree).
+
+Section COMPTREE.
 
-Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat :=
+Variable modulus: Z.
+Hypothesis modulus_pos: modulus > 0.
+
+Fixpoint comptree_match (n: Z) (t: comptree) {struct t}: option nat :=
   match t with
   | CTaction act => Some act
   | CTifeq key act t' =>
-      if Int.eq n key then Some act else comptree_match n t'
+      if zeq n key then Some act else comptree_match n t'
   | CTiflt key t1 t2 =>
-      if Int.ltu n key then comptree_match n t1 else comptree_match n t2
+      if zlt n key then comptree_match n t1 else comptree_match n t2
   | CTjumptable ofs sz tbl t' =>
-      if Int.ltu (Int.sub n ofs) sz
-      then list_nth_z tbl (Int.unsigned (Int.sub n ofs))
+      let delta := (n - ofs) mod modulus in
+      if zlt delta sz
+      then list_nth_z tbl (delta mod Int.modulus)
       else comptree_match n t'
   end.
 
@@ -91,36 +79,36 @@ Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat :=
   and prove correct Coq functions that take a table and a comparison
   tree, and check that their semantics are equivalent. *)
 
-Fixpoint split_lt (pivot: int) (cases: table)
+Fixpoint split_lt (pivot: Z) (cases: table)
                   {struct cases} : table * table :=
   match cases with
   | nil => (nil, nil)
   | (key, act) :: rem =>
       let (l, r) := split_lt pivot rem in
-      if Int.ltu key pivot
+      if zlt key pivot
       then ((key, act) :: l, r)
       else (l, (key, act) :: r)
   end.
 
-Fixpoint split_eq (pivot: int) (cases: table)
+Fixpoint split_eq (pivot: Z) (cases: table)
                   {struct cases} : option nat * table :=
   match cases with
   | nil => (None, nil)
   | (key, act) :: rem =>
       let (same, others) := split_eq pivot rem in
-      if Int.eq key pivot
+      if zeq key pivot
       then (Some act, others)
       else (same, (key, act) :: others)
   end.
 
-Fixpoint split_between (dfl: nat) (ofs sz: int) (cases: table)
-                       {struct cases} : IntMap.t nat * table :=
+Fixpoint split_between (dfl: nat) (ofs sz: Z) (cases: table)
+                       {struct cases} : ZMap.t nat * table :=
   match cases with
-  | nil => (IntMap.init dfl, nil)
+  | nil => (ZMap.init dfl, nil)
   | (key, act) :: rem =>
       let (inside, outside) := split_between dfl ofs sz rem in
-      if Int.ltu (Int.sub key ofs) sz
-      then (IntMap.set key act inside, outside)
+      if zlt ((key - ofs) mod modulus) sz
+      then (ZMap.set key act inside, outside)
       else (inside, (key, act) :: outside)
   end.
 
@@ -130,13 +118,13 @@ Definition refine_low_bound (v lo: Z) :=
 Definition refine_high_bound (v hi: Z) :=
   if zeq v hi then hi - 1 else hi.
 
-Fixpoint validate_jumptable (cases: IntMap.t nat) 
-                            (tbl: list nat) (n: int) {struct tbl} : bool :=
+Fixpoint validate_jumptable (cases: ZMap.t nat) 
+                            (tbl: list nat) (n: Z) {struct tbl} : bool :=
   match tbl with
   | nil => true
   | act :: rem =>
-      beq_nat act (IntMap.get n cases)
-      && validate_jumptable cases rem (Int.add n Int.one)
+      beq_nat act (ZMap.get n cases)
+      && validate_jumptable cases rem (Zsucc n)
   end.
 
 Fixpoint validate (default: nat) (cases: table) (t: comptree)
@@ -147,211 +135,217 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree)
       | nil =>
           beq_nat act default
       | (key1, act1) :: _ =>
-          zeq (Int.unsigned key1) lo && zeq lo hi && beq_nat act act1
+          zeq key1 lo && zeq lo hi && beq_nat act act1
       end
   | CTifeq pivot act t' =>
+      zle 0 pivot && zlt pivot modulus &&
       match split_eq pivot cases with
       | (None, _) =>
           false
       | (Some act', others) =>
           beq_nat act act' 
           && validate default others t'
-                      (refine_low_bound (Int.unsigned pivot) lo)
-                      (refine_high_bound (Int.unsigned pivot) hi)
+                      (refine_low_bound pivot lo)
+                      (refine_high_bound pivot hi)
       end
   | CTiflt pivot t1 t2 =>
+      zle 0 pivot && zlt pivot modulus &&
       match split_lt pivot cases with
       | (lcases, rcases) =>
-          validate default lcases t1 lo (Int.unsigned pivot - 1)
-          && validate default rcases t2 (Int.unsigned pivot) hi
+          validate default lcases t1 lo (pivot - 1)
+          && validate default rcases t2 pivot hi
       end
   | CTjumptable ofs sz tbl t' =>
       let tbl_len := list_length_z tbl in
+      zle 0 ofs && zle 0 sz && zlt (ofs + sz) modulus &&
+      zle sz tbl_len && zlt sz Int.modulus &&
       match split_between default ofs sz cases with
       | (inside, outside) =>
-          zle (Int.unsigned sz) tbl_len
-          && zle tbl_len Int.max_signed
-          && validate_jumptable inside tbl ofs
+          validate_jumptable inside tbl ofs
           && validate default outside t' lo hi
      end
   end.
 
 Definition validate_switch (default: nat) (cases: table) (t: comptree) :=
-  validate default cases t 0 Int.max_unsigned.
+  validate default cases t 0 (modulus - 1).
+
+(** Structural properties checked by validation *)
+
+Inductive wf_comptree: comptree -> Prop :=
+  | wf_action: forall act,
+      wf_comptree (CTaction act)
+  | wf_ifeq: forall key act cne,
+      0 <= key < modulus -> wf_comptree cne -> wf_comptree (CTifeq key act cne)
+  | wf_iflt: forall key clt cge,
+      0 <= key < modulus -> wf_comptree clt -> wf_comptree cge -> wf_comptree (CTiflt key clt cge)
+  | wf_jumptable: forall ofs sz acts cother,
+      0 <= ofs < modulus -> 0 <= sz < modulus ->
+      wf_comptree cother ->
+      wf_comptree (CTjumptable ofs sz acts cother).
+
+Lemma validate_wf:
+  forall default t cases lo hi,
+  validate default cases t lo hi = true ->
+  wf_comptree t.
+Proof.
+  induction t; simpl; intros; InvBooleans.
+- constructor.
+- destruct (split_eq key cases) as [[act'|] others]; try discriminate; InvBooleans.
+  constructor; eauto.  
+- destruct (split_lt key cases) as [lc rc]; InvBooleans.
+  constructor; eauto.
+- destruct (split_between default ofs sz cases) as [ins out]; InvBooleans. 
+  constructor; eauto; omega.
+Qed.
 
-(** Correctness proof for validation. *)
+(** Semantic correctness proof for validation. *)
 
 Lemma split_eq_prop:
   forall v default n cases optact cases',
   split_eq n cases = (optact, cases') ->
   switch_target v default cases =
-   (if Int.eq v n
+   (if zeq v n
     then match optact with Some act => act | None => default end
     else switch_target v default cases').
 Proof.
   induction cases; simpl; intros until cases'.
-  intros. inversion H; subst. simpl. 
-  destruct (Int.eq v n); auto.
-  destruct a as [key act]. 
-  case_eq (split_eq n cases). intros same other SEQ.
-  rewrite (IHcases _ _ SEQ).
-  predSpec Int.eq Int.eq_spec key n; intro EQ; inversion EQ; simpl.
-  subst n. destruct (Int.eq v key). auto. auto.
-  predSpec Int.eq Int.eq_spec v key. 
-  subst v. predSpec Int.eq Int.eq_spec key n. congruence. auto.
-  auto.
+- intros. inv H. simpl. destruct (zeq v n); auto.
+- destruct a as [key act].
+  destruct (split_eq n cases) as [same other] eqn:SEQ.
+  rewrite (IHcases same other) by auto. 
+  destruct (zeq key n); intros EQ; inv EQ.
++ destruct (zeq v n); auto. 
++ simpl. destruct (zeq v key). 
+  * subst v. rewrite zeq_false by auto. auto.
+  * auto.
 Qed.
 
 Lemma split_lt_prop:
   forall v default n cases lcases rcases,
   split_lt n cases = (lcases, rcases) ->
   switch_target v default cases =
-    (if Int.ltu v n
+    (if zlt v n
      then switch_target v default lcases
      else switch_target v default rcases).
 Proof.
   induction cases; intros until rcases; simpl.
-  intro. inversion H; subst. simpl.
-  destruct (Int.ltu v n); auto.
-  destruct a as [key act]. 
-  case_eq (split_lt n cases). intros lc rc SEQ.
-  rewrite (IHcases _ _ SEQ).
-  case_eq (Int.ltu key n); intros; inv H0; simpl.
-  predSpec Int.eq Int.eq_spec v key. 
-  subst v. rewrite H. auto.
-  auto.
-  predSpec Int.eq Int.eq_spec v key. 
-  subst v. rewrite H. auto.
-  auto.
+- intros. inv H. simpl. destruct (zlt v n); auto.
+- destruct a as [key act]. 
+  destruct (split_lt n cases) as [lc rc] eqn:SEQ.
+  rewrite (IHcases lc rc) by auto.
+  destruct (zlt key n); intros EQ; inv EQ; simpl.
++ destruct (zeq v key). rewrite zlt_true by omega. auto. auto.
++ destruct (zeq v key). rewrite zlt_false by omega. auto. auto.
 Qed.
 
 Lemma split_between_prop:
   forall v default ofs sz cases inside outside,
   split_between default ofs sz cases = (inside, outside) ->
   switch_target v default cases =
-    (if Int.ltu (Int.sub v ofs) sz
-     then IntMap.get v inside
+    (if zlt ((v - ofs) mod modulus) sz
+     then ZMap.get v inside
      else switch_target v default outside).
 Proof.
   induction cases; intros until outside; simpl; intros SEQ.
-- inv SEQ. destruct (Int.ltu (Int.sub v ofs) sz); auto. rewrite IntMap.gi. auto.
-- destruct a as [key act].
+- inv SEQ. rewrite ZMap.gi. simpl. destruct (zlt ((v - ofs) mod modulus) sz); auto.
+- destruct a as [key act]. 
   destruct (split_between default ofs sz cases) as [ins outs].
-  erewrite IHcases; eauto. 
-  destruct (Int.ltu (Int.sub key ofs) sz) eqn:LT; inv SEQ.
-  + predSpec Int.eq Int.eq_spec v key. 
-    subst v. rewrite LT. rewrite IntMap.gss. auto. 
-    destruct (Int.ltu (Int.sub v ofs) sz). 
-    rewrite IntMap.gso; auto.
-    auto.
-  + simpl. destruct (Int.ltu (Int.sub v ofs) sz) eqn:LT'. 
-    rewrite Int.eq_false. auto. congruence. 
-    auto.
+  erewrite IHcases; eauto.
+  destruct (zlt ((key - ofs) mod modulus) sz); inv SEQ.
++ rewrite ZMap.gsspec. unfold ZIndexed.eq.
+  destruct (zeq v key).
+  subst v. rewrite zlt_true by auto. auto.
+  auto.
++ simpl. destruct (zeq v key). 
+  subst v. rewrite zlt_false by auto. auto.
+  auto.
 Qed.
 
 Lemma validate_jumptable_correct_rec:
   forall cases tbl base v,
   validate_jumptable cases tbl base = true ->
-  0 <= Int.unsigned v < list_length_z tbl ->
-  list_nth_z tbl (Int.unsigned v) = Some(IntMap.get (Int.add base v) cases).
+  0 <= v < list_length_z tbl ->
+  list_nth_z tbl v = Some(ZMap.get (base + v) cases).
 Proof.
-  induction tbl; intros until v; simpl.
-  unfold list_length_z; simpl. intros. omegaContradiction.
-  rewrite list_length_z_cons. intros. destruct (andb_prop _ _ H). clear H.
-  generalize (beq_nat_eq _ _ (sym_equal H1)). clear H1. intro. subst a.
-  destruct (zeq (Int.unsigned v) 0).
-  unfold Int.add. rewrite e. rewrite Zplus_0_r. rewrite Int.repr_unsigned. auto.
-  assert (Int.unsigned (Int.sub v Int.one) = Int.unsigned v - 1).
-    unfold Int.sub. change (Int.unsigned Int.one) with 1. 
-    apply Int.unsigned_repr. split. omega.
-    generalize (Int.unsigned_range_2 v). omega.
-  replace (Int.add base v) with (Int.add (Int.add base Int.one) (Int.sub v Int.one)).
-  rewrite <- IHtbl. rewrite H. auto. auto. rewrite H. omega. 
-  rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite Int.add_assoc. 
-  replace (Int.add Int.one (Int.neg Int.one)) with Int.zero.
-  rewrite Int.add_zero. apply Int.add_commut.
-  rewrite Int.add_neg_zero; auto.
+  induction tbl; simpl; intros.
+- unfold list_length_z in H0. simpl in H0. omegaContradiction.
+- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. 
+  destruct (zeq v 0).
+  + replace (base + v) with base by omega. congruence.
+  + replace (base + v) with (Z.succ base + Z.pred v) by omega. 
+    apply IHtbl. auto. omega. 
 Qed.
 
 Lemma validate_jumptable_correct:
   forall cases tbl ofs v sz,
   validate_jumptable cases tbl ofs = true ->
-  Int.ltu (Int.sub v ofs) sz = true ->
-  Int.unsigned sz <= list_length_z tbl ->
-  list_nth_z tbl (Int.unsigned (Int.sub v ofs)) = Some(IntMap.get v cases).
+  (v - ofs) mod modulus < sz ->
+  0 <= sz -> 0 <= ofs -> ofs + sz < modulus ->
+  0 <= v < modulus ->
+  sz <= list_length_z tbl ->
+  list_nth_z tbl ((v - ofs) mod modulus) = Some(ZMap.get v cases).
 Proof.
   intros.
-  exploit Int.ltu_inv; eauto. intros. 
-  rewrite (validate_jumptable_correct_rec cases tbl ofs).
-  rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite <- Int.sub_add_opp. 
-  rewrite Int.sub_idem. rewrite Int.add_zero. auto. 
-  auto.
-  omega. 
+  rewrite (validate_jumptable_correct_rec cases tbl ofs); auto.
+- f_equal. f_equal. rewrite Zmod_small. omega. 
+  destruct (zle ofs v). omega. 
+  assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus).
+  { rewrite Zmod_small. omega. omega. }
+  rewrite Z_mod_plus in M by auto. rewrite M in H0. omega.
+- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. 
 Qed.
 
 Lemma validate_correct_rec:
-  forall default v t cases lo hi,
+  forall default v,
+  0 <= v < modulus ->
+  forall t cases lo hi,
   validate default cases t lo hi = true ->
-  lo <= Int.unsigned v <= hi ->
+  lo <= v <= hi ->
   comptree_match v t = Some (switch_target v default cases).
 Proof.
-Opaque Int.sub.
-  induction t; simpl; intros until hi.
-  (* base case *)
+  intros default v VRANGE. induction t; simpl; intros until hi.
+- (* base case *)
   destruct cases as [ | [key1 act1] cases1]; intros.
-  replace n with default. reflexivity. 
-  symmetry. apply beq_nat_eq. auto.
-  destruct (andb_prop _ _ H). destruct (andb_prop _ _ H1). clear H H1.
-  assert (Int.unsigned key1 = lo). eapply proj_sumbool_true; eauto.
-  assert (lo = hi). eapply proj_sumbool_true; eauto.
-  assert (Int.unsigned v = Int.unsigned key1). omega.
-  replace n with act1.
-  simpl. unfold Int.eq. rewrite H5. rewrite zeq_true. auto.
-  symmetry. apply beq_nat_eq. auto.
-  (* eq node *)
-  case_eq (split_eq i cases). intros optact cases' EQ. 
-  destruct optact as [ act | ]. 2: congruence.
-  intros. destruct (andb_prop _ _ H). clear H.
++ apply beq_nat_true in H. subst act. reflexivity. 
++ InvBooleans. apply beq_nat_true in H2. subst. simpl. 
+  destruct (zeq v hi). auto. omegaContradiction.
+- (* eq node *)
+  destruct (split_eq key cases) as [optact others] eqn:EQ. intros.
+  destruct optact as [act1|]; InvBooleans; try discriminate.
+  apply beq_nat_true in H.
   rewrite (split_eq_prop v default _ _ _ _ EQ).
-  predSpec Int.eq Int.eq_spec v i.
-  f_equal. apply beq_nat_eq; auto.
-  eapply IHt. eauto.
-  assert (Int.unsigned v <> Int.unsigned i).
-    rewrite <- (Int.repr_unsigned v) in H.
-    rewrite <- (Int.repr_unsigned i) in H.
-    congruence.
-  split.
-  unfold refine_low_bound. destruct (zeq (Int.unsigned i) lo); omega.
-  unfold refine_high_bound. destruct (zeq (Int.unsigned i) hi); omega.
-  (* lt node *)
-  case_eq (split_lt i cases). intros lcases rcases EQ V RANGE.
-  destruct (andb_prop _ _ V). clear V.
-  rewrite (split_lt_prop v default _ _ _ _ EQ). 
-  unfold Int.ltu. destruct (zlt (Int.unsigned v) (Int.unsigned i)).
+  destruct (zeq v key). 
+  + congruence.
+  + eapply IHt; eauto. 
+    unfold refine_low_bound, refine_high_bound. split.
+    destruct (zeq key lo); omega. 
+    destruct (zeq key hi); omega.
+- (* lt node *)
+  destruct (split_lt key cases) as [lcases rcases] eqn:EQ; intros; InvBooleans.
+  rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key). 
   eapply IHt1. eauto. omega.
   eapply IHt2. eauto. omega.
-  (* jumptable node *)
-  case_eq (split_between default i i0 cases). intros ins outs EQ V RANGE.
-  destruct (andb_prop _ _ V). clear V.
-  destruct (andb_prop _ _ H). clear H.
-  destruct (andb_prop _ _ H1). clear H1.
+- (* jumptable node *)
+  destruct (split_between default ofs sz cases) as [ins outs] eqn:EQ; intros; InvBooleans.
   rewrite (split_between_prop v _ _ _ _ _ _ EQ).
-  case_eq (Int.ltu (Int.sub v i) i0); intros.
-  eapply validate_jumptable_correct; eauto. 
-  eapply proj_sumbool_true; eauto.
+  assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega).
+  destruct (zlt ((v - ofs) mod modulus) sz).
+  rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto.  
   eapply IHt; eauto. 
 Qed.
 
 Definition table_tree_agree
     (default: nat) (cases: table) (t: comptree) : Prop :=
-  forall v, comptree_match v t = Some(switch_target v default cases).
+  forall v, 0 <= v < modulus -> comptree_match v t = Some(switch_target v default cases).
 
 Theorem validate_switch_correct:
   forall default t cases,
   validate_switch default cases t = true ->
-  table_tree_agree default cases t.
+  wf_comptree t /\ table_tree_agree default cases t.
 Proof.
-  unfold validate_switch, table_tree_agree; intros.
-  eapply validate_correct_rec; eauto. 
-  apply Int.unsigned_range_2.
+  unfold validate_switch, table_tree_agree; split.
+  eapply validate_wf; eauto. 
+  intros; eapply validate_correct_rec; eauto. omega. 
 Qed.
+
+End COMPTREE.
diff --git a/common/Switchaux.ml b/common/Switchaux.ml
new file mode 100644
index 0000000..15480ae
--- /dev/null
+++ b/common/Switchaux.ml
@@ -0,0 +1,99 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Datatypes
+open Camlcoq
+open Switch
+
+(* Compiling a switch table into a decision tree *)
+
+module ZSet = Set.Make(Z)
+
+let normalize_table tbl =
+  let rec norm keys accu = function
+  | [] -> (accu, keys)
+  | (key, act) :: rem ->
+      if ZSet.mem key keys
+      then norm keys accu rem
+      else norm (ZSet.add key keys) ((key, act) :: accu) rem
+  in norm ZSet.empty [] tbl
+
+let compile_switch_as_tree modulus default tbl =
+  let sw = Array.of_list tbl in
+  Array.stable_sort (fun (n1, _) (n2, _) -> Z.compare n1 n2) sw;
+  let rec build lo hi minval maxval =
+    match hi - lo with
+    | 0 ->
+       CTaction default
+    | 1 ->
+       let (key, act) = sw.(lo) in
+       if Z.sub maxval minval = Z.zero
+       then CTaction act
+       else CTifeq(key, act, CTaction default)
+    | 2 ->
+       let (key1, act1) = sw.(lo)
+       and (key2, act2) = sw.(lo+1) in
+       CTifeq(key1, act1,
+         if Z.sub maxval minval = Z.one
+         then CTaction act2
+         else CTifeq(key2, act2, CTaction default))
+    | 3 ->
+       let (key1, act1) = sw.(lo)
+       and (key2, act2) = sw.(lo+1)
+       and (key3, act3) = sw.(lo+2) in
+       CTifeq(key1, act1, 
+        CTifeq(key2, act2,
+          if Z.sub maxval minval = Z.of_uint 2
+          then CTaction act3
+          else CTifeq(key3, act3, CTaction default)))
+    | _ ->
+       let mid = (lo + hi) / 2 in
+       let (pivot, _) = sw.(mid) in
+       CTiflt(pivot,
+              build lo mid minval (Z.sub pivot Z.one),
+              build mid hi pivot maxval)
+  in build 0 (Array.length sw) Z.zero modulus
+
+let compile_switch_as_jumptable default cases minkey maxkey =
+  let tblsize = 1 + Z.to_int (Z.sub maxkey minkey) in
+  assert (tblsize >= 0 && tblsize <= Sys.max_array_length);
+  let tbl = Array.make tblsize default in
+  List.iter
+    (fun (key, act) ->
+       let pos = Z.to_int (Z.sub key minkey) in
+       tbl.(pos) <- act)
+    cases;
+  CTjumptable(minkey,
+              Z.of_uint tblsize,
+              Array.to_list tbl,
+              CTaction default)
+
+let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) =
+  let span = Z.sub maxkey minkey in
+  assert (Z.ge span Z.zero);
+  let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases)
+  and table_size = Z.add (Z.of_uint 8) span in
+  numcases >= 7           (* small jump tables are always less efficient *)
+  && Z.le table_size tree_size
+  && Z.lt span (Z.of_uint Sys.max_array_length)
+
+let compile_switch modulus default table =
+  let (tbl, keys) = normalize_table table in
+  if ZSet.is_empty keys then CTaction default else begin
+    let minkey = ZSet.min_elt keys
+    and maxkey = ZSet.max_elt keys in
+    if dense_enough (List.length tbl) minkey maxkey
+    then compile_switch_as_jumptable default tbl minkey maxkey
+    else compile_switch_as_tree modulus default tbl
+  end
+
+
diff --git a/extraction/extraction.v b/extraction/extraction.v
index d987629..a097bdb 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -16,6 +16,7 @@ Require AST.
 Require Iteration.
 Require Floats.
 Require SelectLong.
+Require Selection.
 Require RTLgen.
 Require Inlining.
 Require ValueDomain.
@@ -62,9 +63,9 @@ Extract Constant SelectLong.get_helper =>
 Extract Constant SelectLong.get_builtin =>
   "fun s sg ->
      Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))".
+Extract Constant Selection.compile_switch => "Switchaux.compile_switch".
 
 (* RTLgen *)
-Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch".
 Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely".
 Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2.
 
@@ -133,7 +134,7 @@ Load extractionMachdep.
 (* Avoid name clashes *)
 Extraction Blacklist List String Int.
 
-(* Cutting the dependancy to R. *)
+(* Cutting the dependency to R. *)
 Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false".
 Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false".
 Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false".