From ab3f3a52c8737dbad6c599d7afc5720346e00abe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Mar 2020 19:08:49 +0100 Subject: CSE3 --- backend/CSE3analysisproof.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'backend/CSE3analysisproof.v') 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. -- cgit