Changeset 1153 for Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma
- Timestamp:
- Aug 30, 2011, 6:55:12 PM (9 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1110-1132,1136-1150
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma
r1091 r1153 2 2 include "ERTL/ERTLToLTLI.ma". 3 3 include "LTL/LTL.ma". 4 include "ERTL/spill.ma". 4 5 5 6 definition translate_internal ≝ 6 7 λf. 7 8 λint_fun: ertl_internal_function. 8 mk_ltl_internal_function ? 9 (ertl_if_luniverse int_fun) 10 (ertl_if_runiverse int_fun) 11 (ertl_if_stacksize int_fun) 12 (ertl_if_graph int_fun) 13 ? 14 ?. 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 } 15 117 16 118 definition translate_funct ≝
Note: See TracChangeset
for help on using the changeset viewer.