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, 33 insertions, 44 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 84606210..0d25d84a 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -616,51 +616,40 @@ Fixpoint add_equations (rl: list reg) (ml: list mreg) (e: eqs) : option eqs :=
   of pseudoregisters of type [Tlong] in two locations containing the
   two 32-bit halves of the 64-bit integer. *)
 
-Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list loc) (e: eqs) : option eqs :=
+Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc)) (e: eqs) : option eqs :=
   match rl, tyl, ll with
   | nil, nil, nil => Some e
-  | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll =>
-      add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e))
-  | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll =>
+  | r1 :: rl, ty :: tyl, One l1 :: ll =>
       add_equations_args rl tyl ll (add_equation (Eq Full r1 l1) e)
+  | r1 :: rl, Tlong :: tyl, Twolong l1 l2 :: ll =>
+      add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e))
   | _, _, _ => None
   end.
 
 (** [add_equations_res] is similar but is specialized to the case where
   there is only one pseudo-register. *)
 
-Function add_equations_res (r: reg) (oty: option typ) (ll: list loc) (e: eqs) : option eqs :=
-  match oty with
-  | Some Tlong =>
-      match ll with
-      | l1 :: l2 :: nil => Some (add_equation (Eq Low r l2) (add_equation (Eq High r l1) e))
-      | _ => None
-      end
-  | _ =>
-      match ll with
-      | l1 :: nil => Some (add_equation (Eq Full r l1) e)
-      | _ => None
-      end
+Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs :=
+  match p, oty with
+  | One mr, _ =>
+      Some (add_equation (Eq Full r (R mr)) e)
+  | Twolong mr1 mr2, Some Tlong =>
+      Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e))
+  | _, _ =>
+      None
   end.
 
 (** [remove_equations_res] is similar to [add_equations_res] but removes
   equations instead of adding them. *)
 
-Function remove_equations_res (r: reg) (oty: option typ) (ll: list loc) (e: eqs) : option eqs :=
-  match oty with
-  | Some Tlong =>
-      match ll with
-      | l1 :: l2 :: nil =>
-          if Loc.diff_dec l2 l1
-          then Some (remove_equation (Eq Low r l2) (remove_equation (Eq High r l1) e))
-          else None
-      | _ => None
-      end
-  | _ =>
-      match ll with
-      | l1 :: nil => Some (remove_equation (Eq Full r l1) e)
-      | _ => None
-      end
+Function remove_equations_res (r: reg) (p: rpair mreg) (e: eqs) : option eqs :=
+  match p with
+  | One mr =>
+      Some (remove_equation (Eq Full r (R mr)) e)
+  | Twolong mr1 mr2 =>
+      if mreg_eq mr2 mr1
+      then None
+      else Some (remove_equation (Eq Low r (R mr2)) (remove_equation (Eq High r (R mr1)) e))
   end.
 
 (** [add_equations_ros] adds an equation, if needed, between an optional
@@ -960,10 +949,11 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       track_moves env mv1 e3
   | BScall sg ros args res mv1 ros' mv2 s =>
       let args' := loc_arguments sg in
-      let res' := map R (loc_result sg) in
+      let res' := loc_result sg in
       do e1 <- track_moves env mv2 e;
-      do e2 <- remove_equations_res res (sig_res sg) res' e1;
-      assertion (forallb (fun l => reg_loc_unconstrained res l e2) res');
+      do e2 <- remove_equations_res res res' e1;
+      assertion (forallb (fun l => reg_loc_unconstrained res l e2)
+                         (map R (regs_of_rpair res')));
       assertion (no_caller_saves e2);
       do e3 <- add_equation_ros ros ros' e2;
       do e4 <- add_equations_args args (sig_args sg) args' e3;
@@ -1000,7 +990,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
   | BSreturn None mv =>
       track_moves env mv empty_eqs
   | BSreturn (Some arg) mv =>
-      let arg' := map R (loc_result (RTL.fn_sig f)) in
+      let arg' := loc_result (RTL.fn_sig f) in
       do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
       track_moves env mv e1
   end.
@@ -1184,15 +1174,15 @@ Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) :=
   involving pseudoregs [r'] not in [rparams]: these equations are
   automatically satisfied since the initial value of [r'] is [Vundef]. *)
 
-Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e: eqs)
+Function compat_entry (rparams: list reg) (lparams: list (rpair loc)) (e: eqs)
                       {struct rparams} : bool :=
-  match rparams, tys, lparams with
-  | nil, nil, nil => true
-  | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll =>
-      compat_left2 r1 l1 l2 e && compat_entry rl tyl ll e
-  | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll =>
-      compat_left r1 l1 e && compat_entry rl tyl ll e
-  | _, _, _ => false
+  match rparams, lparams with
+  | nil, nil => true
+  | r1 :: rl,  One l1 :: ll =>
+      compat_left r1 l1 e && compat_entry rl ll e
+  | r1 :: rl, Twolong l1 l2 :: ll =>
+      compat_left2 r1 l1 l2 e && compat_entry rl ll e
+  | _, _ => false
   end.
 
 (** Checking the satisfiability of equations inferred at function entry
@@ -1204,7 +1194,6 @@ Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function)
   do mv <- pair_entrypoints rtl ltl;
   do e2 <- track_moves env mv e1;
   assertion (compat_entry (RTL.fn_params rtl)
-                          (sig_args (RTL.fn_sig rtl))
                           (loc_parameters (RTL.fn_sig rtl)) e2);
   assertion (can_undef destroyed_at_function_entry e2);
   assertion (zeq (RTL.fn_stacksize rtl) (LTL.fn_stacksize ltl));