source: Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/liveness.ml @ 1468

Last change on this file since 1468 was 1468, checked in by tranquil, 9 years ago
  • implemented constant propagation
  • implementing partial redundancy elimination
File size: 9.1 KB
Line 
1(* Pasted from Pottier's PP compiler *)
2
3open ERTL
4
5(* In the following, a ``variable'' means a pseudo-register or an
6   allocatable hardware register. *)
7
8(* These functions allow turning an [ERTL] control flow graph into an
9   explicit graph, that is, making successor edges explicit. This is
10   useful in itself and facilitates the computation of predecessor
11   edges. *)
12
13let statement_successors (stmt : statement) =
14  match stmt with
15  | St_return _ ->
16    Label.Set.empty
17  | St_skip l
18  | St_comment (_, l)
19  | St_cost (_, l)
20  | St_ind_0 (_, l)
21  | St_ind_inc (_, l)
22  | St_set_hdw (_, _, l)
23  | St_get_hdw (_, _, l)
24  | St_hdw_to_hdw (_, _, l)
25  | St_newframe l
26  | St_delframe l
27  | St_framesize (_, l)
28  | St_push (_, l)
29  | St_pop (_, l)
30  | St_addrH (_, _, l)
31  | St_addrL (_, _, l)
32  | St_int (_, _, l)
33  | St_move (_, _, l)
34  | St_opaccsA (_, _, _, _, l)
35  | St_opaccsB (_, _, _, _, l)
36  | St_op1 (_, _, _, l)
37  | St_op2 (_, _, _, _, l)
38  | St_clear_carry l
39  | St_set_carry l
40  | St_load (_, _, _, l)
41  | St_store (_, _, _, l)
42  | St_call_id (_, _, l) ->
43    Label.Set.singleton l
44  | St_cond (_, l1, l2) ->
45    Label.Set.add l1 (Label.Set.singleton l2)
46
47(* The analysis uses the lattice of sets of variables. The lattice's
48   join operation is pointwise set union, which reflects the fact that
49   a variable is deemed live at a program point if and only if it is
50   live at any of the successors of that program point. *)
51
52module L = struct
53
54  (* A set of variable is represented as a pair of a set of
55     pseudo-registers and a set of hardware registers. *)
56
57  type t =
58      Register.Set.t * I8051.RegisterSet.t
59
60  type property =
61      t
62
63  let bottom =
64    Register.Set.empty, I8051.RegisterSet.empty
65
66  let psingleton r =
67    Register.Set.singleton r, I8051.RegisterSet.empty
68
69  let hsingleton hwr =
70    Register.Set.empty, I8051.RegisterSet.singleton hwr
71
72  let join (rset1, hwrset1) (rset2, hwrset2) =
73    (Register.Set.union rset1 rset2, I8051.RegisterSet.union hwrset1 hwrset2)
74
75  let diff (rset1, hwrset1) (rset2, hwrset2) =
76    (Register.Set.diff rset1 rset2, I8051.RegisterSet.diff hwrset1 hwrset2)
77
78  let equal (rset1, hwrset1) (rset2, hwrset2) =
79    Register.Set.equal rset1 rset2 && I8051.RegisterSet.equal hwrset1 hwrset2
80
81  let is_maximal _ =
82    false
83
84end
85
86module F = Fix.Make (Label.ImpMap) (L)
87
88(* These are the sets of variables defined at (written by) a statement. *)
89
90let defined (stmt : statement) : L.t =
91  match stmt with
92  | St_skip _
93  | St_comment _
94  | St_cost _
95        | St_ind_0 _
96        | St_ind_inc _
97  | St_push _
98  | St_store _
99  | St_cond _
100  | St_return _ ->
101    L.bottom
102  | St_clear_carry _
103  | St_set_carry _ ->
104    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
105  | St_op2 (I8051.Add, r, _, _, _)
106  | St_op2 (I8051.Addc, r, _, _, _)
107  | St_op2 (I8051.Sub, r, _, _, _) ->
108    L.join (L.hsingleton I8051.carry) (L.psingleton r)
109  | St_op1 (I8051.Inc, r, _, _)
110  | St_get_hdw (r, _, _)
111  | St_framesize (r, _)
112  | St_pop (r, _)
113  | St_int (r, _, _)
114  | St_addrH (r, _, _)
115  | St_addrL (r, _, _)
116  | St_move (r, _, _)
117  | St_opaccsA (_, r, _, _, _)
118  | St_opaccsB (_, r, _, _, _)
119  | St_op1 (_, r, _, _)
120  | St_op2 (_, r, _, _, _)
121  | St_load (r, _, _, _) ->
122    L.psingleton r
123  | St_set_hdw (r, _, _)
124  | St_hdw_to_hdw (r, _, _) ->
125    L.hsingleton r
126  | St_call_id _ ->
127      (* Potentially destroys all caller-save hardware registers. *)
128    Register.Set.empty, I8051.caller_saved
129  | St_newframe _
130  | St_delframe _ ->
131    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
132
133let set_of_list rl =
134  List.fold_right I8051.RegisterSet.add rl I8051.RegisterSet.empty
135
136(* This is the set of variables used at (read by) a statement. *)
137
138let set_of_list =
139  let f set r = I8051.RegisterSet.add r set in
140  List.fold_left f I8051.RegisterSet.empty
141
142let ret_regs = set_of_list I8051.rets
143
144let used (stmt : statement) : L.t =
145  match stmt with
146  | St_skip _
147  | St_comment _
148  | St_cost _
149  | St_ind_0 _
150  | St_ind_inc _
151  | St_framesize _
152  | St_pop _
153  | St_addrH _
154  | St_addrL _
155  | St_int _
156  | St_clear_carry _
157  | St_set_carry _ ->
158    L.bottom
159  | St_call_id (_, nparams, _) ->
160    (* Reads the hardware registers that are used to pass parameters. *)
161    Register.Set.empty,
162    set_of_list (MiscPottier.prefix nparams I8051.parameters)
163  | St_get_hdw (_, r, _)
164  | St_hdw_to_hdw (_, r, _) ->
165    L.hsingleton r
166  | St_set_hdw (_, r, _)
167  | St_push (r, _)
168  | St_move (_, r, _)
169  | St_op1 (_, _, r, _)
170  | St_cond (r, _, _) ->
171    L.psingleton r
172  | St_op2 (I8051.Addc, _, r1, r2, _) ->
173    L.join (L.join (L.psingleton r1) (L.psingleton r2))
174      (L.hsingleton I8051.carry)
175  | St_opaccsA (_, _, r1, r2, _)
176  | St_opaccsB (_, _, r1, r2, _)
177  | St_op2 (_, _, r1, r2, _)
178  | St_load (_, r1, r2, _) ->
179    L.join (L.psingleton r1) (L.psingleton r2)
180  | St_store (r1, r2, r3, _) ->
181    L.join (L.join (L.psingleton r1) (L.psingleton r2)) (L.psingleton r3)
182  | St_newframe _
183  | St_delframe _ ->
184    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)   
185  | St_return _ ->
186    Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
187
188(* A statement is considered pure if it has no side effect, that is, if
189   its only effect is to write a value to its destination variable.
190
191   A pure statement whose destination is dead after the statement will
192   be eliminated during the translation of [ERTL] to [LTL]. This is done by
193   replacing the statement with an [St_skip] statement.
194
195   [eliminable liveafter stmt] returns [Some l], where [l] is [stmt]'s single
196   successor, if statement [stmt] is eliminable. Otherwise, it returns
197   [None]. The parameter [liveafter] is the set of variables that are live
198   after the statement. *)
199
200let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
201  match stmt with
202  | St_skip _
203  | St_comment _
204  | St_cost _
205  | St_ind_0 _
206  | St_ind_inc _
207  | St_newframe _
208  | St_delframe _
209  | St_pop _
210  | St_push _
211  | St_clear_carry _
212  | St_set_carry _
213  | St_store _
214  | St_call_id _
215  | St_cond _
216  | St_return _ ->
217    None
218  | St_get_hdw (r, _, l)
219  | St_framesize (r, l)
220  | St_int (r, _, l)
221  | St_addrH (r, _, l)
222  | St_addrL (r, _, l)
223  | St_move (r, _, l)
224  | St_opaccsA (_, r, _, _, l)
225  | St_opaccsB (_, r, _, _, l)
226  | St_op1 (_, r, _, l)
227  | St_op2 (_, r, _, _, l)
228  | St_load (r, _, _, l) ->
229    if (Register.Set.mem r pliveafter) ||
230       (I8051.RegisterSet.mem I8051.carry hliveafter) then None else Some l
231  | St_set_hdw (r, _, l)
232  | St_hdw_to_hdw (r, _, l) ->
233    if I8051.RegisterSet.mem r hliveafter then None else Some l
234
235(* This is the abstract semantics of instructions. It defines the
236   variables that are live before the instruction in terms of
237   those that are live after the instruction. *)
238
239(* The standard definition is: a variable is considered live
240   before the instruction if either (1) it is used by the instruction,
241   or (2) it is live after the instruction and not defined by the
242   instruction.
243
244   As an exception to this rule, if the instruction is eliminable,
245   then a variable is considered live before the instruction
246   if and only if it is live after the instruction. This anticipates
247   on the instruction's elimination.
248
249   This exception means that the source variables of a pure
250   instruction need not be considered live if the instruction's result
251   is unused. This allows a sequence of pure instructions whose end
252   result is dead to be considered entirely dead.
253
254   It is a simple, but not entirely trivial, exercise to check that
255   this transfer function is monotone. *)
256
257let statement_semantics (stmt : statement) (liveafter : L.t) : L.t =
258  match eliminable liveafter stmt with
259  | None ->
260      L.join (L.diff liveafter (defined stmt)) (used stmt)
261  | Some _ ->
262      liveafter
263
264(* A valuation is a function that maps a program point (a control flow
265   graph label) to the set of variables that are live after that
266   point. *)
267
268type valuation =
269    Label.t -> L.t
270
271(* This is how we turn an [ERTL] procedure into a liveness analysis
272   problem and solve it. *)
273
274let analyze (int_fun : internal_function) : valuation =
275
276  (* Formulate the problem. Construct a system (recursive) equations
277     that describe the live variables before and after each
278     instruction. *)
279
280  (* The following two functions, [livebefore] and [liveafter],
281     define these equations. Both use an oracle, a valuation --
282     also called [liveafter] -- which is supposed to tell us
283     which variables are live after each label. *)
284
285  (* The live variables before an instruction are computed, using the
286     instruction's semantics, in terms of the live variables after the
287     instruction -- which are given by the oracle. *)
288
289  let livebefore label (liveafter : valuation) : L.t =
290    let stmt : statement = Label.Map.find label int_fun.f_graph in
291    statement_semantics stmt (liveafter label)
292  in
293
294  (* The live variables after an instruction are the union of the live
295     variables before each of the instruction's successors. *)
296
297  let liveafter label (liveafter : valuation) : L.t =
298    let stmt : statement = Label.Map.find label int_fun.f_graph in
299    Label.Set.fold (fun successor accu ->
300      L.join (livebefore successor liveafter) accu
301    ) (statement_successors stmt) L.bottom
302  in
303
304  (* Compute the least fixed point of these recursive equations. *)
305
306  F.lfp liveafter
Note: See TracBrowser for help on using the repository browser.