Introduce register pairs to describe calling conventions more precisely

This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations.

In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves.  We will need to change this in the future to support 64-bit processors.  The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting.  Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves.

Summary of changes:
- AST: introduce the type "rpair A" of register pairs
- Conventions1, Conventions: use it when describing calling conventions
- LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls
- Events: suppress external_call', no longer useful
- All passes from Allocation to Asmgen: adapt accordingly.

1 files changed, 119 insertions, 143 deletions

diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index abd28b18..3eae50ef 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -88,33 +88,43 @@ Definition dummy_float_reg := F0.   (**r Used in [Coloring]. *)
   so we have code in [arm/PrintAsm.ml] that inserts additional moves
   to/from [F0]. *)
 
-Definition loc_result (s: signature) : list mreg :=
+Definition loc_result (s: signature) : rpair mreg :=
   match s.(sig_res) with
-  | None => R0 :: nil
-  | Some (Tint | Tany32) => R0 :: nil
-  | Some (Tfloat | Tsingle | Tany64) => F0 :: nil
-  | Some Tlong => R1 :: R0 :: nil
+  | None => One R0
+  | Some (Tint | Tany32) => One R0
+  | Some (Tfloat | Tsingle | Tany64) => One F0
+  | Some Tlong => Twolong R1 R0
   end.
 
 (** The result registers have types compatible with that given in the signature. *)
 
 Lemma loc_result_type:
   forall sig,
-  subtype_list (proj_sig_res' sig) (map mreg_type (loc_result sig)) = true.
+  subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
 Proof.
-  intros. unfold proj_sig_res', loc_result. destruct (sig_res sig) as [[]|]; auto.
+  intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
 Qed.
 
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
-  forall (s: signature) (r: mreg),
-  In r (loc_result s) -> is_callee_save r = false.
+  forall (s: signature),
+  forall_rpair (fun r => is_callee_save r = false) (loc_result s).
 Proof.
   intros.
-  assert (r = R0 \/ r = R1 \/ r = F0).
-    unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition.
-  destruct H0 as [A | [A | A]]; subst r; auto.
+  unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+Qed.
+
+(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
+
+Lemma loc_result_pair:
+  forall sg,
+  match loc_result sg with
+  | One _ => True
+  | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+  end.
+Proof.
+  intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence. 
 Qed.
 
 (** ** Location of function arguments *)
@@ -149,28 +159,28 @@ Definition freg_param (n: Z) : mreg :=
   match list_nth_z float_param_regs n with Some r => r | None => F0 end.
 
 Fixpoint loc_arguments_hf
-     (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list loc :=
+     (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
   | (Tint | Tany32) as ty :: tys =>
       if zlt ir 4
-      then R (ireg_param ir) :: loc_arguments_hf tys (ir + 1) fr ofs
-      else S Outgoing ofs ty :: loc_arguments_hf tys ir fr (ofs + 1)
+      then One (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 1) fr ofs
+      else One (S Outgoing ofs ty) :: loc_arguments_hf tys ir fr (ofs + 1)
   | (Tfloat | Tany64) as ty :: tys =>
       if zlt fr 8
-      then R (freg_param fr) :: loc_arguments_hf tys ir (fr + 1) ofs
+      then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs
       else let ofs := align ofs 2 in
-           S Outgoing ofs ty :: loc_arguments_hf tys ir fr (ofs + 2)
+           One (S Outgoing ofs ty) :: loc_arguments_hf tys ir fr (ofs + 2)
   | Tsingle :: tys =>
       if zlt fr 8
-      then R (freg_param fr) :: loc_arguments_hf tys ir (fr + 1) ofs
-      else S Outgoing ofs Tsingle :: loc_arguments_hf tys ir fr (ofs + 1)
+      then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs
+      else One (S Outgoing ofs Tsingle) :: loc_arguments_hf tys ir fr (ofs + 1)
   | Tlong :: tys =>
       let ir := align ir 2 in
       if zlt ir 4
-      then R (ireg_param (ir + 1)) :: R (ireg_param ir) :: loc_arguments_hf tys (ir + 2) fr ofs
+      then Twolong (R (ireg_param (ir + 1))) (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 2) fr ofs
       else let ofs := align ofs 2 in
-          S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_hf tys ir fr (ofs + 2)
+           Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: loc_arguments_hf tys ir fr (ofs + 2)
   end.
 
 (** For the "softfloat" configuration, as well as for variable-argument functions
@@ -194,30 +204,30 @@ we insert additional code around function calls and returns that moves
 data appropriately. *)
 
 Fixpoint loc_arguments_sf
-     (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
+     (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
   | (Tint|Tany32) as ty :: tys =>
-      (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty)
+      One (if zlt ofs 0 then R (ireg_param (ofs + 4)) else S Outgoing ofs ty)
       :: loc_arguments_sf tys (ofs + 1)
   | (Tfloat|Tany64) as ty :: tys =>
       let ofs := align ofs 2 in
-      (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty)
+      One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs ty)
       :: loc_arguments_sf tys (ofs + 2)
   | Tsingle :: tys =>
-      (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle)
+      One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle)
       :: loc_arguments_sf tys (ofs + 1)
   | Tlong :: tys =>
       let ofs := align ofs 2 in
-      (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint)
-      :: (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint)
+      Twolong (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint)
+              (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint)
       :: loc_arguments_sf tys (ofs + 2)
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
 
-Definition loc_arguments (s: signature) : list loc :=
+Definition loc_arguments (s: signature) : list (rpair loc) :=
   match Archi.abi with
   | Archi.Softfloat =>
       loc_arguments_sf s.(sig_args) (-4)
@@ -279,185 +289,151 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
   | _ => False
   end.
 
-Remark ireg_param_in_params: forall n, In (ireg_param n) int_param_regs.
+Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
+  match l with
+  | R r => is_callee_save r = false
+  | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
+  | _ => False
+  end.
+
+Remark ireg_param_caller_save: forall n, is_callee_save (ireg_param n) = false.
 Proof.
   unfold ireg_param; intros.
+  assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal.
   destruct (list_nth_z int_param_regs n) as [r|] eqn:NTH.
-  eapply list_nth_z_in; eauto.
-  simpl; auto.
+  apply A. eapply list_nth_z_in; eauto.
+  auto.
 Qed.
 
-Remark freg_param_in_params: forall n, In (freg_param n) float_param_regs.
+Remark freg_param_caller_save: forall n, is_callee_save (freg_param n) = false.
 Proof.
   unfold freg_param; intros.
+  assert (A: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
   destruct (list_nth_z float_param_regs n) as [r|] eqn:NTH.
-  eapply list_nth_z_in; eauto.
-  simpl; auto.
+  apply A. eapply list_nth_z_in; eauto.
+  auto.
 Qed.
 
 Remark loc_arguments_hf_charact:
-  forall tyl ir fr ofs l,
-  In l (loc_arguments_hf tyl ir fr ofs) ->
-  match l with
-  | R r => In r int_param_regs \/ In r float_param_regs
-  | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
-  | S _ _ _ => False
-  end.
+  forall tyl ir fr ofs p,
+  In p (loc_arguments_hf tyl ir fr ofs) -> forall_rpair (loc_argument_charact ofs) p.
 Proof.
-  assert (INCR: forall l ofs1 ofs2,
-            match l with
-            | R r => In r int_param_regs \/ In r float_param_regs
-            | S Outgoing ofs' ty => ofs' >= ofs2 /\ typealign ty = 1
-            | S _ _ _ => False
-            end ->
-            ofs1 <= ofs2 ->
-            match l with
-            | R r => In r int_param_regs \/ In r float_param_regs
-            | S Outgoing ofs' ty => ofs' >= ofs1 /\ typealign ty = 1
-            | S _ _ _ => False
-            end).
-  {
-    intros. destruct l; auto. destruct sl; auto. intuition omega.
-  }
+  assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p).
+  { destruct p; simpl; intuition eauto. }
   induction tyl; simpl loc_arguments_hf; intros.
   elim H.
   destruct a.
 - (* int *)
   destruct (zlt ir 4); destruct H.
-  subst. left; apply ireg_param_in_params.
+  subst. apply ireg_param_caller_save.
   eapply IHtyl; eauto.
   subst. split; [omega | auto].
-  eapply INCR. eapply IHtyl; eauto. omega.
+  eapply Y; eauto. omega.
 - (* float *)
   destruct (zlt fr 8); destruct H.
-  subst. right; apply freg_param_in_params.
+  subst. apply freg_param_caller_save.
   eapply IHtyl; eauto.
   subst. split. apply Zle_ge. apply align_le. omega. auto.
-  eapply INCR. eapply IHtyl; eauto.
-  apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
+  eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
 - (* long *)
   set (ir' := align ir 2) in *.
   assert (ofs <= align ofs 2) by (apply align_le; omega).
   destruct (zlt ir' 4).
-  destruct H. subst l; left; apply ireg_param_in_params.
-  destruct H. subst l; left; apply ireg_param_in_params.
+  destruct H. subst p. split; apply ireg_param_caller_save. 
   eapply IHtyl; eauto.
-  destruct H. subst l; split; [ omega | auto ].
-  destruct H. subst l; split; [ omega | auto ].
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct H. subst p. split; (split; [ omega | auto ]).
+  eapply Y. eapply IHtyl; eauto. omega.
 - (* single *)
   destruct (zlt fr 8); destruct H.
-  subst. right; apply freg_param_in_params.
+  subst. apply freg_param_caller_save.
   eapply IHtyl; eauto.
-  subst. split; [omega | auto].
-  eapply INCR. eapply IHtyl; eauto. omega.
+  subst. split; [omega|auto].
+  eapply Y; eauto. omega.
 - (* any32 *)
   destruct (zlt ir 4); destruct H.
-  subst. left; apply ireg_param_in_params.
+  subst. apply ireg_param_caller_save.
   eapply IHtyl; eauto.
   subst. split; [omega | auto].
-  eapply INCR. eapply IHtyl; eauto. omega.
+  eapply Y; eauto. omega.
 - (* any64 *)
   destruct (zlt fr 8); destruct H.
-  subst. right; apply freg_param_in_params.
+  subst. apply freg_param_caller_save.
   eapply IHtyl; eauto.
   subst. split. apply Zle_ge. apply align_le. omega. auto.
-  eapply INCR. eapply IHtyl; eauto.
-  apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
+  eapply Y; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega.
 Qed.
 
 Remark loc_arguments_sf_charact:
-  forall tyl ofs l,
-  In l (loc_arguments_sf tyl ofs) ->
-  match l with
-  | R r => In r int_param_regs \/ In r float_param_regs
-  | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ typealign ty = 1
-  | S _ _ _ => False
-  end.
+  forall tyl ofs p,
+  In p (loc_arguments_sf tyl ofs) -> forall_rpair (loc_argument_charact (Zmax 0 ofs)) p.
 Proof.
-  assert (INCR: forall l ofs1 ofs2,
-            match l with
-            | R r => In r int_param_regs \/ In r float_param_regs
-            | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ typealign ty = 1
-            | S _ _ _ => False
-            end ->
-            ofs1 <= ofs2 ->
-            match l with
-            | R r => In r int_param_regs \/ In r float_param_regs
-            | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ typealign ty = 1
-            | S _ _ _ => False
-            end).
-  {
-    intros. destruct l; auto. destruct sl; auto. intuition xomega.
-  }
+  assert (X: forall ofs1 ofs2 l, loc_argument_charact (Zmax 0 ofs2) l -> ofs1 <= ofs2 -> loc_argument_charact (Zmax 0 ofs1) l).
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition xomega. }
+  assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact (Zmax 0 ofs2)) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact (Zmax 0 ofs1)) p).
+  { destruct p; simpl; intuition eauto. }
   induction tyl; simpl loc_arguments_sf; intros.
   elim H.
   destruct a.
 - (* int *)
   destruct H.
-  destruct (zlt ofs 0); subst l.
-  left; apply ireg_param_in_params.
-  split. xomega. auto.
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct (zlt ofs 0); subst p.
+  apply ireg_param_caller_save.
+  split; [xomega|auto].
+  eapply Y; eauto. omega.
 - (* float *)
   set (ofs' := align ofs 2) in *.
   assert (ofs <= ofs') by (apply align_le; omega).
   destruct H.
-  destruct (zlt ofs' 0); subst l.
-  right; apply freg_param_in_params.
-  split. xomega. auto.
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct (zlt ofs' 0); subst p.
+  apply freg_param_caller_save.
+  split; [xomega|auto].
+  eapply Y. eapply IHtyl; eauto. omega.
 - (* long *)
   set (ofs' := align ofs 2) in *.
   assert (ofs <= ofs') by (apply align_le; omega).
   destruct H.
-  destruct (zlt ofs' 0); subst l.
-  left; apply ireg_param_in_params.
-  split. xomega. auto.
-  destruct H.
-  destruct (zlt ofs' 0); subst l.
-  left; apply ireg_param_in_params.
-  split. xomega. auto.
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct (zlt ofs' 0); subst p.
+  split; apply ireg_param_caller_save.
+  split; (split; [xomega|auto]).
+  eapply Y. eapply IHtyl; eauto. omega.
 - (* single *)
   destruct H.
-  destruct (zlt ofs 0); subst l.
-  right; apply freg_param_in_params.
-  split. xomega. auto.
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct (zlt ofs 0); subst p.
+  apply freg_param_caller_save.
+  split; [xomega|auto].
+  eapply Y; eauto. omega.
 - (* any32 *)
   destruct H.
-  destruct (zlt ofs 0); subst l.
-  left; apply ireg_param_in_params.
-  split. xomega. auto.
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct (zlt ofs 0); subst p.
+  apply ireg_param_caller_save.
+  split; [xomega|auto].
+  eapply Y; eauto. omega.
 - (* any64 *)
   set (ofs' := align ofs 2) in *.
   assert (ofs <= ofs') by (apply align_le; omega).
   destruct H.
-  destruct (zlt ofs' 0); subst l.
-  right; apply freg_param_in_params.
-  split. xomega. auto.
-  eapply INCR. eapply IHtyl; eauto. omega.
+  destruct (zlt ofs' 0); subst p.
+  apply freg_param_caller_save.
+  split; [xomega|auto].
+  eapply Y. eapply IHtyl; eauto. omega.
 Qed.
 
 Lemma loc_arguments_acceptable:
-  forall (s: signature) (l: loc),
-  In l (loc_arguments s) -> loc_argument_acceptable l.
+  forall (s: signature) (p: rpair loc),
+  In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
 Proof.
   unfold loc_arguments; intros.
-  assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal.
-  assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
-  assert (C: forall r, In r int_param_regs \/ In r float_param_regs -> is_callee_save r = false).
-  { intros. destruct H0; auto. }
-  assert (In l (loc_arguments_sf (sig_args s) (-4)) -> loc_argument_acceptable l).
-  { intros. red. exploit loc_arguments_sf_charact; eauto.
-    destruct l as [r | [] ofs ty]; auto. 
-    intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. }
-  assert (In l (loc_arguments_hf (sig_args s) 0 0 0) -> loc_argument_acceptable l).
-  { intros. red. exploit loc_arguments_hf_charact; eauto.
-    destruct l as [r | [] ofs ty]; auto. 
-    intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. }
+  assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
+  { unfold loc_argument_charact, loc_argument_acceptable.
+    destruct l as [r | [] ofs ty]; auto. intros (A & B); split; auto. rewrite B; apply Z.divide_1_l. }
+  assert (Y: forall p, forall_rpair (loc_argument_charact 0) p -> forall_rpair loc_argument_acceptable p).
+  { destruct p0; simpl; intuition auto. }
+  assert (In p (loc_arguments_sf (sig_args s) (-4)) -> forall_rpair loc_argument_acceptable p).
+  { intros. exploit loc_arguments_sf_charact; eauto. }
+  assert (In p (loc_arguments_hf (sig_args s) 0 0 0) -> forall_rpair loc_argument_acceptable p).
+  { intros. exploit loc_arguments_hf_charact; eauto. }
   destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
 Qed.
 
@@ -516,7 +492,7 @@ Qed.
 
 Lemma loc_arguments_hf_bounded:
   forall ofs ty tyl ir fr ofs0,
-  In (S Outgoing ofs ty) (loc_arguments_hf tyl ir fr ofs0) ->
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf tyl ir fr ofs0)) ->
   ofs + typesize ty <= size_arguments_hf tyl ir fr ofs0.
 Proof.
   induction tyl; simpl; intros.
@@ -564,7 +540,7 @@ Qed.
 
 Lemma loc_arguments_sf_bounded:
   forall ofs ty tyl ofs0,
-  In (S Outgoing ofs ty) (loc_arguments_sf tyl ofs0) ->
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) ->
   Zmax 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0.
 Proof.
   induction tyl; simpl; intros.
@@ -602,14 +578,14 @@ 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) (regs_of_rpairs (loc_arguments s)) ->
   ofs + typesize ty <= size_arguments s.
 Proof.
   unfold loc_arguments, size_arguments; intros.
-  assert (In (S Outgoing ofs ty) (loc_arguments_sf (sig_args s) (-4)) ->
+  assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) ->
           ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)).
   { intros. eapply Zle_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. }
-  assert (In (S Outgoing ofs ty) (loc_arguments_hf (sig_args s) 0 0 0) ->
+  assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) ->
           ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0).
   { intros. eapply loc_arguments_hf_bounded; eauto. }
   destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; eauto.