Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

1 files changed, 513 insertions, 0 deletions

diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v
new file mode 100644
index 00000000..5f5cc510
--- /dev/null
+++ b/lib/FSetAVLplus.v
@@ -0,0 +1,513 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** An extension of [FSetAVL] (finite sets as balanced binary search trees)
+  with extra interval-based operations, more efficient than standard
+  operations. *)
+
+Require Import FSetInterface.
+Require FSetAVL.
+Require Import Coqlib.
+
+Module Make(X: OrderedType).
+
+Include FSetAVL.Make(X).
+
+Module Raw := MSet.Raw.
+
+Section MEM_BETWEEN.
+
+(** [mem_between above below s] is [true] iff there exists an element of [s]
+  that belongs to the interval described by the predicates [above] and [below].
+  Using the monotonicity of [above] and [below], the implementation of
+  [mem_between] avoids traversing the subtrees of [s] that
+  lie entirely outside the interval of interest. *)
+
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_mem_between (m: Raw.tree) : bool :=
+  match m with
+  | Raw.Leaf => false
+  | Raw.Node _ l x r =>
+      if above_low_bound x
+      then if below_high_bound x
+           then true
+           else raw_mem_between l
+      else raw_mem_between r
+  end.
+
+Definition mem_between (m: t) : bool := raw_mem_between m.(MSet.this).
+
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Lemma raw_mem_between_1:
+  forall m,
+  raw_mem_between m = true ->
+  exists x, Raw.In x m /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  induction m; simpl; intros.
+- discriminate.
+- destruct (above_low_bound t1) eqn: LB; [destruct (below_high_bound t1) eqn: HB | idtac].
+  + (* in interval *)
+    exists t1; split; auto.  apply Raw.IsRoot. auto. 
+  + (* above interval *)
+    exploit IHm1; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InLeft; auto.
+  + (* below interval *)
+    exploit IHm2; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InRight; auto.
+Qed.
+
+Lemma raw_mem_between_2:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
+  raw_mem_between m = true.
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- rewrite Raw.In_node_iff in H1. 
+  destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
+  + (* in interval *)
+    auto.
+  + (* above interval *)
+    assert (X.eq x x0 \/ X.lt x0 x -> False).
+    { intros. exploit below_monotone; eauto. congruence. }
+    intuition.
+  + assert (X.eq x x0 \/ X.lt x x0 -> False).
+    { intros. exploit above_monotone; eauto. congruence. }
+    intuition.
+Qed.
+
+Theorem mem_between_1:
+  forall s,
+  mem_between s = true ->
+  exists x, In x s /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  intros. apply raw_mem_between_1. auto. 
+Qed.
+
+Theorem mem_between_2:
+  forall x s,
+  In x s -> above_low_bound x = true -> below_high_bound x = true ->
+  mem_between s = true.
+Proof.
+  unfold mem_between; intros. apply raw_mem_between_2 with x; auto. apply MSet.is_ok.
+Qed.
+
+End MEM_BETWEEN.
+
+Section ELEMENTS_BETWEEN.
+
+(** [elements_between above below s] returns the set of elements of [s]
+  that belong to the interval [above,below]. *)
+
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_elements_between (m: Raw.tree) : Raw.tree :=
+  match m with
+  | Raw.Leaf => Raw.Leaf
+  | Raw.Node _ l x r =>
+      if above_low_bound x then
+        if below_high_bound x then
+          Raw.join (raw_elements_between l) x (raw_elements_between r)
+        else
+          raw_elements_between l
+      else
+        raw_elements_between r
+  end.
+
+Remark In_raw_elements_between_1:
+  forall x m,
+  Raw.In x (raw_elements_between m) -> Raw.In x m.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- rewrite Raw.In_node_iff. 
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. intuition. 
+  + left; apply IHm1; auto.
+  + right; right; apply IHm2; auto.
+Qed.
+
+Lemma raw_elements_between_ok:
+  forall m, Raw.bst m -> Raw.bst (raw_elements_between m).
+Proof.
+  induction 1; simpl.
+- constructor.
+- destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
+  + apply Raw.join_ok; auto.
+    red; intros. apply l0. apply In_raw_elements_between_1; auto.
+    red; intros. apply g. apply In_raw_elements_between_1; auto.
+  + auto.
+  + auto.
+Qed.
+
+Definition elements_between (s: t) : t :=
+  @MSet.Mkt (raw_elements_between s.(MSet.this)) (raw_elements_between_ok s.(MSet.this) s.(MSet.is_ok)).
+
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Remark In_raw_elements_between_2:
+  forall x m,
+  Raw.In x (raw_elements_between m) -> above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. intuition.
+    apply above_monotone with t1; auto. 
+    apply below_monotone with t1; auto.
+  + auto.
+  + auto.
+Qed.
+
+Remark In_raw_elements_between_3:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
+  Raw.In x (raw_elements_between m).
+Proof.
+  induction 1; simpl; intros.
+- auto.
+- rewrite Raw.In_node_iff in H1.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac].
+  + rewrite Raw.join_spec. intuition. 
+  + assert (X.eq x x0 \/ X.lt x0 x -> False).
+    { intros. exploit below_monotone; eauto. congruence. }
+    intuition. elim H7. apply g. auto.
+  + assert (X.eq x x0 \/ X.lt x x0 -> False).
+    { intros. exploit above_monotone; eauto. congruence. }
+    intuition. elim H7. apply l0. auto.
+Qed.
+
+Theorem elements_between_iff:
+  forall x s,
+  In x (elements_between s) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  intros. unfold elements_between, In; simpl. split.
+  intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto. 
+  intros [A [B C]]. apply In_raw_elements_between_3; auto. apply MSet.is_ok.
+Qed.
+
+End ELEMENTS_BETWEEN.
+
+Section FOR_ALL_BETWEEN.
+
+(** [for_all_between pred above below s] is [true] iff all elements of [s]
+  in a given variation interval satisfy predicate [pred].
+  The variation interval is given by two predicates [above] and [below]
+  which must both hold if the element is part of the interval.
+  Using the monotonicity of [above] and [below], the implementation of
+  [for_all_between] avoids traversing the subtrees of [s] that
+  lie entirely outside the interval of interest. *)
+
+Variable pred: elt -> bool.
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_for_all_between (m: Raw.tree) : bool :=
+  match m with
+  | Raw.Leaf => true
+  | Raw.Node _ l x r =>
+      if above_low_bound x
+      then if below_high_bound x
+           then raw_for_all_between l && pred x && raw_for_all_between r
+           else raw_for_all_between l
+      else raw_for_all_between r
+  end.
+
+Definition for_all_between (m: t) : bool := raw_for_all_between m.(MSet.this).
+
+Hypothesis pred_compat:
+  forall x1 x2, X.eq x1 x2 -> pred x1 = pred x2.
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Lemma raw_for_all_between_1:
+  forall x m,
+  Raw.bst m ->
+  raw_for_all_between m = true ->
+  Raw.In x m ->
+  above_low_bound x = true ->
+  below_high_bound x = true ->
+  pred x = true.
+Proof.
+  induction 1; simpl; intros.
+- inv H0. 
+- destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
+  + (* in interval *)
+    destruct (andb_prop _ _ H1) as [P C]. destruct (andb_prop _ _ P) as [A B]. clear H1 P.
+    inv H2.
+    * erewrite pred_compat; eauto. 
+    * apply IHbst1; auto.
+    * apply IHbst2; auto.
+  + (* above interval *)
+    inv H2.
+    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). 
+      congruence.
+    * apply IHbst1; auto.
+    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
+      congruence.
+  + (* below interval *)
+    inv H2.
+    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). 
+      congruence.
+    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
+      congruence.
+    * apply IHbst2; auto.
+Qed.
+
+Lemma raw_for_all_between_2:
+  forall m,
+  Raw.bst m ->
+  (forall x, Raw.In x m -> above_low_bound x = true -> below_high_bound x = true -> pred x = true) ->
+  raw_for_all_between m = true.
+Proof.
+  induction 1; intros; simpl.
+- auto.
+- destruct (above_low_bound x) eqn: LB; [destruct (below_high_bound x) eqn: HB | idtac].
+  + (* in interval *)
+    rewrite IHbst1. rewrite (H1 x). rewrite IHbst2. auto.
+    intros. apply H1; auto. apply Raw.InRight; auto.
+    apply Raw.IsRoot. reflexivity. auto. auto. 
+    intros. apply H1; auto. apply Raw.InLeft; auto.
+  + (* above interval *)
+    apply IHbst1. intros. apply H1; auto. apply Raw.InLeft; auto.
+  + (* below interval *)
+    apply IHbst2. intros. apply H1; auto. apply Raw.InRight; auto.
+Qed.
+
+Theorem for_all_between_iff:
+  forall s,
+  for_all_between s = true <-> (forall x, In x s -> above_low_bound x = true -> below_high_bound x = true -> pred x = true).
+Proof.
+  unfold for_all_between; intros; split; intros.
+- eapply raw_for_all_between_1; eauto. apply MSet.is_ok. 
+- apply raw_for_all_between_2; auto. apply MSet.is_ok.
+Qed.
+
+End FOR_ALL_BETWEEN.
+
+Section PARTITION_BETWEEN.
+
+Variable above_low_bound: elt -> bool.
+Variable below_high_bound: elt -> bool.
+
+Fixpoint raw_partition_between (m: Raw.tree) : Raw.tree * Raw.tree :=
+  match m with
+  | Raw.Leaf => (Raw.Leaf, Raw.Leaf)
+  | Raw.Node _ l x r =>
+      if above_low_bound x then
+        if below_high_bound x then
+          (let (l1, l2) := raw_partition_between l in
+           let (r1, r2) := raw_partition_between r in
+           (Raw.join l1 x r1, Raw.concat l2 r2))
+        else
+          (let (l1, l2) := raw_partition_between l in
+           (l1, Raw.join l2 x r))
+      else
+        (let (r1, r2) := raw_partition_between r in
+         (r1, Raw.join l x r2))
+  end.
+
+Remark In_raw_partition_between_1:
+  forall x m,
+  Raw.In x (fst (raw_partition_between m)) -> Raw.In x m.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. 
+  + rewrite Raw.In_node_iff. intuition.
+  + rewrite Raw.In_node_iff. intuition.
+Qed.
+
+Remark In_raw_partition_between_2:
+  forall x m,
+  Raw.In x (snd (raw_partition_between m)) -> Raw.In x m.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition. 
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
+Qed.
+
+Lemma raw_partition_between_ok:
+  forall m, Raw.bst m -> Raw.bst (fst (raw_partition_between m)) /\ Raw.bst (snd (raw_partition_between m)).
+Proof.
+  induction 1; simpl.
+- split; constructor.
+- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2]. 
+  destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
+  + split.
+    apply Raw.join_ok; auto.
+    red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto. 
+    red; intros. apply g. apply In_raw_partition_between_1. rewrite REQ; auto.
+    apply Raw.concat_ok; auto.
+    intros. transitivity x. 
+    apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. 
+    apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
+  + split.
+    auto.
+    apply Raw.join_ok; auto.
+    red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. 
+  + split.
+    auto.
+    apply Raw.join_ok; auto.
+    red; intros. apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
+Qed.
+
+Hypothesis above_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x1 x2 -> above_low_bound x1 = true -> above_low_bound x2 = true.
+Hypothesis below_monotone:
+  forall x1 x2, X.eq x1 x2 \/ X.lt x2 x1 -> below_high_bound x1 = true -> below_high_bound x2 = true.
+
+Remark In_raw_partition_between_3:
+  forall x m,
+  Raw.In x (fst (raw_partition_between m)) -> above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  induction m; simpl; intros.
+- inv H.
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
+  + rewrite Raw.join_spec in H. intuition.
+    apply above_monotone with t1; auto. 
+    apply below_monotone with t1; auto.
+  + auto.
+  + auto.
+Qed.
+
+Remark In_raw_partition_between_4:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x (snd (raw_partition_between m)) -> above_low_bound x = false \/ below_high_bound x = false.
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
+  + simpl in H1. rewrite Raw.concat_spec in H1. intuition. 
+  + assert (forall y, X.eq y x0 \/ X.lt x0 y -> below_high_bound y = false).
+    { intros. destruct (below_high_bound y) eqn:E; auto. 
+      assert (below_high_bound x0 = true) by (apply below_monotone with y; auto).
+      congruence. }
+    simpl in H1. rewrite Raw.join_spec in H1. intuition.
+  + assert (forall y, X.eq y x0 \/ X.lt y x0 -> above_low_bound y = false).
+    { intros. destruct (above_low_bound y) eqn:E; auto. 
+      assert (above_low_bound x0 = true) by (apply above_monotone with y; auto).
+      congruence. }
+    simpl in H1. rewrite Raw.join_spec in H1. intuition.
+Qed.
+
+Remark In_raw_partition_between_5:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = true -> below_high_bound x = true ->
+  Raw.In x (fst (raw_partition_between m)).
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
+  + simpl. rewrite Raw.join_spec. inv H1. 
+    auto.
+    right; left; apply IHbst1; auto. 
+    right; right; apply IHbst2; auto.
+  + simpl. inv H1. 
+    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
+    congruence.
+    auto. 
+    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). 
+    congruence.
+  + simpl. inv H1. 
+    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
+    congruence.
+    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). 
+    congruence.
+    eauto.
+Qed.
+
+Remark In_raw_partition_between_6:
+  forall x m,
+  Raw.bst m ->
+  Raw.In x m -> above_low_bound x = false \/ below_high_bound x = false ->
+  Raw.In x (snd (raw_partition_between m)).
+Proof.
+  induction 1; simpl; intros.
+- inv H.
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+  destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
+  destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
+  + simpl. rewrite Raw.concat_spec. inv H1.
+    assert (below_high_bound x = true) by (apply below_monotone with x0; auto; left; symmetry; auto).
+    assert (above_low_bound x = true) by (apply above_monotone with x0; auto; left; symmetry; auto).
+    destruct H2; congruence.
+    left; apply IHbst1; auto.
+    right; apply IHbst2; auto.
+  + simpl. rewrite Raw.join_spec. inv H1. 
+    auto.
+    right; left; apply IHbst1; auto. 
+    auto.
+  + simpl. rewrite Raw.join_spec. inv H1. 
+    auto.
+    auto.
+    right; right; apply IHbst2; auto.
+Qed.
+
+Definition partition_between (s: t) : t * t :=
+  let p := raw_partition_between s.(MSet.this) in
+  (@MSet.Mkt (fst p) (proj1 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok))),
+   @MSet.Mkt (snd p) (proj2 (raw_partition_between_ok s.(MSet.this) s.(MSet.is_ok)))).
+
+Theorem partition_between_iff_1:
+  forall x s,
+  In x (fst (partition_between s)) <->
+  In x s /\ above_low_bound x = true /\ below_high_bound x = true.
+Proof.
+  intros. unfold partition_between, In; simpl. split. 
+  intros. split. apply In_raw_partition_between_1; auto. eapply In_raw_partition_between_3; eauto.
+  intros [A [B C]]. apply In_raw_partition_between_5; auto. apply MSet.is_ok.
+Qed.
+
+Theorem partition_between_iff_2:
+  forall x s,
+  In x (snd (partition_between s)) <->
+  In x s /\ (above_low_bound x = false \/ below_high_bound x = false).
+Proof.
+  intros. unfold partition_between, In; simpl. split. 
+  intros. split. apply In_raw_partition_between_2; auto. eapply In_raw_partition_between_4; eauto. apply MSet.is_ok.
+  intros [A B]. apply In_raw_partition_between_6; auto. apply MSet.is_ok.
+Qed.
+
+End PARTITION_BETWEEN.
+
+End Make.