source: Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml @ 1589

Last change on this file since 1589 was 1589, checked in by tranquil, 8 years ago
  • turned to argument-less return statements for RTLabs and RTL (there was a hidden invariant, for which the arguments of return statements where equal to the f_result field of the function definition: they were useless and an optimization was breaking the compilation)
  • corrected a bug in liveness analysis I had introduced
File size: 11.4 KB
Line 
1(* Pasted from Pottier's PP compiler *)
2
3(* This module translates [ERTL] statements into [LTL] statements. It is
4   parameterized over a module [Env], whose signature appears below, which
5   provides support for mapping pseudo-registers to stack slots or hardware
6   registers and for generating instructions (which requires allocating fresh
7   control flow graph labels). *)
8
9type decision =
10  | Spill of AST.immediate
11  | Color of I8051.register
12
13module Make (Env : sig
14
15  val lookup: Register.t -> decision
16
17  (* [generate stmt] returns a fresh statement label, which it associates with
18     [stmt] in the control flow graph. *)
19
20  val generate: LTL.statement -> Label.t
21
22  val fresh_label: unit -> Label.t
23
24  val add_graph: Label.t -> LTL.statement -> unit
25
26  val locals: int
27
28  val stacksize: int
29
30end) = struct
31
32  open Env
33  open I8051
34
35
36  type argument =
37    | AColor of I8051.register
38    | ASpill of AST.immediate
39    | AImm of AST.immediate
40
41  let lookup_as_arg r = match lookup r with
42    | Spill k -> ASpill k
43    | Color r -> AColor r
44
45  let lookup_arg = function
46    | RTL.Imm k -> AImm k
47    | RTL.Reg r -> lookup_as_arg r
48
49  let adjust off = locals - (off + I8051.int_size)
50
51  (* side-effects : dpl, dph, a *)
52  let move_sp_to_dptr off l =
53    let off = adjust off in
54    if off = 0 then
55      let l = generate (LTL.St_from_acc (I8051.dph, l)) in
56      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
57      let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
58      LTL.St_to_acc (I8051.spl, l)
59    else
60      let l = generate (LTL.St_from_acc (I8051.dph, l)) in
61      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
62      let l = generate (LTL.St_int (I8051.a, 0, l)) in
63      let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
64      let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
65      LTL.St_int (I8051.a, off, l)
66
67
68  (* side-effects : dpl, dph, a *)
69  let get_stack r off l =
70    let l =
71      if I8051.eq_reg r I8051.a then l else generate (LTL.St_from_acc (r, l)) in
72    let l = generate (LTL.St_load l) in
73    move_sp_to_dptr off l
74
75  (* side-effects : dpl, dph, a *)
76  let set_stack_not_a off r l =
77    let l = generate (LTL.St_store l) in
78    let l = generate (LTL.St_to_acc (r, l)) in
79    move_sp_to_dptr off l
80
81  (* side-effects : dpl, dph, st0 *)
82  let set_stack_a off l =
83    let l = generate (set_stack_not_a off I8051.st0 l) in
84    LTL.St_from_acc (I8051.st0, l)
85
86  (* side-effects : dpl, dph, st0 if r = a, a if r != a *)
87  let set_stack off r =
88    if I8051.eq_reg r I8051.a then set_stack_a off else
89      set_stack_not_a off r
90
91  (* side-effects : dpl, dph, a *)
92  let set_stack_int off k l =
93    let l = generate (LTL.St_store l) in
94    let l = generate (LTL.St_int (I8051.a, k, l)) in
95    move_sp_to_dptr off l
96
97
98  (* side-effects : (dpl, dph, a) if dest spilled *)
99  let move_int (dest : decision) (k : int) l =
100    match dest with
101      | Color desthwr -> LTL.St_int (desthwr, k, l)
102      | Spill off -> set_stack_int off k l
103
104  (* side-effects : none if dest = src, a if both colored,
105                    (dpl, dph, a) if src spilled or src imm and dest spilled,
106                    (dpl, dph, a, st0) if dest spilled *)
107  let move (dest : decision) (src : argument) l =
108    match dest, src with
109      | _, AImm k -> move_int dest k l
110      (* Both pseudo-registers are translated to hardware registers. Issue move
111         statements, or no statement at all if both pseudo-registers reside in
112         the same hardware register. *)
113      | Color desthwr, AColor sourcehwr
114        when I8051.eq_reg desthwr sourcehwr ->
115        LTL.St_skip l
116      | Color desthwr, AColor sourcehwr
117        when I8051.eq_reg desthwr I8051.a ->
118        LTL.St_to_acc (sourcehwr, l)
119      | Color desthwr, AColor sourcehwr
120        when I8051.eq_reg sourcehwr I8051.a ->
121        LTL.St_from_acc (desthwr, l)
122      | Color desthwr, AColor sourcehwr ->
123        let l = generate (LTL.St_from_acc (desthwr, l)) in
124        LTL.St_to_acc (sourcehwr, l)
125
126      (* One pseudo-register is translated to a hardware register, while the
127         other is spilled. Issue a single stack access instruction. *)
128      | Color desthwr, ASpill off -> get_stack desthwr off l
129      | Spill off, AColor sourcehwr -> set_stack off sourcehwr l
130
131      (* Both pseudo-registers are spilled. Combine the previous two cases. Of
132         course, if the two pseudo-registers have been spilled into the same
133         stack slot, there is nothing to do. *)
134      | Spill off1, ASpill off2 when off1 = off2 ->
135        LTL.St_skip l
136      | Spill off1, ASpill off2 ->
137        let l = generate (set_stack_a off1 l) in
138        get_stack I8051.a off2 l
139
140  (* side-effects (dpl, dph) if either spilled, (dpl, dph, b) if both *)
141  let op2 op (dest : decision) (src1 : argument) (src2 : argument) l =
142    let l = generate (move dest (AColor I8051.a) l) in
143    match op, src1, src2 with
144      | _, _, AImm k ->
145        let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in
146        move (Color I8051.a) src1 l
147        (* if op is commutative, we can do as above if first is hwr *)
148      | (Add | Addc | And | Or | Xor), AImm k, _ ->
149        let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in
150        move (Color I8051.a) src2 l
151      | _, _, AColor src2hwr ->
152        let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in
153        move (Color I8051.a) src1 l
154      | (Add | Addc | And | Or | Xor), AColor src1hwr, _ ->
155        let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in
156        move (Color I8051.a) src2 l
157      | _, _, _ ->
158        let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in
159        let l = generate (move (Color I8051.a) src1 l) in
160        move (Color I8051.b) src2 l
161
162  (* side-effects : a, b if both spilled *)
163  let move_to_dptr (addr1 : argument) (addr2 : argument) l =
164    match addr1, addr2 with
165      | ASpill _, ASpill _  ->
166        let l = generate (move (Color I8051.dph) (AColor I8051.b) l) in
167        let l = generate (move (Color I8051.dpl) addr1 l) in
168        move (Color I8051.b) addr2 l
169      | (AColor _ | AImm _) , _ ->
170        (* the following does not change dph, as addr1 is hwr *)
171        let l = generate (move (Color I8051.dpl) addr1 l) in
172        move (Color I8051.dph) addr2 l
173      | _, (AColor _ | AImm _) ->
174        (* the following does not change dpl, as addr2 is hwr *)
175        let l = generate (move (Color I8051.dph) addr2 l) in
176        move (Color I8051.dpl) addr1 l
177
178  (* side-effects :  dpl, dph, b if both addr spilled,
179                     st0 if srcr = a or srcr spilled, a if srcrs != a *)
180  let store (addr1 : argument) (addr2 : argument) (srcr : argument) l =
181    let l = generate (LTL.St_store l) in
182    match srcr with
183      | AColor r when I8051.eq_reg r a ->
184        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
185        let l = generate (move_to_dptr addr1 addr2 l) in
186        LTL.St_from_acc (I8051.st0, l)
187      | AColor r ->
188        let l = generate (LTL.St_to_acc (r, l)) in
189        move_to_dptr addr1 addr2 l
190      | AImm k ->
191        let l = generate (LTL.St_int (I8051.a, k, l)) in
192        move_to_dptr addr1 addr2 l
193      | ASpill _ ->
194        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
195        let l = generate (move_to_dptr addr1 addr2 l) in
196        move (Color I8051.st0) srcr l
197
198  let newframe l =
199    if stacksize = 0 then LTL.St_skip l
200    else
201      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
202      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm 0, l)) in
203      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
204      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
205      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm stacksize, l)) in
206      let l = generate (LTL.St_clear_carry l) in
207      LTL.St_to_acc (I8051.spl, l)
208
209  let delframe l =
210    if stacksize = 0 then LTL.St_skip l
211    else
212      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
213      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
214      let l = generate (LTL.St_int (I8051.a, 0, l)) in
215      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
216      let l = generate (LTL.St_op2 (I8051.Add, LTL.Imm stacksize, l)) in
217      LTL.St_to_acc (I8051.spl, l)
218
219
220  (* ------------------------------------------------------------------------ *)
221
222  (* [translate_statement] turns a [ERTL] statement into a [LTL] statement, or
223     sequence of statements, that transfers control to the same label(s).
224
225     Existing statement labels are preserved, that is, the labels in the new
226     control flow graph form a superset of the labels in the existing control
227     flow graph. *)
228
229  let translate_statement (stmt : ERTL.statement) : LTL.statement =
230    match stmt with
231
232      | ERTL.St_skip l ->
233        LTL.St_skip l
234
235      | ERTL.St_comment (s, l) ->
236        LTL.St_comment (s, l)
237
238      | ERTL.St_cost (cost_lbl, l) ->
239        LTL.St_cost (cost_lbl, l)
240
241      | ERTL.St_ind_0 (i, l) ->
242        LTL.St_ind_0 (i, l)
243
244      | ERTL.St_ind_inc (i, l) ->
245        LTL.St_ind_inc (i, l)
246
247      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
248        move (lookup destr) (AColor sourcehwr) l
249
250      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
251        move (Color desthwr) (lookup_arg sourcer) l
252
253      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
254        move (Color r1) (AColor r2) l
255
256      | ERTL.St_newframe l ->
257        newframe l
258
259      | ERTL.St_delframe l ->
260        delframe l
261
262      | ERTL.St_framesize (r, l) ->
263        move_int (lookup r) stacksize l
264
265      | ERTL.St_pop (r, l) ->
266        let l = generate (move (lookup r) (AColor I8051.a) l) in
267        LTL.St_pop l
268
269      | ERTL.St_push (r, l) ->
270        let l = generate (LTL.St_push l) in
271        move (Color I8051.a) (lookup_arg r) l
272
273      | ERTL.St_addrH (r, x, l) ->
274        let l = generate (move (lookup r) (AColor I8051.dph) l) in
275        LTL.St_addr (x, l)
276
277      | ERTL.St_addrL (r, x, l) ->
278        let l = generate (move (lookup r) (AColor I8051.dpl) l) in
279        LTL.St_addr (x, l)
280
281      | ERTL.St_move (r, a, l) ->
282        move (lookup r) (lookup_arg a) l
283
284      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
285        let l = generate (move (lookup destr) (AColor I8051.a) l) in
286        let l = generate (LTL.St_opaccs (opaccs, l)) in
287        let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in
288        move (Color I8051.b) (lookup_arg srcr2) l
289
290      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
291        let l = generate (move (lookup destr) (AColor I8051.b) l) in
292        let l = generate (LTL.St_opaccs (opaccs, l)) in
293        let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in
294        move (Color I8051.b) (lookup_arg srcr2) l
295
296      | ERTL.St_op1 (op1, destr, srcr, l) ->
297        let l = generate (move (lookup destr) (AColor I8051.a) l) in
298        let l = generate (LTL.St_op1 (op1, l)) in
299        move (Color I8051.a) (lookup_as_arg srcr) l
300
301      | ERTL.St_op2 (op, destr, arg1, arg2, l) ->
302        op2 op (lookup destr) (lookup_arg arg1) (lookup_arg arg2) l
303
304      | ERTL.St_clear_carry l ->
305        LTL.St_clear_carry l
306
307      | ERTL.St_set_carry l ->
308        LTL.St_set_carry l
309
310      | ERTL.St_load (destr, addr1, addr2, l) ->
311        let l = generate (move (lookup destr) (AColor I8051.a) l) in
312        let l = generate (LTL.St_load l) in
313        move_to_dptr (lookup_arg addr1) (lookup_arg addr2) l
314
315      | ERTL.St_store (addr1, addr2, srcr, l) ->
316        store (lookup_arg addr1) (lookup_arg addr2) (lookup_arg srcr) l
317
318      | ERTL.St_call_id (f, _, l) ->
319        LTL.St_call_id (f, l)
320
321      | ERTL.St_call_ptr (f1, f2, _, l) ->
322        let l = generate (LTL.St_call_ptr l) in
323        move_to_dptr (lookup_as_arg f1) (lookup_as_arg f2) l
324
325      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
326        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
327        move (Color I8051.a) (lookup_as_arg srcr) l
328
329      | ERTL.St_return _ ->
330        LTL.St_return
331
332(* ------------------------------------------------------------------------- *)
333
334end
Note: See TracBrowser for help on using the repository browser.