Changeset 1281 for src/ERTL


Ignore:
Timestamp:
Sep 28, 2011, 11:08:37 PM (9 years ago)
Author:
sacerdot
Message:

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1275 r1281  
    33include "ERTL/spill.ma".
    44include "ASM/Arithmetic.ma".
    5 
    6 (* XXX: define an interference graph for a function and colour it, allowing
    7         the consultation of registers.
    8 definition initial_colouring ≝
    9   λglobals.
    10   λint_fun.
    11   let 〈ignore, graph〉 ≝ build globals int_fun in
    12   let coloured ≝ colour_initial graph in
    13     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 in
    24     let restricted ≝ ig_restrict g (λv.
    25       match colouring decision coloured v with
    26       [ decision_spill ⇒ true
    27       | decision_colour _ ⇒ false
    28       ]
    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 in
    36       colour_stack prepared.
    37 
    38 definition lookup ≝
    39   λinitial.
    40   λsecond.
    41   λr.
    42   match interference_lookup initial r with
    43   [ decision_colour _ ⇒ ?
    44   | decision_spill ⇒ ?
    45   ].
    46 *)
    475
    486definition fresh_label ≝
     
    397355    | joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    398356      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
    401358      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
    424364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
    425365      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    426366      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    427367      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 in
     368      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
    429369        〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
    430370    ]
     
    522462
    523463definition 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.