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 "common/Errors.ma". |
---|
37 | include "common/AST.ma". |
---|
38 | (*include "Values.ma".*) |
---|
39 | include "common/FrontEndMem.ma". |
---|
40 | |
---|
41 | (* * The type of global environments. The parameter [F] is the type |
---|
42 | of function descriptions. *) |
---|
43 | (* Functions are given negative block numbers *) |
---|
44 | record genv_t (F:Type[0]) : Type[0] ≝ { |
---|
45 | functions: positive_map F; |
---|
46 | nextfunction: Pos; |
---|
47 | symbols: identifier_map SymbolTag block |
---|
48 | }. |
---|
49 | |
---|
50 | definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝ |
---|
51 | λF,name_fun,g. |
---|
52 | let blk_id ≝ nextfunction ? g in |
---|
53 | let b ≝ mk_block Code (neg blk_id) in |
---|
54 | mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g)) |
---|
55 | (succ blk_id) |
---|
56 | (add ?? (symbols … g) (\fst name_fun) b). |
---|
57 | |
---|
58 | definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝ |
---|
59 | λF,name,b,g. |
---|
60 | mk_genv_t F (functions … g) |
---|
61 | (nextfunction … g) |
---|
62 | (add ?? (symbols … g) name b). |
---|
63 | |
---|
64 | (* Construct environment and initial memory store *) |
---|
65 | definition empty_mem ≝ empty. (* XXX*) |
---|
66 | definition empty : ∀F. genv_t F ≝ |
---|
67 | λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??). |
---|
68 | |
---|
69 | definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝ |
---|
70 | λF,init,fns. |
---|
71 | foldr ?? (add_funct F) init fns. |
---|
72 | |
---|
73 | (* Return the address of the given global symbol, if any. *) |
---|
74 | definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝ |
---|
75 | λF,ge. lookup ?? (symbols … ge). |
---|
76 | |
---|
77 | (* init *) |
---|
78 | |
---|
79 | definition store_init_data : ∀F.genv_t F → mem → block → Z → init_data → option mem ≝ |
---|
80 | λF,ge,m,b,p,id. |
---|
81 | (* store checks that the address came from something capable of representing |
---|
82 | addresses of the memory region in question - here there are no real |
---|
83 | pointers, so use the real region. *) |
---|
84 | let ptr ≝ mk_pointer (block_region m b) b ? (mk_offset p) in |
---|
85 | match id with |
---|
86 | [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n) |
---|
87 | | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n) |
---|
88 | | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n) |
---|
89 | | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n) |
---|
90 | | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n) |
---|
91 | | Init_addrof r' symb ofs ⇒ |
---|
92 | match find_symbol … ge symb with |
---|
93 | [ None ⇒ None ? |
---|
94 | | Some b' ⇒ |
---|
95 | match pointer_compat_dec b' r' with |
---|
96 | [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))) |
---|
97 | | inr _ ⇒ None ? |
---|
98 | ] |
---|
99 | ] |
---|
100 | | Init_space n ⇒ Some ? m |
---|
101 | | Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r') |
---|
102 | ]. |
---|
103 | cases b // |
---|
104 | qed. |
---|
105 | |
---|
106 | definition size_init_data : init_data → nat ≝ |
---|
107 | λi_data.match i_data with |
---|
108 | [ Init_int8 _ ⇒ 1 |
---|
109 | | Init_int16 _ ⇒ 2 |
---|
110 | | Init_int32 _ ⇒ 4 |
---|
111 | | Init_float32 _ ⇒ 4 |
---|
112 | | Init_float64 _ ⇒ 8 |
---|
113 | | Init_space n ⇒ max n 0 |
---|
114 | | Init_null r ⇒ size_pointer r |
---|
115 | | Init_addrof r _ _ ⇒ size_pointer r]. |
---|
116 | |
---|
117 | let rec store_init_data_list (F:Type[0]) (ge:genv_t F) |
---|
118 | (m: mem) (b: block) (p: Z) (idl: list init_data) |
---|
119 | on idl : option mem ≝ |
---|
120 | match idl with |
---|
121 | [ nil ⇒ Some ? m |
---|
122 | | cons id idl' ⇒ |
---|
123 | match store_init_data F ge m b p id with |
---|
124 | [ None ⇒ None ? |
---|
125 | | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl' |
---|
126 | ] |
---|
127 | ]. |
---|
128 | |
---|
129 | definition size_init_data_list : list init_data → nat ≝ |
---|
130 | λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data. |
---|
131 | |
---|
132 | (* Nonessential properties that may require arithmetic |
---|
133 | nremark size_init_data_list_pos: |
---|
134 | ∀i_data. OZ ≤ size_init_data_list i_data. |
---|
135 | #i_data;elim i_data;//; |
---|
136 | #a;#tl;cut (OZ ≤ size_init_data a) |
---|
137 | ##[cases a;normalize;//; |
---|
138 | #x;cases x;normalize;//; |
---|
139 | ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl)); |
---|
140 | cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m) |
---|
141 | ##[cases (size_init_data a) in Hsize IH; |
---|
142 | ##[##1,2:/3/ |
---|
143 | ##|normalize;#n;#Hfalse;elim Hfalse] |
---|
144 | ##|#Hdisc;cases Hdisc |
---|
145 | ##[#Heq;nrewrite > Heq;//; |
---|
146 | ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2; |
---|
147 | (* TODO: arithmetics *) napply daemon] |
---|
148 | ##] |
---|
149 | ##] |
---|
150 | qed. |
---|
151 | *) |
---|
152 | |
---|
153 | |
---|
154 | (* init *) |
---|
155 | |
---|
156 | axiom InitDataStoreFailed : String. |
---|
157 | |
---|
158 | definition add_globals : ∀F,V:Type[0]. |
---|
159 | (V → (list init_data)) → |
---|
160 | genv_t F × mem → list (ident × region × V) → |
---|
161 | (genv_t F × mem) ≝ |
---|
162 | λF,V,extract_init,init_env,vars. |
---|
163 | foldl ?? |
---|
164 | (λg_st: genv_t F × mem. λid_init: ident × region × V. |
---|
165 | let 〈id, r, init_info〉 ≝ id_init in |
---|
166 | let init ≝ extract_init init_info in |
---|
167 | let 〈g,st〉 ≝ g_st in |
---|
168 | let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in |
---|
169 | let g' ≝ add_symbol ? id b g in |
---|
170 | 〈g', st'〉 |
---|
171 | ) |
---|
172 | init_env vars. |
---|
173 | |
---|
174 | definition init_globals : ∀F,V:Type[0]. |
---|
175 | (V → (list init_data)) → |
---|
176 | genv_t F → mem → list (ident × region × V) → |
---|
177 | res mem ≝ |
---|
178 | λF,V,extract_init,g,m,vars. |
---|
179 | foldl ?? |
---|
180 | (λst: res mem. λid_init: ident × region × V. |
---|
181 | let 〈id, r, init_info〉 ≝ id_init in |
---|
182 | let init ≝ extract_init init_info in |
---|
183 | do st ← st; |
---|
184 | match find_symbol … g id with |
---|
185 | [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init) |
---|
186 | | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *) |
---|
187 | ] ) |
---|
188 | (OK ? m) vars. |
---|
189 | |
---|
190 | definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv_t (F (prog_var_names … p)) × mem) ≝ |
---|
191 | λF,V,init_info,p. |
---|
192 | add_globals … init_info |
---|
193 | 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉 |
---|
194 | (prog_vars ?? p). |
---|
195 | |
---|
196 | (* Return the global environment for the given program. *) |
---|
197 | definition globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)) ≝ |
---|
198 | λF,V,i,p. |
---|
199 | \fst (globalenv_allocmem F V i p). |
---|
200 | |
---|
201 | (* Return the global environment for the given program with no data initialisation. *) |
---|
202 | definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝ |
---|
203 | λF,p. |
---|
204 | globalenv F nat (λn.[Init_space n]) p. |
---|
205 | |
---|
206 | (* Return the initial memory state for the given program. *) |
---|
207 | definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝ |
---|
208 | λF,V,i,p. |
---|
209 | let 〈g,m〉 ≝ globalenv_allocmem F V i p in |
---|
210 | init_globals ? V i g m (prog_vars ?? p). |
---|
211 | |
---|
212 | (* Setup memory when data initialisation is not required (has the benefit |
---|
213 | of being total. *) |
---|
214 | definition alloc_mem: ∀F. program F nat → mem ≝ |
---|
215 | λF,p. |
---|
216 | \snd (globalenv_allocmem F nat (λn. [Init_space n]) p). |
---|
217 | |
---|
218 | (* Return the function description associated with the given address, if any. *) |
---|
219 | definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝ |
---|
220 | λF,ge,b. match block_region b with [ Code ⇒ |
---|
221 | match block_id b with [ neg p ⇒ lookup_opt … p (functions … ge) |
---|
222 | | _ ⇒ None ? ] | _ ⇒ None ? ]. |
---|
223 | |
---|
224 | (* Same as [find_funct_ptr] but the function address is given as |
---|
225 | a value, which must be a pointer with offset 0. *) |
---|
226 | definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝ |
---|
227 | λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then find_funct_ptr … ge (pblock ptr) else None ? | _ ⇒ None ? ]. |
---|
228 | |
---|
229 | |
---|
230 | lemma find_funct_find_funct_ptr : ∀F,ge,v,f. |
---|
231 | find_funct F ge v = Some F f → |
---|
232 | ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset) ∧ find_funct_ptr F ge b = Some F f. |
---|
233 | #F #ge * |
---|
234 | [ #f #E normalize in E; destruct |
---|
235 | | #sz #i #f #E normalize in E; destruct |
---|
236 | | #f #fn #E normalize in E; destruct |
---|
237 | | #r #f #E normalize in E; destruct |
---|
238 | | * #pty #b #c * #off #f #E whd in E:(??%?); |
---|
239 | cases off in E ⊢ %; [ 2,3: #x ] |
---|
240 | #E whd in E:(??%?); destruct |
---|
241 | %{pty} %{b} %{c} % // @E |
---|
242 | ] qed. |
---|
243 | |
---|
244 | |
---|
245 | lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m. |
---|
246 | find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b. |
---|
247 | #F #V #init * * // * // #blk |
---|
248 | whd in ⊢ (? → ? → ? → ??%%); |
---|
249 | #vars elim vars |
---|
250 | [ #ge #m % |
---|
251 | | * * #id #r #v #tl #IH #ge #m |
---|
252 | whd in match (add_globals ?????); |
---|
253 | whd in ⊢ (??(???(??(???(????%?))))?); |
---|
254 | cases (alloc ????) #m' #b |
---|
255 | whd in ⊢ (??(???(??(???(????%?))))?); |
---|
256 | >IH cases ge #fnmap #nextblock #symmap |
---|
257 | whd in ⊢ (??(???%)?); |
---|
258 | % |
---|
259 | ] qed. |
---|
260 | |
---|
261 | lemma add_globals_match : ∀A,B,V,W,initV,initW. |
---|
262 | ∀P:(ident × region × V) → (ident × region × W) → Prop. |
---|
263 | (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
264 | ∀vars,ge,ge',m,vars'. |
---|
265 | symbols ? ge = symbols … ge' → |
---|
266 | All2 … P vars vars' → |
---|
267 | symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧ |
---|
268 | \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars'). |
---|
269 | #A #B #V #W #initV #initW #P #varsOK |
---|
270 | #vars elim vars |
---|
271 | [ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ] |
---|
272 | | * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ] |
---|
273 | * * #id' #r' #w #tl' #E * #p #TL |
---|
274 | whd in match (add_globals A ????); |
---|
275 | change with (add_globals A ????) in match (foldl ?????); |
---|
276 | whd in match (add_globals B ????); |
---|
277 | change with (add_globals B ????) in match (foldl (genv_t B × mem) ????); |
---|
278 | cases (varsOK … p) #E1 #E2 |
---|
279 | destruct >E2 cases (alloc ????) #m' #b |
---|
280 | @IH /2/ |
---|
281 | whd in match (add_symbol ????); |
---|
282 | whd in match (add_symbol ????); |
---|
283 | >E % |
---|
284 | ] qed. |
---|
285 | |
---|
286 | lemma pre_matching_fns_get_same_blocks : ∀A,B,P. |
---|
287 | (∀f,g. P f g → \fst f = \fst g) → |
---|
288 | ∀fns,fns'. |
---|
289 | All2 … P fns fns' → |
---|
290 | let ge ≝ add_functs A (empty ?) fns in |
---|
291 | let ge' ≝ add_functs B (empty ?) fns' in |
---|
292 | nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'. |
---|
293 | #A #B #P #fnOK #fns elim fns |
---|
294 | [ * [ #_ % % | #h #t * ] |
---|
295 | | * #id #f #tl #IH * [ * ] |
---|
296 | * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H |
---|
297 | whd in match (add_functs ???); |
---|
298 | change with (add_functs ???) in match (foldr ?????); |
---|
299 | whd in match (add_functs B ??); |
---|
300 | change with (add_functs ???) in match (foldr (ident × B) ????); |
---|
301 | cases (IH tl' H) #E1 #E2 |
---|
302 | % [ >E1 % | >E1 >E2 % ] |
---|
303 | ] qed. |
---|
304 | |
---|
305 | lemma matching_fns_get_same_blocks : ∀A,B,P. |
---|
306 | (∀f,g. P f g → \fst f = \fst g) → |
---|
307 | ∀fns,fns'. |
---|
308 | All2 … P fns fns' → |
---|
309 | let ge ≝ add_functs A (empty ?) fns in |
---|
310 | let ge' ≝ add_functs B (empty ?) fns' in |
---|
311 | symbols … ge = symbols … ge'. |
---|
312 | #A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK |
---|
313 | qed. |
---|
314 | |
---|
315 | (* |
---|
316 | (* * ** Properties of the operations. *) |
---|
317 | |
---|
318 | find_funct_inv: |
---|
319 | ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F. |
---|
320 | find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero; |
---|
321 | find_funct_find_funct_ptr: |
---|
322 | ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block. |
---|
323 | find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b; |
---|
324 | |
---|
325 | find_symbol_exists: |
---|
326 | ∀F,V: Type[0]. ∀p: program F V. |
---|
327 | ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V. |
---|
328 | in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) → |
---|
329 | ∃b. find_symbol ? (globalenv ?? p) id = Some ? b; |
---|
330 | find_funct_ptr_exists: |
---|
331 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F. |
---|
332 | list_norepet ? (prog_funct_names ?? p) → |
---|
333 | list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) → |
---|
334 | in_list ? 〈id, f〉 (prog_funct ?? p) → |
---|
335 | ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 |
---|
336 | ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f; |
---|
337 | |
---|
338 | find_funct_ptr_inversion: |
---|
339 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
340 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
341 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
342 | find_funct_inversion: |
---|
343 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
344 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
345 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
346 | find_funct_ptr_symbol_inversion: |
---|
347 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F. |
---|
348 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → |
---|
349 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
350 | in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
351 | |
---|
352 | find_funct_ptr_prop: |
---|
353 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
354 | (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → |
---|
355 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
356 | P f; |
---|
357 | find_funct_prop: |
---|
358 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
359 | (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → |
---|
360 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
361 | P f; |
---|
362 | |
---|
363 | initmem_nullptr: |
---|
364 | ∀F,V: Type[0]. ∀p: program F V. |
---|
365 | let m ≝ init_mem ?? p in |
---|
366 | valid_block m nullptr ∧ |
---|
367 | (blocks m) nullptr = empty_block 0 0 Any; |
---|
368 | (* initmem_inject_neutral: |
---|
369 | ∀F,V: Type[0]. ∀p: program F V. |
---|
370 | mem_inject_neutral (init_mem ?? p);*) |
---|
371 | find_funct_ptr_negative: |
---|
372 | ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F. |
---|
373 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0; |
---|
374 | find_symbol_not_fresh: |
---|
375 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. |
---|
376 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p); |
---|
377 | find_symbol_not_nullptr: |
---|
378 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. |
---|
379 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr; |
---|
380 | global_addresses_distinct: |
---|
381 | ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2. |
---|
382 | id1≠id2 → |
---|
383 | find_symbol ? (globalenv ?? p) id1 = Some ? b1 → |
---|
384 | find_symbol ? (globalenv ?? p) id2 = Some ? b2 → |
---|
385 | b1≠b2; |
---|
386 | |
---|
387 | (* * Commutation properties between program transformations |
---|
388 | and operations over global environments. *) |
---|
389 | |
---|
390 | find_funct_ptr_rev_transf: |
---|
391 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
392 | ∀b : block. ∀tf : B. |
---|
393 | find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf → |
---|
394 | ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf; |
---|
395 | find_funct_rev_transf: |
---|
396 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
397 | ∀v : val. ∀tf : B. |
---|
398 | find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → |
---|
399 | ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf; |
---|
400 | |
---|
401 | (* * Commutation properties between partial program transformations |
---|
402 | and operations over global environments. *) |
---|
403 | |
---|
404 | find_funct_ptr_transf_partial: |
---|
405 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
406 | transform_partial_program … transf p = OK ? p' → |
---|
407 | ∀b: block. ∀f: A. |
---|
408 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
409 | ∃f'. |
---|
410 | find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f'; |
---|
411 | find_funct_transf_partial: |
---|
412 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
413 | transform_partial_program … transf p = OK ? p' → |
---|
414 | ∀v: val. ∀f: A. |
---|
415 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
416 | ∃f'. |
---|
417 | find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f'; |
---|
418 | find_symbol_transf_partial: |
---|
419 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
420 | transform_partial_program … transf p = OK ? p' → |
---|
421 | ∀s: ident. |
---|
422 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
423 | init_mem_transf_partial: |
---|
424 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
425 | transform_partial_program … transf p = OK ? p' → |
---|
426 | init_mem ?? p' = init_mem ?? p; |
---|
427 | find_funct_ptr_rev_transf_partial: |
---|
428 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
429 | transform_partial_program … transf p = OK ? p' → |
---|
430 | ∀b : block. ∀tf : B. |
---|
431 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
432 | ∃f : A. |
---|
433 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf; |
---|
434 | find_funct_rev_transf_partial: |
---|
435 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
436 | transform_partial_program … transf p = OK ? p' → |
---|
437 | ∀v : val. ∀tf : B. |
---|
438 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
439 | ∃f : A. |
---|
440 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*; |
---|
441 | |
---|
442 | find_funct_ptr_transf_partial2: |
---|
443 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
444 | ∀p: program A V. ∀p': program B W. |
---|
445 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
446 | ∀b: block. ∀f: A. |
---|
447 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
448 | ∃f'. |
---|
449 | find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f'; |
---|
450 | find_funct_transf_partial2: |
---|
451 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
452 | ∀p: program A V. ∀p': program B W. |
---|
453 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
454 | ∀v: val. ∀f: A. |
---|
455 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
456 | ∃f'. |
---|
457 | find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f'; |
---|
458 | find_symbol_transf_partial2: |
---|
459 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
460 | ∀p: program A V. ∀p': program B W. |
---|
461 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
462 | ∀s: ident. |
---|
463 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
464 | init_mem_transf_partial2: |
---|
465 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
466 | ∀p: program A V. ∀p': program B W. |
---|
467 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
468 | init_mem ?? p' = init_mem ?? p; |
---|
469 | find_funct_ptr_rev_transf_partial2: |
---|
470 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
471 | ∀p: program A V. ∀p': program B W. |
---|
472 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
473 | ∀b: block. ∀tf: B. |
---|
474 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
475 | ∃f : A. |
---|
476 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf; |
---|
477 | find_funct_rev_transf_partial2: |
---|
478 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
479 | ∀p: program A V. ∀p': program B W. |
---|
480 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
481 | ∀v: val. ∀tf: B. |
---|
482 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
483 | ∃f : A. |
---|
484 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ; |
---|
485 | |
---|
486 | (* * Commutation properties between matching between programs |
---|
487 | and operations over global environments. *) |
---|
488 | *) *) |
---|
489 | |
---|
490 | (* First, show that nextfunction only depends on the number of functions: *) |
---|
491 | |
---|
492 | let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝ |
---|
493 | match n with |
---|
494 | [ O ⇒ p |
---|
495 | | S m ⇒ succ (nat_plus_pos m p) |
---|
496 | ]. |
---|
497 | |
---|
498 | lemma nextfunction_length : ∀A,l,ge. |
---|
499 | nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge). |
---|
500 | #A #l elim l // #h #t #IH #ge |
---|
501 | whd in ⊢ (??%%); >IH // |
---|
502 | qed. |
---|
503 | |
---|
504 | (* Now link functions in related programs, but without dealing with the type |
---|
505 | casts yet. *) |
---|
506 | |
---|
507 | lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P. |
---|
508 | find_funct_ptr … (globalenv A V initV p) b = Some ? f → |
---|
509 | All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') → |
---|
510 | ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'. |
---|
511 | #A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P |
---|
512 | cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ] |
---|
513 | [ 12: | *: #F whd in F:(??%?); destruct ] |
---|
514 | >vars_irrelevant_to_find_funct_ptr |
---|
515 | >vars_irrelevant_to_find_funct_ptr |
---|
516 | letin varnames ≝ (map ??? vars) |
---|
517 | cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?) |
---|
518 | // |
---|
519 | cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?)) |
---|
520 | // |
---|
521 | generalize in match (empty ?); |
---|
522 | generalize in match (empty ?); |
---|
523 | generalize in match fns'; |
---|
524 | elim fns |
---|
525 | [ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct |
---|
526 | | * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?); |
---|
527 | whd in match (functions ??); |
---|
528 | change with (add_functs ???) in match (foldr ?????); |
---|
529 | cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl))) |
---|
530 | [ #E destruct >lookup_opt_insert_hit #E destruct |
---|
531 | cases fns' [ * ] |
---|
532 | * #id' #fn' #tl' * #M #Mtl |
---|
533 | %{fn'} % // whd in ⊢ (??%?); |
---|
534 | whd in match (functions ??); |
---|
535 | change with (add_functs ???) in match (foldr ???? tl'); |
---|
536 | >nextfunction_length >nextfunction_length <NF >(All2_length … Mtl) |
---|
537 | >lookup_opt_insert_hit @refl |
---|
538 | | #NE >lookup_opt_insert_miss // |
---|
539 | #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl |
---|
540 | cases (IH ?????? Mtl) |
---|
541 | [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ] |
---|
542 | | skip |
---|
543 | | 4: @NF |
---|
544 | | skip |
---|
545 | | // |
---|
546 | | @FFP |
---|
547 | ] |
---|
548 | ] |
---|
549 | ] qed. |
---|
550 | |
---|
551 | discriminator Prod. |
---|
552 | |
---|
553 | (* Now prove the full version. *) |
---|
554 | |
---|
555 | lemma find_funct_ptr_match: |
---|
556 | ∀M:matching.∀initV,initW. |
---|
557 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
558 | ∀MATCH:match_program … M p p'. |
---|
559 | ∀b: block. ∀f: m_A M (prog_var_names … p). |
---|
560 | find_funct_ptr … (globalenv … initV p) b = Some ? f → |
---|
561 | ∃tf : m_B M (prog_var_names … p'). |
---|
562 | find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). |
---|
563 | [ 2: >(matching_vars … (mp_vars … MATCH)) % ] |
---|
564 | * #A #B #V #W #match_fn #match_var #initV #initW |
---|
565 | #p #p' * #Mvars #Mfn #Mmain |
---|
566 | #b #f #FFP |
---|
567 | @(find_funct_ptr_All2 A B V W ??????? FFP) |
---|
568 | lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars) |
---|
569 | #E |
---|
570 | @(All2_mp … Mfn) |
---|
571 | * #id #f * #id' #f' |
---|
572 | <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E |
---|
573 | normalize #H @(match_funct_entry_inv … H) // |
---|
574 | qed. |
---|
575 | |
---|
576 | lemma |
---|
577 | find_funct_ptr_transf_partial2: |
---|
578 | ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W. |
---|
579 | ∀p: program A V. ∀p': program B W. |
---|
580 | transform_partial_program2 … p transf_fun transf_var = OK ? p' → |
---|
581 | ∀b: block. ∀f: A ?. |
---|
582 | find_funct_ptr ? (globalenv … iV p) b = Some ? f → |
---|
583 | ∃f'. |
---|
584 | find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'. |
---|
585 | #A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP |
---|
586 | cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP) |
---|
587 | [2: @iW |
---|
588 | | #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E |
---|
589 | #TF %{f'} % // |
---|
590 | -FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' % |
---|
591 | qed. |
---|
592 | |
---|
593 | lemma match_funct_entry_id : ∀M,vs,vs',f,g. |
---|
594 | match_funct_entry M vs vs' f g → \fst f = \fst g. |
---|
595 | #M #vs #vs' #f #g * // |
---|
596 | qed. |
---|
597 | |
---|
598 | lemma |
---|
599 | find_symbol_match: |
---|
600 | ∀M:matching. |
---|
601 | ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
602 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
603 | match_program … M p p' → |
---|
604 | ∀s: ident. |
---|
605 | find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s. |
---|
606 | * #A #B #V #W #match_fun #match_var #initV #initW #initsize |
---|
607 | * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s |
---|
608 | whd in ⊢ (??%%); |
---|
609 | @sym_eq |
---|
610 | @(eq_f ??(λx. lookup SymbolTag block x s)) |
---|
611 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
612 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
613 | change with (add_globals ?????) in match (foldl ?????); |
---|
614 | change with (add_globals ?????) in match (foldl ? (ident×region×V) ???); |
---|
615 | @(proj1 … (add_globals_match … Mvars)) |
---|
616 | [ @(matching_fns_get_same_blocks … Mfns) |
---|
617 | #f #g @match_funct_entry_id |
---|
618 | | * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ] |
---|
619 | ] qed. |
---|
620 | |
---|
621 | lemma |
---|
622 | find_symbol_transf_partial2: |
---|
623 | ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W. |
---|
624 | (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) → |
---|
625 | ∀p: program A V. ∀p': program B W. |
---|
626 | transform_partial_program2 … p transf_fun transf_var = OK ? p' → |
---|
627 | ∀s: ident. |
---|
628 | find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s. |
---|
629 | #A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s |
---|
630 | @(find_symbol_match … (transform_partial_program2_match … TPP2)) |
---|
631 | #v0 #w0 * #id #r #v #w @sizeOK |
---|
632 | qed. |
---|
633 | |
---|
634 | lemma |
---|
635 | find_funct_ptr_transf: |
---|
636 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
637 | ∀b: block. ∀f: A ?. |
---|
638 | find_funct_ptr ? (globalenv … iV p) b = Some ? f → |
---|
639 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f). |
---|
640 | #A #B #V #iV * #vars #fns #main #tf #b #f #FFP |
---|
641 | cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP) |
---|
642 | [ 2: @iV |
---|
643 | | #f' * #FFP' |
---|
644 | whd in ⊢ (???(match % with [_⇒?]) → ?); (* XXX this line only required to workaround unification bug *) |
---|
645 | generalize in match (matching_vars ????); |
---|
646 | whd in match (prog_var_names ???); whd in match (prog_vars ???); |
---|
647 | #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' % |
---|
648 | ] qed. |
---|
649 | |
---|
650 | lemma |
---|
651 | find_funct_transf: |
---|
652 | ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. |
---|
653 | ∀v: val. ∀f: A ?. |
---|
654 | find_funct ? (globalenv … iV p) v = Some ? f → |
---|
655 | find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f). |
---|
656 | #A #B #V #iV #tf #p #v #f #FF |
---|
657 | cases (find_funct_find_funct_ptr ???? FF) |
---|
658 | #r * #b * #pc * #E destruct #FFP |
---|
659 | change with (find_funct_ptr ???) in ⊢ (??%?); |
---|
660 | @(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *) |
---|
661 | qed. |
---|
662 | |
---|
663 | lemma |
---|
664 | find_symbol_transf: |
---|
665 | ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. |
---|
666 | ∀s: ident. |
---|
667 | find_symbol ? (globalenv … iV (transform_program … p transf)) s = |
---|
668 | find_symbol ? (globalenv … iV p) s. |
---|
669 | #A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?)) |
---|
670 | #v0 #w0 * // |
---|
671 | qed. |
---|
672 | |
---|
673 | lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d. |
---|
674 | symbols A ge = symbols … ge' → |
---|
675 | store_init_data A ge m b o d = store_init_data B ge' m b o d. |
---|
676 | #A #B #ge #ge' #m #b #o #d #SYM |
---|
677 | whd in ⊢ (??%%); |
---|
678 | cases d #d' try @refl |
---|
679 | #id #n whd in ⊢ (??%%); |
---|
680 | whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl |
---|
681 | qed. |
---|
682 | |
---|
683 | lemma store_init_data_list_symbols : ∀A,B,ge,ge',b. |
---|
684 | symbols A ge = symbols … ge' → |
---|
685 | ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d. |
---|
686 | #A #B #ge #ge' #b #SYM #d elim d |
---|
687 | [ // |
---|
688 | | #hd #tl #IH #m #o |
---|
689 | whd in ⊢ (??%%); |
---|
690 | >(store_init_data_symbols … SYM) |
---|
691 | cases (store_init_data ??????) |
---|
692 | [ % |
---|
693 | | #m' @IH |
---|
694 | ] |
---|
695 | ] qed. |
---|
696 | |
---|
697 | lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop. |
---|
698 | ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) → |
---|
699 | ∀ge:genv_t A. ∀ge':genv_t B. |
---|
700 | symbols … ge = symbols … ge' → |
---|
701 | ∀m. ∀vars,vars'. |
---|
702 | All2 … P vars vars' → |
---|
703 | init_globals A V iV ge m vars = init_globals B W iW ge' m vars'. |
---|
704 | #A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars |
---|
705 | whd in ⊢ (? → ? → ??%%); |
---|
706 | generalize in match (OK ? m); |
---|
707 | elim vars |
---|
708 | [ #rm * |
---|
709 | [ #_ % |
---|
710 | | #h #t * |
---|
711 | ] |
---|
712 | | * #idr #v #tl #IH #rm |
---|
713 | * [ * ] |
---|
714 | * #idr' #w #tl' |
---|
715 | * #p cases (varsOK … p) #E1 #E2 destruct #TL |
---|
716 | whd in ⊢ (??%%); cases idr' #id #r cases rm #m' |
---|
717 | whd in ⊢ (??(????%?)(????%?)); |
---|
718 | [ whd in match (find_symbol ?? id); |
---|
719 | whd in match (find_symbol B ? id); |
---|
720 | >SYM cases (lookup ??? id) |
---|
721 | [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ] |
---|
722 | ] @IH // |
---|
723 | ] qed. |
---|
724 | |
---|
725 | lemma |
---|
726 | init_mem_match: |
---|
727 | ∀M:matching. |
---|
728 | ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) → |
---|
729 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
730 | match_program … M p p' → |
---|
731 | init_mem … iW p' = init_mem … iV p. |
---|
732 | * #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain |
---|
733 | whd in ⊢ (??%%); |
---|
734 | change with (add_globals ?????) in match (globalenv_allocmem ??? p'); |
---|
735 | change with (add_globals ?????) in match (globalenv_allocmem ??? p); |
---|
736 | cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars) |
---|
737 | [ 8: @(matching_fns_get_same_blocks … Mfns) |
---|
738 | #f0 #g0 * // |
---|
739 | | cases (add_globals ?????) #ge1 #m1 |
---|
740 | cases (add_globals ?????) #ge2 #m2 |
---|
741 | #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars) |
---|
742 | [ #v0 #w0 * #id #r #v #w /3/ |
---|
743 | | @SYM |
---|
744 | ] |
---|
745 | | 4: #v0 #w0 * #id #r #v #w #V % // >iSAME // |
---|
746 | | *: skip |
---|
747 | ] qed. |
---|
748 | |
---|
749 | lemma |
---|
750 | init_mem_transf: |
---|
751 | ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. |
---|
752 | init_mem … iV (transform_program … p transf) = init_mem … iV p. |
---|
753 | #A #B #C #iV #transf #p |
---|
754 | @(init_mem_match … (transform_program_match … transf ?)) |
---|
755 | // |
---|
756 | qed. |
---|
757 | |
---|
758 | |
---|
759 | (* Package up transform_program results for global envs nicely. *) |
---|
760 | |
---|
761 | record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ { |
---|
762 | rg_find_symbol: ∀s. |
---|
763 | find_symbol … ge s = find_symbol … ge' s; |
---|
764 | rg_find_funct: ∀v,f. |
---|
765 | find_funct … ge v = Some ? f → |
---|
766 | find_funct … ge' v = Some ? (t f); |
---|
767 | rg_find_funct_ptr: ∀b,f. |
---|
768 | find_funct_ptr … ge b = Some ? f → |
---|
769 | find_funct_ptr … ge' b = Some ? (t f) |
---|
770 | }. |
---|
771 | |
---|
772 | theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs. |
---|
773 | related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)). |
---|
774 | #A #B #V #iV #p #tf % |
---|
775 | [ #s @sym_eq @(find_symbol_transf A B V iV tf p) |
---|
776 | | @(find_funct_transf A B V iV tf p) |
---|
777 | | @(find_funct_ptr_transf A B V iV p tf) |
---|
778 | ] qed. |
---|
779 | |
---|
780 | |
---|
781 | (* |
---|
782 | |
---|
783 | find_funct_ptr_match: |
---|
784 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
785 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
786 | match_program … match_fun match_var p p' → |
---|
787 | ∀b: block. ∀f: A. |
---|
788 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
789 | ∃tf : B. |
---|
790 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf; |
---|
791 | find_funct_ptr_rev_match: |
---|
792 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
793 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
794 | match_program … match_fun match_var p p' → |
---|
795 | ∀b: block. ∀tf: B. |
---|
796 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
797 | ∃f : A. |
---|
798 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf; |
---|
799 | find_funct_match: |
---|
800 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
801 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
802 | match_program … match_fun match_var p p' → |
---|
803 | ∀v: val. ∀f: A. |
---|
804 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
805 | ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf; |
---|
806 | find_funct_rev_match: |
---|
807 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
808 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
809 | match_program … match_fun match_var p p' → |
---|
810 | ∀v: val. ∀tf: B. |
---|
811 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
812 | ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf; |
---|
813 | find_symbol_match: |
---|
814 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
815 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
816 | match_program … match_fun match_var p p' → |
---|
817 | ∀s: ident. |
---|
818 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
819 | *) |
---|
820 | (* |
---|
821 | Definition find_funct_ptr ? (g: genv) (b: block) : option F := |
---|
822 | ZMap.get b g.(functions). |
---|
823 | |
---|
824 | Definition find_funct (g: genv) (v: val) : option F := |
---|
825 | match v with |
---|
826 | | Vptr b ofs => |
---|
827 | if Int.eq ofs Int.zero then find_funct_ptr ? g b else None |
---|
828 | | _ => |
---|
829 | None |
---|
830 | end. |
---|
831 | |
---|
832 | Definition find_symbol ? (g: genv) (symb: ident) : option block := |
---|
833 | PTree.get symb g.(symbols). |
---|
834 | |
---|
835 | Lemma find_funct_inv: |
---|
836 | forall (ge: t) (v: val) (f: F), |
---|
837 | find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero. |
---|
838 | Proof. |
---|
839 | intros until f. unfold find_funct. destruct v; try (intros; discriminate). |
---|
840 | generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros. |
---|
841 | exists b. congruence. |
---|
842 | discriminate. |
---|
843 | Qed. |
---|
844 | |
---|
845 | Lemma find_funct_find_funct_ptr: |
---|
846 | forall (ge: t) (b: block), |
---|
847 | find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. |
---|
848 | Proof. |
---|
849 | intros. simpl. |
---|
850 | generalize (Int.eq_spec Int.zero Int.zero). |
---|
851 | case (Int.eq Int.zero Int.zero); intros. |
---|
852 | auto. tauto. |
---|
853 | Qed. |
---|
854 | *) |
---|
855 | |
---|
856 | (* |
---|
857 | ##[ #A B C transf p b f; elim p; #fns main vars; |
---|
858 | elim fns; |
---|
859 | ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct; |
---|
860 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?); |
---|
861 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
862 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
863 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
864 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
865 | ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH; |
---|
866 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
867 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?); |
---|
868 | ##[ #H; destruct (H); //; |
---|
869 | ##| #H; napply IH; napply H; |
---|
870 | ##] |
---|
871 | ##] |
---|
872 | ##] |
---|
873 | ##] |
---|
874 | ##| #A B C transf p v f; elim v; |
---|
875 | ##[ whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
876 | ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
877 | ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero); |
---|
878 | whd in ⊢ (??%? → ??%?); |
---|
879 | ##[ elim p; #fns main vars; elim fns; |
---|
880 | ##[ whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
881 | ##| #h t; elim h; #f fn IH; |
---|
882 | whd in ⊢ (??%? → ??%?); |
---|
883 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
884 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
885 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
886 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
887 | ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH; |
---|
888 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
889 | ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H; |
---|
890 | ##[ destruct (H); //; |
---|
891 | ##| napply IH; napply H; |
---|
892 | ##] |
---|
893 | ##] |
---|
894 | ##] |
---|
895 | ##] |
---|
896 | ##| #H; destruct; |
---|
897 | ##] |
---|
898 | ##] |
---|
899 | ##| #A B C transf p id; elim p; #fns main vars; |
---|
900 | elim fns; |
---|
901 | ##[ normalize; // |
---|
902 | ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH; |
---|
903 | elim (ident_eq fid id); #e; |
---|
904 | ##[ whd in ⊢ (??%%); |
---|
905 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
906 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
907 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
908 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
909 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
910 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
911 | ##| // |
---|
912 | ##] |
---|
913 | ##] |
---|
914 | ##| whd in ⊢ (??%%); nrewrite > IH; napply refl; |
---|
915 | ##] |
---|
916 | ##] |
---|
917 | ##| //; |
---|
918 | ##| #A B C transf p b tf; elim p; #fns main vars; |
---|
919 | elim fns; |
---|
920 | ##[ normalize; #H; destruct; |
---|
921 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
922 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
923 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
924 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
925 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
926 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
927 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
928 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
929 | ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; |
---|
930 | ##| #H; napply IH; napply H; |
---|
931 | ##] |
---|
932 | ##] |
---|
933 | ##] |
---|
934 | ##] |
---|
935 | ##| #A B C transf p v tf; elim p; #fns main vars; elim v; |
---|
936 | ##[ normalize; #H; destruct; |
---|
937 | ##| ##2,3: #x; normalize; #H; destruct; |
---|
938 | ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero); |
---|
939 | ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
940 | elim fns; |
---|
941 | ##[ normalize; #H; destruct; |
---|
942 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
943 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
944 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
945 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
946 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
947 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
948 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
949 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
950 | ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; |
---|
951 | ##| #H; napply IH; napply H; |
---|
952 | ##] |
---|
953 | ##] |
---|
954 | ##] |
---|
955 | ##] |
---|
956 | ##| normalize; #H; destruct; |
---|
957 | ##] |
---|
958 | ##] |
---|
959 | ##] qed. |
---|
960 | |
---|
961 | |
---|
962 | Lemma functions_globalenv: |
---|
963 | forall (p: program F V), |
---|
964 | functions (globalenv p) = functions (add_functs empty p.(prog_funct)). |
---|
965 | Proof. |
---|
966 | assert (forall init vars, |
---|
967 | functions (fst (add_globals init vars)) = functions (fst init)). |
---|
968 | induction vars; simpl. |
---|
969 | reflexivity. |
---|
970 | destruct a as [[id1 init1] info1]. destruct (add_globals init vars). |
---|
971 | simpl. exact IHvars. |
---|
972 | |
---|
973 | unfold add_globals; simpl. |
---|
974 | intros. unfold globalenv; unfold globalenv_initmem. |
---|
975 | rewrite H. reflexivity. |
---|
976 | Qed. |
---|
977 | |
---|
978 | Lemma initmem_nullptr: |
---|
979 | forall (p: program F V), |
---|
980 | let m := init_mem p in |
---|
981 | valid_block m nullptr /\ |
---|
982 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef). |
---|
983 | Proof. |
---|
984 | pose (P := fun m => valid_block m nullptr /\ |
---|
985 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)). |
---|
986 | assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))). |
---|
987 | induction vars; simpl; intros. |
---|
988 | auto. |
---|
989 | destruct a as [[id1 in1] inf1]. |
---|
990 | destruct (add_globals init vars) as [g st]. |
---|
991 | simpl in *. destruct IHvars. split. |
---|
992 | red; simpl. red in H0. omega. |
---|
993 | simpl. rewrite update_o. auto. unfold block. red in H0. omega. |
---|
994 | |
---|
995 | intro. unfold init_mem, globalenv_initmem. apply H. |
---|
996 | red; simpl. split. compute. auto. reflexivity. |
---|
997 | Qed. |
---|
998 | |
---|
999 | Lemma initmem_inject_neutral: |
---|
1000 | forall (p: program F V), |
---|
1001 | mem_inject_neutral (init_mem p). |
---|
1002 | Proof. |
---|
1003 | assert (forall g0 vars g1 m, |
---|
1004 | add_globals (g0, Mem.empty) vars = (g1, m) → |
---|
1005 | mem_inject_neutral m). |
---|
1006 | Opaque alloc_init_data. |
---|
1007 | induction vars; simpl. |
---|
1008 | intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H). |
---|
1009 | simpl in H1. rewrite Mem.getN_init in H1. |
---|
1010 | replace v with Vundef. auto. destruct chunk; simpl in H1; auto. |
---|
1011 | destruct a as [[id1 init1] info1]. |
---|
1012 | caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. |
---|
1013 | caseEq (alloc_init_data m1 init1). intros m2 b ALLOC. |
---|
1014 | intros. inv H. |
---|
1015 | eapply Mem.alloc_init_data_neutral; eauto. |
---|
1016 | intros. caseEq (globalenv_initmem p). intros g m EQ. |
---|
1017 | unfold init_mem; rewrite EQ; simpl. |
---|
1018 | unfold globalenv_initmem in EQ. eauto. |
---|
1019 | Qed. |
---|
1020 | |
---|
1021 | Remark nextfunction_add_functs_neg: |
---|
1022 | forall fns, nextfunction (add_functs empty fns) < 0. |
---|
1023 | Proof. |
---|
1024 | induction fns; simpl; intros. omega. unfold Zpred. omega. |
---|
1025 | Qed. |
---|
1026 | |
---|
1027 | Theorem find_funct_ptr_negative: |
---|
1028 | forall (p: program F V) (b: block) (f: F), |
---|
1029 | find_funct_ptr ? (globalenv p) b = Some ? f → b < 0. |
---|
1030 | Proof. |
---|
1031 | intros until f. |
---|
1032 | assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0). |
---|
1033 | induction fns; simpl. |
---|
1034 | rewrite ZMap.gi. congruence. |
---|
1035 | rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro. |
---|
1036 | intro. rewrite e. apply nextfunction_add_functs_neg. |
---|
1037 | auto. |
---|
1038 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
1039 | intros. eauto. |
---|
1040 | Qed. |
---|
1041 | |
---|
1042 | Remark find_symbol_add_functs_negative: |
---|
1043 | forall (fns: list (ident * F)) s b, |
---|
1044 | (symbols (add_functs empty fns)) ! s = Some ? b → b < 0. |
---|
1045 | Proof. |
---|
1046 | induction fns; simpl; intros until b. |
---|
1047 | rewrite PTree.gempty. congruence. |
---|
1048 | rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro. |
---|
1049 | intro EQ; inversion EQ. apply nextfunction_add_functs_neg. |
---|
1050 | eauto. |
---|
1051 | Qed. |
---|
1052 | |
---|
1053 | Remark find_symbol_add_symbols_not_fresh: |
---|
1054 | forall fns vars g m s b, |
---|
1055 | add_globals (add_functs empty fns, Mem.empty) vars = (g, m) → |
---|
1056 | (symbols g)!s = Some ? b → |
---|
1057 | b < nextblock m. |
---|
1058 | Proof. |
---|
1059 | induction vars; simpl; intros until b. |
---|
1060 | intros. inversion H. subst g m. simpl. |
---|
1061 | generalize (find_symbol_add_functs_negative fns s H0). omega. |
---|
1062 | Transparent alloc_init_data. |
---|
1063 | destruct a as [[id1 init1] info1]. |
---|
1064 | caseEq (add_globals (add_functs empty fns, Mem.empty) vars). |
---|
1065 | intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. |
---|
1066 | unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro. |
---|
1067 | intro EQ; inversion EQ. omega. |
---|
1068 | intro. generalize (IHvars _ _ _ _ ADG H). omega. |
---|
1069 | Qed. |
---|
1070 | |
---|
1071 | Theorem find_symbol_not_fresh: |
---|
1072 | forall (p: program F V) (id: ident) (b: block), |
---|
1073 | find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p). |
---|
1074 | Proof. |
---|
1075 | intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. |
---|
1076 | caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty) |
---|
1077 | (prog_vars p)); intros g m EQ. |
---|
1078 | simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto. |
---|
1079 | Qed. |
---|
1080 | |
---|
1081 | Lemma find_symbol_exists: |
---|
1082 | forall (p: program F V) |
---|
1083 | (id: ident) (init: list init_data) (v: V), |
---|
1084 | In (id, init, v) (prog_vars p) → |
---|
1085 | ∃b. find_symbol ? (globalenv p) id = Some ? b. |
---|
1086 | Proof. |
---|
1087 | intros until v. |
---|
1088 | assert (forall initm vl, In (id, init, v) vl → |
---|
1089 | ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b). |
---|
1090 | induction vl; simpl; intros. |
---|
1091 | elim H. |
---|
1092 | destruct a as [[id0 init0] v0]. |
---|
1093 | caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. |
---|
1094 | rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto. |
---|
1095 | elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. |
---|
1096 | intros. unfold globalenv, find_symbol, globalenv_initmem. auto. |
---|
1097 | Qed. |
---|
1098 | |
---|
1099 | Remark find_symbol_above_nextfunction: |
---|
1100 | forall (id: ident) (b: block) (fns: list (ident * F)), |
---|
1101 | let g := add_functs empty fns in |
---|
1102 | PTree.get id g.(symbols) = Some ? b → |
---|
1103 | b > g.(nextfunction). |
---|
1104 | Proof. |
---|
1105 | induction fns; simpl. |
---|
1106 | rewrite PTree.gempty. congruence. |
---|
1107 | rewrite PTree.gsspec. case (peq id (fst a)); intro. |
---|
1108 | intro EQ. inversion EQ. unfold Zpred. omega. |
---|
1109 | intros. generalize (IHfns H). unfold Zpred; omega. |
---|
1110 | Qed. |
---|
1111 | |
---|
1112 | Remark find_symbol_add_globals: |
---|
1113 | forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)), |
---|
1114 | ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) → |
---|
1115 | find_symbol ? (fst (add_globals ge_m vars)) id = |
---|
1116 | find_symbol ? (fst ge_m) id. |
---|
1117 | Proof. |
---|
1118 | unfold find_symbol; induction vars; simpl; intros. |
---|
1119 | auto. |
---|
1120 | destruct a as [[id0 init0] var0]. simpl in *. |
---|
1121 | caseEq (add_globals ge_m vars); intros ge' m' EQ. |
---|
1122 | simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. |
---|
1123 | apply IHvars. tauto. intuition congruence. |
---|
1124 | Qed. |
---|
1125 | |
---|
1126 | Lemma find_funct_ptr_exists: |
---|
1127 | forall (p: program F V) (id: ident) (f: F), |
---|
1128 | list_norepet (prog_funct_names p) → |
---|
1129 | list_disjoint (prog_funct_names p) (prog_var_names p) → |
---|
1130 | In (id, f) (prog_funct p) → |
---|
1131 | ∃b. find_symbol ? (globalenv p) id = Some ? b |
---|
1132 | /\ find_funct_ptr ? (globalenv p) b = Some ? f. |
---|
1133 | Proof. |
---|
1134 | intros until f. |
---|
1135 | assert (forall (fns: list (ident * F)), |
---|
1136 | list_norepet (map (@fst ident F) fns) → |
---|
1137 | In (id, f) fns → |
---|
1138 | ∃b. find_symbol ? (add_functs empty fns) id = Some ? b |
---|
1139 | /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f). |
---|
1140 | unfold find_symbol, find_funct_ptr. induction fns; intros. |
---|
1141 | elim H0. |
---|
1142 | destruct a as [id0 f0]; simpl in *. inv H. |
---|
1143 | unfold add_funct; simpl. |
---|
1144 | rewrite PTree.gsspec. destruct (peq id id0). |
---|
1145 | subst id0. econstructor; split. eauto. |
---|
1146 | replace f0 with f. apply ZMap.gss. |
---|
1147 | elim H0; intro. congruence. elim H3. |
---|
1148 | change id with (@fst ident F (id, f)). apply List.in_map. auto. |
---|
1149 | exploit IHfns; eauto. elim H0; intro. congruence. auto. |
---|
1150 | intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto. |
---|
1151 | generalize (find_symbol_above_nextfunction _ _ X). |
---|
1152 | unfold block; unfold ZIndexed.t; intro; omega. |
---|
1153 | |
---|
1154 | intros. exploit H; eauto. intros [b [X Y]]. |
---|
1155 | exists b; split. |
---|
1156 | unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. |
---|
1157 | assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. |
---|
1158 | unfold prog_funct_names. change id with (fst (id, f)). |
---|
1159 | apply List.in_map; auto. |
---|
1160 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
1161 | assumption. |
---|
1162 | Qed. |
---|
1163 | |
---|
1164 | Lemma find_funct_ptr_inversion: |
---|
1165 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
1166 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1167 | ∃id. In (id, f) (prog_funct p). |
---|
1168 | Proof. |
---|
1169 | intros until f. |
---|
1170 | assert (forall fns: list (ident * F), |
---|
1171 | find_funct_ptr ? (add_functs empty fns) b = Some ? f → |
---|
1172 | ∃id. In (id, f) fns). |
---|
1173 | unfold find_funct_ptr. induction fns; simpl. |
---|
1174 | rewrite ZMap.gi. congruence. |
---|
1175 | destruct a as [id0 f0]; simpl. |
---|
1176 | rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))). |
---|
1177 | intro. inv H. exists id0; auto. |
---|
1178 | intro. exploit IHfns; eauto. intros [id A]. exists id; auto. |
---|
1179 | unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto. |
---|
1180 | Qed. |
---|
1181 | |
---|
1182 | Lemma find_funct_ptr_prop: |
---|
1183 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
1184 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
1185 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1186 | P f. |
---|
1187 | Proof. |
---|
1188 | intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto. |
---|
1189 | Qed. |
---|
1190 | |
---|
1191 | Lemma find_funct_inversion: |
---|
1192 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
1193 | find_funct (globalenv p) v = Some ? f → |
---|
1194 | ∃id. In (id, f) (prog_funct p). |
---|
1195 | Proof. |
---|
1196 | intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H. |
---|
1197 | rewrite find_funct_find_funct_ptr ? in H. |
---|
1198 | eapply find_funct_ptr_inversion; eauto. |
---|
1199 | Qed. |
---|
1200 | |
---|
1201 | Lemma find_funct_prop: |
---|
1202 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
1203 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
1204 | find_funct (globalenv p) v = Some ? f → |
---|
1205 | P f. |
---|
1206 | Proof. |
---|
1207 | intros. exploit find_funct_inversion; eauto. intros [id A]. eauto. |
---|
1208 | Qed. |
---|
1209 | |
---|
1210 | Lemma find_funct_ptr_symbol_inversion: |
---|
1211 | forall (p: program F V) (id: ident) (b: block) (f: F), |
---|
1212 | find_symbol ? (globalenv p) id = Some ? b → |
---|
1213 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1214 | In (id, f) p.(prog_funct). |
---|
1215 | Proof. |
---|
1216 | intros until f. |
---|
1217 | assert (forall fns, |
---|
1218 | let g := add_functs empty fns in |
---|
1219 | PTree.get id g.(symbols) = Some ? b → |
---|
1220 | ZMap.get b g.(functions) = Some ? f → |
---|
1221 | In (id, f) fns). |
---|
1222 | induction fns; simpl. |
---|
1223 | rewrite ZMap.gi. congruence. |
---|
1224 | set (g := add_functs empty fns). |
---|
1225 | rewrite PTree.gsspec. rewrite ZMap.gsspec. |
---|
1226 | case (peq id (fst a)); intro. |
---|
1227 | intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. |
---|
1228 | intro EQ2. left. destruct a. simpl in *. congruence. |
---|
1229 | intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto. |
---|
1230 | generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega. |
---|
1231 | assert (forall g0 m0, b < 0 → |
---|
1232 | forall vars g m, |
---|
1233 | add_globals (g0, m0) vars = (g, m) → |
---|
1234 | PTree.get id g.(symbols) = Some ? b → |
---|
1235 | PTree.get id g0.(symbols) = Some ? b). |
---|
1236 | induction vars; simpl. |
---|
1237 | intros. inv H1. auto. |
---|
1238 | destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). |
---|
1239 | intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1. |
---|
1240 | unfold add_symbol; intros A B. rewrite <- B. simpl. |
---|
1241 | rewrite PTree.gsspec. case (peq id id1); intros. |
---|
1242 | assert (b > 0). inv H1. apply nextblock_pos. |
---|
1243 | omegaContradiction. |
---|
1244 | eauto. |
---|
1245 | intros. |
---|
1246 | generalize (find_funct_ptr_negative _ _ H2). intro. |
---|
1247 | pose (g := add_functs empty (prog_funct p)). |
---|
1248 | apply H. |
---|
1249 | apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). |
---|
1250 | auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. |
---|
1251 | reflexivity. assumption. rewrite <- functions_globalenv. assumption. |
---|
1252 | Qed. |
---|
1253 | |
---|
1254 | Theorem find_symbol_not_nullptr: |
---|
1255 | forall (p: program F V) (id: ident) (b: block), |
---|
1256 | find_symbol ? (globalenv p) id = Some ? b → b <> nullptr. |
---|
1257 | Proof. |
---|
1258 | intros until b. |
---|
1259 | assert (forall fns, |
---|
1260 | find_symbol ? (add_functs empty fns) id = Some ? b → |
---|
1261 | b <> nullptr). |
---|
1262 | unfold find_symbol; induction fns; simpl. |
---|
1263 | rewrite PTree.gempty. congruence. |
---|
1264 | destruct a as [id1 f1]. simpl. rewrite PTree.gsspec. |
---|
1265 | destruct (peq id id1); intros. |
---|
1266 | inversion H. generalize (nextfunction_add_functs_neg fns). |
---|
1267 | unfold block, nullptr; omega. |
---|
1268 | auto. |
---|
1269 | set (g0 := add_functs empty p.(prog_funct)). |
---|
1270 | assert (forall vars g m, |
---|
1271 | add_globals (g0, Mem.empty) vars = (g, m) → |
---|
1272 | find_symbol ? g id = Some ? b → |
---|
1273 | b <> nullptr). |
---|
1274 | induction vars; simpl; intros until m. |
---|
1275 | intros. inversion H0. subst g. apply H with (prog_funct p). auto. |
---|
1276 | destruct a as [[id1 init1] info1]. |
---|
1277 | caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2. |
---|
1278 | inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec. |
---|
1279 | destruct (peq id id1); intros. |
---|
1280 | inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega. |
---|
1281 | eauto. |
---|
1282 | intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto. |
---|
1283 | Qed. |
---|
1284 | |
---|
1285 | Theorem global_addresses_distinct: |
---|
1286 | forall (p: program F V) id1 id2 b1 b2, |
---|
1287 | id1<>id2 → |
---|
1288 | find_symbol ? (globalenv p) id1 = Some ? b1 → |
---|
1289 | find_symbol ? (globalenv p) id2 = Some ? b2 → |
---|
1290 | b1<>b2. |
---|
1291 | Proof. |
---|
1292 | intros. |
---|
1293 | assert (forall fns, |
---|
1294 | find_symbol ? (add_functs empty fns) id1 = Some ? b1 → |
---|
1295 | find_symbol ? (add_functs empty fns) id2 = Some ? b2 → |
---|
1296 | b1 <> b2). |
---|
1297 | unfold find_symbol. induction fns; simpl; intros. |
---|
1298 | rewrite PTree.gempty in H2. discriminate. |
---|
1299 | destruct a as [id f]; simpl in *. |
---|
1300 | rewrite PTree.gsspec in H2. |
---|
1301 | destruct (peq id1 id). subst id. inv H2. |
---|
1302 | rewrite PTree.gso in H3; auto. |
---|
1303 | generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega. |
---|
1304 | rewrite PTree.gsspec in H3. |
---|
1305 | destruct (peq id2 id). subst id. inv H3. |
---|
1306 | generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega. |
---|
1307 | eauto. |
---|
1308 | set (ge0 := add_functs empty p.(prog_funct)). |
---|
1309 | assert (forall (vars: list (ident * list init_data * V)) ge m, |
---|
1310 | add_globals (ge0, Mem.empty) vars = (ge, m) → |
---|
1311 | find_symbol ? ge id1 = Some ? b1 → |
---|
1312 | find_symbol ? ge id2 = Some ? b2 → |
---|
1313 | b1 <> b2). |
---|
1314 | unfold find_symbol. induction vars; simpl. |
---|
1315 | intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto. |
---|
1316 | intros ge m. destruct a as [[id init] info]. |
---|
1317 | caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B. |
---|
1318 | unfold add_symbol. simpl. intros. |
---|
1319 | rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3. |
---|
1320 | rewrite PTree.gso in H4; auto. |
---|
1321 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega. |
---|
1322 | rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4. |
---|
1323 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega. |
---|
1324 | eauto. |
---|
1325 | set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)). |
---|
1326 | apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m). |
---|
1327 | fold ge_m. apply surjective_pairing. auto. auto. |
---|
1328 | Qed. |
---|
1329 | |
---|
1330 | End GENV. |
---|
1331 | |
---|
1332 | (* Global environments and program transformations. *) |
---|
1333 | |
---|
1334 | Section MATCH_PROGRAM. |
---|
1335 | |
---|
1336 | Variable A B V W: Type. |
---|
1337 | Variable match_fun: A → B → Prop. |
---|
1338 | Variable match_var: V → W → Prop. |
---|
1339 | Variable p: program A V. |
---|
1340 | Variable p': program B W. |
---|
1341 | Hypothesis match_prog: |
---|
1342 | match_program match_fun match_var p p'. |
---|
1343 | |
---|
1344 | Lemma add_functs_match: |
---|
1345 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
1346 | list_forall2 (match_funct_etry match_fun) fns tfns → |
---|
1347 | let r := add_functs (empty A) fns in |
---|
1348 | let tr := add_functs (empty B) tfns in |
---|
1349 | nextfunction tr = nextfunction r /\ |
---|
1350 | symbols tr = symbols r /\ |
---|
1351 | forall (b: block) (f: A), |
---|
1352 | ZMap.get b (functions r) = Some ? f → |
---|
1353 | ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf. |
---|
1354 | Proof. |
---|
1355 | induction 1; simpl. |
---|
1356 | |
---|
1357 | split. reflexivity. split. reflexivity. |
---|
1358 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
1359 | |
---|
1360 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
1361 | simpl. red in H. destruct H. |
---|
1362 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
1363 | rewrite X. rewrite Y. |
---|
1364 | split. auto. |
---|
1365 | split. congruence. |
---|
1366 | intros b f. |
---|
1367 | repeat (rewrite ZMap.gsspec). |
---|
1368 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
1369 | intro EQ; inv EQ. exists fn2; auto. |
---|
1370 | auto. |
---|
1371 | Qed. |
---|
1372 | |
---|
1373 | Lemma add_functs_rev_match: |
---|
1374 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
1375 | list_forall2 (match_funct_etry match_fun) fns tfns → |
---|
1376 | let r := add_functs (empty A) fns in |
---|
1377 | let tr := add_functs (empty B) tfns in |
---|
1378 | nextfunction tr = nextfunction r /\ |
---|
1379 | symbols tr = symbols r /\ |
---|
1380 | forall (b: block) (tf: B), |
---|
1381 | ZMap.get b (functions tr) = Some ? tf → |
---|
1382 | ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf. |
---|
1383 | Proof. |
---|
1384 | induction 1; simpl. |
---|
1385 | |
---|
1386 | split. reflexivity. split. reflexivity. |
---|
1387 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
1388 | |
---|
1389 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
1390 | simpl. red in H. destruct H. |
---|
1391 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
1392 | rewrite X. rewrite Y. |
---|
1393 | split. auto. |
---|
1394 | split. congruence. |
---|
1395 | intros b f. |
---|
1396 | repeat (rewrite ZMap.gsspec). |
---|
1397 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
1398 | intro EQ; inv EQ. exists fn1; auto. |
---|
1399 | auto. |
---|
1400 | Qed. |
---|
1401 | |
---|
1402 | Lemma mem_add_globals_match: |
---|
1403 | forall (g1: genv A) (g2: genv B) (m: mem) |
---|
1404 | (vars: list (ident * list init_data * V)) |
---|
1405 | (tvars: list (ident * list init_data * W)), |
---|
1406 | list_forall2 (match_var_etry match_var) vars tvars → |
---|
1407 | snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). |
---|
1408 | Proof. |
---|
1409 | induction 1; simpl. |
---|
1410 | auto. |
---|
1411 | destruct a1 as [[id1 init1] info1]. |
---|
1412 | destruct b1 as [[id2 init2] info2]. |
---|
1413 | red in H. destruct H as [X [Y Z]]. subst id2 init2. |
---|
1414 | generalize IHlist_forall2. |
---|
1415 | destruct (add_globals (g1, m) al). |
---|
1416 | destruct (add_globals (g2, m) bl). |
---|
1417 | simpl. intro. subst m1. auto. |
---|
1418 | Qed. |
---|
1419 | |
---|
1420 | Lemma symbols_add_globals_match: |
---|
1421 | forall (g1: genv A) (g2: genv B) (m: mem), |
---|
1422 | symbols g1 = symbols g2 → |
---|
1423 | forall (vars: list (ident * list init_data * V)) |
---|
1424 | (tvars: list (ident * list init_data * W)), |
---|
1425 | list_forall2 (match_var_etry match_var) vars tvars → |
---|
1426 | symbols (fst (add_globals (g1, m) vars)) = |
---|
1427 | symbols (fst (add_globals (g2, m) tvars)). |
---|
1428 | Proof. |
---|
1429 | induction 2; simpl. |
---|
1430 | auto. |
---|
1431 | destruct a1 as [[id1 init1] info1]. |
---|
1432 | destruct b1 as [[id2 init2] info2]. |
---|
1433 | red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. |
---|
1434 | generalize IHlist_forall2. |
---|
1435 | generalize (mem_add_globals_match g1 g2 m H1). |
---|
1436 | destruct (add_globals (g1, m) al). |
---|
1437 | destruct (add_globals (g2, m) bl). |
---|
1438 | simpl. intros. congruence. |
---|
1439 | Qed. |
---|
1440 | |
---|
1441 | Theorem find_funct_ptr_match: |
---|
1442 | forall (b: block) (f: A), |
---|
1443 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1444 | ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf. |
---|
1445 | Proof. |
---|
1446 | intros until f. destruct match_prog as [X [Y Z]]. |
---|
1447 | destruct (add_functs_match X) as [P [Q R]]. |
---|
1448 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
1449 | auto. |
---|
1450 | Qed. |
---|
1451 | |
---|
1452 | Theorem find_funct_ptr_rev_match: |
---|
1453 | forall (b: block) (tf: B), |
---|
1454 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
1455 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf. |
---|
1456 | Proof. |
---|
1457 | intros until tf. destruct match_prog as [X [Y Z]]. |
---|
1458 | destruct (add_functs_rev_match X) as [P [Q R]]. |
---|
1459 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
1460 | auto. |
---|
1461 | Qed. |
---|
1462 | |
---|
1463 | Theorem find_funct_match: |
---|
1464 | forall (v: val) (f: A), |
---|
1465 | find_funct (globalenv p) v = Some ? f → |
---|
1466 | ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf. |
---|
1467 | Proof. |
---|
1468 | intros until f. unfold find_funct. |
---|
1469 | case v; try (intros; discriminate). |
---|
1470 | intros b ofs. |
---|
1471 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
1472 | apply find_funct_ptr_match. |
---|
1473 | Qed. |
---|
1474 | |
---|
1475 | Theorem find_funct_rev_match: |
---|
1476 | forall (v: val) (tf: B), |
---|
1477 | find_funct (globalenv p') v = Some ? tf → |
---|
1478 | ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf. |
---|
1479 | Proof. |
---|
1480 | intros until tf. unfold find_funct. |
---|
1481 | case v; try (intros; discriminate). |
---|
1482 | intros b ofs. |
---|
1483 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
1484 | apply find_funct_ptr_rev_match. |
---|
1485 | Qed. |
---|
1486 | |
---|
1487 | Lemma symbols_init_match: |
---|
1488 | symbols (globalenv p') = symbols (globalenv p). |
---|
1489 | Proof. |
---|
1490 | unfold globalenv. unfold globalenv_initmem. |
---|
1491 | destruct match_prog as [X [Y Z]]. |
---|
1492 | destruct (add_functs_match X) as [P [Q R]]. |
---|
1493 | simpl. symmetry. apply symbols_add_globals_match. auto. auto. |
---|
1494 | Qed. |
---|
1495 | |
---|
1496 | Theorem find_symbol_match: |
---|
1497 | forall (s: ident), |
---|
1498 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
1499 | Proof. |
---|
1500 | intros. unfold find_symbol. |
---|
1501 | rewrite symbols_init_match. auto. |
---|
1502 | Qed. |
---|
1503 | |
---|
1504 | Theorem init_mem_match: |
---|
1505 | init_mem p' = init_mem p. |
---|
1506 | Proof. |
---|
1507 | unfold init_mem. unfold globalenv_initmem. |
---|
1508 | destruct match_prog as [X [Y Z]]. |
---|
1509 | symmetry. apply mem_add_globals_match. auto. |
---|
1510 | Qed. |
---|
1511 | |
---|
1512 | End MATCH_PROGRAM. |
---|
1513 | |
---|
1514 | Section TRANSF_PROGRAM_PARTIAL2. |
---|
1515 | |
---|
1516 | Variable A B V W: Type. |
---|
1517 | Variable transf_fun: A → res B. |
---|
1518 | Variable transf_var: V → res W. |
---|
1519 | Variable p: program A V. |
---|
1520 | Variable p': program B W. |
---|
1521 | Hypothesis transf_OK: |
---|
1522 | transform_partial_program2 transf_fun transf_var p = OK ? p'. |
---|
1523 | |
---|
1524 | Remark prog_match: |
---|
1525 | match_program |
---|
1526 | (fun fd tfd => transf_fun fd = OK ? tfd) |
---|
1527 | (fun info tinfo => transf_var info = OK ? tinfo) |
---|
1528 | p p'. |
---|
1529 | Proof. |
---|
1530 | apply transform_partial_program2_match; auto. |
---|
1531 | Qed. |
---|
1532 | |
---|
1533 | Theorem find_funct_ptr_transf_partial2: |
---|
1534 | forall (b: block) (f: A), |
---|
1535 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1536 | ∃f'. |
---|
1537 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'. |
---|
1538 | Proof. |
---|
1539 | intros. |
---|
1540 | exploit find_funct_ptr_match. eexact prog_match. eauto. |
---|
1541 | intros [tf [X Y]]. exists tf; auto. |
---|
1542 | Qed. |
---|
1543 | |
---|
1544 | Theorem find_funct_ptr_rev_transf_partial2: |
---|
1545 | forall (b: block) (tf: B), |
---|
1546 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
1547 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf. |
---|
1548 | Proof. |
---|
1549 | intros. |
---|
1550 | exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. |
---|
1551 | Qed. |
---|
1552 | |
---|
1553 | Theorem find_funct_transf_partial2: |
---|
1554 | forall (v: val) (f: A), |
---|
1555 | find_funct (globalenv p) v = Some ? f → |
---|
1556 | ∃f'. |
---|
1557 | find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'. |
---|
1558 | Proof. |
---|
1559 | intros. |
---|
1560 | exploit find_funct_match. eexact prog_match. eauto. |
---|
1561 | intros [tf [X Y]]. exists tf; auto. |
---|
1562 | Qed. |
---|
1563 | |
---|
1564 | Theorem find_funct_rev_transf_partial2: |
---|
1565 | forall (v: val) (tf: B), |
---|
1566 | find_funct (globalenv p') v = Some ? tf → |
---|
1567 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf. |
---|
1568 | Proof. |
---|
1569 | intros. |
---|
1570 | exploit find_funct_rev_match. eexact prog_match. eauto. auto. |
---|
1571 | Qed. |
---|
1572 | |
---|
1573 | Theorem find_symbol_transf_partial2: |
---|
1574 | forall (s: ident), |
---|
1575 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
1576 | Proof. |
---|
1577 | intros. eapply find_symbol_match. eexact prog_match. |
---|
1578 | Qed. |
---|
1579 | |
---|
1580 | Theorem init_mem_transf_partial2: |
---|
1581 | init_mem p' = init_mem p. |
---|
1582 | Proof. |
---|
1583 | intros. eapply init_mem_match. eexact prog_match. |
---|
1584 | Qed. |
---|
1585 | |
---|
1586 | End TRANSF_PROGRAM_PARTIAL2. |
---|
1587 | |
---|
1588 | Section TRANSF_PROGRAM_PARTIAL. |
---|
1589 | |
---|
1590 | Variable A B V: Type. |
---|
1591 | Variable transf: A → res B. |
---|
1592 | Variable p: program A V. |
---|
1593 | Variable p': program B V. |
---|
1594 | Hypothesis transf_OK: transform_partial_program transf p = OK ? p'. |
---|
1595 | |
---|
1596 | Remark transf2_OK: |
---|
1597 | transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'. |
---|
1598 | Proof. |
---|
1599 | rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. |
---|
1600 | destruct (map_partial prefix_funct_name transf (prog_funct p)); auto. |
---|
1601 | rewrite map_partial_identity; auto. |
---|
1602 | Qed. |
---|
1603 | |
---|
1604 | Theorem find_funct_ptr_transf_partial: |
---|
1605 | forall (b: block) (f: A), |
---|
1606 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1607 | ∃f'. |
---|
1608 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'. |
---|
1609 | Proof. |
---|
1610 | exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
1611 | Qed. |
---|
1612 | |
---|
1613 | Theorem find_funct_ptr_rev_transf_partial: |
---|
1614 | forall (b: block) (tf: B), |
---|
1615 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
1616 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf. |
---|
1617 | Proof. |
---|
1618 | exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
1619 | Qed. |
---|
1620 | |
---|
1621 | Theorem find_funct_transf_partial: |
---|
1622 | forall (v: val) (f: A), |
---|
1623 | find_funct (globalenv p) v = Some ? f → |
---|
1624 | ∃f'. |
---|
1625 | find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'. |
---|
1626 | Proof. |
---|
1627 | exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
1628 | Qed. |
---|
1629 | |
---|
1630 | Theorem find_funct_rev_transf_partial: |
---|
1631 | forall (v: val) (tf: B), |
---|
1632 | find_funct (globalenv p') v = Some ? tf → |
---|
1633 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf. |
---|
1634 | Proof. |
---|
1635 | exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
1636 | Qed. |
---|
1637 | |
---|
1638 | Theorem find_symbol_transf_partial: |
---|
1639 | forall (s: ident), |
---|
1640 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
1641 | Proof. |
---|
1642 | exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
1643 | Qed. |
---|
1644 | |
---|
1645 | Theorem init_mem_transf_partial: |
---|
1646 | init_mem p' = init_mem p. |
---|
1647 | Proof. |
---|
1648 | exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
1649 | Qed. |
---|
1650 | |
---|
1651 | End TRANSF_PROGRAM_PARTIAL. |
---|
1652 | |
---|
1653 | Section TRANSF_PROGRAM. |
---|
1654 | |
---|
1655 | Variable A B V: Type. |
---|
1656 | Variable transf: A → B. |
---|
1657 | Variable p: program A V. |
---|
1658 | Let tp := transform_program transf p. |
---|
1659 | |
---|
1660 | Remark transf_OK: |
---|
1661 | transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp. |
---|
1662 | Proof. |
---|
1663 | unfold tp, transform_program, transform_partial_program. |
---|
1664 | rewrite map_partial_total. reflexivity. |
---|
1665 | Qed. |
---|
1666 | |
---|
1667 | Theorem find_funct_ptr_transf: |
---|
1668 | forall (b: block) (f: A), |
---|
1669 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
1670 | find_funct_ptr ? (globalenv tp) b = Some ? (transf f). |
---|
1671 | Proof. |
---|
1672 | intros. |
---|
1673 | destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
1674 | as [f' [X Y]]. congruence. |
---|
1675 | Qed. |
---|
1676 | |
---|
1677 | Theorem find_funct_ptr_rev_transf: |
---|
1678 | forall (b: block) (tf: B), |
---|
1679 | find_funct_ptr ? (globalenv tp) b = Some ? tf → |
---|
1680 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf. |
---|
1681 | Proof. |
---|
1682 | intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto. |
---|
1683 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
1684 | Qed. |
---|
1685 | |
---|
1686 | Theorem find_funct_transf: |
---|
1687 | forall (v: val) (f: A), |
---|
1688 | find_funct (globalenv p) v = Some ? f → |
---|
1689 | find_funct (globalenv tp) v = Some ? (transf f). |
---|
1690 | Proof. |
---|
1691 | intros. |
---|
1692 | destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
1693 | as [f' [X Y]]. congruence. |
---|
1694 | Qed. |
---|
1695 | |
---|
1696 | Theorem find_funct_rev_transf: |
---|
1697 | forall (v: val) (tf: B), |
---|
1698 | find_funct (globalenv tp) v = Some ? tf → |
---|
1699 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf. |
---|
1700 | Proof. |
---|
1701 | intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto. |
---|
1702 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
1703 | Qed. |
---|
1704 | |
---|
1705 | Theorem find_symbol_transf: |
---|
1706 | forall (s: ident), |
---|
1707 | find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s. |
---|
1708 | Proof. |
---|
1709 | exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). |
---|
1710 | Qed. |
---|
1711 | |
---|
1712 | Theorem init_mem_transf: |
---|
1713 | init_mem tp = init_mem p. |
---|
1714 | Proof. |
---|
1715 | exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK). |
---|
1716 | Qed. |
---|
1717 | |
---|
1718 | End TRANSF_PROGRAM. |
---|
1719 | |
---|
1720 | End Genv. |
---|
1721 | *) |
---|
1722 | |
---|