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, 19 insertions, 189 deletions

diff --git a/backend/Conventions.v b/backend/Conventions.v
index c11bf47c..abfe4eee 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -22,110 +22,6 @@ Require Export Conventions1.
     [arch/abi/Conventions1.v].  This file adds various processor-independent
     definitions and lemmas. *)
 
-(** * Acceptable locations for register allocation *)
-
-(** The following predicate describes the locations that can be assigned
-  to an RTL pseudo-register during register allocation: a non-temporary
-  machine register or a [Local] stack slot are acceptable. *)
-
-Definition loc_acceptable (l: loc) : Prop :=
-  match l with
-  | R r => ~(In l temporaries)
-  | S (Local ofs ty) => ofs >= 0
-  | S (Incoming _ _) => False
-  | S (Outgoing _ _) => False
-  end.
-
-Definition locs_acceptable (ll: list loc) : Prop :=
-  forall l, In l ll -> loc_acceptable l.
-
-Lemma temporaries_not_acceptable:
-  forall l, loc_acceptable l -> Loc.notin l temporaries.
-Proof.
-  unfold loc_acceptable; destruct l.
-  simpl. intuition congruence.
-  destruct s; try contradiction. 
-  intro. simpl. tauto.
-Qed.
-Hint Resolve temporaries_not_acceptable: locs.
-
-Lemma locs_acceptable_disj_temporaries:
-  forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries.
-Proof.
-  intros. apply Loc.notin_disjoint. intros.
-  apply temporaries_not_acceptable. auto. 
-Qed.
-
-Lemma loc_acceptable_noteq_diff:
-  forall l1 l2,
-  loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2.
-Proof.
-  unfold loc_acceptable, Loc.diff; destruct l1; destruct l2;
-  try (destruct s); try (destruct s0); intros; auto; try congruence.
-  case (zeq z z0); intro. 
-  compare t t0; intro.
-  subst z0; subst t0; tauto.
-  tauto. tauto.
-  contradiction. contradiction.
-Qed.
-
-Lemma loc_acceptable_notin_notin:
-  forall r ll,
-  loc_acceptable r ->
-  ~(In r ll) -> Loc.notin r ll.
-Proof.
-  induction ll; simpl; intros.
-  auto.
-  split. apply loc_acceptable_noteq_diff. assumption. 
-  apply sym_not_equal. tauto. 
-  apply IHll. assumption. tauto. 
-Qed.
-
-(** * Additional properties of result and argument locations *)
-
-(** The result location is not a callee-save register. *)
-
-Lemma loc_result_not_callee_save:
-  forall (s: signature),
-  ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs).
-Proof.
-  intros. generalize (loc_result_caller_save s).
-  generalize (int_callee_save_not_destroyed (loc_result s)).
-  generalize (float_callee_save_not_destroyed (loc_result s)).
-  tauto.
-Qed.
-
-(** Callee-save registers do not overlap with argument locations. *)
-
-Lemma arguments_not_preserved:
-  forall sig l,
-  Loc.notin l destroyed_at_call -> loc_acceptable l ->
-  Loc.notin l (loc_arguments sig).
-Proof.
-  intros. destruct l; red in H0. 
-  apply Loc.reg_notin. red; intros. 
-  exploit Loc.notin_not_in; eauto. eapply arguments_caller_save; eauto.
-  destruct s; try contradiction.
-  unfold loc_arguments. apply loc_arguments_rec_notin_local. 
-Qed.
-
-(** There is no partial overlap between arguments and acceptable locations. *)
-
-Lemma no_overlap_arguments:
-  forall args sg,
-  locs_acceptable args ->
-  Loc.no_overlap args (loc_arguments sg).
-Proof.
-  unfold Loc.no_overlap; intros.
-  generalize (H r H0).
-  generalize (loc_arguments_acceptable _ _ H1).
-  destruct s; destruct r; simpl.
-  intros. case (mreg_eq m0 m); intro. left; congruence. tauto.
-  intros. right; destruct s; auto.
-  intros. right. auto.
-  destruct s; try tauto. destruct s0; tauto.
-Qed.
-
 (** ** Location of function parameters *)
 
 (** A function finds the values of its parameter in the same locations
@@ -135,86 +31,39 @@ Qed.
 
 Definition parameter_of_argument (l: loc) : loc :=
   match l with
-  | S (Outgoing n ty) => S (Incoming n ty)
+  | S Outgoing n ty => S Incoming n ty
   | _ => l
   end.
 
 Definition loc_parameters (s: signature) :=
   List.map parameter_of_argument (loc_arguments s).
 
-Lemma loc_parameters_type:
-  forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args).
-Proof.
-  intros. unfold loc_parameters.
-  rewrite list_map_compose. 
-  rewrite <- loc_arguments_type.
-  apply list_map_exten.
-  intros. destruct x; simpl. auto. 
-  destruct s; reflexivity.
-Qed.
-
-Lemma loc_parameters_length:
-  forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args).
-Proof.
-  intros. unfold loc_parameters. rewrite list_length_map. 
-  apply loc_arguments_length.
-Qed.
-
-Lemma loc_parameters_not_temporaries:
-  forall sig, Loc.disjoint (loc_parameters sig) temporaries.
-Proof.
-  intro; red; intros.
-  unfold loc_parameters in H. 
-  elim (list_in_map_inv _ _ _ H). intros y [EQ IN].
-  generalize (loc_arguments_not_temporaries sig y x2 IN H0).
-  subst x1. destruct x2.
-  destruct y; simpl. auto. destruct s; auto.
-  byContradiction. generalize H0. simpl. NotOrEq.
-Qed.
-
-Lemma no_overlap_parameters:
-  forall params sg,
-  locs_acceptable params ->
-  Loc.no_overlap (loc_parameters sg) params.
-Proof.
-  unfold Loc.no_overlap; intros.
-  unfold loc_parameters in H0. 
-  elim (list_in_map_inv _ _ _ H0). intros t [EQ IN].
-  rewrite EQ. 
-  generalize (loc_arguments_acceptable _ _ IN).
-  generalize (H s H1).
-  destruct s; destruct t; simpl.
-  intros. case (mreg_eq m0 m); intro. left; congruence. tauto.
-  intros. right; destruct s; simpl; auto.
-  intros; right; auto.
-  destruct s; try tauto. destruct s0; try tauto. 
-  intros; simpl. tauto.
-Qed.
-
 Lemma incoming_slot_in_parameters:
   forall ofs ty sg,
-  In (S (Incoming ofs ty)) (loc_parameters sg) ->
-  In (S (Outgoing ofs ty)) (loc_arguments sg).
+  In (S Incoming ofs ty) (loc_parameters sg) ->
+  In (S Outgoing ofs ty) (loc_arguments sg).
 Proof.
   intros.
   unfold loc_parameters in H. 
-  change (S (Incoming ofs ty)) with (parameter_of_argument (S (Outgoing ofs ty))) in H.
+  change (S Incoming ofs ty) with (parameter_of_argument (S Outgoing ofs ty)) in H.
   exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
   exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
   destruct x; simpl in A; try discriminate.
-  destruct s; try contradiction. 
+  destruct sl; try contradiction. 
   inv A. auto.
 Qed. 
 
-
 (** * Tail calls *)
 
 (** A tail-call is possible for a signature if the corresponding
     arguments are all passed in registers. *)
 
+(** A tail-call is possible for a signature if the corresponding
+    arguments are all passed in registers. *)
+
 Definition tailcall_possible (s: signature) : Prop :=
   forall l, In l (loc_arguments s) ->
-  match l with R _ => True | S _ => False end.
+  match l with R _ => True | S _ _ _ => False end.
 
 (** Decide whether a tailcall is possible. *)
 
@@ -223,7 +72,7 @@ Definition tailcall_is_possible (sg: signature) : bool :=
     match l with
     | nil => true
     | R _ :: l' => tcisp l'
-    | S _ :: l' => false
+    | S _ _ _ :: l' => false
     end
   in tcisp (loc_arguments sg).
 
@@ -237,31 +86,12 @@ Proof.
   destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
 Qed.
 
-(** * Counting temporaries *)
-
-(** Given a list [tys] of types representing arguments to an operator,
-  [arity_ok tys] returns [true] if there are enough temporaries to
-  reload all arguments into temporaries. *)
-
-Fixpoint arity_ok_rec (tys: list typ) (itmps ftmps: list mreg)
-                      {struct tys} : bool :=
-  match tys with
-  | nil => true
-  | Tint :: ts =>
-      match itmps with
-      | nil => false
-      | it1 :: its => arity_ok_rec ts its ftmps
-      end
-  | Tfloat :: ts =>
-      match ftmps with
-      | nil => false
-      | ft1 :: fts => arity_ok_rec ts itmps fts
-      end
-  end.
-
-Definition arity_ok (tys: list typ) :=
-  arity_ok_rec tys int_temporaries float_temporaries.
-
-
-
-
+Lemma zero_size_arguments_tailcall_possible:
+  forall sg, size_arguments sg = 0 -> tailcall_possible sg.
+Proof.
+  intros; red; intros. exploit loc_arguments_acceptable; eauto. 
+  unfold loc_argument_acceptable. 
+  destruct l; intros. auto. destruct sl; try contradiction. destruct H1. 
+  generalize (loc_arguments_bounded _ _ _ H0).
+  generalize (typesize_pos ty). omega. 
+Qed.