Changeset 1260


Ignore:
Timestamp:
Sep 23, 2011, 3:04:20 PM (8 years ago)
Author:
mulligan
Message:

commit for csc

Location:
src
Files:
1 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1256 r1260  
    9292
    9393definition get_stack:
    94  ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
    95   ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag) ≝
     94 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
    9695  λglobals: list ident.
    9796  λint_fun.
     
    10099  λoff.
    101100  λl.
     101  λoriginal_label.
    102102    let off ≝ adjust_off globals int_fun off in
    103103    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     
    105105    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    106106    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    107     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     107    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    108108    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    109109    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    110     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    111       〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉.
     110    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
     111      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    112112
    113113definition set_stack:
    114114  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    115     → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag))
     115    → Register → label → ?
    116116  λglobals: list ident.
    117117  λint_fun.
     
    120120  λr.
    121121  λl.
     122  λoriginal_label.
    122123  let off ≝ adjust_off globals int_fun off in
    123124  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     
    125126  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    126127  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    127   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     128  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    128129  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    129130  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    130   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    131     〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l, graph, luniv〉.
     131  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
     132    〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
     133
    132134
    133135definition write ≝
    134136  λglobals: list ident.
    135   λint_fun.
     137  λint_fun: ertl_internal_function globals.
    136138  λvaluation.
    137139  λcoloured_graph.
     
    139141  λr.
    140142  λl.
     143  λoriginal_label: label.
    141144  match colouring valuation coloured_graph (inl … r) with
    142145  [ decision_spill off ⇒
    143     let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in
    144     let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
     146    let luniv ≝ joint_if_luniverse … int_fun in
     147    let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
    145148      〈RegisterSST, l, graph, luniv〉
    146149  | decision_colour hwr ⇒
     
    151154definition read ≝
    152155  λglobals: list ident.
    153   λint_fun.
     156  λint_fun: ertl_internal_function globals.
    154157  λvaluation.
    155158  λcoloured_graph.
     
    157160  λr.
    158161  λstmt.
     162  λoriginal_label: label.
    159163  match colouring valuation coloured_graph (inl … r) with
    160   [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt hwr)
     164  [ decision_colour hwr ⇒
     165    let luniv ≝ joint_if_luniverse … int_fun in
     166      〈add_graph globals original_label (stmt hwr) graph, luniv〉
    161167  | decision_spill off ⇒
    162168    let temphwr ≝ RegisterSST in
    163     let 〈l, graph, luniv〉 ≝ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt temphwr) in
    164     let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l in
    165       generate globals luniv graph stmt
     169    let luniv ≝ joint_if_luniverse … int_fun in
     170    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
     171      get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
    166172  ].
    167173
     
    173179  λsrc: decision.
    174180  λl: label.
     181  λoriginal_label.
    175182  match dest with
    176183  [ decision_colour dest_hwr ⇒
     
    179186      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    180187      if eq_Register dest_hwr src_hwr then
    181         〈joint_st_goto … globals l, graph, luniv〉
     188        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    182189      else
    183190        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    184           〈joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l, graph, luniv〉
    185     | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l
     191          〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉
     192    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    186193    ]
    187194  | decision_spill dest_off ⇒
    188195    match src with
    189     [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l
     196    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
    190197    | decision_spill src_off ⇒
    191198      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    192199      if eq_nat dest_off src_off then
    193         〈joint_st_goto … globals l, graph, luniv〉
     200        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    194201      else
    195202        let temp_hwr ≝ RegisterSST in
    196         let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l in
    197         let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
    198           get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l
     203        let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
     204          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
    199205    ]
    200206  ].
     
    205211  λgraph: ltl_statement_graph globals.
    206212  λl: label.
     213  λoriginal_label: label.
    207214  if eq_nat (stacksize globals int_fun) 0 then
    208     〈joint_st_goto … globals l, graph, (joint_if_luniverse globals (ertl_params globals) int_fun)〉
     215    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     216      〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    209217  else
    210218    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    211219    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    212     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     220    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
    213221    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    214222    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    215223    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    216     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     224    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
    217225    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
    218226    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
    219       〈joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l, graph, luniv〉.
     227      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
    220228
    221229definition delframe ≝
     
    224232  λgraph: graph (ltl_statement globals).
    225233  λl.
     234  λoriginal_label: label.
    226235  if eq_nat (stacksize globals int_fun) 0 then
    227     〈joint_st_goto (ltl_params globals) globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     236    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     237      〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    228238  else
    229239    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    230240    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    231     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     241    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    232242    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    233243    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    234     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    235       〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     244    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
     245      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
    236246
    237247definition translate_statement ≝
     
    242252  λgraph: ltl_statement_graph globals.
    243253  λstmt: ertl_statement globals.
     254  λoriginal_label: label.
    244255  match stmt with
    245256  [ joint_st_sequential seq l ⇒
     
    247258    match seq with
    248259    [ joint_instr_comment c ⇒
    249       〈joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l, graph, luniv〉
     260      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l) graph, luniv〉
    250261    | joint_instr_cost_label cost_lbl ⇒
    251       〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     262      〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l) graph, luniv〉
    252263    | joint_instr_pop r ⇒
    253264      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    254265      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    255         〈joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l, graph, luniv〉
     266        〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l) graph, luniv〉
    256267    | joint_instr_push r ⇒
    257268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
    258269      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    259       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
    260         〈joint_st_goto … globals l, graph, luniv〉
     270      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     271      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
     272      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l frees) in
     273        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     274    | _ ⇒ ?
     275    ]
     276  | _ ⇒ ?
     277  ].
    261278    | joint_instr_cond srcr lbl_true ⇒
    262279      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    263280      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    264281      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
    265         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    266     | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
     282        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     283    | joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l) graph, luniv〉
    267284    | joint_instr_store addr1 addr2 srcr ⇒
    268285      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
     
    278295      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    279296      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
    280         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
     297        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    281298    | joint_instr_load destr addr1 addr2 ⇒
    282299      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
     
    291308      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    292309      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
    293         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    294     | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
    295     | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
    296     | joint_instr_op2 op2 destr srcr
     310        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     311    | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) graph, luniv〉
     312    | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_set_carry … globals) l) graph, luniv〉
     313    | joint_instr_op2 op2 destr srcr1 srcr2
    297314      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    298315      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    299       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
    300       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    301       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
     316      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it it RegisterB) l) in
     317      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     318      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    302319      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    303320      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     321      let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     322        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     323    | joint_instr_op1 op1 destr srcr  ⇒
     324      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
     325      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     326      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it it) l) in
     327      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    304328      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
    305         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
    306     | joint_instr_op1 op1 acc_a ⇒
    307       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a l in
    308       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    309       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
    310       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    311       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
    312         〈joint_st_goto (ltl_params globals) globals l, graph, luniv〉
     329        〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    313330    | joint_instr_int r i ⇒
    314331      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    315         〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     332        〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l) graph, luniv〉
    316333    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    317334      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
     
    334351      let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    335352      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
    336         〈joint_st_goto … globals l, graph, luniv〉
     353        〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    337354    | joint_instr_move pair_regs ⇒
    338355      let regl ≝ \fst pair_regs in
     
    341358      [ pseudo p1  ⇒
    342359        match regr with
    343         [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l
    344         | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l
     360        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
     361        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
    345362        ]
    346363      | hardware h1 ⇒
    347364        match regr with
    348         [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l
     365        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    349366        | hardware h2 ⇒
    350367          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
    351             〈joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l, graph, luniv〉
     368            〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l) graph, luniv〉
    352369        ]
    353370      ]
     371      | _ ⇒ ?
     372    ]
     373  | _ ⇒ ?
     374  ].
     375   
    354376    | joint_instr_address lbl prf dpl dph ⇒
    355377      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in
     
    364386    | joint_instr_extension ext ⇒
    365387      match ext with
    366       [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
    367       | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
    368       | ertl_st_ext_frame_size r l
     388      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l
     389      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l
     390      | ertl_st_ext_frame_size r
    369391        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    370392          〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     
    375397  ].
    376398
    377 axiom Sm_leq_n_m_leq_n:
     399lemma Sm_leq_n_m_leq_n:
    378400  ∀m, n: nat.
    379401    S m ≤ n → m ≤ n.
     402  #m #n /2/
     403qed.
    380404
    381405let rec mapi_aux
    382406  (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
    383407    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n ≝
    384   match n return λn. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
     408  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
    385409  [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
    386     match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
     410    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
    387411    [ Leaf l ⇒ λprf. Leaf … (f accu l)
    388412    | Stub s ⇒ λprf. Stub … s
     
    390414    ] (refl … 0)
    391415  | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
    392     match trie return λx. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
     416    match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
    393417    [ Leaf l ⇒ λabsrd. ⊥
    394418    | Stub s ⇒ λprf. Stub … s
    395419    | Node n'' l r ⇒ λprf.
    396420      Node ? n'' ? ?
    397 (*      (mapi_aux a b f n' ? (l⌈n'' ↦ n'⌉) ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
    398                  (mapi_aux a b f n' ? (r⌈n'' ↦ n'⌉) ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))*)
    399     ] (refl ? (S n'))
     421    ] (refl nat (S n'))
    400422  ].
    401423  [ 1,2: destruct(absrd)
     
    420442  ]
    421443qed.
     444
     445definition mapi ≝
     446  λa, b: Type[0].
     447  λf: label → a → b.
     448  λtrie: BitVectorTrie a 16.
     449    let f' ≝ λbv: BitVector 16. λa.
     450      f (an_identifier LabelTag bv) a
     451    in
     452      mapi_aux a b f' 16 ? trie [[]].
     453  //
     454qed.
    422455 
    423 check mapi_aux.
    424 
    425456definition translate_internal ≝
    426457  λglobals.
    427458  λint_fun.
    428   let uses ≝ examine_internal globals int_fun in
    429   let
     459  let graph ≝ ((empty_map …) : ltl_statement_graph globals) in
     460  let valuation ≝ analyse globals int_fun in
     461  let coloured_graph ≝ build valuation in
     462  let liveafter ≝ analyse globals int_fun in
     463  let blah ≝ mapi … (λlabel. λstmt_graph_luniv.
     464    let stmt ≝
     465      match eliminable globals (liveafter label) stmt with
     466      [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉
     467      | None           ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt
     468      ]
     469    in
     470      ?) (joint_if_code … int_fun)
     471  in ?.
     472 
     473 
     474 
     475      let stmt =
     476        match Liveness.eliminable (G.liveafter label) stmt with
     477        | Some successor ->
     478            LTL.St_skip successor
     479        | None ->
     480            I.translate_statement stmt
     481      in
     482      graph := Label.Map.add label stmt !graph
     483    ) int_fun.ERTL.f_graph
    430484
    431485definition translate_funct ≝
  • src/ERTL/liveness.ma

    r1250 r1260  
    8080  [ joint_st_sequential seq l ⇒
    8181    match seq with
    82     [ joint_instr_op2 op2 r _ ⇒
     82    [ joint_instr_op2 op2 r1 r2 _ ⇒
    8383      match op2 with
    84       [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    85       | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    86       | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    87       | _ ⇒ lattice_psingleton r
     84      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     85      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     86      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry)  (lattice_psingleton r1)
     87      | _ ⇒ lattice_psingleton r1
    8888      ]
    8989    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    9090    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    9191    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    92     | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     92    | joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    9393    | joint_instr_pop r ⇒ lattice_psingleton r
    9494    | joint_instr_int r _ ⇒ lattice_psingleton r
     
    111111    | joint_instr_extension ext ⇒
    112112      match ext with
    113       [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    114       | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    115       | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r]]
     113      [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     114      | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     115      | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
    116116  | joint_st_return ⇒ lattice_bottom
    117117  | joint_st_goto l ⇒ lattice_bottom
     
    126126  [ joint_st_sequential seq l ⇒
    127127    match seq with
    128     [ joint_instr_op2 op2 acc_a r
     128    [ joint_instr_op2 op2 acc_a r1 r2
    129129      match op2 with
    130130      [ Addc ⇒
    131         lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
    132       | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
     131        lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
     132      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    133133      ]
    134134    | joint_instr_clear_carry ⇒ lattice_bottom
     
    136136    (* acc_a and acc_b *)
    137137    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    138     | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     138    | joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2
    139139    | joint_instr_pop r ⇒ lattice_bottom
    140140    | joint_instr_int r _ ⇒ lattice_bottom
     
    158158  | joint_instr_extension ext ⇒
    159159    match ext with
    160     [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    161     | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    162     | ertl_st_ext_frame_size r l ⇒ lattice_bottom]]
     160    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     161    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     162    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
    163163  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    164164  | joint_st_goto l ⇒ lattice_bottom
     
    173173  [ joint_st_sequential seq l ⇒
    174174    match seq with
    175     [ joint_instr_op2 op2 acc_a r
    176       if set_member … (eq_identifier …) acc_a pliveafter ∨
     175    [ joint_instr_op2 op2 r1 r2 r3
     176      if set_member … (eq_identifier …) r1 pliveafter ∨
    177177         set_member … eq_Register RegisterCarry hliveafter then
    178178        None ?
     
    188188      else
    189189        Some ? l
    190     | joint_instr_op1 op1 r
    191       if set_member … (eq_identifier …) r pliveafter ∨
     190    | joint_instr_op1 op1 r1 r2
     191      if set_member … (eq_identifier …) r1 pliveafter ∨
    192192         set_member … eq_Register RegisterCarry hliveafter then
    193193        None ?
     
    237237    | joint_instr_extension ext ⇒
    238238      match ext with
    239       [ ertl_st_ext_new_frame l ⇒ None ?
    240       | ertl_st_ext_del_frame l ⇒ None ?
    241       | ertl_st_ext_frame_size r l
     239      [ ertl_st_ext_new_frame ⇒ None ?
     240      | ertl_st_ext_del_frame ⇒ None ?
     241      | ertl_st_ext_frame_size r
    242242        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
    243243           set_member ? eq_Register RegisterCarry hliveafter then
  • src/ERTL/uses.ma

    r1253 r1260  
    4141    | joint_instr_address lbl prf r1 r2 ⇒ count r1 (count r2 uses)
    4242    | joint_instr_opaccs opaccs acc_a acc_b ⇒ count acc_a (count acc_b uses)
    43     | joint_instr_op1 op1 r1 ⇒ count r1 uses
    44     | joint_instr_op2 op2 r1 r2 ⇒ count r1 (count r2 uses)
     43    | joint_instr_op1 op1 r1 r2 ⇒ count r1 (count r2 uses)
     44    | joint_instr_op2 op2 r1 r2 r3 ⇒ count r1 (count r2 (count r3 uses))
    4545    | joint_instr_load destr r1 r2 ⇒ count r1 (count r2 (count destr uses))
    4646    | joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses))
     
    4848    | joint_instr_extension ext ⇒
    4949      match ext with
    50       [ ertl_st_ext_new_frame l ⇒ uses
    51       | ertl_st_ext_del_frame l ⇒ uses
    52       | ertl_st_ext_frame_size r l ⇒ count r uses]]
     50      [ ertl_st_ext_new_frame ⇒ uses
     51      | ertl_st_ext_del_frame ⇒ uses
     52      | ertl_st_ext_frame_size r ⇒ count r uses]]
    5353  | joint_st_return ⇒ uses
    5454  | joint_st_goto l ⇒ uses
  • src/joint/Joint.ma

    r1255 r1260  
    33include "common/AST.ma".
    44include "common/Registers.ma".
    5 include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
     5include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
    66include "common/Graphs.ma".
    77
  • src/utilities/extralib.ma

    r1250 r1260  
    721721| #m #H @(False_ind … H)
    722722] qed.
    723 
    724 (* Stuff about Sigma types *)
    725 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    726  λA,P,c. match c with [ dp w _ ⇒ w ].
    727 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
Note: See TracChangeset for help on using the changeset viewer.