source: C-semantics/Globalenvs.ma @ 125

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

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

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