Changeset 1282


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

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

Location:
src
Files:
1 deleted
10 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
  • src/LIN/LINToASM.ma

    r1275 r1282  
    3131  let generated ≝
    3232    match instr with
    33     [ joint_st_sequential instr' _ ⇒
     33    [ sequential instr' _ ⇒
    3434      match instr' with
    35       [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    36       | joint_instr_cond acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     35      [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     36      | COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3737      | _ ⇒ set_empty ?
    3838      ]
    39     | joint_st_return ⇒ set_empty ?
    40     | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
     39    | RETURN ⇒ set_empty ?
     40    | GOTO lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
    4141  in
    4242  match label with
     
    8787  λstatement: pre_lin_statement globals_old.
    8888  match statement with
    89   [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    90   | joint_st_return ⇒ Instruction (RET ?)
    91   | joint_st_sequential instr _ ⇒
     89  [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl)
     90  | RETURN ⇒ Instruction (RET ?)
     91  | sequential instr _ ⇒
    9292      match instr with
    93       [ joint_instr_extension ext ⇒ ⊥
    94       | joint_instr_comment comment ⇒ Comment comment
    95       | joint_instr_cost_label lbl ⇒ Cost (word_of_identifier ? lbl)
    96       | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
    97       | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
    98       | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    99       | joint_instr_call_id f _ _ ⇒ Call (word_of_identifier ? f)
    100       | joint_instr_opaccs accs _ _ _ _ ⇒
     93      [ extension ext ⇒ ⊥
     94      | COMMENT comment ⇒ Comment comment
     95      | COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl)
     96      | POP _ ⇒ Instruction (POP ? accumulator_address)
     97      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     98      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     99      | CALL_ID f _ _ ⇒ Call (word_of_identifier ? f)
     100      | OPACCS accs _ _ _ _ ⇒
    101101        match accs with
    102102        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    103103        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    104104        ]
    105       | joint_instr_op1 op1 _ _ ⇒
     105      | OP1 op1 _ _ ⇒
    106106        match op1 with
    107107        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    108108        | Inc ⇒ Instruction (INC ? ACC_A)
    109109        ]
    110       | joint_instr_op2 op2 _ _ reg ⇒
     110      | OP2 op2 _ _ reg ⇒
    111111        match op2 with
    112112        [ Add ⇒
     
    189189          ] (subaddressing_modein … reg')
    190190        ]
    191       | joint_instr_int reg byte ⇒
     191      | INT reg byte ⇒
    192192        let reg' ≝ register_address reg in
    193193          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    202202          | _ ⇒ λother: False. ⊥
    203203          ] (subaddressing_modein … reg')
    204       | joint_instr_move regs ⇒
     204      | MOVE regs ⇒
    205205         match regs with
    206206          [ from_acc reg ⇒
     
    230230               | _ ⇒ λother: False. ⊥
    231231               ] (subaddressing_modein … reg')]
    232       | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    233       | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    234       | joint_instr_address addr proof _ _ ⇒
     232      | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     233      | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     234      | ADDRESS addr proof _ _ ⇒
    235235        let look ≝ association addr globals (prf ? proof) in
    236236          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    237       | joint_instr_cond _ lbl ⇒
     237      | COND _ lbl ⇒
    238238        (* dpm: this should be handled in translate_code! *)
    239239        Instruction (JNZ ? (word_of_identifier ? lbl))
    240       | joint_instr_set_carry
     240      | SET_CARRY
    241241        Instruction (SETB ? CARRY)
    242242      ]
  • src/LTL/LTLToLIN.ma

    r1250 r1282  
    88  λs: ltl_statement globals.
    99  match s with
    10   [ joint_st_return ⇒ joint_st_return ??
    11   | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
    12   | joint_st_goto l ⇒ joint_st_goto lin_params_ globals l
     10  [ RETURN ⇒ RETURN ??
     11  | sequential instr lbl ⇒ sequential … instr it
     12  | GOTO l ⇒ GOTO lin_params_ globals l
    1313  ].
    1414
     
    2727  | S n' ⇒
    2828    if set_member … (word_of_identifier … l) visited then
    29      〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉
     29     〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉
    3030    else
    3131     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
     
    3636       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
    3737       match statement with
    38        [ joint_st_sequential instr l2 ⇒
     38       [ sequential instr l2 ⇒
    3939         match instr with
    40          [ joint_instr_cond acc_a_reg l1 ⇒
     40         [ COND acc_a_reg l1 ⇒
    4141            let 〈required', generated''〉 ≝
    4242             visit globals g required visited' generated' l2 n' in
     
    4747               visit globals g required'' visited' generated'' l1 n'
    4848         | _ ⇒ visit globals g required visited' generated' l2 n']
    49      | joint_st_return ⇒ 〈required, generated'〉
    50      | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n']]].
     49     | RETURN ⇒ 〈required, generated'〉
     50     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
    5151[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
    5252qed.
  • src/RTL/RTLTailcall.ma

    r1275 r1282  
    88  λgraph: codeT … (rtlntc_params globals).
    99  match stmt with
    10   [ joint_st_sequential seq DUMMY ⇒
     10  [ sequential seq DUMMY ⇒
    1111     match seq with
    12       [ joint_instr_extension ext ⇒
     12      [ extension ext ⇒
    1313         match ext with
    1414          [ rtl_st_ext_tailcall_id f args ⇒
    15               add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit)
     15              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
    1616          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
    17               add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
     17              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
    1818          | _ ⇒ graph ]
    1919      | _ ⇒ graph ]
  • src/RTL/RTLtoERTL.ma

    r1280 r1282  
    1010   λdestr_srcr.λstart_lbl.
    1111    let 〈destr, srcr〉 ≝ destr_srcr in
    12      adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
     12     adds_graph ertl_params1 globals [ sequential … (MOVE … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
    1313  in
    1414   map ? ? save_hdws_internal l.
     
    2020    λstart_lbl: label.
    2121     let 〈srcr, destr〉 ≝ srcr_destr in
    22      adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
     22     adds_graph ertl_params1 globals [ sequential … (MOVE … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
    2323   in
    2424    map ? ? restore_hdws_internal l.
     
    2828  λparams: list register.
    2929  match params with
    30   [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto … start_lbl ] start_lbl]
     30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … start_lbl ] start_lbl]
    3131  | _ ⇒
    3232    let l ≝ zip_pottier ? ? params RegisterParams in
     
    4444  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    4545  adds_graph ertl_params1 globals [
    46     joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;
    47     joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl;
    48     joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl;
    49     joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
    50     joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl;
    51     joint_st_sequential … (joint_instr_int … addr2 (bitvector_of_nat 8 0)) start_lbl;
    52     joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
    53     joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl;
    54     joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl
     46    sequential … (extension … (ertl_st_ext_frame_size addr1)) start_lbl;
     47    sequential … (INT … tmpr int_offset) start_lbl;
     48    sequential … (OP2 … Sub addr1 addr1 tmpr) start_lbl;
     49    sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
     50    sequential … (OP2 … Add addr1 addr1 tmpr) start_lbl;
     51    sequential … (INT … addr2 (bitvector_of_nat 8 0)) start_lbl;
     52    sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
     53    sequential … (OP2 … Addc addr2 addr2 tmpr) start_lbl;
     54    sequential … (LOAD … destr addr1 addr2) start_lbl
    5555  ] start_lbl dest_lbl def.
    5656 
     
    5858  λglobals,params.
    5959  match params with
    60   [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl ]
     60  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl ]
    6161  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
    6262
     
    8484      add_translates …
    8585         ((adds_graph ertl_params1 … [
    86                      joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
     86                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
    8787                   ]) ::
    8888         (adds_graph … [
    89                       joint_st_sequential … (joint_instr_pop … sral) start_lbl;
    90                       joint_st_sequential … (joint_instr_pop … srah) start_lbl
     89                      sequential … (POP … sral) start_lbl;
     90                      sequential … (POP … srah) start_lbl
    9191                   ]) ::
    9292         (save_hdws … sregs) @
     
    113113    let restl ≝ \snd (\fst crl) in
    114114    let restr ≝ \snd (\snd crl) in
    115     let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero …)) start_lbl in
    116     let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
     115    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) start_lbl in
     116    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) start_lbl in
    117117    let saves ≝ map2 … f_save commonl commonr crl_proof in
    118     let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
     118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) start_lbl in
    119119    let defaults ≝ map … f_default restl in
    120120      adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     
    127127    let commonl ≝ \fst (\fst crl) in
    128128    let commonr ≝ \fst (\snd crl) in
    129     let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
     129    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) start_lbl in
    130130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    131131      adds_graph ertl_params1 … insts start_lbl
     
    150150        restore_hdws … sregs @
    151151        [adds_graph … [
    152           joint_st_sequential … (joint_instr_push … srah) start_lbl;
    153           joint_st_sequential … (joint_instr_push … sral) start_lbl
     152          sequential … (PUSH … srah) start_lbl;
     153          sequential … (PUSH … sral) start_lbl
    154154        ]] @
    155155        [adds_graph ertl_params1 … [
    156           joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
     156          sequential … (extension … ertl_st_ext_del_frame) start_lbl
    157157        ]] @
    158158        [assign_result globals]
     
    205205  λglobals,params.
    206206  match params with
    207   [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl]
     207  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl]
    208208  | _ ⇒
    209209    let l ≝ zip_pottier ? ? params RegisterParams in
     
    223223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    224224    adds_graph ertl_params1 … [
    225       joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl;
    226       joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
    227       joint_st_sequential … (joint_instr_clear_carry …) start_lbl;
    228       joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl;
    229       joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
    230       joint_st_sequential … (joint_instr_int … addr2 (zero ?)) start_lbl;
    231       joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl;
    232       joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) start_lbl
     225      sequential … (INT … addr1 int_off) start_lbl;
     226      sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
     227      sequential … (CLEAR_CARRY …) start_lbl;
     228      sequential … (OP2 … Sub addr1 tmpr addr1) start_lbl;
     229      sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
     230      sequential … (INT … addr2 (zero ?)) start_lbl;
     231      sequential … (OP2 … Sub addr2 tmpr addr2) start_lbl;
     232      sequential … (STORE … addr1 addr2 srcr) start_lbl
    233233    ] start_lbl dest_lbl def.   
    234234
     
    236236  λglobals,params.
    237237  match params with
    238   [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [joint_st_goto … start_lbl] start_lbl]
     238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO … start_lbl] start_lbl]
    239239  | _ ⇒
    240240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
     
    259259    let commonl ≝ \fst (\fst crl) in
    260260    let commonr ≝ \fst (\snd crl) in
    261     let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware st, hardware ret〉) start_lbl in
     261    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) start_lbl in
    262262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    263263    match reduce_strong ? ? ret_regs RegisterSTS with
     
    265265      let commonl ≝ \fst (\fst crl) in
    266266      let commonr ≝ \fst (\snd crl) in
    267       let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in
     267      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) start_lbl in
    268268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    269269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
     
    281281    add_translates ertl_params1 globals (
    282282      set_params … args @ [
    283       adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
     283      adds_graph ertl_params1 … [ sequential … (CALL_ID … f nb_args it) start_lbl ];
    284284      fetch_result … ret_regs
    285285      ]
     
    294294  λdef.
    295295  match stmt with
    296   [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
    297   | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def
    298   | joint_st_sequential seq lbl' ⇒
     296  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
     297  | RETURN ⇒ add_graph … lbl (RETURN …) def
     298  | sequential seq lbl' ⇒
    299299     match seq with
    300       [ joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    301       | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    302       | joint_instr_call_id f args ret_regs ⇒
     300      [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     301      | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     302      | CALL_ID f args ret_regs ⇒
    303303         translate_call_id … f args ret_regs lbl lbl' def
    304       | joint_instr_move rs ⇒
     304      | MOVE rs ⇒
    305305         let 〈r1,r2〉 ≝ rs in
    306306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
    307           add_graph ertl_params1 ? lbl (joint_st_sequential … (joint_instr_move … rs) lbl') def
    308       | joint_instr_extension ext ⇒
     307          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
     308      | extension ext ⇒
    309309         match ext with
    310310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    311311          | rtlntc_st_ext_address r1 r2 ⇒
    312312             adds_graph ertl_params1 … [
    313               joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    314               joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
     313              sequential … (MOVE … 〈pseudo r1, hardware RegisterSPL〉) lbl;
     314              sequential … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) lbl
    315315             ] lbl lbl' def]
    316316      (*CSC: everything is just copied to re-type it from now on;
    317317        the problem is call_id that takes different parameters, but that is pattern-matched
    318318        above. It could be made nicer at the cost of making all the rest of the code uglier *)
    319       | joint_instr_cost_label cost_lbl ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cost_label … cost_lbl) lbl') def
    320       | joint_instr_address x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_address … x prf r1 r2) lbl') def
    321       | joint_instr_int r i ⇒  add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_int … r i) lbl') def
    322       | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
    323           add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
    324       | joint_instr_op1 op1 destr srcr ⇒
    325         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def
    326       | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
    327         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
    328       | joint_instr_clear_carry
    329         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_clear_carry …) lbl') def
    330       | joint_instr_set_carry
    331         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_set_carry …) lbl') def
    332       | joint_instr_load destr addr1 addr2 ⇒
    333         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_load … destr addr1 addr2) lbl') def
    334       | joint_instr_store addr1 addr2 srcr ⇒
    335         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) lbl') def
    336       | joint_instr_cond srcr lbl_true ⇒
    337         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cond … srcr lbl_true) lbl') def
    338       | joint_instr_comment msg ⇒
    339         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_comment … msg) lbl') def
     319      | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
     320      | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
     321      | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
     322      | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
     323          add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
     324      | OP1 op1 destr srcr ⇒
     325        add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
     326      | OP2 op2 destr srcr1 srcr2 ⇒
     327        add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
     328      | CLEAR_CARRY
     329        add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
     330      | SET_CARRY
     331        add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
     332      | LOAD destr addr1 addr2 ⇒
     333        add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
     334      | STORE addr1 addr2 srcr ⇒
     335        add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
     336      | COND srcr lbl_true ⇒
     337        add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
     338      | COMMENT msg ⇒
     339        add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
    340340      ]].
    341341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
     
    350350  let entry' ≝ joint_if_entry … def in
    351351  let exit' ≝ joint_if_exit … def in
    352   let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in
    353   let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in
     352  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
     353  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
    354354  let def' ≝
    355355    mk_joint_internal_function globals (ertl_params globals)
     
    390390    | Some stmt ⇒
    391391      match stmt with
    392       [ joint_st_sequential inst lbl ⇒
     392      [ sequential inst lbl ⇒
    393393         match inst with
    394           [ joint_instr_cost_label cost_lbl ⇒
    395              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (joint_st_goto … lbl) def〉
     394          [ COST_LABEL cost_lbl ⇒
     395             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
    396396          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    397       | joint_st_return ⇒ 〈None …, def〉
    398       | joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
     397      | RETURN ⇒ 〈None …, def〉
     398      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
    399399      ]]].
    400400   
     
    408408  match cost_label with
    409409  [ None ⇒ def
    410   | Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def
     410  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    411411  ].
    412412
  • src/RTLabs/RTLAbstoRTL.ma

    r1281 r1282  
    144144
    145145definition translate_cst_int_internal ≝
    146   λglobals,dest_lbl,r,i. joint_st_sequential rtl_params_ globals (joint_instr_int … r i) dest_lbl.
     146  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
    147147
    148148(*CSC: XXXXX *)
     
    161161  λdestr: register.
    162162  λsrcr: register.
    163     joint_st_sequential rtl_params_ globals (joint_instr_move … 〈destr,srcr〉) start_lbl.
     163    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl.
    164164
    165165definition translate_move ≝
     
    212212    add_translates … [
    213213      adds_graph rtl_params1 … [
    214         joint_st_sequential rtl_params_ … (joint_instr_int rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
     214        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
    215215        ];
    216216      translate_move globals destrs zeros
     
    10151015  λdef: joint_internal_function … (rtl_params globals).
    10161016  match stmt with
    1017   [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
     1017  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    10181018  | _ ⇒ ? ].
    10191019(*
     
    10871087  let entry' ≝ f_entry def in
    10881088  let exit' ≝ f_exit def in
    1089   let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in
    1090   let graph' ≝ add … graph' exit' (joint_st_goto … exit') in
     1089  let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in
     1090  let graph' ≝ add … graph' exit' (GOTO … exit') in
    10911091  let res ≝
    10921092    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
  • src/joint/Joint.ma

    r1280 r1282  
    3030
    3131inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
    32   | joint_instr_comment: String → joint_instruction p globals
    33   | joint_instr_cost_label: costlabel → joint_instruction p globals
    34   | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
    35   | joint_instr_move: pair_reg p → joint_instruction p globals
    36   | joint_instr_pop: acc_a_reg p → joint_instruction p globals
    37   | joint_instr_push: acc_a_reg p → joint_instruction p globals
    38   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    39   | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
    40   | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    41   | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
    42   | joint_instr_clear_carry: joint_instruction p globals
    43   | joint_instr_set_carry: joint_instruction p globals
    44   | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
    45   | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    46   | joint_instr_call_id: ident → call_args p → call_dest p → joint_instruction p globals
    47   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
    48   | joint_instr_extension: extend_statements p → joint_instruction p globals.
     32  | COMMENT: String → joint_instruction p globals
     33  | COST_LABEL: costlabel → joint_instruction p globals
     34  | INT: generic_reg p → Byte → joint_instruction p globals
     35  | MOVE: pair_reg p → joint_instruction p globals
     36  | POP: acc_a_reg p → joint_instruction p globals
     37  | PUSH: acc_a_reg p → joint_instruction p globals
     38  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
     39  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
     40  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     41  | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
     42  | CLEAR_CARRY: joint_instruction p globals
     43  | SET_CARRY: joint_instruction p globals
     44  | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
     45  | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
     46  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
     47  | COND: acc_a_reg p → label → joint_instruction p globals
     48  | extension: extend_statements p → joint_instruction p globals.
    4949
    5050inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    51   | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    52   | joint_st_goto: label → joint_statement p globals
    53   | joint_st_return: joint_statement p globals.
     51  | sequential: joint_instruction p globals → succ p → joint_statement p globals
     52  | GOTO: label → joint_statement p globals
     53  | RETURN: joint_statement p globals.
    5454
    5555record params0: Type[1] ≝
  • src/joint/TranslateUtils.ma

    r1280 r1282  
    4242  λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.
    4343  match e with
    44   [ joint_st_goto _ ⇒ joint_st_goto … l
    45   | joint_st_return ⇒ joint_st_return ??
    46   | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr l].
     44  [ GOTO _ ⇒ GOTO … l
     45  | RETURN ⇒ RETURN ??
     46  | sequential instr _ ⇒ sequential … globals instr l].
    4747
    4848(*CSC: bad programming habit: the code below puts everywhere a fake
     
    5656    on stmt_list ≝
    5757  match stmt_list with
    58   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
     58  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    5959  | cons stmt stmt_list ⇒
    6060    match stmt_list with
     
    7474    on translate_list ≝
    7575  match translate_list with
    76   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
     76  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    7777  | cons trans translate_list ⇒
    7878    match translate_list with
Note: See TracChangeset for help on using the changeset viewer.