Changeset 2107
- Timestamp:
- Jun 22, 2012, 2:07:38 PM (6 years ago)
- Location:
- src
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/labelSimulation.ma
r2105 r2107 1065 1065 ] qed. 1066 1066 1067 (* FIXME: to globalenvs and prove *)1068 axiom transform_program_init_mem : ∀A,B,V,p,f,init.1069 init_mem ?? init p = init_mem ?? init (transform_program A B V p f).1070 1071 1067 1072 1068 lemma initial_state_in_simulation : ∀p,s. … … 1086 1082 [ whd in ⊢ (??%?); 1087 1083 change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?); 1088 <transform_program_init_mem>Em in ⊢ (??%?);1084 >init_mem_transf >Em in ⊢ (??%?); 1089 1085 whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); 1090 1086 whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain') -
src/common/Globalenvs.ma
r2105 r2107 259 259 ] qed. 260 260 261 lemma matching_globals_get_same_blocks: ∀A,B,V,W,initV,initW.261 lemma add_globals_match : ∀A,B,V,W,initV,initW. 262 262 ∀P:(ident × region × V) → (ident × region × W) → Prop. 263 263 (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → … … 265 265 symbols ? ge = symbols … ge' → 266 266 All2 … P vars vars' → 267 symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')). 267 symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧ 268 \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars'). 268 269 #A #B #V #W #initV #initW #P #varsOK 269 270 #vars elim vars 270 [ #ge #ge' #m * [ #E #_ @E | #h #t #_ * ]271 [ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ] 271 272 | * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ] 272 273 * * #id' #r' #w #tl' #E * #p #TL … … 277 278 cases (varsOK … p) #E1 #E2 278 279 destruct >E2 cases (alloc ????) #m' #b 279 @IH / /280 @IH /2/ 280 281 whd in match (add_symbol ????); 281 282 whd in match (add_symbol ????); … … 387 388 and operations over global environments. *) 388 389 389 init_mem_transf:390 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.391 init_mem ?? (transform_program … transf p) = init_mem ?? p;392 390 find_funct_ptr_rev_transf: 393 391 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. … … 615 613 change with (add_globals ?????) in match (foldl ?????); 616 614 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???); 617 @(matching_globals_get_same_blocks … Mvars) 618 [ * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ] 619 | @(matching_fns_get_same_blocks … Mfns) 615 @(proj1 … (add_globals_match … Mvars)) 616 [ @(matching_fns_get_same_blocks … Mfns) 620 617 #f #g @match_funct_entry_id 618 | * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ] 621 619 ] qed. 622 620 … … 672 670 qed. 673 671 674 (* Package up transform_program results nicely. *) 672 lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d. 673 symbols A ge = symbols … ge' → 674 store_init_data A ge m b o d = store_init_data B ge' m b o d. 675 #A #B #ge #ge' #m #b #o #d #SYM 676 whd in ⊢ (??%%); 677 cases d #d' try @refl 678 #id #n whd in ⊢ (??%%); 679 whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl 680 qed. 681 682 lemma store_init_data_list_symbols : ∀A,B,ge,ge',b. 683 symbols A ge = symbols … ge' → 684 ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d. 685 #A #B #ge #ge' #b #SYM #d elim d 686 [ // 687 | #hd #tl #IH #m #o 688 whd in ⊢ (??%%); 689 >(store_init_data_symbols … SYM) 690 cases (store_init_data ??????) 691 [ % 692 | #m' @IH 693 ] 694 ] qed. 695 696 lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop. 697 ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) → 698 ∀ge:genv_t A. ∀ge':genv_t B. 699 symbols … ge = symbols … ge' → 700 ∀m. ∀vars,vars'. 701 All2 … P vars vars' → 702 init_globals A V iV ge m vars = init_globals B W iW ge' m vars'. 703 #A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars 704 whd in ⊢ (? → ? → ??%%); 705 generalize in match (OK ? m); 706 elim vars 707 [ #rm * 708 [ #_ % 709 | #h #t * 710 ] 711 | * #idr #v #tl #IH #rm 712 * [ * ] 713 * #idr' #w #tl' 714 * #p cases (varsOK … p) #E1 #E2 destruct #TL 715 whd in ⊢ (??%%); cases idr' #id #r cases rm #m' 716 whd in ⊢ (??(????%?)(????%?)); 717 [ whd in match (find_symbol ?? id); 718 whd in match (find_symbol B ? id); 719 >SYM cases (lookup ??? id) 720 [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ] 721 ] @IH // 722 ] qed. 723 724 lemma 725 init_mem_match: 726 ∀M:matching. 727 ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) → 728 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 729 match_program … M p p' → 730 init_mem … iW p' = init_mem … iV p. 731 * #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain 732 whd in ⊢ (??%%); 733 change with (add_globals ?????) in match (globalenv_allocmem ??? p'); 734 change with (add_globals ?????) in match (globalenv_allocmem ??? p); 735 cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars) 736 [ 8: @(matching_fns_get_same_blocks … Mfns) 737 #f0 #g0 * // 738 | cases (add_globals ?????) #ge1 #m1 739 cases (add_globals ?????) #ge2 #m2 740 #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars) 741 [ #v0 #w0 * #id #r #v #w /3/ 742 | @SYM 743 ] 744 | 4: #v0 #w0 * #id #r #v #w #V % // >iSAME // 745 | *: skip 746 ] qed. 747 748 lemma 749 init_mem_transf: 750 ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. 751 init_mem … iV (transform_program … p transf) = init_mem … iV p. 752 #A #B #C #iV #transf #p 753 @(init_mem_match … (transform_program_match … transf ?)) 754 // 755 qed. 756 757 758 (* Package up transform_program results for global envs nicely. *) 675 759 676 760 record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ { … … 732 816 ∀s: ident. 733 817 find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; 734 init_mem_match: 735 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 736 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 737 match_program … match_fun match_var p p' → 738 init_mem ?? p' = init_mem ?? p*) 739 818 *) 740 819 (* 741 820 Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
Note: See TracChangeset
for help on using the changeset viewer.