source: src/common/Globalenvs.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

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