Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 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 deleted
6 edited
1 copied

Legend:

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

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

    r1197 r1311  
    1 include "ASM/I8051.ma".
    21include "joint/Joint.ma".
    3 include "utilities/BitVectorTrieSet.ma".
    4 include "utilities/IdentifierTools.ma".
    5 include "common/Graphs.ma".
    6 include "common/CostLabel.ma".
    7 include "common/Registers.ma".
    8 
    9 definition registers ≝ list register.
    102
    113inductive move_registers: Type[0] ≝
     
    146                 
    157inductive ertl_statement_extension: Type[0] ≝
    16   | ertl_st_ext_new_frame: label → ertl_statement_extension
    17   | ertl_st_ext_del_frame: label → ertl_statement_extension
    18   | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
     8  | ertl_st_ext_new_frame: ertl_statement_extension
     9  | ertl_st_ext_del_frame: ertl_statement_extension
     10  | ertl_st_ext_frame_size: register → ertl_statement_extension.
    1911
    20 definition ertl_params: params ≝
    21  mk_params
    22    register register register register
    23      (move_registers × move_registers) register
    24        ertl_statement_extension unit (list register) nat.
     12definition ertl_params__: params__ ≝
     13 mk_params__ register register register register (move_registers × move_registers)
     14  register nat unit ertl_statement_extension.
     15definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
     16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
     17definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
     18definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
    2519
    26 definition ertl_statement ≝ joint_statement ertl_params.
     20definition ertl_statement ≝ joint_statement ertl_params_.
    2721
    28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
     22definition ertl_internal_function ≝
     23  λglobals.joint_internal_function … (ertl_params globals).
    2924
    30 record ertl_internal_function (globals: list ident): Type[0] ≝
    31 {
    32   ertl_if_luniverse: universe LabelTag;
    33   ertl_if_runiverse: universe RegisterTag;
    34   ertl_if_params: nat;
    35   ertl_if_locals: registers;
    36   ertl_if_stacksize: nat;
    37   ertl_if_graph: ertl_statement_graph globals;
    38   ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    39   ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    40 }.
    41 
    42 definition set_luniverse ≝
    43   λglobals  : list ident.
    44   λint_fun  : ertl_internal_function globals.
    45   λluniverse: universe LabelTag.
    46   let runiverse ≝ ertl_if_runiverse globals int_fun in
    47   let params    ≝ ertl_if_params globals int_fun in
    48   let locals    ≝ ertl_if_locals globals int_fun in
    49   let stacksize ≝ ertl_if_stacksize globals int_fun in
    50   let graph     ≝ ertl_if_graph globals int_fun in
    51   let entry     ≝ ertl_if_entry globals int_fun in
    52   let exit      ≝ ertl_if_exit globals int_fun in
    53     mk_ertl_internal_function globals
    54       luniverse runiverse params locals
    55       stacksize graph entry exit.
    56 
    57 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    58  
    59 record ertl_program (globals: list ident): Type[0] ≝
    60 {
    61   ertl_pr_vars: list (ident × nat);
    62   ertl_pr_funcs: list (ident × (ertl_function globals));
    63   ertl_pr_main: option ident
    64 }.
    65 
    66 
    67 (* XXX: changed from O'Caml
    68   | ertl_st_addr_h: register → ident → label → ertl_statement
    69   | ertl_st_addr_l: register → ident → label → ertl_statement
    70 *)
    71 
    72 (* XXX: changed from O'Caml
    73   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    74   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    75 *)
     25definition ertl_program ≝ joint_program ertl_params.
  • 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 …)).
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1197 r1311  
    11include "ASM/Util.ma".
    22include "ERTL/ERTL.ma".
    3 
    4 definition list_set_union ≝
    5   λA: Type[0].
    6   λeq_a: A → A → bool.
    7   λl: list A.
    8   λr: list A.
    9     nub_by A eq_a (l @ r).
    10 
    11 definition list_set_add ≝
    12   λA: Type[0].
    13   λeq_a: A → A → bool.
    14   λa: A.
    15   λs: list A.
    16     nub_by A eq_a (a :: s).
    17 
    18 definition list_set_diff ≝
    19   λA: Type[0].
    20   λeq_a: A → A → bool.
    21   λl: list A.
    22   λr: list A.
    23     filter A (λx. member A eq_a x r) l.
    24 
    25 definition list_set_equal ≝
    26   λA: Type[0].
    27   λeq_a: A → A → bool.
    28   λl: list A.
    29   λr: list A.
    30     foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    31 
    32 definition list_set_member ≝ member.
    33 
    34 definition list_set_fold ≝ foldr.
     3include "utilities/adt/set_adt.ma".
    354
    365definition statement_successors ≝
     
    387  λs: ertl_statement globals.
    398  match s with
    40   [ joint_st_sequential seq l ⇒
    41     match seq with
    42     [ joint_instr_cond acc_a_reg lbl_true ⇒
    43         list_set_add ? (eq_identifier ?) lbl_true [ l ]
    44     | _ ⇒ [ l ]
    45     ]
    46   | joint_st_extension ext ⇒
    47     match ext with
    48     [ ertl_st_ext_new_frame l ⇒ [ l ]
    49     | ertl_st_ext_del_frame l ⇒ [ l ]
    50     | ertl_st_ext_frame_size r l ⇒ [ l ]
    51     ]
    52   | joint_st_goto l ⇒ [ l ]
    53   | joint_st_return ⇒ [ ]
    54   ].
    55 
    56 definition register_lattice ≝ (list register) × (list Register).
     9  [ sequential seq l ⇒
     10    match seq with
     11    [ COND acc_a_reg lbl_true ⇒
     12        set_insert … lbl_true (set_singleton … l)
     13    | _ ⇒ set_singleton … l ]
     14  | GOTO l ⇒ set_singleton … l
     15  | RETURN ⇒ set_empty ?
     16  ].
     17
     18definition register_lattice ≝ (set register) × (set Register).
    5719definition lattice_property ≝ register_lattice.
    58 definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
     20definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
    5921definition lattice_psingleton: register → register_lattice ≝
    6022  λr.
    61     〈[ r ], [ ]〉.
     23    〈set_singleton … r, set_empty …〉.
    6224definition lattice_hsingleton: Register → register_lattice ≝
    6325  λr.
    64     〈[ ], [ r ]〉.
     26    〈set_empty …, set_singleton … r〉.
    6527
    6628definition lattice_join: register_lattice → register_lattice → register_lattice ≝
     
    6931  let 〈lp, lh〉 ≝ left in
    7032  let 〈rp, rh〉 ≝ right in
    71     〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
     33    〈set_union … lp rp, set_union … lh rh〉.
    7234
    7335definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
     
    7638  let 〈lp, lh〉 ≝ left in
    7739  let 〈rp, rh〉 ≝ right in
    78     〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
     40    〈set_diff … lp rp, set_diff … lh rh〉.
    7941
    8042definition lattice_equal: register_lattice → register_lattice → bool ≝
     
    8345  let 〈lp, lh〉 ≝ left in
    8446  let 〈rp, rh〉 ≝ right in
    85     andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
     47    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
    8648
    8749definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
     
    10264definition property ≝
    10365  mk_lattice_property_sig
    104     ((list register) × (list Register))
     66    ((set register) × (set Register))
    10567    lattice_property
    10668    lattice_bottom
     
    11678  λs: ertl_statement globals.
    11779  match s with
    118   [ joint_st_sequential seq l ⇒
    119     match seq with
    120     [ joint_instr_op2 op2 r _ ⇒
     80  [ sequential seq l ⇒
     81    match seq with
     82    [ OP2 op2 r1 r2 _ ⇒
    12183      match op2 with
    122       [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    123       | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    124       | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    125       | _ ⇒ lattice_psingleton r
    126       ]
    127     | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    128     | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    129     | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    130     | joint_instr_op1 op1 r ⇒ lattice_psingleton r
    131     | joint_instr_pop r ⇒ lattice_psingleton r
    132     | joint_instr_int r _ ⇒ lattice_psingleton r
    133     | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    134     | joint_instr_load r _ _ ⇒ lattice_psingleton r
     84      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     85      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     86      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry)  (lattice_psingleton r1)
     87      | _ ⇒ lattice_psingleton r1
     88      ]
     89    | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
     90    | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
     91    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     92       lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
     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
    13598    (* Potentially destroys all caller-save hardware registers. *)
    136     | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉
    137     | joint_instr_comment c ⇒ lattice_bottom
    138     | joint_instr_cond r lbl_true ⇒ lattice_bottom
    139     | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
    140     | joint_instr_cost_label clabel ⇒ lattice_bottom
    141     | joint_instr_push r ⇒ lattice_bottom
    142     | 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 ⇒
    143106      (* first register relevant only *)
    144107      let r1 ≝ \fst pair_reg in
     
    147110      | hardware h ⇒ lattice_hsingleton h
    148111      ]
    149     ]
    150   | joint_st_return ⇒ lattice_bottom
    151   | joint_st_extension ext ⇒
    152     match ext with
    153     [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    154     | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    155     | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
    156     ]
    157   | joint_st_goto l ⇒ lattice_bottom
    158   ].
    159 
    160 definition list_set_of_list ≝
    161   λrl.
    162     foldr ? ? (list_set_add Register eq_Register) rl [ ].
    163 
    164 definition list_set_of_list2 ≝
    165   let f ≝ λset. λr. list_set_add Register eq_Register r set in
    166     foldl ? ? f [ ].
    167 
    168 definition ret_regs ≝ list_set_of_list RegisterRets.
     112    | extension ext ⇒
     113      match ext with
     114      [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     115      | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     116      | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
     117  | RETURN ⇒ lattice_bottom
     118  | GOTO l ⇒ lattice_bottom
     119  ].
     120
     121definition ret_regs ≝ set_from_list … RegisterRets.
    169122
    170123definition used ≝
     
    172125  λs: ertl_statement globals.
    173126  match s with
    174   [ joint_st_sequential seq l ⇒
    175     match seq with
    176     [ joint_instr_op2 op2 acc_a r
     127  [ sequential seq l ⇒
     128    match seq with
     129    [ OP2 op2 acc_a r1 r2
    177130      match op2 with
    178131      [ Addc ⇒
    179         lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
    180       | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
    181       ]
    182     | joint_instr_clear_carry ⇒ lattice_bottom
    183     | joint_instr_set_carry ⇒ lattice_bottom
     132        lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
     133      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     134      ]
     135    | CLEAR_CARRY ⇒ lattice_bottom
     136    | SET_CARRY ⇒ lattice_bottom
    184137    (* acc_a and acc_b *)
    185     | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    186     | joint_instr_op1 op1 r ⇒ lattice_psingleton r
    187     | joint_instr_pop r ⇒ lattice_bottom
    188     | joint_instr_int r _ ⇒ lattice_bottom
    189     | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
    190     | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
     138    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     139       lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
     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)
    191145    (* Reads the hardware registers that are used to pass parameters. *)
    192     | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉
    193     | joint_instr_comment c ⇒ lattice_bottom
    194     | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
    195     | 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 ⇒
    196150      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
    197     | joint_instr_cost_label clabel ⇒ lattice_bottom
    198     | joint_instr_push r ⇒ lattice_psingleton r
    199     | joint_instr_move pair_reg ⇒
     151    | COST_LABEL clabel ⇒ lattice_bottom
     152    | PUSH r ⇒ lattice_psingleton r
     153    | MOVE pair_reg ⇒
    200154      (* only second reg in pair relevant *)
    201155      let r2 ≝ \snd pair_reg in
     
    204158      | hardware h ⇒ lattice_hsingleton h
    205159      ]
    206     ]
    207   | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    208   | joint_st_goto l ⇒ lattice_bottom
    209   | joint_st_extension ext ⇒
     160  | extension ext ⇒
    210161    match ext with
    211     [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    212     | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    213     | ertl_st_ext_frame_size r l ⇒ lattice_bottom
    214     ]
     162    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     163    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     164    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
     165  | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     166  | GOTO l ⇒ lattice_bottom
    215167  ].
    216168
     
    221173  let 〈pliveafter, hliveafter〉 ≝ l in
    222174  match s with
    223   [ joint_st_sequential seq l ⇒
    224     match seq with
    225     [ joint_instr_op2 op2 acc_a r
    226       if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
    227          list_set_member Register eq_Register RegisterCarry hliveafter then
    228         None ?
    229       else
    230         Some ? l
    231     | joint_instr_clear_carry ⇒ None ?
    232     | joint_instr_set_carry ⇒ None ?
    233     | joint_instr_opaccs opaccs r1 r2 ⇒
    234       if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    235          list_set_member register (eq_identifier ?) r2 pliveafter ∨
    236          list_set_member Register eq_Register RegisterCarry hliveafter then
    237         None ?
    238       else
    239         Some ? l
    240     | joint_instr_op1 op1 r
    241       if list_set_member register (eq_identifier ?) r pliveafter ∨
    242          list_set_member Register eq_Register RegisterCarry hliveafter then
    243         None ?
    244       else
    245         Some ? l
    246     | joint_instr_pop r ⇒ None ?
    247     | joint_instr_int r _ ⇒
    248       if list_set_member register (eq_identifier ?) r pliveafter ∨
    249          list_set_member Register eq_Register RegisterCarry hliveafter then
    250         None ?
    251       else
    252         Some ? l
    253     | joint_instr_address _ _ r1 r2 ⇒
    254       if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    255          list_set_member register (eq_identifier ?) r2 pliveafter ∨
    256          list_set_member Register eq_Register RegisterCarry hliveafter then
    257         None ?
    258       else
    259         Some ? l
    260     | joint_instr_load acc_a dpl dph ⇒
    261       if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
    262          list_set_member Register eq_Register RegisterCarry hliveafter then
    263         None ?
    264       else
    265         Some ? l
    266     | joint_instr_call_id _ nparams ⇒ None ?
    267     | joint_instr_comment c ⇒ None ?
    268     | joint_instr_cond r lbl_true ⇒ None ?
    269     | joint_instr_store acc_a dpl dph ⇒ None ?
    270     | joint_instr_cost_label clabel ⇒ None ?
    271     | joint_instr_push r ⇒ None ?
    272     | joint_instr_move pair_reg ⇒
     175  [ sequential seq l ⇒
     176    match seq with
     177    [ OP2 op2 r1 r2 r3
     178      if set_member … (eq_identifier …) r1 pliveafter ∨
     179         set_member … eq_Register RegisterCarry hliveafter then
     180        None ?
     181      else
     182        Some ? l
     183    | CLEAR_CARRY ⇒ None ?
     184    | SET_CARRY ⇒ None ?
     185    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     186      if set_member … (eq_identifier …) dr1 pliveafter ∨
     187         set_member … (eq_identifier …) dr2 pliveafter ∨
     188         set_member … eq_Register RegisterCarry hliveafter then
     189        None ?
     190      else
     191        Some ? l
     192    | OP1 op1 r1 r2
     193      if set_member … (eq_identifier …) r1 pliveafter ∨
     194         set_member … eq_Register RegisterCarry hliveafter then
     195        None ?
     196      else
     197        Some ? l
     198    | POP r ⇒ None ?
     199    | INT r _ ⇒
     200      if set_member … (eq_identifier …) r pliveafter ∨
     201         set_member … eq_Register RegisterCarry hliveafter then
     202        None ?
     203      else
     204        Some ? l
     205    | ADDRESS _ _ r1 r2 ⇒
     206      if set_member … (eq_identifier …) r1 pliveafter ∨
     207         set_member … (eq_identifier …) r2 pliveafter ∨
     208         set_member … eq_Register RegisterCarry hliveafter then
     209        None ?
     210      else
     211        Some ? l
     212    | LOAD acc_a dpl dph ⇒
     213      if set_member ? (eq_identifier …) acc_a pliveafter ∨
     214         set_member … eq_Register RegisterCarry hliveafter then
     215        None ?
     216      else
     217        Some ? l
     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 ⇒
    273225      let r1 ≝ \fst pair_reg in
    274226      let r2 ≝ \snd pair_reg in
    275227      match r1 with
    276228      [ pseudo p1 ⇒
    277         if list_set_member register (eq_identifier ?) p1 pliveafter ∨
    278            list_set_member Register eq_Register RegisterCarry hliveafter then
     229        if set_member … (eq_identifier …) p1 pliveafter ∨
     230           set_member … eq_Register RegisterCarry hliveafter then
    279231          None ?
    280232        else
    281233          Some ? l
    282234      | hardware h1 ⇒
    283         if list_set_member Register eq_Register h1 hliveafter then
     235        if set_member … eq_Register h1 hliveafter then
    284236          None ?
    285237        else
    286           Some ? l
    287       ]
    288     ]
    289   | joint_st_goto l ⇒ None ?
    290   | joint_st_return ⇒ None ?
    291   | joint_st_extension ext ⇒
    292     match ext with
    293     [ ertl_st_ext_new_frame l ⇒ None ?
    294     | ertl_st_ext_del_frame l ⇒ None ?
    295     | ertl_st_ext_frame_size r l ⇒
    296       if list_set_member register (eq_identifier ?) r pliveafter ∨
    297         list_set_member Register eq_Register RegisterCarry hliveafter then
    298         None ?
    299       else
    300         Some ? l
    301     ]
     238          Some ? l]
     239    | extension ext ⇒
     240      match ext with
     241      [ ertl_st_ext_new_frame ⇒ None ?
     242      | ertl_st_ext_del_frame ⇒ None ?
     243      | ertl_st_ext_frame_size r ⇒
     244        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
     245           set_member ? eq_Register RegisterCarry hliveafter then
     246          None ?
     247        else
     248          Some ? l]]
     249  | GOTO l ⇒ None ?
     250  | RETURN ⇒ None ?
    302251  ].
    303252
     
    319268definition livebefore ≝
    320269  λglobals: list ident.
    321   λint_fun.
     270  λint_fun: ertl_internal_function globals.
    322271  λlabel.
    323272  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph globals int_fun) label with
     273  match lookup … (joint_if_code … int_fun) label with
    325274  [ None      ⇒ ?
    326275  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
     
    330279
    331280definition liveafter ≝
    332   λglobals.
    333   λint_fun.
    334   λlivebefore.
     281  λglobals: list ident.
     282  λint_fun: ertl_internal_function globals.
     283  λlivebefore: label → ?.
    335284  λlabel.
    336285  λliveafter: valuation.
    337   match lookup … (ertl_if_graph globals int_fun) label with
     286  match lookup … (joint_if_code … int_fun) label with
    338287  [ None      ⇒ ?
    339   | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
     288  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    340289      lattice_join (livebefore successor liveafter) accu)
    341       lattice_bottom (statement_successors globals stmt)
     290      (statement_successors globals stmt) lattice_bottom
    342291  ].
    343292  cases not_implemented (* XXX *)
  • Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

    r1197 r1311  
    4949axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    5050
    51 definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).
    5252
    5353(* CSC: frame reduced to this *)
     
    139139
    140140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    141 axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
     141axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).
    142142
    143143definition init_locals : list register → register_env val ≝
     
    191191  (* CSC: monadic notation missing here *)
    192192    bind ?? (fetch_function globals st) (λf.
    193     OK ? (ertl_if_stacksize globals f)).
     193    OK ? (joint_if_stacksize globals … f)).
    194194
    195195definition get_hwsp : state → res address ≝
  • Deliverables/D3.3/id-lookup-branch/ERTL/spill.ma

    r1153 r1311  
    11include "common/AST.ma".
    2 include "utilities/Interference.ma".
     2include "ERTL/Interference.ma".
    33
    44definition decision ≝ Immediate.
Note: See TracChangeset for help on using the changeset viewer.