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

Last change on this file since 1542 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

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