Changeset 1144 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Aug 30, 2011, 3:53:21 PM (9 years ago)
Author:
mulligan
Message:

added build.ma file. matita bug found

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1128 r1144  
    77  λf.
    88  λint_fun: ertl_internal_function.
    9     mk_ltl_internal_function ?
    10       (ertl_if_luniverse int_fun)
    11       (ertl_if_runiverse int_fun)
    12       (ertl_if_stacksize int_fun)
    13       (ertl_if_graph int_fun)
    14       ?
    15       ?.
     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 =
     59    match lookup r with
     60    | Coloring.Spill ->
     61        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
     62    | Coloring.Color color ->
     63        ERTLToLTLI.Color color
     64  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. *)
     94
     95  let () =
     96    Label.Map.iter (fun label stmt ->
     97      let stmt =
     98        match Liveness.eliminable (G.liveafter label) stmt with
     99        | Some successor ->
     100            LTL.St_skip successor
     101        | None ->
     102            I.translate_statement stmt
     103      in
     104      graph := Label.Map.add label stmt !graph
     105    ) int_fun.ERTL.f_graph
     106  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  }
    16117
    17118definition translate_funct ≝
Note: See TracChangeset for help on using the changeset viewer.