source: src/common/Globalenvs.ma @ 1881

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

First cut at using back-end memory model throughout.
Note the correction to BEValues.

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