diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 17:34:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 17:34:03 +0100 |
| commit | e4c7ff447ad30832c42ee51f0fe7e1cf62d2eee9 (patch) | |
| tree | a8f92ebb47582726fc86900055d9ce46c72614cf /backend/CSE2proof.v | |
| parent | 27b985393cd8d90a3d6f5e9f13bdf90e4300bb8e (diff) | |
| download | compcert-kvx-e4c7ff447ad30832c42ee51f0fe7e1cf62d2eee9.tar.gz compcert-kvx-e4c7ff447ad30832c42ee51f0fe7e1cf62d2eee9.zip | |
wellformed_reg_kill_mem
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 4d503f90..0d369e7a 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -321,7 +321,8 @@ Proof. rewrite PTree.gro by congruence. apply Hrel; trivial. Qed. - +Local Hint Resolve wellformed_reg_kill_reg : wellformed. + Lemma wellformed_mem_kill_mem: forall rel, (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)). @@ -343,6 +344,21 @@ Proof. Qed. Local Hint Resolve wellformed_mem_kill_mem : wellformed. +Lemma wellformed_reg_kill_mem: + forall rel, + (wellformed_reg rel) -> (wellformed_reg (kill_mem rel)). +Proof. + unfold wellformed_reg, kill_mem. + simpl. + intros rel Hrel. + intros i j sv KILLMEM KILLABLE. + apply Hrel with (sv := sv); trivial. + rewrite PTree.gremove_t in KILLMEM. + destruct ((mem_used rel) ! i) in KILLMEM. + discriminate. + assumption. +Qed. + Lemma wellformed_mem_move: forall r dst rel, (wellformed_mem rel) -> (wellformed_mem (move r dst rel)). |