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. --- backend/Lineartyping.v | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'backend/Lineartyping.v') diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 50cd16d6..123c6b5a 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -37,7 +37,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool := match sl with | Local => zle 0 ofs | Outgoing => zle 0 ofs - | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig)) + | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig))) end && Zdivide_dec (typealign ty) ofs (typealign_pos ty). @@ -155,15 +155,19 @@ Proof. red; intros. unfold Locmap.init. red; auto. Qed. -Lemma wt_setlist: - forall vl rl rs, - Val.has_type_list vl (map mreg_type rl) -> +Lemma wt_setpair: + forall sg v rs, + Val.has_type v (proj_sig_res sg) -> wt_locset rs -> - wt_locset (Locmap.setlist (map R rl) vl rs). + wt_locset (Locmap.setpair (loc_result sg) v rs). Proof. - induction vl; destruct rl; simpl; intros; try contradiction. + intros. generalize (loc_result_pair sg) (loc_result_type sg). + destruct (loc_result sg); simpl Locmap.setpair. +- intros. apply wt_setreg; auto. eapply Val.has_subtype; eauto. +- intros (A & B & C & D) E. + apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I. + apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I. auto. - destruct H. apply IHvl; auto. apply wt_setreg; auto. Qed. Lemma wt_setres: @@ -334,8 +338,8 @@ Proof. econstructor. eauto. eauto. eauto. apply wt_undef_regs. apply wt_call_regs. auto. - (* external function *) - econstructor. auto. apply wt_setlist; auto. - eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto. + econstructor. auto. apply wt_setpair; auto. + eapply external_call_well_typed; eauto. - (* return *) inv WTSTK. econstructor; eauto. Qed. -- cgit