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, 26 insertions, 8 deletions

diff --git a/backend/Locations.v b/backend/Locations.v
index 6ca84ea7..52abfc46 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -386,17 +386,35 @@ Module Locmap.
     auto.
   Qed.
 
-  Fixpoint setlist (ll: list loc) (vl: list val) (m: t) {struct ll} : t :=
-    match ll, vl with
-    | l1 :: ls, v1 :: vs => setlist ls vs (set l1 v1 m)
-    | _, _ => m
+  Definition getpair (p: rpair loc) (m: t) : val :=
+    match p with
+    | One l => m l
+    | Twolong l1 l2 => Val.longofwords (m l1) (m l2)
     end.
 
-  Lemma gsetlisto: forall l ll vl m, Loc.notin l ll -> (setlist ll vl m) l = m l.
+  Definition setpair (p: rpair mreg) (v: val) (m: t) : t :=
+    match p with
+    | One r => set (R r) v m
+    | Twolong hi lo => set (R lo) (Val.loword  v) (set (R hi) (Val.hiword v) m)
+    end.
+
+  Lemma getpair_exten:
+    forall p ls1 ls2,
+    (forall l, In l (regs_of_rpair p) -> ls2 l = ls1 l) ->
+    getpair p ls2 = getpair p ls1.
   Proof.
-    induction ll; simpl; intros.
-    auto.
-    destruct vl; auto. destruct H. rewrite IHll; auto. apply gso; auto. apply Loc.diff_sym; auto.
+    intros. destruct p; simpl. 
+    apply H; simpl; auto.
+    f_equal; apply H; simpl; auto.
+  Qed.
+
+  Lemma gpo:
+    forall p v m l,
+    forall_rpair (fun r => Loc.diff l (R r)) p -> setpair p v m l = m l.
+  Proof.
+    intros; destruct p; simpl in *. 
+  - apply gso. apply Loc.diff_sym; auto.
+  - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto.
   Qed.
 
   Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t :=