- Timestamp:
- Sep 21, 2011, 5:28:06 PM (10 years ago)
- Location:
- src/ERTL
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL.ma
r1223 r1241 13 13 | ertl_st_ext_frame_size: register → label → ertl_statement_extension. 14 14 15 definition ertl_params_: params_ ≝ 16 mk_params_ register register register register 17 (move_registers × move_registers) register 18 ertl_statement_extension unit (list register) nat. 19 15 20 definition ertl_params: params ≝ 16 mk_params 17 register register register register 18 (move_registers × move_registers) register 19 ertl_statement_extension unit (list register) nat. 21 mk_params ertl_params_ label. 20 22 21 23 definition ertl_statement ≝ joint_statement ertl_params. 22 24 25 (* 23 26 definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝ 24 27 λglobals. 25 28 mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …). 29 *) 26 30 27 31 definition ertl_internal_function ≝ 28 λglobals. joint_internal_function globals … (ertl_sem_params_ globals).32 joint_internal_function ertl_params. 29 33 30 definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).34 definition ertl_program ≝ joint_program ertl_params. -
src/ERTL/ERTLToLTL.ma
r1232 r1241 3 3 include "ERTL/spill.ma". 4 4 include "ERTL/build.ma". 5 include "ERTL/uses.ma". 5 6 include "ERTL/Interference.ma". 6 7 include "ASM/Arithmetic.ma". … … 78 79 λglobals. 79 80 λint_fun. 80 colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals)int_fun).81 colour_locals + (joint_if_stacksize ertl_params globals int_fun). 81 82 82 83 definition stacksize ≝ 83 84 λglobals. 84 85 λint_fun. 85 colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals)int_fun).86 colour_locals + (joint_if_stacksize ertl_params globals int_fun). 86 87 87 88 definition adjust_off ≝ … … 103 104 λl. 104 105 let off ≝ adjust_off globals int_fun off in 105 let luniv ≝ joint_if_luniverse globals …int_fun in106 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 106 107 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in 107 108 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in … … 123 124 λl. 124 125 let off ≝ adjust_off globals int_fun off in 125 let luniv ≝ joint_if_luniverse globals …int_fun in126 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 126 127 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in 127 128 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in … … 147 148 〈RegisterSST, l, graph, luniv〉 148 149 | decision_colour hwr ⇒ 149 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun in150 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 150 151 〈hwr, l, graph, luniv〉 151 152 ]. … … 160 161 λstmt. 161 162 match lookup valuation coloured_graph (inl … r) with 162 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun) graph (stmt hwr)163 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt hwr) 163 164 | decision_spill off ⇒ 164 165 let temphwr ≝ RegisterSST in 165 let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals …int_fun) graph (stmt temphwr) in166 let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt temphwr) in 166 167 let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in 167 168 generate globals luniv graph stmt … … 179 180 match src with 180 181 [ decision_colour src_hwr ⇒ 181 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun in182 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 182 183 if eq_Register dest_hwr src_hwr then 183 184 〈joint_st_goto … globals l, graph, luniv〉 … … 191 192 [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l 192 193 | decision_spill src_off ⇒ 193 let luniv ≝ joint_if_luniverse globals …int_fun in194 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 194 195 if eq_nat dest_off src_off then 195 196 〈joint_st_goto … globals l, graph, luniv〉 … … 208 209 λl: label. 209 210 if eq_nat (stacksize globals int_fun) 0 then 210 〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun)〉211 〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse ertl_params globals int_fun)〉 211 212 else 212 let luniv ≝ joint_if_luniverse globals …int_fun in213 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 213 214 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 214 215 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in … … 227 228 λl. 228 229 if eq_nat (stacksize globals int_fun) 0 then 229 〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun〉230 〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse ertl_params globals int_fun〉 230 231 else 231 let luniv ≝ joint_if_luniverse globals …int_fun in232 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 232 233 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in 233 234 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in … … 246 247 match stmt with 247 248 [ joint_st_sequential seq l ⇒ 248 let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun in249 let luniv ≝ joint_if_luniverse ertl_params globals int_fun in 249 250 match seq with 250 251 [ joint_instr_comment c ⇒ … … 258 259 | joint_instr_push r ⇒ 259 260 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in 260 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in261 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 261 262 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 262 263 〈joint_st_goto ltl_params globals l, graph, luniv〉 263 264 | joint_instr_cond srcr lbl_true ⇒ 264 265 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in 265 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in266 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 266 267 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 267 268 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 273 274 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 274 275 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 275 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in276 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 276 277 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 277 278 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 278 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in279 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 279 280 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 280 281 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in … … 288 289 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in 289 290 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in 290 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in291 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 291 292 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 292 293 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in 293 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in294 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 294 295 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 295 296 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 300 301 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 301 302 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in 302 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in303 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 303 304 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 304 305 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 305 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in306 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 306 307 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 307 308 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 310 311 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 311 312 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in 312 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in313 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 313 314 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 314 315 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 320 321 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 321 322 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 322 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in323 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 323 324 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 324 325 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 325 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in326 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 326 327 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 327 328 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in 328 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in329 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 329 330 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in 330 331 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in 331 332 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in 332 333 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in 333 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in334 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 334 335 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 335 336 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in 336 let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in337 let luniv ≝ set_luniverse ertl_params globals int_fun luniv in 337 338 let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in 338 339 〈joint_st_goto ltl_params globals l, graph, luniv〉 … … 359 360 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in 360 361 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in 361 let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals)int_fun luniv in362 let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in 362 363 let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in 363 364 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in … … 365 366 〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉 366 367 ] 367 | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals …int_fun〉368 | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals …int_fun〉368 | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse ertl_params globals int_fun〉 369 | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse ertl_params globals int_fun〉 369 370 | joint_st_extension ext ⇒ 370 371 match ext with … … 380 381 λglobals. 381 382 λint_fun. 382 383 let uses ≝ examine_internal globals int_fun in ?. 383 384 384 385 definition translate_funct ≝ -
src/ERTL/Interference.ma
r1232 r1241 1 include "basics/types.ma".2 include "basics/list.ma".3 include "common/Graphs.ma".4 include "common/Order.ma".5 include "common/Registers.ma".6 1 include "ERTL/ERTL.ma". 7 2 include "ERTL/liveness.ma". 8 9 include "utilities/adt/table_adt.ma".10 include "utilities/adt/priority_set_adt.ma".11 include "utilities/adt/set_adt.ma".12 include "utilities/adt/set_table_adt.ma".13 include "utilities/adt/register_table.ma".14 3 15 4 definition vertex ≝ register ⊎ Register. … … 37 26 axiom build: ∀valuation. coloured_graph valuation. 38 27 28 (* 39 29 (* definition vertex_set ≝ set vertex. *) 40 30 definition vertex_priority_set ≝ priority_set vertex. … … 43 33 definition Register_set_table ≝ set_table vertex (set Register). 44 34 definition Register_set ≝ set Register. 35 *) 45 36 46 37 (* -
src/ERTL/liveness.ma
r1223 r1241 283 283 λlabel. 284 284 λliveafter: valuation. 285 match lookup ? ? (joint_if_graph … int_fun)label with285 match joint_if_lookup … int_fun label with 286 286 [ None ⇒ ? 287 287 | Some stmt ⇒ statement_semantics globals stmt (liveafter label) … … 296 296 λlabel. 297 297 λliveafter: valuation. 298 match lookup … (joint_if_graph … int_fun)label with298 match joint_if_lookup … int_fun label with 299 299 [ None ⇒ ? 300 300 | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice. -
src/ERTL/uses.ma
r1188 r1241 1 1 include "ERTL/ERTL.ma". 2 2 3 let rec assoc_list_find 4 (A: Type[0]) (B: Type[0]) (eq_a: A → A → bool) (to_find: A) 5 (def: B) (l: list (A × B)) 6 on l ≝ 7 match l with 8 [ nil ⇒ def 9 | cons hd tl ⇒ 10 if eq_a (\fst hd) to_find then 11 \snd hd 12 else 13 assoc_list_find A B eq_a to_find def tl 3 include "utilities/adt/table_adt.ma". 4 5 definition lookup: table register nat → register → nat ≝ 6 λuses. 7 λr: register. 8 match tbl_find … r uses with 9 [ None ⇒ 0 10 | Some uses ⇒ uses 14 11 ]. 15 16 definition lookup ≝ 17 λuses. 18 λr. 19 assoc_list_find register nat (eq_identifier ?) uses 0 r. 12 13 definition count: register → table register nat → ? ≝ 14 λr: register. 15 λuses: table register nat. 16 tbl_insert … r ((lookup uses r) + 1) uses. 17 18 definition examine_statement ≝ 19 λglobals: list ident. 20 λstmt: ertl_statement globals. 21 λuses: table register nat. 22 match stmt with 23 [ joint_st_sequential seq l ⇒ 24 match seq with 25 [ joint_instr_comment c ⇒ uses 26 | joint_instr_cost_label c ⇒ uses 27 | joint_instr_move pair_regs ⇒ 28 let reg1 ≝ \fst pair_regs in 29 let reg2 ≝ \snd pair_regs in 30 match reg1 with 31 [ pseudo p ⇒ count p uses 32 | hardware h1 ⇒ 33 match reg2 with 34 [ pseudo p ⇒ count p uses 35 | hardware h2 ⇒ uses 36 ] 37 ] 38 | joint_instr_clear_carry ⇒ uses 39 | joint_instr_set_carry ⇒ uses 40 | joint_instr_call_id _ _ ⇒ uses 41 | joint_instr_pop r ⇒ count r uses 42 | joint_instr_push r ⇒ count r uses 43 | joint_instr_int r _ ⇒ count r uses 44 | joint_instr_address lbl prf r1 r2 ⇒ count r1 (count r2 uses) 45 | joint_instr_opaccs opaccs acc_a acc_b ⇒ count acc_a (count acc_b uses) 46 | joint_instr_op1 op1 r1 ⇒ count r1 uses 47 | joint_instr_op2 op2 r1 r2 ⇒ count r1 (count r2 uses) 48 | joint_instr_load destr r1 r2 ⇒ count r1 (count r2 (count destr uses)) 49 | joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses)) 50 | joint_instr_cond srcr l2 ⇒ count srcr uses 51 ] 52 | joint_st_return ⇒ uses 53 | joint_st_goto l ⇒ uses 54 | joint_st_extension ext ⇒ 55 match ext with 56 [ ertl_st_ext_new_frame l ⇒ uses 57 | ertl_st_ext_del_frame l ⇒ uses 58 | ertl_st_ext_frame_size r l ⇒ count r uses 59 ] 60 ]. 61 62 definition examine_internal ≝ 63 λglobals: list ident. 64 λint_fun: ertl_internal_function globals. 65 let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph … int_fun) (tbl_empty …) in 66 lookup uses.
Note: See TracChangeset
for help on using the changeset viewer.