Amelioration compilation des switch

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 25 insertions, 12 deletions

diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
index 826f9887..d9203808 100644
--- a/caml/RTLgenaux.ml
+++ b/caml/RTLgenaux.ml
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open Camlcoq
 open Switch
 open CminorSel
 
@@ -37,23 +38,35 @@ let normalize_table tbl =
 let compile_switch default table =
   let sw = Array.of_list (normalize_table table) in
   Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw;
-  let rec build lo hi =
+  let rec build lo hi minval maxval =
     match hi - lo with
     | 0 ->
        CTaction default
     | 1 ->
-       CTifeq(fst sw.(lo), snd sw.(lo), CTaction default)
+       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 ->
-       CTifeq(fst sw.(lo), snd sw.(lo),
-       CTifeq(fst sw.(lo+1), snd sw.(lo+1),
-       CTaction default))
+       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 ->
-       CTifeq(fst sw.(lo), snd sw.(lo),
-       CTifeq(fst sw.(lo+1), snd sw.(lo+1),
-       CTifeq(fst sw.(lo+2), snd sw.(lo+2),
-       CTaction default)))
+       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
-       CTiflt(fst sw.(mid), build lo mid, build mid hi)
-  in build 0 (Array.length sw)
-
+       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