source: Deliverables/D3.1/C-semantics/Globalenvs.ma @ 496

Last change on this file since 496 was 496, checked in by campbell, 9 years ago

First pass at moving regions to block type.

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