source: src/common/Globalenvs.ma @ 1994

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

Remove redundant allocation definition in Globalenvs.

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