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

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