diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 19:08:49 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 19:08:49 +0100 |
| commit | ab3f3a52c8737dbad6c599d7afc5720346e00abe (patch) | |
| tree | 8dd6535da29ead6d8ab9c97357d35b82c01f6554 /backend/CSE3analysisproof.v | |
| parent | 62d66f9447330ea4f3c31503465c5dee9ed6a0f5 (diff) | |
| download | compcert-kvx-ab3f3a52c8737dbad6c599d7afc5720346e00abe.tar.gz compcert-kvx-ab3f3a52c8737dbad6c599d7afc5720346e00abe.zip | |
CSE3
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index d3681398..fde411cf 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -169,6 +169,25 @@ Proof. - assumption. Qed. +Definition xlget_moves (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : + Regmap.t PSet.t := + List.fold_left(fun already eq_id_no => + match get_move (snd eq_id_no) with + | Some rhs => add_i_j (eq_lhs (snd eq_id_no)) rhs already + | None => already + end) eqs m. + +Lemma xlget_moves_monotone: + forall eqs m i j, + PSet.contains (Regmap.get i m) j = true -> + PSet.contains (Regmap.get i (xlget_moves eqs m)) j = true. +Proof. + induction eqs; intros; simpl; trivial. + destruct get_move; auto with cse3. +Qed. + +Hint Resolve xlget_moves_monotone : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). @@ -259,4 +278,6 @@ Section SOUNDNESS. - rewrite Regmap.gso by congruence. assumption. Qed. + + End SOUNDNESS. |