source: src/common/extraGlobalenvs.ma @ 3367

Last change on this file since 3367 was 2783, checked in by piccolo, 7 years ago

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

File size: 15.5 KB
Line 
1include "common/AST.ma".
2include "common/Globalenvs.ma".
3
4(*
5axiom find_funct_ptr_symbol_inversion:
6    ∀F,V,init. ∀p: program F V.
7    ∀id: ident. ∀b: block. ∀f: F ?.
8    find_symbol ? (globalenv ?? init p) id = Some ? b →
9    find_funct_ptr ? (globalenv ?? init p) b = Some ? f →
10    In … (prog_funct ?? p) 〈id, f〉.
11
12axiom find_funct_ptr_exists:
13    ∀F,V,init. ∀p: program F V. ∀id: ident. ∀f: F ?.
14    In … (prog_funct ?? p) 〈id, f〉 →
15    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b
16      ∧ find_funct_ptr ? (globalenv ?? init p) b = Some ? f.
17
18axiom find_symbol_exists:
19    ∀F,V,init. ∀p: program F V.
20           ∀id: ident. ∀r,v.
21    In ? (prog_vars ?? p) 〈〈id, r〉, v〉 →
22    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b.
23
24definition is_function ≝ λF.λge : genv_t F.
25  λi : ident.∃fd.
26    ! bl ← find_symbol … ge i ;
27    find_funct_ptr … ge bl = Some ? fd.
28
29definition is_internal_function ≝ λF.λge : genv_t (fundef F).
30  λi : ident.∃fd.
31    ! bl ← find_symbol … ge i ;
32    find_funct_ptr … ge bl = Some ? (Internal ? fd).
33
34definition is_internal_function_of_program :
35  ∀A.program (λvars.fundef (A vars)) ℕ → ident → Prop ≝
36  λA,prog,i.is_internal_function … (globalenv_noinit … prog) i.
37
38definition funct_of_ident : ∀F,ge.
39  ident → option (Σi.is_function F ge i)
40≝ λF,ge,i.
41match ?
42return λx.! bl ← find_symbol … ge i ;
43    find_funct_ptr … ge bl = x → ?
44with
45[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
46| None ⇒ λ_.None ?
47] (refl …).
48*)
49
50lemma symbol_of_function_block_ok :
51  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
52#F #ge #b #FFP
53cut (∀A,B : Type[0].∀P : B → Prop.∀x : option A.∀c1,c2.
54  (∀v.∀prf : x = Some ? v.P (c1 v prf)) →
55  (∀prf:x = None ?.P (c2 prf)) →
56  P (match x return λy.x = y → ? with
57     [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf]
58     (refl …))) [ #A #B #P * // ] #aux
59whd in ⊢ (???(??%)); @aux [//] #H
60generalize in match (? : False); *
61qed.
62
63(*
64definition funct_of_block : ∀F,ge.
65  block → option  (Σi.is_function F ge i) ≝
66λF,ge,bl.
67   match find_funct_ptr … ge bl
68   return λx.find_funct_ptr … ge bl = x → ? with
69   [ Some fd ⇒ λprf.return mk_Sig
70        ident (λi.is_function F ge i)
71        (symbol_of_function_block … ge bl ?)
72        (ex_intro … fd ?)
73   | None ⇒ λ_.None ?
74   ] (refl …).
75[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
76| >prf % #ABS destruct(ABS)
77]
78qed.
79
80definition block_of_funct ≝ λF,ge.
81  λi : Σi.is_function F ge i.
82  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
83  [ Some bl ⇒ λ_.bl
84  | None ⇒ λprf.⊥
85  ] (pi2 … i).
86cases prf #fd normalize #ABS destruct(ABS)
87qed.
88
89definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝
90λF,ge,i.
91match ! bl ← find_symbol … ge i ;
92        find_funct_ptr … ge bl
93return λx.(∃fd.x = ?) → ?
94with
95[ Some fd ⇒ λ_.fd
96| None ⇒ λprf.⊥
97] (pi2 … i).
98cases prf #fd #ABS destruct
99qed.
100
101lemma description_of_internal_function : ∀F,ge,i,fn.
102  description_of_function ? ge i = Internal F fn → is_internal_function … ge i.
103#F #ge * #i * #fd #EQ
104#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
105%{EQ}
106qed.
107
108definition int_funct_of_block : ∀F,ge.
109  block → option (Σi.is_internal_function F ge i) ≝
110  λF,ge,bl.
111  ! f ← funct_of_block … ge bl ;
112  match ?
113  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
114  with
115  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
116  | External fn ⇒ λ_.None ?
117  ] (refl …).
118@(description_of_internal_function … prf)
119qed.
120
121lemma internal_function_is_function : ∀F,ge,i.
122  is_internal_function F ge i → is_function … ge i.
123#F #ge #i * #fn #prf %{prf} qed.
124
125definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝
126λF,ge,i.
127match ! bl ← find_symbol … ge i ;
128        find_funct_ptr … ge bl
129return λx.(∃fn.x = ?) → ?
130with
131[ Some fd ⇒
132  match fd return λx.(∃fn.Some ? x = ?) → ? with
133  [ Internal fn ⇒ λ_.fn
134  | External _ ⇒ λprf.⊥
135  ]
136| None ⇒ λprf.⊥
137] (pi2 … i).
138cases prf #fn #ABS destruct
139qed.
140
141lemma if_propagate :
142∀A_in,A_out.
143∀trans.
144∀prog_in : program (λvars.fundef (A_in vars)) ℕ.
145let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝
146  transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
147∀i.is_internal_function_of_program … prog_in i →
148is_internal_function_of_program … prog_out i.
149#A_in #A_out #trans #prog_in #ident
150* #ifn
151inversion (find_symbol ???) [ #_ #ABS whd in ABS : (??%%); destruct(ABS) ]
152#bl #EQfind >m_return_bind #EQfunct_ptr
153%{(trans … ifn)}
154>find_symbol_transf >EQfind >m_return_bind
155>(find_funct_ptr_transf … EQfunct_ptr) %
156qed.
157
158lemma block_of_funct_ident_is_code : ∀F,ge,i.
159  block_region (block_of_funct F ge i) = Code.
160#F #ge * #i * #fd
161whd in ⊢ (?→??(?%)?);
162cases (find_symbol ???)
163[ #ABS normalize in ABS; destruct(ABS) ]
164#bl normalize nodelta >m_return_bind
165whd in ⊢ (??%?→?); cases (block_region bl)
166[ #ABS normalize in ABS; destruct(ABS) ]
167#_ %
168qed.
169
170lemma prog_if_of_function_transform :
171  ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ.
172  let prog_out : program (λvars.fundef (B vars)) ℕ ≝
173    transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
174  ∀i_out : Σi.is_internal_function_of_program … prog_out i.
175  ∀i_in : Σi.is_internal_function_of_program … prog_in i.
176  pi1 … i_out = pi1 … i_in →
177  if_of_function … i_out = trans … (if_of_function … i_in).
178#A #B #trans #prog * #i1 #i_prf1 * #i2 #i_prf2 #EQ destruct(EQ)
179cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
180  ∀m.∀prf : Q m.∀f1,f2.
181  (∀x,prf.m = Some ? x → P (f1 x prf)) →
182  (∀prf.m = None ? → P (f2 prf)) →
183  P (match m return λx.Q x → ? with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
184  [ #A #B #Q #P * /2 by / ] #aux
185whd in ⊢ (??%?); @aux
186[2: #prf #EQ generalize in match (? : False); * ]
187#fd * #ifn #EQ1 #EQ destruct normalize nodelta
188whd in ⊢ (???(??%)); @aux
189[2: #prf #EQ generalize in match (? : False); * ]
190#fd' * #ifn' #EQ1' #EQ' destruct normalize nodelta
191inversion (find_symbol ???) in EQ'; [ #_ #ABS whd in ABS: (??%%); destruct ]
192#bl #EQfind >m_return_bind #EQfunct
193>find_symbol_transf in EQ; >EQfind >m_return_bind
194>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
195qed.
196*)
197
198include alias "common/PositiveMap.ma".
199
200lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
201id < (nextfunction ? ge) →
202lookup_opt … id (functions ? ge) = None ? →
203lookup_opt … id (functions … (add_functs F ge l)) = None ?.
204#F #ge #l #id whd in match add_functs; normalize nodelta
205elim l -l [ #_ normalize //]
206* #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
207>lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
208#f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
209| cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
210[elim tl [normalize //]
211#x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
212#H2 lapply(transitive_le … H H2) @lt_to_not_eq
213qed.
214
215lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
216lookup_opt … id (functions ? (\fst gem)) = None ? →
217lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?.
218#F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
219** #x1 #x2 #x3 #tl whd in match add_globals;
220normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
221cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
222normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
223#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
224qed.
225
226 
227lemma globalenv_no_minus_one :
228 ∀F,V,i,p.
229  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?.
230#F #V #i #p
231whd in match find_funct_ptr; normalize nodelta
232whd in match globalenv;
233whd in match globalenv_allocmem; normalize nodelta
234@add_globals_functions_miss @add_functs_functions_miss normalize //
235qed.
236
237lemma globalenv_no_zero :
238 ∀F,V,i,p.
239  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. //
240qed.
241
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 TracBrowser for help on using the repository browser.