1 | |
---|
2 | include "Clight/Csyntax.ma". |
---|
3 | include "Clight/TypeComparison.ma". |
---|
4 | include "utilities/lists.ma". |
---|
5 | include "utilities/deppair.ma". |
---|
6 | |
---|
7 | (* Identify local variables that must be allocated memory. *) |
---|
8 | |
---|
9 | let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝ |
---|
10 | match e with |
---|
11 | [ Expr ed ty ⇒ |
---|
12 | match ed with |
---|
13 | [ Ederef e1 ⇒ gather_mem_vars_expr e1 |
---|
14 | | Eaddrof e1 ⇒ gather_mem_vars_addr e1 |
---|
15 | | Eunop _ e1 ⇒ gather_mem_vars_expr e1 |
---|
16 | | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
17 | gather_mem_vars_expr e2 |
---|
18 | | Ecast _ e1 ⇒ gather_mem_vars_expr e1 |
---|
19 | | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪ |
---|
20 | gather_mem_vars_expr e2 ∪ |
---|
21 | gather_mem_vars_expr e3 |
---|
22 | | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
23 | gather_mem_vars_expr e2 |
---|
24 | | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
25 | gather_mem_vars_expr e2 |
---|
26 | | Efield e1 _ ⇒ gather_mem_vars_expr e1 |
---|
27 | | Ecost _ e1 ⇒ gather_mem_vars_expr e1 |
---|
28 | | _ ⇒ ∅ |
---|
29 | ] |
---|
30 | ] |
---|
31 | and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝ |
---|
32 | match e with |
---|
33 | [ Expr ed ty ⇒ |
---|
34 | match ed with |
---|
35 | [ Evar x ⇒ { (x) } |
---|
36 | | Ederef e1 ⇒ gather_mem_vars_expr e1 |
---|
37 | | Efield e1 _ ⇒ gather_mem_vars_addr e1 |
---|
38 | | _ ⇒ ∅ (* not an lvalue *) |
---|
39 | ] |
---|
40 | ]. |
---|
41 | |
---|
42 | let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝ |
---|
43 | match s with |
---|
44 | [ Sskip ⇒ ∅ |
---|
45 | | Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
46 | gather_mem_vars_expr e2 |
---|
47 | | Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪ |
---|
48 | gather_mem_vars_expr e2 ∪ |
---|
49 | (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es) |
---|
50 | | Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
51 | gather_mem_vars_stmt s2 |
---|
52 | | Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
53 | gather_mem_vars_stmt s1 ∪ |
---|
54 | gather_mem_vars_stmt s2 |
---|
55 | | Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ |
---|
56 | gather_mem_vars_stmt s1 |
---|
57 | | Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ |
---|
58 | gather_mem_vars_stmt s1 |
---|
59 | | Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
60 | gather_mem_vars_expr e1 ∪ |
---|
61 | gather_mem_vars_stmt s2 ∪ |
---|
62 | gather_mem_vars_stmt s3 |
---|
63 | | Sbreak ⇒ ∅ |
---|
64 | | Scontinue ⇒ ∅ |
---|
65 | | Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] |
---|
66 | | Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪ |
---|
67 | gather_mem_vars_ls ls |
---|
68 | | Slabel _ s1 ⇒ gather_mem_vars_stmt s1 |
---|
69 | | Sgoto _ ⇒ ∅ |
---|
70 | | Scost _ s1 ⇒ gather_mem_vars_stmt s1 |
---|
71 | ] |
---|
72 | and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝ |
---|
73 | match ls with |
---|
74 | [ LSdefault s1 ⇒ gather_mem_vars_stmt s1 |
---|
75 | | LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
76 | gather_mem_vars_ls ls1 |
---|
77 | ]. |
---|
78 | |
---|
79 | inductive var_type : Type[0] ≝ |
---|
80 | | Global : region → var_type |
---|
81 | | Stack : nat → var_type |
---|
82 | | Local : var_type |
---|
83 | . |
---|
84 | |
---|
85 | definition var_types ≝ identifier_map SymbolTag var_type. |
---|
86 | |
---|
87 | axiom UndeclaredIdentifier : String. |
---|
88 | |
---|
89 | definition lookup' ≝ |
---|
90 | λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). |
---|
91 | |
---|
92 | definition local_id : var_types → ident → Prop ≝ |
---|
93 | λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ]. |
---|
94 | |
---|
95 | (* Note that the semantics allows locals to shadow globals. |
---|
96 | Parameters start out as locals, but get stack allocated if their address |
---|
97 | is taken. We will add code to store them if that's the case. |
---|
98 | *) |
---|
99 | |
---|
100 | definition always_alloc : type → bool ≝ |
---|
101 | λt. match t with |
---|
102 | [ Tarray _ _ _ ⇒ true |
---|
103 | | Tstruct _ _ ⇒ true |
---|
104 | | Tunion _ _ ⇒ true |
---|
105 | | _ ⇒ false |
---|
106 | ]. |
---|
107 | |
---|
108 | definition characterise_vars : list (ident×region) → function → var_types × nat ≝ |
---|
109 | λglobals, f. |
---|
110 | let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in |
---|
111 | let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in |
---|
112 | let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. |
---|
113 | let 〈m,stack_high〉 ≝ ms in |
---|
114 | let 〈id,ty〉 ≝ v in |
---|
115 | let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id |
---|
116 | then 〈Stack stack_high,stack_high + sizeof ty〉 |
---|
117 | else 〈Local, stack_high〉 in |
---|
118 | 〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in |
---|
119 | 〈m,stacksize〉. |
---|
120 | |
---|
121 | lemma local_id_add_global : ∀vars,id,r,id'. |
---|
122 | local_id (add ?? vars id (Global r)) id' → local_id vars id'. |
---|
123 | #var #id #r #id' |
---|
124 | whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?) |
---|
125 | cases (identifier_eq ? id id') |
---|
126 | [ #E >E >lookup_add_hit whd in ⊢ (% → ?) * |
---|
127 | | #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/ |
---|
128 | ] qed. |
---|
129 | |
---|
130 | lemma local_id_add_miss : ∀vars,id,t,id'. |
---|
131 | id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'. |
---|
132 | #vars #id #t #id' #NE |
---|
133 | whd in ⊢ (% → %) |
---|
134 | whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]) |
---|
135 | >lookup_add_miss |
---|
136 | [ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ] |
---|
137 | qed. |
---|
138 | |
---|
139 | include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *) |
---|
140 | |
---|
141 | lemma characterise_vars_all : ∀l,f,vars,n. |
---|
142 | characterise_vars l f = 〈vars,n〉 → |
---|
143 | ∀i. local_id vars i → |
---|
144 | Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f). |
---|
145 | #globals #f |
---|
146 | whd in ⊢ (∀_.∀_.??%? → ?) |
---|
147 | elim (fn_params f @ fn_vars f) |
---|
148 | [ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind |
---|
149 | elim globals in H |
---|
150 | [ normalize // |
---|
151 | | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H) |
---|
152 | ] |
---|
153 | | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i |
---|
154 | cases (identifier_eq ? id i) |
---|
155 | [ #E' <E' #H % @refl |
---|
156 | | #NE #H whd %2 >(contract_pair var_types nat ?) in E; |
---|
157 | whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) |
---|
158 | cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?) |
---|
159 | #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2 |
---|
160 | @(IH m0 n0) |
---|
161 | [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ |
---|
162 | | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE |
---|
163 | ] |
---|
164 | ] |
---|
165 | ] qed. |
---|
166 | |
---|
167 | include "Cminor/syntax.ma". |
---|
168 | include "common/Errors.ma". |
---|
169 | |
---|
170 | alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". |
---|
171 | |
---|
172 | axiom BadlyTypedAccess : String. |
---|
173 | axiom BadLvalue : String. |
---|
174 | axiom MissingField : String. |
---|
175 | |
---|
176 | alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)". |
---|
177 | alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)". |
---|
178 | |
---|
179 | (* XXX: For some reason matita refuses to pick the right one unless forced. *) |
---|
180 | alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)". |
---|
181 | |
---|
182 | definition translate_unop : type → CLunop → res CMunop ≝ |
---|
183 | λty.λop:CLunop. |
---|
184 | match op with |
---|
185 | [ Onotbool ⇒ OK ? CMnotbool |
---|
186 | | Onotint ⇒ OK ? Onotint |
---|
187 | | Oneg ⇒ |
---|
188 | match ty with |
---|
189 | [ Tint _ _ ⇒ OK ? Onegint |
---|
190 | | Tfloat _ ⇒ OK ? Onegf |
---|
191 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
192 | ] |
---|
193 | ]. |
---|
194 | |
---|
195 | definition translate_add ≝ |
---|
196 | λty1,e1,ty2,e2,ty'. |
---|
197 | let ty1' ≝ typ_of_type ty1 in |
---|
198 | let ty2' ≝ typ_of_type ty2 in |
---|
199 | match classify_add ty1 ty2 with |
---|
200 | [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2) |
---|
201 | | add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2) |
---|
202 | (* XXX using the integer size for e2 as the offset's size isn't right, because |
---|
203 | if e2 produces an 8bit value then the true offset might overflow *) |
---|
204 | | add_case_pi ty ⇒ |
---|
205 | match ty2' with |
---|
206 | [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty)))))) |
---|
207 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
208 | ] |
---|
209 | | add_case_ip ty ⇒ |
---|
210 | match ty1' with |
---|
211 | [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty)))))) |
---|
212 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
213 | ] |
---|
214 | | add_default ⇒ Error ? (msg TypeMismatch) |
---|
215 | ]. |
---|
216 | |
---|
217 | definition translate_sub ≝ |
---|
218 | λty1,e1,ty2,e2,ty'. |
---|
219 | let ty1' ≝ typ_of_type ty1 in |
---|
220 | let ty2' ≝ typ_of_type ty2 in |
---|
221 | match classify_sub ty1 ty2 with |
---|
222 | [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2) |
---|
223 | | sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2) |
---|
224 | (* XXX choosing offset sizes? *) |
---|
225 | | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) |
---|
226 | | sub_case_pp ty ⇒ |
---|
227 | match ty' with (* XXX overflow *) |
---|
228 | [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty))))) |
---|
229 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
230 | ] |
---|
231 | | sub_default ⇒ Error ? (msg TypeMismatch) |
---|
232 | ]. |
---|
233 | |
---|
234 | definition translate_mul ≝ |
---|
235 | λty1,e1,ty2,e2,ty'. |
---|
236 | let ty1' ≝ typ_of_type ty1 in |
---|
237 | let ty2' ≝ typ_of_type ty2 in |
---|
238 | match classify_mul ty1 ty2 with |
---|
239 | [ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2) |
---|
240 | | mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2) |
---|
241 | | mul_default ⇒ Error ? (msg TypeMismatch) |
---|
242 | ]. |
---|
243 | |
---|
244 | definition translate_div ≝ |
---|
245 | λty1,e1,ty2,e2,ty'. |
---|
246 | let ty1' ≝ typ_of_type ty1 in |
---|
247 | let ty2' ≝ typ_of_type ty2 in |
---|
248 | match classify_div ty1 ty2 with |
---|
249 | [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) |
---|
250 | | div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2) |
---|
251 | | div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2) |
---|
252 | | div_default ⇒ Error ? (msg TypeMismatch) |
---|
253 | ]. |
---|
254 | |
---|
255 | definition translate_mod ≝ |
---|
256 | λty1,e1,ty2,e2,ty'. |
---|
257 | let ty1' ≝ typ_of_type ty1 in |
---|
258 | let ty2' ≝ typ_of_type ty2 in |
---|
259 | match classify_mod ty1 ty2 with |
---|
260 | [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) |
---|
261 | | mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2) |
---|
262 | | mod_default ⇒ Error ? (msg TypeMismatch) |
---|
263 | ]. |
---|
264 | |
---|
265 | definition translate_shr ≝ |
---|
266 | λty1,e1,ty2,e2,ty'. |
---|
267 | let ty1' ≝ typ_of_type ty1 in |
---|
268 | let ty2' ≝ typ_of_type ty2 in |
---|
269 | match classify_shr ty1 ty2 with |
---|
270 | [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) |
---|
271 | | shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2) |
---|
272 | | shr_default ⇒ Error ? (msg TypeMismatch) |
---|
273 | ]. |
---|
274 | |
---|
275 | definition translate_cmp ≝ |
---|
276 | λc,ty1,e1,ty2,e2,ty'. |
---|
277 | let ty1' ≝ typ_of_type ty1 in |
---|
278 | let ty2' ≝ typ_of_type ty2 in |
---|
279 | match classify_cmp ty1 ty2 with |
---|
280 | [ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2) |
---|
281 | | cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2) |
---|
282 | | cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2) |
---|
283 | | cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2) |
---|
284 | | cmp_default ⇒ Error ? (msg TypeMismatch) |
---|
285 | ]. |
---|
286 | |
---|
287 | definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝ |
---|
288 | λop,ty1,e1,ty2,e2,ty. |
---|
289 | let ty' ≝ typ_of_type ty in |
---|
290 | match op with |
---|
291 | [ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty' |
---|
292 | | Osub ⇒ translate_sub ty1 e1 ty2 e2 ty' |
---|
293 | | Omul ⇒ translate_mul ty1 e1 ty2 e2 ty' |
---|
294 | | Omod ⇒ translate_mod ty1 e1 ty2 e2 ty' |
---|
295 | | Odiv ⇒ translate_div ty1 e1 ty2 e2 ty' |
---|
296 | | Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2) |
---|
297 | | Oor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2) |
---|
298 | | Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2) |
---|
299 | | Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2) |
---|
300 | | Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty' |
---|
301 | | Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty' |
---|
302 | | One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty' |
---|
303 | | Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty' |
---|
304 | | Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty' |
---|
305 | | Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty' |
---|
306 | | Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty' |
---|
307 | ]. |
---|
308 | |
---|
309 | lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. |
---|
310 | expr_vars ? e1 P → |
---|
311 | expr_vars ? e2 P → |
---|
312 | translate_binop op ty1 e1 ty2 e2 ty = OK ? e → |
---|
313 | expr_vars ? e P. |
---|
314 | #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 |
---|
315 | whd in ⊢ (??%? → ?) |
---|
316 | [ cases (classify_add ty1 ty2) |
---|
317 | [ 3,4: #z ] whd in ⊢ (??%? → ?) |
---|
318 | [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?) |
---|
319 | * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) |
---|
320 | whd in c:(??%?); destruct % [ @H1 | % // @H2 ] |
---|
321 | | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?) |
---|
322 | * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) |
---|
323 | whd in c:(??%?); destruct % [ @H2 | % // @H1 ] |
---|
324 | | *: #E destruct (E) % try @H1 @H2 |
---|
325 | ] |
---|
326 | | cases (classify_sub ty1 ty2) |
---|
327 | [ 3,4: #z] whd in ⊢ (??%? → ?) |
---|
328 | [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?) |
---|
329 | * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) |
---|
330 | whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I |
---|
331 | | *: #E destruct (E) % try @H1 try @H2 % // @H2 |
---|
332 | ] |
---|
333 | | cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct |
---|
334 | % try @H1 @H2 |
---|
335 | | cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct |
---|
336 | % try @H1 @H2 |
---|
337 | | cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct |
---|
338 | % try @H1 @H2 |
---|
339 | | 6,7,8,9: #E destruct % try @H1 @H2 |
---|
340 | | cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 |
---|
341 | | 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 |
---|
342 | ] qed. |
---|
343 | |
---|
344 | (* We'll need to implement proper translation of pointers if we really do memory |
---|
345 | spaces. *) |
---|
346 | definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝ |
---|
347 | λr1,r2,P. |
---|
348 | match r1 return λx.P x → res (P r2) with |
---|
349 | [ Any ⇒ match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
350 | | Data ⇒ match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
351 | | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
352 | | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
353 | | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
354 | | Code ⇒ match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
355 | ]. |
---|
356 | |
---|
357 | definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ |
---|
358 | λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. |
---|
359 | |
---|
360 | definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ |
---|
361 | λP,ty1,ty2. |
---|
362 | match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with |
---|
363 | [ Tint sz1 sg1 ⇒ λe. |
---|
364 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
365 | [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e) |
---|
366 | | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e) |
---|
367 | | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e) |
---|
368 | | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e) |
---|
369 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
370 | ] |
---|
371 | | Tfloat sz1 ⇒ λe. |
---|
372 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
373 | [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?» |
---|
374 | | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *) |
---|
375 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
376 | ] |
---|
377 | | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) |
---|
378 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with |
---|
379 | [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?» |
---|
380 | | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e |
---|
381 | | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e |
---|
382 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
383 | ] |
---|
384 | | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) |
---|
385 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
386 | [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?» |
---|
387 | | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e |
---|
388 | | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e |
---|
389 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
390 | ] |
---|
391 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
392 | ]. whd @use_sig qed. |
---|
393 | |
---|
394 | definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ |
---|
395 | λty1,ty2,P,p. |
---|
396 | do E ← assert_type_eq ty1 ty2; |
---|
397 | OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). |
---|
398 | |
---|
399 | definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2). |
---|
400 | * * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
401 | qed. |
---|
402 | |
---|
403 | definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). |
---|
404 | * [ #sz1 #sg1 | #r1 | #sz1 ] |
---|
405 | * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ] |
---|
406 | [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ] |
---|
407 | *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
408 | | *; #P #p @(region_should_eq r1 ?? p) |
---|
409 | | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
410 | ] qed. |
---|
411 | |
---|
412 | |
---|
413 | lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r. |
---|
414 | * |
---|
415 | [ 5: #r #ty #n #r' normalize #E destruct @refl |
---|
416 | | 6: #args #ret #r normalize #E destruct @refl |
---|
417 | | *: normalize #a #b try #c try #d destruct |
---|
418 | [ cases a in d; normalize; cases b; normalize #E destruct |
---|
419 | | cases a in c; normalize #E destruct |
---|
420 | ] |
---|
421 | ] qed. |
---|
422 | |
---|
423 | let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝ |
---|
424 | match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with |
---|
425 | [ Expr ed ty ⇒ |
---|
426 | match ed with |
---|
427 | [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?» |
---|
428 | | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» |
---|
429 | | Evar id ⇒ |
---|
430 | do c as E ← lookup' vars id; |
---|
431 | match c return λx.? = ? → res (Σe':CMexpr ?. ?) with |
---|
432 | [ Global r ⇒ λ_. |
---|
433 | match access_mode ty with |
---|
434 | [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» |
---|
435 | | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» |
---|
436 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
437 | ] |
---|
438 | | Stack n ⇒ λE. |
---|
439 | match access_mode ty with |
---|
440 | [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?» |
---|
441 | | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?» |
---|
442 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
443 | ] |
---|
444 | | Local ⇒ λE. OK ? «Id ? id, ?» |
---|
445 | ] E |
---|
446 | | Ederef e1 ⇒ |
---|
447 | do e1' ← translate_expr vars e1; |
---|
448 | match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with |
---|
449 | [ ASTptr r ⇒ λe1'. |
---|
450 | match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with |
---|
451 | [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?» |
---|
452 | | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; |
---|
453 | OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉ |
---|
454 | | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) |
---|
455 | ] (access_mode_typ ty) |
---|
456 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
457 | ] e1' |
---|
458 | | Eaddrof e1 ⇒ |
---|
459 | do e1' ← translate_addr vars e1; |
---|
460 | match typ_of_type ty return λx.res (Σz:CMexpr x.?) with |
---|
461 | [ ASTptr r ⇒ |
---|
462 | match e1' with |
---|
463 | [ dp r1 e1' ⇒ region_should_eq r1 r ? e1' |
---|
464 | ] |
---|
465 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
466 | ] |
---|
467 | | Eunop op e1 ⇒ |
---|
468 | do op' ← translate_unop ty op; |
---|
469 | do e1' ← translate_expr vars e1; |
---|
470 | OK ? «Op1 ?? op' e1', ?» |
---|
471 | | Ebinop op e1 e2 ⇒ |
---|
472 | do e1' ← translate_expr vars e1; |
---|
473 | do e2' ← translate_expr vars e2; |
---|
474 | do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty; |
---|
475 | OK ? «e', ?» |
---|
476 | | Ecast ty1 e1 ⇒ |
---|
477 | do e1' ← translate_expr vars e1; |
---|
478 | do e' ← translate_cast ? (typeof e1) ty1 e1'; |
---|
479 | do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e'; |
---|
480 | OK ? e' |
---|
481 | | Econdition e1 e2 e3 ⇒ |
---|
482 | do e1' ← translate_expr vars e1; |
---|
483 | do e2' ← translate_expr vars e2; |
---|
484 | do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
485 | do e3' ← translate_expr vars e3; |
---|
486 | do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3'; |
---|
487 | match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with |
---|
488 | [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?» |
---|
489 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
490 | ] e1' |
---|
491 | | Eandbool e1 e2 ⇒ |
---|
492 | do e1' ← translate_expr vars e1; |
---|
493 | do e2' ← translate_expr vars e2; |
---|
494 | match ty with |
---|
495 | [ Tint sz _ ⇒ |
---|
496 | do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
497 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with |
---|
498 | [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?» |
---|
499 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
500 | ] e1' |
---|
501 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
502 | ] |
---|
503 | | Eorbool e1 e2 ⇒ |
---|
504 | do e1' ← translate_expr vars e1; |
---|
505 | do e2' ← translate_expr vars e2; |
---|
506 | match ty with |
---|
507 | [ Tint sz _ ⇒ |
---|
508 | do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
509 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with |
---|
510 | [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?» |
---|
511 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
512 | ] e1' |
---|
513 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
514 | ] |
---|
515 | | Esizeof ty1 ⇒ |
---|
516 | match ty with |
---|
517 | [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?» |
---|
518 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
519 | ] |
---|
520 | | Efield e1 id ⇒ |
---|
521 | match typeof e1 with |
---|
522 | [ Tstruct _ fl ⇒ |
---|
523 | do e1' ← translate_addr vars e1; |
---|
524 | match e1' with |
---|
525 | [ dp r e1' ⇒ |
---|
526 | do off ← field_offset id fl; |
---|
527 | match access_mode ty with |
---|
528 | [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?» |
---|
529 | | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?» |
---|
530 | | By_nothing ⇒ Error ? (msg BadlyTypedAccess) |
---|
531 | ] |
---|
532 | ] |
---|
533 | | Tunion _ _ ⇒ |
---|
534 | do e1' ← translate_addr vars e1; |
---|
535 | match e1' with |
---|
536 | [ dp r e1' ⇒ |
---|
537 | match access_mode ty return λx. access_mode ty = x → res ? with |
---|
538 | [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?» |
---|
539 | | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1'; |
---|
540 | OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉ |
---|
541 | | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) |
---|
542 | ] (refl ? (access_mode ty)) |
---|
543 | ] |
---|
544 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
545 | ] |
---|
546 | | Ecost l e1 ⇒ |
---|
547 | do e1' ← translate_expr vars e1; |
---|
548 | do e' ← OK ? «Ecost ? l e1',?»; |
---|
549 | typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' |
---|
550 | ] |
---|
551 | ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ |
---|
552 | match e with |
---|
553 | [ Expr ed _ ⇒ |
---|
554 | match ed with |
---|
555 | [ Evar id ⇒ |
---|
556 | do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); |
---|
557 | match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with |
---|
558 | [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»» |
---|
559 | | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»» |
---|
560 | | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *) |
---|
561 | ] |
---|
562 | | Ederef e1 ⇒ |
---|
563 | do e1' ← translate_expr vars e1; |
---|
564 | match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with |
---|
565 | [ ASTptr r ⇒ λe1'.OK ? «r, e1'» |
---|
566 | | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) |
---|
567 | ] e1' |
---|
568 | | Efield e1 id ⇒ |
---|
569 | match typeof e1 with |
---|
570 | [ Tstruct _ fl ⇒ |
---|
571 | do e1' ← translate_addr vars e1; |
---|
572 | do off ← field_offset id fl; |
---|
573 | match e1' with |
---|
574 | [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ») |
---|
575 | ] |
---|
576 | | Tunion _ _ ⇒ translate_addr vars e1 |
---|
577 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
578 | ] |
---|
579 | | _ ⇒ Error ? (msg BadLvalue) |
---|
580 | ] |
---|
581 | ]. |
---|
582 | whd try @I |
---|
583 | [ >E @I |
---|
584 | | >(E ? (refl ??)) @refl |
---|
585 | | 3,4: @use_sig |
---|
586 | | @(translate_binop_vars … E) @use_sig |
---|
587 | | % [ % ] @use_sig |
---|
588 | | % [ % @use_sig ] whd @I |
---|
589 | | % [ % [ @use_sig | @I ] | @use_sig ] |
---|
590 | | % [ @use_sig | @I ] |
---|
591 | | % [ @use_sig | @I ] |
---|
592 | | >(access_mode_typ … E) @refl |
---|
593 | | @use_sig |
---|
594 | | @use_sig |
---|
595 | | % [ @use_sig | @I ] |
---|
596 | ] qed. |
---|
597 | |
---|
598 | inductive destination (vars:var_types) : Type[0] ≝ |
---|
599 | | IdDest : ∀id:ident. local_id vars id → destination vars |
---|
600 | | MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. |
---|
601 | |
---|
602 | definition translate_dest ≝ |
---|
603 | λvars,e1,ty2. |
---|
604 | do q ← match access_mode ty2 with |
---|
605 | [ By_value q ⇒ OK ? q |
---|
606 | | By_reference r ⇒ OK ? (Mpointer r) |
---|
607 | | By_nothing ⇒ Error ? (msg BadlyTypedAccess) |
---|
608 | ]; |
---|
609 | match e1 with |
---|
610 | [ Expr ed1 ty1 ⇒ |
---|
611 | match ed1 with |
---|
612 | [ Evar id ⇒ |
---|
613 | do c as E ← lookup' vars id; |
---|
614 | match c return λx.? → ? with |
---|
615 | [ Local ⇒ λE. OK ? (IdDest vars id ?) |
---|
616 | | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0))) |
---|
617 | | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n))) |
---|
618 | ] E |
---|
619 | | _ ⇒ |
---|
620 | do e1' ← translate_addr vars e1; |
---|
621 | match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ] |
---|
622 | ] |
---|
623 | ]. |
---|
624 | whd // >E @I |
---|
625 | qed. |
---|
626 | |
---|
627 | definition lenv ≝ identifier_map SymbolTag (identifier Label). |
---|
628 | |
---|
629 | axiom MissingLabel : String. |
---|
630 | |
---|
631 | definition lookup_label ≝ |
---|
632 | λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). |
---|
633 | |
---|
634 | definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l. |
---|
635 | |
---|
636 | let rec labels_defined (s:statement) : list ident ≝ |
---|
637 | match s with |
---|
638 | [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 |
---|
639 | | Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 |
---|
640 | | Swhile _ s ⇒ labels_defined s |
---|
641 | | Sdowhile _ s ⇒ labels_defined s |
---|
642 | | Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 |
---|
643 | | Sswitch _ ls ⇒ labels_defined_switch ls |
---|
644 | | Slabel l s ⇒ l::(labels_defined s) |
---|
645 | | Scost _ s ⇒ labels_defined s |
---|
646 | | _ ⇒ [ ] |
---|
647 | ] |
---|
648 | and labels_defined_switch (ls:labeled_statements) : list ident ≝ |
---|
649 | match ls with |
---|
650 | [ LSdefault s ⇒ labels_defined s |
---|
651 | | LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls |
---|
652 | ]. |
---|
653 | |
---|
654 | definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). |
---|
655 | |
---|
656 | definition labels_translated : lenv → statement → stmt → Prop ≝ |
---|
657 | λlbls,s,s'. ∀l. |
---|
658 | (Exists ? (λl'.l' = l) (labels_defined s)) → |
---|
659 | ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'. |
---|
660 | |
---|
661 | definition stmt_inv ≝ |
---|
662 | λvars. λlbls:lenv. |
---|
663 | stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s). |
---|
664 | |
---|
665 | definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝ |
---|
666 | λvars,e1,e2. |
---|
667 | do e2' ← translate_expr vars e2; |
---|
668 | do dest ← translate_dest vars e1 (typeof e2); |
---|
669 | match dest with |
---|
670 | [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?» |
---|
671 | | MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» |
---|
672 | ]. |
---|
673 | #ls whd % |
---|
674 | [ % // @use_sig |
---|
675 | | @I |
---|
676 | | % @use_sig |
---|
677 | | @I |
---|
678 | ] qed. |
---|
679 | |
---|
680 | definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ |
---|
681 | λA,B,f,oa. |
---|
682 | match oa with |
---|
683 | [ None ⇒ OK ? (None ?) |
---|
684 | | Some a ⇒ do b ← f a; OK ? (Some ? b) |
---|
685 | ]. |
---|
686 | |
---|
687 | definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝ |
---|
688 | λv,e. |
---|
689 | do e' ← translate_expr v e; |
---|
690 | OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?». |
---|
691 | whd @use_sig |
---|
692 | qed. |
---|
693 | |
---|
694 | axiom FIXME : String. |
---|
695 | |
---|
696 | record tmpgen : Type[0] ≝ { |
---|
697 | tmp_universe : universe SymbolTag; |
---|
698 | tmp_env : list (ident × typ) |
---|
699 | }. |
---|
700 | |
---|
701 | definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝ |
---|
702 | λc,g. |
---|
703 | let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in |
---|
704 | 〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉. |
---|
705 | |
---|
706 | lemma lookup_label_hit : ∀lbls,l,l'. |
---|
707 | lookup_label lbls l = OK ? l' → |
---|
708 | lpresent lbls l'. |
---|
709 | #lbls #l #l' #E whd %{l} @E |
---|
710 | qed. |
---|
711 | |
---|
712 | definition add_tmps : var_types → tmpgen → var_types ≝ |
---|
713 | λvs,g. |
---|
714 | foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g). |
---|
715 | |
---|
716 | definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝ |
---|
717 | λvars,u1,u2. |
---|
718 | ∀id. local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id. |
---|
719 | |
---|
720 | lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q. |
---|
721 | 〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'. |
---|
722 | #tmp #g #g' #vars #q |
---|
723 | whd in ⊢ (???% → ?) |
---|
724 | generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) |
---|
725 | * #tmp' #u whd in ⊢ (???% → ?) #E |
---|
726 | >(pair_eq2 ?????? E) |
---|
727 | #id #H |
---|
728 | whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] |
---|
729 | cases (identifier_eq ? id tmp') |
---|
730 | [ #E1 >E1 >lookup_add_hit @I |
---|
731 | | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1) |
---|
732 | ] qed. |
---|
733 | |
---|
734 | definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝ |
---|
735 | λvars,lbls,s,u,su'. |
---|
736 | let 〈s',u'〉 ≝ su' in |
---|
737 | stmt_inv (add_tmps vars u') lbls s' ∧ |
---|
738 | labels_translated lbls s s' ∧ |
---|
739 | tmps_preserved vars u u'. |
---|
740 | |
---|
741 | lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su. |
---|
742 | trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su). |
---|
743 | #var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1 |
---|
744 | qed. |
---|
745 | |
---|
746 | lemma trans_inv_labels : ∀vars,lbls,s,u,su. |
---|
747 | trans_inv vars lbls s u su → labels_translated lbls s (\fst su). |
---|
748 | #vars #lbls #s #u * #s' #u' * * #_ #H #_ @H |
---|
749 | qed. |
---|
750 | |
---|
751 | lemma local_id_add_local_oblivious : ∀vars,id,id'. |
---|
752 | local_id vars id → local_id (add ?? vars id' Local) id. |
---|
753 | #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) |
---|
754 | cases (identifier_eq ? id id') |
---|
755 | [ #E >E >lookup_add_hit @I |
---|
756 | | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E) |
---|
757 | ] qed. |
---|
758 | |
---|
759 | lemma local_id_add_tmps_oblivious : ∀vars,id,u. |
---|
760 | local_id vars id → local_id (add_tmps vars u) id. |
---|
761 | #vars #id * #u #l #H elim l |
---|
762 | [ // |
---|
763 | | * #id' #ty #tl @local_id_add_local_oblivious |
---|
764 | ] qed. |
---|
765 | |
---|
766 | lemma add_tmps_oblivious : ∀vars,lbls,s,u. |
---|
767 | stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s. |
---|
768 | #vars #lbls #s #u #H |
---|
769 | @(stmt_P_mp … H) |
---|
770 | #s' * #H1 #H2 % |
---|
771 | [ @(stmt_vars_mp … H1) |
---|
772 | #id @local_id_add_tmps_oblivious |
---|
773 | | @H2 |
---|
774 | ] qed. |
---|
775 | |
---|
776 | lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars. |
---|
777 | 〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp. |
---|
778 | #tmp #u #q #u0 #vars |
---|
779 | whd in ⊢ (???% → ?) |
---|
780 | generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) |
---|
781 | * #tmp' #u' whd in ⊢ (???% → ?) #E |
---|
782 | >(pair_eq1 ?????? E) >(pair_eq2 ?????? E) |
---|
783 | whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit |
---|
784 | @I |
---|
785 | qed. |
---|
786 | |
---|
787 | lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x. |
---|
788 | #A #P #P' #H1 * #x #H2 @H1 @H2 |
---|
789 | qed. |
---|
790 | |
---|
791 | definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝ |
---|
792 | λA,B,C,P,e,f. |
---|
793 | match e with |
---|
794 | [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ] |
---|
795 | | Error msg ⇒ Error ? msg |
---|
796 | ]. |
---|
797 | |
---|
798 | notation > "vbox('do' 〈ident v1, ident v2〉 'with' ident H ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}. |
---|
799 | (* |
---|
800 | notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. |
---|
801 | notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. |
---|
802 | notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. |
---|
803 | *) |
---|
804 | interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f). |
---|
805 | |
---|
806 | let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝ |
---|
807 | match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with |
---|
808 | [ Sskip ⇒ OK ? «〈St_skip, u〉, ?» |
---|
809 | | Sassign e1 e2 ⇒ |
---|
810 | do s' ← translate_assign vars e1 e2; |
---|
811 | OK ? «〈eject ?? s', u〉, ?» |
---|
812 | | Scall ret ef args ⇒ |
---|
813 | do ef' ← translate_expr vars ef; |
---|
814 | do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef'; |
---|
815 | do args' ← mmap_sigma … (translate_expr_sigma vars) args; |
---|
816 | match ret with |
---|
817 | [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?» |
---|
818 | | Some e1 ⇒ |
---|
819 | do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) |
---|
820 | match dest with |
---|
821 | [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?» |
---|
822 | | MemDest r q e1' ⇒ |
---|
823 | let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in |
---|
824 | OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?» |
---|
825 | ] |
---|
826 | ] |
---|
827 | | Ssequence s1 s2 ⇒ |
---|
828 | do 〈s1', u1〉 with H1 ← translate_statement vars lbls u s1; |
---|
829 | do 〈s2', u2〉 with H2 ← translate_statement vars lbls u1 s2; |
---|
830 | OK ? «〈St_seq s1' s2', u2〉, ?» |
---|
831 | | Sifthenelse e1 s1 s2 ⇒ |
---|
832 | do e1' ← translate_expr vars e1; |
---|
833 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with |
---|
834 | [ ASTint _ _ ⇒ λe1'. |
---|
835 | do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; |
---|
836 | do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2; |
---|
837 | OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?» |
---|
838 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
839 | ] e1' |
---|
840 | | Swhile e1 s1 ⇒ |
---|
841 | do e1' ← translate_expr vars e1; |
---|
842 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with |
---|
843 | [ ASTint _ _ ⇒ λe1'. |
---|
844 | do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; |
---|
845 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
846 | OK ? «〈St_block |
---|
847 | (St_loop |
---|
848 | (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?» |
---|
849 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
850 | ] e1' |
---|
851 | | Sdowhile e1 s1 ⇒ |
---|
852 | do e1' ← translate_expr vars e1; |
---|
853 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with |
---|
854 | [ ASTint _ _ ⇒ λe1'. |
---|
855 | do 〈s1',u〉 with H1 ← translate_statement vars lbls u s1; |
---|
856 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
857 | OK ? «〈St_block |
---|
858 | (St_loop |
---|
859 | (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?» |
---|
860 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
861 | ] e1' |
---|
862 | | Sfor s1 e1 s2 s3 ⇒ |
---|
863 | do e1' ← translate_expr vars e1; |
---|
864 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with |
---|
865 | [ ASTint _ _ ⇒ λe1'. |
---|
866 | do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; |
---|
867 | do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2; |
---|
868 | do 〈s3', u〉 with H3 ← translate_statement vars lbls u s3; |
---|
869 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
870 | OK ? «〈St_seq s1' |
---|
871 | (St_block |
---|
872 | (St_loop |
---|
873 | (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?» |
---|
874 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
875 | ] e1' |
---|
876 | | Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?» |
---|
877 | | Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?» |
---|
878 | | Sreturn ret ⇒ |
---|
879 | match ret with |
---|
880 | [ None ⇒ OK ? «〈St_return (None ?), u〉, ?» |
---|
881 | | Some e1 ⇒ |
---|
882 | do e1' ← translate_expr vars e1; |
---|
883 | OK ? «〈St_return (Some ? (dp … e1')), u〉, ?» |
---|
884 | ] |
---|
885 | | Sswitch e1 ls ⇒ Error ? (msg FIXME) |
---|
886 | | Slabel l s1 ⇒ |
---|
887 | do l' as E ← lookup_label lbls l; |
---|
888 | do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; |
---|
889 | OK ? «〈St_label l' s1', u〉, ?» |
---|
890 | | Sgoto l ⇒ |
---|
891 | do l' as E ← lookup_label lbls l; |
---|
892 | OK ? «〈St_goto l', u〉, ?» |
---|
893 | | Scost l s1 ⇒ |
---|
894 | do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1; |
---|
895 | OK ? «〈St_cost l s1', u〉, ?» |
---|
896 | ]. |
---|
897 | try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj |
---|
898 | try @I |
---|
899 | try (#l #H @(match H in False with [ ])) |
---|
900 | try (#id #H @H) |
---|
901 | [ @add_tmps_oblivious @(use_sig ?? s') |
---|
902 | | @local_id_add_tmps_oblivious @p |
---|
903 | ] |
---|
904 | try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious) |
---|
905 | [ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious |
---|
906 | | 2,4: @(local_id_fresh_tmp … Etmp) |
---|
907 | | @(alloc_tmp_preserves … Etmp) |
---|
908 | | 7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H | *: @H4 ] |
---|
909 | | 8,12: @(trans_inv_stmt_inv … H2) |
---|
910 | | 9,13: #l #H cases (Exists_append … H) |
---|
911 | [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1 |
---|
912 | %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ] |
---|
913 | | *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2 |
---|
914 | %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ] |
---|
915 | ] |
---|
916 | | 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L |
---|
917 | | 15,18: @(π1 (π1 H1)) |
---|
918 | | 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1 |
---|
919 | %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ] |
---|
920 | | 17,20: @(π2 H1) |
---|
921 | (* Sfor *) |
---|
922 | | @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ] |
---|
923 | | @(π1 (π1 H3)) |
---|
924 | | @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ] |
---|
925 | | #l #H cases (Exists_append … H) |
---|
926 | [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1 |
---|
927 | %{l'} % [ @E1 | @Exists_append_l @D1 ] |
---|
928 | | #EX cases (Exists_append … EX) |
---|
929 | [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2 |
---|
930 | %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ] |
---|
931 | | #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3 |
---|
932 | %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ] |
---|
933 | ] |
---|
934 | ] |
---|
935 | | #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H |
---|
936 | (* Slabel *) |
---|
937 | | %{l} @E |
---|
938 | | @(π1 (π1 H1)) |
---|
939 | | #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ] |
---|
940 | | @(π2 H1) |
---|
941 | (* Sgoto *) |
---|
942 | | %{l} @E |
---|
943 | | @(π1 (π1 H1)) |
---|
944 | (* Scost *) |
---|
945 | | @(π2 (π1 H1)) |
---|
946 | | @(π2 H1) |
---|
947 | ] qed. |
---|
948 | |
---|
949 | |
---|
950 | axiom ParamGlobalMixup : String. |
---|
951 | |
---|
952 | (* ls and s0 aren't real parameters, they're just there for giving the invariant. *) |
---|
953 | definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝ |
---|
954 | λvars,ls,s0,u,params,s. foldl ?? (λsu,it. |
---|
955 | let 〈id,ty〉 ≝ it in |
---|
956 | do 〈s,u〉 with Is ← su; |
---|
957 | do t as E ← lookup' vars id; |
---|
958 | match t return λx.? → ? with |
---|
959 | [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is» |
---|
960 | | Stack n ⇒ λE. |
---|
961 | do q ← match access_mode ty with |
---|
962 | [ By_value q ⇒ OK ? q |
---|
963 | | By_reference r ⇒ OK ? (Mpointer r) |
---|
964 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
965 | ]; |
---|
966 | OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?» |
---|
967 | | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] |
---|
968 | ] E) (OK ? s) params. |
---|
969 | try @conj try @conj try @conj try @conj try @conj try @conj |
---|
970 | try @I |
---|
971 | [ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I |
---|
972 | | @(π1 (π1 Is)) |
---|
973 | | @(π2 (π1 Is)) |
---|
974 | | @(π2 Is) |
---|
975 | ] qed. |
---|
976 | |
---|
977 | (* |
---|
978 | lemma local_id_add_local : ∀vars,id,id'. |
---|
979 | local_id vars id → |
---|
980 | local_id (add ?? vars id' Local) id. |
---|
981 | #vars #id #id' #H |
---|
982 | whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id') |
---|
983 | [ #E < E >lookup_add_hit // |
---|
984 | | #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/ |
---|
985 | ] qed. |
---|
986 | *) |
---|
987 | axiom DuplicateLabel : String. |
---|
988 | |
---|
989 | definition lenv_list_inv : lenv → lenv → list ident → Prop ≝ |
---|
990 | λlbls0,lbls,ls. |
---|
991 | ∀l,l'. lookup_label lbls l = OK ? l' → |
---|
992 | Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'. |
---|
993 | |
---|
994 | lemma lookup_label_add : ∀lbls,l,l'. |
---|
995 | lookup_label (add … lbls l l') l = OK ? l'. |
---|
996 | #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl |
---|
997 | qed. |
---|
998 | |
---|
999 | lemma lookup_label_miss : ∀lbls,l,l',l0. |
---|
1000 | l0 ≠ l → |
---|
1001 | lookup_label (add … lbls l l') l0 = lookup_label lbls l0. |
---|
1002 | #lbls #l #l' #l0 * #NE |
---|
1003 | whd in ⊢ (??%%) |
---|
1004 | >lookup_add_miss |
---|
1005 | [ @refl | @(eq_identifier_elim ?? l0 l) |
---|
1006 | [ #E cases (NE E) |
---|
1007 | | #_ @I |
---|
1008 | ] |
---|
1009 | ] |
---|
1010 | qed. |
---|
1011 | |
---|
1012 | let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝ |
---|
1013 | match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with |
---|
1014 | [ nil ⇒ OK ? «lbls, ?» |
---|
1015 | | cons l t ⇒ |
---|
1016 | match lookup_label lbls l return λx.lookup_label lbls l = x → ? with |
---|
1017 | [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel) |
---|
1018 | | Error _ ⇒ λLOOK. |
---|
1019 | let 〈l',u1〉 ≝ fresh … u in |
---|
1020 | do lbls1 ← populate_lenv t (add … lbls l l') u1; |
---|
1021 | OK ? «eject … lbls1, ?» |
---|
1022 | ] (refl ? (lookup_label lbls l)) |
---|
1023 | ]. |
---|
1024 | [ #l #l' #H %2 @H |
---|
1025 | | cases lbls1 #lbls' #I whd in ⊢ (??%?) |
---|
1026 | #l1 #l1' #E1 @(eq_identifier_elim … l l1) |
---|
1027 | [ #E %1 %1 @E |
---|
1028 | | #NE cases (I l1 l1' E1) |
---|
1029 | [ #H %1 %2 @H |
---|
1030 | | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H |
---|
1031 | ] |
---|
1032 | ] |
---|
1033 | ] qed. |
---|
1034 | |
---|
1035 | definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝ |
---|
1036 | λbody. |
---|
1037 | do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?); |
---|
1038 | OK ? «lbls, ?». |
---|
1039 | #l #l' #E cases (H l l' E) // |
---|
1040 | whd in ⊢ (??%? → ?) #H destruct |
---|
1041 | qed. |
---|
1042 | |
---|
1043 | lemma local_id_split : ∀vars,tmpgen,i. |
---|
1044 | local_id (add_tmps vars tmpgen) i → |
---|
1045 | local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen). |
---|
1046 | #vars #tmpgen #i |
---|
1047 | whd in ⊢ (?%? → ?) |
---|
1048 | elim (tmp_env tmpgen) |
---|
1049 | [ #H %1 @H |
---|
1050 | | * #id #ty #tl #IH |
---|
1051 | cases (identifier_eq ? i id) |
---|
1052 | [ #E >E #H %2 whd %1 @refl |
---|
1053 | | * #NE #H cases (IH ?) |
---|
1054 | [ #H' %1 @H' |
---|
1055 | | #H' %2 %2 @H' |
---|
1056 | | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
1057 | >lookup_add_miss in H; [ #H @H | @eq_identifier_elim // #E cases (NE E) ] |
---|
1058 | ] |
---|
1059 | ] |
---|
1060 | ] qed. |
---|
1061 | |
---|
1062 | lemma Exists_squeeze : ∀A,P,l1,l2,l3. |
---|
1063 | Exists A P (l1@l3) → Exists A P (l1@l2@l3). |
---|
1064 | #A #P #l1 #l2 #l3 #EX |
---|
1065 | cases (Exists_append … EX) |
---|
1066 | [ #EX1 @Exists_append_l @EX1 |
---|
1067 | | #EX3 @Exists_append_r @Exists_append_r @EX3 |
---|
1068 | ] qed. |
---|
1069 | |
---|
1070 | definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝ |
---|
1071 | λtmpuniverse, globals, f. |
---|
1072 | do «lbls, Ilbls» ← build_label_env (fn_body f); |
---|
1073 | let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in |
---|
1074 | let tmp ≝ mk_tmpgen tmpuniverse [ ] in |
---|
1075 | do s ← translate_statement vartypes lbls tmp (fn_body f); |
---|
1076 | do 〈s,tmp〉 with Is ← alloc_params vartypes lbls ?? (fn_params f) s; |
---|
1077 | OK ? (mk_internal_function |
---|
1078 | (opttyp_of_type (fn_return f)) |
---|
1079 | (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f)) |
---|
1080 | ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) |
---|
1081 | stacksize |
---|
1082 | s ?). |
---|
1083 | cases Is * #S #L #TP |
---|
1084 | @(stmt_P_mp ???? S) |
---|
1085 | #s1 * #H1 #H2 % |
---|
1086 | [ @(stmt_vars_mp … H1) |
---|
1087 | #i #H |
---|
1088 | cases (local_id_split … H) |
---|
1089 | [ #H' @Exists_squeeze >map_append |
---|
1090 | @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H' |
---|
1091 | | skip |
---|
1092 | | * #id #ty #E1 <E1 @refl |
---|
1093 | ] |
---|
1094 | | #EX @Exists_append_r @Exists_append_l @EX |
---|
1095 | ] |
---|
1096 | | @(stmt_labels_mp … H2) |
---|
1097 | #l * #l' #LOOKUP |
---|
1098 | lapply (Ilbls l' l LOOKUP) #DEFINED |
---|
1099 | cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex) |
---|
1100 | #H @H |
---|
1101 | ] qed. |
---|
1102 | |
---|
1103 | definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝ |
---|
1104 | λtmpuniverse,globals,f. |
---|
1105 | match f with |
---|
1106 | [ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn') |
---|
1107 | | CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty))) |
---|
1108 | ]. |
---|
1109 | |
---|
1110 | (* TODO: move universe generation to higher level once we do runtime function |
---|
1111 | generation. Cheating a bit - we only need the new identifiers to be fresh |
---|
1112 | for individual functions. *) |
---|
1113 | include "Clight/fresh.ma". |
---|
1114 | |
---|
1115 | definition clight_to_cminor : clight_program → res Cminor_program ≝ |
---|
1116 | λp. |
---|
1117 | let tmpuniverse ≝ universe_for_program p in |
---|
1118 | let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in |
---|
1119 | let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in |
---|
1120 | let globals ≝ fun_globals @ var_globals in |
---|
1121 | transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)). |
---|