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, 34 insertions, 17 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index b350b047..010d5d7b 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -310,12 +310,12 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
 Definition undef_flags (rs: regset) : regset :=
   fun r => match r with CR _ => Vundef | _ => rs r end.
 
-(** Assigning multiple registers *)
+(** Assigning a register pair *)
 
-Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
-  match rl, vl with
-  | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
-  | _, _ => rs
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
+  match p with
+  | One r => rs#r <- v
+  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
   end.
 
 (** Assigning the result of a builtin *)
@@ -813,12 +813,21 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
                 (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v ->
       extcall_arg rs m (S Outgoing ofs ty) v.
 
+Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
+  | extcall_arg_one: forall l v,
+      extcall_arg rs m l v ->
+      extcall_arg_pair rs m (One l) v
+  | extcall_arg_twolong: forall hi lo vhi vlo,
+      extcall_arg rs m hi vhi ->
+      extcall_arg rs m lo vlo ->
+      extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
+
 Definition extcall_arguments
     (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
+  list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
 
-Definition loc_external_result (sg: signature) : list preg :=
-  map preg_of (loc_result sg).
+Definition loc_external_result (sg: signature) : rpair preg :=
+  map_rpair preg_of (loc_result sg).
 
 (** Execution of the instruction at [rs#PC]. *)
 
@@ -848,9 +857,9 @@ Inductive step: state -> trace -> state -> Prop :=
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
-      external_call' ef ge args m t res m' ->
+      external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (set_regs (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) ->
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) ->
       step (State rs m) t (State rs' m').
 
 End RELSEM.
@@ -884,13 +893,21 @@ Remark extcall_arguments_determ:
   extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
 Proof.
   intros until m.
-  assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 ->
-          forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2).
+  assert (A: forall l v1 v2,
+             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
+  { intros. inv H; inv H0; congruence. }
+  assert (B: forall p v1 v2,
+             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
+  { intros. inv H; inv H0. 
+    eapply A; eauto.
+    f_equal; eapply A; eauto. }
+  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
+             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
+  {
     induction 1; intros vl2 EA; inv EA.
     auto.
-    f_equal; auto.
-    inv H; inv H3; congruence.
-  intros. red in H0; red in H1. eauto.
+    f_equal; eauto. }
+  intros. eapply C; eauto.
 Qed.
 
 Lemma semantics_determinate: forall p, determinate (semantics p).
@@ -911,13 +928,13 @@ Ltac Equalities :=
   exploit external_call_determ. eexact H5. eexact H11. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
   assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-  exploit external_call_determ'. eexact H3. eexact H8. intros [A B].
+  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
 (* trace length *)
   red; intros; inv H; simpl.
   omega.
   inv H3; eapply external_call_trace_length; eauto.
-  inv H2; eapply external_call_trace_length; eauto.
+  eapply external_call_trace_length; eauto.
 (* initial states *)
   inv H; inv H0. f_equal. congruence.
 (* final no step *)