1 | include "RTLabs/syntax.ma". |
---|
2 | include "RTL/RTL.ma". |
---|
3 | include "common/AssocList.ma". |
---|
4 | include "common/Graphs.ma". |
---|
5 | |
---|
6 | definition add_graph ≝ |
---|
7 | λlbl: label. |
---|
8 | λstmt. |
---|
9 | λdef. |
---|
10 | let f_labgen' ≝ f_labgen def in |
---|
11 | let f_reggen' ≝ f_reggen def in |
---|
12 | let f_sig' ≝ f_sig def in |
---|
13 | let f_result' ≝ f_result def in |
---|
14 | let f_params' ≝ f_params def in |
---|
15 | let f_locals' ≝ f_locals def in |
---|
16 | let f_ptrs' ≝ f_ptrs def in |
---|
17 | let f_stacksize' ≝ f_stacksize def in |
---|
18 | let f_graph' ≝ add ? ? (f_graph def) lbl stmt in |
---|
19 | let f_entry' ≝ f_entry def in |
---|
20 | let f_exit' ≝ f_exit def in |
---|
21 | mk_internal_function |
---|
22 | f_labgen' f_reggen' f_sig' f_result' |
---|
23 | f_params' f_locals' f_ptrs' f_stacksize' |
---|
24 | f_graph' f_entry' f_exit'. |
---|
25 | |
---|
26 | definition fresh_label ≝ |
---|
27 | λdef. |
---|
28 | match fresh LabelTag (f_labgen def) with |
---|
29 | [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ) |
---|
30 | | Error ⇒ None ? |
---|
31 | ]. |
---|
32 | |
---|
33 | axiom fresh_reg: internal_function → internal_function × register. |
---|
34 | |
---|
35 | let rec fresh_regs (def: internal_function) (n: nat) on n ≝ |
---|
36 | match n with |
---|
37 | [ O ⇒ 〈def, [ ]〉 |
---|
38 | | S n ⇒ |
---|
39 | let 〈def, res〉 ≝ fresh_regs def n in |
---|
40 | let 〈def, r〉 ≝ fresh_reg def in |
---|
41 | 〈def, r :: res〉 |
---|
42 | ]. |
---|
43 | |
---|
44 | definition addr_regs ≝ |
---|
45 | λregs. |
---|
46 | match regs with |
---|
47 | [ cons hd tl ⇒ |
---|
48 | match tl with |
---|
49 | [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉 |
---|
50 | | nil ⇒ None (register × register) |
---|
51 | ] |
---|
52 | | nil ⇒ None (register × register) |
---|
53 | ]. |
---|
54 | |
---|
55 | inductive register_type: Type[0] ≝ |
---|
56 | | register_int: register → register_type |
---|
57 | | register_ptr: register → register → register_type. |
---|
58 | |
---|
59 | definition local_env ≝ assoc_list register register_type. |
---|
60 | |
---|
61 | definition initialize_local_env_internal ≝ |
---|
62 | λeq. |
---|
63 | λruniverse. |
---|
64 | λptrs. |
---|
65 | λlenv. |
---|
66 | λr. |
---|
67 | let fresh ≝ snd ? ? (fresh_reg runiverse) in |
---|
68 | let rt ≝ |
---|
69 | match member ? eq r ptrs with |
---|
70 | [ true ⇒ register_ptr r fresh |
---|
71 | | false ⇒ register_int r |
---|
72 | ] |
---|
73 | in |
---|
74 | assoc_list_add ? ? 〈r, rt〉 lenv. |
---|
75 | |
---|
76 | definition initialize_local_env ≝ |
---|
77 | λruniverse. |
---|
78 | λptrs. |
---|
79 | λregisters. |
---|
80 | foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers. |
---|
81 | |
---|
82 | definition filter_and_to_list_local_env_internal ≝ |
---|
83 | λlenv. |
---|
84 | λl. |
---|
85 | λr. |
---|
86 | match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with |
---|
87 | [ Some entry ⇒ |
---|
88 | match entry with |
---|
89 | [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ]) |
---|
90 | | register_int r ⇒ (l @ [ r ]) |
---|
91 | ] |
---|
92 | | None ⇒ [ ] (* dpm: should this be none? *) |
---|
93 | ]. |
---|
94 | |
---|
95 | definition filter_and_to_list_local_env ≝ |
---|
96 | λlenv. |
---|
97 | λregisters. |
---|
98 | foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers. |
---|
99 | |
---|
100 | definition list_of_register_type ≝ |
---|
101 | λrt. |
---|
102 | match rt with |
---|
103 | [ register_ptr r1 r2 ⇒ [ r1; r2 ] |
---|
104 | | register_int r ⇒ [ r ] |
---|
105 | ]. |
---|
106 | |
---|
107 | definition find_and_list ≝ |
---|
108 | λr. |
---|
109 | λlenv. |
---|
110 | match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with |
---|
111 | [ None ⇒ [ ] (* dpm: should this be none? *) |
---|
112 | | Some lkup ⇒ list_of_register_type lkup |
---|
113 | ]. |
---|
114 | |
---|
115 | definition find_and_list_args ≝ |
---|
116 | λargs. |
---|
117 | λlenv. |
---|
118 | map ? ? (λr. find_and_list r lenv) args. |
---|
119 | |
---|
120 | definition find_and_addr ≝ |
---|
121 | λr. |
---|
122 | λlenv. |
---|
123 | match find_and_list r lenv with |
---|
124 | [ cons hd tl ⇒ |
---|
125 | match tl with |
---|
126 | [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉 |
---|
127 | | nil ⇒ None ? |
---|
128 | ] |
---|
129 | | nil ⇒ None ? (* dpm: was assert false *) |
---|
130 | ]. |
---|
131 | |
---|
132 | definition rtl_args ≝ |
---|
133 | λregs_list. |
---|
134 | λlenv. |
---|
135 | flatten ? (find_and_list_args regs_list lenv). |
---|
136 | |
---|
137 | definition change_label ≝ |
---|
138 | λlbl. |
---|
139 | λstmt. |
---|
140 | match stmt with |
---|
141 | [ rtl_st_skip _ ⇒ rtl_st_skip lbl |
---|
142 | | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl |
---|
143 | | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl |
---|
144 | | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl |
---|
145 | | rtl_st_int r i _ ⇒ rtl_st_int r i lbl |
---|
146 | | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl |
---|
147 | | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl |
---|
148 | | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl |
---|
149 | | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl |
---|
150 | | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl |
---|
151 | | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl |
---|
152 | | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl |
---|
153 | | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl |
---|
154 | | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl |
---|
155 | | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a |
---|
156 | | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a |
---|
157 | | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2 |
---|
158 | | rtl_st_return r ⇒ rtl_st_return r |
---|
159 | | _ ⇒ ? |
---|
160 | ]. |
---|
161 | |
---|
162 | let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) def ≝ |
---|
163 | match stmt_list with |
---|
164 | [ nil ⇒ def |
---|
165 | | cons hd tl ⇒ |
---|
166 | match tl with |
---|
167 | [ nil ⇒ add_graph start_lbl (change_lbl dest_lbl stmt) def |
---|
168 | | cons hd' tl' ⇒ ? |
---|
169 | ] |
---|
170 | ]. |
---|
171 | |
---|
172 | let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with |
---|
173 | | [] -> def |
---|
174 | | [stmt] -> |
---|
175 | add_graph start_lbl (change_label dest_lbl stmt) def |
---|
176 | | stmt :: stmt_list -> |
---|
177 | let tmp_lbl = fresh_label def in |
---|
178 | let stmt = change_label tmp_lbl stmt in |
---|
179 | let def = add_graph start_lbl stmt def in |
---|
180 | adds_graph stmt_list tmp_lbl dest_lbl def |
---|