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 | |
---|
268 | axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. |
---|
269 | |
---|
270 | (* Conjectured simulation results |
---|
271 | |
---|
272 | We split these based on the start state: |
---|
273 | |
---|
274 | 1. ‘normal’ states take some [S n] normal steps and simulates them by [S m] |
---|
275 | normal steps in Cminor; |
---|
276 | 2. call and return steps are simulated by a call/return step plus [m] normal |
---|
277 | steps (to copy stack allocated parameters / results); and |
---|
278 | 3. lone cost label steps are simulates by a lone cost label step |
---|
279 | |
---|
280 | These should allow us to maintain enough structure to identify the Cminor |
---|
281 | subtrace corresponding to a measurable Clight subtrace. |
---|
282 | *) |
---|
283 | |
---|
284 | definition clight_normal : Clight_state → bool ≝ |
---|
285 | λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
286 | |
---|
287 | definition cminor_normal : Cminor_state → bool ≝ |
---|
288 | λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
289 | |
---|
290 | axiom clight_cminor_normal : |
---|
291 | ∀INV:clight_cminor_inv. |
---|
292 | ∀s1,s1',s2,tr. |
---|
293 | clight_cminor_rel INV s1 s1' → |
---|
294 | clight_normal s1 → |
---|
295 | ¬ Clight_labelled s1 → |
---|
296 | ∃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〉) → |
---|
297 | ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. |
---|
298 | tr = tr' ∧ |
---|
299 | clight_cminor_rel INV s2 s2' |
---|
300 | ). |
---|
301 | |
---|
302 | axiom clight_cminor_call_return : |
---|
303 | ∀INV:clight_cminor_inv. |
---|
304 | ∀s1,s1',s2,tr. |
---|
305 | clight_cminor_rel INV s1 s1' → |
---|
306 | match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] → |
---|
307 | after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
308 | ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'. |
---|
309 | tr = tr' ∧ |
---|
310 | clight_cminor_rel INV s2 s2' |
---|
311 | ). |
---|
312 | |
---|
313 | axiom clight_cminor_cost : |
---|
314 | ∀INV:clight_cminor_inv. |
---|
315 | ∀s1,s1',s2,tr. |
---|
316 | clight_cminor_rel INV s1 s1' → |
---|
317 | Clight_labelled s1 → |
---|
318 | after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
319 | after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'. |
---|
320 | tr = tr' ∧ |
---|
321 | clight_cminor_rel INV s2 s2' |
---|
322 | ). |
---|
323 | |
---|