Changeset 1098 for Deliverables/D3.3/id-lookup-branch/ERTL

Timestamp:

Aug 3, 2011, 2:48:11 PM (10 years ago)

Author:

campbell

Message:

Merge branch with trunk

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• ERTL/liveness.ma (modified) (2 diffs)

Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

@@ -30 +30 @@
   λr: list A.
     foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
+
+definition list_set_member ≝
+  λA: Type[0].
+  λeq_a: A → A → bool.
+  λa: A.
+  λl: list A.
+    member A eq_a a l.
 
 definition statement_successors ≝
@@ -106 +113 @@
   | ertl_st_cond _ _ _ ⇒ lattice_bottom
   | ertl_st_return _ ⇒ lattice_bottom
-  | ertl_st_clear_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
-  | ertl_st_set_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
-  | _ ⇒ ?
-  ].
-
-let defined (stmt : statement) : L.t =
+  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
+  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
+  | ertl_st_op2 op2 r _ _ _ ⇒
+    match op2 with
+    [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
+    | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
+    | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
+    | _ ⇒ lattice_psingleton r
+    ]
+  | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
+  | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
+  | ertl_st_frame_size r _ ⇒ lattice_psingleton r
+  | 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_move r _ _ ⇒ lattice_psingleton r
+  | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
+  | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
+  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
+  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
+  | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
+  (* Potentially destroys all caller-save hardware registers. *)
+  | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
+  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
+  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
+  ].
+
+definition list_set_of_list ≝
+  λrl.
+    foldr ? ? (list_set_add Register eq_Register) rl [ ].
+
+definition list_set_of_list2 ≝
+  let f ≝ λset. λr. list_set_add Register eq_Register r set in
+    foldl ? ? f [ ].
+
+definition ret_regs ≝ list_set_of_list RegisterRets.
+
+definition used: ertl_statement → register_lattice ≝
+  λstmt.
   match stmt with
-  | St_clear_carry _
-  | St_set_carry _ ->
-    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
-  | St_op2 (I8051.Add, r, _, _, _)
-  | St_op2 (I8051.Addc, r, _, _, _)
-  | St_op2 (I8051.Sub, r, _, _, _) ->
-    L.join (L.hsingleton I8051.carry) (L.psingleton r)
-  | St_op1 (I8051.Inc, r, _, _)
-  | St_get_hdw (r, _, _)
-  | St_framesize (r, _)
-  | St_pop (r, _)
-  | St_int (r, _, _)
-  | St_addrH (r, _, _)
-  | St_addrL (r, _, _)
-  | St_move (r, _, _)
-  | St_opaccsA (_, r, _, _, _)
-  | St_opaccsB (_, r, _, _, _)
-  | St_op1 (_, r, _, _)
-  | St_op2 (_, r, _, _, _)
-  | St_load (r, _, _, _) ->
-    L.psingleton r
-  | St_set_hdw (r, _, _)
-  | St_hdw_to_hdw (r, _, _) ->
-    L.hsingleton r
-  | St_call_id _ ->
-      (* Potentially destroys all caller-save hardware registers. *)
-    Register.Set.empty, I8051.caller_saved
-  | St_newframe _
-  | St_delframe _ ->
-    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
+  [ ertl_st_skip _ ⇒ lattice_bottom
+  | ertl_st_cost _ _ ⇒ lattice_bottom
+  | ertl_st_comment _ _ ⇒ lattice_bottom
+  | 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_int _ _ _ ⇒ lattice_bottom
+  | ertl_st_clear_carry _ ⇒ lattice_bottom
+  | ertl_st_set_carry _ ⇒ lattice_bottom
+    (* 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)〉
+  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
+  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
+  | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
+  | ertl_st_push r _ ⇒ lattice_psingleton r
+  | ertl_st_move _ r _ ⇒ lattice_psingleton r
+  | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
+  | ertl_st_cond r _ _ ⇒ lattice_psingleton r
+  | ertl_st_op2 op2 _ r1 r2 _ ⇒
+    match op2 with
+    [ Addc ⇒
+      lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
+    | _ ⇒ 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_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
+  | ertl_st_store r1 r2 r3 _ ⇒
+    lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
+  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
+  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
+  | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
+  ].
+
+definition eliminable: register_lattice → ertl_statement → option label ≝
+  λl.
+  λstmt.
+  let 〈pliveafter, hliveafter〉 ≝ l in
+  match stmt with
+  [ ertl_st_skip _ ⇒ None ?
+  | ertl_st_comment _ _ ⇒ None ?
+  | ertl_st_cost _ _ ⇒ None ?
+  | ertl_st_new_frame _ ⇒ None ?
+  | ertl_st_del_frame _ ⇒ None ?
+  | ertl_st_pop _ _ ⇒ None ?
+  | ertl_st_push _ _ ⇒ None ?
+  | ertl_st_clear_carry _  ⇒ None ?
+  | ertl_st_set_carry _  ⇒ None ?
+  | ertl_st_store _ _ _ _ ⇒ None ?
+  | ertl_st_call_id _ _ _ ⇒ None ?
+  | ertl_st_cond _ _ _ ⇒ None ?
+  | ertl_st_return _ ⇒ None ?
+  | ertl_st_get_hdw 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_frame_size 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_int 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_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 ∨
+       list_set_member Register eq_Register RegisterCarry hliveafter then
+      None ?
+    else
+      Some ? l
+  | ertl_st_move 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_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 ∨
+       list_set_member Register eq_Register RegisterCarry hliveafter then
+      None ?
+    else
+      Some ? l
+  | ertl_st_op1 _ 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_op2 _ 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_load 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_set_hdw r _ l ⇒
+    if list_set_member Register eq_Register r hliveafter then
+      None ?
+    else
+      Some ? l
+  | ertl_st_hdw_to_hdw r _ l ⇒
+    if list_set_member Register eq_Register r hliveafter then
+      None ?
+    else
+      Some ? l
+  ].
+
+definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
+  λstmt.
+  λliveafter.
+  match eliminable liveafter stmt with
+  [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
+  | Some l ⇒ liveafter
+  ].
+
+definition valuation ≝ label → register_lattice.
+
+definition analyse: ertl_internal_function → valuation ≝
+  λint_fun.
+  let livebefore ≝ λlabel. λliveafter: valuation.
+    match lookup ? ? (ertl_if_graph int_fun) label with
+    [ None      ⇒ ?
+    | Some stmt ⇒ statement_semantics stmt (liveafter label)
+    ]
+  in ?.