source: src/common/Globalenvs.ma @ 1988

Last change on this file since 1988 was 1988, checked in by campbell, 6 years ago

Abstraction of the memory contents in the memory models is no longer
necessary.

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