From 82f9d1f96b30106a338e77ec83b7321c2c65f929 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 17 May 2016 15:37:56 +0200
Subject: 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.
---
 backend/Conventions.v | 48 ++++++++++++++++++++++++++++--------------------
 1 file changed, 28 insertions(+), 20 deletions(-)

(limited to 'backend/Conventions.v')

diff --git a/backend/Conventions.v b/backend/Conventions.v
index 69cdd07d..64a83a58 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -22,6 +22,18 @@ Require Export Conventions1.
     [arch/abi/Conventions1.v].  This file adds various processor-independent
     definitions and lemmas. *)
 
+Lemma loc_arguments_acceptable_2:
+  forall s l,
+  In l (regs_of_rpairs (loc_arguments s)) -> loc_argument_acceptable l.
+Proof.
+  intros until l. generalize (loc_arguments_acceptable s). generalize (loc_arguments s).
+  induction l0 as [ | p pl]; simpl; intros.
+- contradiction.
+- rewrite in_app_iff in H0. destruct H0.
+  exploit H; eauto. destruct p; simpl in *; intuition congruence.
+  apply IHpl; auto.
+Qed.
+  
 (** ** Location of function parameters *)
 
 (** A function finds the values of its parameter in the same locations
@@ -35,22 +47,25 @@ Definition parameter_of_argument (l: loc) : loc :=
   | _ => l
   end.
 
-Definition loc_parameters (s: signature) :=
-  List.map parameter_of_argument (loc_arguments s).
+Definition loc_parameters (s: signature) : list (rpair loc) :=
+  List.map (map_rpair parameter_of_argument) (loc_arguments s).
 
 Lemma incoming_slot_in_parameters:
   forall ofs ty sg,
-  In (S Incoming ofs ty) (loc_parameters sg) ->
-  In (S Outgoing ofs ty) (loc_arguments sg).
+  In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters sg)) ->
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)).
 Proof.
   intros.
-  unfold loc_parameters in H.
+  replace (regs_of_rpairs (loc_parameters sg)) with (List.map parameter_of_argument (regs_of_rpairs (loc_arguments sg))) in H.
   change (S Incoming ofs ty) with (parameter_of_argument (S Outgoing ofs ty)) in H.
   exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
-  exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
+  exploit loc_arguments_acceptable_2; eauto. unfold loc_argument_acceptable; intros.
   destruct x; simpl in A; try discriminate.
   destruct sl; try contradiction.
   inv A. auto.
+  unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros.
+  auto.
+  rewrite map_app. f_equal; auto. destruct p; auto. 
 Qed.
 
 (** * Tail calls *)
@@ -62,34 +77,27 @@ Qed.
     arguments are all passed in registers. *)
 
 Definition tailcall_possible (s: signature) : Prop :=
-  forall l, In l (loc_arguments s) ->
+  forall l, In l (regs_of_rpairs (loc_arguments s)) ->
   match l with R _ => True | S _ _ _ => False end.
 
 (** Decide whether a tailcall is possible. *)
 
 Definition tailcall_is_possible (sg: signature) : bool :=
-  let fix tcisp (l: list loc) :=
-    match l with
-    | nil => true
-    | R _ :: l' => tcisp l'
-    | S _ _ _ :: l' => false
-    end
-  in tcisp (loc_arguments sg).
+  List.forallb
+    (fun l => match l with R _ => true | S _ _ _ => false end)
+    (regs_of_rpairs (loc_arguments sg)).
 
 Lemma tailcall_is_possible_correct:
   forall s, tailcall_is_possible s = true -> tailcall_possible s.
 Proof.
-  intro s. unfold tailcall_is_possible, tailcall_possible.
-  generalize (loc_arguments s). induction l; simpl; intros.
-  elim H0.
-  destruct a.
-  destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
+  unfold tailcall_is_possible; intros. rewrite forallb_forall in H. 
+  red; intros. apply H in H0. destruct l; [auto|discriminate]. 
 Qed.
 
 Lemma zero_size_arguments_tailcall_possible:
   forall sg, size_arguments sg = 0 -> tailcall_possible sg.
 Proof.
-  intros; red; intros. exploit loc_arguments_acceptable; eauto.
+  intros; red; intros. exploit loc_arguments_acceptable_2; eauto.
   unfold loc_argument_acceptable.
   destruct l; intros. auto. destruct sl; try contradiction. destruct H1.
   generalize (loc_arguments_bounded _ _ _ H0).
-- 
cgit