source: Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.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: 11.7 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  let adjust off = locals - (off + I8051.int_size)
36
37  let get_stack r off l =
38    let off = adjust off in
39    let l = generate (LTL.St_from_acc (r, l)) in
40    let l = generate (LTL.St_load l) in
41    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
42    let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
43    let l = generate (LTL.St_int (I8051.a, 0, l)) in
44    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
45    let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
46    LTL.St_int (I8051.a, off, l)
47
48  let set_stack_preamble off l =
49    let off = adjust off in
50    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
51    let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
52    let l = generate (LTL.St_int (I8051.a, 0, l)) in
53    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
54    let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
55    LTL.St_int (I8051.a, off, l)
56
57  let set_stack off r l =
58    let l = generate (LTL.St_store l) in
59    let l = generate (LTL.St_to_acc (r, l)) in
60    set_stack_preamble off l
61
62  let set_stack_int off k l =
63    let l = generate (LTL.St_store l) in
64    let l = generate (LTL.St_int (I8051.a, k, l)) in
65    set_stack_preamble off l
66
67  (* let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) = *)
68  (*   match lookup r with *)
69
70  (*     | Color hwr -> *)
71  (*       (\* Pseudo-register [r] has been mapped to hardware register *)
72  (*          [hwr]. Just write into [hwr] and branch to [l]. *\) *)
73  (*       (hwr, l) *)
74
75  (*     | Spill off -> *)
76  (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
77  (*          of the stack. Then, write into [sst] (never allocated) and transfer *)
78  (*          control to an instruction that copies [sst] in the designated *)
79  (*          location of the stack before branching to [l]. *\) *)
80  (*       (I8051.sst, generate (set_stack off I8051.sst l)) *)
81
82
83  (* let read (r : Register.t) (stmt : I8051.register -> LTL.statement) = *)
84  (*   match lookup r with *)
85  (*     | Color hwr -> *)
86  (*       (\* Pseudo-register [r] has been mapped to hardware register [hwr]. Just *)
87  (*          generate statement [stmt] with a reference to register [hwr]. *\) *)
88  (*       generate (stmt hwr) *)
89
90  (*     | Spill off -> *)
91  (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
92  (*          of the stack. Issue a statement that copies the designated area in *)
93  (*          the stack into the temporary unallocatable hardware register [sst], *)
94  (*          then generate statement [stmt] with a reference to register *)
95  (*          [sst]. *\) *)
96  (*       let temphwr = I8051.sst in *)
97  (*       let l = generate (stmt temphwr) in *)
98  (*       generate (get_stack temphwr off l) *)
99
100
101  let move (dest : decision) (src : decision) l =
102    match dest, src with
103
104      (* Both pseudo-registers are translated to hardware registers. Issue move
105         statements, or no statement at all if both pseudo-registers reside in
106         the same hardware register. *)
107      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr ->
108        LTL.St_skip l
109      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr I8051.a ->
110        LTL.St_to_acc (sourcehwr, l)
111      | Color desthwr, Color sourcehwr when I8051.eq_reg sourcehwr I8051.a ->
112        LTL.St_from_acc (desthwr, l)
113      | Color desthwr, Color sourcehwr ->
114        let l = generate (LTL.St_from_acc (desthwr, l)) in
115        LTL.St_to_acc (sourcehwr, l)
116
117      (* One pseudo-register is translated to a hardware register, while the
118         other is spilled. Issue a single stack access instruction. *)
119      | Color desthwr, Spill off -> get_stack desthwr off l
120      | Spill off, Color sourcehwr -> set_stack off sourcehwr l
121
122      (* Both pseudo-registers are spilled. Combine the previous two cases. Of
123         course, if the two pseudo-registers have been spilled into the same
124         stack slot, there is nothing to do. *)
125      | Spill off1, Spill off2 when off1 = off2 ->
126        LTL.St_skip l
127      | Spill off1, Spill off2 ->
128        let temphwr = I8051.sst in
129        let l = generate (set_stack off1 temphwr l) in
130        get_stack temphwr off2 l
131
132  let move_int (dest : decision) (k : int) l =
133    match dest with
134      | Color desthwr -> LTL.St_int (desthwr, k, l)
135      | Spill off -> set_stack_int off k l
136
137  let op2 op (dest : decision) (src1 : decision) (src2 : decision) l =
138    let l = generate (move dest (Color I8051.a) l) in
139    match op, src1, src2 with
140      | _, _, Color src2hwr ->
141        let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in
142        move (Color I8051.a) src1 l
143        (* if op is commutative, we can do as above if first is hwr *)
144      | (Add | Addc | And | Or | Xor), Color src1hwr, _ ->
145        let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in
146        move (Color I8051.a) src2 l
147        (* otherwise we have to use b *)
148      | _ ->
149        let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in
150        let l = generate (move (Color I8051.a) src1 l) in
151        move (Color I8051.b) src2 l
152
153  let move_to_dptr (addr1 : decision) (addr2 : decision) l =
154    match addr1, addr2 with
155      | Color _, _ ->
156        (* the following does not change dph, as addr1 is hwr *)
157        let l = generate (move (Color I8051.dpl) addr1 l) in
158        move (Color I8051.dph) addr2 l
159      | _, Color _ ->
160        (* the following does not change dph, as addr1 is hwr *)
161        let l = generate (move (Color I8051.dph) addr2 l) in
162        move (Color I8051.dpl) addr1 l
163      | _ ->
164        let l = generate (move (Color I8051.dph) (Color I8051.b) l) in
165        let l = generate (move (Color I8051.dpl) addr1 l) in
166        move (Color I8051.b) addr2 l
167
168  let store addr1 addr2 srcr l =
169    let l = generate (LTL.St_store l) in
170    match srcr with
171      | Color _ ->
172        let l = generate (move (Color I8051.a) srcr l) in
173        move_to_dptr addr1 addr2 l
174      | _ ->
175        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
176        let l = generate (move_to_dptr addr1 addr2 l) in
177        move (Color I8051.st0) srcr l
178
179  let newframe l =
180    if stacksize = 0 then LTL.St_skip l
181    else
182      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
183      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm 0, l)) in
184      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
185      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
186      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm stacksize, l)) in
187      let l = generate (LTL.St_clear_carry l) in
188      LTL.St_to_acc (I8051.spl, l)
189
190  let delframe l =
191    if stacksize = 0 then LTL.St_skip l
192    else
193      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
194      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
195      let l = generate (LTL.St_int (I8051.a, 0, l)) in
196      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
197      let l = generate (LTL.St_op2 (I8051.Add, LTL.Imm stacksize, l)) in
198      LTL.St_to_acc (I8051.spl, l)
199
200
201  (* ------------------------------------------------------------------------ *)
202
203  (* [translate_statement] turns a [ERTL] statement into a [LTL] statement, or
204     sequence of statements, that transfers control to the same label(s).
205
206     Existing statement labels are preserved, that is, the labels in the new
207     control flow graph form a superset of the labels in the existing control
208     flow graph. *)
209
210  let translate_statement (stmt : ERTL.statement) : LTL.statement =
211    match stmt with
212
213      | ERTL.St_skip l ->
214        LTL.St_skip l
215
216      | ERTL.St_comment (s, l) ->
217        LTL.St_comment (s, l)
218
219      | ERTL.St_cost (cost_lbl, l) ->
220        LTL.St_cost (cost_lbl, l)
221
222      | ERTL.St_ind_0 (i, l) ->
223        LTL.St_ind_0 (i, l)
224
225      | ERTL.St_ind_inc (i, l) ->
226        LTL.St_ind_inc (i, l)
227
228      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
229        move (lookup destr) (Color sourcehwr) l
230
231      | ERTL.St_set_hdw (desthwr, RTL.Reg sourcer, l) ->
232        move (Color desthwr) (lookup sourcer) l
233
234      | ERTL.St_set_hdw (desthwr, RTL.Imm k, l) ->
235        move_int (Color desthwr) k l
236
237      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
238        move (Color r1) (Color r2) l
239
240      | ERTL.St_newframe l ->
241        newframe l
242
243      | ERTL.St_delframe l ->
244        delframe l
245
246      | ERTL.St_framesize (r, l) ->
247        move_int (lookup r) stacksize l
248
249      | ERTL.St_pop (r, l) ->
250        let l = generate (move (lookup r) (Color I8051.a) l) in
251        LTL.St_pop l
252
253      | ERTL.St_push (r, l) ->
254        let l = generate (LTL.St_push l) in
255        move (Color I8051.a) (lookup r) l
256
257      | ERTL.St_addrH (r, x, l) ->
258        let l = generate (move (lookup r) (Color I8051.dph) l) in
259        LTL.St_addr (x, l)
260
261      | ERTL.St_addrL (r, x, l) ->
262        let l = generate (move (lookup r) (Color I8051.dpl) l) in
263        LTL.St_addr (x, l)
264
265      | ERTL.St_move (r, RTL.Imm i, l) ->
266        move_int (lookup r) i l
267
268      | ERTL.St_move (r1, RTL.Reg r2, l) ->
269        move (lookup r1) (lookup r2) l
270
271      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
272        let l = generate (move (lookup destr) (Color I8051.a) l) in
273        let l = generate (LTL.St_opaccs (opaccs, l)) in
274        let l = generate (move (Color I8051.a) (lookup srcr1) l) in
275        move (Color I8051.b) (lookup srcr2) l
276
277      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
278        let l = generate (move (lookup destr) (Color I8051.b) l) in
279        let l = generate (LTL.St_opaccs (opaccs, l)) in
280        let l = generate (move (Color I8051.a) (lookup srcr1) l) in
281        move (Color I8051.b) (lookup srcr2) l
282
283      | ERTL.St_op1 (op1, destr, srcr, l) ->
284        let l = generate (move (lookup destr) (Color I8051.a) l) in
285        let l = generate (LTL.St_op1 (op1, l)) in
286        move (Color I8051.a) (lookup srcr) l
287
288      | ERTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, l) ->
289        op2 op (lookup destr) (lookup srcr1) (lookup srcr2) l
290
291      | ERTL.St_op2 (op2, destr, srcr1, RTL.Imm k, l) ->
292        let l = generate (move (lookup destr) (Color I8051.a) l) in
293        let l = generate (LTL.St_op2 (op2, LTL.Imm k, l)) in
294        move (Color I8051.a) (lookup srcr1) l
295
296      | ERTL.St_clear_carry l ->
297        LTL.St_clear_carry l
298
299      | ERTL.St_set_carry l ->
300        LTL.St_set_carry l
301
302      (* act differently on hardware registers? if at least one of
303         the address bytes is hdw use of st0 can be avoided. And in
304         case of non-hdw, the read could actually target a register
305         directly *)
306      | ERTL.St_load (destr, addr1, addr2, l) ->
307        let l = generate (move (lookup destr) (Color I8051.a) l) in
308        let l = generate (LTL.St_load l) in
309        move_to_dptr (lookup addr1) (lookup addr2) l
310
311      | ERTL.St_store (addr1, addr2, srcr, l) ->
312        store (lookup addr1) (lookup addr2) (lookup srcr) l
313
314      | ERTL.St_call_id (f, _, l) ->
315        LTL.St_call_id (f, l)
316
317      | ERTL.St_call_ptr (f1, f2, _, l) ->
318        let l = generate (LTL.St_call_ptr l) in
319        move_to_dptr (lookup f1) (lookup f2) l
320
321      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
322        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
323        move (Color I8051.a) (lookup srcr) l
324
325      | ERTL.St_return _ ->
326        LTL.St_return
327
328(* ------------------------------------------------------------------------- *)
329
330end
Note: See TracBrowser for help on using the repository browser.