Changeset 1144
 Timestamp:
 Aug 30, 2011, 3:53:21 PM (9 years ago)
 Location:
 src/ERTL
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1128 r1144 7 7 λf. 8 8 λint_fun: ertl_internal_function. 9 mk_ltl_internal_function ? 10 (ertl_if_luniverse int_fun) 11 (ertl_if_runiverse int_fun) 12 (ertl_if_stacksize int_fun) 13 (ertl_if_graph int_fun) 14 ? 15 ?. 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 pseudoregister 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 } 16 117 17 118 definition translate_funct ≝ 
src/ERTL/liveness.ma
r1124 r1144 49 49  ertl_st_push _ l ⇒ [ l ] 50 50  ertl_st_pop _ l ⇒ [ l ] 51  ertl_st_addr_h _ _ l ⇒ [ l ] 52  ertl_st_addr_l _ _ l ⇒ [ l ] 51  ertl_st_addr _ _ _ l ⇒ [ l ] 53 52  ertl_st_int _ _ l ⇒ [ l ] 54 53  ertl_st_move _ _ l ⇒ [ l ] 55  ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ] 56  ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ] 54  ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ] 57 55  ertl_st_op1 _ _ _ l ⇒ [ l ] 58 56  ertl_st_op2 _ _ _ _ l ⇒ [ l ] … … 148 146  ertl_st_pop r _ ⇒ lattice_psingleton r 149 147  ertl_st_int r _ _ ⇒ lattice_psingleton r 150  ertl_st_addr_h r _ _ ⇒ lattice_psingleton r 151  ertl_st_addr_l r _ _ ⇒ lattice_psingleton r 148  ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 152 149  ertl_st_move r _ _ ⇒ lattice_psingleton r 153  ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r154  ertl_st_opaccs _b _ r _ _ _ ⇒ lattice_psingleton r150 (* XXX: change from o'caml *) 151  ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 155 152  ertl_st_load r _ _ _ ⇒ lattice_psingleton r 156 153  ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r … … 180 177  ertl_st_frame_size _ _ ⇒ lattice_bottom 181 178  ertl_st_pop _ _ ⇒ lattice_bottom 182  ertl_st_addr_h _ _ _ ⇒ lattice_bottom 183  ertl_st_addr_l _ _ _ ⇒ lattice_bottom 179  ertl_st_addr _ _ _ _ ⇒ lattice_bottom 184 180  ertl_st_int _ _ _ ⇒ lattice_bottom 185 181  ertl_st_clear_carry _ ⇒ lattice_bottom … … 187 183 (* Reads the hardware registers that are used to pass parameters. *) 188 184  ertl_st_call_id _ nparams _ ⇒ 189 〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams)RegisterParameters)〉185 〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉 190 186  ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r 191 187  ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r … … 201 197  _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 202 198 ] 203  ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 204  ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 199  ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2) 205 200  ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 206 201  ertl_st_store r1 r2 r3 _ ⇒ … … 247 242 else 248 243 Some ? l 249  ertl_st_addr_h r _ l ⇒ 250 if list_set_member register (eq_identifier ?) r pliveafter ∨ 251 list_set_member Register eq_Register RegisterCarry hliveafter then 252 None ? 253 else 254 Some ? l 255  ertl_st_addr_l r _ l ⇒ 256 if list_set_member register (eq_identifier ?) r pliveafter ∨ 244  ertl_st_addr r1 r2 _ l ⇒ 245 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 246 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 257 247 list_set_member Register eq_Register RegisterCarry hliveafter then 258 248 None ? … … 265 255 else 266 256 Some ? l 267  ertl_st_opaccs_a _ r _ _ l ⇒ 268 if list_set_member register (eq_identifier ?) r pliveafter ∨ 269 list_set_member Register eq_Register RegisterCarry hliveafter then 270 None ? 271 else 272 Some ? l 273  ertl_st_opaccs_b _ r _ _ l ⇒ 274 if list_set_member register (eq_identifier ?) r pliveafter ∨ 257  ertl_st_opaccs _ d1 d2 _ _ l ⇒ 258 if list_set_member register (eq_identifier ?) d1 pliveafter ∨ 259 list_set_member register (eq_identifier ?) d2 pliveafter ∨ 275 260 list_set_member Register eq_Register RegisterCarry hliveafter then 276 261 None ?
Note: See TracChangeset
for help on using the changeset viewer.