source: Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma @ 1091

Last change on this file since 1091 was 1091, checked in by campbell, 9 years ago

Merge trunk into id-lookup-branch

File size: 4.2 KB
Line 
1
2include "ASM/Util.ma".
3include "ERTL/ERTL.ma".
4
5definition list_set_union ≝
6  λA: Type[0].
7  λeq_a: A → A → bool.
8  λl: list A.
9  λr: list A.
10    nub_by A eq_a (l @ r).
11
12definition list_set_add ≝
13  λA: Type[0].
14  λeq_a: A → A → bool.
15  λa: A.
16  λs: list A.
17    nub_by A eq_a (a :: s).
18
19definition list_set_diff ≝
20  λA: Type[0].
21  λeq_a: A → A → bool.
22  λl: list A.
23  λr: list A.
24    filter A (λx. member A eq_a x r) l.
25
26definition list_set_equal ≝
27  λA: Type[0].
28  λeq_a: A → A → bool.
29  λl: list A.
30  λr: list A.
31    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
32
33definition statement_successors ≝
34  λs: ertl_statement.
35  match s with
36  [ ertl_st_return _ ⇒ [ ]
37  | ertl_st_skip l ⇒ [ l ]
38  | ertl_st_comment c l ⇒ [ l ]
39  | ertl_st_cost c l ⇒ [ l ]
40  | ertl_st_set_hdw _ _ l ⇒ [ l ]
41  | ertl_st_get_hdw _ _ l ⇒ [ l ]
42  | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
43  | ertl_st_new_frame l ⇒ [ l ]
44  | ertl_st_del_frame l ⇒ [ l ]
45  | ertl_st_frame_size _ l ⇒ [ l ]
46  | ertl_st_push _ l ⇒ [ l ]
47  | ertl_st_pop _ l ⇒ [ l ]
48  | ertl_st_addr_h _ _ l ⇒ [ l ]
49  | ertl_st_addr_l _ _ l ⇒ [ l ]
50  | ertl_st_int _ _ l ⇒ [ l ]
51  | ertl_st_move _ _ l ⇒ [ l ]
52  | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
53  | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
54  | ertl_st_op1 _ _ _ l ⇒ [ l ]
55  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
56  | ertl_st_clear_carry l ⇒ [ l ]
57  | ertl_st_set_carry l ⇒ [ l ]
58  | ertl_st_load _ _ _ l ⇒ [ l ]
59  | ertl_st_store _ _ _ l ⇒ [ l ]
60  | ertl_st_call_id _ _ l ⇒ [ l ]
61  | ertl_st_cond _ l1 l2 ⇒
62      list_set_add ? (eq_identifier ?) l1 [ l2 ]
63  ].
64
65definition register_lattice ≝ (list register) × (list Register).
66definition lattice_property ≝ register_lattice.
67definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
68definition lattice_psingleton: register → register_lattice ≝
69  λr.
70    〈[ r ], [ ]〉.
71definition lattice_hsingleton: Register → register_lattice ≝
72  λr.
73    〈[ ], [ r ]〉.
74
75definition lattice_join: register_lattice → register_lattice → register_lattice ≝
76  λleft.
77  λright.
78  let 〈lp, lh〉 ≝ left in
79  let 〈rp, rh〉 ≝ right in
80    〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
81
82definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
83  λleft.
84  λright.
85  let 〈lp, lh〉 ≝ left in
86  let 〈rp, rh〉 ≝ right in
87    〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
88
89definition lattice_equal: register_lattice → register_lattice → bool ≝
90  λleft.
91  λright.
92  let 〈lp, lh〉 ≝ left in
93  let 〈rp, rh〉 ≝ right in
94    andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
95
96definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
97
98definition defined: ertl_statement → register_lattice ≝
99  λs.
100  match s with
101  [ ertl_st_skip _ ⇒ lattice_bottom
102  | ertl_st_comment _ _ ⇒ lattice_bottom
103  | ertl_st_cost _ _ ⇒ lattice_bottom
104  | ertl_st_push _ _⇒ lattice_bottom
105  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
106  | ertl_st_cond _ _ _ ⇒ lattice_bottom
107  | ertl_st_return _ ⇒ lattice_bottom
108  | ertl_st_clear_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
109  | ertl_st_set_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉
110  | _ ⇒ ?
111  ].
112
113let defined (stmt : statement) : L.t =
114  match stmt with
115  | St_clear_carry _
116  | St_set_carry _ ->
117    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
118  | St_op2 (I8051.Add, r, _, _, _)
119  | St_op2 (I8051.Addc, r, _, _, _)
120  | St_op2 (I8051.Sub, r, _, _, _) ->
121    L.join (L.hsingleton I8051.carry) (L.psingleton r)
122  | St_op1 (I8051.Inc, r, _, _)
123  | St_get_hdw (r, _, _)
124  | St_framesize (r, _)
125  | St_pop (r, _)
126  | St_int (r, _, _)
127  | St_addrH (r, _, _)
128  | St_addrL (r, _, _)
129  | St_move (r, _, _)
130  | St_opaccsA (_, r, _, _, _)
131  | St_opaccsB (_, r, _, _, _)
132  | St_op1 (_, r, _, _)
133  | St_op2 (_, r, _, _, _)
134  | St_load (r, _, _, _) ->
135    L.psingleton r
136  | St_set_hdw (r, _, _)
137  | St_hdw_to_hdw (r, _, _) ->
138    L.hsingleton r
139  | St_call_id _ ->
140      (* Potentially destroys all caller-save hardware registers. *)
141    Register.Set.empty, I8051.caller_saved
142  | St_newframe _
143  | St_delframe _ ->
144    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
Note: See TracBrowser for help on using the repository browser.