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/Tunnelingproof.v | |
| parent | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (diff) | |
| download | compcert-c58b421571b0354eea602adbdae674bd1f4847e3.tar.gz compcert-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/Tunnelingproof.v')
| -rw-r--r-- | backend/Tunnelingproof.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index c6644ceb..fd97ce33 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -334,6 +334,14 @@ Proof. induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef. Qed. +Lemma locmap_undef_caller_save_regs_lessdef: + forall ls1 ls2, + locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l; auto. destruct (Conventions1.is_callee_save r); auto. +Qed. + Lemma find_function_translated: forall ros ls tls fd, locmap_lessdef ls tls -> @@ -516,7 +524,7 @@ Proof. left; simpl; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. - simpl. econstructor; eauto using locmap_setpair_lessdef. + simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef. - (* return *) inv STK. inv H1. left; econstructor; split. |