Changeset 1152 for src/ERTL/ERTLToLTL.ma
- Timestamp:
- Aug 30, 2011, 5:43:39 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTL.ma
r1144 r1152 5 5 6 6 definition translate_internal ≝ 7 λglobals: list ident. 7 8 λf. 8 9 λ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 = 10 let lookup ≝ λr. 59 11 match lookup r with 60 | Coloring.Spill ->12 | colour_spill -> 61 13 ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring) 62 | Coloring.Color color ->14 | colour_colour color -> 63 15 ERTLToLTLI.Color color 64 16 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. *) 17 let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in 18 let stacksize ≝ (ertl_if_params int_fun) + locals in 19 mk_ltl_internal_function 20 globals 21 (ertl_if_luniverse int_fun) 22 (ertl_if_runiverse int_fun) 23 stacksize. 94 24 95 25 let () = … … 105 35 ) int_fun.ERTL.f_graph 106 36 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 = !graph116 }117 37 118 38 definition translate_funct ≝
Note: See TracChangeset
for help on using the changeset viewer.