diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 21:08:04 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 21:08:04 +0100 |
| commit | dabfcfe9aeffe4bcb3d2a27a46e2b10b5d725154 (patch) | |
| tree | a94edb31dd86bea27239da998d5518eb5c716278 /backend/CSE2proof.v | |
| parent | c877fef46e86bbd088e3d3937ce96572bee0101d (diff) | |
| download | compcert-kvx-dabfcfe9aeffe4bcb3d2a27a46e2b10b5d725154.tar.gz compcert-kvx-dabfcfe9aeffe4bcb3d2a27a46e2b10b5d725154.zip | |
wellformedness for reg begins; simplified
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 86bc123d..350cdb24 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -72,8 +72,10 @@ Definition wellformed_reg (rel : RELATION.t) : Prop := forall i j sv, (var_to_sym rel) ! i = Some sv -> kill_sym_val j sv = true -> - exists uses, (reg_used rel) ! j = Some uses /\ - uses ! i = Some tt. + match (reg_used rel) ! j with + | Some uses => uses ! i = Some tt + | None => False + end. Lemma wellformed_mem_top : wellformed_mem RELATION.top. Proof. @@ -134,20 +136,15 @@ Proof. destruct (eq_sym_val syma symb); try discriminate. subst syma. inv COMBINE. - assert (exists usesA : pset, (reg_used a) ! j = Some usesA /\ usesA ! i = Some tt) as USESA by auto. - assert (exists usesB : pset, (reg_used b) ! j = Some usesB /\ usesB ! i = Some tt) as USESB by auto. - destruct USESA as [uA [uA1 uA2]]. - destruct USESB as [uB [uB1 uB2]]. rewrite PTree.gcombine_null. - rewrite uA1. - rewrite uB1. - pose proof (PTree.bempty_canon_correct (pset_inter uA uB) i) as EMPTY. - destruct PTree.bempty_canon. + destruct ((reg_used a) ! j) as [uA| ]; destruct ((reg_used b) ! j) as [uB | ]; auto. + { pose proof (PTree.bempty_canon_correct (pset_inter uA uB) i) as EMPTY. + destruct PTree.bempty_canon. - rewrite gpset_inter_none in EMPTY. intuition congruence. - - econstructor; split; eauto. - rewrite gpset_inter_some. + - rewrite gpset_inter_some. auto. + } Qed. Local Hint Resolve wellformed_reg_lub : wellformed. |