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

Last change on this file was 2100, checked in by tranquil, 7 years ago

temporary solution to a bug where operations on spilled registers disrupted the carry bit

File size: 12.1 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, st1 if adjust off <> 0 *)
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_op2 (I8051.Sub, LTL.Reg I8051.st1, l)) in
61      let l = generate (LTL.St_clear_carry l) in
62      let l = generate (LTL.St_int (I8051.a, 0, l)) in
63      (* ^ restore the carry bit ^ *)
64      let l = generate (LTL.St_from_acc (I8051.dph, l)) in
65      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
66      let l = generate (LTL.St_int (I8051.a, 0, l)) in
67      let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
68      let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
69      let l = generate (LTL.St_int (I8051.a, off, l)) in
70      let l = generate (LTL.St_from_acc (I8051.st1, l)) in
71      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Imm 0, l)) in
72      LTL.St_int (I8051.a, 0, l)
73      (* ^ save the carry bit ^ *)
74
75
76  (* side-effects : dpl, dph, a, st1 if adjust off <> 0 *)
77  let get_stack r off l =
78    let l =
79      if I8051.eq_reg r I8051.a then l else generate (LTL.St_from_acc (r, l)) in
80    let l = generate (LTL.St_load l) in
81    move_sp_to_dptr off l
82
83  (* side-effects : dpl, dph, a, st1 if adjust off <> 0 *)
84  let set_stack_not_a off r l =
85    let l = generate (LTL.St_store l) in
86    let l = generate (LTL.St_to_acc (r, l)) in
87    move_sp_to_dptr off l
88
89  (* side-effects : dpl, dph, st0, st1 if adjust off <> 0 *)
90  let set_stack_a off l =
91    let l = generate (set_stack_not_a off I8051.st0 l) in
92    LTL.St_from_acc (I8051.st0, l)
93
94  (* side-effects : dpl, dph, st0 if r = a, a if r != a, st1 if adjust off <> 0 *)
95  let set_stack off r =
96    if I8051.eq_reg r I8051.a then set_stack_a off else
97      set_stack_not_a off r
98
99  (* side-effects : dpl, dph, a, st1 if adjust off <> 0 *)
100  let set_stack_int off k l =
101    let l = generate (LTL.St_store l) in
102    let l = generate (LTL.St_int (I8051.a, k, l)) in
103    move_sp_to_dptr off l
104
105
106  (* side-effects : (dpl, dph, a, st1 if adjust off <> 0) if dest spilled *)
107  let move_int (dest : decision) (k : int) l =
108    match dest with
109      | Color desthwr -> LTL.St_int (desthwr, k, l)
110      | Spill off -> set_stack_int off k l
111
112  (* side-effects : none if dest = src, a if both colored,
113                    (dpl, dph, a, st1 if adjust off <> 0) if src spilled or src imm and dest spilled,
114                    (dpl, dph, a, st0, st1 if adjust off <> 0) if dest spilled *)
115  let move (dest : decision) (src : argument) l =
116    match dest, src with
117      | _, AImm k -> move_int dest k l
118      (* Both pseudo-registers are translated to hardware registers. Issue move
119         statements, or no statement at all if both pseudo-registers reside in
120         the same hardware register. *)
121      | Color desthwr, AColor sourcehwr
122        when I8051.eq_reg desthwr sourcehwr ->
123        LTL.St_skip l
124      | Color desthwr, AColor sourcehwr
125        when I8051.eq_reg desthwr I8051.a ->
126        LTL.St_to_acc (sourcehwr, l)
127      | Color desthwr, AColor sourcehwr
128        when I8051.eq_reg sourcehwr I8051.a ->
129        LTL.St_from_acc (desthwr, l)
130      | Color desthwr, AColor sourcehwr ->
131        let l = generate (LTL.St_from_acc (desthwr, l)) in
132        LTL.St_to_acc (sourcehwr, l)
133
134      (* One pseudo-register is translated to a hardware register, while the
135         other is spilled. Issue a single stack access instruction. *)
136      | Color desthwr, ASpill off -> get_stack desthwr off l
137      | Spill off, AColor sourcehwr -> set_stack off sourcehwr l
138
139      (* Both pseudo-registers are spilled. Combine the previous two cases. Of
140         course, if the two pseudo-registers have been spilled into the same
141         stack slot, there is nothing to do. *)
142      | Spill off1, ASpill off2 when off1 = off2 ->
143        LTL.St_skip l
144      | Spill off1, ASpill off2 ->
145        let l = generate (set_stack_a off1 l) in
146        get_stack I8051.a off2 l
147
148  (* side-effects (dpl, dph) if either spilled, (dpl, dph, b) if both *)
149  let op2 op (dest : decision) (src1 : argument) (src2 : argument) l =
150    let l = generate (move dest (AColor I8051.a) l) in
151    match op, src1, src2 with
152      | _, _, AImm k ->
153        let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in
154        move (Color I8051.a) src1 l
155        (* if op is commutative, we can do as above if first is hwr *)
156      | (Add | Addc | And | Or | Xor), AImm k, _ ->
157        let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in
158        move (Color I8051.a) src2 l
159      | _, _, AColor src2hwr ->
160        let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in
161        move (Color I8051.a) src1 l
162      | (Add | Addc | And | Or | Xor), AColor src1hwr, _ ->
163        let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in
164        move (Color I8051.a) src2 l
165      | _, _, _ ->
166        let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in
167        let l = generate (move (Color I8051.a) src1 l) in
168        move (Color I8051.b) src2 l
169
170  (* side-effects : a, b if both spilled *)
171  let move_to_dptr (addr1 : argument) (addr2 : argument) l =
172    match addr1, addr2 with
173      | ASpill _, ASpill _  ->
174        let l = generate (move (Color I8051.dph) (AColor I8051.b) l) in
175        let l = generate (move (Color I8051.dpl) addr1 l) in
176        move (Color I8051.b) addr2 l
177      | (AColor _ | AImm _) , _ ->
178        (* the following does not change dph, as addr1 is hwr *)
179        let l = generate (move (Color I8051.dpl) addr1 l) in
180        move (Color I8051.dph) addr2 l
181      | _, (AColor _ | AImm _) ->
182        (* the following does not change dpl, as addr2 is hwr *)
183        let l = generate (move (Color I8051.dph) addr2 l) in
184        move (Color I8051.dpl) addr1 l
185
186  (* side-effects :  dpl, dph, b if both addr spilled,
187                     st0 if srcr = a or srcr spilled, a if srcrs != a *)
188  let store (addr1 : argument) (addr2 : argument) (srcr : argument) l =
189    let l = generate (LTL.St_store l) in
190    match srcr with
191      | AColor r when I8051.eq_reg r a ->
192        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
193        let l = generate (move_to_dptr addr1 addr2 l) in
194        LTL.St_from_acc (I8051.st0, l)
195      | AColor r ->
196        let l = generate (LTL.St_to_acc (r, l)) in
197        move_to_dptr addr1 addr2 l
198      | AImm k ->
199        let l = generate (LTL.St_int (I8051.a, k, l)) in
200        move_to_dptr addr1 addr2 l
201      | ASpill _ ->
202        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
203        let l = generate (move_to_dptr addr1 addr2 l) in
204        move (Color I8051.st0) srcr l
205
206  let newframe l =
207    if stacksize = 0 then LTL.St_skip l
208    else
209      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
210      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm 0, l)) in
211      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
212      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
213      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm stacksize, l)) in
214      let l = generate (LTL.St_clear_carry l) in
215      LTL.St_to_acc (I8051.spl, l)
216
217  let delframe l =
218    if stacksize = 0 then LTL.St_skip l
219    else
220      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
221      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
222      let l = generate (LTL.St_int (I8051.a, 0, l)) in
223      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
224      let l = generate (LTL.St_op2 (I8051.Add, LTL.Imm stacksize, l)) in
225      LTL.St_to_acc (I8051.spl, l)
226
227
228  (* ------------------------------------------------------------------------ *)
229
230  (* [translate_statement] turns a [ERTL] statement into a [LTL] statement, or
231     sequence of statements, that transfers control to the same label(s).
232
233     Existing statement labels are preserved, that is, the labels in the new
234     control flow graph form a superset of the labels in the existing control
235     flow graph. *)
236
237  let translate_statement (stmt : ERTL.statement) : LTL.statement =
238    match stmt with
239
240      | ERTL.St_skip l ->
241        LTL.St_skip l
242
243      | ERTL.St_comment (s, l) ->
244        LTL.St_comment (s, l)
245
246      | ERTL.St_cost (cost_lbl, l) ->
247        LTL.St_cost (cost_lbl, l)
248
249      | ERTL.St_ind_0 (i, l) ->
250        LTL.St_ind_0 (i, l)
251
252      | ERTL.St_ind_inc (i, l) ->
253        LTL.St_ind_inc (i, l)
254
255      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
256        move (lookup destr) (AColor sourcehwr) l
257
258      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
259        move (Color desthwr) (lookup_arg sourcer) l
260
261      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
262        move (Color r1) (AColor r2) l
263
264      | ERTL.St_newframe l ->
265        newframe l
266
267      | ERTL.St_delframe l ->
268        delframe l
269
270      | ERTL.St_framesize (r, l) ->
271        move_int (lookup r) stacksize l
272
273      | ERTL.St_pop (r, l) ->
274        let l = generate (move (lookup r) (AColor I8051.a) l) in
275        LTL.St_pop l
276
277      | ERTL.St_push (r, l) ->
278        let l = generate (LTL.St_push l) in
279        move (Color I8051.a) (lookup_arg r) l
280
281      | ERTL.St_addrH (r, x, l) ->
282        let l = generate (move (lookup r) (AColor I8051.dph) l) in
283        LTL.St_addr (x, l)
284
285      | ERTL.St_addrL (r, x, l) ->
286        let l = generate (move (lookup r) (AColor I8051.dpl) l) in
287        LTL.St_addr (x, l)
288
289      | ERTL.St_move (r, a, l) ->
290        move (lookup r) (lookup_arg a) l
291
292      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
293        let l = generate (move (lookup destr) (AColor I8051.a) l) in
294        let l = generate (LTL.St_opaccs (opaccs, l)) in
295        let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in
296        move (Color I8051.b) (lookup_arg srcr2) l
297
298      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
299        let l = generate (move (lookup destr) (AColor I8051.b) l) in
300        let l = generate (LTL.St_opaccs (opaccs, l)) in
301        let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in
302        move (Color I8051.b) (lookup_arg srcr2) l
303
304      | ERTL.St_op1 (op1, destr, srcr, l) ->
305        let l = generate (move (lookup destr) (AColor I8051.a) l) in
306        let l = generate (LTL.St_op1 (op1, l)) in
307        move (Color I8051.a) (lookup_as_arg srcr) l
308
309      | ERTL.St_op2 (op, destr, arg1, arg2, l) ->
310        op2 op (lookup destr) (lookup_arg arg1) (lookup_arg arg2) l
311
312      | ERTL.St_clear_carry l ->
313        LTL.St_clear_carry l
314
315      | ERTL.St_set_carry l ->
316        LTL.St_set_carry l
317
318      | ERTL.St_load (destr, addr1, addr2, l) ->
319        let l = generate (move (lookup destr) (AColor I8051.a) l) in
320        let l = generate (LTL.St_load l) in
321        move_to_dptr (lookup_arg addr1) (lookup_arg addr2) l
322
323      | ERTL.St_store (addr1, addr2, srcr, l) ->
324        store (lookup_arg addr1) (lookup_arg addr2) (lookup_arg srcr) l
325
326      | ERTL.St_call_id (f, _, l) ->
327        LTL.St_call_id (f, l)
328
329      | ERTL.St_call_ptr (f1, f2, _, l) ->
330        let l = generate (LTL.St_call_ptr l) in
331        move_to_dptr (lookup_as_arg f1) (lookup_as_arg f2) l
332
333      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
334        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
335        move (Color I8051.a) (lookup_as_arg srcr) l
336
337      | ERTL.St_return _ ->
338        LTL.St_return
339
340(* ------------------------------------------------------------------------- *)
341
342end
Note: See TracBrowser for help on using the repository browser.