source: src/common/Globalenvs.ma @ 1999

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

Make back-end use the main global envs.

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