Changeset 1131


Ignore:
Timestamp:
Aug 29, 2011, 5:19:31 PM (8 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
Files:
3 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
  • src/RTL/RTLtoERTL.ma

    r1107 r1131  
    9797  | ertl_st_pop r _ ⇒ ertl_st_pop r l
    9898  | ertl_st_push r _ ⇒ ertl_st_push r l
    99   | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
    100   | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
     99  | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
    101100  | ertl_st_int r i _ ⇒ ertl_st_int r i l
    102101  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
     
    489488  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
    490489  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
    491   | rtl_st_addr r1 r2 x lbl' ⇒
    492     adds_graph [
    493       ertl_st_addr_l r1 x lbl;
    494       ertl_st_addr_h r2 x lbl
    495     ] lbl lbl' def
     490  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
    496491  | rtl_st_stack_addr r1 r2 lbl' ⇒
    497492    adds_graph [
     
    619614      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    620615      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    621       | ertl_st_addr_h _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    622       | ertl_st_addr_l _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     616      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    623617      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    624618      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
Note: See TracChangeset for help on using the changeset viewer.