blob: 485b606774f259f8039f7d797b3eba15a385bcbb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps CSE2deps.
Require Import HashedSet.
Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
Definition t := PSet.t.
Definition eq (x : t) (y : t) := x = y.
Lemma eq_refl: forall x, eq x x.
Proof.
unfold eq. trivial.
Qed.
Lemma eq_sym: forall x y, eq x y -> eq y x.
Proof.
unfold eq. congruence.
Qed.
Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
Proof.
unfold eq. congruence.
Qed.
Definition beq (x y : t) := if PSet.eq x y then true else false.
Lemma beq_correct: forall x y, beq x y = true -> eq x y.
Proof.
unfold beq.
intros.
destruct PSet.eq; congruence.
Qed.
Definition ge (x y : t) := (PSet.is_subset x y) = true.
Lemma ge_refl: forall x y, eq x y -> ge x y.
Proof.
unfold eq, ge.
intros.
subst y.
apply PSet.is_subset_spec.
trivial.
Qed.
Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
Proof.
unfold ge.
intros.
rewrite PSet.is_subset_spec in *.
intuition.
Qed.
Definition lub := PSet.inter.
Lemma ge_lub_left: forall x y, ge (lub x y) x.
Proof.
unfold ge, lub.
intros.
apply PSet.is_subset_spec.
intro.
rewrite PSet.ginter.
rewrite andb_true_iff.
intuition.
Qed.
Lemma ge_lub_right: forall x y, ge (lub x y) y.
Proof.
unfold ge, lub.
intros.
apply PSet.is_subset_spec.
intro.
rewrite PSet.ginter.
rewrite andb_true_iff.
intuition.
Qed.
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 := node.
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.
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.
Definition get_kills (eqs : PTree.t equation) :
Regmap.t PSet.t :=
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).
Record eq_context := mkeqcontext
{ eq_catalog : node -> option equation;
eq_kills : reg -> PSet.t }.
Section OPERATIONS.
Context {ctx : eq_context}.
Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t :=
PSet.subtract rel (eq_kills ctx r).
End OPERATIONS.
Definition totoro := RELATION.lub.
|
