source: src/common/Globalenvs.ma @ 2107

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

Memory initialisation and program transformations.

File size: 63.3 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 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
286lemma 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
305lemma 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
313qed.
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
492let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝
493match n with
494[ O ⇒ p
495| S m ⇒ succ (nat_plus_pos m p)
496].
497
498lemma 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
501whd in ⊢ (??%%); >IH //
502qed.
503
504(* Now link functions in related programs, but without dealing with the type
505   casts yet. *)
506
507lemma 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
512cases 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
516letin varnames ≝ (map ??? vars)
517cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?)
518//
519cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?))
520//
521generalize in match (empty ?);
522generalize in match (empty ?);
523generalize in match fns';
524elim 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
551discriminator Prod.
552
553(* Now prove the full version. *)
554
555lemma 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)
568lapply (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
573normalize #H @(match_funct_entry_inv … H) //
574qed.
575
576lemma
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
586cases (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' %
591qed.
592
593lemma 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 * //
596qed.
597
598lemma
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
608whd in ⊢ (??%%);
609@sym_eq
610@(eq_f ??(λx. lookup SymbolTag block x s))
611whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
612whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
613change with (add_globals ?????) in match (foldl ?????);
614change 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 
621lemma
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
632qed.
633
634lemma
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
641cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP)
642[ 2: @iV
643| #f' * #FFP'
644  generalize in match (matching_vars ????);
645  whd in match (prog_var_names ???); whd in match (prog_vars ???);
646  #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' %
647] qed.
648
649lemma
650  find_funct_transf:
651    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
652    ∀v: val. ∀f: A ?.
653    find_funct ? (globalenv … iV p) v = Some ? f →
654    find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f).
655#A #B #V #iV #tf #p #v #f #FF
656cases (find_funct_find_funct_ptr ???? FF)
657#r * #b * #pc * #E destruct #FFP
658change with (find_funct_ptr ???) in ⊢ (??%?);
659@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
660qed.
661
662lemma
663  find_symbol_transf:
664    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
665    ∀s: ident.
666    find_symbol ? (globalenv … iV (transform_program … p transf)) s =
667    find_symbol ? (globalenv … iV p) s.
668#A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?))
669#v0 #w0 * //
670qed.
671
672lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d.
673  symbols A ge = symbols … ge' →
674  store_init_data A ge m b o d = store_init_data B ge' m b o d.
675#A #B #ge #ge' #m #b #o #d #SYM
676whd in ⊢ (??%%);
677cases d #d' try @refl
678#id #n whd in ⊢ (??%%);
679whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
680qed.
681
682lemma store_init_data_list_symbols : ∀A,B,ge,ge',b.
683  symbols A ge = symbols … ge' →
684  ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d.
685#A #B #ge #ge' #b #SYM #d elim d
686[ //
687| #hd #tl #IH #m #o
688  whd in ⊢ (??%%);
689  >(store_init_data_symbols … SYM)
690  cases (store_init_data ??????)
691  [ %
692  | #m' @IH
693  ]
694] qed.
695
696lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop.
697  ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) →
698  ∀ge:genv_t A. ∀ge':genv_t B.
699  symbols … ge = symbols … ge' →
700   ∀m. ∀vars,vars'.
701  All2 … P vars vars' →
702  init_globals A V iV ge m vars = init_globals B W iW ge' m vars'.
703#A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars
704whd in ⊢ (? → ? → ??%%);
705generalize in match (OK ? m);
706elim vars
707[ #rm *
708  [ #_ %
709  | #h #t *
710  ]
711| * #idr #v #tl #IH #rm
712  * [ * ]
713  * #idr' #w #tl'
714  * #p cases (varsOK … p) #E1 #E2 destruct #TL
715  whd in ⊢ (??%%); cases idr' #id #r cases rm #m'
716  whd in ⊢ (??(????%?)(????%?));
717  [ whd in match (find_symbol ?? id);
718    whd in match (find_symbol B ? id);
719    >SYM cases (lookup ??? id)
720    [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ]
721  ] @IH //
722] qed.
723
724lemma
725  init_mem_match:
726    ∀M:matching.
727    ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) →
728    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
729    match_program … M p p' →
730    init_mem … iW p' = init_mem … iV p.
731* #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain
732whd in ⊢ (??%%);
733change with (add_globals ?????) in match (globalenv_allocmem ??? p');
734change with (add_globals ?????) in match (globalenv_allocmem ??? p);
735cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars)
736[ 8: @(matching_fns_get_same_blocks … Mfns)
737     #f0 #g0 * //
738| cases (add_globals ?????) #ge1 #m1
739  cases (add_globals ?????) #ge2 #m2
740  #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars)
741  [ #v0 #w0 * #id #r #v #w /3/
742  | @SYM
743  ]
744| 4: #v0 #w0 * #id #r #v #w #V % // >iSAME //
745| *: skip
746] qed.
747
748lemma
749  init_mem_transf:
750    ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V.
751    init_mem … iV (transform_program … p transf) = init_mem … iV p.
752#A #B #C #iV #transf #p
753@(init_mem_match … (transform_program_match … transf ?))
754//
755qed.
756   
757
758(* Package up transform_program results for global envs nicely. *)
759
760record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
761  rg_find_symbol: ∀s.
762    find_symbol … ge s = find_symbol … ge' s;
763  rg_find_funct: ∀v,f.
764    find_funct … ge v = Some ? f →
765    find_funct … ge' v = Some ? (t f);
766  rg_find_funct_ptr: ∀b,f.
767    find_funct_ptr … ge b = Some ? f →
768    find_funct_ptr … ge' b = Some ? (t f)
769}.
770
771theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
772  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
773#A #B #V #iV #p #tf %
774[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
775| @(find_funct_transf A B V iV tf p)
776| @(find_funct_ptr_transf A B V iV p tf)
777] qed.
778
779
780(*
781
782  find_funct_ptr_match:
783    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
784           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
785    match_program … match_fun match_var p p' →
786    ∀b: block. ∀f: A.
787    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
788    ∃tf : B.
789    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
790  find_funct_ptr_rev_match:
791    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
792           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
793    match_program … match_fun match_var p p' →
794    ∀b: block. ∀tf: B.
795    find_funct_ptr ? (globalenv ?? p') b = Some ? tf →
796    ∃f : A.
797    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
798  find_funct_match:
799    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
800           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
801    match_program … match_fun match_var p p' →
802    ∀v: val. ∀f: A.
803    find_funct ? (globalenv ?? p) v = Some ? f →
804    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
805  find_funct_rev_match:
806    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
807           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
808    match_program … match_fun match_var p p' →
809    ∀v: val. ∀tf: B.
810    find_funct ? (globalenv ?? p') v = Some ? tf →
811    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
812  find_symbol_match:
813    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
814           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
815    match_program … match_fun match_var p p' →
816    ∀s: ident.
817    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
818*)
819(*
820Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
821  ZMap.get b g.(functions).
822
823Definition find_funct (g: genv) (v: val) : option F :=
824  match v with
825  | Vptr b ofs =>
826      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
827  | _ =>
828      None
829  end.
830
831Definition find_symbol ? (g: genv) (symb: ident) : option block :=
832  PTree.get symb g.(symbols).
833
834Lemma find_funct_inv:
835  forall (ge: t) (v: val) (f: F),
836  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
837Proof.
838  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
839  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
840  exists b. congruence.
841  discriminate.
842Qed.
843
844Lemma find_funct_find_funct_ptr:
845  forall (ge: t) (b: block),
846  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
847Proof.
848  intros. simpl.
849  generalize (Int.eq_spec Int.zero Int.zero).
850  case (Int.eq Int.zero Int.zero); intros.
851  auto. tauto.
852Qed.
853*)
854
855(*
856##[ #A B C transf p b f; elim p; #fns main vars;
857    elim fns;
858    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
859    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
860        nrewrite > (?:nextfunction ?? = length ? t);
861        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
862            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
863        ##| nrewrite > (?:nextfunction ?? = length ? t);
864          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
865              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
866          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
867            ##[ #H; destruct (H); //;
868            ##| #H; napply IH; napply H;
869            ##]
870          ##]
871        ##]
872    ##]
873##| #A B C transf p v f; elim v;
874    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
875    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
876    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
877        whd in ⊢ (??%? → ??%?);
878        ##[ elim p; #fns main vars; elim fns;
879          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
880          ##| #h t; elim h; #f fn IH;
881              whd in ⊢ (??%? → ??%?);
882              nrewrite > (?:nextfunction ?? = length ? t);
883              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
884                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
885              ##| nrewrite > (?:nextfunction ?? = length ? t);
886                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
887                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
888                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
889                  ##[ destruct (H); //;
890                  ##| napply IH; napply H;
891                  ##]
892                ##]
893              ##]
894          ##]
895       ##| #H; destruct;
896       ##]
897    ##]
898##| #A B C transf p id; elim p; #fns main vars;
899    elim fns;
900    ##[ normalize; //
901    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
902        elim (ident_eq fid id); #e;
903        ##[ whd in ⊢ (??%%);
904          nrewrite > (?:nextfunction ?? = length ? t);
905          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
906              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
907          ##| nrewrite > (?:nextfunction ?? = length ? t);
908            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
909                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
910            ##| //
911            ##]
912          ##]
913        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
914        ##]
915    ##]
916##| //;
917##| #A B C transf p b tf; elim p; #fns main vars;
918    elim fns;
919    ##[ normalize; #H; destruct;
920    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
921        nrewrite > (?:nextfunction ?? = length ? t);
922        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
923            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
924        ##| nrewrite > (?:nextfunction ?? = length ? t);
925          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
926              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
927          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
928            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
929            ##| #H; napply IH; napply H;
930            ##]
931          ##]
932        ##]
933    ##]
934##| #A B C transf p v tf; elim p; #fns main vars; elim v;
935  ##[ normalize; #H; destruct;
936  ##| ##2,3: #x; normalize; #H; destruct;
937  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
938    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
939      elim fns;
940      ##[ normalize; #H; destruct;
941      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
942          nrewrite > (?:nextfunction ?? = length ? t);
943          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
944              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
945          ##| nrewrite > (?:nextfunction ?? = length ? t);
946            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
947                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
948            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
949              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
950              ##| #H; napply IH; napply H;
951              ##]
952            ##]
953          ##]
954      ##]
955    ##| normalize; #H; destruct;
956    ##]
957 ##]
958##] qed.
959         
960
961Lemma functions_globalenv:
962  forall (p: program F V),
963  functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
964Proof.
965  assert (forall init vars,
966     functions (fst (add_globals init vars)) = functions (fst init)).
967  induction vars; simpl.
968  reflexivity.
969  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
970  simpl. exact IHvars.
971
972  unfold add_globals; simpl.
973  intros. unfold globalenv; unfold globalenv_initmem.
974  rewrite H. reflexivity.
975Qed.
976
977Lemma initmem_nullptr:
978  forall (p: program F V),
979  let m := init_mem p in
980  valid_block m nullptr /\
981  m.(blocks) nullptr = mkblock 0 0 (fun y => Undef).
982Proof.
983  pose (P := fun m => valid_block m nullptr /\
984        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)).
985  assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))).
986  induction vars; simpl; intros.
987  auto.
988  destruct a as [[id1 in1] inf1].
989  destruct (add_globals init vars) as [g st].
990  simpl in *. destruct IHvars. split.
991  red; simpl. red in H0. omega.
992  simpl. rewrite update_o. auto. unfold block. red in H0. omega.
993
994  intro. unfold init_mem, globalenv_initmem. apply H.
995  red; simpl. split. compute. auto. reflexivity.
996Qed.
997
998Lemma initmem_inject_neutral:
999  forall (p: program F V),
1000  mem_inject_neutral (init_mem p).
1001Proof.
1002  assert (forall g0 vars g1 m,
1003      add_globals (g0, Mem.empty) vars = (g1, m) →
1004      mem_inject_neutral m).
1005  Opaque alloc_init_data.
1006  induction vars; simpl.
1007  intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H).
1008  simpl in H1. rewrite Mem.getN_init in H1.
1009  replace v with Vundef. auto. destruct chunk; simpl in H1; auto.
1010  destruct a as [[id1 init1] info1].
1011  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ.
1012  caseEq (alloc_init_data m1 init1). intros m2 b ALLOC.
1013  intros. inv H.
1014  eapply Mem.alloc_init_data_neutral; eauto.
1015  intros. caseEq (globalenv_initmem p). intros g m EQ.
1016  unfold init_mem; rewrite EQ; simpl.
1017  unfold globalenv_initmem in EQ. eauto.
1018Qed.     
1019
1020Remark nextfunction_add_functs_neg:
1021  forall fns, nextfunction (add_functs empty fns) < 0.
1022Proof.
1023  induction fns; simpl; intros. omega. unfold Zpred. omega.
1024Qed.
1025
1026Theorem find_funct_ptr_negative:
1027  forall (p: program F V) (b: block) (f: F),
1028  find_funct_ptr ? (globalenv p) b = Some ? f → b < 0.
1029Proof.
1030  intros until f.
1031  assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0).
1032    induction fns; simpl.
1033    rewrite ZMap.gi. congruence.
1034    rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro.
1035    intro. rewrite e. apply nextfunction_add_functs_neg.
1036    auto.
1037  unfold find_funct_ptr. rewrite functions_globalenv.
1038  intros. eauto.
1039Qed.
1040
1041Remark find_symbol_add_functs_negative:
1042  forall (fns: list (ident * F)) s b,
1043  (symbols (add_functs empty fns)) ! s = Some ? b → b < 0.
1044Proof.
1045  induction fns; simpl; intros until b.
1046  rewrite PTree.gempty. congruence.
1047  rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro.
1048  intro EQ; inversion EQ. apply nextfunction_add_functs_neg.
1049  eauto.
1050Qed.
1051
1052Remark find_symbol_add_symbols_not_fresh:
1053  forall fns vars g m s b,
1054  add_globals (add_functs empty fns, Mem.empty) vars = (g, m) →
1055  (symbols g)!s = Some ? b →
1056  b < nextblock m.
1057Proof.
1058  induction vars; simpl; intros until b.
1059  intros. inversion H. subst g m. simpl.
1060  generalize (find_symbol_add_functs_negative fns s H0). omega.
1061  Transparent alloc_init_data.
1062  destruct a as [[id1 init1] info1].
1063  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
1064  intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
1065  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
1066  intro EQ; inversion EQ. omega.
1067  intro. generalize (IHvars _ _ _ _ ADG H). omega.
1068Qed.
1069
1070Theorem find_symbol_not_fresh:
1071  forall (p: program F V) (id: ident) (b: block),
1072  find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p).
1073Proof.
1074  intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
1075  caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty)
1076                      (prog_vars p)); intros g m EQ.
1077  simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto.
1078Qed.
1079
1080Lemma find_symbol_exists:
1081  forall (p: program F V)
1082         (id: ident) (init: list init_data) (v: V),
1083  In (id, init, v) (prog_vars p) →
1084  ∃b. find_symbol ? (globalenv p) id = Some ? b.
1085Proof.
1086  intros until v.
1087  assert (forall initm vl, In (id, init, v) vl →
1088           ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b).
1089  induction vl; simpl; intros.
1090  elim H.
1091  destruct a as [[id0 init0] v0].
1092  caseEq (add_globals initm vl). intros g1 m1 EQ. simpl.
1093  rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto.
1094  elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto.
1095  intros. unfold globalenv, find_symbol, globalenv_initmem. auto.
1096Qed.
1097
1098Remark find_symbol_above_nextfunction:
1099  forall (id: ident) (b: block) (fns: list (ident * F)),
1100  let g := add_functs empty fns in
1101  PTree.get id g.(symbols) = Some ? b →
1102  b > g.(nextfunction).
1103Proof.
1104  induction fns; simpl.
1105  rewrite PTree.gempty. congruence.
1106  rewrite PTree.gsspec. case (peq id (fst a)); intro.
1107  intro EQ. inversion EQ. unfold Zpred. omega.
1108  intros. generalize (IHfns H). unfold Zpred; omega.
1109Qed.
1110
1111Remark find_symbol_add_globals:
1112  forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)),
1113  ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) →
1114  find_symbol ? (fst (add_globals ge_m vars)) id =
1115  find_symbol ? (fst ge_m) id.
1116Proof.
1117  unfold find_symbol; induction vars; simpl; intros.
1118  auto.
1119  destruct a as [[id0 init0] var0]. simpl in *.
1120  caseEq (add_globals ge_m vars); intros ge' m' EQ.
1121  simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars.
1122  apply IHvars. tauto. intuition congruence.
1123Qed.
1124
1125Lemma find_funct_ptr_exists:
1126  forall (p: program F V) (id: ident) (f: F),
1127  list_norepet (prog_funct_names p) →
1128  list_disjoint (prog_funct_names p) (prog_var_names p) →
1129  In (id, f) (prog_funct p) →
1130  ∃b. find_symbol ? (globalenv p) id = Some ? b
1131         /\ find_funct_ptr ? (globalenv p) b = Some ? f.
1132Proof.
1133  intros until f.
1134  assert (forall (fns: list (ident * F)),
1135           list_norepet (map (@fst ident F) fns) →
1136           In (id, f) fns →
1137           ∃b. find_symbol ? (add_functs empty fns) id = Some ? b
1138                   /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f).
1139  unfold find_symbol, find_funct_ptr. induction fns; intros.
1140  elim H0.
1141  destruct a as [id0 f0]; simpl in *. inv H.
1142  unfold add_funct; simpl.
1143  rewrite PTree.gsspec. destruct (peq id id0).
1144  subst id0. econstructor; split. eauto.
1145  replace f0 with f. apply ZMap.gss.
1146  elim H0; intro. congruence. elim H3.
1147  change id with (@fst ident F (id, f)). apply List.in_map. auto.
1148  exploit IHfns; eauto. elim H0; intro. congruence. auto.
1149  intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto.
1150  generalize (find_symbol_above_nextfunction _ _ X).
1151  unfold block; unfold ZIndexed.t; intro; omega.
1152
1153  intros. exploit H; eauto. intros [b [X Y]].
1154  exists b; split.
1155  unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals.
1156  assumption. apply list_disjoint_notin with (prog_funct_names p). assumption.
1157  unfold prog_funct_names. change id with (fst (id, f)).
1158  apply List.in_map; auto.
1159  unfold find_funct_ptr. rewrite functions_globalenv.
1160  assumption.
1161Qed.
1162
1163Lemma find_funct_ptr_inversion:
1164  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1165  find_funct_ptr ? (globalenv p) b = Some ? f →
1166  ∃id. In (id, f) (prog_funct p).
1167Proof.
1168  intros until f.
1169  assert (forall fns: list (ident * F),
1170    find_funct_ptr ? (add_functs empty fns) b = Some ? f →
1171    ∃id. In (id, f) fns).
1172  unfold find_funct_ptr. induction fns; simpl.
1173  rewrite ZMap.gi. congruence.
1174  destruct a as [id0 f0]; simpl.
1175  rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))).
1176  intro. inv H. exists id0; auto.
1177  intro. exploit IHfns; eauto. intros [id A]. exists id; auto.
1178  unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto.
1179Qed.
1180
1181Lemma find_funct_ptr_prop:
1182  forall (P: F → Prop) (p: program F V) (b: block) (f: F),
1183  (forall id f, In (id, f) (prog_funct p) → P f) →
1184  find_funct_ptr ? (globalenv p) b = Some ? f →
1185  P f.
1186Proof.
1187  intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto.
1188Qed.
1189
1190Lemma find_funct_inversion:
1191  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1192  find_funct (globalenv p) v = Some ? f →
1193  ∃id. In (id, f) (prog_funct p).
1194Proof.
1195  intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H.
1196  rewrite find_funct_find_funct_ptr ? in H.
1197  eapply find_funct_ptr_inversion; eauto.
1198Qed.
1199
1200Lemma find_funct_prop:
1201  forall (P: F → Prop) (p: program F V) (v: val) (f: F),
1202  (forall id f, In (id, f) (prog_funct p) → P f) →
1203  find_funct (globalenv p) v = Some ? f →
1204  P f.
1205Proof.
1206  intros. exploit find_funct_inversion; eauto. intros [id A]. eauto.
1207Qed.
1208
1209Lemma find_funct_ptr_symbol_inversion:
1210  forall (p: program F V) (id: ident) (b: block) (f: F),
1211  find_symbol ? (globalenv p) id = Some ? b →
1212  find_funct_ptr ? (globalenv p) b = Some ? f →
1213  In (id, f) p.(prog_funct).
1214Proof.
1215  intros until f.
1216  assert (forall fns,
1217           let g := add_functs empty fns in
1218           PTree.get id g.(symbols) = Some ? b →
1219           ZMap.get b g.(functions) = Some ? f →
1220           In (id, f) fns).
1221    induction fns; simpl.
1222    rewrite ZMap.gi. congruence.
1223    set (g := add_functs empty fns).
1224    rewrite PTree.gsspec. rewrite ZMap.gsspec.
1225    case (peq id (fst a)); intro.
1226    intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true.
1227    intro EQ2. left. destruct a. simpl in *. congruence.
1228    intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto.
1229    generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega.
1230  assert (forall g0 m0, b < 0 →
1231          forall vars g m,
1232          add_globals (g0, m0) vars = (g, m) →
1233          PTree.get id g.(symbols) = Some ? b →
1234          PTree.get id g0.(symbols) = Some ? b).
1235    induction vars; simpl.
1236    intros. inv H1. auto.
1237    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars).
1238    intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
1239    unfold add_symbol; intros A B. rewrite <- B. simpl.
1240    rewrite PTree.gsspec. case (peq id id1); intros.
1241    assert (b > 0). inv H1. apply nextblock_pos.
1242    omegaContradiction.
1243    eauto.
1244  intros.
1245  generalize (find_funct_ptr_negative _ _ H2). intro.
1246  pose (g := add_functs empty (prog_funct p)).
1247  apply H. 
1248  apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p).
1249  auto. unfold globalenv, init_mem. rewrite <- surjective_pairing.
1250  reflexivity. assumption. rewrite <- functions_globalenv. assumption.
1251Qed.
1252
1253Theorem find_symbol_not_nullptr:
1254  forall (p: program F V) (id: ident) (b: block),
1255  find_symbol ? (globalenv p) id = Some ? b → b <> nullptr.
1256Proof.
1257  intros until b.
1258  assert (forall fns,
1259          find_symbol ? (add_functs empty fns) id = Some ? b →
1260          b <> nullptr).
1261    unfold find_symbol; induction fns; simpl.
1262    rewrite PTree.gempty. congruence.
1263    destruct a as [id1 f1]. simpl. rewrite PTree.gsspec.
1264    destruct (peq id id1); intros.
1265    inversion H. generalize (nextfunction_add_functs_neg fns).
1266    unfold block, nullptr; omega.
1267    auto.
1268  set (g0 := add_functs empty p.(prog_funct)).
1269  assert (forall vars g m,
1270          add_globals (g0, Mem.empty) vars = (g, m) →
1271          find_symbol ? g id = Some ? b →
1272          b <> nullptr).
1273    induction vars; simpl; intros until m.
1274    intros. inversion H0. subst g. apply H with (prog_funct p). auto.
1275    destruct a as [[id1 init1] info1].
1276    caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2.
1277    inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec.
1278    destruct (peq id id1); intros.
1279    inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega.
1280    eauto.
1281  intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto.
1282Qed.
1283
1284Theorem global_addresses_distinct:
1285  forall (p: program F V) id1 id2 b1 b2,
1286  id1<>id2 →
1287  find_symbol ? (globalenv p) id1 = Some ? b1 →
1288  find_symbol ? (globalenv p) id2 = Some ? b2 →
1289  b1<>b2.
1290Proof.
1291  intros.
1292  assert (forall fns,
1293    find_symbol ? (add_functs empty fns) id1 = Some ? b1 →
1294    find_symbol ? (add_functs empty fns) id2 = Some ? b2 →
1295    b1 <> b2).
1296  unfold find_symbol. induction fns; simpl; intros.
1297  rewrite PTree.gempty in H2. discriminate.
1298  destruct a as [id f]; simpl in *.
1299  rewrite PTree.gsspec in H2.
1300  destruct (peq id1 id). subst id. inv H2.
1301  rewrite PTree.gso in H3; auto.
1302  generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega.
1303  rewrite PTree.gsspec in H3.
1304  destruct (peq id2 id). subst id. inv H3.
1305  generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega.
1306  eauto.
1307  set (ge0 := add_functs empty p.(prog_funct)).
1308  assert (forall (vars: list (ident * list init_data * V)) ge m,
1309    add_globals (ge0, Mem.empty) vars = (ge, m) →
1310    find_symbol ? ge id1 = Some ? b1 →
1311    find_symbol ? ge id2 = Some ? b2 →
1312    b1 <> b2).
1313  unfold find_symbol. induction vars; simpl.
1314  intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto.
1315  intros ge m. destruct a as [[id init] info].
1316  caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B.
1317  unfold add_symbol. simpl. intros.
1318  rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3.
1319  rewrite PTree.gso in H4; auto.
1320  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega.
1321  rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4.
1322  generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega.
1323  eauto.
1324  set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)).
1325  apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m).
1326  fold ge_m. apply surjective_pairing. auto. auto.
1327Qed.
1328
1329End GENV.
1330
1331(* Global environments and program transformations. *)
1332
1333Section MATCH_PROGRAM.
1334
1335Variable A B V W: Type.
1336Variable match_fun: A → B → Prop.
1337Variable match_var: V → W → Prop.
1338Variable p: program A V.
1339Variable p': program B W.
1340Hypothesis match_prog:
1341  match_program match_fun match_var p p'.
1342
1343Lemma add_functs_match:
1344  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1345  list_forall2 (match_funct_etry match_fun) fns tfns →
1346  let r := add_functs (empty A) fns in
1347  let tr := add_functs (empty B) tfns in
1348  nextfunction tr = nextfunction r /\
1349  symbols tr = symbols r /\
1350  forall (b: block) (f: A),
1351  ZMap.get b (functions r) = Some ? f →
1352  ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf.
1353Proof.
1354  induction 1; simpl.
1355
1356  split. reflexivity. split. reflexivity.
1357  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1358
1359  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1360  simpl. red in H. destruct H.
1361  destruct IHlist_forall2 as [X [Y Z]].
1362  rewrite X. rewrite Y. 
1363  split. auto.
1364  split. congruence.
1365  intros b f.
1366  repeat (rewrite ZMap.gsspec).
1367  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1368  intro EQ; inv EQ. exists fn2; auto.
1369  auto.
1370Qed.
1371
1372Lemma add_functs_rev_match:
1373  forall (fns: list (ident * A)) (tfns: list (ident * B)),
1374  list_forall2 (match_funct_etry match_fun) fns tfns →
1375  let r := add_functs (empty A) fns in
1376  let tr := add_functs (empty B) tfns in
1377  nextfunction tr = nextfunction r /\
1378  symbols tr = symbols r /\
1379  forall (b: block) (tf: B),
1380  ZMap.get b (functions tr) = Some ? tf →
1381  ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf.
1382Proof.
1383  induction 1; simpl.
1384
1385  split. reflexivity. split. reflexivity.
1386  intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
1387
1388  destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2].
1389  simpl. red in H. destruct H.
1390  destruct IHlist_forall2 as [X [Y Z]].
1391  rewrite X. rewrite Y. 
1392  split. auto.
1393  split. congruence.
1394  intros b f.
1395  repeat (rewrite ZMap.gsspec).
1396  destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))).
1397  intro EQ; inv EQ. exists fn1; auto.
1398  auto.
1399Qed.
1400
1401Lemma mem_add_globals_match:
1402  forall (g1: genv A) (g2: genv B) (m: mem)
1403         (vars: list (ident * list init_data * V))
1404         (tvars: list (ident * list init_data * W)),
1405  list_forall2 (match_var_etry match_var) vars tvars →
1406  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
1407Proof.
1408  induction 1; simpl.
1409  auto.
1410  destruct a1 as [[id1 init1] info1].
1411  destruct b1 as [[id2 init2] info2].
1412  red in H. destruct H as [X [Y Z]]. subst id2 init2.
1413  generalize IHlist_forall2.
1414  destruct (add_globals (g1, m) al).
1415  destruct (add_globals (g2, m) bl).
1416  simpl. intro. subst m1. auto.
1417Qed.
1418
1419Lemma symbols_add_globals_match:
1420  forall (g1: genv A) (g2: genv B) (m: mem),
1421  symbols g1 = symbols g2 →
1422  forall (vars: list (ident * list init_data * V))
1423         (tvars: list (ident * list init_data * W)),
1424  list_forall2 (match_var_etry match_var) vars tvars →
1425  symbols (fst (add_globals (g1, m) vars)) =
1426  symbols (fst (add_globals (g2, m) tvars)).
1427Proof.
1428  induction 2; simpl.
1429  auto.
1430  destruct a1 as [[id1 init1] info1].
1431  destruct b1 as [[id2 init2] info2].
1432  red in H0. destruct H0 as [X [Y Z]]. subst id2 init2.
1433  generalize IHlist_forall2.
1434  generalize (mem_add_globals_match g1 g2 m H1).
1435  destruct (add_globals (g1, m) al).
1436  destruct (add_globals (g2, m) bl).
1437  simpl. intros. congruence.
1438Qed.
1439
1440Theorem find_funct_ptr_match:
1441  forall (b: block) (f: A),
1442  find_funct_ptr ? (globalenv p) b = Some ? f →
1443  ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf.
1444Proof.
1445  intros until f. destruct match_prog as [X [Y Z]].
1446  destruct (add_functs_match X) as [P [Q R]].
1447  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1448  auto.
1449Qed.
1450
1451Theorem find_funct_ptr_rev_match:
1452  forall (b: block) (tf: B),
1453  find_funct_ptr ? (globalenv p') b = Some ? tf →
1454  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf.
1455Proof.
1456  intros until tf. destruct match_prog as [X [Y Z]].
1457  destruct (add_functs_rev_match X) as [P [Q R]].
1458  unfold find_funct_ptr. repeat rewrite functions_globalenv.
1459  auto.
1460Qed.
1461
1462Theorem find_funct_match:
1463  forall (v: val) (f: A),
1464  find_funct (globalenv p) v = Some ? f →
1465  ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf.
1466Proof.
1467  intros until f. unfold find_funct.
1468  case v; try (intros; discriminate).
1469  intros b ofs.
1470  case (Int.eq ofs Int.zero); try (intros; discriminate).
1471  apply find_funct_ptr_match.
1472Qed.
1473
1474Theorem find_funct_rev_match:
1475  forall (v: val) (tf: B),
1476  find_funct (globalenv p') v = Some ? tf →
1477  ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf.
1478Proof.
1479  intros until tf. unfold find_funct.
1480  case v; try (intros; discriminate).
1481  intros b ofs.
1482  case (Int.eq ofs Int.zero); try (intros; discriminate).
1483  apply find_funct_ptr_rev_match.
1484Qed.
1485
1486Lemma symbols_init_match:
1487  symbols (globalenv p') = symbols (globalenv p).
1488Proof.
1489  unfold globalenv. unfold globalenv_initmem.
1490  destruct match_prog as [X [Y Z]].
1491  destruct (add_functs_match X) as [P [Q R]].
1492  simpl. symmetry. apply symbols_add_globals_match. auto. auto.
1493Qed.
1494
1495Theorem find_symbol_match:
1496  forall (s: ident),
1497  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1498Proof.
1499  intros. unfold find_symbol.
1500  rewrite symbols_init_match. auto.
1501Qed.
1502
1503Theorem init_mem_match:
1504  init_mem p' = init_mem p.
1505Proof.
1506  unfold init_mem. unfold globalenv_initmem.
1507  destruct match_prog as [X [Y Z]].
1508  symmetry. apply mem_add_globals_match. auto.
1509Qed.
1510
1511End MATCH_PROGRAM.
1512
1513Section TRANSF_PROGRAM_PARTIAL2.
1514
1515Variable A B V W: Type.
1516Variable transf_fun: A → res B.
1517Variable transf_var: V → res W.
1518Variable p: program A V.
1519Variable p': program B W.
1520Hypothesis transf_OK:
1521  transform_partial_program2 transf_fun transf_var p = OK ? p'.
1522
1523Remark prog_match:
1524  match_program
1525    (fun fd tfd => transf_fun fd = OK ? tfd)
1526    (fun info tinfo => transf_var info = OK ? tinfo)
1527    p p'.
1528Proof.
1529  apply transform_partial_program2_match; auto.
1530Qed.
1531
1532Theorem find_funct_ptr_transf_partial2:
1533  forall (b: block) (f: A),
1534  find_funct_ptr ? (globalenv p) b = Some ? f →
1535  ∃f'.
1536  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'.
1537Proof.
1538  intros.
1539  exploit find_funct_ptr_match. eexact prog_match. eauto.
1540  intros [tf [X Y]]. exists tf; auto.
1541Qed.
1542
1543Theorem find_funct_ptr_rev_transf_partial2:
1544  forall (b: block) (tf: B),
1545  find_funct_ptr ? (globalenv p') b = Some ? tf →
1546  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf.
1547Proof.
1548  intros.
1549  exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto.
1550Qed.
1551
1552Theorem find_funct_transf_partial2:
1553  forall (v: val) (f: A),
1554  find_funct (globalenv p) v = Some ? f →
1555  ∃f'.
1556  find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'.
1557Proof.
1558  intros.
1559  exploit find_funct_match. eexact prog_match. eauto.
1560  intros [tf [X Y]]. exists tf; auto.
1561Qed.
1562
1563Theorem find_funct_rev_transf_partial2:
1564  forall (v: val) (tf: B),
1565  find_funct (globalenv p') v = Some ? tf →
1566  ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf.
1567Proof.
1568  intros.
1569  exploit find_funct_rev_match. eexact prog_match. eauto. auto.
1570Qed.
1571
1572Theorem find_symbol_transf_partial2:
1573  forall (s: ident),
1574  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1575Proof.
1576  intros. eapply find_symbol_match. eexact prog_match.
1577Qed.
1578
1579Theorem init_mem_transf_partial2:
1580  init_mem p' = init_mem p.
1581Proof.
1582  intros. eapply init_mem_match. eexact prog_match.
1583Qed.
1584
1585End TRANSF_PROGRAM_PARTIAL2.
1586
1587Section TRANSF_PROGRAM_PARTIAL.
1588
1589Variable A B V: Type.
1590Variable transf: A → res B.
1591Variable p: program A V.
1592Variable p': program B V.
1593Hypothesis transf_OK: transform_partial_program transf p = OK ? p'.
1594
1595Remark transf2_OK:
1596  transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'.
1597Proof.
1598  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
1599  destruct (map_partial prefix_funct_name transf (prog_funct p)); auto.
1600  rewrite map_partial_identity; auto.
1601Qed.
1602
1603Theorem find_funct_ptr_transf_partial:
1604  forall (b: block) (f: A),
1605  find_funct_ptr ? (globalenv p) b = Some ? f →
1606  ∃f'.
1607  find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'.
1608Proof.
1609  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1610Qed.
1611
1612Theorem find_funct_ptr_rev_transf_partial:
1613  forall (b: block) (tf: B),
1614  find_funct_ptr ? (globalenv p') b = Some ? tf →
1615  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf.
1616Proof.
1617  exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1618Qed.
1619
1620Theorem find_funct_transf_partial:
1621  forall (v: val) (f: A),
1622  find_funct (globalenv p) v = Some ? f →
1623  ∃f'.
1624  find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'.
1625Proof.
1626  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1627Qed.
1628
1629Theorem find_funct_rev_transf_partial:
1630  forall (v: val) (tf: B),
1631  find_funct (globalenv p') v = Some ? tf →
1632  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf.
1633Proof.
1634  exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1635Qed.
1636
1637Theorem find_symbol_transf_partial:
1638  forall (s: ident),
1639  find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s.
1640Proof.
1641  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1642Qed.
1643
1644Theorem init_mem_transf_partial:
1645  init_mem p' = init_mem p.
1646Proof.
1647  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
1648Qed.
1649
1650End TRANSF_PROGRAM_PARTIAL.
1651
1652Section TRANSF_PROGRAM.
1653
1654Variable A B V: Type.
1655Variable transf: A → B.
1656Variable p: program A V.
1657Let tp := transform_program transf p.
1658
1659Remark transf_OK:
1660  transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp.
1661Proof.
1662  unfold tp, transform_program, transform_partial_program.
1663  rewrite map_partial_total. reflexivity.
1664Qed.
1665
1666Theorem find_funct_ptr_transf:
1667  forall (b: block) (f: A),
1668  find_funct_ptr ? (globalenv p) b = Some ? f →
1669  find_funct_ptr ? (globalenv tp) b = Some ? (transf f).
1670Proof.
1671  intros.
1672  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1673  as [f' [X Y]]. congruence.
1674Qed.
1675
1676Theorem find_funct_ptr_rev_transf:
1677  forall (b: block) (tf: B),
1678  find_funct_ptr ? (globalenv tp) b = Some ? tf →
1679  ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf.
1680Proof.
1681  intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto.
1682  intros [f [X Y]]. exists f; split. auto. congruence.
1683Qed.
1684
1685Theorem find_funct_transf:
1686  forall (v: val) (f: A),
1687  find_funct (globalenv p) v = Some ? f →
1688  find_funct (globalenv tp) v = Some ? (transf f).
1689Proof.
1690  intros.
1691  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H)
1692  as [f' [X Y]]. congruence.
1693Qed.
1694
1695Theorem find_funct_rev_transf:
1696  forall (v: val) (tf: B),
1697  find_funct (globalenv tp) v = Some ? tf →
1698  ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf.
1699Proof.
1700  intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto.
1701  intros [f [X Y]]. exists f; split. auto. congruence.
1702Qed.
1703
1704Theorem find_symbol_transf:
1705  forall (s: ident),
1706  find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s.
1707Proof.
1708  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
1709Qed.
1710
1711Theorem init_mem_transf:
1712  init_mem tp = init_mem p.
1713Proof.
1714  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
1715Qed.
1716
1717End TRANSF_PROGRAM.
1718
1719End Genv.
1720*)
1721
Note: See TracBrowser for help on using the repository browser.