Amelioration compilation des switch

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

3 files changed, 96 insertions, 42 deletions

diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
index 826f988..d920380 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
diff --git a/common/Switch.v b/common/Switch.v
index d98ecaa..8124aea 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -80,26 +80,43 @@ Fixpoint split_eq (pivot: int) (cases: table)
       else (same, (key, act) :: others)
   end.
 
-Fixpoint validate_switch (default: nat) (cases: table) (t: comptree)
-                  {struct t} : bool :=
+Definition refine_low_bound (v lo: Z) :=
+  if zeq v lo then lo + 1 else lo.
+
+Definition refine_high_bound (v hi: Z) :=
+  if zeq v hi then hi - 1 else hi.
+
+Fixpoint validate (default: nat) (cases: table) (t: comptree)
+                  (lo hi: Z) {struct t} : bool :=
   match t with
   | CTaction act =>
       match cases with
-      | nil => beq_nat act default
-      | _ => false
+      | nil =>
+          beq_nat act default
+      | (key1, act1) :: _ =>
+          zeq (Int.unsigned key1) lo && zeq lo hi && beq_nat act act1
       end
   | CTifeq pivot act t' =>
       match split_eq pivot cases with
-      | (None, _) => false
-      | (Some act', others) => beq_nat act act' && validate_switch default others t'
+      | (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)
       end
   | CTiflt pivot t1 t2 =>
       match split_lt pivot cases with
       | (lcases, rcases) =>
-          validate_switch default lcases t1 && validate_switch default rcases t2
+          validate default lcases t1 lo (Int.unsigned pivot - 1)
+          && validate default rcases t2 (Int.unsigned pivot) hi
       end
   end.
 
+Definition validate_switch (default: nat) (cases: table) (t: comptree) :=
+  validate default cases t 0 Int.max_unsigned.
+
 (** Correctness proof for validation. *)
 
 Lemma split_eq_prop:
@@ -146,35 +163,58 @@ Proof.
   auto.
 Qed.
 
+Lemma validate_correct_rec:
+  forall default v t cases lo hi,
+  validate default cases t lo hi = true ->
+  lo <= Int.unsigned v <= hi ->
+  switch_target v default cases = comptree_match v t.
+Proof.
+  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.
+  rewrite (split_eq_prop v default _ _ _ _ EQ).
+  predSpec Int.eq Int.eq_spec v i.
+  symmetry. 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)).
+  eapply IHt1. eauto. omega.
+  eapply IHt2. eauto. omega.
+Qed.
+
 Definition table_tree_agree
     (default: nat) (cases: table) (t: comptree) : Prop :=
   forall v, switch_target v default cases = comptree_match v t.
 
-Lemma validate_switch_correct:
+Theorem validate_switch_correct:
   forall default t cases,
   validate_switch default cases t = true ->
   table_tree_agree default cases t.
 Proof.
-  induction t; simpl; intros until cases.
-  (* base case *)
-  destruct cases. 2: congruence.
-  intro. replace n with default. 
-  red; intros; simpl; 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). 
-  replace n with act. 
-  generalize (IHt _ H1); intro.  
-  red; intros. simpl. rewrite <- H2.
-  change act with (match Some act with Some act => act | None => default end).
-  eapply split_eq_prop; eauto.
-  symmetry. apply beq_nat_eq. auto. 
-  (* lt node *)
-  case_eq (split_lt i cases). intros lcases rcases EQ V.
-  destruct (andb_prop _ _ V). 
-  red; intros. simpl. 
-  rewrite <- (IHt1 _ H). rewrite <- (IHt2 _ H0). 
-  eapply split_lt_prop; eauto.
+  unfold validate_switch, table_tree_agree; intros.
+  eapply validate_correct_rec; eauto. 
+  apply Int.unsigned_range_2.
 Qed.
diff --git a/test/cminor/switchtbl.cm b/test/cminor/switchtbl.cm
index 07bda7e..9605499 100644
--- a/test/cminor/switchtbl.cm
+++ b/test/cminor/switchtbl.cm
@@ -1,6 +1,7 @@
 "f"(x): int -> int
 {
   match (x) {
+  case -1: return -11;
   case 0: return 00;
   case 1: return 11;
   case 2: return 22;