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

diff --git a/common/Events.v b/common/Events.v
index 040029fb..c94d6d35 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1487,193 +1487,6 @@ Proof.
   intros. exploit external_call_determ. eexact H. eexact H0. intuition.
 Qed.
 
-(** Late in the back-end, calling conventions for external calls change:
-  arguments and results of type [Tlong] are passed as two integers.
-  We now wrap [external_call] to adapt to this convention. *)
-
-Fixpoint decode_longs (tyl: list typ) (vl: list val) : list val :=
-  match tyl with
-  | nil => nil
-  | Tlong :: tys =>
-      match vl with
-      | v1 :: v2 :: vs => Val.longofwords v1 v2 :: decode_longs tys vs
-      | _ => nil
-      end
-  | ty :: tys =>
-      match vl with
-      | v1 :: vs => v1 :: decode_longs tys vs
-      | _ => nil
-      end
-  end.
-
-Definition encode_long (oty: option typ) (v: val) : list val :=
-  match oty with
-  | Some Tlong => Val.hiword v :: Val.loword v :: nil
-  | _ => v :: nil
-  end.
-
-Definition proj_sig_res' (s: signature) : list typ :=
-  match s.(sig_res) with
-  | Some Tlong => Tint :: Tint :: nil
-  | Some ty => ty :: nil
-  | None => Tint :: nil
-  end.
-
-Inductive external_call'
-      (ef: external_function) (ge: Senv.t)
-      (vargs: list val) (m1: mem) (t: trace) (vres: list val) (m2: mem) : Prop :=
-  external_call'_intro: forall v,
-    external_call ef ge (decode_longs (sig_args (ef_sig ef)) vargs) m1 t v m2 ->
-    vres = encode_long (sig_res (ef_sig ef)) v ->
-    external_call' ef ge vargs m1 t vres m2.
-
-Lemma decode_longs_lessdef:
-  forall tyl vl1 vl2, Val.lessdef_list vl1 vl2 -> Val.lessdef_list (decode_longs tyl vl1) (decode_longs tyl vl2).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_lessdef; auto.
-Qed.
-
-Lemma decode_longs_inject:
-  forall f tyl vl1 vl2, Val.inject_list f vl1 vl2 -> Val.inject_list f (decode_longs tyl vl1) (decode_longs tyl vl2).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. Qed.
-
-Lemma encode_long_lessdef:
-  forall oty v1 v2, Val.lessdef v1 v2 -> Val.lessdef_list (encode_long oty v1) (encode_long oty v2).
-Proof.
-  intros. destruct oty as [[]|]; simpl; auto.
-  constructor. apply Val.hiword_lessdef; auto. constructor. apply Val.loword_lessdef; auto. auto.
-Qed.
-
-Lemma encode_long_inject:
-  forall f oty v1 v2, Val.inject f v1 v2 -> Val.inject_list f (encode_long oty v1) (encode_long oty v2).
-Proof.
-  intros. destruct oty as [[]|]; simpl; auto.
-  constructor. apply Val.hiword_inject; auto. constructor. apply Val.loword_inject; auto. auto.
-Qed.
-
-Lemma encode_long_has_type:
-  forall v sg,
-  Val.has_type v (proj_sig_res sg) ->
-  Val.has_type_list (encode_long (sig_res sg) v) (proj_sig_res' sg).
-Proof.
-  unfold proj_sig_res, proj_sig_res', encode_long; intros.
-  destruct (sig_res sg) as [[] | ]; simpl; auto.
-  destruct v; simpl; auto.
-Qed.
-
-Lemma external_call_well_typed':
-  forall ef ge vargs m1 t vres m2,
-  external_call' ef ge vargs m1 t vres m2 ->
-  Val.has_type_list vres (proj_sig_res' (ef_sig ef)).
-Proof.
-  intros. inv H. apply encode_long_has_type.
-  eapply external_call_well_typed; eauto.
-Qed.
-
-Lemma external_call_symbols_preserved':
-  forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
-  external_call' ef ge1 vargs m1 t vres m2 ->
-  Senv.equiv ge1 ge2 ->
-  external_call' ef ge2 vargs m1 t vres m2.
-Proof.
-  intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto.
-Qed.
-
-Lemma external_call_valid_block':
-  forall ef ge vargs m1 t vres m2 b,
-  external_call' ef ge vargs m1 t vres m2 ->
-  Mem.valid_block m1 b -> Mem.valid_block m2 b.
-Proof.
-  intros. inv H. eapply external_call_valid_block; eauto.
-Qed.
-
-Lemma external_call_nextblock':
-  forall ef ge vargs m1 t vres m2,
-  external_call' ef ge vargs m1 t vres m2 ->
-  Ple (Mem.nextblock m1) (Mem.nextblock m2).
-Proof.
-  intros. inv H. eapply external_call_nextblock; eauto.
-Qed.
-
-Lemma external_call_mem_extends':
-  forall ef ge vargs m1 t vres m2 m1' vargs',
-  external_call' ef ge vargs m1 t vres m2 ->
-  Mem.extends m1 m1' ->
-  Val.lessdef_list vargs vargs' ->
-  exists vres' m2',
-     external_call' ef ge vargs' m1' t vres' m2'
-  /\ Val.lessdef_list vres vres'
-  /\ Mem.extends m2 m2'
-  /\ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'.
-Proof.
-  intros. inv H.
-  exploit external_call_mem_extends; eauto.
-  eapply decode_longs_lessdef; eauto.
-  intros (v' & m2' & A & B & C & D).
-  exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition.
-  econstructor; eauto.
-  eapply encode_long_lessdef; eauto.
-Qed.
-
-Lemma external_call_mem_inject':
-  forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs',
-  meminj_preserves_globals ge f ->
-  external_call' ef ge vargs m1 t vres m2 ->
-  Mem.inject f m1 m1' ->
-  Val.inject_list f vargs vargs' ->
-  exists f' vres' m2',
-     external_call' ef ge vargs' m1' t vres' m2'
-  /\ Val.inject_list f' vres vres'
-  /\ Mem.inject f' m2 m2'
-  /\ Mem.unchanged_on (loc_unmapped f) m1 m2
-  /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
-  /\ inject_incr f f'
-  /\ inject_separated f f' m1 m1'.
-Proof.
-  intros. inv H0.
-  exploit external_call_mem_inject; eauto.
-  eapply decode_longs_inject; eauto.
-  intros (f' & v' & m2' & A & B & C & D & E & P & Q).
-  exists f'; exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition.
-  econstructor; eauto.
-  apply encode_long_inject; auto.
-Qed.
-
-Lemma external_call_determ':
-  forall ef ge vargs m t1 vres1 m1 t2 vres2 m2,
-  external_call' ef ge vargs m t1 vres1 m1 ->
-  external_call' ef ge vargs m t2 vres2 m2 ->
-  match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2).
-Proof.
-  intros. inv H; inv H0. exploit external_call_determ. eexact H1. eexact H.
-  intros [A B]. split. auto. intros. destruct B as [C D]; auto. subst. auto.
-Qed.
-
-Lemma external_call_match_traces':
-  forall ef ge vargs m t1 vres1 m1 t2 vres2 m2,
-  external_call' ef ge vargs m t1 vres1 m1 ->
-  external_call' ef ge vargs m t2 vres2 m2 ->
-  match_traces ge t1 t2.
-Proof.
-  intros. inv H; inv H0. eapply external_call_match_traces; eauto.
-Qed.
-
-Lemma external_call_deterministic':
-  forall ef ge vargs m t vres1 m1 vres2 m2,
-  external_call' ef ge vargs m t vres1 m1 ->
-  external_call' ef ge vargs m t vres2 m2 ->
-  vres1 = vres2 /\ m1 = m2.
-Proof.
-  intros. inv H; inv H0.
-  exploit external_call_deterministic. eexact H1. eexact H. intros [A B].
-  split; congruence.
-Qed.
-
 (** * Evaluation of builtin arguments *)
 
 Section EVAL_BUILTIN_ARG.