source: src/joint/BEGlobalenvs.ma @ 1988

Last change on this file since 1988 was 1988, checked in by campbell, 6 years ago

Abstraction of the memory contents in the memory models is no longer
necessary.

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