diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 21:39:43 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 21:56:53 +0100 |
| commit | f2b898dfb741210596e5fb92e44094fc0fdb989e (patch) | |
| tree | 5341a058037854e8019d5dd1ff9fba1cbfc84835 /backend/CSE3analysis.v | |
| parent | e76b8244db0c8394eb9f62a573ea0f511bd8db31 (diff) | |
| download | compcert-kvx-f2b898dfb741210596e5fb92e44094fc0fdb989e.tar.gz compcert-kvx-f2b898dfb741210596e5fb92e44094fc0fdb989e.zip | |
xget_kills_monotone
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 31 |
1 files changed, 27 insertions, 4 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index c490ec08..3e225fb4 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -146,10 +146,33 @@ Proof. - apply IHilist. assumption. Qed. - -Definition xget_kills (eqs : PTree.t equation) := + +Definition xget_kills (eqs : PTree.t equation) (m : Regmap.t PSet.t) : + Regmap.t PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => add_i_j (eq_lhs eq) eqno - (add_ilist_j (eq_args eq) eqno already)). - + (add_ilist_j (eq_args eq) eqno already)) eqs m. + +Lemma xget_kills_monotone : + forall eqs m i j, + PSet.contains (Regmap.get i m) j = true -> + PSet.contains (Regmap.get i (xget_kills eqs m)) j = true. +Proof. + unfold xget_kills. + intros eqs m. + rewrite PTree.fold_spec. + generalize (PTree.elements eqs). + intro. + generalize m. + clear m. + induction l; simpl; trivial. + intros. + apply IHl. + apply add_i_j_monotone. + apply add_ilist_j_monotone. + assumption. +Qed. + +Definition eq_involves (eq : equation) (i : reg) := + i = (eq_lhs eq) \/ In i (eq_args eq). Definition totoro := RELATION.lub. |