From 82f9d1f96b30106a338e77ec83b7321c2c65f929 Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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. --- common/Events.v | 187 -------------------------------------------------------- 1 file changed, 187 deletions(-) (limited to 'common/Events.v') 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. -- cgit