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, 5 insertions, 0 deletions

diff --git a/backend/XTL.ml b/backend/XTL.ml
index 2ddbc50a..a1b7f23b 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -64,6 +64,11 @@ let vlocs ll = List.map vloc ll
 let vmreg mr = L(R mr)
 let vmregs mrl = List.map vmreg mrl
 
+let rec vlocpairs = function
+  | [] -> []
+  | One l :: ll -> L l :: vlocpairs ll
+  | Twolong(l1, l2) :: ll -> L l1 :: L l2 :: vlocpairs ll
+
 (* Tests over variables *)
 
 let is_stack_reg = function