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