source: src/common/Globalenvs.ma @ 2319

Last change on this file since 2319 was 2319, checked in by campbell, 7 years ago

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

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