Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (8 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

    r1197 r1311  
    22include "LTL/LTL.ma".
    33include "ERTL/spill.ma".
    4 include "ERTL/build.ma".
    5 include "utilities/Interference.ma".
    64include "ASM/Arithmetic.ma".
    7 
    8 (* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
    9 
    10 inductive decision: Type[0] ≝
    11   | decision_spill: Byte → decision
    12   | decision_colour: Register → decision.
    13  
    14 definition interference_lookup ≝
    15   λglobals.
    16   λint_fun.
    17   λr.
    18   let 〈liveafter, graph〉 ≝ build globals int_fun in
    19   let lkup ≝ ig_lookup graph r in
    20     vm_find lkup colour_colouring.
    21  
    22 definition lookup: register → decision ≝
    23   λr.
    24   match ? r with
    25   [ colour_spill
    26  
    27 axiom lookup: register → decision.
    285
    296definition fresh_label ≝
     
    318  λluniv.
    329    fresh LabelTag luniv.
     10
     11definition ltl_statement_graph ≝
     12  λglobals.
     13    graph … (ltl_statement globals).
    3314
    3415definition add_graph ≝
     
    5132  λglobals.
    5233  λint_fun.
    53     colour_locals + (ertl_if_stacksize globals int_fun).
     34    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
    5435
    5536definition stacksize ≝
    5637  λglobals.
    5738  λint_fun.
    58     colour_locals + (ertl_if_stacksize globals int_fun).
     39    colour_locals + (joint_if_stacksize globals (ertl_params globals) int_fun).
    5940
    6041definition adjust_off ≝
     
    6748
    6849definition get_stack:
    69  ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
    70   ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
    71 
     50 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label → ? ≝
    7251  λglobals: list ident.
    7352  λint_fun.
     
    7655  λoff.
    7756  λl.
     57  λoriginal_label.
    7858    let off ≝ adjust_off globals int_fun off in
    79     let luniv ≝ ertl_if_luniverse globals int_fun in
    80     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
    81     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    82     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    83     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
    84     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    85     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    86     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    87       〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     59    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     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〉.
    8868
    8969definition set_stack:
    9070  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
    91     → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag))
     71    → Register → label → ?
    9272  λglobals: list ident.
    9373  λint_fun.
     
    9676  λr.
    9777  λl.
     78  λoriginal_label.
    9879  let off ≝ adjust_off globals int_fun off in
    99   let luniv ≝ ertl_if_luniverse globals int_fun in
    100   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
    101   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
    102   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    103   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
    104   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    105   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    106   let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    107     〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
    108 
    109 definition write:
    110   ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
    111     ? ≝
    112   λglobals: list ident.
    113   λint_fun.
     80  let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     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〉.
     89
     90
     91definition write ≝
     92  λglobals: list ident.
     93  λint_fun: ertl_internal_function globals.
     94  λvaluation.
     95  λcoloured_graph.
    11496  λgraph.
    11597  λr.
    11698  λl.
    117   match lookup r with
     99  λoriginal_label: label.
     100  match colouring valuation coloured_graph (inl … r) with
    118101  [ decision_spill off ⇒
    119     let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
    120     let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
     102    let luniv ≝ joint_if_luniverse … int_fun in
     103    let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l original_label in
    121104      〈RegisterSST, l, graph, luniv〉
    122105  | decision_colour hwr ⇒
    123     let luniv ≝ ertl_if_luniverse globals int_fun in
     106    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    124107      〈hwr, l, graph, luniv〉
    125108  ].
    126109
    127 definition read:
    128   ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
    129     → (Register → ltl_statement globals) → ? ≝
    130   λglobals.
    131   λint_fun.
     110definition read ≝
     111  λglobals: list ident.
     112  λint_fun: ertl_internal_function globals.
     113  λvaluation.
     114  λcoloured_graph.
    132115  λgraph.
    133116  λr.
    134117  λstmt.
    135   match lookup r with
    136   [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
     118  λoriginal_label: label.
     119  match colouring valuation coloured_graph (inl … r) with
     120  [ decision_colour hwr ⇒
     121    let luniv ≝ joint_if_luniverse … int_fun in
     122      〈add_graph globals original_label (stmt hwr) graph, luniv〉
    137123  | decision_spill off ⇒
    138124    let temphwr ≝ RegisterSST in
    139     let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
    140     let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
    141       generate globals luniv graph stmt
     125    let luniv ≝ joint_if_luniverse … int_fun in
     126    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (stmt temphwr) in
     127      get_stack globals int_fun graph temphwr (bitvector_of_nat … off) l original_label
    142128  ].
    143129
     
    149135  λsrc: decision.
    150136  λl: label.
     137  λoriginal_label: label.
    151138  match dest with
    152139  [ decision_colour dest_hwr ⇒
    153140    match src with
    154141    [ decision_colour src_hwr ⇒
    155       let luniv ≝ ertl_if_luniverse globals int_fun in
     142      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    156143      if eq_Register dest_hwr src_hwr then
    157         〈joint_st_goto … globals l, graph, luniv〉
     144        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    158145      else
    159         let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
    160           〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
    161     | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
     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〉
     148    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr (bitvector_of_nat … src_off) l original_label
    162149    ]
    163150  | decision_spill dest_off ⇒
    164151    match src with
    165     [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
     152    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph (bitvector_of_nat … dest_off) src_hwr l original_label
    166153    | decision_spill src_off ⇒
    167       let luniv ≝ ertl_if_luniverse globals int_fun in
    168       if eq_bv ? dest_off src_off then
    169         〈joint_st_goto … globals l, graph, luniv〉
     154      let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     155      if eq_nat dest_off src_off then
     156        〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    170157      else
    171158        let temp_hwr ≝ RegisterSST in
    172         let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
    173         let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
    174           get_stack globals int_fun graph temp_hwr src_off l
     159        let 〈graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … dest_off) temp_hwr l original_label in
     160          get_stack globals int_fun graph temp_hwr (bitvector_of_nat … src_off) l original_label
    175161    ]
    176162  ].
     
    181167  λgraph: ltl_statement_graph globals.
    182168  λl: label.
     169  λoriginal_label: label.
    183170  if eq_nat (stacksize globals int_fun) 0 then
    184     〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
     171    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     172      〈add_graph globals original_label (GOTO … globals l) graph, luniv〉
    185173  else
    186     let luniv ≝ ertl_if_luniverse globals int_fun in
    187     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    188     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
    189     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
    190     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
    191     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    192     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
    193     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
    194     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
    195       〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
     174    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     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〉.
    196184
    197185definition delframe ≝
     
    200188  λgraph: graph (ltl_statement globals).
    201189  λl.
     190  λoriginal_label: label.
    202191  if eq_nat (stacksize globals int_fun) 0 then
    203     〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
     192    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     193      〈add_graph globals original_label (GOTO (ltl_params globals) globals l) graph, luniv〉
    204194  else
    205     let luniv ≝ ertl_if_luniverse globals int_fun in
    206     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
    207     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
    208     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
    209     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
    210     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
    211       〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
    212 
    213 definition translate_statement ≝
    214   λglobals: list ident.
    215   λint_fun.
     195    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
     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〉.
     202
     203definition translate_statement:
     204  ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
     205    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
     206      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
     207  λglobals: list ident.
     208  λint_fun.
     209  λvaluation.
     210  λcoloured_graph: coloured_graph valuation.
    216211  λgraph: ltl_statement_graph globals.
    217212  λstmt: ertl_statement globals.
     213  λoriginal_label: label.
    218214  match stmt with
    219   [ joint_st_sequential seq l ⇒
    220     let luniv ≝ ertl_if_luniverse globals int_fun in
     215  [ sequential seq l ⇒
     216    let luniv ≝ joint_if_luniverse globals (ertl_params globals) int_fun in
    221217    match seq with
    222     [ joint_instr_comment c ⇒
    223       〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
    224     | joint_instr_cost_label cost_lbl ⇒
    225       〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
    226     | joint_instr_pop r ⇒
    227       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
    228       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    229         〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
    230     | joint_instr_push r ⇒
    231       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
    232       let int_fun ≝ set_luniverse globals int_fun luniv in
    233       let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    234         〈joint_st_goto ltl_params globals l, graph, luniv〉
    235     | joint_instr_cond srcr lbl_true ⇒
    236       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    237       let int_fun ≝ set_luniverse globals int_fun luniv in
    238       let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    239         〈joint_st_goto ltl_params globals l, graph, luniv〉
    240     | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
    241     | joint_instr_store addr1 addr2 srcr ⇒
    242       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
    243       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
    244       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    245       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    246       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    247       let int_fun ≝ set_luniverse globals int_fun luniv in
    248       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    249       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    250       let int_fun ≝ set_luniverse globals int_fun luniv in
    251       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    252       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    253       let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    254         〈joint_st_goto ltl_params globals l, graph, luniv〉
    255     | joint_instr_load destr addr1 addr2 ⇒
    256       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
    257       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    258       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    259       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    260       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    261       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    262       let int_fun ≝ set_luniverse globals int_fun luniv in
    263       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    264       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    265       let int_fun ≝ set_luniverse globals int_fun luniv in
    266       let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    267         〈joint_st_goto ltl_params globals l, graph, luniv〉
    268     | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
    269     | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
    270     | joint_instr_op2 op2 destr srcr ⇒
    271       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
    272       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    273       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
    274       let luniv ≝ set_luniverse globals int_fun luniv in
    275       let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    276       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    277       let luniv ≝ set_luniverse globals int_fun luniv in
    278       let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    279         〈joint_st_goto ltl_params globals l, graph, luniv〉
    280     | joint_instr_op1 op1 acc_a ⇒
    281       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
    282       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    283       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
    284       let int_fun ≝ set_luniverse globals int_fun luniv in
    285       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    286         〈joint_st_goto ltl_params globals l, graph, luniv〉
    287     | joint_instr_int r i ⇒
    288       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
    289         〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
    290     | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    291       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
    292       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    293       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    294       let luniv ≝ set_luniverse globals int_fun luniv in
    295       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    296       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    297       let luniv ≝ set_luniverse globals int_fun luniv in
    298       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    299       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
    300       let luniv ≝ set_luniverse globals int_fun luniv in
    301       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
    302       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    303       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
    304       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    305       let luniv ≝ set_luniverse globals int_fun luniv in
    306       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    307       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    308       let luniv ≝ set_luniverse globals int_fun luniv in
    309       let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    310         〈joint_st_goto ltl_params globals l, graph, luniv〉
    311     | joint_instr_move pair_regs ⇒
     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 ⇒
     223      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     224      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     225      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 (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
     237      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     238      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     239      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
     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 ⇒
     264      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     265      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     266      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 (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 ⇒
     285      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     286      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     287      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 (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 ⇒
     299      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     300      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     301      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 (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 ⇒
     310      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     311      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     312      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
     313        〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw i) l) graph, luniv〉
     314    | MOVE pair_regs ⇒
    312315      let regl ≝ \fst pair_regs in
    313316      let regr ≝ \snd pair_regs in
    314317      match regl with
    315318      [ pseudo p1  ⇒
    316         match regr with
    317         [ pseudo p2  ⇒ move globals int_fun graph (lookup p1) (lookup p2) l
    318         | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l
     319        match regr with 
     320        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
     321        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
    319322        ]
    320323      | hardware h1 ⇒
    321324        match regr with
    322         [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l
     325        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    323326        | hardware h2 ⇒
    324           let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
    325             〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (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〉
    326329        ]
    327330      ]
    328     | joint_instr_address lbl prf dpl dph ⇒
    329       let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in
    330       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
    331       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    332       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
    333       let int_fun ≝ set_luniverse globals int_fun luniv in
    334       let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in
    335       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
    336       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    337         〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     331    | ADDRESS lbl prf dpl dph ⇒
     332      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     333      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     334      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 (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
     338      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     339      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     340      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     341      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 (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 ⇒
     346      match ext with
     347      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
     348      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label
     349      | ertl_st_ext_frame_size r ⇒
     350        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     351        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     352        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
     353          〈add_graph globals original_label (sequential ltl_params_ globals (INT … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
     354      ]
     355    | OPACCS opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     356      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     357      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 (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〉
    338370    ]
    339   | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
    340   | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
    341   | joint_st_extension ext ⇒
    342     match ext with
    343     [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
    344     | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
    345     | ertl_st_ext_frame_size r l ⇒
    346       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
    347         〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     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〉
     373  ].
     374
     375lemma Sm_leq_n_m_leq_n:
     376  ∀m, n: nat.
     377    S m ≤ n → m ≤ n.
     378  #m #n /2/
     379qed.
     380
     381let rec fold_aux
     382  (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
     383    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝
     384  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
     385  [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
     386    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
     387    [ Leaf l      ⇒ λproof. f path l seed
     388    | Stub s      ⇒ λproof. seed
     389    | Node n' l r ⇒ λabsrd. ⊥
     390    ] (refl … 0)
     391  | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
     392    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
     393    [ Leaf l      ⇒ λabsrd. ⊥
     394    | Stub s      ⇒ λproof. seed
     395    | Node n'' l r ⇒ λproof.
     396        fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉)
     397    ] (refl … (S n'))
     398  ].
     399  [ 1, 2: destruct(absrd)
     400  | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
     401  | 4,7: destruct(proof) %
     402  | 5,6: @Sm_leq_n_m_leq_n // ]
     403qed.
     404
     405definition bvt_fold ≝
     406  λa, b: Type[0].
     407  λf: label → a → b → b.
     408  λtrie: BitVectorTrie a 16.
     409  λseed: b.
     410    let f' ≝ λbv: BitVector 16. λa. λb.
     411      f (an_identifier LabelTag bv) a b
     412    in
     413      fold_aux a b f' seed 16 ? trie [[]].
     414  //
     415qed.
     416
     417definition graph_fold ≝
     418  λglobals.
     419  λb : Type[0].
     420  λf    : label → ertl_statement globals → b → b.
     421  λgraph: graph (ertl_statement globals).
     422  λseed : b.
     423  match graph with
     424  [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed
     425  ]. 
     426
     427definition translate_internal: ∀globals: list ident.
     428  ertl_internal_function globals → ltl_internal_function globals ≝
     429  λglobals: list ident.
     430  λint_fun: ertl_internal_function globals.
     431  let graph ≝ (empty_map … : ltl_statement_graph globals) in
     432  let valuation ≝ analyse globals int_fun in
     433  let coloured_graph ≝ build valuation in
     434  let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
     435    let 〈graph, luniv〉 ≝ graph_luniv in
     436      match eliminable globals (valuation label) stmt with
     437      [ Some successor ⇒ 〈add_graph globals label (GOTO … successor) graph, luniv〉
     438      | None           ⇒
     439        translate_statement globals int_fun valuation coloured_graph graph stmt label
     440      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
     441  in
     442    match joint_if_entry … int_fun with
     443    [ dp entry_label entry_label_prf ⇒
     444      match joint_if_exit … int_fun with
     445      [ dp exit_label exit_label_prf ⇒
     446          mk_joint_internal_function globals (ltl_params globals)
     447            luniv (joint_if_runiverse … int_fun)
     448              it it it (joint_if_stacksize … int_fun)
     449                graph ? ?
     450      ]
     451    ].
     452  [1: %
     453    [1: @entry_label
     454    |2: cases daemon (* XXX *)
    348455    ]
    349   ].
    350 
    351 definition translate_internal ≝
    352   λglobals: list ident.
    353   λf.
    354   λint_fun: ertl_internal_function.
    355   let lookup ≝ λr.
    356     match lookup r with
    357     | colour_spill ->
    358         ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    359     | colour_colour color ->
    360         ERTLToLTLI.Color color
    361   in
    362   let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
    363   let stacksize ≝ (ertl_if_params int_fun) + locals in
    364     mk_ltl_internal_function
    365       globals
    366       (ertl_if_luniverse int_fun)
    367       (ertl_if_runiverse int_fun)
    368       stacksize.
    369 
    370   let () =
    371     Label.Map.iter (fun label stmt ->
    372       let stmt =
    373         match Liveness.eliminable (G.liveafter label) stmt with
    374         | Some successor ->
    375             LTL.St_skip successor
    376         | None ->
    377             I.translate_statement stmt
    378       in
    379       graph := Label.Map.add label stmt !graph
    380     ) int_fun.ERTL.f_graph
    381   in
    382 
    383 definition translate_funct ≝
    384   λname_def.
    385   let 〈name, def〉 ≝ name_def in
    386   let def' ≝
    387     match def with
    388     [ Internal def ⇒ Internal ? (translate_internal name def)
    389     | External def ⇒ External ? def
     456  |2: %
     457    [1: @exit_label
     458    |2: cases daemon (* XXX *)
    390459    ]
    391   in
    392     〈name, def'〉.
    393 
    394 definition translate ≝
    395   λp.
    396   let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
    397     mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
     460  ]
     461qed.
     462
     463definition ertl_to_ltl: ertl_program → ltl_program ≝
     464  λp.transform_program … p (transf_fundef … (translate_internal …)).
Note: See TracChangeset for help on using the changeset viewer.