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

Last change on this file since 2169 was 2169, checked in by tranquil, 6 years ago

corrected bug where definition of carry bit by MUL and DIV (which always clear the bit) was not registered

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