Ignore:
Timestamp:
Aug 29, 2011, 6:01:41 PM (8 years ago)
Author:
mulligan
Message:

fixed ertl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLI.ma

    r1131 r1136  
    2828  λl.
    2929    let off ≝ adjust_off off in
    30     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l)) in
    31     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_load globals) l)) in
    32     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
    33     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
    34     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
    35     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
    36     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
    37       (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l)).
     30    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     31    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
     32    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     33    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     34    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     35    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     36    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     37      joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
    3838
    3939definition set_stack ≝
     
    4343  λl.
    4444  let off ≝ adjust_off off in
    45   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_store globals) l)) in
    46   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l)) in
    47   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
    48   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
    49   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
    50   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
    51   let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
    52     (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l)).
     45  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     46  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
     47  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     48  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     49  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     50  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     51  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     52    joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
    5353
    5454definition write ≝
     
    8383    [ decision_colour src_hwr ⇒
    8484      if eq_Register dest_hwr src_hwr then
    85         ltl_st_skip globals l
     85        joint_st_goto ? globals l
    8686      else
    87         let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l)) in
    88           (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l))
     87        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
     88          joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
    8989    | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
    9090    ]
     
    9494    | decision_spill src_off ⇒
    9595      if eq_bv ? dest_off src_off then
    96         ltl_st_skip globals l
     96        joint_st_goto ? globals l
    9797      else
    9898        let temp_hwr ≝ RegisterSST in
     
    106106  λl.
    107107  if eq_nat stacksize 0 then
    108     ltl_st_skip globals l
     108    joint_st_goto ? globals l
    109109  else
    110     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l)) in
    111     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l)) in
    112     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l)) in
    113     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l)) in
    114     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l)) in
    115     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l)) in
    116     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l)) in
    117     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l)) in
    118       (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l)).
     110    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     111    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
     112    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
     113    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
     114    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     115    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
     116    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
     117    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
     118      joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
    119119
    120120definition delframe ≝
     
    122122  λl.
    123123  if eq_nat stacksize 0 then
    124     ltl_st_skip globals l
     124    joint_st_goto ? globals l
    125125  else
    126     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l)) in
    127     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l)) in
    128     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l)) in
    129     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l)) in
    130     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l)) in
    131       (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l)).
     126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     127    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     128    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     129    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     130    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     131      joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
    132132
    133133definition translate_statement ≝
     
    135135  λstmt: ertl_statement.
    136136  match stmt with
    137   [ ertl_st_skip l ⇒ ltl_st_skip globals l
    138   | ertl_st_comment s l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_comment globals s) l)
    139   | ertl_st_cost cost_lbl l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l)
     137  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
     138  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
     139  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
    140140  | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
    141141  | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
    142142  | ertl_st_hdw_to_hdw r1 r2 l ⇒
    143     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l)) in
    144       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals r2) l)
     143    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
     144      joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
    145145  | ertl_st_new_frame l ⇒ newframe globals l
    146146  | ertl_st_del_frame l ⇒ delframe globals l
    147147  | ertl_st_frame_size r l ⇒
    148148    let 〈hdw, l〉 ≝ write globals r l in
    149       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l)
     149      joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
    150150  | ertl_st_pop r l ⇒
    151151    let 〈hdw, l〉 ≝ write globals r l in
    152     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    153       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_pop globals) l)
     152    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     153      joint_st_sequential ? globals (joint_instr_pop globals) l
    154154  | ertl_st_push r l ⇒
    155     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_push globals) l)) in
    156     let l ≝ read globals r (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    157       ltl_st_skip globals l
     155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
     156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     157      joint_st_goto ? globals l
    158158  | ertl_st_addr rl rh x l ⇒
    159159    let 〈hdw1, l〉 ≝ write globals rh l in
    160     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l)) in
    161     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
    162     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)) in
     160    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
     161    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
     162    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
    163163    let 〈hdw2, l〉 ≝ write globals rl l in
    164     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l)) in
    165     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
    166       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     164    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
     165    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
     166      joint_st_sequential ? globals (joint_instr_address globals x ?) l
    167167(*  | ertl_st_addr_h r x l ⇒
    168168    let 〈hdw, l〉 ≝ write globals r l in
     
    178178  | ertl_st_int r i l ⇒
    179179    let 〈hdw, l〉 ≝ write globals r l in
    180       ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_int globals hdw i) l)
     180      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
    181181  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
    182182  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    183183    let 〈hdw, l〉 ≝ write globals destr l in
    184     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    185     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l)) in
    186     let l ≝ read globals srcr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    187     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l)) in
    188     let l ≝ read globals srcr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    189       ltl_st_skip globals l
     184    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     185    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     186    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     187    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     188    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     189      joint_st_goto ? globals l
    190190  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    191191    let 〈hdw, l〉 ≝ write globals destr l in
    192     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    193     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l)) in
    194     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l)) in
    195     let l ≝ read globals srcr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    196     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l)) in
    197     let l ≝ read globals srcr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    198       ltl_st_skip globals l
     192    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     193    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     194    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     195    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     196    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     197    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     198      joint_st_goto ? globals l
    199199  | ertl_st_op1 op1 destr srcr l ⇒
    200200    let 〈hdw, l〉 ≝ write globals destr l in
    201     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    202     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l)) in
    203     let l ≝ read globals srcr (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    204       ltl_st_skip globals l
     201    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     202    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
     203    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     204      joint_st_goto ? globals l
    205205  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    206206    let 〈hdw, l〉 ≝ write globals destr l in
    207     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    208     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l)) in
    209     let l ≝ read globals srcr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    210     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l)) in
    211     let l ≝ read globals srcr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    212       ltl_st_skip globals l
    213   | ertl_st_clear_carry l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l)
    214   | ertl_st_set_carry l ⇒ ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_set_carry globals) l)
     207    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     208    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
     209    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     210    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     211    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     212      joint_st_goto ? globals l
     213  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
     214  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
    215215  | ertl_st_load destr addr1 addr2 l ⇒
    216216    let 〈hdw, l〉 ≝ write globals destr l in
    217     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
    218     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_load globals) l)) in
    219     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
    220     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l)) in
    221     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
    222     let l ≝ read globals addr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    223     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l)) in
    224     let l ≝ read globals addr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    225       ltl_st_skip globals l
     217    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     218    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
     219    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     221    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     222    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     223    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     224    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     225      joint_st_goto ? globals l
    226226  | ertl_st_store addr1 addr2 srcr l ⇒
    227     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_store globals) l)) in
    228     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l)) in
    229     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l)) in
    230     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l)) in
    231     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l)) in
    232     let l ≝ read globals addr1 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    233     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l)) in
    234     let l ≝ read globals addr2 (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    235     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l)) in
    236     let l ≝ read globals srcr (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    237       ltl_st_skip globals l
    238   | ertl_st_call_id f ignore l ⇒  ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_call_id globals f) l)
     227    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     228    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
     229    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     230    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     231    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     232    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     233    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     234    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     235    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
     236    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     237      joint_st_goto ? globals l
     238  | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
    239239  | ertl_st_cond srcr lbl_true lbl_false ⇒
    240     let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false)) in
    241     let l ≝ read globals srcr (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    242       ltl_st_skip globals l
    243   | ertl_st_return ⇒ ltl_st_lift globals (joint_st_return ? globals)
     240    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
     241    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     242      joint_st_goto ? globals l
     243  | ertl_st_return ⇒ joint_st_return ? globals
    244244  ].
    245245  cases daemon (* XXX: todo -- proofs regarding gvars *)
Note: See TracChangeset for help on using the changeset viewer.