source: Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml @ 1585

Last change on this file since 1585 was 1585, checked in by tranquil, 8 years ago

fighting with a bug of the translation from RTL to ERTL

File size: 3.9 KB
Line 
1
2(* This module provides a translation of ERTL programs to LTL
3   programs. *)
4
5(* Adapted from Pottier's PP compiler *)
6
7let 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          Printf.printf "dead %s!\n%!" (ERTLPrinter.print_statement stmt);
107          LTL.St_skip successor
108        | None ->
109            I.translate_statement stmt
110      in
111      graph := Label.Map.add label stmt !graph
112    ) int_fun.ERTL.f_graph
113  in
114
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
126let 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
132let 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 }
Note: See TracBrowser for help on using the repository browser.