source: Deliverables/D2.2/8051/src/ERTL/liveness.ml @ 1580

Last change on this file since 1580 was 1580, checked in by tranquil, 8 years ago

implemented constant propagation in LTL
cleaned up translations in optimizations, a new module for translations is available

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  | St_call_ptr (_, _, _, l) ->
44    Label.Set.singleton l
45  | St_cond (_, l1, l2) ->
46    Label.Set.add l1 (Label.Set.singleton l2)
47
48(* The analysis uses the lattice of sets of variables. The lattice's
49   join operation is pointwise set union, which reflects the fact that
50   a variable is deemed live at a program point if and only if it is
51   live at any of the successors of that program point. *)
52
53module L = struct
54
55  (* A set of variable is represented as a pair of a set of
56     pseudo-registers and a set of hardware registers. *)
57
58  type t =
59      Register.Set.t * I8051.RegisterSet.t
60
61  type property =
62      t
63
64  let bottom =
65    Register.Set.empty, I8051.RegisterSet.empty
66
67  let psingleton r =
68    Register.Set.singleton r, I8051.RegisterSet.empty
69
70  let hsingleton hwr =
71    Register.Set.empty, I8051.RegisterSet.singleton hwr
72
73  let join (rset1, hwrset1) (rset2, hwrset2) =
74    (Register.Set.union rset1 rset2, I8051.RegisterSet.union hwrset1 hwrset2)
75
76  let diff (rset1, hwrset1) (rset2, hwrset2) =
77    (Register.Set.diff rset1 rset2, I8051.RegisterSet.diff hwrset1 hwrset2)
78
79  let equal (rset1, hwrset1) (rset2, hwrset2) =
80    Register.Set.equal rset1 rset2 && I8051.RegisterSet.equal hwrset1 hwrset2
81
82  let is_maximal _ =
83    false
84
85end
86
87module F = Fix.Make (Label.ImpMap) (L)
88
89(* These are the sets of variables defined at (written by) a statement. *)
90
91let defined (stmt : statement) : L.t =
92  match stmt with
93  | St_skip _
94  | St_comment _
95  | St_cost _
96  | St_ind_0 _
97  | St_ind_inc _
98  | St_push _
99  | St_store _
100  | St_cond _
101  | St_return _ ->
102    L.bottom
103  | St_clear_carry _
104  | St_set_carry _ ->
105    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
106  | St_op2 (I8051.Add, r, _, _, _)
107  | St_op2 (I8051.Addc, r, _, _, _)
108  | St_op2 (I8051.Sub, r, _, _, _) ->
109    L.join (L.hsingleton I8051.carry) (L.psingleton 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 _ | St_call_ptr _  ->
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 add_arg : RTL.argument -> L.property -> L.property = function
145  | RTL.Reg r -> L.join (L.psingleton r)
146  | RTL.Imm _ -> fun x -> x
147
148let used (stmt : statement) : L.t =
149  match stmt with
150  | St_skip _
151  | St_comment _
152  | St_cost _
153  | St_ind_0 _
154  | St_ind_inc _
155  | St_framesize _
156  | St_pop _
157  | St_addrH _
158  | St_addrL _
159  (* | St_int _ *)
160  | St_clear_carry _
161  | St_set_carry _ ->
162    L.bottom
163  | St_call_id (_, nparams, _) ->
164    (* Reads the hardware registers that are used to pass parameters. *)
165    Register.Set.empty,
166    set_of_list (MiscPottier.prefix nparams I8051.parameters)
167  | St_call_ptr (r1, r2, nparams, _) ->
168    (* Reads the hardware registers that are used to pass parameters. *)
169    Register.Set.of_list [r1 ; r2],
170    set_of_list (MiscPottier.prefix nparams I8051.parameters)
171  | St_get_hdw (_, r, _)
172  | St_hdw_to_hdw (_, r, _) ->
173    L.hsingleton r
174  | St_op1 (_, _, r, _)
175  | St_cond (r, _, _) ->
176    L.psingleton r
177  | St_set_hdw (_, a, _)
178  | St_push (a, _)
179  | St_move (_, a, _) ->
180    add_arg a L.bottom
181  | St_op2 ((I8051.Addc | I8051.Sub), _, a1, a2, _) ->
182    add_arg a1 (add_arg a2 (L.hsingleton I8051.carry))
183  | St_opaccsA (_, _, a1, a2, _)
184  | St_opaccsB (_, _, a1, a2, _)
185  | St_op2 (_, _, a1, a2, _)
186  | St_load (_, a1, a2, _) ->
187    add_arg a1 (add_arg a2 L.bottom)
188  | St_store (a1, a2, a3, _) ->
189    add_arg a1 (add_arg a2 (add_arg a3 L.bottom))
190  | St_newframe _
191  | St_delframe _ ->
192    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
193  | St_return _ ->
194    Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
195
196(* A statement is considered pure if it has no side effect, that is, if
197   its only effect is to write a value to its destination variable.
198
199   A pure statement whose destination is dead after the statement will
200   be eliminated during the translation of [ERTL] to [LTL]. This is done by
201   replacing the statement with an [St_skip] statement.
202
203   [eliminable liveafter stmt] returns [Some l], where [l] is [stmt]'s single
204   successor, if statement [stmt] is eliminable. Otherwise, it returns
205   [None]. The parameter [liveafter] is the set of variables that are live
206   after the statement. *)
207
208let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
209  match stmt with
210  | St_skip _
211  | St_comment _
212  | St_cost _
213  | St_ind_0 _
214  | St_ind_inc _
215  | St_newframe _
216  | St_delframe _
217  | St_pop _
218  | St_push _
219  | St_clear_carry _
220  | St_set_carry _
221  | St_store _
222  | St_call_id _
223  | St_call_ptr _
224  | St_cond _
225  | St_return _ ->
226    None
227  | St_get_hdw (r, _, l)
228  | St_framesize (r, l)
229  (* | St_int (r, _, l) *)
230  | St_addrH (r, _, l)
231  | St_addrL (r, _, l)
232  | St_move (r, _, l)
233  | St_opaccsA (_, r, _, _, l)
234  | St_opaccsB (_, r, _, _, l)
235  | St_op1 (_, r, _, l)
236  | St_op2 (_, r, _, _, l)
237  | St_load (r, _, _, l) ->
238    if (Register.Set.mem r pliveafter) ||
239       (I8051.RegisterSet.mem I8051.carry hliveafter) then None else Some l
240  | St_set_hdw (r, _, l)
241  | St_hdw_to_hdw (r, _, l) ->
242    if I8051.RegisterSet.mem r hliveafter then None else Some l
243
244(* This is the abstract semantics of instructions. It defines the
245   variables that are live before the instruction in terms of
246   those that are live after the instruction. *)
247
248(* The standard definition is: a variable is considered live
249   before the instruction if either (1) it is used by the instruction,
250   or (2) it is live after the instruction and not defined by the
251   instruction.
252
253   As an exception to this rule, if the instruction is eliminable,
254   then a variable is considered live before the instruction
255   if and only if it is live after the instruction. This anticipates
256   on the instruction's elimination.
257
258   This exception means that the source variables of a pure
259   instruction need not be considered live if the instruction's result
260   is unused. This allows a sequence of pure instructions whose end
261   result is dead to be considered entirely dead.
262
263   It is a simple, but not entirely trivial, exercise to check that
264   this transfer function is monotone. *)
265
266let statement_semantics (stmt : statement) (liveafter : L.t) : L.t =
267  match eliminable liveafter stmt with
268  | None ->
269      L.join (L.diff liveafter (defined stmt)) (used stmt)
270  | Some _ ->
271      liveafter
272
273(* A valuation is a function that maps a program point (a control flow
274   graph label) to the set of variables that are live after that
275   point. *)
276
277type valuation =
278    Label.t -> L.t
279
280(* This is how we turn an [ERTL] procedure into a liveness analysis
281   problem and solve it. *)
282
283let analyze (int_fun : internal_function) : valuation =
284
285  (* Formulate the problem. Construct a system (recursive) equations
286     that describe the live variables before and after each
287     instruction. *)
288
289  (* The following two functions, [livebefore] and [liveafter],
290     define these equations. Both use an oracle, a valuation --
291     also called [liveafter] -- which is supposed to tell us
292     which variables are live after each label. *)
293
294  (* The live variables before an instruction are computed, using the
295     instruction's semantics, in terms of the live variables after the
296     instruction -- which are given by the oracle. *)
297
298  let livebefore label (liveafter : valuation) : L.t =
299    let stmt : statement = Label.Map.find label int_fun.f_graph in
300    statement_semantics stmt (liveafter label)
301  in
302
303  (* The live variables after an instruction are the union of the live
304     variables before each of the instruction's successors. *)
305
306  let liveafter label (liveafter : valuation) : L.t =
307    let stmt : statement = Label.Map.find label int_fun.f_graph in
308    Label.Set.fold (fun successor accu ->
309      L.join (livebefore successor liveafter) accu
310    ) (statement_successors stmt) L.bottom
311  in
312
313  (* Compute the least fixed point of these recursive equations. *)
314
315  F.lfp liveafter
Note: See TracBrowser for help on using the repository browser.