source: src/common/Globalenvs.ma @ 1599

Last change on this file since 1599 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

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