Ignore:
Timestamp:
Jun 21, 2012, 5:21:04 PM (8 years ago)
Author:
campbell
Message:

Show some results about globalenvs and program transformations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2010 r2105  
    202202definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
    203203λF,p.
    204   \fst (globalenv_allocmem F nat (λn.[Init_space n]) p).
     204  globalenv F nat (λn.[Init_space n]) p.
    205205
    206206(* Return the initial memory state for the given program. *)
     
    242242] qed.
    243243
     244
     245lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m.
     246  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b.
     247#F #V #init * * // * // #blk
     248whd in ⊢ (? → ? → ? → ??%%);
     249#vars elim vars
     250[ #ge #m %
     251| * * #id #r #v #tl #IH #ge #m
     252  whd in match (add_globals ?????);
     253  whd in ⊢ (??(???(??(???(????%?))))?);
     254  cases (alloc ????) #m' #b
     255  whd in ⊢ (??(???(??(???(????%?))))?);
     256  >IH cases ge #fnmap #nextblock #symmap
     257  whd in ⊢ (??(???%)?);
     258  %
     259] qed.
     260
     261lemma matching_globals_get_same_blocks : ∀A,B,V,W,initV,initW.
     262  ∀P:(ident × region × V) → (ident × region × W) → Prop.
     263  (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     264  ∀vars,ge,ge',m,vars'.
     265  symbols ? ge = symbols … ge' →
     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')).
     268#A #B #V #W #initV #initW #P #varsOK
     269#vars elim vars
     270[ #ge #ge' #m * [ #E #_ @E | #h #t #_ * ]
     271| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
     272  * * #id' #r' #w #tl' #E * #p #TL
     273  whd in match (add_globals A ????);
     274  change with (add_globals A ????) in match (foldl ?????);
     275  whd in match (add_globals B ????);
     276  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
     277  cases (varsOK … p) #E1 #E2
     278  destruct >E2 cases (alloc ????) #m' #b
     279  @IH //
     280  whd in match (add_symbol ????);
     281  whd in match (add_symbol ????);
     282  >E %
     283] qed.
     284
     285lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
     286  (∀f,g. P f g → \fst f = \fst g) →
     287  ∀fns,fns'.
     288  All2 … P fns fns' →
     289  let ge ≝ add_functs A (empty ?) fns in
     290  let ge' ≝ add_functs B (empty ?) fns' in
     291  nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'.
     292#A #B #P #fnOK #fns elim fns
     293[ * [ #_ % % | #h #t * ]
     294| * #id #f #tl #IH * [ * ]
     295  * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H
     296  whd in match (add_functs ???);
     297  change with (add_functs ???) in match (foldr ?????);
     298  whd in match (add_functs B ??);
     299  change with (add_functs ???) in match (foldr (ident × B) ????);
     300  cases (IH tl' H) #E1 #E2
     301  % [ >E1 % | >E1 >E2 % ]
     302] qed.
     303
     304lemma matching_fns_get_same_blocks :  ∀A,B,P.
     305  (∀f,g. P f g → \fst f = \fst g) →
     306  ∀fns,fns'.
     307  All2 … P fns fns' →
     308  let ge ≝ add_functs A (empty ?) fns in
     309  let ge' ≝ add_functs B (empty ?) fns' in
     310  symbols … ge = symbols … ge'.
     311#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
     312qed.
    244313
    245314(*
     
    318387  and operations over global environments. *)
    319388
    320   find_funct_ptr_transf:
    321     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    322     ∀b: block. ∀f: A.
    323     find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    324     find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f);
    325   find_funct_transf:
    326     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    327     ∀v: val. ∀f: A.
    328     find_funct ? (globalenv ?? p) v = Some ? f →
    329     find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f);
    330   find_symbol_transf:
    331     ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    332     ∀s: ident.
    333     find_symbol ? (globalenv ?? (transform_program … transf p)) s =
    334     find_symbol ? (globalenv ?? p) s;
    335389  init_mem_transf:
    336390    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
     
    434488(* * Commutation properties between matching between programs
    435489  and operations over global environments. *)
     490*) *)
     491
     492(* First, show that nextfunction only depends on the number of functions: *)
     493
     494let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
     495match n with
     496[ O ⇒ p
     497| S m ⇒ succ (nat_plus_pos m p)
     498].
     499
     500lemma nextfunction_length : ∀A,l,ge.
     501  nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge).
     502#A #l elim l // #h #t #IH #ge
     503whd in ⊢ (??%%); >IH //
     504qed.
     505
     506(* Now link functions in related programs, but without dealing with the type
     507   casts yet. *)
     508
     509lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
     510  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
     511  All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
     512  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
     513#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
     514cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ]
     515[ 12: | *: #F whd in F:(??%?); destruct ]
     516>vars_irrelevant_to_find_funct_ptr
     517>vars_irrelevant_to_find_funct_ptr
     518letin varnames ≝ (map ??? vars)
     519cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
     520//
     521cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
     522//
     523generalize in match (empty ?);
     524generalize in match (empty ?);
     525generalize in match fns';
     526elim fns
     527[ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct
     528| * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?);
     529  whd in match (functions ??);
     530  change with (add_functs ???) in match (foldr ?????);
     531  cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl)))
     532  [ #E destruct  >lookup_opt_insert_hit #E destruct
     533    cases fns' [ * ]
     534    * #id' #fn' #tl' * #M #Mtl
     535    %{fn'} % // whd in ⊢ (??%?);
     536    whd in match (functions ??);
     537    change with (add_functs ???) in match (foldr ???? tl');
     538    >nextfunction_length >nextfunction_length <NF >(All2_length  … Mtl)
     539    >lookup_opt_insert_hit @refl
     540  | #NE >lookup_opt_insert_miss //
     541    #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl
     542    cases (IH ?????? Mtl)
     543    [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ]
     544    | skip
     545    | 4: @NF
     546    | skip
     547    | //
     548    | @FFP
     549    ]
     550  ]
     551] qed.
     552
     553discriminator Prod.
     554
     555(* Now prove the full version. *)
     556
     557lemma find_funct_ptr_match:
     558    ∀M:matching.∀initV,initW.
     559    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     560    ∀MATCH:match_program … M p p'.
     561    ∀b: block. ∀f: m_A M (prog_var_names … p).
     562    find_funct_ptr … (globalenv … initV p) b = Some ? f →
     563    ∃tf : m_B M (prog_var_names … p').
     564    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
     565[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
     566* #A #B #V #W #match_fn #match_var #initV #initW
     567#p #p' * #Mvars #Mfn #Mmain
     568#b #f #FFP
     569@(find_funct_ptr_All2 A B V W ??????? FFP)
     570lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
     571#E
     572@(All2_mp … Mfn)
     573* #id #f * #id' #f'
     574<E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
     575normalize #H @(match_funct_entry_inv … H) //
     576qed.
     577
     578lemma
     579  find_funct_ptr_transf_partial2:
     580    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
     581           ∀p: program A V. ∀p': program B W.
     582    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
     583    ∀b: block. ∀f: A ?.
     584    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
     585    ∃f'.
     586    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
     587#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
     588cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
     589[2: @iW
     590| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
     591#TF %{f'} % //
     592-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
     593qed.
     594
     595lemma match_funct_entry_id : ∀M,vs,vs',f,g.
     596  match_funct_entry M vs vs' f g → \fst f = \fst g.
     597#M #vs #vs' #f #g * //
     598qed.
     599
     600lemma
     601  find_symbol_match:
     602    ∀M:matching.
     603    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     604    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     605    match_program … M p p' →
     606    ∀s: ident.
     607    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
     608* #A #B #V #W #match_fun #match_var #initV #initW #initsize
     609* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
     610whd in ⊢ (??%%);
     611@sym_eq
     612@(eq_f ??(λx. lookup SymbolTag block x s))
     613whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     614whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     615change with (add_globals ?????) in match (foldl ?????);
     616change 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)
     620  #f #g @match_funct_entry_id
     621] qed.
     622 
     623lemma
     624  find_symbol_transf_partial2:
     625    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
     626    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
     627           ∀p: program A V. ∀p': program B W.
     628    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
     629    ∀s: ident.
     630    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
     631#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
     632@(find_symbol_match … (transform_partial_program2_match … TPP2))
     633#v0 #w0 * #id #r #v #w @sizeOK
     634qed.
     635
     636lemma
     637  find_funct_ptr_transf:
     638    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
     639    ∀b: block. ∀f: A ?.
     640    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
     641    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
     642#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
     643cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
     644[ 2: @iV
     645| #f' * #FFP'
     646  generalize in match (matching_vars ????);
     647  whd in match (prog_var_names ???); whd in match (prog_vars ???);
     648  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
     649] qed.
     650
     651lemma
     652  find_funct_transf:
     653    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
     654    ∀v: val. ∀f: A ?.
     655    find_funct ? (globalenv … iV p) v = Some ? f →
     656    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
     657#A #B #V #iV #tf #p #v #f #FF
     658cases (find_funct_find_funct_ptr ???? FF)
     659#r * #b * #pc * #E destruct #FFP
     660change with (find_funct_ptr ???) in ⊢ (??%?);
     661@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
     662qed.
     663
     664lemma
     665  find_symbol_transf:
     666    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
     667    ∀s: ident.
     668    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
     669    find_symbol ? (globalenv … iV p) s.
     670#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
     671#v0 #w0 * //
     672qed.
     673
     674(* Package up transform_program results nicely. *)
     675
     676record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     677  rg_find_symbol: ∀s.
     678    find_symbol … ge s = find_symbol … ge' s;
     679  rg_find_funct: ∀v,f.
     680    find_funct … ge v = Some ? f →
     681    find_funct … ge' v = Some ? (t f);
     682  rg_find_funct_ptr: ∀b,f.
     683    find_funct_ptr … ge b = Some ? f →
     684    find_funct_ptr … ge' b = Some ? (t f)
     685}.
     686
     687theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
     688  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
     689#A #B #V #iV #p #tf %
     690[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
     691| @(find_funct_transf A B V iV tf p)
     692| @(find_funct_ptr_transf A B V iV p tf)
     693] qed.
     694
     695
     696(*
    436697
    437698  find_funct_ptr_match:
     
    475736           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    476737    match_program … match_fun match_var p p' →
    477     init_mem ?? p' = init_mem ?? p*)*)
     738    init_mem ?? p' = init_mem ?? p*)
    478739
    479740(*
Note: See TracChangeset for help on using the changeset viewer.