source: src/common/Globalenvs.ma @ 2428

Last change on this file since 2428 was 2415, checked in by campbell, 7 years ago

Add the ability to map blocks to symbols in preparation for stack space.

File size: 66.7 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Global environments are a component of the dynamic semantics of
17  all languages involved in the compiler.  A global environment
18  maps symbol names (names of functions and of global variables)
19  to the corresponding memory addresses.  It also maps memory addresses
20  of functions to the corresponding function descriptions. 
21
22  Global environments, along with the initial memory state at the beginning
23  of program execution, are built from the program of interest, as follows:
24- A distinct memory address is assigned to each function of the program.
25  These function addresses use negative numbers to distinguish them from
26  addresses of memory blocks.  The associations of function name to function
27  address and function address to function description are recorded in
28  the global environment.
29- For each global variable, a memory block is allocated and associated to
30  the name of the variable.
31
32  These operations reflect (at a high level of abstraction) what takes
33  place during program linking and program loading in a real operating
34  system. *)
35
36include "common/Errors.ma".
37include "common/AST.ma".
38(*include "Values.ma".*)
39include "common/FrontEndMem.ma".
40
41   (* * The type of global environments.  The parameter [F] is the type
42       of function descriptions. *)
43(* Functions are given negative block numbers *)
44record genv_t (F:Type[0]) : Type[0] ≝ {
45  functions: positive_map F;
46  nextfunction: Pos;
47  symbols: identifier_map SymbolTag block
48}.
49
50definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝
51λF,name_fun,g.
52  let blk_id ≝ nextfunction ? g in
53  let b ≝ mk_block Code (neg blk_id) in
54  mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g))
55              (succ blk_id)
56              (add ?? (symbols … g) (\fst name_fun) b).
57
58definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝
59λF,name,b,g.
60  mk_genv_t F (functions … g)
61              (nextfunction … g)
62              (add ?? (symbols … g) name b).
63
64(* Construct environment and initial memory store *)
65definition empty_mem ≝ empty. (* XXX*)
66definition empty : ∀F. genv_t F ≝
67  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??).
68
69definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝
70λF,init,fns.
71  foldr ?? (add_funct F) init fns.
72
73(* Return the address of the given global symbol, if any. *)
74definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
75λF,ge. lookup ?? (symbols … ge).
76
77(* init *)
78
79definition store_init_data : ∀F.genv_t F → mem → block → Z → init_data → option mem ≝
80λF,ge,m,b,p,id.
81  (* store checks that the address came from something capable of representing
82     addresses of the memory region in question - here there are no real
83     pointers, so use the real region. *)
84  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in
85  match id with
86  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
87  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
88  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
89  | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
90  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
91  | Init_addrof (*r'*) symb ofs ⇒
92      match find_symbol … ge symb with
93      [ None ⇒ None ?
94      | Some b' ⇒ (*
95        match pointer_compat_dec b' r' with
96        [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs))))
97        (*| inr _ ⇒ None ?
98        ]*)
99      ]
100  | Init_space n ⇒ Some ? m
101  | Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*))
102  ].
103(*cases b //
104qed.*)
105
106definition size_init_data : init_data → nat ≝
107 λi_data.match i_data with
108  [ Init_int8 _ ⇒ 1
109  | Init_int16 _ ⇒ 2
110  | Init_int32 _ ⇒ 4
111  | Init_float32 _ ⇒ 4
112  | Init_float64 _ ⇒ 8
113  | Init_space n ⇒ max n 0
114  | Init_null (*r*) ⇒ size_pointer (*r*)
115  | Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)].
116
117let rec store_init_data_list (F:Type[0]) (ge:genv_t F)
118                              (m: mem) (b: block) (p: Z) (idl: list init_data)
119                              on idl : option mem ≝
120  match idl with
121  [ nil ⇒ Some ? m
122  | cons id idl' ⇒
123      match store_init_data F ge m b p id with
124      [ None ⇒ None ?
125      | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl'
126      ]
127  ].
128
129definition size_init_data_list : list init_data → nat ≝
130  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data.
131
132(* Nonessential properties that may require arithmetic
133nremark size_init_data_list_pos:
134  ∀i_data. OZ ≤ size_init_data_list i_data.
135#i_data;elim i_data;//;
136#a;#tl;cut (OZ ≤ size_init_data a)
137##[cases a;normalize;//;
138   #x;cases x;normalize;//;
139##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
140   cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
141   ##[cases (size_init_data a) in Hsize IH;
142      ##[##1,2:/3/
143      ##|normalize;#n;#Hfalse;elim Hfalse]
144   ##|#Hdisc;cases Hdisc
145      ##[#Heq;nrewrite > Heq;//;
146      ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2;
147         (* TODO: arithmetics *) napply daemon]
148   ##]
149##]
150qed.
151*)
152
153
154(* init *)
155
156axiom InitDataStoreFailed : String.
157
158definition add_globals : ∀F,V:Type[0].
159       (V → (list init_data)) →
160       genv_t F × mem → list (ident × region × V) →
161       (genv_t F × mem) ≝
162λF,V,extract_init,init_env,vars.
163  foldl ??
164    (λg_st: genv_t F × mem. λid_init: ident × region × V.
165      let 〈id, r, init_info〉 ≝ id_init in
166      let init ≝ extract_init init_info in
167      let 〈g,st〉 ≝ g_st in
168        let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in
169          let g' ≝ add_symbol ? id b g in
170            〈g', st'〉
171        )
172    init_env vars.
173
174definition init_globals : ∀F,V:Type[0].
175       (V → (list init_data)) →
176       genv_t F → mem → list (ident × region × V) →
177       res mem ≝
178λF,V,extract_init,g,m,vars.
179  foldl ??
180    (λst: res mem. λid_init: ident × region × V.
181      let 〈id, r, init_info〉 ≝ id_init in
182      let init ≝ extract_init init_info in
183        do st ← st;
184        match find_symbol … g id with
185        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
186        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
187        ] )
188    (OK ? m) vars.
189
190definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv_t (F (prog_var_names … p)) × mem) ≝
191λF,V,init_info,p.
192  add_globals … init_info
193   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
194   (prog_vars ?? p).
195
196(* Return the global environment for the given program. *)
197definition globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)) ≝
198λF,V,i,p.
199  \fst (globalenv_allocmem F V i p).
200
201(* Return the global environment for the given program with no data initialisation. *)
202definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
203λF,p.
204  globalenv F nat (λn.[Init_space n]) p.
205
206(* Return the initial memory state for the given program. *)
207definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝
208λF,V,i,p.
209  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
210  init_globals ? V i g m (prog_vars ?? p).
211
212(* Setup memory when data initialisation is not required (has the benefit
213   of being total. *)
214definition alloc_mem: ∀F. program F nat → mem ≝
215λF,p.
216  \snd (globalenv_allocmem F nat (λn. [Init_space n]) p).
217
218(* Return the function description associated with the given address, if any. *)
219definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝
220λF,ge,b. match block_region b with [ Code ⇒
221           match block_id b with [ neg p ⇒ lookup_opt … p (functions … ge)
222         | _ ⇒ None ? ] | _ ⇒ None ? ].
223
224(* Same as [find_funct_ptr] but the function address is given as
225   a value, which must be a pointer with offset 0. *)
226definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝
227λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then find_funct_ptr … ge (pblock ptr) else None ? | _ ⇒ None ? ].
228
229
230(* Turn a memory block into the original symbol. *)
231definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝
232λF,genv,b.
233  option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')).
234
235
236lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
237  find_funct F ge v = Some F f →
238  ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
239#F #ge *
240[ #f #E normalize in E; destruct
241| #sz #i #f #E normalize in E; destruct
242| #f #fn #E normalize in E; destruct
243| (*#r*) #f #E normalize in E; destruct
244| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
245  @eq_offset_elim #Eoff
246  #E whd in E:(??%?); destruct
247  (*%{pty}*) %{b} (*%{c}*) % // @E
248] qed.
249
250
251lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m.
252  find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b.
253#F #V #init * * // * // #blk
254whd in ⊢ (? → ? → ? → ??%%);
255#vars elim vars
256[ #ge #m %
257| * * #id #r #v #tl #IH #ge #m
258  whd in match (add_globals ?????);
259  whd in ⊢ (??(???(??(???(????%?))))?);
260  cases (alloc ????) #m' #b
261  whd in ⊢ (??(???(??(???(????%?))))?);
262  >IH cases ge #fnmap #nextblock #symmap
263  whd in ⊢ (??(???%)?);
264  %
265] qed.
266
267lemma add_globals_match : ∀A,B,V,W,initV,initW.
268  ∀P:(ident × region × V) → (ident × region × W) → Prop.
269  (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
270  ∀vars,ge,ge',m,vars'.
271  symbols ? ge = symbols … ge' →
272  All2 … P vars vars' →
273  symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧ 
274  \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars').
275#A #B #V #W #initV #initW #P #varsOK
276#vars elim vars
277[ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ]
278| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
279  * * #id' #r' #w #tl' #E * #p #TL
280  whd in match (add_globals A ????);
281  change with (add_globals A ????) in match (foldl ?????);
282  whd in match (add_globals B ????);
283  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
284  cases (varsOK … p) #E1 #E2
285  destruct >E2 cases (alloc ????) #m' #b
286  @IH /2/
287  whd in match (add_symbol ????);
288  whd in match (add_symbol ????);
289  >E %
290] qed.
291
292lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
293  (∀f,g. P f g → \fst f = \fst g) →
294  ∀fns,fns'.
295  All2 … P fns fns' →
296  let ge ≝ add_functs A (empty ?) fns in
297  let ge' ≝ add_functs B (empty ?) fns' in
298  nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'.
299#A #B #P #fnOK #fns elim fns
300[ * [ #_ % % | #h #t * ]
301| * #id #f #tl #IH * [ * ]
302  * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H
303  whd in match (add_functs ???);
304  change with (add_functs ???) in match (foldr ?????);
305  whd in match (add_functs B ??);
306  change with (add_functs ???) in match (foldr (ident × B) ????);
307  cases (IH tl' H) #E1 #E2
308  % [ >E1 % | >E1 >E2 % ]
309] qed.
310
311lemma matching_fns_get_same_blocks :  ∀A,B,P.
312  (∀f,g. P f g → \fst f = \fst g) →
313  ∀fns,fns'.
314  All2 … P fns fns' →
315  let ge ≝ add_functs A (empty ?) fns in
316  let ge' ≝ add_functs B (empty ?) fns' in
317  symbols … ge = symbols … ge'.
318#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
319qed.
320
321lemma symbol_of_block_rev : ∀F,genv,b,id.
322  symbol_for_block F genv b = Some ? id →
323  find_symbol F genv id = Some ? b.
324#F #genv #b #id #H whd in H:(??%?);
325@(find_lookup … (λid,b'. eq_block b b'))
326lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b'))
327cases (find ????) in H ⊢ %;
328[ normalize #E destruct
329| * #id' #b' normalize in ⊢ (% → ?); #E destruct
330  #H lapply (H … (refl ??))
331  @eq_block_elim
332  [ #E destruct //
333  | #_ *
334  ]
335] qed.
336
337(*
338(* * ** Properties of the operations. *)
339
340  find_funct_inv:
341    ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F.
342    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
343  find_funct_find_funct_ptr:
344    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
345    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
346
347  find_symbol_exists:
348    ∀F,V: Type[0]. ∀p: program F V.
349           ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
350    in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
351    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
352  find_funct_ptr_exists:
353    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
354    list_norepet ? (prog_funct_names ?? p) →
355    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
356    in_list ? 〈id, f〉 (prog_funct ?? p) →
357    ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
358           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;
359
360  find_funct_ptr_inversion:
361    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
362    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
363    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
364  find_funct_inversion:
365    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
366    find_funct ? (globalenv ?? p) v = Some ? f →
367    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
368  find_funct_ptr_symbol_inversion:
369    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
370    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 →
371    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
372    in_list ? 〈id, f〉 (prog_funct ?? p);
373
374  find_funct_ptr_prop:
375    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
376    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
377    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
378    P f;
379  find_funct_prop:
380    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
381    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
382    find_funct ? (globalenv ?? p) v = Some ? f →
383    P f;
384
385  initmem_nullptr:
386    ∀F,V: Type[0]. ∀p: program F V.
387    let m ≝ init_mem ?? p in
388    valid_block m nullptr ∧
389    (blocks m) nullptr = empty_block 0 0 Any;
390(*  initmem_inject_neutral:
391    ∀F,V: Type[0]. ∀p: program F V.
392    mem_inject_neutral (init_mem ?? p);*)
393  find_funct_ptr_negative:
394    ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F.
395    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
396  find_symbol_not_fresh:
397    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
398    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
399  find_symbol_not_nullptr:
400    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
401    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
402  global_addresses_distinct:
403    ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2.
404    id1≠id2 →
405    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
406    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
407    b1≠b2;
408
409(* * Commutation properties between program transformations
410  and operations over global environments. *)
411
412  find_funct_ptr_rev_transf:
413    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
414    ∀b : block. ∀tf : B.
415    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
416    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
417  find_funct_rev_transf:
418    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
419    ∀v : val. ∀tf : B.
420    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
421    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
422
423(* * Commutation properties between partial program transformations
424  and operations over global environments. *)
425
426  find_funct_ptr_transf_partial:
427    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
428    transform_partial_program … transf p = OK ? p' →
429    ∀b: block. ∀f: A.
430    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
431    ∃f'.
432    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
433  find_funct_transf_partial:
434    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
435    transform_partial_program … transf p = OK ? p' →
436    ∀v: val. ∀f: A.
437    find_funct ? (globalenv ?? p) v = Some ? f →
438    ∃f'.
439    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
440  find_symbol_transf_partial:
441    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
442    transform_partial_program … transf p = OK ? p' →
443    ∀s: ident.
444    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
445  init_mem_transf_partial:
446    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
447    transform_partial_program … transf p = OK ? p' →
448    init_mem ?? p' = init_mem ?? p;
449  find_funct_ptr_rev_transf_partial:
450    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
451    transform_partial_program … transf p = OK ? p' →
452    ∀b : block. ∀tf : B.
453    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
454    ∃f : A.
455      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
456  find_funct_rev_transf_partial:
457    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
458    transform_partial_program … transf p = OK ? p' →
459    ∀v : val. ∀tf : B.
460    find_funct ? (globalenv ?? p') v = Some ? tf →
461    ∃f : A.
462      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*;
463
464  find_funct_ptr_transf_partial2:
465    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
466           ∀p: program A V. ∀p': program B W.
467    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
468    ∀b: block. ∀f: A.
469    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
470    ∃f'.
471    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
472  find_funct_transf_partial2:
473    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
474           ∀p: program A V. ∀p': program B W.
475    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
476    ∀v: val. ∀f: A.
477    find_funct ? (globalenv ?? p) v = Some ? f →
478    ∃f'.
479    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
480  find_symbol_transf_partial2:
481    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
482           ∀p: program A V. ∀p': program B W.
483    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
484    ∀s: ident.
485    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
486  init_mem_transf_partial2:
487    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
488           ∀p: program A V. ∀p': program B W.
489    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
490    init_mem ?? p' = init_mem ?? p;
491  find_funct_ptr_rev_transf_partial2:
492    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
493           ∀p: program A V. ∀p': program B W.
494    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
495    ∀b: block. ∀tf: B.
496    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
497    ∃f : A.
498      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
499  find_funct_rev_transf_partial2:
500    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
501           ∀p: program A V. ∀p': program B W.
502    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
503    ∀v: val. ∀tf: B.
504    find_funct ? (globalenv ?? p') v = Some ? tf →
505    ∃f : A.
506      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ;
507
508(* * Commutation properties between matching between programs
509  and operations over global environments. *)
510*) *)
511
512(* First, show that nextfunction only depends on the number of functions: *)
513
514let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
515match n with
516[ O ⇒ p
517| S m ⇒ succ (nat_plus_pos m p)
518].
519
520lemma nextfunction_length : ∀A,l,ge.
521  nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge).
522#A #l elim l // #h #t #IH #ge
523whd in ⊢ (??%%); >IH //
524qed.
525
526(* Now link functions in related programs, but without dealing with the type
527   casts yet. *)
528
529lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
530  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
531  All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
532  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
533#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
534cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
535[ 4: (*12:*) | *: #F whd in F:(??%?); destruct ]
536>vars_irrelevant_to_find_funct_ptr
537>vars_irrelevant_to_find_funct_ptr
538letin varnames ≝ (map ??? vars)
539cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
540//
541cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
542//
543generalize in match (empty ?);
544generalize in match (empty ?);
545generalize in match fns';
546elim fns
547[ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct
548| * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?);
549  whd in match (functions ??);
550  change with (add_functs ???) in match (foldr ?????);
551  cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl)))
552  [ #E destruct  >lookup_opt_insert_hit #E destruct
553    cases fns' [ * ]
554    * #id' #fn' #tl' * #M #Mtl
555    %{fn'} % // whd in ⊢ (??%?);
556    whd in match (functions ??);
557    change with (add_functs ???) in match (foldr ???? tl');
558    >nextfunction_length >nextfunction_length <NF >(All2_length  … Mtl)
559    >lookup_opt_insert_hit @refl
560  | #NE >lookup_opt_insert_miss //
561    #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl
562    cases (IH ?????? Mtl)
563    [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ]
564    | skip
565    | 4: @NF
566    | skip
567    | //
568    | @FFP
569    ]
570  ]
571] qed.
572
573(* lazy proof *)
574lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P.
575  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
576  All ? (λx. P (\snd x)) (prog_funct ?? p) →
577  P f.
578#A #V #b #p #f #initV #P #FFP #ALL
579cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p))
580[ elim (prog_funct … p) in ALL ⊢ %;
581  [ // | #h #t #IH * #Hh #Ht % /2/ ] ]
582#ALL2
583cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2)
584#x * //
585qed.
586
587
588discriminator Prod.
589
590(* Now prove the full version. *)
591
592lemma find_funct_ptr_match:
593    ∀M:matching.∀initV,initW.
594    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
595    ∀MATCH:match_program … M p p'.
596    ∀b: block. ∀f: m_A M (prog_var_names … p).
597    find_funct_ptr … (globalenv … initV p) b = Some ? f →
598    ∃tf : m_B M (prog_var_names … p').
599    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
600[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
601* #A #B #V #W #match_fn #match_var #initV #initW
602#p #p' * #Mvars #Mfn #Mmain
603#b #f #FFP
604@(find_funct_ptr_All2 A B V W ??????? FFP)
605lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
606#E
607@(All2_mp … Mfn)
608* #id #f * #id' #f'
609<E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
610normalize #H @(match_funct_entry_inv … H) //
611qed.
612
613lemma
614  find_funct_ptr_transf_partial2:
615    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
616           ∀p: program A V. ∀p': program B W.
617    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
618    ∀b: block. ∀f: A ?.
619    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
620    ∃f'.
621    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
622#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
623cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
624[2: @iW
625| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
626#TF %{f'} % //
627-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
628qed.
629
630lemma match_funct_entry_id : ∀M,vs,vs',f,g.
631  match_funct_entry M vs vs' f g → \fst f = \fst g.
632#M #vs #vs' #f #g * //
633qed.
634
635lemma
636  find_symbol_match:
637    ∀M:matching.
638    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
639    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
640    match_program … M p p' →
641    ∀s: ident.
642    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
643* #A #B #V #W #match_fun #match_var #initV #initW #initsize
644* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
645whd in ⊢ (??%%);
646@sym_eq
647@(eq_f ??(λx. lookup SymbolTag block x s))
648whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
649whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
650change with (add_globals ?????) in match (foldl ?????);
651change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
652@(proj1 … (add_globals_match … Mvars))
653[ @(matching_fns_get_same_blocks … Mfns)
654  #f #g @match_funct_entry_id
655| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
656] qed.
657 
658lemma
659  find_symbol_transf_partial2:
660    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
661    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
662           ∀p: program A V. ∀p': program B W.
663    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
664    ∀s: ident.
665    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
666#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
667@(find_symbol_match … (transform_partial_program2_match … TPP2))
668#v0 #w0 * #id #r #v #w @sizeOK
669qed.
670
671lemma
672  find_funct_ptr_transf:
673    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
674    ∀b: block. ∀f: A ?.
675    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
676    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
677#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
678cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
679[ 2: @iV
680| #f' * #FFP'
681  whd in ⊢ (???(match % with [_⇒?]) → ?);  (* XXX this line only required to workaround unification bug *)
682  generalize in match (matching_vars ????);
683  whd in match (prog_var_names ???); whd in match (prog_vars ???);
684  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
685] qed.
686
687lemma
688  find_funct_transf:
689    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
690    ∀v: val. ∀f: A ?.
691    find_funct ? (globalenv … iV p) v = Some ? f →
692    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
693#A #B #V #iV #tf #p #v #f #FF
694cases (find_funct_find_funct_ptr ???? FF)
695#b * #E destruct #FFP
696change with (find_funct_ptr ???) in ⊢ (??%?);
697@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
698qed.
699
700lemma
701  find_symbol_transf:
702    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
703    ∀s: ident.
704    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
705    find_symbol ? (globalenv … iV p) s.
706#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
707#v0 #w0 * //
708qed.
709
710lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d.
711  symbols A ge = symbols … ge' →
712  store_init_data A ge m b o d = store_init_data B ge' m b o d.
713#A #B #ge #ge' #m #b #o #d #SYM
714whd in ⊢ (??%%);
715cases d try #d' try @refl
716#n whd in ⊢ (??%%);
717whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
718qed.
719
720lemma store_init_data_list_symbols : ∀A,B,ge,ge',b.
721  symbols A ge = symbols … ge' →
722  ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d.
723#A #B #ge #ge' #b #SYM #d elim d
724[ //
725| #hd #tl #IH #m #o
726  whd in ⊢ (??%%);
727  >(store_init_data_symbols … SYM)
728  cases (store_init_data ??????)
729  [ %
730  | #m' @IH
731  ]
732] qed.
733
734lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop.
735  ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) →
736  ∀ge:genv_t A. ∀ge':genv_t B.
737  symbols … ge = symbols … ge' →
738   ∀m. ∀vars,vars'.
739  All2 … P vars vars' →
740  init_globals A V iV ge m vars = init_globals B W iW ge' m vars'.
741#A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars
742whd in ⊢ (? → ? → ??%%);
743generalize in match (OK ? m);
744elim vars
745[ #rm *
746  [ #_ %
747  | #h #t *
748  ]
749| * #idr #v #tl #IH #rm
750  * [ * ]
751  * #idr' #w #tl'
752  * #p cases (varsOK … p) #E1 #E2 destruct #TL
753  whd in ⊢ (??%%); cases idr' #id #r cases rm #m'
754  whd in ⊢ (??(????%?)(????%?));
755  [ whd in match (find_symbol ?? id);
756    whd in match (find_symbol B ? id);
757    >SYM cases (lookup ??? id)
758    [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ]
759  ] @IH //
760] qed.
761
762lemma
763  init_mem_match:
764    ∀M:matching.
765    ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) →
766    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
767    match_program … M p p' →
768    init_mem … iW p' = init_mem … iV p.
769* #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain
770whd in ⊢ (??%%);
771change with (add_globals ?????) in match (globalenv_allocmem ??? p');
772change with (add_globals ?????) in match (globalenv_allocmem ??? p);
773cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars)
774[ 8: @(matching_fns_get_same_blocks … Mfns)
775     #f0 #g0 * //
776| cases (add_globals ?????) #ge1 #m1
777  cases (add_globals ?????) #ge2 #m2
778  #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars)
779  [ #v0 #w0 * #id #r #v #w /3/
780  | @SYM
781  ]
782| 4: #v0 #w0 * #id #r #v #w #V % // >iSAME //
783| *: skip
784] qed.
785
786lemma
787  init_mem_transf:
788    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
789    init_mem … iV (transform_program … p transf) = init_mem … iV p.
790#A #B #C #iV #transf #p
791@(init_mem_match … (transform_program_match … transf ?))
792//
793qed.
794
795lemma
796  init_mem_transf_gen:
797    ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V.
798    init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p.
799#tag #A #B #C #iV #g #transf #p
800@(init_mem_match … (transform_program_gen_match … transf ?))
801//
802qed.
803   
804
805(* Package up transform_program results for global envs nicely. *)
806
807record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
808  rg_find_symbol: ∀s.
809    find_symbol … ge s = find_symbol … ge' s;
810  rg_find_funct: ∀v,f.
811    find_funct … ge v = Some ? f →
812    find_funct … ge' v = Some ? (t f);
813  rg_find_funct_ptr: ∀b,f.
814    find_funct_ptr … ge b = Some ? f →
815    find_funct_ptr … ge' b = Some ? (t f)
816}.
817
818theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
819  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
820#A #B #V #iV #p #tf %
821[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
822| @(find_funct_transf A B V iV tf p)
823| @(find_funct_ptr_transf A B V iV p tf)
824] qed.
825
826record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
827  rgg_find_symbol: ∀s.
828    find_symbol … ge s = find_symbol … ge' s;
829  rgg_find_funct_ptr: ∀b,f.
830    find_funct_ptr … ge b = Some ? f →
831    ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f));
832  rgg_find_funct: ∀v,f.
833    find_funct … ge v = Some ? f →
834    ∃g. find_funct … ge' v = Some ? (\fst (t g f))
835}.
836
837include "utilities/bool.ma".
838
839theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
840  related_globals_gen tag (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (\fst (transform_program_gen tag A B V g p tf))).
841#tag #A #B #V #iV #g #p #tf %
842[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
843  #v #w * //
844| #b #f #FFP
845  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
846  [ 2: @iV
847  | #fn' * #FFP'
848    generalize in match (matching_vars ????);
849    whd in match (prog_var_names ???); whd in match (prog_vars ???);
850    #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' %
851  | skip
852  ]
853| * [5: #ptr #fn whd in match (find_funct ???);
854     @if_elim #Eoff #FFP
855     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
856       [ 2: @iV
857       | #fn' * #FFP'
858         generalize in match (matching_vars ????);
859         whd in match (prog_var_names ???); whd in match (prog_vars ???);
860         #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E'
861         %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' %
862       ]
863     | destruct
864     ]
865    | *: normalize #A #B try #C try #D destruct
866    ]
867] qed.
868
869
870(*
871
872  find_funct_ptr_match:
873    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
874           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
875    match_program … match_fun match_var p p' →
876    ∀b: block. ∀f: A.
877    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
878    ∃tf : B.
879    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
880  find_funct_ptr_rev_match:
881    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
882           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
883    match_program … match_fun match_var p p' →
884    ∀b: block. ∀tf: B.
885    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
886    ∃f : A.
887    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
888  find_funct_match:
889    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
890           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
891    match_program … match_fun match_var p p' →
892    ∀v: val. ∀f: A.
893    find_funct ? (globalenv ?? p) v = Some ? f →
894    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
895  find_funct_rev_match:
896    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
897           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
898    match_program … match_fun match_var p p' →
899    ∀v: val. ∀tf: B.
900    find_funct ? (globalenv ?? p') v = Some ? tf →
901    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
902  find_symbol_match:
903    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
904           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
905    match_program … match_fun match_var p p' →
906    ∀s: ident.
907    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
908*)
909(*
910Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
911  ZMap.get b g.(functions).
912
913Definition find_funct (g: genv) (v: val) : option F :=
914  match v with
915  | Vptr b ofs =>
916      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
917  | _ =>
918      None
919  end.
920
921Definition find_symbol ? (g: genv) (symb: ident) : option block :=
922  PTree.get symb g.(symbols).
923
924Lemma find_funct_inv:
925  forall (ge: t) (v: val) (f: F),
926  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
927Proof.
928  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
929  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
930  exists b. congruence.
931  discriminate.
932Qed.
933
934Lemma find_funct_find_funct_ptr:
935  forall (ge: t) (b: block),
936  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
937Proof.
938  intros. simpl.
939  generalize (Int.eq_spec Int.zero Int.zero).
940  case (Int.eq Int.zero Int.zero); intros.
941  auto. tauto.
942Qed.
943*)
944
945(*
946##[ #A B C transf p b f; elim p; #fns main vars;
947    elim fns;
948    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
949    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
950        nrewrite > (?:nextfunction ?? = length ? t);
951        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
952            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
953        ##| nrewrite > (?:nextfunction ?? = length ? t);
954          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
955              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
956          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
957            ##[ #H; destruct (H); //;
958            ##| #H; napply IH; napply H;
959            ##]
960          ##]
961        ##]
962    ##]
963##| #A B C transf p v f; elim v;
964    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
965    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
966    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
967        whd in ⊢ (??%? → ??%?);
968        ##[ elim p; #fns main vars; elim fns;
969          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
970          ##| #h t; elim h; #f fn IH;
971              whd in ⊢ (??%? → ??%?);
972              nrewrite > (?:nextfunction ?? = length ? t);
973              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
974                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
975              ##| nrewrite > (?:nextfunction ?? = length ? t);
976                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
977                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
978                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
979                  ##[ destruct (H); //;
980                  ##| napply IH; napply H;
981                  ##]
982                ##]
983              ##]
984          ##]
985       ##| #H; destruct;
986       ##]
987    ##]
988##| #A B C transf p id; elim p; #fns main vars;
989    elim fns;
990    ##[ normalize; //
991    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
992        elim (ident_eq fid id); #e;
993        ##[ whd in ⊢ (??%%);
994          nrewrite > (?:nextfunction ?? = length ? t);
995          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
996              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
997          ##| nrewrite > (?:nextfunction ?? = length ? t);
998            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
999                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1000            ##| //
1001            ##]
1002          ##]
1003        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
1004        ##]
1005    ##]
1006##| //;
1007##| #A B C transf p b tf; elim p; #fns main vars;
1008    elim fns;
1009    ##[ normalize; #H; destruct;
1010    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1011        nrewrite > (?:nextfunction ?? = length ? t);
1012        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1013            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1014        ##| nrewrite > (?:nextfunction ?? = length ? t);
1015          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
1016              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1017          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1018            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
1019            ##| #H; napply IH; napply H;
1020            ##]
1021          ##]
1022        ##]
1023    ##]
1024##| #A B C transf p v tf; elim p; #fns main vars; elim v;
1025  ##[ normalize; #H; destruct;
1026  ##| ##2,3: #x; normalize; #H; destruct;
1027  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
1028    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1029      elim fns;
1030      ##[ normalize; #H; destruct;
1031      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1032          nrewrite > (?:nextfunction ?? = length ? t);
1033          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
1034              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
1035          ##| nrewrite > (?:nextfunction ?? = length ? t);
1036            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
1037                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
1038            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
1039              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
1040              ##| #H; napply IH; napply H;
1041              ##]
1042            ##]
1043          ##]
1044      ##]
1045    ##| normalize; #H; destruct;
1046    ##]
1047 ##]
1048##] qed.
1049         
1050
1051Lemma functions_globalenv:
1052  forall (p: program F V),
1053  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
1054Proof.
1055  assert (forall init vars,
1056     functions (fst (add_globals init vars)) = functions (fst init)).
1057  induction vars; simpl.
1058  reflexivity.
1059  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
1060  simpl. exact IHvars.
1061
1062  unfold add_globals; simpl.
1063  intros. unfold globalenv; unfold globalenv_initmem.
1064  rewrite H. reflexivity.
1065Qed.
1066
1067Lemma initmem_nullptr:
1068  forall (p: program F V),
1069  let m := init_mem p in
1070  valid_block m nullptr /\
1071  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
1072Proof.
1073  pose (P := fun m => valid_block m nullptr /\
1074        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
1075  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
1076  induction vars; simpl; intros.
1077  auto.
1078  destruct a as [[id1 in1] inf1].
1079  destruct (add_globals init vars) as [g st].
1080  simpl in *. destruct IHvars. split.
1081  red; simpl. red in H0. omega.
1082  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
1083
1084  intro. unfold init_mem, globalenv_initmem. apply H.
1085  red; simpl. split. compute. auto. reflexivity.
1086Qed.
1087
1088Lemma initmem_inject_neutral:
1089  forall (p: program F V),
1090  mem_inject_neutral (init_mem p).
1091Proof.
1092  assert (forall g0 vars g1 m,
1093      add_globals (g0, Mem.empty) vars = (g1, m) →
1094      mem_inject_neutral m).
1095  Opaque alloc_init_data.
1096  induction vars; simpl.
1097  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
1098  simpl in H1. rewrite Mem.getN_init in H1.
1099  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
1100  destruct a as [[id1 init1] info1].
1101  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
1102  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
1103  intros. inv H.
1104  eapply Mem.alloc_init_data_neutral; eauto.
1105  intros. caseEq (globalenv_initmem p). intros g m EQ.
1106  unfold init_mem; rewrite EQ; simpl.
1107  unfold globalenv_initmem in EQ. eauto.
1108Qed.     
1109
1110Remark nextfunction_add_functs_neg:
1111  forall fns, nextfunction (add_functs empty fns) < 0.
1112Proof.
1113  induction fns; simpl; intros. omega. unfold Zpred. omega.
1114Qed.
1115
1116Theorem find_funct_ptr_negative:
1117  forall (p: program F V) (b: block) (f: F),
1118  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
1119Proof.
1120  intros until f.
1121  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
1122    induction fns; simpl.
1123    rewrite ZMap.gi. congruence.
1124    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
1125    intro. rewrite e. apply nextfunction_add_functs_neg.
1126    auto.
1127  unfold find_funct_ptr. rewrite functions_globalenv.
1128  intros. eauto.
1129Qed.
1130
1131Remark find_symbol_add_functs_negative:
1132  forall (fns: list (ident * F)) s b,
1133  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
1134Proof.
1135  induction fns; simpl; intros until b.
1136  rewrite PTree.gempty. congruence.
1137  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
1138  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
1139  eauto.
1140Qed.
1141
1142Remark find_symbol_add_symbols_not_fresh:
1143  forall fns vars g m s b,
1144  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
1145  (symbols g)!s = Some ? b →
1146  b < nextblock m.
1147Proof.
1148  induction vars; simpl; intros until b.
1149  intros. inversion H. subst g m. simpl.
1150  generalize (find_symbol_add_functs_negative fns s H0). omega.
1151  Transparent alloc_init_data.
1152  destruct a as [[id1 init1] info1].
1153  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
1154  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
1155  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
1156  intro EQ; inversion EQ. omega.
1157  intro. generalize (IHvars _ _ _ _ ADG H). omega.
1158Qed.
1159
1160Theorem find_symbol_not_fresh:
1161  forall (p: program F V) (id: ident) (b: block),
1162  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
1163Proof.
1164  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
1165  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
1166                      (prog_vars p)); intros g m EQ.
1167  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
1168Qed.
1169
1170Lemma find_symbol_exists:
1171  forall (p: program F V)
1172         (id: ident) (init: list init_data) (v: V),
1173  In (id, init, v) (prog_vars p) →
1174  ∃b. find_symbol ? (globalenv p) id = Some ? b.
1175Proof.
1176  intros until v.
1177  assert (forall initm vl, In (id, init, v) vl →
1178           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
1179  induction vl; simpl; intros.
1180  elim H.
1181  destruct a as [[id0 init0] v0].
1182  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
1183  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
1184  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
1185  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
1186Qed.
1187
1188Remark find_symbol_above_nextfunction:
1189  forall (id: ident) (b: block) (fns: list (ident * F)),
1190  let g := add_functs empty fns in
1191  PTree.get id g.(symbols) = Some ? b →
1192  b > g.(nextfunction).
1193Proof.
1194  induction fns; simpl.
1195  rewrite PTree.gempty. congruence.
1196  rewrite PTree.gsspec. case (peq id (fst a)); intro.
1197  intro EQ. inversion EQ. unfold Zpred. omega.
1198  intros. generalize (IHfns H). unfold Zpred; omega.
1199Qed.
1200
1201Remark find_symbol_add_globals:
1202  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
1203  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
1204  find_symbol ? (fst (add_globals ge_m vars)) id =
1205  find_symbol ? (fst ge_m) id.
1206Proof.
1207  unfold find_symbol; induction vars; simpl; intros.
1208  auto.
1209  destruct a as [[id0 init0] var0]. simpl in *.
1210  caseEq (add_globals ge_m vars); intros ge' m' EQ.
1211  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
1212  apply IHvars. tauto. intuition congruence.
1213Qed.
1214
1215Lemma find_funct_ptr_exists:
1216  forall (p: program F V) (id: ident) (f: F),
1217  list_norepet (prog_funct_names p) →
1218  list_disjoint (prog_funct_names p) (prog_var_names p) →
1219  In (id, f) (prog_funct p) →
1220  ∃b. find_symbol ? (globalenv p) id = Some ? b
1221         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
1222Proof.
1223  intros until f.
1224  assert (forall (fns: list (ident * F)),
1225           list_norepet (map (@fst ident F) fns) →
1226           In (id, f) fns →
1227           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
1228                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
1229  unfold find_symbol, find_funct_ptr. induction fns; intros.
1230  elim H0.
1231  destruct a as [id0 f0]; simpl in *. inv H.
1232  unfold add_funct; simpl.
1233  rewrite PTree.gsspec. destruct (peq id id0).
1234  subst id0. econstructor; split. eauto.
1235  replace f0 with f. apply ZMap.gss.
1236  elim H0; intro. congruence. elim H3.
1237  change id with (@fst ident F (id, f)). apply List.in_map. auto.
1238  exploit IHfns; eauto. elim H0; intro. congruence. auto.
1239  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
1240  generalize (find_symbol_above_nextfunction _ _ X).
1241  unfold block; unfold ZIndexed.t; intro; omega.
1242
1243  intros. exploit H; eauto. intros [b [X Y]].
1244  exists b; split.
1245  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
1246  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
1247  unfold prog_funct_names. change id with (fst (id, f)).
1248  apply List.in_map; auto.
1249  unfold find_funct_ptr. rewrite functions_globalenv.
1250  assumption.
1251Qed.
1252
1253Lemma find_funct_ptr_inversion:
1254  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1255  find_funct_ptr ? (globalenv p) b = Some ? f →
1256  ∃id. In (id, f) (prog_funct p).
1257Proof.
1258  intros until f.
1259  assert (forall fns: list (ident * F),
1260    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
1261    ∃id. In (id, f) fns).
1262  unfold find_funct_ptr. induction fns; simpl.
1263  rewrite ZMap.gi. congruence.
1264  destruct a as [id0 f0]; simpl.
1265  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
1266  intro. inv H. exists id0; auto.
1267  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
1268  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
1269Qed.
1270
1271Lemma find_funct_ptr_prop:
1272  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1273  (forall id f, In (id, f) (prog_funct p) → P f) →
1274  find_funct_ptr ? (globalenv p) b = Some ? f →
1275  P f.
1276Proof.
1277  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
1278Qed.
1279
1280Lemma find_funct_inversion:
1281  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1282  find_funct (globalenv p) v = Some ? f →
1283  ∃id. In (id, f) (prog_funct p).
1284Proof.
1285  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
1286  rewrite find_funct_find_funct_ptr ? in H.
1287  eapply find_funct_ptr_inversion; eauto.
1288Qed.
1289
1290Lemma find_funct_prop:
1291  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1292  (forall id f, In (id, f) (prog_funct p) → P f) →
1293  find_funct (globalenv p) v = Some ? f →
1294  P f.
1295Proof.
1296  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
1297Qed.
1298
1299Lemma find_funct_ptr_symbol_inversion:
1300  forall (p: program F V) (id: ident) (b: block) (f: F),
1301  find_symbol ? (globalenv p) id = Some ? b →
1302  find_funct_ptr ? (globalenv p) b = Some ? f →
1303  In (id, f) p.(prog_funct).
1304Proof.
1305  intros until f.
1306  assert (forall fns,
1307           let g := add_functs empty fns in
1308           PTree.get id g.(symbols) = Some ? b →
1309           ZMap.get b g.(functions) = Some ? f →
1310           In (id, f) fns).
1311    induction fns; simpl.
1312    rewrite ZMap.gi. congruence.
1313    set (g := add_functs empty fns).
1314    rewrite PTree.gsspec. rewrite ZMap.gsspec.
1315    case (peq id (fst a)); intro.
1316    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
1317    intro EQ2. left. destruct a. simpl in *. congruence.
1318    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
1319    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
1320  assert (forall g0 m0, b < 0 →
1321          forall vars g m,
1322          add_globals (g0, m0) vars = (g, m) →
1323          PTree.get id g.(symbols) = Some ? b →
1324          PTree.get id g0.(symbols) = Some ? b).
1325    induction vars; simpl.
1326    intros. inv H1. auto.
1327    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
1328    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
1329    unfold add_symbol; intros A B. rewrite <- B. simpl.
1330    rewrite PTree.gsspec. case (peq id id1); intros.
1331    assert (b > 0). inv H1. apply nextblock_pos.
1332    omegaContradiction.
1333    eauto.
1334  intros.
1335  generalize (find_funct_ptr_negative _ _ H2). intro.
1336  pose (g := add_functs empty (prog_funct p)).
1337  apply H. 
1338  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
1339  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
1340  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
1341Qed.
1342
1343Theorem find_symbol_not_nullptr:
1344  forall (p: program F V) (id: ident) (b: block),
1345  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
1346Proof.
1347  intros until b.
1348  assert (forall fns,
1349          find_symbol ? (add_functs empty fns) id = Some ? b →
1350          b <> nullptr).
1351    unfold find_symbol; induction fns; simpl.
1352    rewrite PTree.gempty. congruence.
1353    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
1354    destruct (peq id id1); intros.
1355    inversion H. generalize (nextfunction_add_functs_neg fns).
1356    unfold block, nullptr; omega.
1357    auto.
1358  set (g0 := add_functs empty p.(prog_funct)).
1359  assert (forall vars g m,
1360          add_globals (g0, Mem.empty) vars = (g, m) →
1361          find_symbol ? g id = Some ? b →
1362          b <> nullptr).
1363    induction vars; simpl; intros until m.
1364    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
1365    destruct a as [[id1 init1] info1].
1366    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
1367    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
1368    destruct (peq id id1); intros.
1369    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
1370    eauto.
1371  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
1372Qed.
1373
1374Theorem global_addresses_distinct:
1375  forall (p: program F V) id1 id2 b1 b2,
1376  id1<>id2 →
1377  find_symbol ? (globalenv p) id1 = Some ? b1 →
1378  find_symbol ? (globalenv p) id2 = Some ? b2 →
1379  b1<>b2.
1380Proof.
1381  intros.
1382  assert (forall fns,
1383    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
1384    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
1385    b1 <> b2).
1386  unfold find_symbol. induction fns; simpl; intros.
1387  rewrite PTree.gempty in H2. discriminate.
1388  destruct a as [id f]; simpl in *.
1389  rewrite PTree.gsspec in H2.
1390  destruct (peq id1 id). subst id. inv H2.
1391  rewrite PTree.gso in H3; auto.
1392  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
1393  rewrite PTree.gsspec in H3.
1394  destruct (peq id2 id). subst id. inv H3.
1395  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
1396  eauto.
1397  set (ge0 := add_functs empty p.(prog_funct)).
1398  assert (forall (vars: list (ident * list init_data * V)) ge m,
1399    add_globals (ge0, Mem.empty) vars = (ge, m) →
1400    find_symbol ? ge id1 = Some ? b1 →
1401    find_symbol ? ge id2 = Some ? b2 →
1402    b1 <> b2).
1403  unfold find_symbol. induction vars; simpl.
1404  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
1405  intros ge m. destruct a as [[id init] info].
1406  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
1407  unfold add_symbol. simpl. intros.
1408  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
1409  rewrite PTree.gso in H4; auto.
1410  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
1411  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
1412  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
1413  eauto.
1414  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
1415  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
1416  fold ge_m. apply surjective_pairing. auto. auto.
1417Qed.
1418
1419End GENV.
1420
1421(* Global environments and program transformations. *)
1422
1423Section MATCH_PROGRAM.
1424
1425Variable A B V W: Type.
1426Variable match_fun: A → B → Prop.
1427Variable match_var: V → W → Prop.
1428Variable p: program A V.
1429Variable p': program B W.
1430Hypothesis match_prog:
1431  match_program match_fun match_var p p'.
1432
1433Lemma add_functs_match:
1434  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1435  list_forall2 (match_funct_etry match_fun) fns tfns →
1436  let r := add_functs (empty A) fns in
1437  let tr := add_functs (empty B) tfns in
1438  nextfunction tr = nextfunction r /\
1439  symbols tr = symbols r /\
1440  forall (b: block) (f: A),
1441  ZMap.get b (functions r) = Some ? f →
1442  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
1443Proof.
1444  induction 1; simpl.
1445
1446  split. reflexivity. split. reflexivity.
1447  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1448
1449  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1450  simpl. red in H. destruct H.
1451  destruct IHlist_forall2 as [X [Y Z]].
1452  rewrite X. rewrite Y. 
1453  split. auto.
1454  split. congruence.
1455  intros b f.
1456  repeat (rewrite ZMap.gsspec).
1457  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1458  intro EQ; inv EQ. exists fn2; auto.
1459  auto.
1460Qed.
1461
1462Lemma add_functs_rev_match:
1463  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1464  list_forall2 (match_funct_etry match_fun) fns tfns →
1465  let r := add_functs (empty A) fns in
1466  let tr := add_functs (empty B) tfns in
1467  nextfunction tr = nextfunction r /\
1468  symbols tr = symbols r /\
1469  forall (b: block) (tf: B),
1470  ZMap.get b (functions tr) = Some ? tf →
1471  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
1472Proof.
1473  induction 1; simpl.
1474
1475  split. reflexivity. split. reflexivity.
1476  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1477
1478  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1479  simpl. red in H. destruct H.
1480  destruct IHlist_forall2 as [X [Y Z]].
1481  rewrite X. rewrite Y. 
1482  split. auto.
1483  split. congruence.
1484  intros b f.
1485  repeat (rewrite ZMap.gsspec).
1486  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1487  intro EQ; inv EQ. exists fn1; auto.
1488  auto.
1489Qed.
1490
1491Lemma mem_add_globals_match:
1492  forall (g1: genv A) (g2: genv B) (m: mem)
1493         (vars: list (ident * list init_data * V))
1494         (tvars: list (ident * list init_data * W)),
1495  list_forall2 (match_var_etry match_var) vars tvars →
1496  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
1497Proof.
1498  induction 1; simpl.
1499  auto.
1500  destruct a1 as [[id1 init1] info1].
1501  destruct b1 as [[id2 init2] info2].
1502  red in H. destruct H as [X [Y Z]]. subst id2 init2.
1503  generalize IHlist_forall2.
1504  destruct (add_globals (g1, m) al).
1505  destruct (add_globals (g2, m) bl).
1506  simpl. intro. subst m1. auto.
1507Qed.
1508
1509Lemma symbols_add_globals_match:
1510  forall (g1: genv A) (g2: genv B) (m: mem),
1511  symbols g1 = symbols g2 →
1512  forall (vars: list (ident * list init_data * V))
1513         (tvars: list (ident * list init_data * W)),
1514  list_forall2 (match_var_etry match_var) vars tvars →
1515  symbols (fst (add_globals (g1, m) vars)) =
1516  symbols (fst (add_globals (g2, m) tvars)).
1517Proof.
1518  induction 2; simpl.
1519  auto.
1520  destruct a1 as [[id1 init1] info1].
1521  destruct b1 as [[id2 init2] info2].
1522  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
1523  generalize IHlist_forall2.
1524  generalize (mem_add_globals_match g1 g2 m H1).
1525  destruct (add_globals (g1, m) al).
1526  destruct (add_globals (g2, m) bl).
1527  simpl. intros. congruence.
1528Qed.
1529
1530Theorem find_funct_ptr_match:
1531  forall (b: block) (f: A),
1532  find_funct_ptr ? (globalenv p) b = Some ? f →
1533  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
1534Proof.
1535  intros until f. destruct match_prog as [X [Y Z]].
1536  destruct (add_functs_match X) as [P [Q R]].
1537  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1538  auto.
1539Qed.
1540
1541Theorem find_funct_ptr_rev_match:
1542  forall (b: block) (tf: B),
1543  find_funct_ptr ? (globalenv p') b = Some ? tf →
1544  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
1545Proof.
1546  intros until tf. destruct match_prog as [X [Y Z]].
1547  destruct (add_functs_rev_match X) as [P [Q R]].
1548  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1549  auto.
1550Qed.
1551
1552Theorem find_funct_match:
1553  forall (v: val) (f: A),
1554  find_funct (globalenv p) v = Some ? f →
1555  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
1556Proof.
1557  intros until f. unfold find_funct.
1558  case v; try (intros; discriminate).
1559  intros b ofs.
1560  case (Int.eq ofs Int.zero); try (intros; discriminate).
1561  apply find_funct_ptr_match.
1562Qed.
1563
1564Theorem find_funct_rev_match:
1565  forall (v: val) (tf: B),
1566  find_funct (globalenv p') v = Some ? tf →
1567  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
1568Proof.
1569  intros until tf. unfold find_funct.
1570  case v; try (intros; discriminate).
1571  intros b ofs.
1572  case (Int.eq ofs Int.zero); try (intros; discriminate).
1573  apply find_funct_ptr_rev_match.
1574Qed.
1575
1576Lemma symbols_init_match:
1577  symbols (globalenv p') = symbols (globalenv p).
1578Proof.
1579  unfold globalenv. unfold globalenv_initmem.
1580  destruct match_prog as [X [Y Z]].
1581  destruct (add_functs_match X) as [P [Q R]].
1582  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
1583Qed.
1584
1585Theorem find_symbol_match:
1586  forall (s: ident),
1587  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1588Proof.
1589  intros. unfold find_symbol.
1590  rewrite symbols_init_match. auto.
1591Qed.
1592
1593Theorem init_mem_match:
1594  init_mem p' = init_mem p.
1595Proof.
1596  unfold init_mem. unfold globalenv_initmem.
1597  destruct match_prog as [X [Y Z]].
1598  symmetry. apply mem_add_globals_match. auto.
1599Qed.
1600
1601End MATCH_PROGRAM.
1602
1603Section TRANSF_PROGRAM_PARTIAL2.
1604
1605Variable A B V W: Type.
1606Variable transf_fun: A → res B.
1607Variable transf_var: V → res W.
1608Variable p: program A V.
1609Variable p': program B W.
1610Hypothesis transf_OK:
1611  transform_partial_program2 transf_fun transf_var p = OK ? p'.
1612
1613Remark prog_match:
1614  match_program
1615    (fun fd tfd => transf_fun fd = OK ? tfd)
1616    (fun info tinfo => transf_var info = OK ? tinfo)
1617    p p'.
1618Proof.
1619  apply transform_partial_program2_match; auto.
1620Qed.
1621
1622Theorem find_funct_ptr_transf_partial2:
1623  forall (b: block) (f: A),
1624  find_funct_ptr ? (globalenv p) b = Some ? f →
1625  ∃f'.
1626  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1627Proof.
1628  intros.
1629  exploit find_funct_ptr_match. eexact prog_match. eauto.
1630  intros [tf [X Y]]. exists tf; auto.
1631Qed.
1632
1633Theorem find_funct_ptr_rev_transf_partial2:
1634  forall (b: block) (tf: B),
1635  find_funct_ptr ? (globalenv p') b = Some ? tf →
1636  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1637Proof.
1638  intros.
1639  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1640Qed.
1641
1642Theorem find_funct_transf_partial2:
1643  forall (v: val) (f: A),
1644  find_funct (globalenv p) v = Some ? f →
1645  ∃f'.
1646  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1647Proof.
1648  intros.
1649  exploit find_funct_match. eexact prog_match. eauto.
1650  intros [tf [X Y]]. exists tf; auto.
1651Qed.
1652
1653Theorem find_funct_rev_transf_partial2:
1654  forall (v: val) (tf: B),
1655  find_funct (globalenv p') v = Some ? tf →
1656  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1657Proof.
1658  intros.
1659  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1660Qed.
1661
1662Theorem find_symbol_transf_partial2:
1663  forall (s: ident),
1664  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1665Proof.
1666  intros. eapply find_symbol_match. eexact prog_match.
1667Qed.
1668
1669Theorem init_mem_transf_partial2:
1670  init_mem p' = init_mem p.
1671Proof.
1672  intros. eapply init_mem_match. eexact prog_match.
1673Qed.
1674
1675End TRANSF_PROGRAM_PARTIAL2.
1676
1677Section TRANSF_PROGRAM_PARTIAL.
1678
1679Variable A B V: Type.
1680Variable transf: A → res B.
1681Variable p: program A V.
1682Variable p': program B V.
1683Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1684
1685Remark transf2_OK:
1686  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1687Proof.
1688  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1689  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1690  rewrite map_partial_identity; auto.
1691Qed.
1692
1693Theorem find_funct_ptr_transf_partial:
1694  forall (b: block) (f: A),
1695  find_funct_ptr ? (globalenv p) b = Some ? f →
1696  ∃f'.
1697  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1698Proof.
1699  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1700Qed.
1701
1702Theorem find_funct_ptr_rev_transf_partial:
1703  forall (b: block) (tf: B),
1704  find_funct_ptr ? (globalenv p') b = Some ? tf →
1705  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1706Proof.
1707  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1708Qed.
1709
1710Theorem find_funct_transf_partial:
1711  forall (v: val) (f: A),
1712  find_funct (globalenv p) v = Some ? f →
1713  ∃f'.
1714  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1715Proof.
1716  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1717Qed.
1718
1719Theorem find_funct_rev_transf_partial:
1720  forall (v: val) (tf: B),
1721  find_funct (globalenv p') v = Some ? tf →
1722  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1723Proof.
1724  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1725Qed.
1726
1727Theorem find_symbol_transf_partial:
1728  forall (s: ident),
1729  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1730Proof.
1731  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1732Qed.
1733
1734Theorem init_mem_transf_partial:
1735  init_mem p' = init_mem p.
1736Proof.
1737  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1738Qed.
1739
1740End TRANSF_PROGRAM_PARTIAL.
1741
1742Section TRANSF_PROGRAM.
1743
1744Variable A B V: Type.
1745Variable transf: A → B.
1746Variable p: program A V.
1747Let tp := transform_program transf p.
1748
1749Remark transf_OK:
1750  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1751Proof.
1752  unfold tp, transform_program, transform_partial_program.
1753  rewrite map_partial_total. reflexivity.
1754Qed.
1755
1756Theorem find_funct_ptr_transf:
1757  forall (b: block) (f: A),
1758  find_funct_ptr ? (globalenv p) b = Some ? f →
1759  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1760Proof.
1761  intros.
1762  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1763  as [f' [X Y]]. congruence.
1764Qed.
1765
1766Theorem find_funct_ptr_rev_transf:
1767  forall (b: block) (tf: B),
1768  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1769  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1770Proof.
1771  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1772  intros [f [X Y]]. exists f; split. auto. congruence.
1773Qed.
1774
1775Theorem find_funct_transf:
1776  forall (v: val) (f: A),
1777  find_funct (globalenv p) v = Some ? f →
1778  find_funct (globalenv tp) v = Some ? (transf f).
1779Proof.
1780  intros.
1781  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1782  as [f' [X Y]]. congruence.
1783Qed.
1784
1785Theorem find_funct_rev_transf:
1786  forall (v: val) (tf: B),
1787  find_funct (globalenv tp) v = Some ? tf →
1788  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
1789Proof.
1790  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1791  intros [f [X Y]]. exists f; split. auto. congruence.
1792Qed.
1793
1794Theorem find_symbol_transf:
1795  forall (s: ident),
1796  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1797Proof.
1798  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1799Qed.
1800
1801Theorem init_mem_transf:
1802  init_mem tp = init_mem p.
1803Proof.
1804  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1805Qed.
1806
1807End TRANSF_PROGRAM.
1808
1809End Genv.
1810*)
1811
Note: See TracBrowser for help on using the repository browser.