 Timestamp:
 Sep 28, 2011, 11:08:37 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1275 r1281 3 3 include "ERTL/spill.ma". 4 4 include "ASM/Arithmetic.ma". 5 6 (* XXX: define an interference graph for a function and colour it, allowing7 the consultation of registers.8 definition initial_colouring ≝9 λglobals.10 λint_fun.11 let 〈ignore, graph〉 ≝ build globals int_fun in12 let coloured ≝ colour_initial graph in13 coloured.14 15 definition interference_lookup ≝16 λcoloured: initial_colouring.17 λr.18 colouring … coloured r.19 20 definition prepare_graph_for_second_colouring ≝21 λglobals: list ident.22 λcoloured: initial_colouring.23 let g ≝ the_graph decision coloured in24 let restricted ≝ ig_restrict g (λv.25 match colouring decision coloured v with26 [ decision_spill ⇒ true27  decision_colour _ ⇒ false28 ]29 )30 in restricted.31 32 definition second_colouring ≝33 λglobals: list ident.34 λcoloured.35 let prepared ≝ prepare_graph_for_second_colouring globals coloured in36 colour_stack prepared.37 38 definition lookup ≝39 λinitial.40 λsecond.41 λr.42 match interference_lookup initial r with43 [ decision_colour _ ⇒ ?44  decision_spill ⇒ ?45 ].46 *)47 5 48 6 definition fresh_label ≝ … … 397 355  joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒ 398 356 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 399 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 400 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l fresh_lbl in 357 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in 401 358 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in 402 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in 403 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 404 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 405 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 406 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in 407 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in 408 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 409 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 410 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 411 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in 412 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … fresh_lbl) in 413 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 414 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 415 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 416 let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l fresh_lbl in 417 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in 418 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterB)) l) in 419 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in 420 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 421 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 422 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 423 let 〈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) fresh_lbl in 359 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it it it) l) in 360 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 361 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 362 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 363 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in 424 364 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in 425 365 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 426 366 let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in 427 367 let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in 428 let 〈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) fresh_lbl in368 let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in 429 369 〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉 430 370 ] … … 522 462 523 463 definition ertl_to_ltl: ertl_program → ltl_program ≝ 524 λp. 525 transform_program … p (transf_fundef … (translate_internal …)). 464 λp.transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracChangeset
for help on using the changeset viewer.