Changeset 1160


Ignore:
Timestamp:
Aug 31, 2011, 12:30:27 PM (8 years ago)
Author:
mulligan
Message:

changes to unfunctorised code in ertltoltl.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1154 r1160  
    11include "ERTL/ERTL.ma".
    2 include "ERTL/ERTLToLTLI.ma".
    32include "LTL/LTL.ma".
    43include "ERTL/spill.ma".
    5 
    6 include "ERTL/ERTL.ma".
    7 include "LTL/LTL.ma".
    84include "ASM/Arithmetic.ma".
    95
     
    1511 
    1612axiom lookup: register → decision.
    17 axiom generate: ∀globals: list ident. ltl_statement globals → label.
    18 axiom fresh_label: ∀globals: list ident. ltl_function_definition globals → ltl_function_definition globals × label.
    19 axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals.
    20 axiom num_locals: nat.
     13
     14definition fresh_label ≝
     15  λglobals: list ident.
     16  λluniv.
     17    fresh LabelTag luniv.
     18
     19definition add_graph ≝
     20  λglobals.
     21  λlabel.
     22  λstmt: ltl_statement globals.
     23  λgraph: ltl_statement_graph globals.
     24    add LabelTag ? graph label stmt.
     25
     26definition generate ≝
     27  λglobals: list ident.
     28  λluniv.
     29  λgraph: ltl_statement_graph globals.
     30  λstmt: ltl_statement globals.
     31  let 〈l, luniv〉 ≝ fresh_label globals luniv in
     32  let graph ≝ add_graph globals l stmt graph in
     33    〈l, 〈graph, luniv〉〉.
    2134
    2235definition num_locals ≝
     
    2942
    3043definition adjust_off ≝
     44  λint_fun.
    3145  λoff.
    3246  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
    33   let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? num_locals) int_off false in
     47  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals int_fun)) int_off false in
    3448    sub.
    3549
    3650definition get_stack ≝
    37   λglobals.
     51  λint_fun.
     52  λglobals.
     53  λgraph: graph (ltl_statement (globals)).
    3854  λr.
    3955  λoff.
    4056  λl.
    41     let off ≝ adjust_off off in
    42     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
    43     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
    44     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    45     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    46     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    47     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    48     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    49       joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
     57    let off ≝ adjust_off int_fun off in
     58    let luniv ≝ ertl_if_luniverse int_fun in
     59    let 〈l, 〈graph, luniv〉〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     60    let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
     61    let 〈l, graph〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     62    let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     63    let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     64    let 〈l, graph〉 ≝ generate globals (ertl_if_luniverse int_fun) graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     65    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     66      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉.
    5067
    5168definition set_stack ≝
    52   λglobals.
     69  λint_fun.
     70  λglobals.
     71  λgraph: graph (ltl_statement (globals)).
    5372  λoff.
    5473  λr.
    5574  λl.
    56   let off ≝ adjust_off off in
    57   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
    58   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
    59   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    60   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    61   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    62   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    63   let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    64     joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
     75  let off ≝ adjust_off int_fun off in
     76  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
     77  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
     78  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     79  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     80  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     81  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     82  let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     83    〈joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l, graph〉.
    6584
    6685definition write ≝
    67   λglobals.
     86  λint_fun.
     87  λglobals.
     88  λgraph: graph (ltl_statement (globals)).
    6889  λr: register.
    6990  λl: label.
    7091  match lookup r with
    71   [ decision_spill off ⇒ 〈RegisterSST, generate globals (set_stack globals off RegisterSST l)〉
    72   | decision_colour hwr ⇒ 〈hwr, l〉
     92  [ decision_spill off ⇒
     93    let 〈stmt, graph〉 ≝ set_stack int_fun globals graph off RegisterSST l in
     94      〈RegisterSST, generate globals graph stmt〉
     95  | decision_colour hwr ⇒ 〈hwr, 〈l, graph〉〉
    7396  ].
    7497
    7598definition read ≝
    76   λglobals.
     99  λint_fun.
     100  λglobals.
     101  λgraph: graph (ltl_statement (globals)).
    77102  λr: register.
    78103  λstmt: Register → ltl_statement globals.
    79104  match lookup r with
    80   [ decision_colour hwr ⇒ generate globals (stmt hwr)
     105  [ decision_colour hwr ⇒ generate globals graph (stmt hwr)
    81106  | decision_spill off ⇒
    82107    let temphwr ≝ RegisterSST in
    83     let l ≝ generate globals (stmt temphwr) in
    84       generate globals (get_stack globals temphwr off l)
     108    let 〈l, graph〉 ≝ generate globals graph (stmt temphwr) in
     109    let 〈stmt, graph〉 ≝ get_stack int_fun globals graph temphwr off l in
     110      generate globals graph stmt
    85111  ].
    86112
    87113definition move ≝
    88   λglobals: list ident.
     114  λint_fun.
     115  λglobals: list ident.
     116  λgraph: graph (ltl_statement globals).
    89117  λdest: decision.
    90118  λsrc: decision.
     
    95123    [ decision_colour src_hwr ⇒
    96124      if eq_Register dest_hwr src_hwr then
    97         joint_st_goto ? globals l
     125        〈joint_st_goto ? globals l, graph〉
    98126      else
    99         let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
    100           joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
    101     | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
     127        let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
     128          〈joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l, graph〉
     129    | decision_spill src_off ⇒ get_stack int_fun globals graph dest_hwr src_off l
    102130    ]
    103131  | decision_spill dest_off ⇒
    104132    match src with
    105     [ decision_colour src_hwr ⇒ set_stack globals dest_off src_hwr l
     133    [ decision_colour src_hwr ⇒ set_stack int_fun globals graph dest_off src_hwr l
    106134    | decision_spill src_off ⇒
    107135      if eq_bv ? dest_off src_off then
    108         joint_st_goto ? globals l
     136        〈joint_st_goto ? globals l, graph〉
    109137      else
    110138        let temp_hwr ≝ RegisterSST in
    111         let l ≝ generate globals (set_stack globals dest_off temp_hwr l) in
    112           get_stack globals temp_hwr src_off l
     139        let 〈stmt, graph〉 ≝ set_stack int_fun globals graph dest_off temp_hwr l in
     140        let 〈l, graph〉 ≝ generate globals graph stmt in
     141          get_stack int_fun globals graph temp_hwr src_off l
    113142    ]
    114143  ].
    115144
    116145definition newframe ≝
    117   λglobals.
     146  λint_fun.
     147  λglobals.
     148  λgraph: graph (ltl_statement globals).
    118149  λl.
    119   if eq_nat stacksize 0 then
    120     joint_st_goto ? globals l
     150  if eq_nat (stacksize int_fun) 0 then
     151    〈joint_st_goto ? globals l, graph〉
    121152  else
    122     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    123     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
    124     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
    125     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
    126     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    127     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
    128     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
    129     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
    130       joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
     153    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     154    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
     155    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
     156    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
     157    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     158    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
     159    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
     160    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
     161      〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph〉.
    131162
    132163definition delframe ≝
    133   λglobals.
     164  λint_fun.
     165  λglobals.
     166  λgraph: graph (ltl_statement globals).
    134167  λl.
    135   if eq_nat stacksize 0 then
    136     joint_st_goto ? globals l
     168  if eq_nat (stacksize int_fun) 0 then
     169    〈joint_st_goto ? globals l, graph〉
    137170  else
    138     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    139     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    140     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    141     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    142     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    143       joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
     171    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     172    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     173    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     174    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     175    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     176      〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉.
    144177
    145178definition translate_statement ≝
    146   λglobals: list ident.
     179  λint_fun.
     180  λglobals: list ident.
     181  λgraph: graph (ltl_statement globals).
    147182  λstmt: ertl_statement.
    148183  match stmt with
    149   [ ertl_st_skip l ⇒ joint_st_goto ? globals l
    150   | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
    151   | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
    152   | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
    153   | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
     184  [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉
     185  | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
     186  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
     187  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
     188  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
    154189  | ertl_st_hdw_to_hdw r1 r2 l ⇒
    155     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
    156       joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
    157   | ertl_st_new_frame l ⇒ newframe globals l
    158   | ertl_st_del_frame l ⇒ delframe globals l
     190    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
     191      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
     192  | ertl_st_new_frame l ⇒ newframe int_fun globals graph l
     193  | ertl_st_del_frame l ⇒ delframe int_fun globals graph l
    159194  | ertl_st_frame_size r l ⇒
    160     let 〈hdw, l〉 ≝ write globals r l in
    161       joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
     195    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     196    let 〈l, graph〉 ≝ l in
     197      〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉
    162198  | ertl_st_pop r l ⇒
    163     let 〈hdw, l〉 ≝ write globals r l in
    164     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    165       joint_st_sequential ? globals (joint_instr_pop globals) l
     199    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     200    let 〈l, graph〉 ≝ l in
     201    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     202      〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉
    166203  | ertl_st_push r l ⇒
    167     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
    168     let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    169       joint_st_goto ? globals l
     204    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in
     205    let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     206      〈joint_st_goto ? globals l, graph〉
    170207  | ertl_st_addr rl rh x l ⇒
    171     let 〈hdw1, l〉 ≝ write globals rh l in
    172     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
    173     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    174     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
    175     let 〈hdw2, l〉 ≝ write globals rl l in
    176     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
    177     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
    178       joint_st_sequential ? globals (joint_instr_address globals x ?) l
     208    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
     209    let 〈l, graph〉 ≝ l in
     210    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
     211    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
     212    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
     213    let 〈hdw2, l〉 ≝ write int_fun globals graph rl l in
     214    let 〈l, graph〉 ≝ l in
     215    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
     216    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
     217      〈joint_st_sequential ? globals (joint_instr_address globals x ?) l, graph〉
    179218(*  | ertl_st_addr_h r x l ⇒
    180     let 〈hdw, l〉 ≝ write globals r l in
    181     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    182     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
     219    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     220    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     221    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
    183222      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    184223  | ertl_st_addr_l r x l ⇒
    185     let 〈hdw, l〉 ≝ write globals r l in
    186     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    187     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
     224    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     225    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     226    let 〈l, graph〉 ≝ generate globals graph (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
    188227      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    189228*)
    190229  | ertl_st_int r i l ⇒
    191     let 〈hdw, l〉 ≝ write globals r l in
    192       joint_st_sequential ? globals (joint_instr_int globals hdw i) l
    193   | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
     230    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     231    let 〈l, graph〉 ≝ l in
     232      〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉
     233  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
    194234  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
    195     let 〈hdw, l〉 ≝ write globals destr1 l in
    196     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    197     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    198     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    199     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    200     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    201     let l ≝ generate globals (joint_st_goto ? globals l) in
    202     let 〈hdw, l〉 ≝ write globals destr2 l in
    203     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    204     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    205     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    206     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    207     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    208     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    209       joint_st_goto ? globals l
     235    let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in
     236    let 〈l, graph〉 ≝ l in
     237    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     238    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     239    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     240    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     241    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     242    let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in
     243    let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in
     244    let 〈l, graph〉 ≝ l in
     245    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     246    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     247    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     248    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     249    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     250    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     251      〈joint_st_goto ? globals l, graph〉
    210252(*
    211253  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    212     let 〈hdw, l〉 ≝ write globals destr l in
    213     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    214     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    215     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    216     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    217     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     254    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
     255    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     256    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     257    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     258    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     259    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    218260      joint_st_goto ? globals l
    219261  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    220     let 〈hdw, l〉 ≝ write globals destr l in
    221     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    222     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    223     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    224     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    225     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    226     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     262    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
     263    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     264    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     265    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     266    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     267    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     268    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    227269      joint_st_goto ? globals l
    228270*)
    229271  | ertl_st_op1 op1 destr srcr l ⇒
    230     let 〈hdw, l〉 ≝ write globals destr l in
    231     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    232     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    233     let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    234       joint_st_goto ? globals l
     272    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
     273    let 〈l, graph〉 ≝ l in
     274    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     275    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
     276    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     277      〈joint_st_goto ? globals l, graph〉
    235278  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    236     let 〈hdw, l〉 ≝ write globals destr l in
    237     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    238     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
    239     let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    240     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    241     let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    242       joint_st_goto ? globals l
    243   | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
    244   | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
     279    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
     280    let 〈l, graph〉 ≝ l in
     281    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     282    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
     283    let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     284    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     285    let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     286      〈joint_st_goto ? globals l, graph〉
     287  | ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉
     288  | ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉
    245289  | ertl_st_load destr addr1 addr2 l ⇒
    246     let 〈hdw, l〉 ≝ write globals destr l in
    247     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    248     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
    249     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    250     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    251     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    252     let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    253     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    254     let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    255       joint_st_goto ? globals l
     290    let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
     291    let 〈l, graph〉 ≝ l in
     292    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     293    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
     294    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     295    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     296    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     297    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     298    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     299    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     300      〈joint_st_goto ? globals l, graph〉
    256301  | ertl_st_store addr1 addr2 srcr l ⇒
    257     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
    258     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
    259     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    260     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    261     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    262     let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    263     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    264     let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    265     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    266     let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    267       joint_st_goto ? globals l
    268   | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
     302    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
     303    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
     304    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     305    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     306    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     307    let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     308    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     309    let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     310    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
     311    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     312      〈joint_st_goto ? globals l, graph〉
     313  | ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉
    269314  | ertl_st_cond srcr lbl_true lbl_false ⇒
    270     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    271     let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    272       joint_st_goto ? globals l
    273   | ertl_st_return ⇒ joint_st_return ? globals
     315    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
     316    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     317      〈joint_st_goto ? globals l, graph〉
     318  | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉
    274319  ].
    275320  cases daemon (* XXX: todo -- proofs regarding gvars *)
Note: See TracChangeset for help on using the changeset viewer.