From dc13dcbf1138be32db14be0a9e132d8326bb2dc5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 5 Mar 2020 21:10:49 +0100
Subject: xget_kills

---
 backend/CSE3analysis.v | 74 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 06de1b08..c490ec08 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -78,4 +78,78 @@ End RELATION.
 Module RB := ADD_BOTTOM(RELATION).
 Module DS := Dataflow_Solver(RB)(NodeSetForward).
 
+Inductive sym_op : Type :=
+| SOp : operation -> sym_op
+| SLoad : memory_chunk -> addressing -> sym_op.
+
+Record equation :=
+  mkequation
+    { eq_lhs : reg;
+      eq_op : sym_op;
+      eq_args : list reg }.
+
+Definition eq_id := positive.
+
+Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
+  Regmap.set i (PSet.add j (Regmap.get i m)) m.
+
+Lemma add_i_j_adds : forall i j m,
+    PSet.contains (Regmap.get i (add_i_j i j m)) j = true.
+Proof.
+  intros.
+  unfold add_i_j.
+  rewrite Regmap.gss.
+  auto with pset.
+Qed.
+
+Lemma add_i_j_monotone : forall i j i' j' m,
+    PSet.contains (Regmap.get i' m) j' = true ->
+    PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true.
+Proof.
+  intros.
+  unfold add_i_j.
+  destruct (peq i i').
+  - subst i'.
+    rewrite Regmap.gss.
+    destruct (peq j j').
+    + subst j'.
+      apply PSet.gadds.
+    + eauto with pset.
+  - rewrite Regmap.gso.
+    assumption.
+    congruence.
+Qed.
+
+Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) :=
+  List.fold_left (fun already i => add_i_j i j already) ilist m.
+
+Lemma add_ilist_j_monotone : forall ilist j i' j' m,
+    PSet.contains (Regmap.get i' m) j' = true ->
+    PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true.
+Proof.
+  induction ilist; simpl; intros until m; intro CONTAINS; trivial.
+  apply IHilist.
+  apply add_i_j_monotone.
+  assumption.
+Qed.
+
+Lemma add_ilist_j_adds : forall ilist j m,
+    forall i, In i ilist ->
+              PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true.
+Proof.
+  induction ilist; simpl; intros until i; intro IN.
+  contradiction.
+  destruct IN as [HEAD | TAIL].
+  - subst a.
+    apply add_ilist_j_monotone.
+    apply add_i_j_adds.
+  - apply IHilist.
+    assumption.
+Qed.
+    
+Definition xget_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)). 
+             
 Definition totoro := RELATION.lub.
-- 
cgit