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