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

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 9.9 KB
RevLine 
[486]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_get_hdw (destr, sourcehwr, l) ->
168        move (lookup destr) (Color sourcehwr) l
169
170      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
171        move (Color desthwr) (lookup sourcer) l
172
173      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
174        let l = generate (LTL.St_from_acc (r1, l)) in
175        LTL.St_to_acc (r2, l)
176
177      | ERTL.St_newframe l ->
178        newframe l
179
180      | ERTL.St_delframe l ->
181        delframe l
182
183      | ERTL.St_framesize (r, l) ->
184        let (hdw, l) = write r l in
185        LTL.St_int (hdw, stacksize, l)
186
187      | ERTL.St_pop (r, l) ->
188        let (hdw, l) = write r l in
189        let l = generate (LTL.St_from_acc (hdw, l)) in
190        LTL.St_pop l
191
192      | ERTL.St_push (r, l) ->
193        let l = generate (LTL.St_push l) in
194        let l = read r (fun hdw -> LTL.St_to_acc (hdw, l)) in
195        LTL.St_skip l
196
197      | ERTL.St_addrH (r, x, l) ->
198        let (hdw, l) = write r l in
199        let l = generate (LTL.St_from_acc (hdw, l)) in
200        let l = generate (LTL.St_to_acc (I8051.dph, l)) in
201        LTL.St_addr (x, l)
202
203      | ERTL.St_addrL (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.dpl, l)) in
207        LTL.St_addr (x, l)
208
209      | ERTL.St_int (r, i, l) ->
210        let (hdw, l) = write r l in
211        LTL.St_int (hdw, i, l)
212
213      | ERTL.St_move (r1, r2, l) ->
214        move (lookup r1) (lookup r2) l
215
216      | ERTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, l) ->
217        let (hdw, l) = write destr l in
218        let l = generate (LTL.St_from_acc (hdw, l)) in
219        let l = generate (LTL.St_to_acc (I8051.b, l)) in
220        let l = generate (LTL.St_opaccs (I8051.Divu, l)) in
221        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
222        let l = generate (LTL.St_from_acc (I8051.b, l)) in
223        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
224        LTL.St_skip l
225
226      | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, l) ->
227        let (hdw, l) = write destr l in
228        let l = generate (LTL.St_from_acc (hdw, l)) in
229        let l = generate (LTL.St_opaccs (opaccs, l)) in
230        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
231        let l = generate (LTL.St_from_acc (I8051.b, l)) in
232        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
233        LTL.St_skip l
234
235      | ERTL.St_op1 (op1, destr, srcr, l) ->
236        let (hdw, l) = write destr l in
237        let l = generate (LTL.St_from_acc (hdw, l)) in
238        let l = generate (LTL.St_op1 (op1, l)) in
239        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
240        LTL.St_skip l
241
242      | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
243        let (hdw, l) = write destr l in
244        let l = generate (LTL.St_from_acc (hdw, l)) in
245        let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
246        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
247        let l = generate (LTL.St_from_acc (I8051.b, l)) in
248        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
249        LTL.St_skip l
250
251      | ERTL.St_clear_carry l ->
252        LTL.St_clear_carry l
253
254      | ERTL.St_load (destr, addr1, addr2, l) ->
255        let (hdw, l) = write destr l in
256        let l = generate (LTL.St_from_acc (hdw, l)) in
257        let l = generate (LTL.St_load l) in
258        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
259        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
260        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
261        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
262        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
263        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
264        LTL.St_skip l
265
266      | ERTL.St_store (addr1, addr2, srcr, l) ->
267        let l = generate (LTL.St_store l) in
268        let l = generate (LTL.St_to_acc (I8051.st1, l)) in
269        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
270        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
271        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
272        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
273        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
274        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
275        let l = generate (LTL.St_from_acc (I8051.st1, l)) in
276        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
277        LTL.St_skip l
278
279      | ERTL.St_call_id (f, _, l) ->
280        LTL.St_call_id (f, l)
281
282      | ERTL.St_condacc (srcr, lbl_true, lbl_false) ->
283        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
284        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
285        LTL.St_skip l
286
287      | ERTL.St_return _ ->
288        LTL.St_return
289
290(* ------------------------------------------------------------------------- *)
291
292end
Note: See TracBrowser for help on using the repository browser.