Changeset 1152 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Aug 30, 2011, 5:43:39 PM (10 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ERTL/ERTLToLTL.ma

    r1144 r1152  
    55
    66definition translate_internal ≝
     7  λglobals: list ident.
    78  λf.
    89  λint_fun: ertl_internal_function.
    9 
    10   let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in
    11 
    12   let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in
    13 
    14   let generate stmt =
    15     let l = fresh_label () in
    16     add_graph l stmt ;
    17     l in
    18 
    19   (* Build an interference graph for this function, and color
    20      it. Define a function that allows consulting the coloring. *)
    21 
    22   let module G = struct
    23     let liveafter, graph = Build.build int_fun
    24     let uses = Uses.examine_internal int_fun
    25     let verbose = false
    26     let () =
    27       if verbose then
    28         Printf.printf "Starting hardware register allocation for %s.\n" f
    29   end in
    30 
    31   let module C = Coloring.Color (G) in
    32 
    33   let lookup r =
    34     Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
    35   in
    36 
    37   (* Restrict the interference graph to concern spilled vertices only,
    38      and color it again, this time using stack slots as colors. *)
    39 
    40   let module H = struct
    41     let graph = Interference.droph (Interference.restrict G.graph (fun v ->
    42       match Interference.Vertex.Map.find v C.coloring with
    43       | Coloring.Spill ->
    44           true
    45       | Coloring.Color _ ->
    46           false
    47     ))
    48     let verbose = false
    49     let () =
    50       if verbose then
    51         Printf.printf "Starting stack slot allocation for %s.\n" f
    52   end in
    53 
    54   let module S = Spill.Color (H) in
    55 
    56   (* Define a new function that consults both colorings at once. *)
    57 
    58   let lookup r =
     10  let lookup ≝ λr.
    5911    match lookup r with
    60     | Coloring.Spill ->
     12    | colour_spill ->
    6113        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    62     | Coloring.Color color ->
     14    | colour_colour color ->
    6315        ERTLToLTLI.Color color
    6416  in
    65 
    66   (* We are now ready to instantiate the functor that deals with the
    67      translation of instructions. The reason why we make this a
    68      separate functor is purely pedagogical. Smaller modules are
    69      easier to understand. *)
    70 
    71   (* We add the additional stack size required for spilled register to the stack
    72      size previously required for the function: this is the final stack size
    73      required for the locals. *)
    74 
    75   let locals = S.locals + int_fun.ERTL.f_stacksize in
    76 
    77   (* The full stack size is then the size of the locals in the stack plus the
    78      size of the formal parameters of the function. *)
    79 
    80   let stacksize = int_fun.ERTL.f_params + locals in
    81 
    82   let module I = ERTLToLTLI.Make (struct
    83     let lookup = lookup
    84     let generate = generate
    85     let fresh_label = fresh_label
    86     let add_graph = add_graph
    87     let locals = locals
    88     let stacksize = stacksize
    89   end) in
    90 
    91   (* Translate the instructions in the existing control flow graph.
    92      Pure instructions whose destination pseudo-register is dead are
    93      eliminated on the fly. *)
     17  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
     18  let stacksize ≝ (ertl_if_params int_fun) + locals in
     19    mk_ltl_internal_function
     20      globals
     21      (ertl_if_luniverse int_fun)
     22      (ertl_if_runiverse int_fun)
     23      stacksize.
    9424
    9525  let () =
    … …  
    10535    ) int_fun.ERTL.f_graph
    10636  in
    107 
    108   (* Build a [LTL] function. *)
    109 
    110   {
    111     LTL.f_luniverse = int_fun.ERTL.f_luniverse;
    112     LTL.f_stacksize = stacksize ;
    113     LTL.f_entry = int_fun.ERTL.f_entry;
    114     LTL.f_exit = int_fun.ERTL.f_exit;
    115     LTL.f_graph = !graph
    116   }
    11737
    11838definition translate_funct ≝
Note: See TracChangeset for help on using the changeset viewer.