source: src/common/Globalenvs.ma @ 2105

Last change on this file since 2105 was 2105, checked in by campbell, 8 years ago

Show some results about globalenvs and program transformations.

File size: 60.9 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Global environments are a component of the dynamic semantics of
17  all languages involved in the compiler.  A global environment
18  maps symbol names (names of functions and of global variables)
19  to the corresponding memory addresses.  It also maps memory addresses
20  of functions to the corresponding function descriptions. 
21
22  Global environments, along with the initial memory state at the beginning
23  of program execution, are built from the program of interest, as follows:
24- A distinct memory address is assigned to each function of the program.
25  These function addresses use negative numbers to distinguish them from
26  addresses of memory blocks.  The associations of function name to function
27  address and function address to function description are recorded in
28  the global environment.
29- For each global variable, a memory block is allocated and associated to
30  the name of the variable.
31
32  These operations reflect (at a high level of abstraction) what takes
33  place during program linking and program loading in a real operating
34  system. *)
35
36include "common/Errors.ma".
37include "common/AST.ma".
38(*include "Values.ma".*)
39include "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 *)
44record genv_t (F:Type[0]) : Type[0] ≝ {
45  functions: positive_map F;
46  nextfunction: Pos;
47  symbols: identifier_map SymbolTag block
48}.
49
50definition 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
58definition 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 *)
65definition empty_mem ≝ empty. (* XXX*)
66definition empty : ∀F. genv_t F ≝
67  λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??).
68
69definition 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. *)
74definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝
75λF,ge. lookup ?? (symbols … ge).
76
77(* init *)
78
79definition 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  ].
103cases b //
104qed.
105
106definition 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
117let 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
129definition 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
133nremark 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##]
150qed.
151*)
152
153
154(* init *)
155
156axiom InitDataStoreFailed : String.
157
158definition 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
174definition 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
190definition 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. *)
197definition 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. *)
202definition 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. *)
207definition 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. *)
214definition 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. *)
219definition 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. *)
226definition 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
230lemma 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
245lemma 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
248whd 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
261lemma matching_globals_get_same_blocks : ∀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#A #B #V #W #initV #initW #P #varsOK
269#vars elim vars
270[ #ge #ge' #m * [ #E #_ @E | #h #t #_ * ]
271| * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ]
272  * * #id' #r' #w #tl' #E * #p #TL
273  whd in match (add_globals A ????);
274  change with (add_globals A ????) in match (foldl ?????);
275  whd in match (add_globals B ????);
276  change with (add_globals B ????) in match (foldl (genv_t B × mem) ????);
277  cases (varsOK … p) #E1 #E2
278  destruct >E2 cases (alloc ????) #m' #b
279  @IH //
280  whd in match (add_symbol ????);
281  whd in match (add_symbol ????);
282  >E %
283] qed.
284
285lemma pre_matching_fns_get_same_blocks : ∀A,B,P.
286  (∀f,g. P f g → \fst f = \fst g) →
287  ∀fns,fns'.
288  All2 … P fns fns' →
289  let ge ≝ add_functs A (empty ?) fns in
290  let ge' ≝ add_functs B (empty ?) fns' in
291  nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'.
292#A #B #P #fnOK #fns elim fns
293[ * [ #_ % % | #h #t * ]
294| * #id #f #tl #IH * [ * ]
295  * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H
296  whd in match (add_functs ???);
297  change with (add_functs ???) in match (foldr ?????);
298  whd in match (add_functs B ??);
299  change with (add_functs ???) in match (foldr (ident × B) ????);
300  cases (IH tl' H) #E1 #E2
301  % [ >E1 % | >E1 >E2 % ]
302] qed.
303
304lemma matching_fns_get_same_blocks :  ∀A,B,P.
305  (∀f,g. P f g → \fst f = \fst g) →
306  ∀fns,fns'.
307  All2 … P fns fns' →
308  let ge ≝ add_functs A (empty ?) fns in
309  let ge' ≝ add_functs B (empty ?) fns' in
310  symbols … ge = symbols … ge'.
311#A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK
312qed.
313
314(*
315(* * ** Properties of the operations. *)
316
317  find_funct_inv:
318    ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F.
319    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
320  find_funct_find_funct_ptr:
321    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
322    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
323
324  find_symbol_exists:
325    ∀F,V: Type[0]. ∀p: program F V.
326           ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
327    in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
328    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
329  find_funct_ptr_exists:
330    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
331    list_norepet ? (prog_funct_names ?? p) →
332    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
333    in_list ? 〈id, f〉 (prog_funct ?? p) →
334    ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
335           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;
336
337  find_funct_ptr_inversion:
338    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
339    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
340    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
341  find_funct_inversion:
342    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
343    find_funct ? (globalenv ?? p) v = Some ? f →
344    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
345  find_funct_ptr_symbol_inversion:
346    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
347    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 →
348    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
349    in_list ? 〈id, f〉 (prog_funct ?? p);
350
351  find_funct_ptr_prop:
352    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
353    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
354    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
355    P f;
356  find_funct_prop:
357    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
358    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
359    find_funct ? (globalenv ?? p) v = Some ? f →
360    P f;
361
362  initmem_nullptr:
363    ∀F,V: Type[0]. ∀p: program F V.
364    let m ≝ init_mem ?? p in
365    valid_block m nullptr ∧
366    (blocks m) nullptr = empty_block 0 0 Any;
367(*  initmem_inject_neutral:
368    ∀F,V: Type[0]. ∀p: program F V.
369    mem_inject_neutral (init_mem ?? p);*)
370  find_funct_ptr_negative:
371    ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F.
372    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
373  find_symbol_not_fresh:
374    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
375    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
376  find_symbol_not_nullptr:
377    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
378    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
379  global_addresses_distinct:
380    ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2.
381    id1≠id2 →
382    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
383    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
384    b1≠b2;
385
386(* * Commutation properties between program transformations
387  and operations over global environments. *)
388
389  init_mem_transf:
390    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
391    init_mem ?? (transform_program … transf p) = init_mem ?? p;
392  find_funct_ptr_rev_transf:
393    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
394    ∀b : block. ∀tf : B.
395    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
396    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
397  find_funct_rev_transf:
398    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
399    ∀v : val. ∀tf : B.
400    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
401    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
402
403(* * Commutation properties between partial program transformations
404  and operations over global environments. *)
405
406  find_funct_ptr_transf_partial:
407    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
408    transform_partial_program … transf p = OK ? p' →
409    ∀b: block. ∀f: A.
410    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
411    ∃f'.
412    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
413  find_funct_transf_partial:
414    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
415    transform_partial_program … transf p = OK ? p' →
416    ∀v: val. ∀f: A.
417    find_funct ? (globalenv ?? p) v = Some ? f →
418    ∃f'.
419    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
420  find_symbol_transf_partial:
421    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
422    transform_partial_program … transf p = OK ? p' →
423    ∀s: ident.
424    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
425  init_mem_transf_partial:
426    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
427    transform_partial_program … transf p = OK ? p' →
428    init_mem ?? p' = init_mem ?? p;
429  find_funct_ptr_rev_transf_partial:
430    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
431    transform_partial_program … transf p = OK ? p' →
432    ∀b : block. ∀tf : B.
433    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
434    ∃f : A.
435      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
436  find_funct_rev_transf_partial:
437    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
438    transform_partial_program … transf p = OK ? p' →
439    ∀v : val. ∀tf : B.
440    find_funct ? (globalenv ?? p') v = Some ? tf →
441    ∃f : A.
442      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*;
443
444  find_funct_ptr_transf_partial2:
445    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
446           ∀p: program A V. ∀p': program B W.
447    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
448    ∀b: block. ∀f: A.
449    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
450    ∃f'.
451    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
452  find_funct_transf_partial2:
453    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
454           ∀p: program A V. ∀p': program B W.
455    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
456    ∀v: val. ∀f: A.
457    find_funct ? (globalenv ?? p) v = Some ? f →
458    ∃f'.
459    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
460  find_symbol_transf_partial2:
461    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
462           ∀p: program A V. ∀p': program B W.
463    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
464    ∀s: ident.
465    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
466  init_mem_transf_partial2:
467    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
468           ∀p: program A V. ∀p': program B W.
469    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
470    init_mem ?? p' = init_mem ?? p;
471  find_funct_ptr_rev_transf_partial2:
472    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
473           ∀p: program A V. ∀p': program B W.
474    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
475    ∀b: block. ∀tf: B.
476    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
477    ∃f : A.
478      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
479  find_funct_rev_transf_partial2:
480    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
481           ∀p: program A V. ∀p': program B W.
482    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
483    ∀v: val. ∀tf: B.
484    find_funct ? (globalenv ?? p') v = Some ? tf →
485    ∃f : A.
486      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ;
487
488(* * Commutation properties between matching between programs
489  and operations over global environments. *)
490*) *)
491
492(* First, show that nextfunction only depends on the number of functions: *)
493
494let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
495match n with
496[ O ⇒ p
497| S m ⇒ succ (nat_plus_pos m p)
498].
499
500lemma nextfunction_length : ∀A,l,ge.
501  nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge).
502#A #l elim l // #h #t #IH #ge
503whd in ⊢ (??%%); >IH //
504qed.
505
506(* Now link functions in related programs, but without dealing with the type
507   casts yet. *)
508
509lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P.
510  find_funct_ptr … (globalenv A V initV p) b = Some ? f →
511  All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') →
512  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
513#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
514cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ]
515[ 12: | *: #F whd in F:(??%?); destruct ]
516>vars_irrelevant_to_find_funct_ptr
517>vars_irrelevant_to_find_funct_ptr
518letin varnames ≝ (map ??? vars)
519cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
520//
521cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
522//
523generalize in match (empty ?);
524generalize in match (empty ?);
525generalize in match fns';
526elim fns
527[ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct
528| * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?);
529  whd in match (functions ??);
530  change with (add_functs ???) in match (foldr ?????);
531  cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl)))
532  [ #E destruct  >lookup_opt_insert_hit #E destruct
533    cases fns' [ * ]
534    * #id' #fn' #tl' * #M #Mtl
535    %{fn'} % // whd in ⊢ (??%?);
536    whd in match (functions ??);
537    change with (add_functs ???) in match (foldr ???? tl');
538    >nextfunction_length >nextfunction_length <NF >(All2_length  … Mtl)
539    >lookup_opt_insert_hit @refl
540  | #NE >lookup_opt_insert_miss //
541    #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl
542    cases (IH ?????? Mtl)
543    [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP' | @P' ]
544    | skip
545    | 4: @NF
546    | skip
547    | //
548    | @FFP
549    ]
550  ]
551] qed.
552
553discriminator Prod.
554
555(* Now prove the full version. *)
556
557lemma find_funct_ptr_match:
558    ∀M:matching.∀initV,initW.
559    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
560    ∀MATCH:match_program … M p p'.
561    ∀b: block. ∀f: m_A M (prog_var_names … p).
562    find_funct_ptr … (globalenv … initV p) b = Some ? f →
563    ∃tf : m_B M (prog_var_names … p').
564    find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
565[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
566* #A #B #V #W #match_fn #match_var #initV #initW
567#p #p' * #Mvars #Mfn #Mmain
568#b #f #FFP
569@(find_funct_ptr_All2 A B V W ??????? FFP)
570lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars)
571#E
572@(All2_mp … Mfn)
573* #id #f * #id' #f'
574<E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E
575normalize #H @(match_funct_entry_inv … H) //
576qed.
577
578lemma
579  find_funct_ptr_transf_partial2:
580    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
581           ∀p: program A V. ∀p': program B W.
582    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
583    ∀b: block. ∀f: A ?.
584    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
585    ∃f'.
586    find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'.
587#A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP
588cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP)
589[2: @iW
590| #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E
591#TF %{f'} % //
592-FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' %
593qed.
594
595lemma match_funct_entry_id : ∀M,vs,vs',f,g.
596  match_funct_entry M vs vs' f g → \fst f = \fst g.
597#M #vs #vs' #f #g * //
598qed.
599
600lemma
601  find_symbol_match:
602    ∀M:matching.
603    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
604    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
605    match_program … M p p' →
606    ∀s: ident.
607    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
608* #A #B #V #W #match_fun #match_var #initV #initW #initsize
609* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
610whd in ⊢ (??%%);
611@sym_eq
612@(eq_f ??(λx. lookup SymbolTag block x s))
613whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
614whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
615change with (add_globals ?????) in match (foldl ?????);
616change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
617@(matching_globals_get_same_blocks … Mvars)
618[ * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
619| @(matching_fns_get_same_blocks … Mfns)
620  #f #g @match_funct_entry_id
621] qed.
622 
623lemma
624  find_symbol_transf_partial2:
625    ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W.
626    (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) →
627           ∀p: program A V. ∀p': program B W.
628    transform_partial_program2 … p transf_fun transf_var = OK ? p' →
629    ∀s: ident.
630    find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s.
631#A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s
632@(find_symbol_match … (transform_partial_program2_match … TPP2))
633#v0 #w0 * #id #r #v #w @sizeOK
634qed.
635
636lemma
637  find_funct_ptr_transf:
638    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
639    ∀b: block. ∀f: A ?.
640    find_funct_ptr ? (globalenv … iV p) b = Some ? f →
641    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f).
642#A #B #V #iV * #vars #fns #main #tf #b #f #FFP
643cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
644[ 2: @iV
645| #f' * #FFP'
646  generalize in match (matching_vars ????);
647  whd in match (prog_var_names ???); whd in match (prog_vars ???);
648  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
649] qed.
650
651lemma
652  find_funct_transf:
653    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
654    ∀v: val. ∀f: A ?.
655    find_funct ? (globalenv … iV p) v = Some ? f →
656    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
657#A #B #V #iV #tf #p #v #f #FF
658cases (find_funct_find_funct_ptr ???? FF)
659#r * #b * #pc * #E destruct #FFP
660change with (find_funct_ptr ???) in ⊢ (??%?);
661@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
662qed.
663
664lemma
665  find_symbol_transf:
666    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
667    ∀s: ident.
668    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
669    find_symbol ? (globalenv … iV p) s.
670#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
671#v0 #w0 * //
672qed.
673
674(* Package up transform_program results nicely. *)
675
676record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
677  rg_find_symbol: ∀s.
678    find_symbol … ge s = find_symbol … ge' s;
679  rg_find_funct: ∀v,f.
680    find_funct … ge v = Some ? f →
681    find_funct … ge' v = Some ? (t f);
682  rg_find_funct_ptr: ∀b,f.
683    find_funct_ptr … ge b = Some ? f →
684    find_funct_ptr … ge' b = Some ? (t f)
685}.
686
687theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
688  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
689#A #B #V #iV #p #tf %
690[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
691| @(find_funct_transf A B V iV tf p)
692| @(find_funct_ptr_transf A B V iV p tf)
693] qed.
694
695
696(*
697
698  find_funct_ptr_match:
699    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
700           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
701    match_program … match_fun match_var p p' →
702    ∀b: block. ∀f: A.
703    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
704    ∃tf : B.
705    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
706  find_funct_ptr_rev_match:
707    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
708           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
709    match_program … match_fun match_var p p' →
710    ∀b: block. ∀tf: B.
711    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
712    ∃f : A.
713    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
714  find_funct_match:
715    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
716           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
717    match_program … match_fun match_var p p' →
718    ∀v: val. ∀f: A.
719    find_funct ? (globalenv ?? p) v = Some ? f →
720    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
721  find_funct_rev_match:
722    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
723           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
724    match_program … match_fun match_var p p' →
725    ∀v: val. ∀tf: B.
726    find_funct ? (globalenv ?? p') v = Some ? tf →
727    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
728  find_symbol_match:
729    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
730           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
731    match_program … match_fun match_var p p' →
732    ∀s: ident.
733    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
734  init_mem_match:
735    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
736           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
737    match_program … match_fun match_var p p' →
738    init_mem ?? p' = init_mem ?? p*)
739
740(*
741Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
742  ZMap.get b g.(functions).
743
744Definition find_funct (g: genv) (v: val) : option F :=
745  match v with
746  | Vptr b ofs =>
747      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
748  | _ =>
749      None
750  end.
751
752Definition find_symbol ? (g: genv) (symb: ident) : option block :=
753  PTree.get symb g.(symbols).
754
755Lemma find_funct_inv:
756  forall (ge: t) (v: val) (f: F),
757  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
758Proof.
759  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
760  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
761  exists b. congruence.
762  discriminate.
763Qed.
764
765Lemma find_funct_find_funct_ptr:
766  forall (ge: t) (b: block),
767  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
768Proof.
769  intros. simpl.
770  generalize (Int.eq_spec Int.zero Int.zero).
771  case (Int.eq Int.zero Int.zero); intros.
772  auto. tauto.
773Qed.
774*)
775
776(*
777##[ #A B C transf p b f; elim p; #fns main vars;
778    elim fns;
779    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
780    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
781        nrewrite > (?:nextfunction ?? = length ? t);
782        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
783            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
784        ##| nrewrite > (?:nextfunction ?? = length ? t);
785          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
786              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
787          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
788            ##[ #H; destruct (H); //;
789            ##| #H; napply IH; napply H;
790            ##]
791          ##]
792        ##]
793    ##]
794##| #A B C transf p v f; elim v;
795    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
796    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
797    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
798        whd in ⊢ (??%? → ??%?);
799        ##[ elim p; #fns main vars; elim fns;
800          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
801          ##| #h t; elim h; #f fn IH;
802              whd in ⊢ (??%? → ??%?);
803              nrewrite > (?:nextfunction ?? = length ? t);
804              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
805                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
806              ##| nrewrite > (?:nextfunction ?? = length ? t);
807                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
808                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
809                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
810                  ##[ destruct (H); //;
811                  ##| napply IH; napply H;
812                  ##]
813                ##]
814              ##]
815          ##]
816       ##| #H; destruct;
817       ##]
818    ##]
819##| #A B C transf p id; elim p; #fns main vars;
820    elim fns;
821    ##[ normalize; //
822    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
823        elim (ident_eq fid id); #e;
824        ##[ whd in ⊢ (??%%);
825          nrewrite > (?:nextfunction ?? = length ? t);
826          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
827              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
828          ##| nrewrite > (?:nextfunction ?? = length ? t);
829            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
830                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
831            ##| //
832            ##]
833          ##]
834        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
835        ##]
836    ##]
837##| //;
838##| #A B C transf p b tf; elim p; #fns main vars;
839    elim fns;
840    ##[ normalize; #H; destruct;
841    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
842        nrewrite > (?:nextfunction ?? = length ? t);
843        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
844            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
845        ##| nrewrite > (?:nextfunction ?? = length ? t);
846          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
847              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
848          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
849            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
850            ##| #H; napply IH; napply H;
851            ##]
852          ##]
853        ##]
854    ##]
855##| #A B C transf p v tf; elim p; #fns main vars; elim v;
856  ##[ normalize; #H; destruct;
857  ##| ##2,3: #x; normalize; #H; destruct;
858  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
859    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
860      elim fns;
861      ##[ normalize; #H; destruct;
862      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
863          nrewrite > (?:nextfunction ?? = length ? t);
864          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
865              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
866          ##| nrewrite > (?:nextfunction ?? = length ? t);
867            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
868                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
869            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
870              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
871              ##| #H; napply IH; napply H;
872              ##]
873            ##]
874          ##]
875      ##]
876    ##| normalize; #H; destruct;
877    ##]
878 ##]
879##] qed.
880         
881
882Lemma functions_globalenv:
883  forall (p: program F V),
884  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
885Proof.
886  assert (forall init vars,
887     functions (fst (add_globals init vars)) = functions (fst init)).
888  induction vars; simpl.
889  reflexivity.
890  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
891  simpl. exact IHvars.
892
893  unfold add_globals; simpl.
894  intros. unfold globalenv; unfold globalenv_initmem.
895  rewrite H. reflexivity.
896Qed.
897
898Lemma initmem_nullptr:
899  forall (p: program F V),
900  let m := init_mem p in
901  valid_block m nullptr /\
902  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
903Proof.
904  pose (P := fun m => valid_block m nullptr /\
905        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
906  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
907  induction vars; simpl; intros.
908  auto.
909  destruct a as [[id1 in1] inf1].
910  destruct (add_globals init vars) as [g st].
911  simpl in *. destruct IHvars. split.
912  red; simpl. red in H0. omega.
913  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
914
915  intro. unfold init_mem, globalenv_initmem. apply H.
916  red; simpl. split. compute. auto. reflexivity.
917Qed.
918
919Lemma initmem_inject_neutral:
920  forall (p: program F V),
921  mem_inject_neutral (init_mem p).
922Proof.
923  assert (forall g0 vars g1 m,
924      add_globals (g0, Mem.empty) vars = (g1, m) →
925      mem_inject_neutral m).
926  Opaque alloc_init_data.
927  induction vars; simpl.
928  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
929  simpl in H1. rewrite Mem.getN_init in H1.
930  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
931  destruct a as [[id1 init1] info1].
932  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
933  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
934  intros. inv H.
935  eapply Mem.alloc_init_data_neutral; eauto.
936  intros. caseEq (globalenv_initmem p). intros g m EQ.
937  unfold init_mem; rewrite EQ; simpl.
938  unfold globalenv_initmem in EQ. eauto.
939Qed.     
940
941Remark nextfunction_add_functs_neg:
942  forall fns, nextfunction (add_functs empty fns) < 0.
943Proof.
944  induction fns; simpl; intros. omega. unfold Zpred. omega.
945Qed.
946
947Theorem find_funct_ptr_negative:
948  forall (p: program F V) (b: block) (f: F),
949  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
950Proof.
951  intros until f.
952  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
953    induction fns; simpl.
954    rewrite ZMap.gi. congruence.
955    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
956    intro. rewrite e. apply nextfunction_add_functs_neg.
957    auto.
958  unfold find_funct_ptr. rewrite functions_globalenv.
959  intros. eauto.
960Qed.
961
962Remark find_symbol_add_functs_negative:
963  forall (fns: list (ident * F)) s b,
964  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
965Proof.
966  induction fns; simpl; intros until b.
967  rewrite PTree.gempty. congruence.
968  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
969  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
970  eauto.
971Qed.
972
973Remark find_symbol_add_symbols_not_fresh:
974  forall fns vars g m s b,
975  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
976  (symbols g)!s = Some ? b →
977  b < nextblock m.
978Proof.
979  induction vars; simpl; intros until b.
980  intros. inversion H. subst g m. simpl.
981  generalize (find_symbol_add_functs_negative fns s H0). omega.
982  Transparent alloc_init_data.
983  destruct a as [[id1 init1] info1].
984  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
985  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
986  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
987  intro EQ; inversion EQ. omega.
988  intro. generalize (IHvars _ _ _ _ ADG H). omega.
989Qed.
990
991Theorem find_symbol_not_fresh:
992  forall (p: program F V) (id: ident) (b: block),
993  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
994Proof.
995  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
996  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
997                      (prog_vars p)); intros g m EQ.
998  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
999Qed.
1000
1001Lemma find_symbol_exists:
1002  forall (p: program F V)
1003         (id: ident) (init: list init_data) (v: V),
1004  In (id, init, v) (prog_vars p) →
1005  ∃b. find_symbol ? (globalenv p) id = Some ? b.
1006Proof.
1007  intros until v.
1008  assert (forall initm vl, In (id, init, v) vl →
1009           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
1010  induction vl; simpl; intros.
1011  elim H.
1012  destruct a as [[id0 init0] v0].
1013  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
1014  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
1015  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
1016  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
1017Qed.
1018
1019Remark find_symbol_above_nextfunction:
1020  forall (id: ident) (b: block) (fns: list (ident * F)),
1021  let g := add_functs empty fns in
1022  PTree.get id g.(symbols) = Some ? b →
1023  b > g.(nextfunction).
1024Proof.
1025  induction fns; simpl.
1026  rewrite PTree.gempty. congruence.
1027  rewrite PTree.gsspec. case (peq id (fst a)); intro.
1028  intro EQ. inversion EQ. unfold Zpred. omega.
1029  intros. generalize (IHfns H). unfold Zpred; omega.
1030Qed.
1031
1032Remark find_symbol_add_globals:
1033  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
1034  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
1035  find_symbol ? (fst (add_globals ge_m vars)) id =
1036  find_symbol ? (fst ge_m) id.
1037Proof.
1038  unfold find_symbol; induction vars; simpl; intros.
1039  auto.
1040  destruct a as [[id0 init0] var0]. simpl in *.
1041  caseEq (add_globals ge_m vars); intros ge' m' EQ.
1042  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
1043  apply IHvars. tauto. intuition congruence.
1044Qed.
1045
1046Lemma find_funct_ptr_exists:
1047  forall (p: program F V) (id: ident) (f: F),
1048  list_norepet (prog_funct_names p) →
1049  list_disjoint (prog_funct_names p) (prog_var_names p) →
1050  In (id, f) (prog_funct p) →
1051  ∃b. find_symbol ? (globalenv p) id = Some ? b
1052         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
1053Proof.
1054  intros until f.
1055  assert (forall (fns: list (ident * F)),
1056           list_norepet (map (@fst ident F) fns) →
1057           In (id, f) fns →
1058           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
1059                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
1060  unfold find_symbol, find_funct_ptr. induction fns; intros.
1061  elim H0.
1062  destruct a as [id0 f0]; simpl in *. inv H.
1063  unfold add_funct; simpl.
1064  rewrite PTree.gsspec. destruct (peq id id0).
1065  subst id0. econstructor; split. eauto.
1066  replace f0 with f. apply ZMap.gss.
1067  elim H0; intro. congruence. elim H3.
1068  change id with (@fst ident F (id, f)). apply List.in_map. auto.
1069  exploit IHfns; eauto. elim H0; intro. congruence. auto.
1070  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
1071  generalize (find_symbol_above_nextfunction _ _ X).
1072  unfold block; unfold ZIndexed.t; intro; omega.
1073
1074  intros. exploit H; eauto. intros [b [X Y]].
1075  exists b; split.
1076  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
1077  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
1078  unfold prog_funct_names. change id with (fst (id, f)).
1079  apply List.in_map; auto.
1080  unfold find_funct_ptr. rewrite functions_globalenv.
1081  assumption.
1082Qed.
1083
1084Lemma find_funct_ptr_inversion:
1085  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1086  find_funct_ptr ? (globalenv p) b = Some ? f →
1087  ∃id. In (id, f) (prog_funct p).
1088Proof.
1089  intros until f.
1090  assert (forall fns: list (ident * F),
1091    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
1092    ∃id. In (id, f) fns).
1093  unfold find_funct_ptr. induction fns; simpl.
1094  rewrite ZMap.gi. congruence.
1095  destruct a as [id0 f0]; simpl.
1096  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
1097  intro. inv H. exists id0; auto.
1098  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
1099  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
1100Qed.
1101
1102Lemma find_funct_ptr_prop:
1103  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1104  (forall id f, In (id, f) (prog_funct p) → P f) →
1105  find_funct_ptr ? (globalenv p) b = Some ? f →
1106  P f.
1107Proof.
1108  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
1109Qed.
1110
1111Lemma find_funct_inversion:
1112  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1113  find_funct (globalenv p) v = Some ? f →
1114  ∃id. In (id, f) (prog_funct p).
1115Proof.
1116  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
1117  rewrite find_funct_find_funct_ptr ? in H.
1118  eapply find_funct_ptr_inversion; eauto.
1119Qed.
1120
1121Lemma find_funct_prop:
1122  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1123  (forall id f, In (id, f) (prog_funct p) → P f) →
1124  find_funct (globalenv p) v = Some ? f →
1125  P f.
1126Proof.
1127  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
1128Qed.
1129
1130Lemma find_funct_ptr_symbol_inversion:
1131  forall (p: program F V) (id: ident) (b: block) (f: F),
1132  find_symbol ? (globalenv p) id = Some ? b →
1133  find_funct_ptr ? (globalenv p) b = Some ? f →
1134  In (id, f) p.(prog_funct).
1135Proof.
1136  intros until f.
1137  assert (forall fns,
1138           let g := add_functs empty fns in
1139           PTree.get id g.(symbols) = Some ? b →
1140           ZMap.get b g.(functions) = Some ? f →
1141           In (id, f) fns).
1142    induction fns; simpl.
1143    rewrite ZMap.gi. congruence.
1144    set (g := add_functs empty fns).
1145    rewrite PTree.gsspec. rewrite ZMap.gsspec.
1146    case (peq id (fst a)); intro.
1147    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
1148    intro EQ2. left. destruct a. simpl in *. congruence.
1149    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
1150    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
1151  assert (forall g0 m0, b < 0 →
1152          forall vars g m,
1153          add_globals (g0, m0) vars = (g, m) →
1154          PTree.get id g.(symbols) = Some ? b →
1155          PTree.get id g0.(symbols) = Some ? b).
1156    induction vars; simpl.
1157    intros. inv H1. auto.
1158    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
1159    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
1160    unfold add_symbol; intros A B. rewrite <- B. simpl.
1161    rewrite PTree.gsspec. case (peq id id1); intros.
1162    assert (b > 0). inv H1. apply nextblock_pos.
1163    omegaContradiction.
1164    eauto.
1165  intros.
1166  generalize (find_funct_ptr_negative _ _ H2). intro.
1167  pose (g := add_functs empty (prog_funct p)).
1168  apply H. 
1169  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
1170  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
1171  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
1172Qed.
1173
1174Theorem find_symbol_not_nullptr:
1175  forall (p: program F V) (id: ident) (b: block),
1176  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
1177Proof.
1178  intros until b.
1179  assert (forall fns,
1180          find_symbol ? (add_functs empty fns) id = Some ? b →
1181          b <> nullptr).
1182    unfold find_symbol; induction fns; simpl.
1183    rewrite PTree.gempty. congruence.
1184    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
1185    destruct (peq id id1); intros.
1186    inversion H. generalize (nextfunction_add_functs_neg fns).
1187    unfold block, nullptr; omega.
1188    auto.
1189  set (g0 := add_functs empty p.(prog_funct)).
1190  assert (forall vars g m,
1191          add_globals (g0, Mem.empty) vars = (g, m) →
1192          find_symbol ? g id = Some ? b →
1193          b <> nullptr).
1194    induction vars; simpl; intros until m.
1195    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
1196    destruct a as [[id1 init1] info1].
1197    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
1198    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
1199    destruct (peq id id1); intros.
1200    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
1201    eauto.
1202  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
1203Qed.
1204
1205Theorem global_addresses_distinct:
1206  forall (p: program F V) id1 id2 b1 b2,
1207  id1<>id2 →
1208  find_symbol ? (globalenv p) id1 = Some ? b1 →
1209  find_symbol ? (globalenv p) id2 = Some ? b2 →
1210  b1<>b2.
1211Proof.
1212  intros.
1213  assert (forall fns,
1214    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
1215    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
1216    b1 <> b2).
1217  unfold find_symbol. induction fns; simpl; intros.
1218  rewrite PTree.gempty in H2. discriminate.
1219  destruct a as [id f]; simpl in *.
1220  rewrite PTree.gsspec in H2.
1221  destruct (peq id1 id). subst id. inv H2.
1222  rewrite PTree.gso in H3; auto.
1223  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
1224  rewrite PTree.gsspec in H3.
1225  destruct (peq id2 id). subst id. inv H3.
1226  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
1227  eauto.
1228  set (ge0 := add_functs empty p.(prog_funct)).
1229  assert (forall (vars: list (ident * list init_data * V)) ge m,
1230    add_globals (ge0, Mem.empty) vars = (ge, m) →
1231    find_symbol ? ge id1 = Some ? b1 →
1232    find_symbol ? ge id2 = Some ? b2 →
1233    b1 <> b2).
1234  unfold find_symbol. induction vars; simpl.
1235  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
1236  intros ge m. destruct a as [[id init] info].
1237  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
1238  unfold add_symbol. simpl. intros.
1239  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
1240  rewrite PTree.gso in H4; auto.
1241  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
1242  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
1243  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
1244  eauto.
1245  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
1246  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
1247  fold ge_m. apply surjective_pairing. auto. auto.
1248Qed.
1249
1250End GENV.
1251
1252(* Global environments and program transformations. *)
1253
1254Section MATCH_PROGRAM.
1255
1256Variable A B V W: Type.
1257Variable match_fun: A → B → Prop.
1258Variable match_var: V → W → Prop.
1259Variable p: program A V.
1260Variable p': program B W.
1261Hypothesis match_prog:
1262  match_program match_fun match_var p p'.
1263
1264Lemma add_functs_match:
1265  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1266  list_forall2 (match_funct_etry match_fun) fns tfns →
1267  let r := add_functs (empty A) fns in
1268  let tr := add_functs (empty B) tfns in
1269  nextfunction tr = nextfunction r /\
1270  symbols tr = symbols r /\
1271  forall (b: block) (f: A),
1272  ZMap.get b (functions r) = Some ? f →
1273  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
1274Proof.
1275  induction 1; simpl.
1276
1277  split. reflexivity. split. reflexivity.
1278  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1279
1280  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1281  simpl. red in H. destruct H.
1282  destruct IHlist_forall2 as [X [Y Z]].
1283  rewrite X. rewrite Y. 
1284  split. auto.
1285  split. congruence.
1286  intros b f.
1287  repeat (rewrite ZMap.gsspec).
1288  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1289  intro EQ; inv EQ. exists fn2; auto.
1290  auto.
1291Qed.
1292
1293Lemma add_functs_rev_match:
1294  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1295  list_forall2 (match_funct_etry match_fun) fns tfns →
1296  let r := add_functs (empty A) fns in
1297  let tr := add_functs (empty B) tfns in
1298  nextfunction tr = nextfunction r /\
1299  symbols tr = symbols r /\
1300  forall (b: block) (tf: B),
1301  ZMap.get b (functions tr) = Some ? tf →
1302  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
1303Proof.
1304  induction 1; simpl.
1305
1306  split. reflexivity. split. reflexivity.
1307  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1308
1309  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1310  simpl. red in H. destruct H.
1311  destruct IHlist_forall2 as [X [Y Z]].
1312  rewrite X. rewrite Y. 
1313  split. auto.
1314  split. congruence.
1315  intros b f.
1316  repeat (rewrite ZMap.gsspec).
1317  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1318  intro EQ; inv EQ. exists fn1; auto.
1319  auto.
1320Qed.
1321
1322Lemma mem_add_globals_match:
1323  forall (g1: genv A) (g2: genv B) (m: mem)
1324         (vars: list (ident * list init_data * V))
1325         (tvars: list (ident * list init_data * W)),
1326  list_forall2 (match_var_etry match_var) vars tvars →
1327  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
1328Proof.
1329  induction 1; simpl.
1330  auto.
1331  destruct a1 as [[id1 init1] info1].
1332  destruct b1 as [[id2 init2] info2].
1333  red in H. destruct H as [X [Y Z]]. subst id2 init2.
1334  generalize IHlist_forall2.
1335  destruct (add_globals (g1, m) al).
1336  destruct (add_globals (g2, m) bl).
1337  simpl. intro. subst m1. auto.
1338Qed.
1339
1340Lemma symbols_add_globals_match:
1341  forall (g1: genv A) (g2: genv B) (m: mem),
1342  symbols g1 = symbols g2 →
1343  forall (vars: list (ident * list init_data * V))
1344         (tvars: list (ident * list init_data * W)),
1345  list_forall2 (match_var_etry match_var) vars tvars →
1346  symbols (fst (add_globals (g1, m) vars)) =
1347  symbols (fst (add_globals (g2, m) tvars)).
1348Proof.
1349  induction 2; simpl.
1350  auto.
1351  destruct a1 as [[id1 init1] info1].
1352  destruct b1 as [[id2 init2] info2].
1353  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
1354  generalize IHlist_forall2.
1355  generalize (mem_add_globals_match g1 g2 m H1).
1356  destruct (add_globals (g1, m) al).
1357  destruct (add_globals (g2, m) bl).
1358  simpl. intros. congruence.
1359Qed.
1360
1361Theorem find_funct_ptr_match:
1362  forall (b: block) (f: A),
1363  find_funct_ptr ? (globalenv p) b = Some ? f →
1364  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
1365Proof.
1366  intros until f. destruct match_prog as [X [Y Z]].
1367  destruct (add_functs_match X) as [P [Q R]].
1368  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1369  auto.
1370Qed.
1371
1372Theorem find_funct_ptr_rev_match:
1373  forall (b: block) (tf: B),
1374  find_funct_ptr ? (globalenv p') b = Some ? tf →
1375  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
1376Proof.
1377  intros until tf. destruct match_prog as [X [Y Z]].
1378  destruct (add_functs_rev_match X) as [P [Q R]].
1379  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1380  auto.
1381Qed.
1382
1383Theorem find_funct_match:
1384  forall (v: val) (f: A),
1385  find_funct (globalenv p) v = Some ? f →
1386  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
1387Proof.
1388  intros until f. unfold find_funct.
1389  case v; try (intros; discriminate).
1390  intros b ofs.
1391  case (Int.eq ofs Int.zero); try (intros; discriminate).
1392  apply find_funct_ptr_match.
1393Qed.
1394
1395Theorem find_funct_rev_match:
1396  forall (v: val) (tf: B),
1397  find_funct (globalenv p') v = Some ? tf →
1398  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
1399Proof.
1400  intros until tf. unfold find_funct.
1401  case v; try (intros; discriminate).
1402  intros b ofs.
1403  case (Int.eq ofs Int.zero); try (intros; discriminate).
1404  apply find_funct_ptr_rev_match.
1405Qed.
1406
1407Lemma symbols_init_match:
1408  symbols (globalenv p') = symbols (globalenv p).
1409Proof.
1410  unfold globalenv. unfold globalenv_initmem.
1411  destruct match_prog as [X [Y Z]].
1412  destruct (add_functs_match X) as [P [Q R]].
1413  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
1414Qed.
1415
1416Theorem find_symbol_match:
1417  forall (s: ident),
1418  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1419Proof.
1420  intros. unfold find_symbol.
1421  rewrite symbols_init_match. auto.
1422Qed.
1423
1424Theorem init_mem_match:
1425  init_mem p' = init_mem p.
1426Proof.
1427  unfold init_mem. unfold globalenv_initmem.
1428  destruct match_prog as [X [Y Z]].
1429  symmetry. apply mem_add_globals_match. auto.
1430Qed.
1431
1432End MATCH_PROGRAM.
1433
1434Section TRANSF_PROGRAM_PARTIAL2.
1435
1436Variable A B V W: Type.
1437Variable transf_fun: A → res B.
1438Variable transf_var: V → res W.
1439Variable p: program A V.
1440Variable p': program B W.
1441Hypothesis transf_OK:
1442  transform_partial_program2 transf_fun transf_var p = OK ? p'.
1443
1444Remark prog_match:
1445  match_program
1446    (fun fd tfd => transf_fun fd = OK ? tfd)
1447    (fun info tinfo => transf_var info = OK ? tinfo)
1448    p p'.
1449Proof.
1450  apply transform_partial_program2_match; auto.
1451Qed.
1452
1453Theorem find_funct_ptr_transf_partial2:
1454  forall (b: block) (f: A),
1455  find_funct_ptr ? (globalenv p) b = Some ? f →
1456  ∃f'.
1457  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1458Proof.
1459  intros.
1460  exploit find_funct_ptr_match. eexact prog_match. eauto.
1461  intros [tf [X Y]]. exists tf; auto.
1462Qed.
1463
1464Theorem find_funct_ptr_rev_transf_partial2:
1465  forall (b: block) (tf: B),
1466  find_funct_ptr ? (globalenv p') b = Some ? tf →
1467  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1468Proof.
1469  intros.
1470  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1471Qed.
1472
1473Theorem find_funct_transf_partial2:
1474  forall (v: val) (f: A),
1475  find_funct (globalenv p) v = Some ? f →
1476  ∃f'.
1477  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1478Proof.
1479  intros.
1480  exploit find_funct_match. eexact prog_match. eauto.
1481  intros [tf [X Y]]. exists tf; auto.
1482Qed.
1483
1484Theorem find_funct_rev_transf_partial2:
1485  forall (v: val) (tf: B),
1486  find_funct (globalenv p') v = Some ? tf →
1487  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1488Proof.
1489  intros.
1490  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1491Qed.
1492
1493Theorem find_symbol_transf_partial2:
1494  forall (s: ident),
1495  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1496Proof.
1497  intros. eapply find_symbol_match. eexact prog_match.
1498Qed.
1499
1500Theorem init_mem_transf_partial2:
1501  init_mem p' = init_mem p.
1502Proof.
1503  intros. eapply init_mem_match. eexact prog_match.
1504Qed.
1505
1506End TRANSF_PROGRAM_PARTIAL2.
1507
1508Section TRANSF_PROGRAM_PARTIAL.
1509
1510Variable A B V: Type.
1511Variable transf: A → res B.
1512Variable p: program A V.
1513Variable p': program B V.
1514Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1515
1516Remark transf2_OK:
1517  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1518Proof.
1519  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1520  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1521  rewrite map_partial_identity; auto.
1522Qed.
1523
1524Theorem find_funct_ptr_transf_partial:
1525  forall (b: block) (f: A),
1526  find_funct_ptr ? (globalenv p) b = Some ? f →
1527  ∃f'.
1528  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1529Proof.
1530  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1531Qed.
1532
1533Theorem find_funct_ptr_rev_transf_partial:
1534  forall (b: block) (tf: B),
1535  find_funct_ptr ? (globalenv p') b = Some ? tf →
1536  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1537Proof.
1538  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1539Qed.
1540
1541Theorem find_funct_transf_partial:
1542  forall (v: val) (f: A),
1543  find_funct (globalenv p) v = Some ? f →
1544  ∃f'.
1545  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1546Proof.
1547  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1548Qed.
1549
1550Theorem find_funct_rev_transf_partial:
1551  forall (v: val) (tf: B),
1552  find_funct (globalenv p') v = Some ? tf →
1553  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1554Proof.
1555  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1556Qed.
1557
1558Theorem find_symbol_transf_partial:
1559  forall (s: ident),
1560  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1561Proof.
1562  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1563Qed.
1564
1565Theorem init_mem_transf_partial:
1566  init_mem p' = init_mem p.
1567Proof.
1568  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1569Qed.
1570
1571End TRANSF_PROGRAM_PARTIAL.
1572
1573Section TRANSF_PROGRAM.
1574
1575Variable A B V: Type.
1576Variable transf: A → B.
1577Variable p: program A V.
1578Let tp := transform_program transf p.
1579
1580Remark transf_OK:
1581  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1582Proof.
1583  unfold tp, transform_program, transform_partial_program.
1584  rewrite map_partial_total. reflexivity.
1585Qed.
1586
1587Theorem find_funct_ptr_transf:
1588  forall (b: block) (f: A),
1589  find_funct_ptr ? (globalenv p) b = Some ? f →
1590  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1591Proof.
1592  intros.
1593  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1594  as [f' [X Y]]. congruence.
1595Qed.
1596
1597Theorem find_funct_ptr_rev_transf:
1598  forall (b: block) (tf: B),
1599  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1600  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1601Proof.
1602  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1603  intros [f [X Y]]. exists f; split. auto. congruence.
1604Qed.
1605
1606Theorem find_funct_transf:
1607  forall (v: val) (f: A),
1608  find_funct (globalenv p) v = Some ? f →
1609  find_funct (globalenv tp) v = Some ? (transf f).
1610Proof.
1611  intros.
1612  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1613  as [f' [X Y]]. congruence.
1614Qed.
1615
1616Theorem find_funct_rev_transf:
1617  forall (v: val) (tf: B),
1618  find_funct (globalenv tp) v = Some ? tf →
1619  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
1620Proof.
1621  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1622  intros [f [X Y]]. exists f; split. auto. congruence.
1623Qed.
1624
1625Theorem find_symbol_transf:
1626  forall (s: ident),
1627  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1628Proof.
1629  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1630Qed.
1631
1632Theorem init_mem_transf:
1633  init_mem tp = init_mem p.
1634Proof.
1635  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1636Qed.
1637
1638End TRANSF_PROGRAM.
1639
1640End Genv.
1641*)
1642
Note: See TracBrowser for help on using the repository browser.