source: C-semantics/Globalenvs.ma @ 124

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

Initial work on Clight semantics with 8051 memory spaces.

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