source: src/ERTL/liveness.ma @ 1088

Last change on this file since 1088 was 1088, checked in by mulligan, 10 years ago

work on liveness analysis: an imperative nightmare

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