From 62d66f9447330ea4f3c31503465c5dee9ed6a0f5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Mar 2020 18:56:30 +0100 Subject: get_moves --- backend/CSE3analysis.v | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 485b6067..f0af0ac7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -101,7 +101,39 @@ Definition get_kills (eqs : PTree.t equation) : PTree.fold (fun already (eqno : eq_id) (eq : equation) => add_i_j (eq_lhs eq) eqno (add_ilist_j (eq_args eq) eqno already)) eqs - (PMap.init PSet.empty). + (PMap.init PSet.empty). + +Definition is_move (op : operation) : + { op = Omove } + { op <> Omove }. +Proof. + destruct op; try (right ; congruence). + left; trivial. +Qed. + +Definition is_smove (sop : sym_op) : + { sop = SOp Omove } + { sop <> SOp Omove }. +Proof. + destruct sop; try (right ; congruence). + destruct (is_move o). + - left; congruence. + - 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). Record eq_context := mkeqcontext { eq_catalog : node -> option equation; -- cgit