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

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