- 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

2 files changed, 264 insertions, 171 deletions

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
+
+