Changeset 1241 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Sep 21, 2011, 5:28:06 PM (9 years ago)
Author:
mulligan
Message:

changes for claudio

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1232 r1241  
    33include "ERTL/spill.ma".
    44include "ERTL/build.ma".
     5include "ERTL/uses.ma".
    56include "ERTL/Interference.ma".
    67include "ASM/Arithmetic.ma".
     
    7879  λglobals.
    7980  λ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).
    8182
    8283definition stacksize ≝
    8384  λglobals.
    8485  λ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).
    8687
    8788definition adjust_off ≝
     
    103104  λl.
    104105    let off ≝ adjust_off globals int_fun off in
    105     let luniv ≝ joint_if_luniverse globals … int_fun in
     106    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    106107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
    107108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     
    123124  λl.
    124125  let off ≝ adjust_off globals int_fun off in
    125   let luniv ≝ joint_if_luniverse globals … int_fun in
     126  let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    126127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
    127128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
     
    147148      〈RegisterSST, l, graph, luniv〉
    148149  | decision_colour hwr ⇒
    149     let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in
     150    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    150151      〈hwr, l, graph, luniv〉
    151152  ].
     
    160161  λstmt.
    161162  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)
    163164  | decision_spill off ⇒
    164165    let temphwr ≝ RegisterSST in
    165     let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals … int_fun) graph (stmt temphwr) in
     166    let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse ertl_params globals int_fun) graph (stmt temphwr) in
    166167    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in
    167168      generate globals luniv graph stmt
     
    179180    match src with
    180181    [ decision_colour src_hwr ⇒
    181       let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in
     182      let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    182183      if eq_Register dest_hwr src_hwr then
    183184        〈joint_st_goto … globals l, graph, luniv〉
     
    191192    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l
    192193    | decision_spill src_off ⇒
    193       let luniv ≝ joint_if_luniverse globals … int_fun in
     194      let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    194195      if eq_nat dest_off src_off then
    195196        〈joint_st_goto … globals l, graph, luniv〉
     
    208209  λl: label.
    209210  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)〉
    211212  else
    212     let luniv ≝ joint_if_luniverse globals … int_fun in
     213    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    213214    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    214215    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     
    227228  λl.
    228229  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〉
    230231  else
    231     let luniv ≝ joint_if_luniverse globals … int_fun in
     232    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    232233    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    233234    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     
    246247  match stmt with
    247248  [ joint_st_sequential seq l ⇒
    248     let luniv ≝ joint_if_luniverse globals ertl_params (ertl_sem_params_ globals) int_fun in
     249    let luniv ≝ joint_if_luniverse ertl_params globals int_fun in
    249250    match seq with
    250251    [ joint_instr_comment c ⇒
     
    258259    | joint_instr_push r ⇒
    259260      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 in
     261      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    261262      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
    262263        〈joint_st_goto ltl_params globals l, graph, luniv〉
    263264    | joint_instr_cond srcr lbl_true ⇒
    264265      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 in
     266      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    266267      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
    267268        〈joint_st_goto ltl_params globals l, graph, luniv〉
     
    273274      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    274275      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 in
     276      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    276277      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
    277278      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 in
     279      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    279280      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
    280281      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
     
    288289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    289290      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 in
     291      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    291292      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
    292293      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 in
     294      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    294295      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
    295296        〈joint_st_goto ltl_params globals l, graph, luniv〉
     
    300301      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    301302      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 in
     303      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    303304      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
    304305      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 in
     306      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    306307      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
    307308        〈joint_st_goto ltl_params globals l, graph, luniv〉
     
    310311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    311312      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 in
     313      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    313314      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
    314315        〈joint_st_goto ltl_params globals l, graph, luniv〉
     
    320321      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    321322      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 in
     323      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    323324      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
    324325      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 in
     326      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    326327      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
    327328      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 in
     329      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    329330      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in
    330331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    331332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
    332333      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 in
     334      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    334335      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
    335336      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 in
     337      let luniv ≝ set_luniverse ertl_params globals int_fun luniv in
    337338      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
    338339        〈joint_st_goto ltl_params globals l, graph, luniv〉
     
    359360      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    360361      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 in
     362      let int_fun ≝ set_luniverse ertl_params globals int_fun luniv in
    362363      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in
    363364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
     
    365366        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
    366367    ]
    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〉
    369370  | joint_st_extension ext ⇒
    370371    match ext with
     
    380381  λglobals.
    381382  λint_fun.
    382     ?.
     383  let uses ≝ examine_internal globals int_fun in ?.
    383384
    384385definition translate_funct ≝
Note: See TracChangeset for help on using the changeset viewer.