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, 13 insertions, 9 deletions

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 50cd16d6..123c6b5a 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -37,7 +37,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   match sl with
   | Local => zle 0 ofs
   | Outgoing => zle 0 ofs
-  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig))
+  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
   end
   && Zdivide_dec (typealign ty) ofs (typealign_pos ty).
 
@@ -155,15 +155,19 @@ Proof.
   red; intros. unfold Locmap.init. red; auto.
 Qed.
 
-Lemma wt_setlist:
-  forall vl rl rs,
-  Val.has_type_list vl (map mreg_type rl) ->
+Lemma wt_setpair:
+  forall sg v rs,
+  Val.has_type v (proj_sig_res sg) ->
   wt_locset rs ->
-  wt_locset (Locmap.setlist (map R rl) vl rs).
+  wt_locset (Locmap.setpair (loc_result sg) v rs).
 Proof.
-  induction vl; destruct rl; simpl; intros; try contradiction.
+  intros. generalize (loc_result_pair sg) (loc_result_type sg).
+  destruct (loc_result sg); simpl Locmap.setpair.
+- intros. apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+- intros (A & B & C & D) E. 
+  apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
+  apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
   auto.
-  destruct H. apply IHvl; auto. apply wt_setreg; auto.
 Qed.
 
 Lemma wt_setres:
@@ -334,8 +338,8 @@ Proof.
   econstructor. eauto. eauto. eauto.
   apply wt_undef_regs. apply wt_call_regs. auto.
 - (* external function *)
-  econstructor. auto. apply wt_setlist; auto.
-  eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto.
+  econstructor. auto. apply wt_setpair; auto.
+  eapply external_call_well_typed; eauto.
 - (* return *)
   inv WTSTK. econstructor; eauto.
 Qed.