Context Navigation

source: C-semantics/Globalenvs.ma @ 82

Last change on this file since 82 was 24, checked in by campbell, 10 years ago
Separate out IOMonad from the rest of the executable semantics. Start adding simulation results.
File size: 47.5 KB

Line
1	(* *********************************************************************)
2	(* *)
3	(* The Compcert verified compiler *)
4	(* *)
5	(* Xavier Leroy, INRIA Paris-Rocquencourt *)
6	(* *)
7	(* Copyright Institut National de Recherche en Informatique et en *)
8	(* Automatique. All rights reserved. This file is distributed *)
9	(* under the terms of the GNU General Public License as published by *)
10	(* the Free Software Foundation, either version 2 of the License, or *)
11	(* (at your option) any later version. This file is also distributed *)
12	(* under the terms of the INRIA Non-Commercial License Agreement. *)
13	(* *)
14	(* *********************************************************************)
15
16	(* * Global environments are a component of the dynamic semantics of
17	all languages involved in the compiler. A global environment
18	maps symbol names (names of functions and of global variables)
19	to the corresponding memory addresses. It also maps memory addresses
20	of functions to the corresponding function descriptions.
21
22	Global environments, along with the initial memory state at the beginning
23	of program execution, are built from the program of interest, as follows:
24	- A distinct memory address is assigned to each function of the program.
25	These function addresses use negative numbers to distinguish them from
26	addresses of memory blocks. The associations of function name to function
27	address and function address to function description are recorded in
28	the global environment.
29	- For each global variable, a memory block is allocated and associated to
30	the name of the variable.
31
32	These operations reflect (at a high level of abstraction) what takes
33	place during program linking and program loading in a real operating
34	system. *)
35
36	include "Errors.ma".
37	include "AST.ma".
38	include "Values.ma".
39	include "Mem.ma".
40
41	(* FIXME: unimplemented stuff in AST.ma
42	naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V).
43	naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W).
44	naxiom match_program: ∀A,B,V,W:Type. program A V → program B W → Prop.
45	*)
46
47	nrecord 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
306	nlet rec foldl (A,B:Type) (f:A → B → A) (a:A) (l:list B) on l : A ≝
307	match 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 *)
314	nrecord genv (F:Type) : Type ≝ {
315	functions: block → option F;
316	nextfunction: Z;
317	symbols: ident → option block
318	}.
319
320	ndefinition 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	##\| #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	##\| #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
449	Module Genv: GENV.
450
451	Section GENV.
452
453	Variable F: Type. (* The type of functions *)
454	Variable V: Type. (* The type of information over variables *)
455
456	Record 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
462	Definition t := genv.
463
464	Definition 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
470	Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=
471	mkgenv g.(functions)
472	g.(nextfunction)
473	(PTree.set name b g.(symbols)).
474
475	Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
476	ZMap.get b g.(functions).
477
478	Definition 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
486	Definition find_symbol ? (g: genv) (symb: ident) : option block :=
487	PTree.get symb g.(symbols).
488
489	Lemma find_funct_inv:
490	forall (ge: t) (v: val) (f: F),
491	find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
492	Proof.
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.
497	Qed.
498
499	Lemma find_funct_find_funct_ptr:
500	forall (ge: t) (b: block),
501	find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
502	Proof.
503	intros. simpl.
504	generalize (Int.eq_spec Int.zero Int.zero).
505	case (Int.eq Int.zero Int.zero); intros.
506	auto. tauto.
507	Qed.
508
509	(* Construct environment and initial memory store *)
510
511	Definition empty : genv :=
512	mkgenv (ZMap.init None) (-1) (PTree.empty block).
513
514	Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=
515	List.fold_right add_funct init fns.
516
517	Definition 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
529	Definition 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
534	Definition globalenv (p: program F V) : genv :=
535	fst (globalenv_initmem p).
536	Definition init_mem (p: program F V) : mem :=
537	snd (globalenv_initmem p).
538
539	Lemma functions_globalenv:
540	forall (p: program F V),
541	functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
542	Proof.
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.
553	Qed.
554
555	Lemma 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).
560	Proof.
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.
574	Qed.
575
576	Lemma initmem_inject_neutral:
577	forall (p: program F V),
578	mem_inject_neutral (init_mem p).
579	Proof.
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.
596	Qed.
597
598	Remark nextfunction_add_functs_neg:
599	forall fns, nextfunction (add_functs empty fns) < 0.
600	Proof.
601	induction fns; simpl; intros. omega. unfold Zpred. omega.
602	Qed.
603
604	Theorem 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.
607	Proof.
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.
617	Qed.
618
619	Remark find_symbol_add_functs_negative:
620	forall (fns: list (ident * F)) s b,
621	(symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
622	Proof.
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.
628	Qed.
629
630	Remark 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.
635	Proof.
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.
646	Qed.
647
648	Theorem 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).
651	Proof.
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.
656	Qed.
657
658	Lemma 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.
663	Proof.
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.
674	Qed.
675
676	Remark 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).
681	Proof.
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.
687	Qed.
688
689	Remark 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.
694	Proof.
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.
701	Qed.
702
703	Lemma 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.
710	Proof.
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.
739	Qed.
740
741	Lemma 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).
745	Proof.
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.
757	Qed.
758
759	Lemma 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.
764	Proof.
765	intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
766	Qed.
767
768	Lemma 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).
772	Proof.
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.
776	Qed.
777
778	Lemma 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.
783	Proof.
784	intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
785	Qed.
786
787	Lemma 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).
792	Proof.
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.
829	Qed.
830
831	Theorem find_symbol_not_nullptr:
832	forall (p: program F V) (id: ident) (b: block),
833	find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
834	Proof.
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.
860	Qed.
861
862	Theorem 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.
868	Proof.
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.
905	Qed.
906
907	End GENV.
908
909	(* Global environments and program transformations. *)
910
911	Section MATCH_PROGRAM.
912
913	Variable A B V W: Type.
914	Variable match_fun: A → B → Prop.
915	Variable match_var: V → W → Prop.
916	Variable p: program A V.
917	Variable p': program B W.
918	Hypothesis match_prog:
919	match_program match_fun match_var p p'.
920
921	Lemma 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.
931	Proof.
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.
948	Qed.
949
950	Lemma 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.
960	Proof.
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.
977	Qed.
978
979	Lemma 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).
985	Proof.
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.
995	Qed.
996
997	Lemma 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)).
1005	Proof.
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.
1016	Qed.
1017
1018	Theorem 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.
1022	Proof.
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.
1027	Qed.
1028
1029	Theorem 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.
1033	Proof.
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.
1038	Qed.
1039
1040	Theorem 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.
1044	Proof.
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.
1050	Qed.
1051
1052	Theorem 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.
1056	Proof.
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.
1062	Qed.
1063
1064	Lemma symbols_init_match:
1065	symbols (globalenv p') = symbols (globalenv p).
1066	Proof.
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.
1071	Qed.
1072
1073	Theorem find_symbol_match:
1074	forall (s: ident),
1075	find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1076	Proof.
1077	intros. unfold find_symbol.
1078	rewrite symbols_init_match. auto.
1079	Qed.
1080
1081	Theorem init_mem_match:
1082	init_mem p' = init_mem p.
1083	Proof.
1084	unfold init_mem. unfold globalenv_initmem.
1085	destruct match_prog as [X [Y Z]].
1086	symmetry. apply mem_add_globals_match. auto.
1087	Qed.
1088
1089	End MATCH_PROGRAM.
1090
1091	Section TRANSF_PROGRAM_PARTIAL2.
1092
1093	Variable A B V W: Type.
1094	Variable transf_fun: A → res B.
1095	Variable transf_var: V → res W.
1096	Variable p: program A V.
1097	Variable p': program B W.
1098	Hypothesis transf_OK:
1099	transform_partial_program2 transf_fun transf_var p = OK ? p'.
1100
1101	Remark 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'.
1106	Proof.
1107	apply transform_partial_program2_match; auto.
1108	Qed.
1109
1110	Theorem 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'.
1115	Proof.
1116	intros.
1117	exploit find_funct_ptr_match. eexact prog_match. eauto.
1118	intros [tf [X Y]]. exists tf; auto.
1119	Qed.
1120
1121	Theorem 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.
1125	Proof.
1126	intros.
1127	exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1128	Qed.
1129
1130	Theorem 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'.
1135	Proof.
1136	intros.
1137	exploit find_funct_match. eexact prog_match. eauto.
1138	intros [tf [X Y]]. exists tf; auto.
1139	Qed.
1140
1141	Theorem 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.
1145	Proof.
1146	intros.
1147	exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1148	Qed.
1149
1150	Theorem find_symbol_transf_partial2:
1151	forall (s: ident),
1152	find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1153	Proof.
1154	intros. eapply find_symbol_match. eexact prog_match.
1155	Qed.
1156
1157	Theorem init_mem_transf_partial2:
1158	init_mem p' = init_mem p.
1159	Proof.
1160	intros. eapply init_mem_match. eexact prog_match.
1161	Qed.
1162
1163	End TRANSF_PROGRAM_PARTIAL2.
1164
1165	Section TRANSF_PROGRAM_PARTIAL.
1166
1167	Variable A B V: Type.
1168	Variable transf: A → res B.
1169	Variable p: program A V.
1170	Variable p': program B V.
1171	Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1172
1173	Remark transf2_OK:
1174	transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1175	Proof.
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.
1179	Qed.
1180
1181	Theorem 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'.
1186	Proof.
1187	exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1188	Qed.
1189
1190	Theorem 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.
1194	Proof.
1195	exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1196	Qed.
1197
1198	Theorem 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'.
1203	Proof.
1204	exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1205	Qed.
1206
1207	Theorem 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.
1211	Proof.
1212	exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1213	Qed.
1214
1215	Theorem find_symbol_transf_partial:
1216	forall (s: ident),
1217	find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1218	Proof.
1219	exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1220	Qed.
1221
1222	Theorem init_mem_transf_partial:
1223	init_mem p' = init_mem p.
1224	Proof.
1225	exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1226	Qed.
1227
1228	End TRANSF_PROGRAM_PARTIAL.
1229
1230	Section TRANSF_PROGRAM.
1231
1232	Variable A B V: Type.
1233	Variable transf: A → B.
1234	Variable p: program A V.
1235	Let tp := transform_program transf p.
1236
1237	Remark transf_OK:
1238	transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1239	Proof.
1240	unfold tp, transform_program, transform_partial_program.
1241	rewrite map_partial_total. reflexivity.
1242	Qed.
1243
1244	Theorem 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).
1248	Proof.
1249	intros.
1250	destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1251	as [f' [X Y]]. congruence.
1252	Qed.
1253
1254	Theorem 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.
1258	Proof.
1259	intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1260	intros [f [X Y]]. exists f; split. auto. congruence.
1261	Qed.
1262
1263	Theorem 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).
1267	Proof.
1268	intros.
1269	destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1270	as [f' [X Y]]. congruence.
1271	Qed.
1272
1273	Theorem 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.
1277	Proof.
1278	intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1279	intros [f [X Y]]. exists f; split. auto. congruence.
1280	Qed.
1281
1282	Theorem find_symbol_transf:
1283	forall (s: ident),
1284	find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1285	Proof.
1286	exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1287	Qed.
1288
1289	Theorem init_mem_transf:
1290	init_mem tp = init_mem p.
1291	Proof.
1292	exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1293	Qed.
1294
1295	End TRANSF_PROGRAM.
1296
1297	End Genv.
1298	*)

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format