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/Stackingproof.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/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f7570f57..5dbc4532 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -666,6 +666,16 @@ Proof. apply agree_regs_set_reg; auto. Qed. +Lemma agree_regs_undef_caller_save_regs: + forall j ls rs, + agree_regs j ls rs -> + agree_regs j (LTL.undef_caller_save_regs ls) (Mach.undef_caller_save_regs rs). +Proof. + intros; red; intros. + unfold LTL.undef_caller_save_regs, Mach.undef_caller_save_regs. + destruct (is_callee_save r); auto. +Qed. + (** Preservation under assignment of stack slot *) Lemma agree_regs_set_slot: @@ -826,6 +836,16 @@ Proof. unfold return_regs. destruct l; auto. rewrite H; auto. Qed. +Lemma agree_callee_save_undef_caller_save_regs: + forall ls1 ls2, + agree_callee_save ls1 ls2 -> + agree_callee_save (LTL.undef_caller_save_regs ls1) ls2. +Proof. + intros; red; intros. unfold LTL.undef_caller_save_regs. + destruct l; auto. + rewrite H0; auto. +Qed. + Lemma agree_callee_save_set_result: forall sg v ls1 ls2, agree_callee_save ls1 ls2 -> @@ -2113,8 +2133,10 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_states_return with (j := j'). eapply match_stacks_change_meminj; eauto. - apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto. - apply agree_callee_save_set_result; auto. + apply agree_regs_set_pair. apply agree_regs_undef_caller_save_regs. + apply agree_regs_inject_incr with j; auto. + auto. + apply agree_callee_save_set_result. apply agree_callee_save_undef_caller_save_regs. auto. apply stack_contents_change_meminj with j; auto. rewrite sep_comm, sep_assoc; auto. |