1 | include "Clight/toCminor.ma". |
---|
2 | |
---|
3 | (* When we characterise the local Clight variables, those that are stack |
---|
4 | allocated are given disjoint regions of the stack. *) |
---|
5 | |
---|
6 | lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty. |
---|
7 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
8 | lookup ?? vartypes id = Some ? 〈Stack n,ty〉 → |
---|
9 | ∀id',n',ty'. id ≠ id' → |
---|
10 | lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 → |
---|
11 | n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'. |
---|
12 | #globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty |
---|
13 | whd in ⊢ (??%? → ?); |
---|
14 | generalize in match vartypes; -vartypes |
---|
15 | generalize in match stacksize; -stacksize |
---|
16 | elim (args@vars) |
---|
17 | [ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct |
---|
18 | elim globals in L; |
---|
19 | [ normalize #L destruct |
---|
20 | | * * #id' #r #ty' #tl #IH |
---|
21 | whd in match (foldr ?????); |
---|
22 | #L cases (lookup_add_cases ??????? L) |
---|
23 | [ * #E1 #E2 destruct |
---|
24 | | @IH |
---|
25 | ] |
---|
26 | ] |
---|
27 | | * #id1 #ty1 #tl #IH #stacksize #vartypes |
---|
28 | whd in match (foldr ?????); |
---|
29 | (* Avoid writing out the definition again *) |
---|
30 | letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %; |
---|
31 | lapply (refl ? ih) whd in match ih; -ih |
---|
32 | cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %); |
---|
33 | #vartypes' #stack' #FOLD #IH |
---|
34 | whd in ⊢ (??(match % with [_⇒?])? → ?); |
---|
35 | cases (orb ??) |
---|
36 | #CHAR whd in CHAR:(??%?); destruct |
---|
37 | #L cases (lookup_add_cases ??????? L) |
---|
38 | [ 1,3: * #E1 #E2 destruct |
---|
39 | #id' #n' #ty' #NE >lookup_add_miss /2/ |
---|
40 | #L' %1 -L -IH |
---|
41 | generalize in match vartypes' in FOLD L' ⊢ %; -vartypes' |
---|
42 | generalize in match stack'; -stack' |
---|
43 | elim tl |
---|
44 | [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥ |
---|
45 | elim globals in L'; |
---|
46 | [ normalize #E destruct |
---|
47 | | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????); |
---|
48 | #L cases (lookup_add_cases ??????? L) |
---|
49 | [ * #E1 #E2 destruct |
---|
50 | | @IH |
---|
51 | ] |
---|
52 | ] |
---|
53 | | * #id2 #ty2 #tl2 #IH #stack' #vartypes' |
---|
54 | whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
55 | #vartypes2 #stack2 #IH |
---|
56 | whd in ⊢ (??%? → ?); |
---|
57 | cases (orb ??) |
---|
58 | [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L) |
---|
59 | [ * #E1 #E2 destruct // |
---|
60 | | #L'' lapply (IH ?? (refl ??) L'') /2/ |
---|
61 | ] |
---|
62 | | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L) |
---|
63 | [ * #E1 #E2 destruct |
---|
64 | | #L'' lapply (IH ?? (refl ??) L'') /2/ |
---|
65 | ] |
---|
66 | ] |
---|
67 | ] |
---|
68 | | -L #L #id' #n' #ty' #NE #L' |
---|
69 | cases (lookup_add_cases ??????? L') |
---|
70 | [ * #E1 #E2 destruct |
---|
71 | %2 -IH -L' |
---|
72 | generalize in match vartypes' in FOLD L; -vartypes' |
---|
73 | generalize in match stack'; -stack' |
---|
74 | elim tl |
---|
75 | [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥ |
---|
76 | elim globals in L; |
---|
77 | [ normalize #E destruct |
---|
78 | | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????); |
---|
79 | #L cases (lookup_add_cases ??????? L) |
---|
80 | [ * #E1 #E2 destruct |
---|
81 | | @IH |
---|
82 | ] |
---|
83 | ] |
---|
84 | | * #id1 #ty1 #tl1 #IH #stack' #vartypes' |
---|
85 | whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
86 | #vartypes2 #stack2 #IH |
---|
87 | whd in ⊢ (??%? → ?); |
---|
88 | cases (orb ??) |
---|
89 | #E whd in E:(??%?); destruct |
---|
90 | #L cases (lookup_add_cases ??????? L) |
---|
91 | [ 1,3: * #E1 #E2 destruct // |
---|
92 | | 2,4: #L' lapply (IH ?? (refl ??) L') /2/ |
---|
93 | ] |
---|
94 | ] |
---|
95 | | @(IH … (refl ??) L … NE) |
---|
96 | ] |
---|
97 | | -L #L #id' #n' #ty' #NE #L' |
---|
98 | cases (lookup_add_cases ??????? L') |
---|
99 | [ * #E1 #E2 destruct |
---|
100 | | @(IH … (refl ??) L … NE) |
---|
101 | ] |
---|
102 | ] |
---|
103 | ] qed. |
---|
104 | |
---|
105 | (* And everything is in the stack frame. *) |
---|
106 | |
---|
107 | lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty. |
---|
108 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
109 | lookup ?? vartypes id = Some ? 〈Stack n,ty〉 → |
---|
110 | n + sizeof ty ≤ stacksize. |
---|
111 | #globals * #ret #args #vars #body whd in match (characterise_vars ??); |
---|
112 | elim (args@vars) |
---|
113 | [ #vartypes #stacksize #id #n #ty #FOLD #L @⊥ |
---|
114 | whd in FOLD:(??%?); destruct elim globals in L; |
---|
115 | [ #E normalize in E; destruct |
---|
116 | | * * #id' #r' #ty' #tl' #IH |
---|
117 | whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L) |
---|
118 | [ * #E1 #E2 destruct |
---|
119 | | @IH |
---|
120 | ] |
---|
121 | ] |
---|
122 | | * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty |
---|
123 | whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
124 | #vartypes' #stackspace' #IH |
---|
125 | whd in ⊢ (??(match % with [_⇒?])? → ?); |
---|
126 | cases (orb ??) whd in ⊢ (??%? → ?); |
---|
127 | #E destruct #L cases (lookup_add_cases ??????? L) |
---|
128 | [ 1,3: * #E1 #E2 destruct // |
---|
129 | | 2,4: #L' lapply (IH … (refl ??) L') /2/ |
---|
130 | ] |
---|
131 | ] qed. |
---|
132 | |
---|
133 | (* Local variables show up in the variable characterisation as local. *) |
---|
134 | |
---|
135 | lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id. |
---|
136 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
137 | Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) → |
---|
138 | ∃t. local_id vartypes id t. |
---|
139 | #globals * #ret #args #vars #body |
---|
140 | whd in match (characterise_vars ??); elim (args@vars) |
---|
141 | [ #vartypes #stacksize #id #_ * |
---|
142 | | * #hd #ty #tl #IH |
---|
143 | #vartypes #stacksize #id |
---|
144 | whd in match (foldr ?????); |
---|
145 | cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
146 | #vartypes' #stackspace' #IH |
---|
147 | whd in ⊢ (??(match % with [_⇒?])? → ?); |
---|
148 | cases (orb ??) |
---|
149 | #E whd in E:(??%?); destruct * |
---|
150 | [ 1,3: #E destruct %{(typ_of_type ty)} |
---|
151 | whd whd in match (lookup' ??); >lookup_add_hit // |
---|
152 | | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC |
---|
153 | cases (identifier_eq ? id hd) |
---|
154 | [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit // |
---|
155 | | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss // |
---|
156 | ] |
---|
157 | ] |
---|
158 | ] qed. |
---|
159 | |
---|
160 | (* Put knowledge that Globals are global into a more useful form than the |
---|
161 | one used for the invariant. *) |
---|
162 | |
---|
163 | lemma characterise_vars_global : ∀globals,f,vartypes,stacksize. |
---|
164 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
165 | ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 → |
---|
166 | Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧ |
---|
167 | ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f). |
---|
168 | #globals #f #vartypes #stacksize #CHAR #id #r #ty #L |
---|
169 | cases (characterise_vars_src … CHAR id ?) |
---|
170 | [ * #r' * #ty' >L |
---|
171 | * #E1 destruct (E1) #EX |
---|
172 | % |
---|
173 | [ @EX |
---|
174 | | % #EX' cases (characterise_vars_localid … CHAR EX') |
---|
175 | #ty' whd in ⊢ (% → ?); >L * |
---|
176 | ] |
---|
177 | | * #ty' whd in ⊢ (% → ?); >L * |
---|
178 | | whd >(opt_eq_from_res ???? L) % #E destruct |
---|
179 | ] qed. |
---|
180 | |
---|
181 | |
---|
182 | (* Show how the global environments match up. *) |
---|
183 | |
---|
184 | lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'. |
---|
185 | map_partial_All A B P f l H = OK ? l' → |
---|
186 | All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'. |
---|
187 | #A #B #P #f #l |
---|
188 | elim l |
---|
189 | [ #H #l' #MAP normalize in MAP; destruct // |
---|
190 | | #h #t #IH * #p #H #l' |
---|
191 | whd in ⊢ (??%? → ?); |
---|
192 | lapply (refl ? (f h p)) whd in match (proj1 ???); |
---|
193 | cases (f h p) in ⊢ (???% → %); |
---|
194 | [ #b #E #MAP cases (bind_inversion ????? MAP) |
---|
195 | #tl' * #MAP' #E' normalize in E'; destruct |
---|
196 | % [ %{p} @E | @IH [ @H | @MAP' ] ] |
---|
197 | | #m #_ #X normalize in X; destruct |
---|
198 | ] |
---|
199 | ] qed. |
---|
200 | |
---|
201 | |
---|
202 | definition clight_cminor_matching : clight_program → matching ≝ |
---|
203 | λp. |
---|
204 | let tmpuniverse ≝ universe_for_program p in |
---|
205 | let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in |
---|
206 | let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in |
---|
207 | let globals ≝ fun_globals @ var_globals in |
---|
208 | mk_matching |
---|
209 | ?? (list init_data × type) (list init_data) |
---|
210 | (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor) |
---|
211 | (λv,w. \fst v = w). |
---|
212 | |
---|
213 | lemma clight_to_cminor_varnames : ∀p,p'. |
---|
214 | clight_to_cminor p = OK ? p' → |
---|
215 | prog_var_names … p = prog_var_names … p'. |
---|
216 | * #vars #fns #main * #vars' #fns' #main' |
---|
217 | #TO cases (bind_inversion ????? TO) #fns'' * #MAP #E |
---|
218 | whd in E:(??%%); destruct |
---|
219 | -MAP normalize |
---|
220 | elim vars |
---|
221 | [ // |
---|
222 | | * * #id #r * #d #t #tl #IH normalize >IH // |
---|
223 | ] qed. |
---|
224 | |
---|
225 | |
---|
226 | lemma clight_to_cminor_matches : ∀p,p'. |
---|
227 | clight_to_cminor p = OK ? p' → |
---|
228 | match_program (clight_cminor_matching p) p p'. |
---|
229 | * #vars #fns #main * #vars' #fns' #main' |
---|
230 | #TO cases (bind_inversion ????? TO) #fns'' * #MAP #E |
---|
231 | whd in E:(??%%); destruct |
---|
232 | % |
---|
233 | [ -MAP whd in match (m_V ?); whd in match (m_W ?); |
---|
234 | elim vars |
---|
235 | [ // |
---|
236 | | * * #id #r * #init #ty #tl #IH % |
---|
237 | [ % // |
---|
238 | | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/ |
---|
239 | ] |
---|
240 | ] |
---|
241 | | @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP |
---|
242 | * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E |
---|
243 | normalize in E; destruct |
---|
244 | <(clight_to_cminor_varnames … TO) |
---|
245 | % whd |
---|
246 | % [2: % [2: @TRANSF | skip ] | skip ] |
---|
247 | | % |
---|
248 | ] qed. |
---|
249 | |
---|
250 | include "Clight/Cexec.ma". |
---|
251 | include "Clight/abstract.ma". |
---|
252 | include "Cminor/abstract.ma". |
---|
253 | |
---|
254 | (* Invariants used in simulation *) |
---|
255 | |
---|
256 | record clight_cminor_inv : Type[0] ≝ { |
---|
257 | globals : list (ident × region × type); |
---|
258 | ge_cl : genv_t clight_fundef; |
---|
259 | ge_cm : genv_t (fundef internal_function); |
---|
260 | eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s; |
---|
261 | trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f → |
---|
262 | ∃tmp_u,f',H1,H2. |
---|
263 | translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧ |
---|
264 | find_funct … ge_cm v = Some ? f' |
---|
265 | }. |
---|
266 | |
---|
267 | include "Clight/CexecInd.ma". |
---|
268 | include "Clight/frontend_misc.ma". |
---|
269 | include "Clight/memoryInjections.ma". |
---|
270 | |
---|
271 | lemma intsize_eq_inversion : |
---|
272 | ∀sz,sz'. |
---|
273 | ∀A:Type[0]. |
---|
274 | ∀ok,not_ok. |
---|
275 | intsize_eq_elim' sz sz' (λsz,sz'. res A) |
---|
276 | (OK ? ok) |
---|
277 | (Error ? not_ok) = (OK ? ok) → |
---|
278 | sz = sz'. |
---|
279 | * * try // normalize |
---|
280 | #A #ok #not_ok #Habsurd destruct |
---|
281 | qed. |
---|
282 | |
---|
283 | definition local_matching ≝ |
---|
284 | λE:embedding. |
---|
285 | λm,m':mem. |
---|
286 | λen:cl_env. |
---|
287 | λvenv:cm_env. |
---|
288 | λsp:block. |
---|
289 | λvars:var_types. |
---|
290 | |
---|
291 | ∀id,cl_blo. lookup SymbolTag ? en id = Some ? cl_blo → |
---|
292 | match lookup ?? vars id with |
---|
293 | [ Some kind ⇒ |
---|
294 | let 〈vtype, type〉 ≝ kind in |
---|
295 | match vtype with |
---|
296 | [ Stack n ⇒ |
---|
297 | E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉 |
---|
298 | | Local ⇒ |
---|
299 | ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v → |
---|
300 | ∃v'. lookup ?? venv id = Some ? v' ∧ |
---|
301 | value_eq E v v' |
---|
302 | | _ ⇒ False ] |
---|
303 | | None ⇒ False ]. |
---|
304 | |
---|
305 | lemma type_should_eq_inversion : |
---|
306 | ∀ty1,ty2,P,f,res. |
---|
307 | type_should_eq ty1 ty2 P f = OK ? res → |
---|
308 | ty1 = ty2 ∧ f ≃ res. |
---|
309 | #ty1 #ty2 #P #f #res normalize |
---|
310 | cases (type_eq_dec ty1 ty2) normalize nodelta |
---|
311 | [ 2: #Hneq #Habsurd destruct ] |
---|
312 | #Heq #Heq2 @conj try assumption |
---|
313 | destruct (Heq2) cases Heq normalize nodelta |
---|
314 | @eq_to_jmeq @refl |
---|
315 | qed. |
---|
316 | |
---|
317 | lemma load_value_of_type_by_ref : |
---|
318 | ∀ty,m,b,off,val. |
---|
319 | load_value_of_type ty m b off = Some ? val → |
---|
320 | typ_of_type ty ≃ ASTptr → |
---|
321 | access_mode ty ≃ By_reference → |
---|
322 | val = Vptr (mk_pointer b off). |
---|
323 | * |
---|
324 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
325 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
326 | #m #b #off #val |
---|
327 | [ 1,6,7: normalize #Habsurd destruct (Habsurd) |
---|
328 | | 4,5: normalize #Heq #_ #_ destruct @refl |
---|
329 | | 2: #_ normalize #Heq destruct |
---|
330 | | *: #Hload normalize #_ #H |
---|
331 | lapply (jmeq_to_eq ??? H) #Heq destruct |
---|
332 | ] qed. |
---|
333 | |
---|
334 | |
---|
335 | |
---|
336 | (* TODO : memory injections + link clight env+mem with local env+stack+mem *) |
---|
337 | lemma eval_expr_sim : |
---|
338 | ∀(inv:clight_cminor_inv). |
---|
339 | |
---|
340 | ∀(cl_env:cl_env). |
---|
341 | ∀(cl_m:mem). |
---|
342 | |
---|
343 | ∀(cm_env:cm_env). |
---|
344 | ∀(sp:block). |
---|
345 | ∀(cm_m:mem). |
---|
346 | ∀(vars:var_types). |
---|
347 | |
---|
348 | ∀E:embedding. |
---|
349 | ∀minj:memory_inj E cl_m cm_m. |
---|
350 | local_matching E cl_m cm_m cl_env cm_env sp vars → |
---|
351 | |
---|
352 | (*vars = pi1 … (characterise_vars … [globals] [f]) →*) |
---|
353 | (*local_matching en m venv sp m' → *) |
---|
354 | |
---|
355 | (∀(e:expr). |
---|
356 | ∀(e':CMexpr (typ_of_type (typeof e))). |
---|
357 | ∀Hexpr_vars. |
---|
358 | translate_expr vars e = OK ? («e', Hexpr_vars») → |
---|
359 | ∀cl_val,trace,Hyp_present. |
---|
360 | exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 → |
---|
361 | ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧ |
---|
362 | value_eq E cl_val cm_val) ∧ |
---|
363 | |
---|
364 | (∀ed,ty. |
---|
365 | ∀(e':CMexpr (typ_of_type ty)). |
---|
366 | ∀Hexpr_vars. |
---|
367 | translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») → |
---|
368 | ∀resblo,resoff,trace,Hyp_present. |
---|
369 | exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 → |
---|
370 | (* TODO: shift 〈resblo, resoff〉 through E *) |
---|
371 | eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉). |
---|
372 | #inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching |
---|
373 | @expr_lvalue_ind_combined |
---|
374 | [ 1: (* Integer constant *) |
---|
375 | #csz #ty cases ty |
---|
376 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
377 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
378 | #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate |
---|
379 | #val #trace #Hpresent #Hexec_cl |
---|
380 | whd in Htranslate:(??%?); |
---|
381 | [ 1,3,4,5,6,7,8: destruct ] |
---|
382 | (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with |
---|
383 | sand inside. *) |
---|
384 | @cthulhu |
---|
385 | | 2: * |
---|
386 | [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 |
---|
387 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
388 | try /2 by I/ |
---|
389 | #ty whd in ⊢ (% → ?); #Hind |
---|
390 | whd in match (Plvalue ???); |
---|
391 | whd in match (typeof ?); |
---|
392 | #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec |
---|
393 | whd in Hexec:(??%?); |
---|
394 | whd in match (exec_lvalue' ?????) in Hexec:(??%?); |
---|
395 | cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success |
---|
396 | whd in Hcl_success:(???%); |
---|
397 | [ 1: (* var case *) |
---|
398 | |
---|
399 | lapply Hcl_success -Hcl_success |
---|
400 | (* Peform case analysis on presence of variable in local Clight env. |
---|
401 | * if success, exec_expr/exec_lvalue tells us that it shoud be local. *) |
---|
402 | @(match lookup SymbolTag block cl_env var_id |
---|
403 | return λx.(lookup SymbolTag block cl_env var_id = x) → ? |
---|
404 | with |
---|
405 | [ None ⇒ λHcl_lookup. ? |
---|
406 | | Some loc ⇒ λHcl_lookup. ? |
---|
407 | ] (refl ? (lookup SymbolTag block cl_env var_id))) |
---|
408 | normalize nodelta |
---|
409 | [ 1: (* global case *) |
---|
410 | @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *) |
---|
411 | | 2: (* local case *) |
---|
412 | #Heq destruct (Heq) |
---|
413 | lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr |
---|
414 | * #var_id_alloc_type * #var_id_type * |
---|
415 | generalize in match var_id_alloc_type; * normalize nodelta |
---|
416 | [ 1: (* Global case. This should be contradictory, right ? |
---|
417 | * If lookup succeeded, then our local shadows any global with the same |
---|
418 | * name, and [characterise_vars] should say so. TODO, this lemma. *) |
---|
419 | @cthulhu |
---|
420 | | 2: (* Stack local *) |
---|
421 | lapply Hcl_load_success -Hcl_load_success |
---|
422 | lapply Hyp_present -Hyp_present |
---|
423 | lapply Hexpr_vars -Hexpr_vars |
---|
424 | lapply cm_expr -cm_expr inversion (access_mode ty) |
---|
425 | [ #typ_of_ty | | #typ_of_ty ] |
---|
426 | #Heq_typ_of_type #Heq_access_mode |
---|
427 | #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success |
---|
428 | #stack_depth #Hlookup_vartype_success normalize nodelta |
---|
429 | whd in ⊢ ((???%) → ?); #Heq destruct (Heq) |
---|
430 | lapply (Hlocal_matching … Hcl_lookup) |
---|
431 | whd in Hlookup_vartype_success:(??%?); |
---|
432 | cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success |
---|
433 | * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq) |
---|
434 | >Hlookup' normalize nodelta #Hembedding_eq |
---|
435 | cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success |
---|
436 | #loaded_val * #Hload_val |
---|
437 | whd in ⊢ ((???%) → ?); #Heq destruct (Heq) |
---|
438 | lapply (opt_to_res_inversion ???? Hload_val) -Hload_val |
---|
439 | #Hload_success |
---|
440 | whd in match (eval_expr ???????); |
---|
441 | cut (pointer_translation (mk_pointer cl_b zero_offset) E = |
---|
442 | Some ? (mk_pointer sp (offset_of_Z stack_depth))) |
---|
443 | [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta |
---|
444 | >offset_plus_0 @refl ] |
---|
445 | #Hpointer_translation |
---|
446 | [ 2: (* By-ref *) |
---|
447 | whd in Hload_success:(??%?); |
---|
448 | lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode) |
---|
449 | #Heq_val |
---|
450 | >Heq_val |
---|
451 | %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))} |
---|
452 | @conj try @refl |
---|
453 | %4 (* boring and trivial *) |
---|
454 | @cthulhu |
---|
455 | | 1: (* By value *) |
---|
456 | lapply (mi_inj … Hinj … Hpointer_translation … Hload_success) |
---|
457 | [ @(load_by_value_success_valid_pointer … Hload_success) |
---|
458 | lapply (jmeq_to_eq ??? Heq_typ_of_type) |
---|
459 | #Heq_typ_of_type' |
---|
460 | (* boring and trivial *) |
---|
461 | @cthulhu ] |
---|
462 | * #cm_val * #Hload_in_cm #Hvalue_eq |
---|
463 | %{cm_val} @conj try assumption |
---|
464 | (* unpack Hload_in_cm using Heq_access_mode as an hypothesis. profit *) |
---|
465 | @cthulhu ] |
---|
466 | | 3: (* Register local variable *) |
---|
467 | #Hlookup_eq |
---|
468 | lapply (res_inversion ?????? Hlookup_eq) |
---|
469 | * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq) |
---|
470 | #Htype_eq |
---|
471 | cases (type_should_eq_inversion |
---|
472 | var_id_type |
---|
473 | ty |
---|
474 | (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars)) |
---|
475 | … Htype_eq) -Htype_eq |
---|
476 | (* Reverting all premises in order to perform type rewrite *) |
---|
477 | #Htype_eq |
---|
478 | lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq |
---|
479 | lapply Hcl_load_success -Hcl_load_success |
---|
480 | lapply Hcl_lookup -Hcl_lookup |
---|
481 | lapply Hyp_present -Hyp_present |
---|
482 | lapply Hexpr_vars -Hexpr_vars |
---|
483 | lapply cm_expr |
---|
484 | destruct (Htype_eq) |
---|
485 | #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup' |
---|
486 | #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq |
---|
487 | destruct (Hexpr_eq) |
---|
488 | whd in match (eval_expr ???????); |
---|
489 | whd in match (lookup_present ?????); |
---|
490 | lapply (Hlocal_matching … Hcl_lookup) >Hlookup' normalize nodelta |
---|
491 | cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success |
---|
492 | #loaded_val * #Hload_val |
---|
493 | whd in ⊢ ((???%) → ?); #Heq destruct (Heq) |
---|
494 | lapply (opt_to_res_inversion ???? Hload_val) -Hload_val |
---|
495 | #Hload_success #Hlookup_in_cm_env |
---|
496 | cases (Hlookup_in_cm_env ? Hload_success) #val' |
---|
497 | * #Hlookup_in_cm #Hvalue_eq %{val'} |
---|
498 | cases Hyp_present |
---|
499 | >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption |
---|
500 | (* seems ok *) |
---|
501 | ] |
---|
502 | ] |
---|
503 | | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *) |
---|
504 | cases (bind_inversion ????? Hcl_success) -Hcl_success |
---|
505 | * #cl_subexpr_val #cl_subexpr_trace * |
---|
506 | whd in ⊢ (? → (???%) → ?); |
---|
507 | @(match cl_subexpr_val |
---|
508 | return λx. cl_subexpr_val = x → ? |
---|
509 | with |
---|
510 | [ Vundef ⇒ λHval_eq. ? |
---|
511 | | Vint sz' i ⇒ λHval_eq. ? |
---|
512 | | Vnull ⇒ λHval_eq. ? |
---|
513 | | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta |
---|
514 | [ 1,2,3: #_ #Habsurd destruct ] |
---|
515 | #Hcl_exec_to_pointer #Heq destruct (Heq) |
---|
516 | (* Now that we have executed the Clight part, reduce the Cminor one *) |
---|
517 | whd in Htranslate_expr:(??%?); |
---|
518 | cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr |
---|
519 | * #cm_expr #Hexpr_vars * #Htranslate_expr |
---|
520 | whd (* ... *) @cthulhu |
---|
521 | | 3: @cthulhu ] |
---|
522 | | *: @cthulhu |
---|
523 | ] qed. |
---|
524 | |
---|
525 | |
---|
526 | |
---|
527 | axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. |
---|
528 | |
---|
529 | (* Conjectured simulation results |
---|
530 | |
---|
531 | We split these based on the start state: |
---|
532 | |
---|
533 | 1. ‘normal’ states take some [S n] normal steps and simulates them by [S m] |
---|
534 | normal steps in Cminor; |
---|
535 | 2. call and return steps are simulated by a call/return step plus [m] normal |
---|
536 | steps (to copy stack allocated parameters / results); and |
---|
537 | 3. lone cost label steps are simulates by a lone cost label step |
---|
538 | |
---|
539 | These should allow us to maintain enough structure to identify the Cminor |
---|
540 | subtrace corresponding to a measurable Clight subtrace. |
---|
541 | *) |
---|
542 | |
---|
543 | definition clight_normal : Clight_state → bool ≝ |
---|
544 | λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
545 | |
---|
546 | definition cminor_normal : Cminor_state → bool ≝ |
---|
547 | λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
548 | |
---|
549 | axiom clight_cminor_normal : |
---|
550 | ∀INV:clight_cminor_inv. |
---|
551 | ∀s1,s1',s2,tr. |
---|
552 | clight_cminor_rel INV s1 s1' → |
---|
553 | clight_normal s1 → |
---|
554 | ¬ Clight_labelled s1 → |
---|
555 | ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
556 | ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. |
---|
557 | tr = tr' ∧ |
---|
558 | clight_cminor_rel INV s2 s2' |
---|
559 | ). |
---|
560 | |
---|
561 | axiom clight_cminor_call_return : |
---|
562 | ∀INV:clight_cminor_inv. |
---|
563 | ∀s1,s1',s2,tr. |
---|
564 | clight_cminor_rel INV s1 s1' → |
---|
565 | match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] → |
---|
566 | after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
567 | ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. |
---|
568 | tr = tr' ∧ |
---|
569 | clight_cminor_rel INV s2 s2' |
---|
570 | ). |
---|
571 | |
---|
572 | axiom clight_cminor_cost : |
---|
573 | ∀INV:clight_cminor_inv. |
---|
574 | ∀s1,s1',s2,tr. |
---|
575 | clight_cminor_rel INV s1 s1' → |
---|
576 | Clight_labelled s1 → |
---|
577 | after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
578 | after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'. |
---|
579 | tr = tr' ∧ |
---|
580 | clight_cminor_rel INV s2 s2' |
---|
581 | ). |
---|
582 | |
---|