Changeset 1131 for src/ERTL


Ignore:
Timestamp:
Aug 29, 2011, 5:19:31 PM (9 years ago)
Author:
mulligan
Message:

changes to syntax of ertl: removed ertl_st_addr_l and ertl_st_addr_h in favourn of unified instruction ertl_st_addr

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1107 r1131  
    2020  | ertl_st_pop: register → label → ertl_statement
    2121  | ertl_st_push: register → label → ertl_statement
     22  | ertl_st_addr: register → register → ident → label → ertl_statement
     23(* XXX: changed from O'Caml
    2224  | ertl_st_addr_h: register → ident → label → ertl_statement
    2325  | ertl_st_addr_l: register → ident → label → ertl_statement
     26*)
    2427  | ertl_st_int: register → Byte → label → ertl_statement
    2528  | ertl_st_move: register → register → label → ertl_statement
  • src/ERTL/ERTLToLTLI.ma

    r1128 r1131  
    156156    let l ≝ read globals r (λhdw. ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l)) in
    157157      ltl_st_skip globals l
    158   | ertl_st_addr_h r x l ⇒
     158  | ertl_st_addr rl rh x l ⇒
     159    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
     163    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)
     167(*  | ertl_st_addr_h r x l ⇒
    159168    let 〈hdw, l〉 ≝ write globals r l in
    160169    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     
    166175    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
    167176      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
Note: See TracChangeset for help on using the changeset viewer.