Changeset 2107


Ignore:
Timestamp:
Jun 22, 2012, 2:07:38 PM (5 years ago)
Author:
campbell
Message:

Memory initialisation and program transformations.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2105 r2107  
    10651065] qed.
    10661066
    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 
    10711067
    10721068lemma initial_state_in_simulation : ∀p,s.
     
    10861082[ whd in ⊢ (??%?);
    10871083  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 ⊢ (??%?);
    10891085  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
    10901086  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
  • src/common/Globalenvs.ma

    r2105 r2107  
    259259] qed.
    260260
    261 lemma matching_globals_get_same_blocks : ∀A,B,V,W,initV,initW.
     261lemma add_globals_match : ∀A,B,V,W,initV,initW.
    262262  ∀P:(ident × region × V) → (ident × region × W) → Prop.
    263263  (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     
    265265  symbols ? ge = symbols … ge' →
    266266  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').
    268269#A #B #V #W #initV #initW #P #varsOK
    269270#vars elim vars
    270 [ #ge #ge' #m * [ #E #_ @E | #h #t #_ * ]
     271[ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ]
    271272| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
    272273  * * #id' #r' #w #tl' #E * #p #TL
     
    277278  cases (varsOK … p) #E1 #E2
    278279  destruct >E2 cases (alloc ????) #m' #b
    279   @IH //
     280  @IH /2/
    280281  whd in match (add_symbol ????);
    281282  whd in match (add_symbol ????);
     
    387388  and operations over global environments. *)
    388389
    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;
    392390  find_funct_ptr_rev_transf:
    393391    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
     
    615613change with (add_globals ?????) in match (foldl ?????);
    616614change 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)
    620617  #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) ]
    621619] qed.
    622620 
     
    672670qed.
    673671
    674 (* Package up transform_program results nicely. *)
     672lemma 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
     676whd in ⊢ (??%%);
     677cases d #d' try @refl
     678#id #n whd in ⊢ (??%%);
     679whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
     680qed.
     681
     682lemma 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
     696lemma 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
     704whd in ⊢ (? → ? → ??%%);
     705generalize in match (OK ? m);
     706elim 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
     724lemma
     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
     732whd in ⊢ (??%%);
     733change with (add_globals ?????) in match (globalenv_allocmem ??? p');
     734change with (add_globals ?????) in match (globalenv_allocmem ??? p);
     735cases (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
     748lemma
     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//
     755qed.
     756   
     757
     758(* Package up transform_program results for global envs nicely. *)
    675759
    676760record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     
    732816    ∀s: ident.
    733817    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*)
    740819(*
    741820Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
Note: See TracChangeset for help on using the changeset viewer.