Changeset 1282 for src/ERTL


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

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

Location:
src/ERTL
Files:
1 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1281 r1282  
    5858    let off ≝ adjust_off globals int_fun off in
    5959    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    60     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
    61     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    62     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    63     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    64     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    65     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    66     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
    67       〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
     60    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc r)) l) in
     61    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (LOAD … globals it it it) l) in
     62    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
     63    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
     64    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
     65    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
     66    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
     67      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    6868
    6969definition set_stack:
     
    7979  let off ≝ adjust_off globals int_fun off in
    8080  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    81   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
    82   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    83   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    84   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    85   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    86   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    87   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
    88     〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
     81  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (STORE … globals it it it) l) in
     82  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc r)) l) in
     83  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPH)) l) in
     84  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
     85  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
     86  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterDPL)) l) in
     87  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
     88    〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … (ltl_params globals) globals RegisterA off) l) graph, luniv〉.
    8989
    9090
     
    142142      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    143143      if eq_Register dest_hwr src_hwr then
    144         〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     144        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    145145      else
    146         let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    147           〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc src_hwr)) l) graph, luniv〉
     146        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc dest_hwr)) l) in
     147          〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc src_hwr)) l) graph, luniv〉
    148148    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    149149    ]
     
    154154      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    155155      if eq_nat dest_off src_off then
    156         〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     156        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    157157      else
    158158        let temp_hwr ≝ RegisterSST in
     
    170170  if eq_nat (stacksize globals int_fun) 0 then
    171171    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    172       〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     172      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    173173  else
    174174    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    175     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    176     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPH) l) in
    177     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    178     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    179     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    180     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it it RegisterDPL) l) in
    181     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
    182     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
    183       〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move … globals (to_acc RegisterSPL)) l) graph, luniv〉.
     175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
     176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPH) l) in
     177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPH (zero ?)) l) in
     178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterSPH)) l) in
     179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
     180    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Sub it it RegisterDPL) l) in
     181    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (CLEAR_CARRY … globals) l) in
     182    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     183      〈add_graph globals original_label (sequential (ltl_params globals) globals (MOVE … globals (to_acc RegisterSPL)) l) graph, luniv〉.
    184184
    185185definition delframe ≝
     
    191191  if eq_nat (stacksize globals int_fun) 0 then
    192192    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    193       〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     193      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
    194194  else
    195195    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    196     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    197     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it it RegisterSPH) l) in
    198     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    199     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    200     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it it RegisterSPL) l) in
    201       〈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〉.
     196    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPH)) l) in
     197    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Addc it it RegisterSPH) l) in
     198    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (INT … globals RegisterA (zero ?)) l) in
     199    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterSPL)) l) in
     200    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (OP2 … globals Add it it RegisterSPL) l) in
     201      〈add_graph globals original_label (sequential (ltl_params globals) globals (INT … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
    202202
    203203definition translate_statement:
     
    213213  λoriginal_label: label.
    214214  match stmt with
    215   [ joint_st_sequential seq l ⇒
     215  [ sequential seq l ⇒
    216216    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    217217    match seq with
    218     [ joint_instr_comment c ⇒
    219       〈add_graph globals original_label (joint_st_sequential … (joint_instr_comment … c) l) graph, luniv〉
    220     | joint_instr_cost_label cost_lbl ⇒
    221       〈add_graph globals original_label (joint_st_sequential … (joint_instr_cost_label … cost_lbl) l) graph, luniv〉
    222     | joint_instr_pop r ⇒
     218    [ COMMENT c ⇒
     219      〈add_graph globals original_label (sequential … (COMMENT … c) l) graph, luniv〉
     220    | COST_LABEL cost_lbl ⇒
     221      〈add_graph globals original_label (sequential … (COST_LABEL … cost_lbl) l) graph, luniv〉
     222    | POP r ⇒
    223223      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    224224      let int_fun ≝ set_luniverse globals ? int_fun luniv in
    225225      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    226       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    227         〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_pop … it) l) graph, luniv〉
    228     | joint_instr_push r ⇒
    229       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_push … it) l) in
    230       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    231       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    232       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    233       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    234         〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    235     | joint_instr_cond srcr lbl_true ⇒
    236       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_cond … it lbl_true) l) in
     226      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     227        〈add_graph globals original_label (sequential ltl_params_ globals (POP … it) l) graph, luniv〉
     228    | PUSH r ⇒
     229      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (PUSH … globals it) l) in
     230      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     231      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     232      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     233      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     234        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
     235    | COND srcr lbl_true ⇒
     236      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (COND … it lbl_true) l) in
    237237      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    238238      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    239239      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
    240       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    241         〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    242     | joint_instr_call_id f ignore ignore' ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore ignore') l) graph, luniv〉
    243     | joint_instr_store addr1 addr2 srcr ⇒
    244       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
    245       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST1)) l) in
    246       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
    247       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
    248       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
    249       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    250       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    251       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    252       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    253       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
    254       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    255       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    256       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    257       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    258       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST1)) fresh_lbl) in
    259       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    260       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    261       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    262         〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    263     | joint_instr_load destr addr1 addr2 ⇒
     240      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     241        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
     242    | CALL_ID f ignore ignore' ⇒ 〈add_graph globals original_label (sequential … (CALL_ID … f ignore ignore') l) graph, luniv〉
     243    | STORE addr1 addr2 srcr ⇒
     244      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (STORE … it it it) l) in
     245      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST1)) l) in
     246      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
     247      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
     248      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
     249      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     250      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     251      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     252      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     253      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
     254      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     255      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     256      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     257      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     258      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST1)) fresh_lbl) in
     259      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     260      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     261      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     262        〈add_graph globals original_label (GOTO … l) graph, luniv〉
     263    | LOAD destr addr1 addr2 ⇒
    264264      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    265265      let int_fun ≝ set_luniverse globals ? int_fun luniv in
    266266      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    267       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    268       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_load … it it it) l) in
    269       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
    270       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
    271       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
    272       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    273       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    274       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    275       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    276       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
    277       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    278       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    279       let int_fun ≝ set_luniverse globals ? int_fun luniv in
    280       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    281         〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    282     | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_clear_carry …) l) graph, luniv〉
    283     | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_set_carry …) l) graph, luniv〉
    284     | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
     267      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (LOAD … it it it) l) in
     269      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPH)) l) in
     270      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (to_acc RegisterST0)) l) in
     271      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterDPL)) l) in
     272      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     273      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     274      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     275      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     276      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterST0)) fresh_lbl) in
     277      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     278      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     279      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     280      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     281        〈add_graph globals original_label (GOTO … fresh_lbl) graph, luniv〉
     282    | CLEAR_CARRY ⇒ 〈add_graph globals original_label (sequential … (CLEAR_CARRY …) l) graph, luniv〉
     283    | SET_CARRY ⇒ 〈add_graph globals original_label (sequential … (SET_CARRY …) l) graph, luniv〉
     284    | OP2 op2 destr srcr1 srcr2 ⇒
    285285      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    286286      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    287287      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    288       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    289       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op2 … op2 it it RegisterB) l) in
    290       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    291       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    292       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    293       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
    294       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    295       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    296       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    297         〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    298     | joint_instr_op1 op1 destr srcr ⇒
     288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP2 … op2 it it RegisterB) l) in
     290      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     291      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     292      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc RegisterB)) fresh_lbl) in
     294      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     295      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     296      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     297        〈add_graph globals original_label (GOTO … l) graph, luniv〉
     298    | OP1 op1 destr srcr ⇒
    299299      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    300300      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    301301      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
    302       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    303       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op1 … op1 it it) l) in
    304       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    305       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    306       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    307       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    308         〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    309     | joint_instr_int r i ⇒
     302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     303      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (OP1 … op1 it it) l) in
     304      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     305      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     306      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     307      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. sequential … (MOVE … (to_acc hdw)) l) fresh_lbl in
     308        〈add_graph globals original_label (GOTO … l) graph, luniv〉
     309    | INT r i ⇒
    310310      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    311311      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    312312      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    313         〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw i) l) graph, luniv〉
    314     | joint_instr_move pair_regs ⇒
     313        〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
     314    | MOVE pair_regs ⇒
    315315      let regl ≝ \fst pair_regs in
    316316      let regr ≝ \snd pair_regs in
     
    325325        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    326326        | hardware h2 ⇒
    327           let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc h1)) l) in
    328             〈add_graph globals original_label (joint_st_sequential ltl_params_ … (joint_instr_move … (to_acc h2)) l) graph, luniv〉
     327          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc h1)) l) in
     328            〈add_graph globals original_label (sequential ltl_params_ … (MOVE … (to_acc h2)) l) graph, luniv〉
    329329        ]
    330330      ]
    331     | joint_instr_address lbl prf dpl dph ⇒
     331    | ADDRESS lbl prf dpl dph ⇒
    332332      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    333333      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    334334      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
    335       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
    336       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    337       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
     335      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw1)) l) in
     336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPH)) l) in
     337      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (ADDRESS … globals lbl prf it it) l) in
    338338      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    339339      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    340340      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    341341      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
    342       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
    343       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    344         〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_address … lbl prf it it) l) graph, luniv〉
    345     | joint_instr_extension ext ⇒
     342      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc hdw2)) l) in
     343      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (to_acc RegisterDPL)) l) in
     344        〈add_graph globals original_label (sequential ltl_params_ globals (ADDRESS … lbl prf it it) l) graph, luniv〉
     345    | extension ext ⇒
    346346      match ext with
    347347      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
     
    351351        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    352352        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
    353           〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
     353          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
    354354      ]
    355     | joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     355    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    356356      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    357357      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
    358       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) 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
    364       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
    365       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    366       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    367       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv 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
    369         〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
     358      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (MOVE … (from_acc hdw)) l) in
     359      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … (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. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
     364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (sequential … globals (MOVE … globals (from_acc RegisterB)) fresh_lbl) in
     365      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     366      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     367      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     368      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. sequential … globals (MOVE … globals (to_acc hdw)) l) fresh_lbl in
     369        〈add_graph globals original_label (GOTO … globals fresh_lbl) graph, luniv〉
    370370    ]
    371   | joint_st_return ⇒ 〈add_graph globals original_label (joint_st_return ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    372   | joint_st_goto l ⇒ 〈add_graph globals original_label (joint_st_goto ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     371  | RETURN ⇒ 〈add_graph globals original_label (RETURN ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     372  | GOTO l ⇒ 〈add_graph globals original_label (GOTO ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    373373  ].
    374374
     
    435435    let 〈graph, luniv〉 ≝ graph_luniv in
    436436      match eliminable globals (valuation label) stmt with
    437       [ Some successor ⇒ 〈add_graph globals label (joint_st_goto … successor) graph, luniv〉
     437      [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
    438438      | None           ⇒
    439439        translate_statement globals int_fun valuation coloured_graph graph stmt label
  • src/ERTL/Interference.ma

    r1241 r1282  
    2525
    2626axiom build: ∀valuation. coloured_graph valuation.
    27 
    28 (*
    29 (* definition vertex_set ≝ set vertex. *)
    30 definition vertex_priority_set ≝ priority_set vertex.
    31 definition vertex_set_table ≝ set_table vertex (set vertex).
    32 definition vertex_set ≝ set vertex.
    33 definition Register_set_table ≝ set_table vertex (set Register).
    34 definition Register_set ≝ set Register.
    35 *)
    36 
    37 (*
    38 record graph: Type[0] ≝
    39 {
    40   g_regmap     : register_table;
    41   g_ivv        : vertex_set_table;
    42   g_ivh        : Register_set_table;
    43   g_pvv        : vertex_set_table;
    44   g_pvh        : Register_set_table;
    45   g_degree     : vertex_priority_set;
    46   g_nmr        : vertex_priority_set
    47 }.
    48 
    49 definition set_ivv ≝
    50   λgraph.
    51   λivv: vertex_set_table.
    52     let regmap ≝ g_regmap graph in
    53     let ivh    ≝ g_ivh graph in
    54     let pvv    ≝ g_pvv graph in
    55     let pvh    ≝ g_pvh graph in
    56     let degree ≝ g_degree graph in
    57     let nmr    ≝ g_nmr graph in
    58       mk_graph
    59         regmap ivv ivh pvv pvh degree nmr.
    60 
    61 definition set_ivh ≝
    62   λgraph.
    63   λivh: Register_set_table.
    64     let regmap ≝ g_regmap graph in
    65     let ivv    ≝ g_ivv graph in
    66     let pvv    ≝ g_pvv graph in
    67     let pvh    ≝ g_pvh graph in
    68     let degree ≝ g_degree graph in
    69     let nmr    ≝ g_nmr graph in
    70       mk_graph
    71         regmap ivv ivh pvv pvh degree nmr.
    72 
    73 definition set_degree ≝
    74   λgraph.
    75   λdegree: vertex_priority_set.
    76     let regmap ≝ g_regmap graph in
    77     let ivv    ≝ g_ivv graph in
    78     let ivh    ≝ g_ivh graph in
    79     let pvv    ≝ g_pvv graph in
    80     let pvh    ≝ g_pvh graph in
    81     let nmr    ≝ g_nmr graph in
    82       mk_graph
    83         regmap ivv ivh pvv pvh degree nmr.
    84 
    85 definition set_nmr ≝
    86   λgraph.
    87   λnmr: vertex_priority_set.
    88     let regmap ≝ g_regmap graph in
    89     let ivv    ≝ g_ivv graph in
    90     let ivh    ≝ g_ivh graph in
    91     let pvv    ≝ g_pvv graph in
    92     let pvh    ≝ g_pvh graph in
    93     let degree ≝ g_degree graph in
    94       mk_graph
    95         regmap ivv ivh pvv pvh degree nmr.
    96 
    97 definition sg_neighboursv ≝
    98   λgraph: graph.
    99   λv: vertex.
    100     set_tbl_find … v (g_ivv graph).
    101 
    102 definition sg_existsvv ≝
    103   λgraph.
    104   λv1.
    105   λv2.
    106   match sg_neighboursv graph v2 with
    107   [ None       ⇒ false (* XXX: ok? *)
    108   | Some neigh ⇒ set_member ? eq_nat v1 neigh
    109   ].
    110 
    111 definition sg_neighboursh ≝
    112   λgraph.
    113   λv.
    114     set_tbl_find ? ? v (g_ivh graph).
    115 
    116 definition sg_existsvh ≝
    117   λgraph.
    118   λv.
    119   λh.
    120   match sg_neighboursh graph v with
    121   [ None       ⇒ false (* XXX: ok? *)
    122   | Some neigh ⇒ set_member ? eq_Register h neigh
    123   ].
    124 
    125 definition sg_degree ≝
    126   λgraph.
    127   λv.
    128   match sg_neighboursv graph v with
    129   [ None ⇒ None ?
    130   | Some neigh ⇒
    131     match sg_neighboursh graph v with
    132     [ None ⇒ None ?
    133     | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
    134     ]
    135   ].
    136    
    137 definition sg_hwregs ≝
    138   λgraph: graph.
    139     let union ≝ λkey: vertex. set_union ? in
    140     set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).
    141 
    142 axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
    143 
    144 definition sg_mkvvi ≝
    145   λgraph.
    146   λv1.
    147   λv2.
    148     set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).
    149 
    150 definition sg_mkvv ≝
    151   λgraph.
    152   λv1.
    153   λv2.
    154     if eq_nat v1 v2 then
    155       graph
    156     else if sg_existsvv graph v1 v2 then
    157       graph
    158     else
    159       sg_mkvvi graph v1 v2.
    160 
    161 definition sg_rmvv ≝
    162   λgraph.
    163   λv1.
    164   λv2.
    165     set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).
    166 
    167 definition sg_rmvvifx ≝
    168   λgraph.
    169   λv1.
    170   λv2.
    171   if sg_existsvv graph v1 v2 then
    172     sg_rmvv graph v1 v2
    173   else
    174     graph.
    175 
    176 definition sg_mkvhi ≝
    177   λgraph.
    178   λv.
    179   λh.
    180     set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)).
    181 
    182 definition sg_mkvh ≝
    183   λgraph.
    184   λv.
    185   λh.
    186   if sg_existsvh graph v h then
    187     graph
    188   else
    189     sg_mkvhi graph v h.
    190 
    191 definition sg_rmvh ≝
    192   λgraph.
    193   λv.
    194   λh.
    195     set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).
    196 
    197 definition sg_rmvhifx ≝
    198   λgraph.
    199   λv.
    200   λh.
    201     if sg_existsvh graph v h then
    202       sg_rmvh graph v h
    203     else
    204       graph.
    205 
    206 definition sg_coalesce ≝
    207   λg.
    208   λx.
    209   λy.
    210   match sg_neighboursv g x with
    211   [ None       ⇒ None ?
    212   | Some neigh ⇒
    213     let graph ≝ set_fold ? graph (λw. λg.
    214       sg_mkvv (sg_rmvv g x w) y w) neigh g
    215     in
    216     match sg_neighboursh g x with
    217     [ None ⇒ None ?
    218     | Some neigh ⇒
    219       let graph ≝ set_fold ? ? (λh. λg.
    220         sg_mkvh (sg_rmvh g x h) y h) neigh g
    221       in
    222         Some … graph
    223     ]
    224   ].
    225 
    226 definition sg_coalesceh ≝
    227   λg.
    228   λx.
    229   λh.
    230   match sg_neighboursv g x with
    231   [ None       ⇒ None ?
    232   | Some neigh ⇒
    233     let graph ≝ set_fold ? graph (λw. λg.
    234       sg_mkvh (sg_rmvv g x w) w h) neigh g
    235     in
    236     match sg_neighboursh g x with
    237     [ None ⇒ None ?
    238     | Some neigh ⇒
    239       let graph ≝ set_fold ? ? (λk. λg.
    240         sg_rmvh graph x k) neigh g
    241       in
    242         Some … graph
    243     ]
    244   ].
    245 
    246 definition sg_remove ≝
    247   λg.
    248   λx.
    249   match sg_neighboursv g x with
    250   [ None ⇒ None ?
    251   | Some neigh ⇒
    252     let graph ≝
    253       set_fold … (λw. λgraph.
    254         sg_rmvv graph x w) neigh g
    255     in
    256     match sg_neighboursh graph x with
    257     [ None ⇒ None ?
    258     | Some neigh ⇒
    259       let graph ≝ set_fold … (λh. λg.
    260         sg_rmvh g x h) neigh graph
    261       in
    262         Some ? graph
    263     ]
    264   ].
    265 
    266 definition ig_mkvvi ≝
    267   λgraph.
    268   λv1.
    269   λv2.
    270   let graph ≝ sg_mkvvi graph v1 v2 in
    271   let graph ≝ sg_rmvvifx graph v1 v2 in
    272   let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in
    273   let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in
    274     set_degree (set_nmr graph nmr') degree'.
    275 
    276 definition ig_rmvv ≝
    277   λgraph.
    278   λv1.
    279   λv2.
    280   let graph ≝ sg_rmvv graph v1 v2 in
    281   let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in
    282   let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in
    283     set_degree (set_nmr graph nmr') degree'.
    284 
    285 definition ig_mkvhi ≝
    286   λgraph.
    287   λv.
    288   λh.
    289   let graph ≝ sg_mkvhi graph v h in
    290   let graph ≝ sg_rmvhifx graph v h in
    291   let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
    292   let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
    293     set_degree (set_nmr graph nmr) degree.
    294 
    295 definition ig_rmvh ≝
    296   λgraph.
    297   λv.
    298   λh.
    299   let graph ≝ sg_rmvh graph v h in
    300   let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in
    301   let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in
    302     set_degree (set_nmr graph nmr) degree.
    303 
    304 definition pref_nmr ≝
    305   λgraph.
    306   λv.
    307   match sg_neighboursv graph v with
    308   [ None       ⇒ false (* XXX: ok? *)
    309   | Some neigh ⇒
    310     match sg_neighboursh graph v with
    311     [ None        ⇒ false
    312     | Some neigh' ⇒
    313       andb (set_is_empty ? neigh) (set_is_empty ? neigh')
    314     ]
    315   ].
    316 
    317 definition pref_mkcheck ≝
    318   λgraph.
    319   λv.
    320     if pref_nmr graph v then
    321       let nmr' ≝ pset_remove ? v (g_nmr graph) in
    322         set_nmr graph nmr'
    323     else
    324       graph.
    325 
    326 definition pref_mkvvi ≝
    327   λgraph.
    328   λv1.
    329   λv2.
    330     if sg_existsvv graph v1 v2 then
    331       graph
    332     else
    333       let graph ≝ pref_mkcheck graph v1 in
    334       let graph ≝ pref_mkcheck graph v2 in
    335         sg_mkvvi graph v1 v2.
    336 
    337 definition pref_mkvhi ≝
    338   λgraph.
    339   λv.
    340   λh.
    341   if sg_existsvh graph v h then
    342     graph
    343   else
    344     let graph ≝ pref_mkcheck graph v in
    345       sg_mkvhi graph v h.
    346 
    347 (* XXX: look at this carefully *)
    348 definition pref_rmcheck ≝
    349   λgraph.
    350   λv.
    351   if pref_nmr graph v then
    352     match pset_lookup ? v (g_degree graph) with
    353     [ None ⇒ graph (* XXX: ok? *)
    354     | Some pref ⇒
    355       let nmr ≝ pset_insert ? v pref (g_nmr graph) in
    356         set_nmr graph nmr
    357     ]
    358   else
    359     graph.
    360 
    361 definition pref_rmvv ≝
    362   λgraph.
    363   λv1.
    364   λv2.
    365   let graph ≝ sg_rmvv graph v1 v2 in
    366   let graph ≝ pref_rmcheck graph v1 in
    367   let graph ≝ pref_rmcheck graph v2 in
    368     graph.
    369 
    370 definition pref_rmvh ≝
    371   λgraph.
    372   λv.
    373   λh.
    374   let graph ≝ sg_rmvh graph v h in
    375   let graph ≝ pref_rmcheck graph v in
    376     graph.
    377    
    378 definition ig_ipp ≝ sg_neighboursv.
    379 definition ig_iph ≝ sg_neighboursh.
    380 definition ig_ppp ≝ sg_neighboursv.
    381 definition ig_pph ≝ sg_neighboursh.
    382 definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph).
    383 definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph).
    384 definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph).
    385 definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu.
    386   rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu.
    387 
    388 definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝
    389   λa: Type[0].
    390   λcompare: a → a → order.
    391   λf: vertex → a.
    392   λgraph.
    393   let folded ≝ ig_fold … (λw. λaccu.
    394     let dw ≝ f w in
    395       match accu with
    396       [ None      ⇒ Some … 〈dw, w〉
    397       | Some dv_v ⇒
    398         let 〈dv, v〉 ≝ dv_v in
    399           match compare dw dv with
    400           [ order_lt ⇒ Some … 〈dw, w〉
    401           | _        ⇒ accu
    402           ]
    403       ]) graph (None …)
    404   in
    405     match folded with
    406     [ None          ⇒ None …
    407     | Some ignore_v ⇒
    408       let 〈ignore, v〉 ≝ ignore_v in
    409         Some … v
    410     ].
    411    
    412 definition ig_ppedge ≝ vertex × vertex.
    413 
    414 definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p.
    415 
    416 definition ig_phedge ≝ vertex × Register.
    417 
    418 definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p.
    419 
    420 definition ig_create ≝
    421   λregs.
    422   let 〈ignore_int, table'', priority''〉 ≝
    423     foldr … (λr. λv_table_priority'.
    424       let 〈v, table', priority'〉 ≝ v_table_priority' in
    425       let table'' ≝ rt_add r v table' in
    426       let priority'' ≝ pset_insert ? v 0 priority' in
    427         〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
    428   in
    429       mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …)
    430       (set_tbl_empty …) priority'' priority''.
    431 definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph).
    432 definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph).
    433 definition ig_mkipp ≝
    434   λgraph.
    435   λregs1.
    436   λregs2.
    437     set_fold … (λr1. λgraph.
    438       let v1 ≝ ig_lookup graph r1 in
    439         set_fold … (λr2. λgraph.
    440           sg_mkvv graph v1 (ig_lookup graph r2)
    441         ) regs2 graph
    442     ) regs1 graph.
    443 definition ig_mkiph ≝
    444   λgraph.
    445   λregs.
    446   λhwregs.
    447     set_fold … (λr. λgraph.
    448       let v ≝ ig_lookup graph r in
    449         set_fold … (λh. λgraph.
    450           sg_mkvh graph v h
    451         ) hwregs graph
    452     ) regs graph.
    453 definition ig_mki ≝
    454   λgraph.
    455   λregs1_hwregs1.
    456   λregs2_hwregs2.
    457   let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
    458   let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
    459   let graph ≝ ig_mkipp graph regs1 regs2 in
    460   let graph ≝ ig_mkiph graph regs1 hwregs2 in
    461   let graph ≝ ig_mkiph graph regs2 hwregs1 in
    462     graph.
    463 definition ig_mkppp ≝
    464   λgraph.
    465   λr1.
    466   λr2.
    467   let v1 ≝ ig_lookup graph r1 in
    468   let v2 ≝ ig_lookup graph r2 in
    469   let graph ≝ sg_mkvv graph v1 v2 in
    470     graph.
    471 definition ig_mkpph ≝
    472   λgraph.
    473   λr.
    474   λh.
    475   let v ≝ ig_lookup graph r in
    476   let graph ≝ sg_mkvh graph v h in
    477     graph.
    478 (*   
    479 (* XXX: precondition:
    480   x \not\eq y
    481   existsvv graph x y == false i.e. coalesce interfering edges *)
    482 definition ig_coalesce ≝
    483   λgraph.
    484   λx.
    485   λy.
    486   let graph ≝ sg_coalesce graph x y in
    487 
    488 let coalesce graph x y =
    489 
    490   assert (x <> y); (* attempt to coalesce one vertex with itself *)
    491   assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
    492 
    493   (* Perform coalescing in the two subgraphs. *)
    494 
    495   let graph = interference#coalesce graph x y in
    496   let graph = preference#coalesce graph x y in
    497 
    498   (* Remove [x] from all tables. *)
    499 
    500   {
    501     graph with
    502     regmap = RegMap.coalesce x y graph.regmap;
    503     ivh = Vertex.Map.remove x graph.ivh;
    504     pvh = Vertex.Map.remove x graph.pvh;
    505     degree = PrioritySet.remove x graph.degree;
    506     nmr = PrioritySet.remove x graph.nmr;
    507   }
    508 
    509 axiom ig_mkppp: graph → register → register → graph.
    510 axiom ig_mkpph: graph → register → Register → graph.
    511 axiom ig_coalesce: graph → vertex → vertex → graph.
    512 axiom ig_coalesceh: graph → vertex → Register → graph.
    513 axiom ig_remove: graph → vertex → graph.
    514 axiom ig_freeze: graph → vertex → graph.
    515 axiom ig_restrict: graph → (vertex → bool) → graph.
    516 axiom ig_droph: graph → graph.
    517 axiom ig_lookup: graph → register → vertex.
    518 axiom ig_registers: graph → vertex → list register.
    519 axiom ig_degree: graph → vertex → nat.
    520 axiom ig_lowest: graph → option (vertex × nat).
    521 axiom ig_lowest_non_move_related: graph → option (vertex × nat).
    522 axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
    523   graph → option vertex.
    524 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A.
    525 axiom ig_ipp: graph → vertex → vertex_set.
    526 axiom ig_iph: graph → vertex → list Register.
    527 axiom ig_ppp: graph → vertex → vertex_set.
    528 axiom ig_pph: graph → vertex → list Register.
    529 definition ig_ppedge ≝ vertex × vertex.
    530 axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge.
    531 definition ig_phedge ≝ vertex × Register.
    532 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
    533 *)
    534 *)
  • src/ERTL/liveness.ma

    r1275 r1282  
    77  λs: ertl_statement globals.
    88  match s with
    9   [ joint_st_sequential seq l ⇒
    10     match seq with
    11     [ joint_instr_cond acc_a_reg lbl_true ⇒
     9  [ sequential seq l ⇒
     10    match seq with
     11    [ COND acc_a_reg lbl_true ⇒
    1212        set_insert … lbl_true (set_singleton … l)
    1313    | _ ⇒ set_singleton … l ]
    14   | joint_st_goto l ⇒ set_singleton … l
    15   | joint_st_return ⇒ set_empty ?
     14  | GOTO l ⇒ set_singleton … l
     15  | RETURN ⇒ set_empty ?
    1616  ].
    1717
     
    7878  λs: ertl_statement globals.
    7979  match s with
    80   [ joint_st_sequential seq l ⇒
    81     match seq with
    82     [ joint_instr_op2 op2 r1 r2 _ ⇒
     80  [ sequential seq l ⇒
     81    match seq with
     82    [ OP2 op2 r1 r2 _ ⇒
    8383      match op2 with
    8484      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     
    8787      | _ ⇒ lattice_psingleton r1
    8888      ]
    89     | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    90     | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    91     | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     89    | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
     90    | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
     91    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    9292       lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
    93     | joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    94     | joint_instr_pop r ⇒ lattice_psingleton r
    95     | joint_instr_int r _ ⇒ lattice_psingleton r
    96     | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    97     | joint_instr_load r _ _ ⇒ lattice_psingleton r
     93    | OP1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     94    | POP r ⇒ lattice_psingleton r
     95    | INT r _ ⇒ lattice_psingleton r
     96    | ADDRESS _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     97    | LOAD r _ _ ⇒ lattice_psingleton r
    9898    (* Potentially destroys all caller-save hardware registers. *)
    99     | joint_instr_call_id id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    100     | joint_instr_comment c ⇒ lattice_bottom
    101     | joint_instr_cond r lbl_true ⇒ lattice_bottom
    102     | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
    103     | joint_instr_cost_label clabel ⇒ lattice_bottom
    104     | joint_instr_push r ⇒ lattice_bottom
    105     | joint_instr_move pair_reg ⇒
     99    | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
     100    | COMMENT c ⇒ lattice_bottom
     101    | COND r lbl_true ⇒ lattice_bottom
     102    | STORE acc_a dpl dph ⇒ lattice_bottom
     103    | COST_LABEL clabel ⇒ lattice_bottom
     104    | PUSH r ⇒ lattice_bottom
     105    | MOVE pair_reg ⇒
    106106      (* first register relevant only *)
    107107      let r1 ≝ \fst pair_reg in
     
    110110      | hardware h ⇒ lattice_hsingleton h
    111111      ]
    112     | joint_instr_extension ext ⇒
     112    | extension ext ⇒
    113113      match ext with
    114114      [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    115115      | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    116116      | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
    117   | joint_st_return ⇒ lattice_bottom
    118   | joint_st_goto l ⇒ lattice_bottom
     117  | RETURN ⇒ lattice_bottom
     118  | GOTO l ⇒ lattice_bottom
    119119  ].
    120120
     
    125125  λs: ertl_statement globals.
    126126  match s with
    127   [ joint_st_sequential seq l ⇒
    128     match seq with
    129     [ joint_instr_op2 op2 acc_a r1 r2 ⇒
     127  [ sequential seq l ⇒
     128    match seq with
     129    [ OP2 op2 acc_a r1 r2 ⇒
    130130      match op2 with
    131131      [ Addc ⇒
     
    133133      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    134134      ]
    135     | joint_instr_clear_carry ⇒ lattice_bottom
    136     | joint_instr_set_carry ⇒ lattice_bottom
     135    | CLEAR_CARRY ⇒ lattice_bottom
     136    | SET_CARRY ⇒ lattice_bottom
    137137    (* acc_a and acc_b *)
    138     | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     138    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    139139       lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
    140     | joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2
    141     | joint_instr_pop r ⇒ lattice_bottom
    142     | joint_instr_int r _ ⇒ lattice_bottom
    143     | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
    144     | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
     140    | OP1 op1 r1 r2 ⇒ lattice_psingleton r2
     141    | POP r ⇒ lattice_bottom
     142    | INT r _ ⇒ lattice_bottom
     143    | ADDRESS _ _ r1 r2 ⇒ lattice_bottom
     144    | LOAD acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    145145    (* Reads the hardware registers that are used to pass parameters. *)
    146     | joint_instr_call_id _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    147     | joint_instr_comment c ⇒ lattice_bottom
    148     | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
    149     | joint_instr_store acc_a dpl dph ⇒
     146    | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
     147    | COMMENT c ⇒ lattice_bottom
     148    | COND r lbl_true ⇒ lattice_psingleton r
     149    | STORE acc_a dpl dph ⇒
    150150      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
    151     | joint_instr_cost_label clabel ⇒ lattice_bottom
    152     | joint_instr_push r ⇒ lattice_psingleton r
    153     | joint_instr_move pair_reg ⇒
     151    | COST_LABEL clabel ⇒ lattice_bottom
     152    | PUSH r ⇒ lattice_psingleton r
     153    | MOVE pair_reg ⇒
    154154      (* only second reg in pair relevant *)
    155155      let r2 ≝ \snd pair_reg in
     
    158158      | hardware h ⇒ lattice_hsingleton h
    159159      ]
    160   | joint_instr_extension ext ⇒
     160  | extension ext ⇒
    161161    match ext with
    162162    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    163163    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    164164    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
    165   | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    166   | joint_st_goto l ⇒ lattice_bottom
     165  | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     166  | GOTO l ⇒ lattice_bottom
    167167  ].
    168168
     
    173173  let 〈pliveafter, hliveafter〉 ≝ l in
    174174  match s with
    175   [ joint_st_sequential seq l ⇒
    176     match seq with
    177     [ joint_instr_op2 op2 r1 r2 r3 ⇒
     175  [ sequential seq l ⇒
     176    match seq with
     177    [ OP2 op2 r1 r2 r3 ⇒
    178178      if set_member … (eq_identifier …) r1 pliveafter ∨
    179179         set_member … eq_Register RegisterCarry hliveafter then
     
    181181      else
    182182        Some ? l
    183     | joint_instr_clear_carry ⇒ None ?
    184     | joint_instr_set_carry ⇒ None ?
    185     | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     183    | CLEAR_CARRY ⇒ None ?
     184    | SET_CARRY ⇒ None ?
     185    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    186186      if set_member … (eq_identifier …) dr1 pliveafter ∨
    187187         set_member … (eq_identifier …) dr2 pliveafter ∨
     
    190190      else
    191191        Some ? l
    192     | joint_instr_op1 op1 r1 r2 ⇒
     192    | OP1 op1 r1 r2 ⇒
    193193      if set_member … (eq_identifier …) r1 pliveafter ∨
    194194         set_member … eq_Register RegisterCarry hliveafter then
     
    196196      else
    197197        Some ? l
    198     | joint_instr_pop r ⇒ None ?
    199     | joint_instr_int r _ ⇒
     198    | POP r ⇒ None ?
     199    | INT r _ ⇒
    200200      if set_member … (eq_identifier …) r pliveafter ∨
    201201         set_member … eq_Register RegisterCarry hliveafter then
     
    203203      else
    204204        Some ? l
    205     | joint_instr_address _ _ r1 r2 ⇒
     205    | ADDRESS _ _ r1 r2 ⇒
    206206      if set_member … (eq_identifier …) r1 pliveafter ∨
    207207         set_member … (eq_identifier …) r2 pliveafter ∨
     
    210210      else
    211211        Some ? l
    212     | joint_instr_load acc_a dpl dph ⇒
     212    | LOAD acc_a dpl dph ⇒
    213213      if set_member ? (eq_identifier …) acc_a pliveafter ∨
    214214         set_member … eq_Register RegisterCarry hliveafter then
     
    216216      else
    217217        Some ? l
    218     | joint_instr_call_id _ nparams _ ⇒ None ?
    219     | joint_instr_comment c ⇒ None ?
    220     | joint_instr_cond r lbl_true ⇒ None ?
    221     | joint_instr_store acc_a dpl dph ⇒ None ?
    222     | joint_instr_cost_label clabel ⇒ None ?
    223     | joint_instr_push r ⇒ None ?
    224     | joint_instr_move pair_reg ⇒
     218    | CALL_ID _ nparams _ ⇒ None ?
     219    | COMMENT c ⇒ None ?
     220    | COND r lbl_true ⇒ None ?
     221    | STORE acc_a dpl dph ⇒ None ?
     222    | COST_LABEL clabel ⇒ None ?
     223    | PUSH r ⇒ None ?
     224    | MOVE pair_reg ⇒
    225225      let r1 ≝ \fst pair_reg in
    226226      let r2 ≝ \snd pair_reg in
     
    237237        else
    238238          Some ? l]
    239     | joint_instr_extension ext ⇒
     239    | extension ext ⇒
    240240      match ext with
    241241      [ ertl_st_ext_new_frame ⇒ None ?
     
    247247        else
    248248          Some ? l]]
    249   | joint_st_goto l ⇒ None ?
    250   | joint_st_return ⇒ None ?
     249  | GOTO l ⇒ None ?
     250  | RETURN ⇒ None ?
    251251  ].
    252252
Note: See TracChangeset for help on using the changeset viewer.