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, 2 insertions, 4 deletions

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 57fc8b86..dec1b988 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -693,10 +693,8 @@ Proof.
   rewrite A; simpl; rewrite C; simpl.
   rewrite H2; rewrite dec_eq_true.
   replace (tailcall_is_possible sig) with true; auto.
-  revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig).
-  induction l; simpl; intros. auto.
-  exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl.
-  intros; apply H3; auto.
+  symmetry. unfold tailcall_is_possible. apply forallb_forall. 
+  intros. apply H3 in H4. destruct x; intuition auto.
 - (* builtin *)
   exploit type_builtin_args_complete; eauto. instantiate (1 := args). intros [e1 [A B]].
   exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]].