1 | include "common/AST.ma". |
---|
2 | include "common/Globalenvs.ma". |
---|
3 | |
---|
4 | (* |
---|
5 | axiom find_funct_ptr_symbol_inversion: |
---|
6 | ∀F,V,init. ∀p: program F V. |
---|
7 | ∀id: ident. ∀b: block. ∀f: F ?. |
---|
8 | find_symbol ? (globalenv ?? init p) id = Some ? b → |
---|
9 | find_funct_ptr ? (globalenv ?? init p) b = Some ? f → |
---|
10 | In … (prog_funct ?? p) 〈id, f〉. |
---|
11 | |
---|
12 | axiom find_funct_ptr_exists: |
---|
13 | ∀F,V,init. ∀p: program F V. ∀id: ident. ∀f: F ?. |
---|
14 | In … (prog_funct ?? p) 〈id, f〉 → |
---|
15 | ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b |
---|
16 | ∧ find_funct_ptr ? (globalenv ?? init p) b = Some ? f. |
---|
17 | |
---|
18 | axiom find_symbol_exists: |
---|
19 | ∀F,V,init. ∀p: program F V. |
---|
20 | ∀id: ident. ∀r,v. |
---|
21 | In ? (prog_vars ?? p) 〈〈id, r〉, v〉 → |
---|
22 | ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b. |
---|
23 | |
---|
24 | definition is_function ≝ λF.λge : genv_t F. |
---|
25 | λi : ident.∃fd. |
---|
26 | ! bl ← find_symbol … ge i ; |
---|
27 | find_funct_ptr … ge bl = Some ? fd. |
---|
28 | |
---|
29 | definition is_internal_function ≝ λF.λge : genv_t (fundef F). |
---|
30 | λi : ident.∃fd. |
---|
31 | ! bl ← find_symbol … ge i ; |
---|
32 | find_funct_ptr … ge bl = Some ? (Internal ? fd). |
---|
33 | |
---|
34 | definition is_internal_function_of_program : |
---|
35 | ∀A.program (λvars.fundef (A vars)) ℕ → ident → Prop ≝ |
---|
36 | λA,prog,i.is_internal_function … (globalenv_noinit … prog) i. |
---|
37 | |
---|
38 | definition funct_of_ident : ∀F,ge. |
---|
39 | ident → option (Σi.is_function F ge i) |
---|
40 | ≝ λF,ge,i. |
---|
41 | match ? |
---|
42 | return λx.! bl ← find_symbol … ge i ; |
---|
43 | find_funct_ptr … ge bl = x → ? |
---|
44 | with |
---|
45 | [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf» |
---|
46 | | None ⇒ λ_.None ? |
---|
47 | ] (refl …). |
---|
48 | *) |
---|
49 | |
---|
50 | lemma symbol_of_function_block_ok : |
---|
51 | ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf). |
---|
52 | #F #ge #b #FFP |
---|
53 | cut (∀A,B : Type[0].∀P : B → Prop.∀x : option A.∀c1,c2. |
---|
54 | (∀v.∀prf : x = Some ? v.P (c1 v prf)) → |
---|
55 | (∀prf:x = None ?.P (c2 prf)) → |
---|
56 | P (match x return λy.x = y → ? with |
---|
57 | [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf] |
---|
58 | (refl …))) [ #A #B #P * // ] #aux |
---|
59 | whd in ⊢ (???(??%)); @aux [//] #H |
---|
60 | generalize in match (? : False); * |
---|
61 | qed. |
---|
62 | |
---|
63 | (* |
---|
64 | definition funct_of_block : ∀F,ge. |
---|
65 | block → option (Σi.is_function F ge i) ≝ |
---|
66 | λF,ge,bl. |
---|
67 | match find_funct_ptr … ge bl |
---|
68 | return λx.find_funct_ptr … ge bl = x → ? with |
---|
69 | [ Some fd ⇒ λprf.return mk_Sig |
---|
70 | ident (λi.is_function F ge i) |
---|
71 | (symbol_of_function_block … ge bl ?) |
---|
72 | (ex_intro … fd ?) |
---|
73 | | None ⇒ λ_.None ? |
---|
74 | ] (refl …). |
---|
75 | [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf |
---|
76 | | >prf % #ABS destruct(ABS) |
---|
77 | ] |
---|
78 | qed. |
---|
79 | |
---|
80 | definition block_of_funct ≝ λF,ge. |
---|
81 | λi : Σi.is_function F ge i. |
---|
82 | match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with |
---|
83 | [ Some bl ⇒ λ_.bl |
---|
84 | | None ⇒ λprf.⊥ |
---|
85 | ] (pi2 … i). |
---|
86 | cases prf #fd normalize #ABS destruct(ABS) |
---|
87 | qed. |
---|
88 | |
---|
89 | definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝ |
---|
90 | λF,ge,i. |
---|
91 | match ! bl ← find_symbol … ge i ; |
---|
92 | find_funct_ptr … ge bl |
---|
93 | return λx.(∃fd.x = ?) → ? |
---|
94 | with |
---|
95 | [ Some fd ⇒ λ_.fd |
---|
96 | | None ⇒ λprf.⊥ |
---|
97 | ] (pi2 … i). |
---|
98 | cases prf #fd #ABS destruct |
---|
99 | qed. |
---|
100 | |
---|
101 | lemma description_of_internal_function : ∀F,ge,i,fn. |
---|
102 | description_of_function ? ge i = Internal F fn → is_internal_function … ge i. |
---|
103 | #F #ge * #i * #fd #EQ |
---|
104 | #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ |
---|
105 | %{EQ} |
---|
106 | qed. |
---|
107 | |
---|
108 | definition int_funct_of_block : ∀F,ge. |
---|
109 | block → option (Σi.is_internal_function F ge i) ≝ |
---|
110 | λF,ge,bl. |
---|
111 | ! f ← funct_of_block … ge bl ; |
---|
112 | match ? |
---|
113 | return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) |
---|
114 | with |
---|
115 | [ Internal fn ⇒ λprf.return «pi1 … f, ?» |
---|
116 | | External fn ⇒ λ_.None ? |
---|
117 | ] (refl …). |
---|
118 | @(description_of_internal_function … prf) |
---|
119 | qed. |
---|
120 | |
---|
121 | lemma internal_function_is_function : ∀F,ge,i. |
---|
122 | is_internal_function F ge i → is_function … ge i. |
---|
123 | #F #ge #i * #fn #prf %{prf} qed. |
---|
124 | |
---|
125 | definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝ |
---|
126 | λF,ge,i. |
---|
127 | match ! bl ← find_symbol … ge i ; |
---|
128 | find_funct_ptr … ge bl |
---|
129 | return λx.(∃fn.x = ?) → ? |
---|
130 | with |
---|
131 | [ Some fd ⇒ |
---|
132 | match fd return λx.(∃fn.Some ? x = ?) → ? with |
---|
133 | [ Internal fn ⇒ λ_.fn |
---|
134 | | External _ ⇒ λprf.⊥ |
---|
135 | ] |
---|
136 | | None ⇒ λprf.⊥ |
---|
137 | ] (pi2 … i). |
---|
138 | cases prf #fn #ABS destruct |
---|
139 | qed. |
---|
140 | |
---|
141 | lemma if_propagate : |
---|
142 | ∀A_in,A_out. |
---|
143 | ∀trans. |
---|
144 | ∀prog_in : program (λvars.fundef (A_in vars)) ℕ. |
---|
145 | let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝ |
---|
146 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
147 | ∀i.is_internal_function_of_program … prog_in i → |
---|
148 | is_internal_function_of_program … prog_out i. |
---|
149 | #A_in #A_out #trans #prog_in #ident |
---|
150 | * #ifn |
---|
151 | inversion (find_symbol ???) [ #_ #ABS whd in ABS : (??%%); destruct(ABS) ] |
---|
152 | #bl #EQfind >m_return_bind #EQfunct_ptr |
---|
153 | %{(trans … ifn)} |
---|
154 | >find_symbol_transf >EQfind >m_return_bind |
---|
155 | >(find_funct_ptr_transf … EQfunct_ptr) % |
---|
156 | qed. |
---|
157 | |
---|
158 | lemma block_of_funct_ident_is_code : ∀F,ge,i. |
---|
159 | block_region (block_of_funct F ge i) = Code. |
---|
160 | #F #ge * #i * #fd |
---|
161 | whd in ⊢ (?→??(?%)?); |
---|
162 | cases (find_symbol ???) |
---|
163 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
164 | #bl normalize nodelta >m_return_bind |
---|
165 | whd in ⊢ (??%?→?); cases (block_region bl) |
---|
166 | [ #ABS normalize in ABS; destruct(ABS) ] |
---|
167 | #_ % |
---|
168 | qed. |
---|
169 | |
---|
170 | lemma prog_if_of_function_transform : |
---|
171 | ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ. |
---|
172 | let prog_out : program (λvars.fundef (B vars)) ℕ ≝ |
---|
173 | transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
174 | ∀i_out : Σi.is_internal_function_of_program … prog_out i. |
---|
175 | ∀i_in : Σi.is_internal_function_of_program … prog_in i. |
---|
176 | pi1 … i_out = pi1 … i_in → |
---|
177 | if_of_function … i_out = trans … (if_of_function … i_in). |
---|
178 | #A #B #trans #prog * #i1 #i_prf1 * #i2 #i_prf2 #EQ destruct(EQ) |
---|
179 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
180 | ∀m.∀prf : Q m.∀f1,f2. |
---|
181 | (∀x,prf.m = Some ? x → P (f1 x prf)) → |
---|
182 | (∀prf.m = None ? → P (f2 prf)) → |
---|
183 | P (match m return λx.Q x → ? with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
184 | [ #A #B #Q #P * /2 by / ] #aux |
---|
185 | whd in ⊢ (??%?); @aux |
---|
186 | [2: #prf #EQ generalize in match (? : False); * ] |
---|
187 | #fd * #ifn #EQ1 #EQ destruct normalize nodelta |
---|
188 | whd in ⊢ (???(??%)); @aux |
---|
189 | [2: #prf #EQ generalize in match (? : False); * ] |
---|
190 | #fd' * #ifn' #EQ1' #EQ' destruct normalize nodelta |
---|
191 | inversion (find_symbol ???) in EQ'; [ #_ #ABS whd in ABS: (??%%); destruct ] |
---|
192 | #bl #EQfind >m_return_bind #EQfunct |
---|
193 | >find_symbol_transf in EQ; >EQfind >m_return_bind |
---|
194 | >(find_funct_ptr_transf … EQfunct) #EQ'' destruct % |
---|
195 | qed. |
---|
196 | *) |
---|
197 | |
---|
198 | include alias "common/PositiveMap.ma". |
---|
199 | |
---|
200 | lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id. |
---|
201 | id < (nextfunction ? ge) → |
---|
202 | lookup_opt … id (functions ? ge) = None ? → |
---|
203 | lookup_opt … id (functions … (add_functs F ge l)) = None ?. |
---|
204 | #F #ge #l #id whd in match add_functs; normalize nodelta |
---|
205 | elim l -l [ #_ normalize //] |
---|
206 | * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????); |
---|
207 | >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %] |
---|
208 | #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1) |
---|
209 | | cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl)) |
---|
210 | [elim tl [normalize //] |
---|
211 | #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ] |
---|
212 | #H2 lapply(transitive_le … H H2) @lt_to_not_eq |
---|
213 | qed. |
---|
214 | |
---|
215 | lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l. |
---|
216 | lookup_opt … id (functions ? (\fst gem)) = None ? → |
---|
217 | lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. |
---|
218 | #F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H] |
---|
219 | ** #x1 #x2 #x3 #tl whd in match add_globals; |
---|
220 | normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta |
---|
221 | cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; |
---|
222 | normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] |
---|
223 | #f1 #H3 <(drop_fn_lfn … f1 H3) assumption |
---|
224 | qed. |
---|
225 | |
---|
226 | |
---|
227 | lemma globalenv_no_minus_one : |
---|
228 | ∀F,V,i,p. |
---|
229 | find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?. |
---|
230 | #F #V #i #p |
---|
231 | whd in match find_funct_ptr; normalize nodelta |
---|
232 | whd in match globalenv; |
---|
233 | whd in match globalenv_allocmem; normalize nodelta |
---|
234 | @add_globals_functions_miss @add_functs_functions_miss normalize // |
---|
235 | qed. |
---|
236 | |
---|
237 | lemma globalenv_no_zero : |
---|
238 | ∀F,V,i,p. |
---|
239 | find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. // |
---|
240 | qed. |
---|
241 | |
---|
242 | lemma symbol_for_block_match: |
---|
243 | ∀M:matching.∀initV,initW. |
---|
244 | (∀v,w. match_var_entry M v w → |
---|
245 | size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
246 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
247 | ∀MATCH:match_program … M p p'. |
---|
248 | ∀b: block. |
---|
249 | symbol_for_block … (globalenv … initW p') b = |
---|
250 | symbol_for_block … (globalenv … initV p) b. |
---|
251 | * #A #B #V #W #match_fn #match_var #initV #initW #H |
---|
252 | #p #p' * #Mvars #Mfn #Mmain |
---|
253 | #b |
---|
254 | whd in match symbol_for_block; normalize nodelta |
---|
255 | whd in match globalenv in ⊢ (???%); normalize nodelta |
---|
256 | whd in match (globalenv_allocmem ????); |
---|
257 | change with (add_globals ?????) in match (foldl ?????); |
---|
258 | >(proj1 … (add_globals_match … initW … Mvars)) |
---|
259 | [ % |*:] |
---|
260 | [ * #idr #v * #idr' #w #MVE % |
---|
261 | [ inversion MVE |
---|
262 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % |
---|
263 | | @(H … MVE) |
---|
264 | ] |
---|
265 | | @(matching_fns_get_same_blocks … Mfn) |
---|
266 | #f #g @match_funct_entry_id |
---|
267 | ] |
---|
268 | qed. |
---|
269 | |
---|
270 | lemma symbol_for_block_transf : |
---|
271 | ∀A,B,V,init.∀prog_in : program A V. |
---|
272 | ∀trans : ∀vars.A vars → B vars. |
---|
273 | let prog_out ≝ transform_program … prog_in trans in |
---|
274 | ∀bl. |
---|
275 | symbol_for_block … (globalenv … init prog_out) bl = |
---|
276 | symbol_for_block … (globalenv … init prog_in) bl. |
---|
277 | #A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?)) |
---|
278 | #v0 #w0 * // |
---|
279 | qed. |
---|
280 | |
---|
281 | lemma vars_irrelevant_to_find_funct_ptr_inv : |
---|
282 | ∀F,G,V,W. |
---|
283 | ∀P:F → G → Prop. |
---|
284 | ∀init,init',b,vars,vars',ge,ge',m,m',f. |
---|
285 | (find_funct_ptr G ge' b = Some ? f → ∃f'. find_funct_ptr F ge b = Some ? f' ∧ P f' f) → |
---|
286 | symbols F ge = symbols G ge' → |
---|
287 | nextblock m = nextblock m' → |
---|
288 | All2 … (λx,y. \fst x = \fst y) vars vars' → |
---|
289 | find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f → |
---|
290 | ∃f'.find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f' ∧ P f' f. |
---|
291 | #F #G #V #W #P #init #init' |
---|
292 | * * [ 2,3(*,5,6*): #blk ] [ 2: | 1,3: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 whd in H5:(??%?); destruct ] |
---|
293 | #vars elim vars |
---|
294 | [ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H |
---|
295 | | #x #tl #ge #ge' #m #m' #f #_ #_ #_ * |
---|
296 | ] |
---|
297 | | * * #id #r #v #tl #IH * |
---|
298 | [ #ge #ge' #m #m' #f #_ #_ #_ * |
---|
299 | | * * #id' #r' #v' #tl' |
---|
300 | #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH |
---|
301 | whd in match (add_globals ?????); whd in match (add_globals F ????); |
---|
302 | whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?)); |
---|
303 | @(alloc_pair … Enext) #m1 #m2 #b #Enext' |
---|
304 | whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?)); |
---|
305 | #FFP |
---|
306 | @(IH … MATCH FFP) |
---|
307 | [ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
308 | whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?)); |
---|
309 | >Esym |
---|
310 | cases ( lookup SymbolTag block (symbols G ge') id') |
---|
311 | [ @FFP1 |
---|
312 | | * * (* * *) try @FFP1 #p try @FFP1 |
---|
313 | normalize |
---|
314 | cases (decidable_eq_pos blk p) |
---|
315 | [ #E destruct >lookup_opt_pm_set_hit #E destruct |
---|
316 | | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE) |
---|
317 | @FFP1 |
---|
318 | ] |
---|
319 | ] |
---|
320 | | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
321 | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
322 | >Esym % |
---|
323 | | assumption |
---|
324 | ] |
---|
325 | ] |
---|
326 | ] qed. |
---|
327 | |
---|
328 | lemma All2_swap : ∀ A,B,P,l1,l2. All2 A B P l1 l2 → |
---|
329 | All2 B A (λx,y.P y x) l2 l1. |
---|
330 | #A #B #P #l1 elim l1 [* [ #_ @I] #b #tlb *] |
---|
331 | #a #tl_a #IH * [ *] #b #tl_b * #H #H1 whd % [assumption] |
---|
332 | @IH assumption |
---|
333 | qed. |
---|
334 | |
---|
335 | lemma find_funct_ptr_All2_inv : ∀A,B,V,W,b,p. |
---|
336 | ∀initV,initW,p',P.∀f : B (prog_var_names B W p'). |
---|
337 | All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') → |
---|
338 | All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') → |
---|
339 | find_funct_ptr … (globalenv B W initW p') b = Some ? f → |
---|
340 | ∃f'. find_funct_ptr … (globalenv A V initV p) b = Some ? f' ∧ P f' f. |
---|
341 | #A #B #V #W #b * #vars #fns #main #initV #initW * #vars' #fns' #main' #P #f |
---|
342 | #Mfns |
---|
343 | cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ] |
---|
344 | [ 2: (*12:*) | *: #_ #F whd in F:(??%?); destruct ] |
---|
345 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
346 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
347 | @vars_irrelevant_to_find_funct_ptr_inv |
---|
348 | [ letin varnames ≝ (map ??? vars) |
---|
349 | generalize in match fns in Mfns ⊢ %; |
---|
350 | elim fns' |
---|
351 | [ #fns #Mfns whd in ⊢ (??%? → ?); #E destruct |
---|
352 | | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl |
---|
353 | whd in ⊢ (??%? → ?); |
---|
354 | whd in match (functions ??); |
---|
355 | change with (add_functs ???) in match (foldr ?????); |
---|
356 | cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … (All2_swap … Mtl)) * #idA #a * #idB #b * // ] |
---|
357 | #SYMS #NEXT |
---|
358 | cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl))) |
---|
359 | [ #E destruct >lookup_opt_insert_hit #E destruct |
---|
360 | %{fn'} % // whd in ⊢ (??%?); |
---|
361 | whd in match (functions ??); |
---|
362 | change with (add_functs ???) in match (foldr ???? tl'); |
---|
363 | >NEXT >lookup_opt_insert_hit @refl |
---|
364 | | #NE >lookup_opt_insert_miss // |
---|
365 | #FFP cases (IH tl' Mtl ?) |
---|
366 | [ #fn'' * #FFP' #P' %{fn''} % |
---|
367 | [ whd in ⊢ (??%?); |
---|
368 | >lookup_opt_insert_miss [2: <NEXT // ] |
---|
369 | lapply (lookup_drop_fn_different ????? FFP) |
---|
370 | >SYMS |
---|
371 | #L >lookup_drop_fn_irrelevant // @FFP' |
---|
372 | | @P' |
---|
373 | ] |
---|
374 | | @(drop_fn_lfn … FFP) |
---|
375 | ] |
---|
376 | ] |
---|
377 | ] |
---|
378 | | cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ] |
---|
379 | #S #_ @S |
---|
380 | | @refl |
---|
381 | ] qed. |
---|
382 | |
---|
383 | lemma find_funct_ptr_match_inv: |
---|
384 | ∀M:matching.∀initV,initW. |
---|
385 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
386 | ∀MATCH:match_program … M p p'. |
---|
387 | ∀b: block. ∀tf: m_B M (prog_var_names … p'). |
---|
388 | find_funct_ptr … (globalenv … initW p') b = Some ? tf → |
---|
389 | ∃f : m_A M (prog_var_names … p). |
---|
390 | find_funct_ptr … (globalenv … initV p) b = Some ? f ∧ |
---|
391 | match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). |
---|
392 | [ 2: >(matching_vars … (mp_vars … MATCH)) % ] |
---|
393 | * #A #B #V #W #match_fn #match_var #initV #initW |
---|
394 | #p #p' * #Mvars #Mfn #Mmain |
---|
395 | #b #f #FFP @(find_funct_ptr_All2_inv A B V W ????????? FFP) |
---|
396 | [ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars) |
---|
397 | #E |
---|
398 | @(All2_mp … Mfn) |
---|
399 | * #id #f * #id' #f' |
---|
400 | <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E |
---|
401 | normalize #H @(match_funct_entry_inv … H) |
---|
402 | #vs #id1 #f1 #f2 #M % // |
---|
403 | | @(All2_mp … Mvars) |
---|
404 | * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct // |
---|
405 | qed. |
---|
406 | |
---|
407 | lemma find_funct_ptr_transf_none : |
---|
408 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
409 | ∀b: block. |
---|
410 | find_funct_ptr ? (globalenv … iV p) b = None ? → |
---|
411 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?. |
---|
412 | #A #B #V #iV #p #transf #b #EQf inversion(find_funct_ptr ???) [#_ %] |
---|
413 | #tf #EQtf |
---|
414 | cases (find_funct_ptr_match_inv … (transform_program_match … transf ?) … EQtf) |
---|
415 | [2: @iV] #f * #EQf' #_ >EQf in EQf'; #ABS destruct |
---|
416 | qed. |
---|
417 | |
---|
418 | lemma find_funct_ptr_transf_commute : |
---|
419 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
420 | ∀b: block. |
---|
421 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = |
---|
422 | ! f ← find_funct_ptr ? (globalenv … iV p) b; |
---|
423 | return transf … f. |
---|
424 | #A #B #V #iV #p #transf #bl inversion(find_funct_ptr ? (globalenv … iV p) bl) |
---|
425 | [ #EQ >(find_funct_ptr_transf_none … transf … EQ) %] |
---|
426 | #f #EQ >(find_funct_ptr_transf … transf … EQ) % |
---|
427 | qed. |
---|
428 | |
---|
429 | |
---|
430 | |
---|
431 | |
---|
432 | |
---|
433 | |
---|