source: Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma @ 1153

Last change on this file since 1153 was 1153, checked in by campbell, 8 years ago

Merge trunk into branch.

File size: 3.7 KB
Line 
1include "ERTL/ERTL.ma".
2include "ERTL/ERTLToLTLI.ma".
3include "LTL/LTL.ma".
4include "ERTL/spill.ma".
5
6definition translate_internal ≝
7  λf.
8  λ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 =
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  }
117
118definition translate_funct ≝
119  λname_def.
120  let 〈name, def〉 ≝ name_def in
121  let def' ≝
122    match def with
123    [ Internal def ⇒ Internal ? (translate_internal name def)
124    | External def ⇒ External ? def
125    ]
126  in
127    〈name, def'〉.
128
129definition translate ≝
130  λp.
131  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
132    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.