diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 21:58:53 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-09 21:58:53 +0100 |
| commit | fc3c1660ee62b5341ccf75505aa63dca0d2cf16c (patch) | |
| tree | 0ce595db7e1a38db12f17ec25eb4329598f0f2a2 /backend/CSE3analysisproof.v | |
| parent | ab3f3a52c8737dbad6c599d7afc5720346e00abe (diff) | |
| download | compcert-kvx-fc3c1660ee62b5341ccf75505aa63dca0d2cf16c.tar.gz compcert-kvx-fc3c1660ee62b5341ccf75505aa63dca0d2cf16c.zip | |
get moves
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 19 |
1 files changed, 1 insertions, 18 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index fde411cf..29c6618c 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -169,24 +169,7 @@ 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. +Hint Resolve get_kills_has_arg : cse3. Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). |