From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Aug 2014 07:52:12 +0000 Subject: - 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 --- common/Switch.v | 336 ++++++++++++++++++++++++++-------------------------- common/Switchaux.ml | 99 ++++++++++++++++ 2 files changed, 264 insertions(+), 171 deletions(-) create mode 100644 common/Switchaux.ml (limited to 'common') 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 + + -- cgit v1.2.3