Changeset 1138 for src/ERTL


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

merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1136 r1138  
    2727  | ertl_st_int: register → Byte → label → ertl_statement
    2828  | ertl_st_move: register → register → label → ertl_statement
     29  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
     30(* XXX: changed from O'Caml
    2931  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    3032  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     33*)
    3134  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    3235  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
  • src/ERTL/ERTLToLTLI.ma

    r1136 r1138  
    180180      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
     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(*
    182199  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
    183200    let 〈hdw, l〉 ≝ write globals destr l in
     
    197214    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    198215      joint_st_goto ? globals l
     216*)
    199217  | ertl_st_op1 op1 destr srcr l ⇒
    200218    let 〈hdw, l〉 ≝ write globals destr l in
Note: See TracChangeset for help on using the changeset viewer.