Changeset 1144 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Aug 30, 2011, 3:53:21 PM (10 years ago)
Author:
mulligan
Message:

added build.ma file. matita bug found

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1124 r1144  
    4949  | ertl_st_push _ l ⇒ [ l ]
    5050  | ertl_st_pop _ l ⇒ [ l ]
    51   | ertl_st_addr_h _ _ l ⇒ [ l ]
    52   | ertl_st_addr_l _ _ l ⇒ [ l ]
     51  | ertl_st_addr _ _ _ l ⇒ [ l ]
    5352  | ertl_st_int _ _ l ⇒ [ l ]
    5453  | ertl_st_move _ _ l ⇒ [ l ]
    55   | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
    56   | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
     54  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    5755  | ertl_st_op1 _ _ _ l ⇒ [ l ]
    5856  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
     
    148146  | ertl_st_pop r _ ⇒ lattice_psingleton r
    149147  | ertl_st_int r _ _ ⇒ lattice_psingleton r
    150   | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
    151   | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     148  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    152149  | ertl_st_move r _ _ ⇒ lattice_psingleton r
    153   | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
    154   | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
     150  (* XXX: change from o'caml *)
     151  | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    155152  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    156153  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
     
    180177  | ertl_st_frame_size _ _ ⇒ lattice_bottom
    181178  | ertl_st_pop _ _ ⇒ lattice_bottom
    182   | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
    183   | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     179  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    184180  | ertl_st_int _ _ _ ⇒ lattice_bottom
    185181  | ertl_st_clear_carry _ ⇒ lattice_bottom
     
    187183    (* Reads the hardware registers that are used to pass parameters. *)
    188184  | ertl_st_call_id _ nparams _ ⇒
    189     〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     185    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    190186  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    191187  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
     
    201197    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    202198    ]
    203   | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    204   | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     199  | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    205200  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    206201  | ertl_st_store r1 r2 r3 _ ⇒
     
    247242    else
    248243      Some ? l
    249   | ertl_st_addr_h r _ l ⇒
    250     if list_set_member register (eq_identifier ?) r pliveafter ∨
    251        list_set_member Register eq_Register RegisterCarry hliveafter then
    252       None ?
    253     else
    254       Some ? l
    255   | ertl_st_addr_l r _ l ⇒
    256     if list_set_member register (eq_identifier ?) r pliveafter ∨
     244  | ertl_st_addr r1 r2 _ l ⇒
     245    if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     246       list_set_member register (eq_identifier ?) r2 pliveafter ∨
    257247       list_set_member Register eq_Register RegisterCarry hliveafter then
    258248      None ?
     
    265255    else
    266256      Some ? l
    267   | ertl_st_opaccs_a _ r _ _ l ⇒
    268     if list_set_member register (eq_identifier ?) r pliveafter ∨
    269        list_set_member Register eq_Register RegisterCarry hliveafter then
    270       None ?
    271     else
    272       Some ? l
    273   | ertl_st_opaccs_b _ r _ _ l ⇒
    274     if list_set_member register (eq_identifier ?) r pliveafter ∨
     257  | ertl_st_opaccs _ d1 d2 _ _ l ⇒
     258    if list_set_member register (eq_identifier ?) d1 pliveafter ∨
     259       list_set_member register (eq_identifier ?) d2 pliveafter ∨
    275260       list_set_member Register eq_Register RegisterCarry hliveafter then
    276261      None ?
Note: See TracChangeset for help on using the changeset viewer.