- 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

13 files changed, 845 insertions, 479 deletions

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 :=