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

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

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

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