diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 16:52:02 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 16:52:02 +0200 |
| commit | c58b421571b0354eea602adbdae674bd1f4847e3 (patch) | |
| tree | 8c83d3d7428097523d8af00b9abdcf117532be30 /backend/Lineartyping.v | |
| parent | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (diff) | |
| download | compcert-kvx-c58b421571b0354eea602adbdae674bd1f4847e3.tar.gz compcert-kvx-c58b421571b0354eea602adbdae674bd1f4847e3.zip | |
Model external calls as destroying all caller-save registers
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 30cc0d91..fd252dc6 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -149,6 +149,14 @@ Proof. unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto. Qed. +Lemma wt_undef_caller_save_regs: + forall ls, wt_locset ls -> wt_locset (undef_caller_save_regs ls). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l; auto. + destruct (is_callee_save r); auto; simpl; auto. +Qed. + Lemma wt_init: wt_locset (Locmap.init Vundef). Proof. @@ -339,8 +347,9 @@ Local Opaque mreg_type. econstructor. eauto. eauto. eauto. apply wt_undef_regs. apply wt_call_regs. auto. - (* external function *) - econstructor. auto. apply wt_setpair; auto. + econstructor. auto. apply wt_setpair. eapply external_call_well_typed; eauto. + apply wt_undef_caller_save_regs; auto. - (* return *) inv WTSTK. econstructor; eauto. Qed. |