Changeset 1232


Ignore:
Timestamp:
Sep 21, 2011, 11:24:02 AM (8 years ago)
Author:
mulligan
Message:

big changes: got what was implemented in the ertl to ltl pass type checking again

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1230 r1232  
    77
    88(* XXX: define an interference graph for a function and colour it, allowing
    9         the consultation of registers. *)
     9        the consultation of registers.
    1010definition initial_colouring ≝
    1111  λglobals.
     
    4646  | decision_spill ⇒ ?
    4747  ].
     48*)
     49
     50definition lookup ≝ colouring.
    4851
    4952definition fresh_label ≝
     
    5154  λluniv.
    5255    fresh LabelTag luniv.
     56
     57definition ltl_statement_graph ≝
     58  λglobals.
     59    graph … (ltl_statement globals).
    5360
    5461definition add_graph ≝
     
    7178  λglobals.
    7279  λint_fun.
    73     colour_locals + (ertl_if_stacksize globals int_fun).
     80    colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals) int_fun).
    7481
    7582definition stacksize ≝
    7683  λglobals.
    7784  λint_fun.
    78     colour_locals + (ertl_if_stacksize globals int_fun).
     85    colour_locals + (joint_if_stacksize globals ertl_params (ertl_sem_params_ globals) int_fun).
    7986
    8087definition adjust_off ≝
     
    8895definition get_stack:
    8996 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
    90   ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
    91 
     97  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) ≝
    9298  λglobals: list ident.
    9399  λint_fun.
     
    97103  λl.
    98104    let off ≝ adjust_off globals int_fun off in
    99     let luniv ≝ ertl_if_luniverse globals int_fun in
     105    let luniv ≝ joint_if_luniverse globals … int_fun in
    100106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
    101107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     
    117123  λl.
    118124  let off ≝ adjust_off globals int_fun off in
    119   let luniv ≝ ertl_if_luniverse globals int_fun in
     125  let luniv ≝ joint_if_luniverse globals … int_fun in
    120126  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
    121127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
     
    127133    〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
    128134
    129 definition write:
    130   ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
    131     ? ≝
    132   λglobals: list ident.
    133   λint_fun.
     135definition write ≝
     136  λglobals: list ident.
     137  λint_fun.
     138  λvaluation.
     139  λcoloured_graph.
    134140  λgraph.
    135141  λr.
    136142  λl.
    137   match lookup r with
     143  match lookup valuation coloured_graph (inl … r) with
    138144  [ decision_spill off ⇒
    139     let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
     145    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in
    140146    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
    141147      〈RegisterSST, l, graph, luniv〉
    142148  | decision_colour hwr ⇒
    143     let luniv ≝ ertl_if_luniverse globals int_fun in
     149    let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in
    144150      〈hwr, l, graph, luniv〉
    145151  ].
    146152
    147 definition read:
    148   ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
    149     → (Register → ltl_statement globals) → ? ≝
    150   λglobals.
    151   λint_fun.
     153definition read ≝
     154  λglobals: list ident.
     155  λint_fun.
     156  λvaluation.
     157  λcoloured_graph.
    152158  λgraph.
    153159  λr.
    154160  λstmt.
    155   match lookup r with
    156   [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
     161  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)
    157163  | decision_spill off ⇒
    158164    let temphwr ≝ RegisterSST in
    159     let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
    160     let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
     165    let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals … int_fun) graph (stmt temphwr) in
     166    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in
    161167      generate globals luniv graph stmt
    162168  ].
     
    173179    match src with
    174180    [ decision_colour src_hwr ⇒
    175       let luniv ≝ ertl_if_luniverse globals int_fun in
     181      let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in
    176182      if eq_Register dest_hwr src_hwr then
    177183        〈joint_st_goto … globals l, graph, luniv〉
     
    179185        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    180186          〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
    181     | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
     187    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l
    182188    ]
    183189  | decision_spill dest_off ⇒
    184190    match src with
    185     [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
     191    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l
    186192    | decision_spill src_off ⇒
    187       let luniv ≝ ertl_if_luniverse globals int_fun in
    188       if eq_bv ? dest_off src_off then
     193      let luniv ≝ joint_if_luniverse globals … int_fun in
     194      if eq_nat dest_off src_off then
    189195        〈joint_st_goto … globals l, graph, luniv〉
    190196      else
    191197        let temp_hwr ≝ RegisterSST in
    192         let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
     198        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l in
    193199        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
    194           get_stack globals int_fun graph temp_hwr src_off l
     200          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l
    195201    ]
    196202  ].
     
    202208  λl: label.
    203209  if eq_nat (stacksize globals int_fun) 0 then
    204     〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
     210    〈joint_st_goto ltl_params globals l, graph, (joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun)〉
    205211  else
    206     let luniv ≝ ertl_if_luniverse globals int_fun in
     212    let luniv ≝ joint_if_luniverse globals … int_fun in
    207213    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    208214    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     
    221227  λl.
    222228  if eq_nat (stacksize globals int_fun) 0 then
    223     〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
     229    〈joint_st_goto ltl_params globals l, graph, joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun〉
    224230  else
    225     let luniv ≝ ertl_if_luniverse globals int_fun in
     231    let luniv ≝ joint_if_luniverse globals … int_fun in
    226232    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    227233    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     
    234240  λglobals: list ident.
    235241  λint_fun.
     242  λvaluation.
     243  λcoloured_graph: coloured_graph valuation.
    236244  λgraph: ltl_statement_graph globals.
    237245  λstmt: ertl_statement globals.
    238246  match stmt with
    239247  [ joint_st_sequential seq l ⇒
    240     let luniv ≝ ertl_if_luniverse globals int_fun in
     248    let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in
    241249    match seq with
    242250    [ joint_instr_comment c ⇒
     
    245253      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
    246254    | joint_instr_pop r ⇒
    247       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     255      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    248256      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    249257        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
    250258    | joint_instr_push r ⇒
    251259      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
    252       let int_fun ≝ set_luniverse globals int_fun luniv in
    253       let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     260      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     261      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
    254262        〈joint_st_goto ltl_params globals l, graph, luniv〉
    255263    | joint_instr_cond srcr lbl_true ⇒
    256264      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    257       let int_fun ≝ set_luniverse globals int_fun luniv in
    258       let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     265      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     266      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
    259267        〈joint_st_goto ltl_params globals l, graph, luniv〉
    260268    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
     
    265273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    266274      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    267       let int_fun ≝ set_luniverse globals int_fun luniv in
    268       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     275      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     276      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
    269277      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    270       let int_fun ≝ set_luniverse globals int_fun luniv in
    271       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     278      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     279      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
    272280      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    273       let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     281      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
    274282        〈joint_st_goto ltl_params globals l, graph, luniv〉
    275283    | joint_instr_load destr addr1 addr2 ⇒
    276       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     284      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    277285      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    278286      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     
    280288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    281289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    282       let int_fun ≝ set_luniverse globals int_fun luniv in
    283       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     290      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     291      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
    284292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    285       let int_fun ≝ set_luniverse globals int_fun luniv in
    286       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     293      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     294      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
    287295        〈joint_st_goto ltl_params globals l, graph, luniv〉
    288296    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
    289297    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
    290298    | joint_instr_op2 op2 destr srcr ⇒
    291       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     299      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    292300      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    293301      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
    294       let luniv ≝ set_luniverse globals int_fun luniv in
    295       let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     302      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     303      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
    296304      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    297       let luniv ≝ set_luniverse globals int_fun luniv in
    298       let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     305      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     306      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
    299307        〈joint_st_goto ltl_params globals l, graph, luniv〉
    300308    | joint_instr_op1 op1 acc_a ⇒
    301       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
     309      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in
    302310      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    303311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
    304       let int_fun ≝ set_luniverse globals int_fun luniv in
    305       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     312      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     313      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
    306314        〈joint_st_goto ltl_params globals l, graph, luniv〉
    307315    | joint_instr_int r i ⇒
    308       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     316      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    309317        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
    310318    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    311       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
     319      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
    312320      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    313321      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    314       let luniv ≝ set_luniverse globals int_fun luniv in
    315       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     322      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     323      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
    316324      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    317       let luniv ≝ set_luniverse globals int_fun luniv in
    318       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     325      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     326      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
    319327      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
    320       let luniv ≝ set_luniverse globals int_fun luniv in
    321       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
     328      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     329      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in
    322330      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    323331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
    324332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    325       let luniv ≝ set_luniverse globals int_fun luniv in
    326       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     333      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     334      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
    327335      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    328       let luniv ≝ set_luniverse globals int_fun luniv in
    329       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     336      let luniv ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     337      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
    330338        〈joint_st_goto ltl_params globals l, graph, luniv〉
    331339    | joint_instr_move pair_regs ⇒
     
    335343      [ pseudo p1  ⇒
    336344        match regr with
    337         [ pseudo p2  ⇒ move globals int_fun graph (lookup p1) (lookup p2) l
    338         | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l
     345        [ pseudo p2  ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (lookup valuation coloured_graph (inl … p2)) l
     346        | hardware h ⇒ move globals int_fun graph (lookup valuation coloured_graph (inl … p1)) (decision_colour h) l
    339347        ]
    340348      | hardware h1 ⇒
    341349        match regr with
    342         [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l
     350        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup valuation coloured_graph (inl … p)) l
    343351        | hardware h2 ⇒
    344352          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
     
    347355      ]
    348356    | joint_instr_address lbl prf dpl dph ⇒
    349       let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in
     357      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in
    350358      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
    351359      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    352360      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
    353       let int_fun ≝ set_luniverse globals int_fun luniv in
    354       let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in
     361      let int_fun ≝ set_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun luniv in
     362      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in
    355363      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
    356364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    357365        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
    358366    ]
    359   | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
    360   | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     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〉
    361369  | joint_st_extension ext ⇒
    362370    match ext with
     
    364372    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
    365373    | ertl_st_ext_frame_size r l ⇒
    366       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     374      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    367375        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
    368376    ]
     
    370378
    371379definition translate_internal ≝
    372   λglobals: list ident.
    373   λf.
    374   λint_fun: ertl_internal_function.
    375   let lookup ≝ λr.
    376     match lookup r with
    377     | colour_spill ->
    378         ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    379     | colour_colour color ->
    380         ERTLToLTLI.Color color
    381   in
    382   let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
    383   let stacksize ≝ (ertl_if_params int_fun) + locals in
    384     mk_ltl_internal_function
    385       globals
    386       (ertl_if_luniverse int_fun)
    387       (ertl_if_runiverse int_fun)
    388       stacksize.
    389 
    390   let () =
    391     Label.Map.iter (fun label stmt ->
    392       let stmt =
    393         match Liveness.eliminable (G.liveafter label) stmt with
    394         | Some successor ->
    395             LTL.St_skip successor
    396         | None ->
    397             I.translate_statement stmt
    398       in
    399       graph := Label.Map.add label stmt !graph
    400     ) int_fun.ERTL.f_graph
    401   in
     380  λglobals.
     381  λint_fun.
     382    ?.
    402383
    403384definition translate_funct ≝
  • src/ERTL/Interference.ma

    r1230 r1232  
    1515definition vertex ≝ register ⊎ Register.
    1616
    17 record graph: Type[0] ≝
     17inductive decision: Type[0] ≝
     18  | decision_spill: nat → decision
     19  | decision_colour: Register → decision.
     20
     21definition is_member ≝
     22  λvertex.
     23  λregister_lattice.
     24  let 〈l, r〉 ≝ register_lattice in
     25  match vertex with
     26  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
     27  | inr v ⇒ set_member ? eq_Register v r
     28  ].
     29
     30record coloured_graph (v: valuation): Type[1] ≝
    1831{
    19   interferes: vertex → vertex → bool
     32  colouring: vertex → decision;
     33  prop_colouring: ∀l. ∀v1, v2: vertex.
     34    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
    2035}.
    2136
    22 axiom build: ∀globals: list ident. ertl_internal_function globals → valuation × graph.
    23 
    24 inductive decision: Type[0] ≝
    25   | decision_spill: decision
    26   | decision_colour: Register → decision.
    27 
    28 record coloured_graph (d: Type[0]): Type[1] ≝
    29 {
    30   the_graph: graph;
    31   colouring: register → d;
    32   prop_colouring: ∀v1. ∀v2. (interferes the_graph (inl … v1) (inl … v2) = true) → colouring v1 ≠ colouring v2
    33 }.
    34 
    35 definition initial_colouring ≝ coloured_graph decision.
    36 axiom colour_initial: graph → initial_colouring.
    37 definition stack_colouring ≝ coloured_graph nat.
    38 axiom colour_stack: graph → stack_colouring.
    39 
     37axiom build: ∀valuation. coloured_graph valuation.
    4038
    4139(* definition vertex_set ≝ set vertex. *)
     
    517515    nmr = PrioritySet.remove x graph.nmr;
    518516  }
    519 *)
    520 
    521 *)
    522517
    523518axiom ig_mkppp: graph → register → register → graph.
     
    527522axiom ig_remove: graph → vertex → graph.
    528523axiom ig_freeze: graph → vertex → graph.
    529 axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *)
     524axiom ig_restrict: graph → (vertex → bool) → graph.
    530525axiom ig_droph: graph → graph.
    531526axiom ig_lookup: graph → register → vertex.
     
    545540definition ig_phedge ≝ vertex × Register.
    546541axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
     542*)
     543*)
Note: See TracChangeset for help on using the changeset viewer.