Changeset 1144 for src/ERTL/liveness.ma

Timestamp:

Aug 30, 2011, 3:53:21 PM (10 years ago)

Author:

mulligan

Message:

added build.ma file. matita bug found

File:

• src/ERTL/liveness.ma (modified) (7 diffs)

src/ERTL/liveness.ma

@@ -49 +49 @@
   | ertl_st_push _ l ⇒ [ l ]
   | ertl_st_pop _ l ⇒ [ l ]
-  | ertl_st_addr_h _ _ l ⇒ [ l ]
-  | ertl_st_addr_l _ _ l ⇒ [ l ]
+  | ertl_st_addr _ _ _ l ⇒ [ l ]
   | ertl_st_int _ _ l ⇒ [ l ]
   | ertl_st_move _ _ l ⇒ [ l ]
-  | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
-  | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
+  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
   | ertl_st_op1 _ _ _ l ⇒ [ l ]
   | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
@@ -148 +146 @@
   | ertl_st_pop r _ ⇒ lattice_psingleton r
   | ertl_st_int r _ _ ⇒ lattice_psingleton r
-  | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
-  | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
+  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
   | ertl_st_move r _ _ ⇒ lattice_psingleton r
-  | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
-  | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
+  (* XXX: change from o'caml *)
+  | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
   | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
   | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
@@ -180 +177 @@
   | ertl_st_frame_size _ _ ⇒ lattice_bottom
   | ertl_st_pop _ _ ⇒ lattice_bottom
-  | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
-  | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
+  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
   | ertl_st_int _ _ _ ⇒ lattice_bottom
   | ertl_st_clear_carry _ ⇒ lattice_bottom
@@ -187 +183 @@
     (* Reads the hardware registers that are used to pass parameters. *)
   | ertl_st_call_id _ nparams _ ⇒
-    〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
+    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
   | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
   | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
@@ -201 +197 @@
     | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     ]
-  | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
-  | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
+  | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
   | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
   | ertl_st_store r1 r2 r3 _ ⇒
@@ -247 +242 @@
     else
       Some ? l
-  | ertl_st_addr_h r _ l ⇒
-    if list_set_member register (eq_identifier ?) r pliveafter ∨
-       list_set_member Register eq_Register RegisterCarry hliveafter then
-      None ?
-    else
-      Some ? l
-  | ertl_st_addr_l r _ l ⇒
-    if list_set_member register (eq_identifier ?) r pliveafter ∨
+  | ertl_st_addr r1 r2 _ l ⇒
+    if list_set_member register (eq_identifier ?) r1 pliveafter ∨
+       list_set_member register (eq_identifier ?) r2 pliveafter ∨
        list_set_member Register eq_Register RegisterCarry hliveafter then
       None ?
@@ -265 +255 @@
     else
       Some ? l
-  | ertl_st_opaccs_a _ r _ _ l ⇒
-    if list_set_member register (eq_identifier ?) r pliveafter ∨
-       list_set_member Register eq_Register RegisterCarry hliveafter then
-      None ?
-    else
-      Some ? l
-  | ertl_st_opaccs_b _ r _ _ l ⇒
-    if list_set_member register (eq_identifier ?) r pliveafter ∨
+  | ertl_st_opaccs _ d1 d2 _ _ l ⇒
+    if list_set_member register (eq_identifier ?) d1 pliveafter ∨
+       list_set_member register (eq_identifier ?) d2 pliveafter ∨
        list_set_member Register eq_Register RegisterCarry hliveafter then
       None ?