From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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
---
 backend/RTLgenaux.ml | 102 +++++----------------------------------------------
 1 file changed, 9 insertions(+), 93 deletions(-)

(limited to 'backend/RTLgenaux.ml')

diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 75901027..27a4908e 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
-- 
cgit