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

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

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

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