diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 17:03:24 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 17:03:24 +0100 |
| commit | bdaa3eb0ad6486186519ba1ba574e8ac92505cf0 (patch) | |
| tree | 317a87bfe26b092294e24e1e2c38199e1a7cc54d /mppa_k1c/Asmblockgenproof0.v | |
| parent | b873e06abcee1c7f6a51aaabb973b550a52a5b61 (diff) | |
| download | compcert-kvx-bdaa3eb0ad6486186519ba1ba574e8ac92505cf0.tar.gz compcert-kvx-bdaa3eb0ad6486186519ba1ba574e8ac92505cf0.zip | |
Mise à jour vis à vis de CompCert 3.4
Diffstat (limited to 'mppa_k1c/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index e2b72295..443e8757 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -13,6 +13,7 @@ Require Import Locations. Require Import Machblock. Require Import Asmblock. Require Import Asmblockgen. +Require Import Conventions1. Module MB:=Machblock. Module AB:=Asmblock. @@ -301,6 +302,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 (Asmblock.undef_caller_save_regs rs). +Proof. + intros. destruct H. unfold Mach.undef_caller_save_regs, Asmblock.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 (List.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 -> |