source: src/common/Globalenvs.ma @ 2010

Last change on this file since 2010 was 2010, checked in by campbell, 8 years ago

Make globalenvs use proper maps.

File size: 51.2 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 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  ].
103cases 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  \fst (globalenv_allocmem 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
230lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
231  find_funct F ge v = Some F f →
232  ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
233#F #ge *
234[ #f #E normalize in E; destruct
235| #sz #i #f #E normalize in E; destruct
236| #f #fn #E normalize in E; destruct
237| #r #f #E normalize in E; destruct
238| * #pty #b #c * #off #f #E whd in E:(??%?);
239  cases off in E ⊢ %; [ 2,3: #x ]
240  #E whd in E:(??%?); destruct
241  %{pty} %{b} %{c} % // @E
242] qed.
243
244
245(*
246(* * ** Properties of the operations. *)
247
248  find_funct_inv:
249    ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F.
250    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
251  find_funct_find_funct_ptr:
252    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
253    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
254
255  find_symbol_exists:
256    ∀F,V: Type[0]. ∀p: program F V.
257           ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
258    in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
259    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
260  find_funct_ptr_exists:
261    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
262    list_norepet ? (prog_funct_names ?? p) →
263    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
264    in_list ? 〈id, f〉 (prog_funct ?? p) →
265    ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
266           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;
267
268  find_funct_ptr_inversion:
269    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
270    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
271    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
272  find_funct_inversion:
273    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
274    find_funct ? (globalenv ?? p) v = Some ? f →
275    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
276  find_funct_ptr_symbol_inversion:
277    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
278    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 →
279    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
280    in_list ? 〈id, f〉 (prog_funct ?? p);
281
282  find_funct_ptr_prop:
283    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
284    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
285    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
286    P f;
287  find_funct_prop:
288    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
289    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
290    find_funct ? (globalenv ?? p) v = Some ? f →
291    P f;
292
293  initmem_nullptr:
294    ∀F,V: Type[0]. ∀p: program F V.
295    let m ≝ init_mem ?? p in
296    valid_block m nullptr ∧
297    (blocks m) nullptr = empty_block 0 0 Any;
298(*  initmem_inject_neutral:
299    ∀F,V: Type[0]. ∀p: program F V.
300    mem_inject_neutral (init_mem ?? p);*)
301  find_funct_ptr_negative:
302    ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F.
303    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
304  find_symbol_not_fresh:
305    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
306    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
307  find_symbol_not_nullptr:
308    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
309    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
310  global_addresses_distinct:
311    ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2.
312    id1≠id2 →
313    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
314    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
315    b1≠b2;
316
317(* * Commutation properties between program transformations
318  and operations over global environments. *)
319
320  find_funct_ptr_transf:
321    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
322    ∀b: block. ∀f: A.
323    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
324    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f);
325  find_funct_transf:
326    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
327    ∀v: val. ∀f: A.
328    find_funct ? (globalenv ?? p) v = Some ? f →
329    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f);
330  find_symbol_transf:
331    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
332    ∀s: ident.
333    find_symbol ? (globalenv ?? (transform_program … transf p)) s =
334    find_symbol ? (globalenv ?? p) s;
335  init_mem_transf:
336    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
337    init_mem ?? (transform_program … transf p) = init_mem ?? p;
338  find_funct_ptr_rev_transf:
339    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
340    ∀b : block. ∀tf : B.
341    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
342    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
343  find_funct_rev_transf:
344    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
345    ∀v : val. ∀tf : B.
346    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
347    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
348
349(* * Commutation properties between partial program transformations
350  and operations over global environments. *)
351
352  find_funct_ptr_transf_partial:
353    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
354    transform_partial_program … transf p = OK ? p' →
355    ∀b: block. ∀f: A.
356    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
357    ∃f'.
358    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
359  find_funct_transf_partial:
360    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
361    transform_partial_program … transf p = OK ? p' →
362    ∀v: val. ∀f: A.
363    find_funct ? (globalenv ?? p) v = Some ? f →
364    ∃f'.
365    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
366  find_symbol_transf_partial:
367    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
368    transform_partial_program … transf p = OK ? p' →
369    ∀s: ident.
370    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
371  init_mem_transf_partial:
372    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
373    transform_partial_program … transf p = OK ? p' →
374    init_mem ?? p' = init_mem ?? p;
375  find_funct_ptr_rev_transf_partial:
376    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
377    transform_partial_program … transf p = OK ? p' →
378    ∀b : block. ∀tf : B.
379    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
380    ∃f : A.
381      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
382  find_funct_rev_transf_partial:
383    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
384    transform_partial_program … transf p = OK ? p' →
385    ∀v : val. ∀tf : B.
386    find_funct ? (globalenv ?? p') v = Some ? tf →
387    ∃f : A.
388      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*;
389
390  find_funct_ptr_transf_partial2:
391    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
392           ∀p: program A V. ∀p': program B W.
393    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
394    ∀b: block. ∀f: A.
395    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
396    ∃f'.
397    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
398  find_funct_transf_partial2:
399    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
400           ∀p: program A V. ∀p': program B W.
401    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
402    ∀v: val. ∀f: A.
403    find_funct ? (globalenv ?? p) v = Some ? f →
404    ∃f'.
405    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
406  find_symbol_transf_partial2:
407    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
408           ∀p: program A V. ∀p': program B W.
409    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
410    ∀s: ident.
411    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
412  init_mem_transf_partial2:
413    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
414           ∀p: program A V. ∀p': program B W.
415    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
416    init_mem ?? p' = init_mem ?? p;
417  find_funct_ptr_rev_transf_partial2:
418    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
419           ∀p: program A V. ∀p': program B W.
420    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
421    ∀b: block. ∀tf: B.
422    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
423    ∃f : A.
424      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
425  find_funct_rev_transf_partial2:
426    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
427           ∀p: program A V. ∀p': program B W.
428    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
429    ∀v: val. ∀tf: B.
430    find_funct ? (globalenv ?? p') v = Some ? tf →
431    ∃f : A.
432      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ;
433
434(* * Commutation properties between matching between programs
435  and operations over global environments. *)
436
437  find_funct_ptr_match:
438    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
439           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
440    match_program … match_fun match_var p p' →
441    ∀b: block. ∀f: A.
442    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
443    ∃tf : B.
444    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
445  find_funct_ptr_rev_match:
446    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
447           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
448    match_program … match_fun match_var p p' →
449    ∀b: block. ∀tf: B.
450    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
451    ∃f : A.
452    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
453  find_funct_match:
454    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
455           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
456    match_program … match_fun match_var p p' →
457    ∀v: val. ∀f: A.
458    find_funct ? (globalenv ?? p) v = Some ? f →
459    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
460  find_funct_rev_match:
461    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
462           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
463    match_program … match_fun match_var p p' →
464    ∀v: val. ∀tf: B.
465    find_funct ? (globalenv ?? p') v = Some ? tf →
466    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
467  find_symbol_match:
468    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
469           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
470    match_program … match_fun match_var p p' →
471    ∀s: ident.
472    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
473  init_mem_match:
474    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
475           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
476    match_program … match_fun match_var p p' →
477    init_mem ?? p' = init_mem ?? p*)*)
478
479(*
480Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
481  ZMap.get b g.(functions).
482
483Definition find_funct (g: genv) (v: val) : option F :=
484  match v with
485  | Vptr b ofs =>
486      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
487  | _ =>
488      None
489  end.
490
491Definition find_symbol ? (g: genv) (symb: ident) : option block :=
492  PTree.get symb g.(symbols).
493
494Lemma find_funct_inv:
495  forall (ge: t) (v: val) (f: F),
496  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
497Proof.
498  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
499  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
500  exists b. congruence.
501  discriminate.
502Qed.
503
504Lemma find_funct_find_funct_ptr:
505  forall (ge: t) (b: block),
506  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
507Proof.
508  intros. simpl.
509  generalize (Int.eq_spec Int.zero Int.zero).
510  case (Int.eq Int.zero Int.zero); intros.
511  auto. tauto.
512Qed.
513*)
514
515(*
516##[ #A B C transf p b f; elim p; #fns main vars;
517    elim fns;
518    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
519    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
520        nrewrite > (?:nextfunction ?? = length ? t);
521        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
522            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
523        ##| nrewrite > (?:nextfunction ?? = length ? t);
524          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
525              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
526          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
527            ##[ #H; destruct (H); //;
528            ##| #H; napply IH; napply H;
529            ##]
530          ##]
531        ##]
532    ##]
533##| #A B C transf p v f; elim v;
534    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
535    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
536    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
537        whd in ⊢ (??%? → ??%?);
538        ##[ elim p; #fns main vars; elim fns;
539          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
540          ##| #h t; elim h; #f fn IH;
541              whd in ⊢ (??%? → ??%?);
542              nrewrite > (?:nextfunction ?? = length ? t);
543              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
544                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
545              ##| nrewrite > (?:nextfunction ?? = length ? t);
546                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
547                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
548                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
549                  ##[ destruct (H); //;
550                  ##| napply IH; napply H;
551                  ##]
552                ##]
553              ##]
554          ##]
555       ##| #H; destruct;
556       ##]
557    ##]
558##| #A B C transf p id; elim p; #fns main vars;
559    elim fns;
560    ##[ normalize; //
561    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
562        elim (ident_eq fid id); #e;
563        ##[ whd in ⊢ (??%%);
564          nrewrite > (?:nextfunction ?? = length ? t);
565          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
566              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
567          ##| nrewrite > (?:nextfunction ?? = length ? t);
568            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
569                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
570            ##| //
571            ##]
572          ##]
573        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
574        ##]
575    ##]
576##| //;
577##| #A B C transf p b tf; elim p; #fns main vars;
578    elim fns;
579    ##[ normalize; #H; destruct;
580    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
581        nrewrite > (?:nextfunction ?? = length ? t);
582        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
583            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
584        ##| nrewrite > (?:nextfunction ?? = length ? t);
585          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
586              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
587          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
588            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
589            ##| #H; napply IH; napply H;
590            ##]
591          ##]
592        ##]
593    ##]
594##| #A B C transf p v tf; elim p; #fns main vars; elim v;
595  ##[ normalize; #H; destruct;
596  ##| ##2,3: #x; normalize; #H; destruct;
597  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
598    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
599      elim fns;
600      ##[ normalize; #H; destruct;
601      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
602          nrewrite > (?:nextfunction ?? = length ? t);
603          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
604              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
605          ##| nrewrite > (?:nextfunction ?? = length ? t);
606            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
607                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
608            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
609              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
610              ##| #H; napply IH; napply H;
611              ##]
612            ##]
613          ##]
614      ##]
615    ##| normalize; #H; destruct;
616    ##]
617 ##]
618##] qed.
619         
620
621Lemma functions_globalenv:
622  forall (p: program F V),
623  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
624Proof.
625  assert (forall init vars,
626     functions (fst (add_globals init vars)) = functions (fst init)).
627  induction vars; simpl.
628  reflexivity.
629  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
630  simpl. exact IHvars.
631
632  unfold add_globals; simpl.
633  intros. unfold globalenv; unfold globalenv_initmem.
634  rewrite H. reflexivity.
635Qed.
636
637Lemma initmem_nullptr:
638  forall (p: program F V),
639  let m := init_mem p in
640  valid_block m nullptr /\
641  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
642Proof.
643  pose (P := fun m => valid_block m nullptr /\
644        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
645  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
646  induction vars; simpl; intros.
647  auto.
648  destruct a as [[id1 in1] inf1].
649  destruct (add_globals init vars) as [g st].
650  simpl in *. destruct IHvars. split.
651  red; simpl. red in H0. omega.
652  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
653
654  intro. unfold init_mem, globalenv_initmem. apply H.
655  red; simpl. split. compute. auto. reflexivity.
656Qed.
657
658Lemma initmem_inject_neutral:
659  forall (p: program F V),
660  mem_inject_neutral (init_mem p).
661Proof.
662  assert (forall g0 vars g1 m,
663      add_globals (g0, Mem.empty) vars = (g1, m) →
664      mem_inject_neutral m).
665  Opaque alloc_init_data.
666  induction vars; simpl.
667  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
668  simpl in H1. rewrite Mem.getN_init in H1.
669  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
670  destruct a as [[id1 init1] info1].
671  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
672  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
673  intros. inv H.
674  eapply Mem.alloc_init_data_neutral; eauto.
675  intros. caseEq (globalenv_initmem p). intros g m EQ.
676  unfold init_mem; rewrite EQ; simpl.
677  unfold globalenv_initmem in EQ. eauto.
678Qed.     
679
680Remark nextfunction_add_functs_neg:
681  forall fns, nextfunction (add_functs empty fns) < 0.
682Proof.
683  induction fns; simpl; intros. omega. unfold Zpred. omega.
684Qed.
685
686Theorem find_funct_ptr_negative:
687  forall (p: program F V) (b: block) (f: F),
688  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
689Proof.
690  intros until f.
691  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
692    induction fns; simpl.
693    rewrite ZMap.gi. congruence.
694    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
695    intro. rewrite e. apply nextfunction_add_functs_neg.
696    auto.
697  unfold find_funct_ptr. rewrite functions_globalenv.
698  intros. eauto.
699Qed.
700
701Remark find_symbol_add_functs_negative:
702  forall (fns: list (ident * F)) s b,
703  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
704Proof.
705  induction fns; simpl; intros until b.
706  rewrite PTree.gempty. congruence.
707  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
708  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
709  eauto.
710Qed.
711
712Remark find_symbol_add_symbols_not_fresh:
713  forall fns vars g m s b,
714  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
715  (symbols g)!s = Some ? b →
716  b < nextblock m.
717Proof.
718  induction vars; simpl; intros until b.
719  intros. inversion H. subst g m. simpl.
720  generalize (find_symbol_add_functs_negative fns s H0). omega.
721  Transparent alloc_init_data.
722  destruct a as [[id1 init1] info1].
723  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
724  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
725  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
726  intro EQ; inversion EQ. omega.
727  intro. generalize (IHvars _ _ _ _ ADG H). omega.
728Qed.
729
730Theorem find_symbol_not_fresh:
731  forall (p: program F V) (id: ident) (b: block),
732  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
733Proof.
734  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
735  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
736                      (prog_vars p)); intros g m EQ.
737  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
738Qed.
739
740Lemma find_symbol_exists:
741  forall (p: program F V)
742         (id: ident) (init: list init_data) (v: V),
743  In (id, init, v) (prog_vars p) →
744  ∃b. find_symbol ? (globalenv p) id = Some ? b.
745Proof.
746  intros until v.
747  assert (forall initm vl, In (id, init, v) vl →
748           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
749  induction vl; simpl; intros.
750  elim H.
751  destruct a as [[id0 init0] v0].
752  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
753  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
754  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
755  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
756Qed.
757
758Remark find_symbol_above_nextfunction:
759  forall (id: ident) (b: block) (fns: list (ident * F)),
760  let g := add_functs empty fns in
761  PTree.get id g.(symbols) = Some ? b →
762  b > g.(nextfunction).
763Proof.
764  induction fns; simpl.
765  rewrite PTree.gempty. congruence.
766  rewrite PTree.gsspec. case (peq id (fst a)); intro.
767  intro EQ. inversion EQ. unfold Zpred. omega.
768  intros. generalize (IHfns H). unfold Zpred; omega.
769Qed.
770
771Remark find_symbol_add_globals:
772  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
773  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
774  find_symbol ? (fst (add_globals ge_m vars)) id =
775  find_symbol ? (fst ge_m) id.
776Proof.
777  unfold find_symbol; induction vars; simpl; intros.
778  auto.
779  destruct a as [[id0 init0] var0]. simpl in *.
780  caseEq (add_globals ge_m vars); intros ge' m' EQ.
781  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
782  apply IHvars. tauto. intuition congruence.
783Qed.
784
785Lemma find_funct_ptr_exists:
786  forall (p: program F V) (id: ident) (f: F),
787  list_norepet (prog_funct_names p) →
788  list_disjoint (prog_funct_names p) (prog_var_names p) →
789  In (id, f) (prog_funct p) →
790  ∃b. find_symbol ? (globalenv p) id = Some ? b
791         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
792Proof.
793  intros until f.
794  assert (forall (fns: list (ident * F)),
795           list_norepet (map (@fst ident F) fns) →
796           In (id, f) fns →
797           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
798                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
799  unfold find_symbol, find_funct_ptr. induction fns; intros.
800  elim H0.
801  destruct a as [id0 f0]; simpl in *. inv H.
802  unfold add_funct; simpl.
803  rewrite PTree.gsspec. destruct (peq id id0).
804  subst id0. econstructor; split. eauto.
805  replace f0 with f. apply ZMap.gss.
806  elim H0; intro. congruence. elim H3.
807  change id with (@fst ident F (id, f)). apply List.in_map. auto.
808  exploit IHfns; eauto. elim H0; intro. congruence. auto.
809  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
810  generalize (find_symbol_above_nextfunction _ _ X).
811  unfold block; unfold ZIndexed.t; intro; omega.
812
813  intros. exploit H; eauto. intros [b [X Y]].
814  exists b; split.
815  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
816  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
817  unfold prog_funct_names. change id with (fst (id, f)).
818  apply List.in_map; auto.
819  unfold find_funct_ptr. rewrite functions_globalenv.
820  assumption.
821Qed.
822
823Lemma find_funct_ptr_inversion:
824  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
825  find_funct_ptr ? (globalenv p) b = Some ? f →
826  ∃id. In (id, f) (prog_funct p).
827Proof.
828  intros until f.
829  assert (forall fns: list (ident * F),
830    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
831    ∃id. In (id, f) fns).
832  unfold find_funct_ptr. induction fns; simpl.
833  rewrite ZMap.gi. congruence.
834  destruct a as [id0 f0]; simpl.
835  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
836  intro. inv H. exists id0; auto.
837  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
838  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
839Qed.
840
841Lemma find_funct_ptr_prop:
842  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
843  (forall id f, In (id, f) (prog_funct p) → P f) →
844  find_funct_ptr ? (globalenv p) b = Some ? f →
845  P f.
846Proof.
847  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
848Qed.
849
850Lemma find_funct_inversion:
851  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
852  find_funct (globalenv p) v = Some ? f →
853  ∃id. In (id, f) (prog_funct p).
854Proof.
855  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
856  rewrite find_funct_find_funct_ptr ? in H.
857  eapply find_funct_ptr_inversion; eauto.
858Qed.
859
860Lemma find_funct_prop:
861  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
862  (forall id f, In (id, f) (prog_funct p) → P f) →
863  find_funct (globalenv p) v = Some ? f →
864  P f.
865Proof.
866  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
867Qed.
868
869Lemma find_funct_ptr_symbol_inversion:
870  forall (p: program F V) (id: ident) (b: block) (f: F),
871  find_symbol ? (globalenv p) id = Some ? b →
872  find_funct_ptr ? (globalenv p) b = Some ? f →
873  In (id, f) p.(prog_funct).
874Proof.
875  intros until f.
876  assert (forall fns,
877           let g := add_functs empty fns in
878           PTree.get id g.(symbols) = Some ? b →
879           ZMap.get b g.(functions) = Some ? f →
880           In (id, f) fns).
881    induction fns; simpl.
882    rewrite ZMap.gi. congruence.
883    set (g := add_functs empty fns).
884    rewrite PTree.gsspec. rewrite ZMap.gsspec.
885    case (peq id (fst a)); intro.
886    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
887    intro EQ2. left. destruct a. simpl in *. congruence.
888    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
889    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
890  assert (forall g0 m0, b < 0 →
891          forall vars g m,
892          add_globals (g0, m0) vars = (g, m) →
893          PTree.get id g.(symbols) = Some ? b →
894          PTree.get id g0.(symbols) = Some ? b).
895    induction vars; simpl.
896    intros. inv H1. auto.
897    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
898    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
899    unfold add_symbol; intros A B. rewrite <- B. simpl.
900    rewrite PTree.gsspec. case (peq id id1); intros.
901    assert (b > 0). inv H1. apply nextblock_pos.
902    omegaContradiction.
903    eauto.
904  intros.
905  generalize (find_funct_ptr_negative _ _ H2). intro.
906  pose (g := add_functs empty (prog_funct p)).
907  apply H. 
908  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
909  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
910  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
911Qed.
912
913Theorem find_symbol_not_nullptr:
914  forall (p: program F V) (id: ident) (b: block),
915  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
916Proof.
917  intros until b.
918  assert (forall fns,
919          find_symbol ? (add_functs empty fns) id = Some ? b →
920          b <> nullptr).
921    unfold find_symbol; induction fns; simpl.
922    rewrite PTree.gempty. congruence.
923    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
924    destruct (peq id id1); intros.
925    inversion H. generalize (nextfunction_add_functs_neg fns).
926    unfold block, nullptr; omega.
927    auto.
928  set (g0 := add_functs empty p.(prog_funct)).
929  assert (forall vars g m,
930          add_globals (g0, Mem.empty) vars = (g, m) →
931          find_symbol ? g id = Some ? b →
932          b <> nullptr).
933    induction vars; simpl; intros until m.
934    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
935    destruct a as [[id1 init1] info1].
936    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
937    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
938    destruct (peq id id1); intros.
939    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
940    eauto.
941  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
942Qed.
943
944Theorem global_addresses_distinct:
945  forall (p: program F V) id1 id2 b1 b2,
946  id1<>id2 →
947  find_symbol ? (globalenv p) id1 = Some ? b1 →
948  find_symbol ? (globalenv p) id2 = Some ? b2 →
949  b1<>b2.
950Proof.
951  intros.
952  assert (forall fns,
953    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
954    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
955    b1 <> b2).
956  unfold find_symbol. induction fns; simpl; intros.
957  rewrite PTree.gempty in H2. discriminate.
958  destruct a as [id f]; simpl in *.
959  rewrite PTree.gsspec in H2.
960  destruct (peq id1 id). subst id. inv H2.
961  rewrite PTree.gso in H3; auto.
962  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
963  rewrite PTree.gsspec in H3.
964  destruct (peq id2 id). subst id. inv H3.
965  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
966  eauto.
967  set (ge0 := add_functs empty p.(prog_funct)).
968  assert (forall (vars: list (ident * list init_data * V)) ge m,
969    add_globals (ge0, Mem.empty) vars = (ge, m) →
970    find_symbol ? ge id1 = Some ? b1 →
971    find_symbol ? ge id2 = Some ? b2 →
972    b1 <> b2).
973  unfold find_symbol. induction vars; simpl.
974  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
975  intros ge m. destruct a as [[id init] info].
976  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
977  unfold add_symbol. simpl. intros.
978  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
979  rewrite PTree.gso in H4; auto.
980  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
981  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
982  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
983  eauto.
984  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
985  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
986  fold ge_m. apply surjective_pairing. auto. auto.
987Qed.
988
989End GENV.
990
991(* Global environments and program transformations. *)
992
993Section MATCH_PROGRAM.
994
995Variable A B V W: Type.
996Variable match_fun: A → B → Prop.
997Variable match_var: V → W → Prop.
998Variable p: program A V.
999Variable p': program B W.
1000Hypothesis match_prog:
1001  match_program match_fun match_var p p'.
1002
1003Lemma add_functs_match:
1004  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1005  list_forall2 (match_funct_etry match_fun) fns tfns →
1006  let r := add_functs (empty A) fns in
1007  let tr := add_functs (empty B) tfns in
1008  nextfunction tr = nextfunction r /\
1009  symbols tr = symbols r /\
1010  forall (b: block) (f: A),
1011  ZMap.get b (functions r) = Some ? f →
1012  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
1013Proof.
1014  induction 1; simpl.
1015
1016  split. reflexivity. split. reflexivity.
1017  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1018
1019  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1020  simpl. red in H. destruct H.
1021  destruct IHlist_forall2 as [X [Y Z]].
1022  rewrite X. rewrite Y. 
1023  split. auto.
1024  split. congruence.
1025  intros b f.
1026  repeat (rewrite ZMap.gsspec).
1027  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1028  intro EQ; inv EQ. exists fn2; auto.
1029  auto.
1030Qed.
1031
1032Lemma add_functs_rev_match:
1033  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1034  list_forall2 (match_funct_etry match_fun) fns tfns →
1035  let r := add_functs (empty A) fns in
1036  let tr := add_functs (empty B) tfns in
1037  nextfunction tr = nextfunction r /\
1038  symbols tr = symbols r /\
1039  forall (b: block) (tf: B),
1040  ZMap.get b (functions tr) = Some ? tf →
1041  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
1042Proof.
1043  induction 1; simpl.
1044
1045  split. reflexivity. split. reflexivity.
1046  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1047
1048  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1049  simpl. red in H. destruct H.
1050  destruct IHlist_forall2 as [X [Y Z]].
1051  rewrite X. rewrite Y. 
1052  split. auto.
1053  split. congruence.
1054  intros b f.
1055  repeat (rewrite ZMap.gsspec).
1056  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1057  intro EQ; inv EQ. exists fn1; auto.
1058  auto.
1059Qed.
1060
1061Lemma mem_add_globals_match:
1062  forall (g1: genv A) (g2: genv B) (m: mem)
1063         (vars: list (ident * list init_data * V))
1064         (tvars: list (ident * list init_data * W)),
1065  list_forall2 (match_var_etry match_var) vars tvars →
1066  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
1067Proof.
1068  induction 1; simpl.
1069  auto.
1070  destruct a1 as [[id1 init1] info1].
1071  destruct b1 as [[id2 init2] info2].
1072  red in H. destruct H as [X [Y Z]]. subst id2 init2.
1073  generalize IHlist_forall2.
1074  destruct (add_globals (g1, m) al).
1075  destruct (add_globals (g2, m) bl).
1076  simpl. intro. subst m1. auto.
1077Qed.
1078
1079Lemma symbols_add_globals_match:
1080  forall (g1: genv A) (g2: genv B) (m: mem),
1081  symbols g1 = symbols g2 →
1082  forall (vars: list (ident * list init_data * V))
1083         (tvars: list (ident * list init_data * W)),
1084  list_forall2 (match_var_etry match_var) vars tvars →
1085  symbols (fst (add_globals (g1, m) vars)) =
1086  symbols (fst (add_globals (g2, m) tvars)).
1087Proof.
1088  induction 2; simpl.
1089  auto.
1090  destruct a1 as [[id1 init1] info1].
1091  destruct b1 as [[id2 init2] info2].
1092  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
1093  generalize IHlist_forall2.
1094  generalize (mem_add_globals_match g1 g2 m H1).
1095  destruct (add_globals (g1, m) al).
1096  destruct (add_globals (g2, m) bl).
1097  simpl. intros. congruence.
1098Qed.
1099
1100Theorem find_funct_ptr_match:
1101  forall (b: block) (f: A),
1102  find_funct_ptr ? (globalenv p) b = Some ? f →
1103  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
1104Proof.
1105  intros until f. destruct match_prog as [X [Y Z]].
1106  destruct (add_functs_match X) as [P [Q R]].
1107  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1108  auto.
1109Qed.
1110
1111Theorem find_funct_ptr_rev_match:
1112  forall (b: block) (tf: B),
1113  find_funct_ptr ? (globalenv p') b = Some ? tf →
1114  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
1115Proof.
1116  intros until tf. destruct match_prog as [X [Y Z]].
1117  destruct (add_functs_rev_match X) as [P [Q R]].
1118  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1119  auto.
1120Qed.
1121
1122Theorem find_funct_match:
1123  forall (v: val) (f: A),
1124  find_funct (globalenv p) v = Some ? f →
1125  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
1126Proof.
1127  intros until f. unfold find_funct.
1128  case v; try (intros; discriminate).
1129  intros b ofs.
1130  case (Int.eq ofs Int.zero); try (intros; discriminate).
1131  apply find_funct_ptr_match.
1132Qed.
1133
1134Theorem find_funct_rev_match:
1135  forall (v: val) (tf: B),
1136  find_funct (globalenv p') v = Some ? tf →
1137  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
1138Proof.
1139  intros until tf. unfold find_funct.
1140  case v; try (intros; discriminate).
1141  intros b ofs.
1142  case (Int.eq ofs Int.zero); try (intros; discriminate).
1143  apply find_funct_ptr_rev_match.
1144Qed.
1145
1146Lemma symbols_init_match:
1147  symbols (globalenv p') = symbols (globalenv p).
1148Proof.
1149  unfold globalenv. unfold globalenv_initmem.
1150  destruct match_prog as [X [Y Z]].
1151  destruct (add_functs_match X) as [P [Q R]].
1152  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
1153Qed.
1154
1155Theorem find_symbol_match:
1156  forall (s: ident),
1157  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1158Proof.
1159  intros. unfold find_symbol.
1160  rewrite symbols_init_match. auto.
1161Qed.
1162
1163Theorem init_mem_match:
1164  init_mem p' = init_mem p.
1165Proof.
1166  unfold init_mem. unfold globalenv_initmem.
1167  destruct match_prog as [X [Y Z]].
1168  symmetry. apply mem_add_globals_match. auto.
1169Qed.
1170
1171End MATCH_PROGRAM.
1172
1173Section TRANSF_PROGRAM_PARTIAL2.
1174
1175Variable A B V W: Type.
1176Variable transf_fun: A → res B.
1177Variable transf_var: V → res W.
1178Variable p: program A V.
1179Variable p': program B W.
1180Hypothesis transf_OK:
1181  transform_partial_program2 transf_fun transf_var p = OK ? p'.
1182
1183Remark prog_match:
1184  match_program
1185    (fun fd tfd => transf_fun fd = OK ? tfd)
1186    (fun info tinfo => transf_var info = OK ? tinfo)
1187    p p'.
1188Proof.
1189  apply transform_partial_program2_match; auto.
1190Qed.
1191
1192Theorem find_funct_ptr_transf_partial2:
1193  forall (b: block) (f: A),
1194  find_funct_ptr ? (globalenv p) b = Some ? f →
1195  ∃f'.
1196  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1197Proof.
1198  intros.
1199  exploit find_funct_ptr_match. eexact prog_match. eauto.
1200  intros [tf [X Y]]. exists tf; auto.
1201Qed.
1202
1203Theorem find_funct_ptr_rev_transf_partial2:
1204  forall (b: block) (tf: B),
1205  find_funct_ptr ? (globalenv p') b = Some ? tf →
1206  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1207Proof.
1208  intros.
1209  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1210Qed.
1211
1212Theorem find_funct_transf_partial2:
1213  forall (v: val) (f: A),
1214  find_funct (globalenv p) v = Some ? f →
1215  ∃f'.
1216  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1217Proof.
1218  intros.
1219  exploit find_funct_match. eexact prog_match. eauto.
1220  intros [tf [X Y]]. exists tf; auto.
1221Qed.
1222
1223Theorem find_funct_rev_transf_partial2:
1224  forall (v: val) (tf: B),
1225  find_funct (globalenv p') v = Some ? tf →
1226  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1227Proof.
1228  intros.
1229  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1230Qed.
1231
1232Theorem find_symbol_transf_partial2:
1233  forall (s: ident),
1234  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1235Proof.
1236  intros. eapply find_symbol_match. eexact prog_match.
1237Qed.
1238
1239Theorem init_mem_transf_partial2:
1240  init_mem p' = init_mem p.
1241Proof.
1242  intros. eapply init_mem_match. eexact prog_match.
1243Qed.
1244
1245End TRANSF_PROGRAM_PARTIAL2.
1246
1247Section TRANSF_PROGRAM_PARTIAL.
1248
1249Variable A B V: Type.
1250Variable transf: A → res B.
1251Variable p: program A V.
1252Variable p': program B V.
1253Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1254
1255Remark transf2_OK:
1256  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1257Proof.
1258  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1259  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1260  rewrite map_partial_identity; auto.
1261Qed.
1262
1263Theorem find_funct_ptr_transf_partial:
1264  forall (b: block) (f: A),
1265  find_funct_ptr ? (globalenv p) b = Some ? f →
1266  ∃f'.
1267  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1268Proof.
1269  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1270Qed.
1271
1272Theorem find_funct_ptr_rev_transf_partial:
1273  forall (b: block) (tf: B),
1274  find_funct_ptr ? (globalenv p') b = Some ? tf →
1275  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1276Proof.
1277  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1278Qed.
1279
1280Theorem find_funct_transf_partial:
1281  forall (v: val) (f: A),
1282  find_funct (globalenv p) v = Some ? f →
1283  ∃f'.
1284  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1285Proof.
1286  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1287Qed.
1288
1289Theorem find_funct_rev_transf_partial:
1290  forall (v: val) (tf: B),
1291  find_funct (globalenv p') v = Some ? tf →
1292  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1293Proof.
1294  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1295Qed.
1296
1297Theorem find_symbol_transf_partial:
1298  forall (s: ident),
1299  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1300Proof.
1301  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1302Qed.
1303
1304Theorem init_mem_transf_partial:
1305  init_mem p' = init_mem p.
1306Proof.
1307  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1308Qed.
1309
1310End TRANSF_PROGRAM_PARTIAL.
1311
1312Section TRANSF_PROGRAM.
1313
1314Variable A B V: Type.
1315Variable transf: A → B.
1316Variable p: program A V.
1317Let tp := transform_program transf p.
1318
1319Remark transf_OK:
1320  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1321Proof.
1322  unfold tp, transform_program, transform_partial_program.
1323  rewrite map_partial_total. reflexivity.
1324Qed.
1325
1326Theorem find_funct_ptr_transf:
1327  forall (b: block) (f: A),
1328  find_funct_ptr ? (globalenv p) b = Some ? f →
1329  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1330Proof.
1331  intros.
1332  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1333  as [f' [X Y]]. congruence.
1334Qed.
1335
1336Theorem find_funct_ptr_rev_transf:
1337  forall (b: block) (tf: B),
1338  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1339  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1340Proof.
1341  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1342  intros [f [X Y]]. exists f; split. auto. congruence.
1343Qed.
1344
1345Theorem find_funct_transf:
1346  forall (v: val) (f: A),
1347  find_funct (globalenv p) v = Some ? f →
1348  find_funct (globalenv tp) v = Some ? (transf f).
1349Proof.
1350  intros.
1351  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1352  as [f' [X Y]]. congruence.
1353Qed.
1354
1355Theorem find_funct_rev_transf:
1356  forall (v: val) (tf: B),
1357  find_funct (globalenv tp) v = Some ? tf →
1358  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
1359Proof.
1360  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1361  intros [f [X Y]]. exists f; split. auto. congruence.
1362Qed.
1363
1364Theorem find_symbol_transf:
1365  forall (s: ident),
1366  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1367Proof.
1368  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1369Qed.
1370
1371Theorem init_mem_transf:
1372  init_mem tp = init_mem p.
1373Proof.
1374  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1375Qed.
1376
1377End TRANSF_PROGRAM.
1378
1379End Genv.
1380*)
1381
Note: See TracBrowser for help on using the repository browser.