diff options
| -rw-r--r-- | backend/CSE3analysis.v | 15 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 19 |
2 files changed, 4 insertions, 30 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index f0af0ac7..da527995 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -119,21 +119,12 @@ Proof. - right; congruence. Qed. -Definition get_move (eq : equation) := - if is_smove (eq_op eq) - then match eq_args eq with - | h::nil => Some h - | _ => None - end - else None. - Definition get_moves (eqs : PTree.t equation) : Regmap.t PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => - match get_move eq with - | Some rhs => add_i_j (eq_lhs eq) rhs already - | None => already - end) eqs (PMap.init PSet.empty). + if is_smove (eq_op eq) + then add_i_j (eq_lhs eq) eqno already + else already) eqs (PMap.init PSet.empty). Record eq_context := mkeqcontext { eq_catalog : node -> option equation; 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). |