Changeset 2783 for src/common


Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

Location:
src/common
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraMonads.ma

    r2590 r2783  
    305305#y * #y_spec #v_spec %{y} % // >y_spec %
    306306qed.
     307
     308lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
     309res_preserve1 X Y F n (Error … e).
     310#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
     311qed.
  • src/common/GenMem.ma

    r2608 r2783  
    207207    let blocks ≝ update_block … b content (blocks … m) in
    208208     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
     209     
     210(* Axiom of extensional equality for the memory *)     
     211axiom mem_ext_eq :
     212  ∀m1,m2 : mem.
     213  (∀b.let bc1 ≝ blocks m1 b in
     214      let bc2 ≝ blocks m2 b in
     215      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
     216      ∀z.contents bc1 z = contents bc2 z) →
     217  nextblock m1 = nextblock m2 → m1 = m2.     
     218
  • src/common/extraGlobalenvs.ma

    r2608 r2783  
    240240qed.
    241241
     242lemma 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
     254whd in match symbol_for_block; normalize nodelta
     255whd in match globalenv in ⊢ (???%); normalize nodelta
     256whd in match (globalenv_allocmem ????);
     257change 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]
     268qed.
     269
     270lemma 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 * //
     279qed.
     280
     281lemma 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
     328lemma All2_swap : ∀ A,B,P,l1,l2. All2 A B P l1 l2 →
     329All2 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
     333qed.
     334
     335lemma 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
     343cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ]
     344[ 2: (*12:*) | *: #_ #F whd in F:(??%?); destruct ]
     345whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     346whd 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
     383lemma 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 //
     405qed.
     406
     407lemma 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
     414cases (find_funct_ptr_match_inv … (transform_program_match … transf ?) … EQtf)
     415[2: @iV] #f * #EQf' #_ >EQf in EQf'; #ABS destruct
     416qed.
     417
     418lemma 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) %
     427qed.
     428   
     429   
     430
     431
     432
     433
Note: See TracChangeset for help on using the changeset viewer.