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 | *) |
---|