Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

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

Legend:

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

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

    r1109 r1153  
    8383    [ decision_colour src_hwr ⇒
    8484      if eq_Register dest_hwr src_hwr then
    85         joint_st_sequential ? globals (joint_instr_skip globals) l
     85        joint_st_goto ? globals l
    8686      else
    8787        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
     
    9494    | decision_spill src_off ⇒
    9595      if eq_bv ? dest_off src_off then
    96         joint_st_sequential ? globals (joint_instr_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     joint_st_sequential ? globals (joint_instr_skip globals) l
     108    joint_st_goto ? globals l
    109109  else
    110110    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     
    122122  λl.
    123123  if eq_nat stacksize 0 then
    124     joint_st_sequential ? globals (joint_instr_skip globals) l
     124    joint_st_goto ? globals l
    125125  else
    126126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     
    135135  λstmt: ertl_statement.
    136136  match stmt with
    137   [ ertl_st_skip l ⇒ joint_st_sequential ? globals (joint_instr_skip globals) l
     137  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
    138138  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
    139139  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
     
    155155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
    156156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    157       joint_st_sequential ? globals (joint_instr_skip globals) l
    158   | ertl_st_addr_h r x l ⇒
    159     let 〈hdw, l〉 ≝ write globals r l in
    160     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     157      joint_st_goto ? globals l
     158  | ertl_st_addr rl rh x l ⇒
     159    let 〈hdw1, l〉 ≝ write globals rh l in
     160    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
    161161    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
    162       joint_st_sequential ? globals (joint_instr_address globals x ?) l
    163   | ertl_st_addr_l r x l ⇒
    164     let 〈hdw, l〉 ≝ write globals r l in
    165     let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     162    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
     163    let 〈hdw2, l〉 ≝ write globals rl l in
     164    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
    166165    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
    167166      joint_st_sequential ? globals (joint_instr_address globals x ?) l
     167(*  | ertl_st_addr_h r x l ⇒
     168    let 〈hdw, l〉 ≝ write globals r l in
     169    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     170    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
     171      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     172  | ertl_st_addr_l r x l ⇒
     173    let 〈hdw, l〉 ≝ write globals r l in
     174    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     175    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
     176      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     177*)
    168178  | ertl_st_int r i l ⇒
    169179    let 〈hdw, l〉 ≝ write globals r l in
    170180      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
    171181  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
     182  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
     183    let 〈hdw, l〉 ≝ write globals destr1 l in
     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    let l ≝ generate globals (joint_st_goto ? globals l) in
     190    let 〈hdw, l〉 ≝ write globals destr2 l in
     191    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     192    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     193    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     194    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     195    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     196    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     197      joint_st_goto ? globals l
     198(*
    172199  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    173200    let 〈hdw, l〉 ≝ write globals destr l in
     
    177204    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    178205    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    179       joint_st_sequential ? globals (joint_instr_skip globals) l
     206      joint_st_goto ? globals l
    180207  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
    181208    let 〈hdw, l〉 ≝ write globals destr l in
     
    186213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    187214    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    188       joint_st_sequential ? globals (joint_instr_skip globals) l
     215      joint_st_goto ? globals l
     216*)
    189217  | ertl_st_op1 op1 destr srcr l ⇒
    190218    let 〈hdw, l〉 ≝ write globals destr l in
     
    192220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    193221    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    194       joint_st_sequential ? globals (joint_instr_skip globals) l
     222      joint_st_goto ? globals l
    195223  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    196224    let 〈hdw, l〉 ≝ write globals destr l in
     
    200228    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    201229    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    202       joint_st_sequential ? globals (joint_instr_skip globals) l
     230      joint_st_goto ? globals l
    203231  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
    204232  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
     
    213241    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    214242    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    215       joint_st_sequential ? globals (joint_instr_skip globals) l
     243      joint_st_goto ? globals l
    216244  | ertl_st_store addr1 addr2 srcr l ⇒
    217245    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     
    225253    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    226254    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    227       joint_st_sequential ? globals (joint_instr_skip globals) l
    228   | ertl_st_call_id f ignore l ⇒  joint_st_sequential ? globals (joint_instr_call_id globals f) l
     255      joint_st_goto ? globals l
     256  | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
    229257  | ertl_st_cond srcr lbl_true lbl_false ⇒
    230258    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    231259    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    232       joint_st_sequential ? globals (joint_instr_skip globals) l
     260      joint_st_goto ? globals l
    233261  | ertl_st_return ⇒ joint_st_return ? globals
    234262  ].
Note: See TracChangeset for help on using the changeset viewer.