1 | include "ERTL/ERTL.ma". |
---|
2 | include "ERTL/ERTLToLTLI.ma". |
---|
3 | include "LTL/LTL.ma". |
---|
4 | include "ERTL/spill.ma". |
---|
5 | |
---|
6 | definition 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 | |
---|
118 | definition 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 | |
---|
129 | definition 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). |
---|