source: src/common/Globalenvs.ma @ 1516

Last change on this file since 1516 was 1395, checked in by sacerdot, 9 years ago

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

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