1 | include "ASM/I8051.ma". |
---|
2 | include "common/CostLabel.ma". |
---|
3 | include "common/AST.ma". |
---|
4 | include "common/Registers.ma". |
---|
5 | include "common/Graphs.ma". |
---|
6 | |
---|
7 | (* Here is the structure of parameter records (downward edges are coercions, |
---|
8 | the ↓ edges are the only explicitly defined coercions). lin_params and |
---|
9 | graph_params are simple wrappers of unserialized_params, and the coercions |
---|
10 | from them to params instantiate the missing bits with values for linarized |
---|
11 | programs and graph programs respectively. |
---|
12 | |
---|
13 | lin_params graph_params |
---|
14 | | \_____ /____ | |
---|
15 | | / \ | |
---|
16 | \_______ / ↓ ↓ |
---|
17 | \ _\____ params |
---|
18 | \_/ \ | |
---|
19 | / \ \ ↓ |
---|
20 | _____/ unserialized_params |
---|
21 | / _______/ | |
---|
22 | / / | |
---|
23 | stmt_params / local_params |
---|
24 | | __/ | |
---|
25 | inst_params funct_params |
---|
26 | |
---|
27 | inst_params : types needed to define instructions |
---|
28 | stmt_params : adds successor type needed to define statements |
---|
29 | funct_params : types of result register and parameters of function |
---|
30 | local_params : adds types of local registers |
---|
31 | params : adds type of code and lookup function |
---|
32 | graph_params : is made just of inst_params and local_params, and the coercion |
---|
33 | to params adds structure common to graph languages *) |
---|
34 | |
---|
35 | record inst_params : Type[1] ≝ |
---|
36 | { acc_a_reg: Type[0] (* registers that will eventually need to be A *) |
---|
37 | ; acc_b_reg: Type[0] (* registers that will eventually need to be B *) |
---|
38 | ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *) |
---|
39 | ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *) |
---|
40 | ; dpl_reg: Type[0] (* low address registers *) |
---|
41 | ; dph_reg: Type[0] (* high address registers *) |
---|
42 | ; dpl_arg: Type[0] (* low address registers *) |
---|
43 | ; dph_arg: Type[0] (* high address registers *) |
---|
44 | ; snd_arg : Type[0] (* second argument of binary op *) |
---|
45 | ; pair_move: Type[0] (* argument of move instructions *) |
---|
46 | ; call_args: Type[0] (* arguments of function calls *) |
---|
47 | ; call_dest: Type[0] (* possible destination of function computation *) |
---|
48 | ; extend_statements: Type[0] (* other statements not fitting in the general framework *) |
---|
49 | ; ext_forall_labels : (label → Prop) → extend_statements → Prop |
---|
50 | }. |
---|
51 | |
---|
52 | inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝ |
---|
53 | | COMMENT: String → joint_instruction p globals |
---|
54 | | COST_LABEL: costlabel → joint_instruction p globals |
---|
55 | | MOVE: pair_move p → joint_instruction p globals |
---|
56 | | POP: acc_a_reg p → joint_instruction p globals |
---|
57 | | PUSH: acc_a_arg p → joint_instruction p globals |
---|
58 | | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
59 | | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals |
---|
60 | | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals |
---|
61 | | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals |
---|
62 | (* int done with generic move *) |
---|
63 | (*| INT: generic_reg p → Byte → joint_instruction p globals *) |
---|
64 | | CLEAR_CARRY: joint_instruction p globals |
---|
65 | | SET_CARRY: joint_instruction p globals |
---|
66 | | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals |
---|
67 | | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals |
---|
68 | | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals |
---|
69 | | COND: acc_a_reg p → label → joint_instruction p globals |
---|
70 | | extension: extend_statements p → joint_instruction p globals. |
---|
71 | |
---|
72 | (* Paolo: to be moved elsewhere *) |
---|
73 | |
---|
74 | notation "r ← a1 .op. a2" with precedence 50 for |
---|
75 | @{'op2 $op $r $a1 $a2}. |
---|
76 | notation "r ← . op . a" with precedence 50 for |
---|
77 | @{'op1 $op $r $a}. |
---|
78 | notation "r ← a" with precedence 50 for |
---|
79 | @{'mov $r $a}. (* to be set in individual languages *) |
---|
80 | notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for |
---|
81 | @{'opaccs $op $r $s $a1 $a2}. |
---|
82 | |
---|
83 | interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). |
---|
84 | interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). |
---|
85 | interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). |
---|
86 | |
---|
87 | |
---|
88 | |
---|
89 | definition inst_forall_labels : ∀p : inst_params.∀globals. |
---|
90 | (label → Prop) → joint_instruction p globals → Prop ≝ |
---|
91 | λp,g,P,inst. match inst with |
---|
92 | [ COND _ l ⇒ P l |
---|
93 | | extension ext_s ⇒ ext_forall_labels p P ext_s |
---|
94 | | _ ⇒ True |
---|
95 | ]. |
---|
96 | |
---|
97 | record funct_params : Type[1] ≝ |
---|
98 | { resultT : Type[0] |
---|
99 | ; paramsT : Type[0] |
---|
100 | }. |
---|
101 | |
---|
102 | record local_params : Type[1] ≝ |
---|
103 | { funct_pars :> funct_params |
---|
104 | ; localsT: Type[0] |
---|
105 | }. |
---|
106 | |
---|
107 | record unserialized_params : Type[1] ≝ |
---|
108 | { u_inst_pars :> inst_params |
---|
109 | ; u_local_pars :> local_params |
---|
110 | }. |
---|
111 | |
---|
112 | record stmt_params : Type[1] ≝ |
---|
113 | { unserialized_pars :> unserialized_params |
---|
114 | ; succ : Type[0] |
---|
115 | ; succ_forall_labels : (label → Prop) → succ → Prop |
---|
116 | }. |
---|
117 | |
---|
118 | inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ |
---|
119 | | sequential: joint_instruction p globals → succ p → joint_statement p globals |
---|
120 | | GOTO: label → joint_statement p globals |
---|
121 | | RETURN: joint_statement p globals. |
---|
122 | |
---|
123 | record params : Type[1] ≝ |
---|
124 | { stmt_pars :> stmt_params |
---|
125 | ; codeT: list ident → Type[0] |
---|
126 | ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals) |
---|
127 | }. |
---|
128 | |
---|
129 | |
---|
130 | (* for all labels in statement. Uses succ_choice to consider the successor of |
---|
131 | a statement when such successors are labels *) |
---|
132 | definition stmt_forall_labels : ∀p : stmt_params.∀globals. |
---|
133 | (label → Prop) → joint_statement p globals → Prop ≝ |
---|
134 | λp,g,P,stmt. match stmt with |
---|
135 | [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next |
---|
136 | | GOTO l ⇒ P l |
---|
137 | | RETURN ⇒ True |
---|
138 | ]. |
---|
139 | |
---|
140 | record lin_params : Type[1] ≝ |
---|
141 | { l_u_pars :> unserialized_params }. |
---|
142 | |
---|
143 | include "utilities/option.ma". |
---|
144 | |
---|
145 | definition lin_params_to_params ≝ |
---|
146 | λlp : lin_params. mk_params |
---|
147 | (mk_stmt_params lp unit (λ_.λ_.True)) |
---|
148 | (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) |
---|
149 | (* lookup ≝ *)(λglobals,code,lbl.find ?? |
---|
150 | (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in |
---|
151 | ! lbl' ← lbl_opt ; |
---|
152 | if eq_identifier … lbl lbl' then return stmt else None ?) code). |
---|
153 | |
---|
154 | coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params |
---|
155 | on _lp : lin_params to params. |
---|
156 | |
---|
157 | record graph_params : Type[1] ≝ |
---|
158 | { g_u_pars :> unserialized_params }. |
---|
159 | |
---|
160 | include alias "common/Graphs.ma". (* To pick the right lookup *) |
---|
161 | |
---|
162 | (* One common instantiation of params via Graphs of joint_statements |
---|
163 | (all languages but LIN) *) |
---|
164 | definition graph_params_to_params ≝ |
---|
165 | λgp : graph_params. mk_params |
---|
166 | (mk_stmt_params gp label (λP.P)) |
---|
167 | (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) |
---|
168 | (* lookup ≝ *)(λglobals.lookup …). |
---|
169 | |
---|
170 | coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp |
---|
171 | on _gp : graph_params to params. |
---|
172 | |
---|
173 | |
---|
174 | definition labels_present : ∀p : params.∀globals. |
---|
175 | codeT p globals → (joint_statement p globals) → Prop ≝ |
---|
176 | λglobals,p,code,s. stmt_forall_labels globals p |
---|
177 | (λl.lookup … code l ≠ None ?) s. |
---|
178 | |
---|
179 | definition forall_stmts : ∀p : params.∀globals. |
---|
180 | ∀P: joint_statement p globals → Prop. codeT p globals → Prop ≝ |
---|
181 | λglobals,p,P,code. ∀l,s. lookup … code l = Some ? s → P s. |
---|
182 | |
---|
183 | definition code_closed : ∀p : params.∀globals. |
---|
184 | codeT p globals → Prop ≝ λp,globals,code. |
---|
185 | forall_stmts … (labels_present … code) code. |
---|
186 | |
---|
187 | (* CSC: special case where localsT is a list of registers (RTL and ERTL) *) |
---|
188 | definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars. |
---|
189 | (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))). |
---|
190 | |
---|
191 | record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝ |
---|
192 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
193 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
194 | (* Paolo: if we want this machinery to work for RTLabs too, we will need the |
---|
195 | following, right? *) |
---|
196 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
197 | joint_if_result : resultT p; |
---|
198 | joint_if_params : paramsT p; |
---|
199 | joint_if_locals : localsT p; |
---|
200 | (*CSC: XXXXX stacksize unused for LTL-...*) |
---|
201 | joint_if_stacksize: nat; |
---|
202 | joint_if_code : codeT p globals ; |
---|
203 | (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) |
---|
204 | joint_if_entry : Σl: label. lookup … joint_if_code l ≠ None ?; |
---|
205 | (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) |
---|
206 | joint_if_exit : Σl: label. lookup … joint_if_code l ≠ None ? |
---|
207 | }. |
---|
208 | |
---|
209 | definition joint_closed_internal_function ≝ |
---|
210 | λglobals,p. |
---|
211 | Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def). |
---|
212 | |
---|
213 | (* Currified form *) |
---|
214 | definition set_joint_if_exit ≝ |
---|
215 | λglobals,pars. |
---|
216 | λexit: label. |
---|
217 | λp:joint_internal_function globals pars. |
---|
218 | λprf: lookup … (joint_if_code … p) exit ≠ None ?. |
---|
219 | mk_joint_internal_function globals pars |
---|
220 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
221 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
222 | (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf). |
---|
223 | |
---|
224 | definition set_joint_code ≝ |
---|
225 | λglobals: list ident. |
---|
226 | λpars: params. |
---|
227 | λint_fun: joint_internal_function globals pars. |
---|
228 | λgraph: codeT pars globals. |
---|
229 | λentry. |
---|
230 | λexit. |
---|
231 | mk_joint_internal_function globals pars |
---|
232 | (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) |
---|
233 | (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun) |
---|
234 | graph entry exit. |
---|
235 | |
---|
236 | definition set_joint_if_graph ≝ |
---|
237 | λglobals,pars. |
---|
238 | λgraph. |
---|
239 | λp:joint_internal_function globals pars. |
---|
240 | λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?. |
---|
241 | λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?. |
---|
242 | set_joint_code globals pars p |
---|
243 | graph |
---|
244 | (mk_Sig … (joint_if_entry … p) entry_prf) |
---|
245 | (mk_Sig … (joint_if_exit … p) exit_prf). |
---|
246 | |
---|
247 | definition set_luniverse ≝ |
---|
248 | λglobals,pars. |
---|
249 | λp : joint_internal_function globals pars. |
---|
250 | λluniverse: universe LabelTag. |
---|
251 | mk_joint_internal_function globals pars |
---|
252 | luniverse (joint_if_runiverse … p) (joint_if_result … p) |
---|
253 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
254 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
255 | |
---|
256 | definition set_runiverse ≝ |
---|
257 | λglobals,pars. |
---|
258 | λp : joint_internal_function globals pars. |
---|
259 | λruniverse: universe RegisterTag. |
---|
260 | mk_joint_internal_function globals pars |
---|
261 | (joint_if_luniverse … p) runiverse (joint_if_result … p) |
---|
262 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
263 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
264 | |
---|
265 | (* Paolo: probably should move these elsewhere *) |
---|
266 | definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?. |
---|
267 | definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X. |
---|
268 | graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l. |
---|
269 | mk_Sig … (pi1 ?? sig_l) ?. |
---|
270 | @graph_add_lookup |
---|
271 | @(pi2 … sig_l) |
---|
272 | qed. |
---|
273 | |
---|
274 | (* Specialized for graph_params *) |
---|
275 | definition add_graph ≝ |
---|
276 | λg_pars : graph_params.λglobals.λl:label.λstmt. |
---|
277 | λp:joint_internal_function globals g_pars. |
---|
278 | let code ≝ add … (joint_if_code … p) l stmt in |
---|
279 | mk_joint_internal_function ? g_pars |
---|
280 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
281 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
282 | code |
---|
283 | (graph_dom_add_incl … (joint_if_entry … p)) |
---|
284 | (graph_dom_add_incl … (joint_if_exit … p)). |
---|
285 | |
---|
286 | definition set_locals ≝ |
---|
287 | λglobals,pars. |
---|
288 | λp : joint_internal_function globals pars. |
---|
289 | λlocals. |
---|
290 | mk_joint_internal_function globals pars |
---|
291 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
292 | (joint_if_params … p) locals (joint_if_stacksize … p) |
---|
293 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
294 | |
---|
295 | definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals). |
---|
296 | |
---|
297 | definition joint_program ≝ |
---|
298 | λp:params. program (λglobals. joint_function globals p) nat. |
---|