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

(* Pasted from Pottier's PP compiler *)

(* This module translates [ERTL] statements into [LTL] statements. It is
   parameterized over a module [Env], whose signature appears below, which
   provides support for mapping pseudo-registers to stack slots or hardware
   registers and for generating instructions (which requires allocating fresh
   control flow graph labels). *)

type decision =
  | Spill of AST.immediate
  | Color of I8051.register

module Make (Env : sig

  val lookup: Register.t -> decision

  (* [generate stmt] returns a fresh statement label, which it associates with
     [stmt] in the control flow graph. *)

  val generate: LTL.statement -> Label.t

  val fresh_label: unit -> Label.t

  val add_graph: Label.t -> LTL.statement -> unit

  val locals: int

  val stacksize: int

end) = struct

  open Env
  open I8051

  let adjust off = locals - (off + I8051.int_size)

  let get_stack r off l =
    let off = adjust off in
    let l = generate (LTL.St_from_acc (r, l)) in
    let l = generate (LTL.St_load l) in
    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
    let l = generate (LTL.St_int (I8051.a, 0, l)) in
    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
    LTL.St_int (I8051.a, off, l)

  let set_stack off r l =
    let off = adjust off in
    let l = generate (LTL.St_store l) in
    let l = generate (LTL.St_to_acc (r, l)) in
    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
    let l = generate (LTL.St_int (I8051.a, 0, l)) in
    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
    LTL.St_int (I8051.a, off, l)


  let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) =
    match lookup r with

      | Color hwr ->
        (* Pseudo-register [r] has been mapped to hardware register
           [hwr]. Just write into [hwr] and branch to [l]. *)
        (hwr, l)

      | Spill off ->
        (* Pseudo-register [r] has been mapped to offset [off] in the local zone
           of the stack. Then, write into [sst] (never allocated) and transfer
           control to an instruction that copies [sst] in the designated
           location of the stack before branching to [l]. *)
        (I8051.sst, generate (set_stack off I8051.sst l))


  let read (r : Register.t) (stmt : I8051.register -> LTL.statement) =
    match lookup r with
      | Color hwr ->
        (* Pseudo-register [r] has been mapped to hardware register [hwr]. Just
           generate statement [stmt] with a reference to register [hwr]. *)
        generate (stmt hwr)

      | Spill off ->
        (* Pseudo-register [r] has been mapped to offset [off] in the local zone
           of the stack. Issue a statement that copies the designated area in
           the stack into the temporary unallocatable hardware register [sst],
           then generate statement [stmt] with a reference to register
           [sst]. *)
        let temphwr = I8051.sst in
        let l = generate (stmt temphwr) in
        generate (get_stack temphwr off l)


  let move (dest : decision) (src : decision) l =
    match dest, src with

      (* Both pseudo-registers are translated to hardware registers. Issue move
         statements, or no statement at all if both pseudo-registers reside in
         the same hardware register. *)
      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr ->
        LTL.St_skip l
      | Color desthwr, Color sourcehwr ->
        let l = generate (LTL.St_from_acc (desthwr, l)) in
        LTL.St_to_acc (sourcehwr, l)

      (* One pseudo-register is translated to a hardware register, while the
         other is spilled. Issue a single stack access instruction. *)
      | Color desthwr, Spill off -> get_stack desthwr off l
      | Spill off, Color sourcehwr -> set_stack off sourcehwr l

      (* Both pseudo-registers are spilled. Combine the previous two cases. Of
         course, if the two pseudo-registers have been spilled into the same
         stack slot, there is nothing to do. *)
      | Spill off1, Spill off2 when off1 = off2 ->
        LTL.St_skip l
      | Spill off1, Spill off2 ->
        let temphwr = I8051.sst in
        let l = generate (set_stack off1 temphwr l) in
        get_stack temphwr off2 l


  let newframe l =
    if stacksize = 0 then LTL.St_skip l
    else
      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
      let l = generate (LTL.St_op2 (I8051.Sub, I8051.dph, l)) in
      let l = generate (LTL.St_int (I8051.dph, 0, l)) in
      let l = generate (LTL.St_to_acc (I8051.sph, l)) in
      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
      let l = generate (LTL.St_op2 (I8051.Sub, I8051.dpl, l)) in
      let l = generate (LTL.St_clear_carry l) in
      let l = generate (LTL.St_int (I8051.dpl, stacksize, l)) in
      LTL.St_to_acc (I8051.spl, l)

  let delframe l =
    if stacksize = 0 then LTL.St_skip l
    else
      let l = generate (LTL.St_from_acc (I8051.sph, l)) in
      let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
      let l = generate (LTL.St_int (I8051.a, 0, l)) in
      let l = generate (LTL.St_from_acc (I8051.spl, l)) in
      let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
      LTL.St_int (I8051.a, stacksize, l)


  (* ------------------------------------------------------------------------ *)

  (* [translate_statement] turns a [ERTL] statement into a [LTL] statement, or
     sequence of statements, that transfers control to the same label(s).

     Existing statement labels are preserved, that is, the labels in the new
     control flow graph form a superset of the labels in the existing control
     flow graph. *)

  let translate_statement (stmt : ERTL.statement) : LTL.statement =
    match stmt with

      | ERTL.St_skip l ->
        LTL.St_skip l

      | ERTL.St_comment (s, l) ->
        LTL.St_comment (s, l)

      | ERTL.St_cost (cost_lbl, l) ->
        LTL.St_cost (cost_lbl, l)

      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
        move (lookup destr) (Color sourcehwr) l

      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
        move (Color desthwr) (lookup sourcer) l

      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
        let l = generate (LTL.St_from_acc (r1, l)) in
        LTL.St_to_acc (r2, l)

      | ERTL.St_newframe l ->
        newframe l

      | ERTL.St_delframe l ->
        delframe l

      | ERTL.St_framesize (r, l) ->
        let (hdw, l) = write r l in
        LTL.St_int (hdw, stacksize, l)

      | ERTL.St_pop (r, l) ->
        let (hdw, l) = write r l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        LTL.St_pop l

      | ERTL.St_push (r, l) ->
        let l = generate (LTL.St_push l) in
        let l = read r (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_addrH (r, x, l) ->
        let (hdw, l) = write r l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_to_acc (I8051.dph, l)) in
        LTL.St_addr (x, l)

      | ERTL.St_addrL (r, x, l) ->
        let (hdw, l) = write r l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
        LTL.St_addr (x, l)

      | ERTL.St_int (r, i, l) ->
        let (hdw, l) = write r l in
        LTL.St_int (hdw, i, l)

      | ERTL.St_move (r1, r2, l) ->
        move (lookup r1) (lookup r2) l

      | ERTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, l) ->
        let (hdw, l) = write destr l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_to_acc (I8051.b, l)) in
        let l = generate (LTL.St_opaccs (I8051.Divu, l)) in
        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        let l = generate (LTL.St_from_acc (I8051.b, l)) in
        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, l) ->
        let (hdw, l) = write destr l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_opaccs (opaccs, l)) in
        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        let l = generate (LTL.St_from_acc (I8051.b, l)) in
        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_op1 (op1, destr, srcr, l) ->
        let (hdw, l) = write destr l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_op1 (op1, l)) in
        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
        let (hdw, l) = write destr l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        let l = generate (LTL.St_from_acc (I8051.b, l)) in
        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_clear_carry l ->
        LTL.St_clear_carry l

      | ERTL.St_load (destr, addr1, addr2, l) ->
        let (hdw, l) = write destr l in
        let l = generate (LTL.St_from_acc (hdw, l)) in
        let l = generate (LTL.St_load l) in
        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_store (addr1, addr2, srcr, l) ->
        let l = generate (LTL.St_store l) in
        let l = generate (LTL.St_to_acc (I8051.st1, l)) in
        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
        let l = generate (LTL.St_from_acc (I8051.st1, l)) in
        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_call_id (f, _, l) ->
        LTL.St_call_id (f, l)

      | ERTL.St_condacc (srcr, lbl_true, lbl_false) ->
        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
        LTL.St_skip l

      | ERTL.St_return _ ->
        LTL.St_return

(* ------------------------------------------------------------------------- *)

end