Changeset 2783 for src/common/extraGlobalenvs.ma
 Timestamp:
 Mar 6, 2013, 12:09:52 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/extraGlobalenvs.ma
r2608 r2783 240 240 qed. 241 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
Note: See TracChangeset
for help on using the changeset viewer.