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

Last change on this file since 1345 was 1345, checked in by tranquil, 9 years ago

work on ERTL and LTL completed

File size: 9.5 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 Label_ImperativeMap = struct
87
88  type key =
89      Label.Map.key
90 
91  type 'data t =
92      'data Label.Map.t ref
93     
94  let create () =
95    ref Label.Map.empty
96
97  let clear t =
98    t := Label.Map.empty
99   
100  let add k d t =
101    t := Label.Map.add k d !t
102
103  let find k t =
104    Label.Map.find k !t
105
106  let iter f t =
107    Label.Map.iter f !t
108
109end
110
111module F = Fix.Make (Label_ImperativeMap) (L)
112
113(* These are the sets of variables defined at (written by) a statement. *)
114
115let defined (stmt : statement) : L.t =
116  match stmt with
117  | St_skip _
118  | St_comment _
119  | St_cost _
120        | St_ind_0 _
121        | St_ind_inc _
122  | St_push _
123  | St_store _
124  | St_cond _
125  | St_return _ ->
126    L.bottom
127  | St_clear_carry _
128  | St_set_carry _ ->
129    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
130  | St_op2 (I8051.Add, r, _, _, _)
131  | St_op2 (I8051.Addc, r, _, _, _)
132  | St_op2 (I8051.Sub, r, _, _, _) ->
133    L.join (L.hsingleton I8051.carry) (L.psingleton r)
134  | St_op1 (I8051.Inc, r, _, _)
135  | St_get_hdw (r, _, _)
136  | St_framesize (r, _)
137  | St_pop (r, _)
138  | St_int (r, _, _)
139  | St_addrH (r, _, _)
140  | St_addrL (r, _, _)
141  | St_move (r, _, _)
142  | St_opaccsA (_, r, _, _, _)
143  | St_opaccsB (_, r, _, _, _)
144  | St_op1 (_, r, _, _)
145  | St_op2 (_, r, _, _, _)
146  | St_load (r, _, _, _) ->
147    L.psingleton r
148  | St_set_hdw (r, _, _)
149  | St_hdw_to_hdw (r, _, _) ->
150    L.hsingleton r
151  | St_call_id _ ->
152      (* Potentially destroys all caller-save hardware registers. *)
153    Register.Set.empty, I8051.caller_saved
154  | St_newframe _
155  | St_delframe _ ->
156    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
157
158let set_of_list rl =
159  List.fold_right I8051.RegisterSet.add rl I8051.RegisterSet.empty
160
161(* This is the set of variables used at (read by) a statement. *)
162
163let set_of_list =
164  let f set r = I8051.RegisterSet.add r set in
165  List.fold_left f I8051.RegisterSet.empty
166
167let ret_regs = set_of_list I8051.rets
168
169let used (stmt : statement) : L.t =
170  match stmt with
171  | St_skip _
172  | St_comment _
173  | St_cost _
174  | St_ind_0 _
175  | St_ind_inc _
176  | St_framesize _
177  | St_pop _
178  | St_addrH _
179  | St_addrL _
180  | St_int _
181  | St_clear_carry _
182  | St_set_carry _ ->
183    L.bottom
184  | St_call_id (_, nparams, _) ->
185    (* Reads the hardware registers that are used to pass parameters. *)
186    Register.Set.empty,
187    set_of_list (MiscPottier.prefix nparams I8051.parameters)
188  | St_get_hdw (_, r, _)
189  | St_hdw_to_hdw (_, r, _) ->
190    L.hsingleton r
191  | St_set_hdw (_, r, _)
192  | St_push (r, _)
193  | St_move (_, r, _)
194  | St_op1 (_, _, r, _)
195  | St_cond (r, _, _) ->
196    L.psingleton r
197  | St_op2 (I8051.Addc, _, r1, r2, _) ->
198    L.join (L.join (L.psingleton r1) (L.psingleton r2))
199      (L.hsingleton I8051.carry)
200  | St_opaccsA (_, _, r1, r2, _)
201  | St_opaccsB (_, _, r1, r2, _)
202  | St_op2 (_, _, r1, r2, _)
203  | St_load (_, r1, r2, _) ->
204    L.join (L.psingleton r1) (L.psingleton r2)
205  | St_store (r1, r2, r3, _) ->
206    L.join (L.join (L.psingleton r1) (L.psingleton r2)) (L.psingleton r3)
207  | St_newframe _
208  | St_delframe _ ->
209    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)   
210  | St_return _ ->
211    Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
212
213(* A statement is considered pure if it has no side effect, that is, if
214   its only effect is to write a value to its destination variable.
215
216   A pure statement whose destination is dead after the statement will
217   be eliminated during the translation of [ERTL] to [LTL]. This is done by
218   replacing the statement with an [St_skip] statement.
219
220   [eliminable liveafter stmt] returns [Some l], where [l] is [stmt]'s single
221   successor, if statement [stmt] is eliminable. Otherwise, it returns
222   [None]. The parameter [liveafter] is the set of variables that are live
223   after the statement. *)
224
225let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
226  match stmt with
227  | St_skip _
228  | St_comment _
229  | St_cost _
230  | St_ind_0 _
231  | St_ind_inc _
232  | St_newframe _
233  | St_delframe _
234  | St_pop _
235  | St_push _
236  | St_clear_carry _
237  | St_set_carry _
238  | St_store _
239  | St_call_id _
240  | St_cond _
241  | St_return _ ->
242    None
243  | St_get_hdw (r, _, l)
244  | St_framesize (r, l)
245  | St_int (r, _, l)
246  | St_addrH (r, _, l)
247  | St_addrL (r, _, l)
248  | St_move (r, _, l)
249  | St_opaccsA (_, r, _, _, l)
250  | St_opaccsB (_, r, _, _, l)
251  | St_op1 (_, r, _, l)
252  | St_op2 (_, r, _, _, l)
253  | St_load (r, _, _, l) ->
254    if (Register.Set.mem r pliveafter) ||
255       (I8051.RegisterSet.mem I8051.carry hliveafter) then None else Some l
256  | St_set_hdw (r, _, l)
257  | St_hdw_to_hdw (r, _, l) ->
258    if I8051.RegisterSet.mem r hliveafter then None else Some l
259
260(* This is the abstract semantics of instructions. It defines the
261   variables that are live before the instruction in terms of
262   those that are live after the instruction. *)
263
264(* The standard definition is: a variable is considered live
265   before the instruction if either (1) it is used by the instruction,
266   or (2) it is live after the instruction and not defined by the
267   instruction.
268
269   As an exception to this rule, if the instruction is eliminable,
270   then a variable is considered live before the instruction
271   if and only if it is live after the instruction. This anticipates
272   on the instruction's elimination.
273
274   This exception means that the source variables of a pure
275   instruction need not be considered live if the instruction's result
276   is unused. This allows a sequence of pure instructions whose end
277   result is dead to be considered entirely dead.
278
279   It is a simple, but not entirely trivial, exercise to check that
280   this transfer function is monotone. *)
281
282let statement_semantics (stmt : statement) (liveafter : L.t) : L.t =
283  match eliminable liveafter stmt with
284  | None ->
285      L.join (L.diff liveafter (defined stmt)) (used stmt)
286  | Some _ ->
287      liveafter
288
289(* A valuation is a function that maps a program point (a control flow
290   graph label) to the set of variables that are live after that
291   point. *)
292
293type valuation =
294    Label.t -> L.t
295
296(* This is how we turn an [ERTL] procedure into a liveness analysis
297   problem and solve it. *)
298
299let analyze (int_fun : internal_function) : valuation =
300
301  (* Formulate the problem. Construct a system (recursive) equations
302     that describe the live variables before and after each
303     instruction. *)
304
305  (* The following two functions, [livebefore] and [liveafter],
306     define these equations. Both use an oracle, a valuation --
307     also called [liveafter] -- which is supposed to tell us
308     which variables are live after each label. *)
309
310  (* The live variables before an instruction are computed, using the
311     instruction's semantics, in terms of the live variables after the
312     instruction -- which are given by the oracle. *)
313
314  let livebefore label (liveafter : valuation) : L.t =
315    let stmt : statement = Label.Map.find label int_fun.f_graph in
316    statement_semantics stmt (liveafter label)
317  in
318
319  (* The live variables after an instruction are the union of the live
320     variables before each of the instruction's successors. *)
321
322  let liveafter label (liveafter : valuation) : L.t =
323    let stmt : statement = Label.Map.find label int_fun.f_graph in
324    Label.Set.fold (fun successor accu ->
325      L.join (livebefore successor liveafter) accu
326    ) (statement_successors stmt) L.bottom
327  in
328
329  (* Compute the least fixed point of these recursive equations. *)
330
331  F.lfp liveafter
Note: See TracBrowser for help on using the repository browser.