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

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

Port Clight semantics to the new-new matita syntax.

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