Changeset 1138


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
Files:
4 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
  • src/RTL/RTLtoERTL.ma

    r1131 r1138  
    100100  | ertl_st_int r i _ ⇒ ertl_st_int r i l
    101101  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    102   | ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l
    103   | ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l
     102  | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
    104103  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    105104  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
     
    476475    add_translates (
    477476      set_params args @ [
    478       adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args) start_lbl ];
     477      adds_graph [ ertl_st_call_id f nb_args start_lbl ];
    479478      fetch_result ret_regs
    480479      ]
     
    497496  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
    498497  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
     498      add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
     499(* XXX: change from o'caml
    499500    adds_graph [
    500501      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
    501502      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
    502503      ] lbl lbl' def
     504*)
    503505  | rtl_st_op1 op1 destr srcr lbl' ⇒
    504506    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
     
    617619      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    618620      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    619       | ertl_st_opaccs_a _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    620       | ertl_st_opaccs_b _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     621      | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    621622      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    622623      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
  • src/RTLabs/RTLAbstoRTL.ma

    r1077 r1138  
    12281228  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
    12291229  let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
    1230   let result ≝
     1230  let result ≝f
    12311231    match (f_result def) with
    12321232    [ None ⇒ [ ]
Note: See TracChangeset for help on using the changeset viewer.