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/Asmgenproof0.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/Asmgenproof0.v')
| -rw-r--r-- | backend/Asmgenproof0.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868..70c4323c 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -316,6 +316,23 @@ Proof. intros. rewrite Pregmap.gso; auto. Qed. +Lemma agree_undef_caller_save_regs: + forall ms sp rs, + agree ms sp rs -> + agree (Mach.undef_caller_save_regs ms) sp (Asm.undef_caller_save_regs rs). +Proof. + intros. destruct H. unfold Mach.undef_caller_save_regs, Asm.undef_caller_save_regs; split. +- unfold proj_sumbool; rewrite dec_eq_true. auto. +- auto. +- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). + destruct (in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. ++ apply list_in_map_inv in i. destruct i as (mr & A & B). + assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. + apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. ++ destruct (is_callee_save r) eqn:CS; auto. + elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. +Qed. + Lemma agree_change_sp: forall ms sp rs sp', agree ms sp rs -> sp' <> Vundef -> |