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

2 files changed, 98 insertions, 202 deletions

diff --git a/ia32/standard/Conventions1.v b/ia32/standard/Conventions1.v
index 49f5da92..cae20f6e 100644
--- a/ia32/standard/Conventions1.v
+++ b/ia32/standard/Conventions1.v
@@ -21,46 +21,26 @@ Require Import Locations.
 
 (** Machine registers (type [mreg] in module [Locations]) are divided in
   the following groups:
-- Temporaries used for spilling, reloading, and parallel move operations.
-- Allocatable registers, that can be assigned to RTL pseudo-registers.
-  These are further divided into:
--- Callee-save registers, whose value is preserved across a function call.
--- Caller-save registers that can be modified during a function call.
+- Callee-save registers, whose value is preserved across a function call.
+- Caller-save registers that can be modified during a function call.
 
   We follow the x86-32 application binary interface (ABI) in our choice
   of callee- and caller-save registers.
 *)
 
-Definition int_caller_save_regs := AX :: nil.
+Definition int_caller_save_regs := AX :: CX :: DX :: nil.
 
-Definition float_caller_save_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: nil.
+Definition float_caller_save_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil.
 
 Definition int_callee_save_regs := BX :: SI :: DI :: BP :: nil.
 
 Definition float_callee_save_regs : list mreg := nil.
 
-Definition destroyed_at_call_regs :=
-  int_caller_save_regs ++ float_caller_save_regs.
+Definition destroyed_at_call :=
+  FP0 :: int_caller_save_regs ++ float_caller_save_regs.
 
-Definition destroyed_at_call := List.map R destroyed_at_call_regs.
-
-Definition int_temporaries := IT1 :: IT2 :: nil.
-
-Definition float_temporaries := FT1 :: FT2 :: nil.
-
-(** [FP0] is not used for reloading, hence it is not in [float_temporaries],
-  however it is not allocatable, hence it is in [temporaries]. *)
-  
-Definition temporary_regs := IT1 :: IT2 :: FT1 :: FT2 :: FP0 :: nil.
-
-Definition temporaries := List.map R temporary_regs.
-
-Definition destroyed_at_move_regs := FP0 :: nil.
-
-Definition destroyed_at_move := List.map R destroyed_at_move_regs.
-
-Definition dummy_int_reg := AX.     (**r Used in [Coloring]. *)
-Definition dummy_float_reg := X0.   (**r Used in [Coloring]. *)
+Definition dummy_int_reg := AX.     (**r Used in [Regalloc]. *)
+Definition dummy_float_reg := X0.   (**r Used in [Regalloc]. *)
 
 (** The [index_int_callee_save] and [index_float_callee_save] associate
   a unique positive integer to callee-save registers.  This integer is
@@ -147,7 +127,7 @@ Proof.
 Qed.
 
 (** The following lemmas show that
-    (temporaries, destroyed at call, integer callee-save, float callee-save)
+    (destroyed at call, integer callee-save, float callee-save)
     is a partition of the set of machine registers. *)
 
 Lemma int_float_callee_save_disjoint:
@@ -158,34 +138,26 @@ Qed.
 
 Lemma register_classification:
   forall r, 
-  (In (R r) temporaries \/ In (R r) destroyed_at_call) \/
-  (In r int_callee_save_regs \/ In r float_callee_save_regs).
+  In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs.
 Proof.
   destruct r; 
-  try (left; left; simpl; OrEq);
-  try (left; right; simpl; OrEq);
+  try (left; simpl; OrEq);
   try (right; left; simpl; OrEq);
   try (right; right; simpl; OrEq).
 Qed.
 
 Lemma int_callee_save_not_destroyed:
   forall r, 
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    ~(In r int_callee_save_regs).
+    In r destroyed_at_call -> In r int_callee_save_regs -> False.
 Proof.
-  intros; red; intros. elim H.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
+  intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
 Qed.
 
 Lemma float_callee_save_not_destroyed:
   forall r, 
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    ~(In r float_callee_save_regs).
+    In r destroyed_at_call -> In r float_callee_save_regs -> False.
 Proof.
-  intros; red; intros. elim H.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
+  intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
 Qed.
 
 Lemma int_callee_save_type:
@@ -244,13 +216,15 @@ Qed.
   registers [AX] or [FP0], depending on the type of the returned value.
   We treat a function without result as a function with one integer result. *)
 
-Definition loc_result (s: signature) : mreg :=
+Definition loc_result (s: signature) : list mreg :=
   match s.(sig_res) with
-  | None => AX
-  | Some Tint => AX
-  | Some Tfloat => FP0
+  | None => AX :: nil
+  | Some Tint => AX :: nil
+  | Some Tfloat => FP0 :: nil
+  | Some Tlong => DX :: AX :: nil
   end.
 
+(*
 (** The result location has the type stated in the signature. *)
 
 Lemma loc_result_type:
@@ -263,17 +237,18 @@ Proof.
   destruct t; reflexivity.
   reflexivity.
 Qed.
+*)
 
-(** The result location is a caller-save register or a temporary *)
+(** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
-  forall (s: signature), 
-  In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries.
+  forall (s: signature) (r: mreg),
+  In r (loc_result s) -> In r destroyed_at_call.
 Proof.
-  intros; unfold loc_result.
-  destruct (sig_res s).
-  destruct t. left; simpl; OrEq. right; simpl; OrEq.
-  left; simpl; OrEq.
+  intros.
+  assert (r = AX \/ r = DX \/ r = FP0).
+    unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition.
+  destruct H0 as [A | [A | A]]; subst r; simpl; OrEq.
 Qed.
 
 (** ** Location of function arguments *)
@@ -284,8 +259,9 @@ Fixpoint loc_arguments_rec
     (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
   match tyl with
   | nil => nil
-  | Tint :: tys => S (Outgoing ofs Tint) :: loc_arguments_rec tys (ofs + 1)
-  | Tfloat :: tys => S (Outgoing ofs Tfloat) :: loc_arguments_rec tys (ofs + 2)
+  | Tint :: tys => S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 1)
+  | Tfloat :: tys => S Outgoing ofs Tfloat :: loc_arguments_rec tys (ofs + 2)
+  | Tlong :: tys => S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 2)
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
@@ -301,27 +277,19 @@ Fixpoint size_arguments_rec
     (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
   match tyl with
   | nil => ofs
-  | Tint :: tys => size_arguments_rec tys (ofs + 1)
-  | Tfloat :: tys => size_arguments_rec tys (ofs + 2)
+  | ty :: tys => size_arguments_rec tys (ofs + typesize ty)
   end.
 
 Definition size_arguments (s: signature) : Z :=
   size_arguments_rec s.(sig_args) 0.
 
-(** 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.
-
-(** Argument locations are either non-temporary registers or [Outgoing] 
+(** Argument locations are either caller-save registers or [Outgoing] 
   stack slots at nonnegative offsets. *)
 
 Definition loc_argument_acceptable (l: loc) : Prop :=
   match l with
-  | R r => ~(In l temporaries)
-  | S (Outgoing ofs ty) => ofs >= 0
+  | R r => In r destroyed_at_call
+  | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong
   | _ => False
   end.
 
@@ -329,62 +297,36 @@ Remark loc_arguments_rec_charact:
   forall tyl ofs l,
   In l (loc_arguments_rec tyl ofs) ->
   match l with
-  | S (Outgoing ofs' ty) => ofs' >= ofs
+  | S Outgoing ofs' ty => ofs' >= ofs /\ ty <> Tlong
   | _ => False
   end.
 Proof.
   induction tyl; simpl loc_arguments_rec; intros.
-  elim H.
-  destruct a; simpl in H; destruct H.
-  subst l. omega.
-  generalize (IHtyl _ _ H). destruct l; auto. destruct s; auto. omega. 
-  subst l. omega.
-  generalize (IHtyl _ _ H). destruct l; auto. destruct s; auto. omega. 
+  destruct H.
+  destruct a.
+- destruct H. subst l. split. omega. congruence.
+  exploit IHtyl; eauto.
+  destruct l; auto. destruct sl; auto. intuition omega.
+- destruct H. subst l. split. omega. congruence.
+  exploit IHtyl; eauto.
+  destruct l; auto. destruct sl; auto. intuition omega.
+- destruct H. subst l; split; [omega|congruence].
+  destruct H. subst l; split; [omega|congruence].
+  exploit IHtyl; eauto.
+  destruct l; auto. destruct sl; auto. intuition omega.
 Qed.
 
 Lemma loc_arguments_acceptable:
-  forall (s: signature) (r: loc),
-  In r (loc_arguments s) -> loc_argument_acceptable r.
+  forall (s: signature) (l: loc),
+  In l (loc_arguments s) -> loc_argument_acceptable l.
 Proof.
   unfold loc_arguments; intros.
-  generalize (loc_arguments_rec_charact  _ _ _ H).
-  destruct r; tauto.
-Qed.
-Hint Resolve loc_arguments_acceptable: locs.
-
-(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *)
-
-Remark loc_arguments_rec_notin_local:
-  forall tyl ofs ofs0 ty0,
-  Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl ofs).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a; simpl; auto.
-Qed.
-
-Remark loc_arguments_rec_notin_outgoing:
-  forall tyl ofs ofs0 ty0,
-  ofs0 + typesize ty0 <= ofs ->
-  Loc.notin (S (Outgoing ofs0 ty0)) (loc_arguments_rec tyl ofs).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a.
-  split. simpl. omega. apply IHtyl. omega. 
-  split. simpl. omega. apply IHtyl. omega. 
+  exploit loc_arguments_rec_charact; eauto. 
+  unfold loc_argument_acceptable.
+  destruct l; tauto.
 Qed.
 
-Lemma loc_arguments_norepet:
-  forall (s: signature), Loc.norepet (loc_arguments s).
-Proof.
-  intros. unfold loc_arguments. generalize (sig_args s) 0.
-  induction l; simpl; intros.
-  constructor.
-  destruct a; constructor.
-  apply loc_arguments_rec_notin_outgoing. simpl; omega. auto.
-  apply loc_arguments_rec_notin_outgoing. simpl; omega. auto.
-Qed.
+Hint Resolve loc_arguments_acceptable: locs.
 
 (** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
 
@@ -393,9 +335,8 @@ Remark size_arguments_rec_above:
 Proof.
   induction tyl; simpl; intros.
   omega.
-  destruct a.
-  apply Zle_trans with (ofs0 + 1); auto; omega.
-  apply Zle_trans with (ofs0 + 2); auto; omega.
+  apply Zle_trans with (ofs0 + typesize a); auto. 
+  generalize (typesize_pos a); omega.
 Qed.
 
 Lemma size_arguments_above:
@@ -407,56 +348,20 @@ Qed.
 
 Lemma loc_arguments_bounded:
   forall (s: signature) (ofs: Z) (ty: typ),
-  In (S (Outgoing ofs ty)) (loc_arguments s) ->
+  In (S Outgoing ofs ty) (loc_arguments s) ->
   ofs + typesize ty <= size_arguments s.
 Proof.
   intros until ty. unfold loc_arguments, size_arguments. generalize (sig_args s) 0.
   induction l; simpl; intros.
-  elim H.
-  destruct a; simpl in H; destruct H.
-  inv H. apply size_arguments_rec_above.
-  auto.
-  inv H. apply size_arguments_rec_above.
+  destruct H.
+  destruct a.
+  destruct H. inv H. apply size_arguments_rec_above. auto.
+  destruct H. inv H. apply size_arguments_rec_above. auto.
+  destruct H. inv H.
+  simpl typesize. replace (z + 1 + 1) with (z + 2) by omega. apply size_arguments_rec_above.
+  destruct H. inv H. 
+  simpl typesize. apply Zle_trans with (ofs + 2). omega. apply size_arguments_rec_above. 
   auto.
 Qed.
 
-(** Temporary registers do not overlap with argument locations. *)
-
-Lemma loc_arguments_not_temporaries:
-  forall sig, Loc.disjoint (loc_arguments sig) temporaries.
-Proof.
-  intros; red; intros x1 x2 H.
-  generalize (loc_arguments_rec_charact _ _ _ H).
-  destruct x1. tauto. destruct s; intuition.
-  revert H1. simpl; ElimOrEq; auto.
-Qed.
-Hint Resolve loc_arguments_not_temporaries: locs.
-
-(** Argument registers are caller-save. *)
 
-Lemma arguments_caller_save:
-  forall sig r,
-  In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call.
-Proof.
-  unfold loc_arguments; intros.
-  elim (loc_arguments_rec_charact _ _ _ H); simpl.
-Qed.
-
-(** Argument locations agree in number with the function signature. *)
-
-Lemma loc_arguments_length:
-  forall sig,
-  List.length (loc_arguments sig) = List.length sig.(sig_args).
-Proof.
-  intros. unfold loc_arguments. generalize (sig_args sig) 0.
-  induction l; simpl; intros. auto. destruct a; simpl; decEq; auto.
-Qed.
-
-(** Argument locations agree in types with the function signature. *)
-
-Lemma loc_arguments_type:
-  forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args).
-Proof.
-  intros. unfold loc_arguments. generalize (sig_args sig) 0. 
-  induction l; simpl; intros. auto. destruct a; simpl; decEq; auto.
-Qed.
diff --git a/ia32/standard/Stacklayout.v b/ia32/standard/Stacklayout.v
index be854fde..f9d1dafe 100644
--- a/ia32/standard/Stacklayout.v
+++ b/ia32/standard/Stacklayout.v
@@ -19,10 +19,9 @@ Require Import Bounds.
   from bottom (lowest offsets) to top:
 - Space for outgoing arguments to function calls.
 - Back link to parent frame
-- Local stack slots of integer type.
 - Saved values of integer callee-save registers used by the function.
-- Local stack slots of float type.
 - Saved values of float callee-save registers used by the function.
+- Local stack slots.
 - Space for the stack-allocated data declared in Cminor
 - Return address.
 
@@ -36,10 +35,9 @@ Record frame_env : Type := mk_frame_env {
   fe_size: Z;
   fe_ofs_link: Z;
   fe_ofs_retaddr: Z;
-  fe_ofs_int_local: Z;
+  fe_ofs_local: Z;
   fe_ofs_int_callee_save: Z;
   fe_num_int_callee_save: Z;
-  fe_ofs_float_local: Z;
   fe_ofs_float_callee_save: Z;
   fe_num_float_callee_save: Z;
   fe_stack_data: Z
@@ -50,17 +48,16 @@ Record frame_env : Type := mk_frame_env {
 
 Definition make_env (b: bounds) :=
   let olink := 4 * b.(bound_outgoing) in  (* back link *)
-  let oil := olink + 4 in              (* integer locals *)
-  let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *)
-  let oendi := oics + 4 * b.(bound_int_callee_save) in
-  let ofl := align oendi 8 in             (* float locals *)
-  let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
-  let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *)
+  let oics := olink + 4 in                (* integer callee-saves *)
+  let ofcs := align (oics + 4 * b.(bound_int_callee_save)) 8 in (* float callee-saves *)
+  let ol := ofcs + 8 * b.(bound_float_callee_save) in (* locals *)
+  let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *)
   let oretaddr := align (ostkdata + b.(bound_stack_data)) 4 in (* return address *)
   let sz := oretaddr + 4 in (* total size *)
   mk_frame_env sz olink oretaddr
-                  oil oics b.(bound_int_callee_save)
-                  ofl ofcs b.(bound_float_callee_save)
+                  ol
+                  oics b.(bound_int_callee_save)
+                  ofcs b.(bound_float_callee_save)
                   ostkdata.
 
 (** Separation property *)
@@ -70,25 +67,23 @@ Remark frame_env_separated:
   let fe := make_env b in
   0 <= fe_ofs_arg
   /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_link)
-  /\ fe.(fe_ofs_link) + 4 <= fe.(fe_ofs_int_local)
-  /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save)
-  /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local)
-  /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save)
-  /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_stack_data)
+  /\ fe.(fe_ofs_link) + 4 <= fe.(fe_ofs_int_callee_save)
+  /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_callee_save)
+  /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_ofs_local)
+  /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= fe.(fe_stack_data)
   /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_ofs_retaddr)
   /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_size).
 Proof.
   intros.
   generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)).
+  generalize (align_le (fe.(fe_ofs_local) + 4 * b.(bound_local)) 8 (refl_equal _)).
   generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 4 (refl_equal _)).
   unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
-    fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_num_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
+    fe_ofs_local, fe_ofs_int_callee_save, fe_num_int_callee_save,
+    fe_ofs_float_callee_save, fe_num_float_callee_save,
     fe_stack_data, fe_ofs_arg.
   intros.
-  generalize (bound_int_local_pos b); intro;
-  generalize (bound_float_local_pos b); intro;
+  generalize (bound_local_pos b); intro;
   generalize (bound_int_callee_save_pos b); intro;
   generalize (bound_float_callee_save_pos b); intro;
   generalize (bound_outgoing_pos b); intro;
@@ -102,38 +97,34 @@ Remark frame_env_aligned:
   forall b,
   let fe := make_env b in
   (4 | fe.(fe_ofs_link))
-  /\ (4 | fe.(fe_ofs_int_local))
   /\ (4 | fe.(fe_ofs_int_callee_save))
-  /\ (8 | fe.(fe_ofs_float_local))
   /\ (8 | fe.(fe_ofs_float_callee_save))
-  /\ (4 | fe.(fe_ofs_retaddr))
+  /\ (8 | fe.(fe_ofs_local))
   /\ (8 | fe.(fe_stack_data))
+  /\ (4 | fe.(fe_ofs_retaddr))
   /\ (4 | fe.(fe_size)).
 Proof.
   intros.
   unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
-    fe_ofs_int_local, fe_ofs_int_callee_save,
+    fe_ofs_local, fe_ofs_int_callee_save,
     fe_num_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
+    fe_ofs_float_callee_save, fe_num_float_callee_save,
     fe_stack_data.
   set (x1 := 4 * bound_outgoing b).
   assert (4 | x1). unfold x1; exists (bound_outgoing b); ring.
   set (x2 := x1 + 4).
   assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists 1; auto.
-  set (x3 := x2 + 4 * bound_int_local b).
-  assert (4 | x3). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring.
-  set (x4 := x3 + 4 * bound_int_callee_save b).
-  set (x5 := align x4 8).
-  assert (8 | x5). unfold x5. apply align_divides. omega.
-  set (x6 := x5 + 8 * bound_float_local b).
-  assert (8 | x6). unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring.
-  set (x7 := x6 + 8 * bound_float_callee_save b).
-  assert (8 | x7).
-    unfold x7. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
-  set (x8 := align (x7 + bound_stack_data b) 4).
-  assert (4 | x8). apply align_divides. omega.
-  set (x9 := x8 + 4).
-  assert (4 | x9). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto.
+  set (x3 := x2 + 4 * bound_int_callee_save b).
+  set (x4 := align x3 8).
+  assert (8 | x4). unfold x4. apply align_divides. omega.
+  set (x5 := x4 + 8 * bound_float_callee_save b).
+  assert (8 | x5). unfold x5; apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
+  set (x6 := align (x5 + 4 * bound_local b) 8).
+  assert (8 | x6). unfold x6; apply align_divides; omega.
+  set (x7 := align (x6 + bound_stack_data b) 4).
+  assert (4 | x7). unfold x7; apply align_divides; omega.
+  set (x8 := x7 + 4).
+  assert (4 | x8). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto.
   tauto.
 Qed.