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

Last change on this file since 818 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

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