src/ERTL/ERTLToLTLI.ml

   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
   9 type decision =
  10   | Spill of AST.immediate
  11   | Color of I8051.register
  12
  13 module 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
  30 end) = 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_opaccsA (opaccs, 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_opaccs (opaccs, l)) in
 220         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 221         let l = generate (LTL.St_from_acc (I8051.b, l)) in
 222         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 223         LTL.St_skip l
 224
 225       | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
 226         let (hdw, l) = write destr l in
 227         let l = generate (LTL.St_from_acc (hdw, l)) in
 228         let l = generate (LTL.St_to_acc (I8051.b, 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_set_carry l ->
 255         LTL.St_set_carry l
 256
 257       | ERTL.St_load (destr, addr1, addr2, l) ->
 258         let (hdw, l) = write destr l in
 259         let l = generate (LTL.St_from_acc (hdw, l)) in
 260         let l = generate (LTL.St_load l) in
 261         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
 262         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
 263         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
 264         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 265         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
 266         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 267         LTL.St_skip l
 268
 269       | ERTL.St_store (addr1, addr2, srcr, l) ->
 270         let l = generate (LTL.St_store l) in
 271         let l = generate (LTL.St_to_acc (I8051.st1, l)) in
 272         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
 273         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
 274         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
 275         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 276         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
 277         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 278         let l = generate (LTL.St_from_acc (I8051.st1, l)) in
 279         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
 280         LTL.St_skip l
 281
 282       | ERTL.St_call_id (f, _, l) ->
 283         LTL.St_call_id (f, l)
 284
 285       | ERTL.St_call_ptr (f1, f2, _, l) ->
 286         let l = generate (LTL.St_call_ptr l) in
 287         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
 288         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
 289         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
 290         let l = read f1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 291         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
 292         let l = read f2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
 293         LTL.St_skip l
 294
 295       | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
 296         let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
 297         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
 298         LTL.St_skip l
 299
 300       | ERTL.St_return _ ->
 301         LTL.St_return
 302
 303 (* ------------------------------------------------------------------------- *)
 304
 305 end