1 | include "Clight/toCminor.ma". |
---|
2 | include "Clight/CexecInd.ma". |
---|
3 | include "common/Globalenvs.ma". |
---|
4 | include "Clight/memoryInjections.ma". |
---|
5 | include "Clight/abstract.ma". |
---|
6 | include "Cminor/abstract.ma". |
---|
7 | |
---|
8 | (* Expr simulation. Contains important definitions for statements, too. *) |
---|
9 | include "Clight/toCminorCorrectnessExpr.ma". |
---|
10 | |
---|
11 | |
---|
12 | (* When we characterise the local Clight variables, those that are stack |
---|
13 | allocated are given disjoint regions of the stack. *) |
---|
14 | |
---|
15 | lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty. |
---|
16 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
17 | lookup ?? vartypes id = Some ? 〈Stack n,ty〉 → |
---|
18 | ∀id',n',ty'. id ≠ id' → |
---|
19 | lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 → |
---|
20 | n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'. |
---|
21 | #globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty |
---|
22 | whd in ⊢ (??%? → ?); |
---|
23 | generalize in match vartypes; -vartypes |
---|
24 | generalize in match stacksize; -stacksize |
---|
25 | elim (args@vars) |
---|
26 | [ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct |
---|
27 | elim globals in L; |
---|
28 | [ normalize #L destruct |
---|
29 | | * * #id' #r #ty' #tl #IH |
---|
30 | whd in match (foldr ?????); |
---|
31 | #L cases (lookup_add_cases ??????? L) |
---|
32 | [ * #E1 #E2 destruct |
---|
33 | | @IH |
---|
34 | ] |
---|
35 | ] |
---|
36 | | * #id1 #ty1 #tl #IH #stacksize #vartypes |
---|
37 | whd in match (foldr ?????); |
---|
38 | (* Avoid writing out the definition again *) |
---|
39 | letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %; |
---|
40 | lapply (refl ? ih) whd in match ih; -ih |
---|
41 | cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %); |
---|
42 | #vartypes' #stack' #FOLD #IH |
---|
43 | whd in ⊢ (??(match % with [_⇒?])? → ?); |
---|
44 | cases (orb ??) |
---|
45 | #CHAR whd in CHAR:(??%?); destruct |
---|
46 | #L cases (lookup_add_cases ??????? L) |
---|
47 | [ 1,3: * #E1 #E2 destruct |
---|
48 | #id' #n' #ty' #NE >lookup_add_miss /2/ |
---|
49 | #L' %1 -L -IH |
---|
50 | generalize in match vartypes' in FOLD L' ⊢ %; -vartypes' |
---|
51 | generalize in match stack'; -stack' |
---|
52 | elim tl |
---|
53 | [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥ |
---|
54 | elim globals in L'; |
---|
55 | [ normalize #E destruct |
---|
56 | | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????); |
---|
57 | #L cases (lookup_add_cases ??????? L) |
---|
58 | [ * #E1 #E2 destruct |
---|
59 | | @IH |
---|
60 | ] |
---|
61 | ] |
---|
62 | | * #id2 #ty2 #tl2 #IH #stack' #vartypes' |
---|
63 | whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
64 | #vartypes2 #stack2 #IH |
---|
65 | whd in ⊢ (??%? → ?); |
---|
66 | cases (orb ??) |
---|
67 | [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L) |
---|
68 | [ * #E1 #E2 destruct // |
---|
69 | | #L'' lapply (IH ?? (refl ??) L'') /2/ |
---|
70 | ] |
---|
71 | | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L) |
---|
72 | [ * #E1 #E2 destruct |
---|
73 | | #L'' lapply (IH ?? (refl ??) L'') /2/ |
---|
74 | ] |
---|
75 | ] |
---|
76 | ] |
---|
77 | | -L #L #id' #n' #ty' #NE #L' |
---|
78 | cases (lookup_add_cases ??????? L') |
---|
79 | [ * #E1 #E2 destruct |
---|
80 | %2 -IH -L' |
---|
81 | generalize in match vartypes' in FOLD L; -vartypes' |
---|
82 | generalize in match stack'; -stack' |
---|
83 | elim tl |
---|
84 | [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥ |
---|
85 | elim globals in L; |
---|
86 | [ normalize #E destruct |
---|
87 | | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????); |
---|
88 | #L cases (lookup_add_cases ??????? L) |
---|
89 | [ * #E1 #E2 destruct |
---|
90 | | @IH |
---|
91 | ] |
---|
92 | ] |
---|
93 | | * #id1 #ty1 #tl1 #IH #stack' #vartypes' |
---|
94 | whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
95 | #vartypes2 #stack2 #IH |
---|
96 | whd in ⊢ (??%? → ?); |
---|
97 | cases (orb ??) |
---|
98 | #E whd in E:(??%?); destruct |
---|
99 | #L cases (lookup_add_cases ??????? L) |
---|
100 | [ 1,3: * #E1 #E2 destruct // |
---|
101 | | 2,4: #L' lapply (IH ?? (refl ??) L') /2/ |
---|
102 | ] |
---|
103 | ] |
---|
104 | | @(IH … (refl ??) L … NE) |
---|
105 | ] |
---|
106 | | -L #L #id' #n' #ty' #NE #L' |
---|
107 | cases (lookup_add_cases ??????? L') |
---|
108 | [ * #E1 #E2 destruct |
---|
109 | | @(IH … (refl ??) L … NE) |
---|
110 | ] |
---|
111 | ] |
---|
112 | ] qed. |
---|
113 | |
---|
114 | (* And everything is in the stack frame. *) |
---|
115 | |
---|
116 | lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty. |
---|
117 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
118 | lookup ?? vartypes id = Some ? 〈Stack n,ty〉 → |
---|
119 | n + sizeof ty ≤ stacksize. |
---|
120 | #globals * #ret #args #vars #body whd in match (characterise_vars ??); |
---|
121 | elim (args@vars) |
---|
122 | [ #vartypes #stacksize #id #n #ty #FOLD #L @⊥ |
---|
123 | whd in FOLD:(??%?); destruct elim globals in L; |
---|
124 | [ #E normalize in E; destruct |
---|
125 | | * * #id' #r' #ty' #tl' #IH |
---|
126 | whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L) |
---|
127 | [ * #E1 #E2 destruct |
---|
128 | | @IH |
---|
129 | ] |
---|
130 | ] |
---|
131 | | * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty |
---|
132 | whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %; |
---|
133 | #vartypes' #stackspace' #IH |
---|
134 | whd in ⊢ (??(match % with [_⇒?])? → ?); |
---|
135 | cases (orb ??) whd in ⊢ (??%? → ?); |
---|
136 | #E destruct #L cases (lookup_add_cases ??????? L) |
---|
137 | [ 1,3: * #E1 #E2 destruct // |
---|
138 | | 2,4: #L' lapply (IH … (refl ??) L') /2/ |
---|
139 | ] |
---|
140 | ] qed. |
---|
141 | |
---|
142 | |
---|
143 | |
---|
144 | (* Put knowledge that Globals are global into a more useful form than the |
---|
145 | one used for the invariant. *) |
---|
146 | (* XXX superfluous lemma ? Commenting it for now. |
---|
147 | if not superfluous : move to toCminorCorrectnessExpr.ma, after |
---|
148 | [characterise_vars_localid] *) |
---|
149 | (* |
---|
150 | lemma characterise_vars_global : ∀globals,f,vartypes,stacksize. |
---|
151 | characterise_vars globals f = 〈vartypes, stacksize〉 → |
---|
152 | ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 → |
---|
153 | Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧ |
---|
154 | ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f). |
---|
155 | #globals #f #vartypes #stacksize #CHAR #id #r #ty #L |
---|
156 | cases (characterise_vars_src … CHAR id ?) |
---|
157 | [ * #r' * #ty' >L |
---|
158 | * #E1 destruct (E1) #EX |
---|
159 | % |
---|
160 | [ @EX |
---|
161 | | % #EX' cases (characterise_vars_localid … CHAR EX') |
---|
162 | #ty' whd in ⊢ (% → ?); >L * |
---|
163 | ] |
---|
164 | | * #ty' whd in ⊢ (% → ?); >L * |
---|
165 | | whd >(opt_eq_from_res ???? L) % #E destruct |
---|
166 | ] qed. *) |
---|
167 | |
---|
168 | (* Show how the global environments match up. *) |
---|
169 | |
---|
170 | lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'. |
---|
171 | map_partial_All A B P f l H = OK ? l' → |
---|
172 | All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'. |
---|
173 | #A #B #P #f #l |
---|
174 | elim l |
---|
175 | [ #H #l' #MAP normalize in MAP; destruct // |
---|
176 | | #h #t #IH * #p #H #l' |
---|
177 | whd in ⊢ (??%? → ?); |
---|
178 | lapply (refl ? (f h p)) whd in match (proj1 ???); |
---|
179 | cases (f h p) in ⊢ (???% → %); |
---|
180 | [ #b #E #MAP cases (bind_inversion ????? MAP) |
---|
181 | #tl' * #MAP' #E' normalize in E'; destruct |
---|
182 | % [ %{p} @E | @IH [ @H | @MAP' ] ] |
---|
183 | | #m #_ #X normalize in X; destruct |
---|
184 | ] |
---|
185 | ] qed. |
---|
186 | |
---|
187 | |
---|
188 | definition clight_cminor_matching : clight_program → matching ≝ |
---|
189 | λp. |
---|
190 | let tmpuniverse ≝ universe_for_program p in |
---|
191 | let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in |
---|
192 | let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in |
---|
193 | let globals ≝ fun_globals @ var_globals in |
---|
194 | mk_matching |
---|
195 | ?? (list init_data × type) (list init_data) |
---|
196 | (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor) |
---|
197 | (λv,w. \fst v = w). |
---|
198 | |
---|
199 | lemma clight_to_cminor_varnames : ∀p,p'. |
---|
200 | clight_to_cminor p = OK ? p' → |
---|
201 | prog_var_names … p = prog_var_names … p'. |
---|
202 | * #vars #fns #main * #vars' #fns' #main' |
---|
203 | #TO cases (bind_inversion ????? TO) #fns'' * #MAP #E |
---|
204 | whd in E:(??%%); destruct |
---|
205 | -MAP normalize |
---|
206 | elim vars |
---|
207 | [ // |
---|
208 | | * * #id #r * #d #t #tl #IH normalize >IH // |
---|
209 | ] qed. |
---|
210 | |
---|
211 | |
---|
212 | lemma clight_to_cminor_matches : ∀p,p'. |
---|
213 | clight_to_cminor p = OK ? p' → |
---|
214 | match_program (clight_cminor_matching p) p p'. |
---|
215 | * #vars #fns #main * #vars' #fns' #main' |
---|
216 | #TO cases (bind_inversion ????? TO) #fns'' * #MAP #E |
---|
217 | whd in E:(??%%); destruct |
---|
218 | % |
---|
219 | [ -MAP whd in match (m_V ?); whd in match (m_W ?); |
---|
220 | elim vars |
---|
221 | [ // |
---|
222 | | * * #id #r * #init #ty #tl #IH % |
---|
223 | [ % // |
---|
224 | | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/ |
---|
225 | ] |
---|
226 | ] |
---|
227 | | @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP |
---|
228 | * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E |
---|
229 | normalize in E; destruct |
---|
230 | <(clight_to_cminor_varnames … TO) |
---|
231 | % whd |
---|
232 | % [2: % [2: @TRANSF | skip ] | skip ] |
---|
233 | | % |
---|
234 | ] qed. |
---|
235 | |
---|
236 | |
---|
237 | (* This is the statement for expression simulation copied fro toCminorCorrectnessExpr.ma, |
---|
238 | for easier reference. |
---|
239 | lemma eval_expr_sim : |
---|
240 | (* [cl_cm_inv] maps CL globals to CM globals, including functions *) |
---|
241 | ∀cl_cm_inv : clight_cminor_inv. |
---|
242 | (* current function (defines local environment) *) |
---|
243 | ∀f : function. |
---|
244 | (* [alloctype] maps variables to their allocation type (global, stack, register) *) |
---|
245 | ∀alloctype : var_types. |
---|
246 | ∀stacksize : ℕ. |
---|
247 | ∀alloc_hyp : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉. |
---|
248 | (* environments *) |
---|
249 | ∀cl_env : cl_env. |
---|
250 | ∀cm_env : cm_env. |
---|
251 | (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *) |
---|
252 | ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉. |
---|
253 | (* CL and CM memories *) |
---|
254 | ∀cl_m : mem. |
---|
255 | ∀cm_m : mem. |
---|
256 | (* memory injection and matching *) |
---|
257 | ∀embed : embedding. |
---|
258 | ∀injection : memory_inj embed cl_m cm_m. |
---|
259 | ∀stackptr : block. |
---|
260 | ∀matching : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype. |
---|
261 | (* clight expr to cminor expr *) |
---|
262 | (∀(e:expr). |
---|
263 | ∀(e':CMexpr (typ_of_type (typeof e))). |
---|
264 | ∀Hexpr_vars. |
---|
265 | translate_expr alloctype e = OK ? («e', Hexpr_vars») → |
---|
266 | ∀cl_val,trace,Hyp_present. |
---|
267 | exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 → |
---|
268 | ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧ |
---|
269 | value_eq embed cl_val cm_val) ∧ |
---|
270 | (* clight /lvalue/ to cminor /expr/ *) |
---|
271 | (∀ed,ty. |
---|
272 | ∀(e':CMexpr ASTptr). |
---|
273 | ∀Hexpr_vars. |
---|
274 | translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») → |
---|
275 | ∀cl_blo,cl_off,trace,Hyp_present. |
---|
276 | exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 → |
---|
277 | ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧ |
---|
278 | value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val). |
---|
279 | *) |
---|
280 | |
---|
281 | |
---|
282 | |
---|
283 | |
---|
284 | axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. |
---|
285 | |
---|
286 | (* Conjectured simulation results |
---|
287 | |
---|
288 | We split these based on the start state: |
---|
289 | |
---|
290 | 1. ‘normal’ states take some [S n] normal steps and simulates them by [S m] |
---|
291 | normal steps in Cminor; |
---|
292 | 2. call and return steps are simulated by a call/return step plus [m] normal |
---|
293 | steps (to copy stack allocated parameters / results); and |
---|
294 | 3. lone cost label steps are simulates by a lone cost label step |
---|
295 | |
---|
296 | These should allow us to maintain enough structure to identify the Cminor |
---|
297 | subtrace corresponding to a measurable Clight subtrace. |
---|
298 | *) |
---|
299 | |
---|
300 | definition clight_normal : Clight_state → bool ≝ |
---|
301 | λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
302 | |
---|
303 | definition cminor_normal : Cminor_state → bool ≝ |
---|
304 | λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
305 | |
---|
306 | axiom clight_cminor_normal : |
---|
307 | ∀INV:clight_cminor_inv. |
---|
308 | ∀s1,s1',s2,tr. |
---|
309 | clight_cminor_rel INV s1 s1' → |
---|
310 | clight_normal s1 → |
---|
311 | ¬ Clight_labelled s1 → |
---|
312 | ∃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〉) → |
---|
313 | ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. |
---|
314 | tr = tr' ∧ |
---|
315 | clight_cminor_rel INV s2 s2' |
---|
316 | ). |
---|
317 | |
---|
318 | axiom clight_cminor_call_return : |
---|
319 | ∀INV:clight_cminor_inv. |
---|
320 | ∀s1,s1',s2,tr. |
---|
321 | clight_cminor_rel INV s1 s1' → |
---|
322 | match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] → |
---|
323 | after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
324 | ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. |
---|
325 | tr = tr' ∧ |
---|
326 | clight_cminor_rel INV s2 s2' |
---|
327 | ). |
---|
328 | |
---|
329 | axiom clight_cminor_cost : |
---|
330 | ∀INV:clight_cminor_inv. |
---|
331 | ∀s1,s1',s2,tr. |
---|
332 | clight_cminor_rel INV s1 s1' → |
---|
333 | Clight_labelled s1 → |
---|
334 | after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
335 | after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'. |
---|
336 | tr = tr' ∧ |
---|
337 | clight_cminor_rel INV s2 s2' |
---|
338 | ). |
---|
339 | |
---|
340 | axiom clight_cminor_init : ∀cl_program,cm_program,s,s'. |
---|
341 | clight_to_cminor cl_program = OK ? cm_program → |
---|
342 | make_initial_state ?? clight_fullexec cl_program = OK ? s → |
---|
343 | make_initial_state ?? Cminor_fullexec cm_program = OK ? s' → |
---|
344 | ∃INV. clight_cminor_rel INV s s'. |
---|