1 | |
---|
2 | include "ASM/Util.ma". |
---|
3 | include "ERTL/ERTL.ma". |
---|
4 | |
---|
5 | definition 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 | |
---|
12 | definition 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 | |
---|
19 | definition 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 | |
---|
26 | definition 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 | |
---|
33 | definition 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 | |
---|
65 | definition register_lattice ≝ (list register) × (list Register). |
---|
66 | definition lattice_property ≝ register_lattice. |
---|
67 | definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉. |
---|
68 | definition lattice_psingleton: register → register_lattice ≝ |
---|
69 | λr. |
---|
70 | 〈[ r ], [ ]〉. |
---|
71 | definition lattice_hsingleton: Register → register_lattice ≝ |
---|
72 | λr. |
---|
73 | 〈[ ], [ r ]〉. |
---|
74 | |
---|
75 | definition 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 | |
---|
82 | definition 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 | |
---|
89 | definition 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 | |
---|
96 | definition lattice_is_maximal: register_lattice → bool ≝ λl. false. |
---|
97 | |
---|
98 | definition 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 | |
---|
113 | let 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) |
---|