Changeset 1282 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Sep 28, 2011, 11:50:32 PM (9 years ago)
Author:
sacerdot
Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1275 r1282  
    77  λs: ertl_statement globals.
    88  match s with
    9   [ joint_st_sequential seq l ⇒
    10     match seq with
    11     [ joint_instr_cond acc_a_reg lbl_true ⇒
     9  [ sequential seq l ⇒
     10    match seq with
     11    [ COND acc_a_reg lbl_true ⇒
    1212        set_insert … lbl_true (set_singleton … l)
    1313    | _ ⇒ set_singleton … l ]
    14   | joint_st_goto l ⇒ set_singleton … l
    15   | joint_st_return ⇒ set_empty ?
     14  | GOTO l ⇒ set_singleton … l
     15  | RETURN ⇒ set_empty ?
    1616  ].
    1717
     
    7878  λs: ertl_statement globals.
    7979  match s with
    80   [ joint_st_sequential seq l ⇒
    81     match seq with
    82     [ joint_instr_op2 op2 r1 r2 _ ⇒
     80  [ sequential seq l ⇒
     81    match seq with
     82    [ OP2 op2 r1 r2 _ ⇒
    8383      match op2 with
    8484      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     
    8787      | _ ⇒ lattice_psingleton r1
    8888      ]
    89     | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    90     | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    91     | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     89    | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
     90    | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
     91    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    9292       lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
    93     | joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    94     | joint_instr_pop r ⇒ lattice_psingleton r
    95     | joint_instr_int r _ ⇒ lattice_psingleton r
    96     | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    97     | joint_instr_load r _ _ ⇒ lattice_psingleton r
     93    | OP1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     94    | POP r ⇒ lattice_psingleton r
     95    | INT r _ ⇒ lattice_psingleton r
     96    | ADDRESS _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     97    | LOAD r _ _ ⇒ lattice_psingleton r
    9898    (* Potentially destroys all caller-save hardware registers. *)
    99     | joint_instr_call_id id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    100     | joint_instr_comment c ⇒ lattice_bottom
    101     | joint_instr_cond r lbl_true ⇒ lattice_bottom
    102     | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
    103     | joint_instr_cost_label clabel ⇒ lattice_bottom
    104     | joint_instr_push r ⇒ lattice_bottom
    105     | joint_instr_move pair_reg ⇒
     99    | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
     100    | COMMENT c ⇒ lattice_bottom
     101    | COND r lbl_true ⇒ lattice_bottom
     102    | STORE acc_a dpl dph ⇒ lattice_bottom
     103    | COST_LABEL clabel ⇒ lattice_bottom
     104    | PUSH r ⇒ lattice_bottom
     105    | MOVE pair_reg ⇒
    106106      (* first register relevant only *)
    107107      let r1 ≝ \fst pair_reg in
     
    110110      | hardware h ⇒ lattice_hsingleton h
    111111      ]
    112     | joint_instr_extension ext ⇒
     112    | extension ext ⇒
    113113      match ext with
    114114      [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    115115      | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    116116      | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
    117   | joint_st_return ⇒ lattice_bottom
    118   | joint_st_goto l ⇒ lattice_bottom
     117  | RETURN ⇒ lattice_bottom
     118  | GOTO l ⇒ lattice_bottom
    119119  ].
    120120
     
    125125  λs: ertl_statement globals.
    126126  match s with
    127   [ joint_st_sequential seq l ⇒
    128     match seq with
    129     [ joint_instr_op2 op2 acc_a r1 r2 ⇒
     127  [ sequential seq l ⇒
     128    match seq with
     129    [ OP2 op2 acc_a r1 r2 ⇒
    130130      match op2 with
    131131      [ Addc ⇒
     
    133133      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    134134      ]
    135     | joint_instr_clear_carry ⇒ lattice_bottom
    136     | joint_instr_set_carry ⇒ lattice_bottom
     135    | CLEAR_CARRY ⇒ lattice_bottom
     136    | SET_CARRY ⇒ lattice_bottom
    137137    (* acc_a and acc_b *)
    138     | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     138    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    139139       lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
    140     | joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2
    141     | joint_instr_pop r ⇒ lattice_bottom
    142     | joint_instr_int r _ ⇒ lattice_bottom
    143     | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
    144     | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
     140    | OP1 op1 r1 r2 ⇒ lattice_psingleton r2
     141    | POP r ⇒ lattice_bottom
     142    | INT r _ ⇒ lattice_bottom
     143    | ADDRESS _ _ r1 r2 ⇒ lattice_bottom
     144    | LOAD acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    145145    (* Reads the hardware registers that are used to pass parameters. *)
    146     | joint_instr_call_id _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    147     | joint_instr_comment c ⇒ lattice_bottom
    148     | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
    149     | joint_instr_store acc_a dpl dph ⇒
     146    | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
     147    | COMMENT c ⇒ lattice_bottom
     148    | COND r lbl_true ⇒ lattice_psingleton r
     149    | STORE acc_a dpl dph ⇒
    150150      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
    151     | joint_instr_cost_label clabel ⇒ lattice_bottom
    152     | joint_instr_push r ⇒ lattice_psingleton r
    153     | joint_instr_move pair_reg ⇒
     151    | COST_LABEL clabel ⇒ lattice_bottom
     152    | PUSH r ⇒ lattice_psingleton r
     153    | MOVE pair_reg ⇒
    154154      (* only second reg in pair relevant *)
    155155      let r2 ≝ \snd pair_reg in
     
    158158      | hardware h ⇒ lattice_hsingleton h
    159159      ]
    160   | joint_instr_extension ext ⇒
     160  | extension ext ⇒
    161161    match ext with
    162162    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    163163    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    164164    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
    165   | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    166   | joint_st_goto l ⇒ lattice_bottom
     165  | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     166  | GOTO l ⇒ lattice_bottom
    167167  ].
    168168
     
    173173  let 〈pliveafter, hliveafter〉 ≝ l in
    174174  match s with
    175   [ joint_st_sequential seq l ⇒
    176     match seq with
    177     [ joint_instr_op2 op2 r1 r2 r3 ⇒
     175  [ sequential seq l ⇒
     176    match seq with
     177    [ OP2 op2 r1 r2 r3 ⇒
    178178      if set_member … (eq_identifier …) r1 pliveafter ∨
    179179         set_member … eq_Register RegisterCarry hliveafter then
     
    181181      else
    182182        Some ? l
    183     | joint_instr_clear_carry ⇒ None ?
    184     | joint_instr_set_carry ⇒ None ?
    185     | joint_instr_opaccs opaccs dr1 dr2 sr1 sr2 ⇒
     183    | CLEAR_CARRY ⇒ None ?
     184    | SET_CARRY ⇒ None ?
     185    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    186186      if set_member … (eq_identifier …) dr1 pliveafter ∨
    187187         set_member … (eq_identifier …) dr2 pliveafter ∨
     
    190190      else
    191191        Some ? l
    192     | joint_instr_op1 op1 r1 r2 ⇒
     192    | OP1 op1 r1 r2 ⇒
    193193      if set_member … (eq_identifier …) r1 pliveafter ∨
    194194         set_member … eq_Register RegisterCarry hliveafter then
     
    196196      else
    197197        Some ? l
    198     | joint_instr_pop r ⇒ None ?
    199     | joint_instr_int r _ ⇒
     198    | POP r ⇒ None ?
     199    | INT r _ ⇒
    200200      if set_member … (eq_identifier …) r pliveafter ∨
    201201         set_member … eq_Register RegisterCarry hliveafter then
     
    203203      else
    204204        Some ? l
    205     | joint_instr_address _ _ r1 r2 ⇒
     205    | ADDRESS _ _ r1 r2 ⇒
    206206      if set_member … (eq_identifier …) r1 pliveafter ∨
    207207         set_member … (eq_identifier …) r2 pliveafter ∨
     
    210210      else
    211211        Some ? l
    212     | joint_instr_load acc_a dpl dph ⇒
     212    | LOAD acc_a dpl dph ⇒
    213213      if set_member ? (eq_identifier …) acc_a pliveafter ∨
    214214         set_member … eq_Register RegisterCarry hliveafter then
     
    216216      else
    217217        Some ? l
    218     | joint_instr_call_id _ nparams _ ⇒ None ?
    219     | joint_instr_comment c ⇒ None ?
    220     | joint_instr_cond r lbl_true ⇒ None ?
    221     | joint_instr_store acc_a dpl dph ⇒ None ?
    222     | joint_instr_cost_label clabel ⇒ None ?
    223     | joint_instr_push r ⇒ None ?
    224     | joint_instr_move pair_reg ⇒
     218    | CALL_ID _ nparams _ ⇒ None ?
     219    | COMMENT c ⇒ None ?
     220    | COND r lbl_true ⇒ None ?
     221    | STORE acc_a dpl dph ⇒ None ?
     222    | COST_LABEL clabel ⇒ None ?
     223    | PUSH r ⇒ None ?
     224    | MOVE pair_reg ⇒
    225225      let r1 ≝ \fst pair_reg in
    226226      let r2 ≝ \snd pair_reg in
     
    237237        else
    238238          Some ? l]
    239     | joint_instr_extension ext ⇒
     239    | extension ext ⇒
    240240      match ext with
    241241      [ ertl_st_ext_new_frame ⇒ None ?
     
    247247        else
    248248          Some ? l]]
    249   | joint_st_goto l ⇒ None ?
    250   | joint_st_return ⇒ None ?
     249  | GOTO l ⇒ None ?
     250  | RETURN ⇒ None ?
    251251  ].
    252252
Note: See TracChangeset for help on using the changeset viewer.