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

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 3.8 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            LTL.St_skip successor
107        | None ->
108            I.translate_statement stmt
109      in
110      graph := Label.Map.add label stmt !graph
111    ) int_fun.ERTL.f_graph
112  in
113
114  (* Build a [LTL] function. *)
115
116  {
117    LTL.f_luniverse = int_fun.ERTL.f_luniverse;
118    LTL.f_stacksize = stacksize ;
119    LTL.f_entry = int_fun.ERTL.f_entry;
120    LTL.f_exit = int_fun.ERTL.f_exit;
121    LTL.f_graph = !graph
122  }
123
124
125let translate_funct (name, def) =
126  let def' = match def with
127    | ERTL.F_int def -> LTL.F_int (translate_internal name def)
128    | ERTL.F_ext def -> LTL.F_ext def in
129  (name, def')
130
131let translate (p : ERTL.program) : LTL.program =
132  { LTL.vars = p.ERTL.vars;
133    LTL.functs = List.map translate_funct p.ERTL.functs ;
134    LTL.main = p.ERTL.main }
Note: See TracBrowser for help on using the repository browser.