src/ERTL/ERTLToLTL.ml

   1
   2 (* This module provides a translation of ERTL programs to LTL
   3    programs. *)
   4
   5 (* Adapted from Pottier's PP compiler *)
   6
   7 let translate_internal f (int_fun : ERTL.internal_function)
   8     : LTL.internal_function =
   9
  10   (* Allocate a reference that will hold the control flow
  11      graph. Define a function that generates a statement at a fresh
  12      label. *)
  13
  14   let graph = ref Label.Map.empty in
  15
  16   let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in
  17
  18   let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in
  19
  20   let generate stmt =
  21     let l = fresh_label () in
  22     add_graph l stmt ;
  23     l in
  24
  25   (* Build an interference graph for this function, and color
  26      it. Define a function that allows consulting the coloring. *)
  27
  28   let module G = struct
  29     let liveafter, graph = Build.build int_fun
  30     let uses = Uses.examine_internal int_fun
  31     let verbose = false
  32     let () =
  33       if verbose then
  34         Printf.printf "Starting hardware register allocation for %s.\n" f
  35   end in
  36
  37   let module C = Coloring.Color (G) in
  38
  39   let lookup r =
  40     Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
  41   in
  42
  43   (* Restrict the interference graph to concern spilled vertices only,
  44      and color it again, this time using stack slots as colors. *)
  45
  46   let module H = struct
  47     let graph = Interference.droph (Interference.restrict G.graph (fun v ->
  48       match Interference.Vertex.Map.find v C.coloring with
  49       | Coloring.Spill ->
  50           true
  51       | Coloring.Color _ ->
  52           false
  53     ))
  54     let verbose = false
  55     let () =
  56       if verbose then
  57         Printf.printf "Starting stack slot allocation for %s.\n" f
  58   end in
  59
  60   let module S = Spill.Color (H) in
  61
  62   (* Define a new function that consults both colorings at once. *)
  63
  64   let lookup r =
  65     match lookup r with
  66     | Coloring.Spill ->
  67         ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
  68     | Coloring.Color color ->
  69         ERTLToLTLI.Color color
  70   in
  71
  72   (* We are now ready to instantiate the functor that deals with the
  73      translation of instructions. The reason why we make this a
  74      separate functor is purely pedagogical. Smaller modules are
  75      easier to understand. *)
  76
  77   (* We add the additional stack size required for spilled register to the stack
  78      size previously required for the function: this is the final stack size
  79      required for the locals. *)
  80
  81   let locals = S.locals + int_fun.ERTL.f_stacksize in
  82
  83   (* The full stack size is then the size of the locals in the stack plus the
  84      size of the formal parameters of the function. *)
  85
  86   let stacksize = int_fun.ERTL.f_params + locals in
  87
  88   let module I = ERTLToLTLI.Make (struct
  89     let lookup = lookup
  90     let generate = generate
  91     let fresh_label = fresh_label
  92     let add_graph = add_graph
  93     let locals = locals
  94     let stacksize = stacksize
  95   end) in
  96
  97   (* Translate the instructions in the existing control flow graph.
  98      Pure instructions whose destination pseudo-register is dead are
  99      eliminated on the fly. *)
 100
 101   let () =
 102     Label.Map.iter (fun label stmt ->
 103       let stmt =
 104         match Liveness.eliminable (G.liveafter label) stmt with
 105         | Some successor ->
 106             LTL.St_skip successor
 107         | None ->
 108             I.translate_statement stmt
 109       in
 110       graph := Label.Map.add label stmt !graph
 111     ) int_fun.ERTL.f_graph
 112   in
 113
 114   AnnotStackSize.add_stack_size f stacksize;
 115   (* Build a [LTL] function. *)
 116
 117   {
 118     LTL.f_luniverse = int_fun.ERTL.f_luniverse;
 119     LTL.f_stacksize = stacksize ;
 120     LTL.f_entry = int_fun.ERTL.f_entry;
 121     LTL.f_exit = int_fun.ERTL.f_exit;
 122     LTL.f_graph = !graph
 123   }
 124
 125
 126 let translate_funct (name, def) =
 127   let def' = match def with
 128     | ERTL.F_int def -> LTL.F_int (translate_internal name def)
 129     | ERTL.F_ext def -> LTL.F_ext def in
 130   (name, def')
 131
 132 let translate (p : ERTL.program) : LTL.program =
 133   { LTL.vars = p.ERTL.vars;
 134     LTL.functs = List.map translate_funct p.ERTL.functs ;
 135     LTL.main = p.ERTL.main }