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

diff --git a/backend/XTL.mli b/backend/XTL.mli
index 6bdcc8c6..54988d4b 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -64,6 +64,7 @@ val vloc: loc -> var
 val vlocs: loc list -> var list
 val vmreg: mreg -> var
 val vmregs: mreg list -> var list
+val vlocpairs: loc rpair list -> var list
 
 (* Tests over variables *)