diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-05-27 09:03:30 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-05-27 09:03:30 +0200 |
| commit | 5087ec788016b719b4038be08cd55bccc22b3619 (patch) | |
| tree | 58f0a26f4b02364c0823ba64a2de2df1a073e0a4 /backend/Lineartyping.v | |
| parent | b45cdb9dce7df376fd3cb27a32863af90b847b78 (diff) | |
| parent | 8d3dbd3636fbb6a056f5506be8ee2d8839c1aea2 (diff) | |
| download | compcert-5087ec788016b719b4038be08cd55bccc22b3619.tar.gz compcert-5087ec788016b719b4038be08cd55bccc22b3619.zip | |
Merge pull request #99 from AbsInt/register-pairs
Introduce register pairs to describe calling conventions more precisely
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 22 |
1 files changed, 13 insertions, 9 deletions
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. |