[3] | 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 | |
---|
[700] | 36 | include "common/Errors.ma". |
---|
[747] | 37 | include "common/AST.ma". |
---|
[474] | 38 | (*include "Values.ma".*) |
---|
[1993] | 39 | include "common/FrontEndMem.ma". |
---|
[3] | 40 | |
---|
[1986] | 41 | (* * The type of global environments. The parameter [F] is the type |
---|
| 42 | of function descriptions. *) |
---|
| 43 | (* Functions are given negative block numbers *) |
---|
| 44 | record genv_t (F:Type[0]) : Type[0] ≝ { |
---|
[2010] | 45 | functions: positive_map F; |
---|
| 46 | nextfunction: Pos; |
---|
[2439] | 47 | symbols: identifier_map SymbolTag block; |
---|
| 48 | functions_inv: ∀b. lookup_opt ? b functions ≠ None ? → |
---|
[2608] | 49 | ∃id. lookup … symbols id = Some ? (mk_block (*Code*) (neg b)) |
---|
[1986] | 50 | }. |
---|
| 51 | |
---|
[2439] | 52 | (* We deal with shadowed names by overwriting their global environment entry |
---|
| 53 | and getting rid of any function mapping (the latter is necessary so that we |
---|
| 54 | get a reverse mapping). In fact, the parser will prevent these anyway, but |
---|
| 55 | adding the uniqueness of these names throughout would be more trouble than |
---|
| 56 | it's worth. *) |
---|
| 57 | |
---|
| 58 | definition drop_fn : ∀F:Type[0]. ident → genv_t F → genv_t F ≝ |
---|
| 59 | λF,id,g. |
---|
| 60 | let fns ≝ |
---|
| 61 | match lookup ?? (symbols … g) id with |
---|
| 62 | [ None ⇒ functions … g |
---|
| 63 | | Some b' ⇒ |
---|
[2608] | 64 | match block_id b' with |
---|
| 65 | [ neg p ⇒ |
---|
| 66 | pm_set … p (None ?) (functions … g) |
---|
| 67 | | _ ⇒ functions … g |
---|
| 68 | ] |
---|
| 69 | (* match b' with |
---|
[2439] | 70 | [ mk_block r x ⇒ |
---|
| 71 | match r with |
---|
| 72 | [ Code ⇒ |
---|
| 73 | match x with |
---|
| 74 | [ neg p ⇒ pm_set … p (None ?) (functions … g) |
---|
| 75 | | _ ⇒ functions … g |
---|
| 76 | ] |
---|
| 77 | | _ ⇒ functions … g |
---|
| 78 | ] |
---|
| 79 | | _ ⇒ functions … g |
---|
[2608] | 80 | ] *) |
---|
[2439] | 81 | ] |
---|
| 82 | in mk_genv_t F fns (nextfunction … g) (remove … (symbols … g) id) ?. |
---|
| 83 | whd in match fns; -fns |
---|
| 84 | #b #L |
---|
| 85 | cases (functions_inv ? g b ?) |
---|
| 86 | [ #id' #L' |
---|
| 87 | cases (identifier_eq … id id') |
---|
| 88 | [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??)) |
---|
| 89 | | #NE %{id'} >lookup_remove_miss /2/ |
---|
| 90 | ] |
---|
| 91 | | cases (lookup ?? (symbols F g) id) in L; |
---|
| 92 | [ normalize // |
---|
[2608] | 93 | | normalize nodelta * * normalize nodelta try // |
---|
| 94 | #p |
---|
| 95 | @(eqb_elim … b p) |
---|
| 96 | [ #Heq destruct #NE |
---|
| 97 | >lookup_opt_pm_set_hit in NE; #Hneq |
---|
| 98 | @False_ind |
---|
| 99 | @(absurd … (refl ??) Hneq) |
---|
| 100 | | #id >lookup_opt_pm_set_miss // ] |
---|
| 101 | ] |
---|
| 102 | ] qed. |
---|
| 103 | (* |
---|
| 104 | whd in match fns; -fns |
---|
| 105 | #b #L |
---|
| 106 | cases (functions_inv ? g b ?) |
---|
| 107 | [ #id' #L' |
---|
| 108 | cases (identifier_eq … id id') |
---|
| 109 | [ #E destruct >L' in L; normalize >lookup_opt_pm_set_hit * #H cases (H (refl ??)) |
---|
| 110 | | #NE %{id'} >lookup_remove_miss /2/ |
---|
| 111 | ] |
---|
| 112 | | cases (lookup ?? (symbols F g) id) in L; |
---|
| 113 | [ normalize // |
---|
[2439] | 114 | | * * * [ 2,3,5,6: #b' ] normalize // |
---|
| 115 | #H cut (b ≠ b') |
---|
| 116 | [ % #E destruct >lookup_opt_pm_set_hit in H; * /2/ ] |
---|
| 117 | #NE >lookup_opt_pm_set_miss in H; // |
---|
| 118 | ] |
---|
| 119 | ] qed. |
---|
| 120 | |
---|
[2608] | 121 | *) |
---|
[2439] | 122 | lemma drop_fn_id : ∀F,id,ge. |
---|
| 123 | lookup ?? (symbols … (drop_fn F id ge)) id = None ?. |
---|
| 124 | #F #id * #fns #next #syms #inv |
---|
| 125 | whd in match (drop_fn ???); |
---|
| 126 | @lookup_remove_hit |
---|
| 127 | qed. |
---|
| 128 | |
---|
| 129 | lemma drop_fn_lfn : ∀F,id,ge,b,f. |
---|
| 130 | lookup_opt ? b (functions … (drop_fn F id ge)) = Some ? f → |
---|
| 131 | lookup_opt ? b (functions … ge) = Some ? f. |
---|
| 132 | #F #id #ge #b #f |
---|
| 133 | whd in match (drop_fn ???); |
---|
| 134 | cases (lookup ??? id) |
---|
| 135 | [ normalize // |
---|
[2608] | 136 | | * * [2,3: #b' ] normalize // |
---|
[2439] | 137 | cases (decidable_eq_pos b b') |
---|
| 138 | [ #E destruct >lookup_opt_pm_set_hit #E destruct |
---|
| 139 | | #NE >lookup_opt_pm_set_miss // |
---|
| 140 | ] |
---|
| 141 | ] qed. |
---|
| 142 | |
---|
[1986] | 143 | definition add_funct : ∀F:Type[0]. (ident × F) → genv_t F → genv_t F ≝ |
---|
| 144 | λF,name_fun,g. |
---|
| 145 | let blk_id ≝ nextfunction ? g in |
---|
[2608] | 146 | let b ≝ mk_block (* Code *) (neg blk_id) in |
---|
[2439] | 147 | let g' ≝ drop_fn F (\fst name_fun) g in |
---|
| 148 | mk_genv_t F (insert ? blk_id (\snd name_fun) (functions … g')) |
---|
[2010] | 149 | (succ blk_id) |
---|
[2439] | 150 | (add ?? (symbols … g') (\fst name_fun) b) ?. |
---|
| 151 | #b' #L whd in match b; |
---|
| 152 | cases (decidable_eq_pos blk_id b') |
---|
| 153 | [ #E destruct |
---|
| 154 | %{(\fst name_fun)} @lookup_add_hit |
---|
| 155 | | #NE |
---|
| 156 | cases (functions_inv ? g' b' ?) |
---|
| 157 | [ #id #L' %{id} >lookup_add_miss |
---|
| 158 | [ @L' |
---|
| 159 | | % #E destruct |
---|
| 160 | >drop_fn_id in L'; #E destruct |
---|
| 161 | ] |
---|
| 162 | | >lookup_opt_insert_miss in L; /2/ |
---|
| 163 | ] |
---|
| 164 | ] qed. |
---|
[1986] | 165 | |
---|
| 166 | definition add_symbol : ∀F:Type[0]. ident → block → genv_t F → genv_t F ≝ |
---|
| 167 | λF,name,b,g. |
---|
[2439] | 168 | let g' ≝ drop_fn F name g in |
---|
| 169 | mk_genv_t F (functions … g') |
---|
| 170 | (nextfunction … g') |
---|
| 171 | (add ?? (symbols … g') name b) |
---|
| 172 | ?. |
---|
| 173 | #b' #L |
---|
| 174 | cases (functions_inv ? g' b' ?) |
---|
| 175 | [ #id #L' %{id} >lookup_add_miss |
---|
| 176 | [ @L' |
---|
| 177 | | % #E destruct |
---|
| 178 | >drop_fn_id in L'; #E destruct |
---|
| 179 | ] |
---|
| 180 | | @L |
---|
| 181 | ] qed. |
---|
[1986] | 182 | |
---|
| 183 | (* Construct environment and initial memory store *) |
---|
| 184 | definition empty_mem ≝ empty. (* XXX*) |
---|
| 185 | definition empty : ∀F. genv_t F ≝ |
---|
[2439] | 186 | λF. mk_genv_t F (pm_leaf ?) (succ_pos_of_nat … 2) (empty_map ??) ?. |
---|
| 187 | #b #L normalize in L; cases L #L cases (L (refl ??)) |
---|
| 188 | qed. |
---|
[1986] | 189 | |
---|
| 190 | definition add_functs : ∀F:Type[0]. genv_t F → list (ident × F) → genv_t F ≝ |
---|
| 191 | λF,init,fns. |
---|
| 192 | foldr ?? (add_funct F) init fns. |
---|
| 193 | |
---|
[2010] | 194 | (* Return the address of the given global symbol, if any. *) |
---|
| 195 | definition find_symbol: ∀F: Type[0]. genv_t F → ident → option block ≝ |
---|
| 196 | λF,ge. lookup ?? (symbols … ge). |
---|
| 197 | |
---|
[1986] | 198 | (* init *) |
---|
| 199 | |
---|
| 200 | definition store_init_data : ∀F.genv_t F → mem → block → Z → init_data → option mem ≝ |
---|
| 201 | λF,ge,m,b,p,id. |
---|
| 202 | (* store checks that the address came from something capable of representing |
---|
| 203 | addresses of the memory region in question - here there are no real |
---|
| 204 | pointers, so use the real region. *) |
---|
[2185] | 205 | let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in |
---|
[1986] | 206 | match id with |
---|
| 207 | [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n) |
---|
| 208 | | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n) |
---|
| 209 | | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n) |
---|
[2624] | 210 | (*| Init_float32 n ⇒ None ? (*store (ASTfloat F32) m ptr (Vfloat n)*) |
---|
| 211 | | Init_float64 n ⇒ None ? (*store (ASTfloat F64) m ptr (Vfloat n) *)*) |
---|
[2176] | 212 | | Init_addrof (*r'*) symb ofs ⇒ |
---|
[2010] | 213 | match find_symbol … ge symb with |
---|
[1986] | 214 | [ None ⇒ None ? |
---|
[2176] | 215 | | Some b' ⇒ (* |
---|
[1986] | 216 | match pointer_compat_dec b' r' with |
---|
[2176] | 217 | [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs)))) |
---|
| 218 | (*| inr _ ⇒ None ? |
---|
| 219 | ]*) |
---|
[1986] | 220 | ] |
---|
| 221 | | Init_space n ⇒ Some ? m |
---|
[2176] | 222 | | Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*)) |
---|
[1986] | 223 | ]. |
---|
[2176] | 224 | (*cases b // |
---|
| 225 | qed.*) |
---|
[1986] | 226 | |
---|
| 227 | definition size_init_data : init_data → nat ≝ |
---|
| 228 | λi_data.match i_data with |
---|
| 229 | [ Init_int8 _ ⇒ 1 |
---|
| 230 | | Init_int16 _ ⇒ 2 |
---|
| 231 | | Init_int32 _ ⇒ 4 |
---|
[2624] | 232 | (*| Init_float32 _ ⇒ 4 |
---|
| 233 | | Init_float64 _ ⇒ 8*) |
---|
[1986] | 234 | | Init_space n ⇒ max n 0 |
---|
[2176] | 235 | | Init_null (*r*) ⇒ size_pointer (*r*) |
---|
| 236 | | Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)]. |
---|
[1986] | 237 | |
---|
| 238 | let rec store_init_data_list (F:Type[0]) (ge:genv_t F) |
---|
| 239 | (m: mem) (b: block) (p: Z) (idl: list init_data) |
---|
| 240 | on idl : option mem ≝ |
---|
| 241 | match idl with |
---|
| 242 | [ nil ⇒ Some ? m |
---|
| 243 | | cons id idl' ⇒ |
---|
| 244 | match store_init_data F ge m b p id with |
---|
| 245 | [ None ⇒ None ? |
---|
| 246 | | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl' |
---|
| 247 | ] |
---|
| 248 | ]. |
---|
| 249 | |
---|
| 250 | definition size_init_data_list : list init_data → nat ≝ |
---|
| 251 | λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data. |
---|
| 252 | |
---|
| 253 | (* Nonessential properties that may require arithmetic |
---|
| 254 | nremark size_init_data_list_pos: |
---|
| 255 | ∀i_data. OZ ≤ size_init_data_list i_data. |
---|
| 256 | #i_data;elim i_data;//; |
---|
| 257 | #a;#tl;cut (OZ ≤ size_init_data a) |
---|
| 258 | ##[cases a;normalize;//; |
---|
| 259 | #x;cases x;normalize;//; |
---|
| 260 | ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl)); |
---|
| 261 | cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m) |
---|
| 262 | ##[cases (size_init_data a) in Hsize IH; |
---|
| 263 | ##[##1,2:/3/ |
---|
| 264 | ##|normalize;#n;#Hfalse;elim Hfalse] |
---|
| 265 | ##|#Hdisc;cases Hdisc |
---|
| 266 | ##[#Heq;nrewrite > Heq;//; |
---|
| 267 | ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2; |
---|
| 268 | (* TODO: arithmetics *) napply daemon] |
---|
| 269 | ##] |
---|
| 270 | ##] |
---|
| 271 | qed. |
---|
[3] | 272 | *) |
---|
| 273 | |
---|
| 274 | |
---|
[1986] | 275 | (* init *) |
---|
[3] | 276 | |
---|
[1986] | 277 | definition add_globals : ∀F,V:Type[0]. |
---|
| 278 | (V → (list init_data)) → |
---|
| 279 | genv_t F × mem → list (ident × region × V) → |
---|
| 280 | (genv_t F × mem) ≝ |
---|
| 281 | λF,V,extract_init,init_env,vars. |
---|
| 282 | foldl ?? |
---|
| 283 | (λg_st: genv_t F × mem. λid_init: ident × region × V. |
---|
| 284 | let 〈id, r, init_info〉 ≝ id_init in |
---|
| 285 | let init ≝ extract_init init_info in |
---|
| 286 | let 〈g,st〉 ≝ g_st in |
---|
[2608] | 287 | let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) (* r *) in |
---|
[1986] | 288 | let g' ≝ add_symbol ? id b g in |
---|
| 289 | 〈g', st'〉 |
---|
| 290 | ) |
---|
| 291 | init_env vars. |
---|
[3] | 292 | |
---|
[1986] | 293 | definition init_globals : ∀F,V:Type[0]. |
---|
| 294 | (V → (list init_data)) → |
---|
| 295 | genv_t F → mem → list (ident × region × V) → |
---|
| 296 | res mem ≝ |
---|
| 297 | λF,V,extract_init,g,m,vars. |
---|
| 298 | foldl ?? |
---|
| 299 | (λst: res mem. λid_init: ident × region × V. |
---|
| 300 | let 〈id, r, init_info〉 ≝ id_init in |
---|
| 301 | let init ≝ extract_init init_info in |
---|
| 302 | do st ← st; |
---|
[2010] | 303 | match find_symbol … g id with |
---|
[1986] | 304 | [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init) |
---|
| 305 | | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *) |
---|
| 306 | ] ) |
---|
| 307 | (OK ? m) vars. |
---|
[3] | 308 | |
---|
[1986] | 309 | definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv_t (F (prog_var_names … p)) × mem) ≝ |
---|
| 310 | λF,V,init_info,p. |
---|
| 311 | add_globals … init_info |
---|
[1988] | 312 | 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉 |
---|
[1986] | 313 | (prog_vars ?? p). |
---|
[3] | 314 | |
---|
[1986] | 315 | (* Return the global environment for the given program. *) |
---|
| 316 | definition globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p)) ≝ |
---|
| 317 | λF,V,i,p. |
---|
| 318 | \fst (globalenv_allocmem F V i p). |
---|
[24] | 319 | |
---|
[1999] | 320 | (* Return the global environment for the given program with no data initialisation. *) |
---|
| 321 | definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝ |
---|
| 322 | λF,p. |
---|
[2105] | 323 | globalenv F nat (λn.[Init_space n]) p. |
---|
[1999] | 324 | |
---|
[1986] | 325 | (* Return the initial memory state for the given program. *) |
---|
| 326 | definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝ |
---|
| 327 | λF,V,i,p. |
---|
| 328 | let 〈g,m〉 ≝ globalenv_allocmem F V i p in |
---|
| 329 | init_globals ? V i g m (prog_vars ?? p). |
---|
| 330 | |
---|
[1999] | 331 | (* Setup memory when data initialisation is not required (has the benefit |
---|
| 332 | of being total. *) |
---|
| 333 | definition alloc_mem: ∀F. program F nat → mem ≝ |
---|
| 334 | λF,p. |
---|
| 335 | \snd (globalenv_allocmem F nat (λn. [Init_space n]) p). |
---|
| 336 | |
---|
[1986] | 337 | (* Return the function description associated with the given address, if any. *) |
---|
| 338 | definition find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F ≝ |
---|
[2010] | 339 | λF,ge,b. match block_region b with [ Code ⇒ |
---|
| 340 | match block_id b with [ neg p ⇒ lookup_opt … p (functions … ge) |
---|
| 341 | | _ ⇒ None ? ] | _ ⇒ None ? ]. |
---|
[1986] | 342 | |
---|
| 343 | (* Same as [find_funct_ptr] but the function address is given as |
---|
| 344 | a value, which must be a pointer with offset 0. *) |
---|
| 345 | definition find_funct: ∀F: Type[0]. genv_t F → val → option F ≝ |
---|
[2010] | 346 | λ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 ? ]. |
---|
[1986] | 347 | |
---|
| 348 | |
---|
[2415] | 349 | (* Turn a memory block into the original symbol. *) |
---|
| 350 | definition symbol_for_block: ∀F:Type[0]. genv_t F → block → option ident ≝ |
---|
| 351 | λF,genv,b. |
---|
| 352 | option_map ?? (fst ??) (find … (symbols … genv) (λid,b'. eq_block b b')). |
---|
| 353 | |
---|
| 354 | |
---|
[1986] | 355 | lemma find_funct_find_funct_ptr : ∀F,ge,v,f. |
---|
| 356 | find_funct F ge v = Some F f → |
---|
[2176] | 357 | ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset) ∧ find_funct_ptr F ge b = Some F f. |
---|
[1986] | 358 | #F #ge * |
---|
| 359 | [ #f #E normalize in E; destruct |
---|
| 360 | | #sz #i #f #E normalize in E; destruct |
---|
[2468] | 361 | (*| #f #fn #E normalize in E; destruct*) |
---|
[2176] | 362 | | (*#r*) #f #E normalize in E; destruct |
---|
[2185] | 363 | | * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?); |
---|
| 364 | @eq_offset_elim #Eoff |
---|
[2010] | 365 | #E whd in E:(??%?); destruct |
---|
[2176] | 366 | (*%{pty}*) %{b} (*%{c}*) % // @E |
---|
[1986] | 367 | ] qed. |
---|
[2439] | 368 | |
---|
[2107] | 369 | lemma add_globals_match : ∀A,B,V,W,initV,initW. |
---|
[2105] | 370 | ∀P:(ident × region × V) → (ident × region × W) → Prop. |
---|
| 371 | (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
| 372 | ∀vars,ge,ge',m,vars'. |
---|
| 373 | symbols ? ge = symbols … ge' → |
---|
| 374 | All2 … P vars vars' → |
---|
[2107] | 375 | symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')) ∧ |
---|
| 376 | \snd (add_globals A V initV 〈ge,m〉 vars) = \snd (add_globals B W initW 〈ge',m〉 vars'). |
---|
[2105] | 377 | #A #B #V #W #initV #initW #P #varsOK |
---|
| 378 | #vars elim vars |
---|
[2107] | 379 | [ #ge #ge' #m * [ #E #_ % // @E | #h #t #_ * ] |
---|
[2105] | 380 | | * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ] |
---|
| 381 | * * #id' #r' #w #tl' #E * #p #TL |
---|
| 382 | whd in match (add_globals A ????); |
---|
| 383 | change with (add_globals A ????) in match (foldl ?????); |
---|
| 384 | whd in match (add_globals B ????); |
---|
| 385 | change with (add_globals B ????) in match (foldl (genv_t B × mem) ????); |
---|
| 386 | cases (varsOK … p) #E1 #E2 |
---|
[2608] | 387 | destruct >E2 cases (alloc ???) (* cases (alloc ????)*) #m' #b |
---|
[2107] | 388 | @IH /2/ |
---|
[2439] | 389 | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
| 390 | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
[2105] | 391 | >E % |
---|
| 392 | ] qed. |
---|
| 393 | |
---|
[2439] | 394 | |
---|
[2105] | 395 | lemma pre_matching_fns_get_same_blocks : ∀A,B,P. |
---|
| 396 | (∀f,g. P f g → \fst f = \fst g) → |
---|
| 397 | ∀fns,fns'. |
---|
| 398 | All2 … P fns fns' → |
---|
| 399 | let ge ≝ add_functs A (empty ?) fns in |
---|
| 400 | let ge' ≝ add_functs B (empty ?) fns' in |
---|
| 401 | nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'. |
---|
| 402 | #A #B #P #fnOK #fns elim fns |
---|
| 403 | [ * [ #_ % % | #h #t * ] |
---|
| 404 | | * #id #f #tl #IH * [ * ] |
---|
| 405 | * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H |
---|
| 406 | whd in match (add_functs ???); |
---|
| 407 | change with (add_functs ???) in match (foldr ?????); |
---|
| 408 | whd in match (add_functs B ??); |
---|
| 409 | change with (add_functs ???) in match (foldr (ident × B) ????); |
---|
| 410 | cases (IH tl' H) #E1 #E2 |
---|
[2439] | 411 | % [ >E1 % |
---|
| 412 | | whd in match (drop_fn ???); |
---|
| 413 | whd in match (drop_fn ???); |
---|
| 414 | >E1 >E2 % ] |
---|
[2105] | 415 | ] qed. |
---|
| 416 | |
---|
| 417 | lemma matching_fns_get_same_blocks : ∀A,B,P. |
---|
| 418 | (∀f,g. P f g → \fst f = \fst g) → |
---|
| 419 | ∀fns,fns'. |
---|
| 420 | All2 … P fns fns' → |
---|
| 421 | let ge ≝ add_functs A (empty ?) fns in |
---|
| 422 | let ge' ≝ add_functs B (empty ?) fns' in |
---|
| 423 | symbols … ge = symbols … ge'. |
---|
| 424 | #A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK |
---|
| 425 | qed. |
---|
| 426 | |
---|
[2722] | 427 | |
---|
[2415] | 428 | lemma symbol_of_block_rev : ∀F,genv,b,id. |
---|
| 429 | symbol_for_block F genv b = Some ? id → |
---|
| 430 | find_symbol F genv id = Some ? b. |
---|
| 431 | #F #genv #b #id #H whd in H:(??%?); |
---|
| 432 | @(find_lookup … (λid,b'. eq_block b b')) |
---|
| 433 | lapply (find_predicate … (symbols … genv) (λid,b'. eq_block b b')) |
---|
| 434 | cases (find ????) in H ⊢ %; |
---|
| 435 | [ normalize #E destruct |
---|
| 436 | | * #id' #b' normalize in ⊢ (% → ?); #E destruct |
---|
| 437 | #H lapply (H … (refl ??)) |
---|
| 438 | @eq_block_elim |
---|
| 439 | [ #E destruct // |
---|
| 440 | | #_ * |
---|
| 441 | ] |
---|
| 442 | ] qed. |
---|
| 443 | |
---|
[2722] | 444 | lemma symbol_of_block_rev' : ∀F,genv,b. |
---|
| 445 | symbol_for_block F genv b = None ? → |
---|
| 446 | find_funct_ptr F genv b = None ?. |
---|
| 447 | #F #genv * * [ // | // ] #b #H |
---|
| 448 | whd in ⊢ (??%?); |
---|
| 449 | lapply (functions_inv ? genv b) |
---|
| 450 | cases (lookup_opt F b ?) // |
---|
| 451 | #f #H' cases (H' ?) |
---|
| 452 | [ #id #E whd in H:(??%?); |
---|
| 453 | lapply (find_none ?? (symbols … genv) (λid,b'. eq_block (mk_block (neg b)) b') id (mk_block (neg b))) |
---|
| 454 | cases (find ????) in H ⊢ %; |
---|
| 455 | [ normalize #_ #H lapply (H (refl ??) E) >eqb_n_n * |
---|
| 456 | | * #id' #b' normalize #E destruct |
---|
| 457 | ] |
---|
| 458 | | % #E destruct |
---|
| 459 | ] qed. |
---|
| 460 | |
---|
[2896] | 461 | (* For *functions* the mapping between identifiers and blocks is a bijection, |
---|
| 462 | but to show that we have to keep more invariants about the environment. *) |
---|
| 463 | axiom symbol_for_block_fn : ∀F,genv,b,f,id. |
---|
| 464 | find_symbol F genv id = Some ? b → |
---|
| 465 | find_funct_ptr F genv b = Some ? f → |
---|
| 466 | symbol_for_block F genv b = Some ? id. |
---|
| 467 | |
---|
[2439] | 468 | (* The mapping of blocks to symbols is total for functions. *) |
---|
| 469 | |
---|
| 470 | definition symbol_of_function_block : ∀F,ge,b. find_funct_ptr F ge b ≠ None ? → ident ≝ |
---|
| 471 | λF,ge,b,FFP. |
---|
| 472 | match symbol_for_block F ge b return λx. symbol_for_block ??? = x → ? with |
---|
| 473 | [ None ⇒ λH. ⊥ |
---|
| 474 | | Some id ⇒ λ_. id |
---|
| 475 | ] (refl ? (symbol_for_block F ge b)). |
---|
| 476 | whd in H:(??%?); |
---|
[2608] | 477 | cases b in FFP H ⊢ %; * -b [2,3(*,5,6*): #b ] normalize in ⊢ (% → ?); [ 1,3: * #H cases (H (refl ??)) ] |
---|
| 478 | #FFP |
---|
[2439] | 479 | cases (functions_inv … ge b FFP) |
---|
[2608] | 480 | #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block (*Code*) (neg b)) b') id (mk_block (*Code*) (neg b))) |
---|
| 481 | lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block (* Code *) (neg b)) b') id (mk_block (* Code *) (neg b))) |
---|
[2439] | 482 | cases (find ????) |
---|
| 483 | [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ] |
---|
| 484 | | * #id' #b' #_ normalize #_ #E destruct |
---|
| 485 | ] qed. |
---|
| 486 | |
---|
[2722] | 487 | lemma symbol_of_function_block_ok : ∀F,ge,b,FFP,id. |
---|
| 488 | symbol_of_function_block F ge b FFP = id → |
---|
| 489 | symbol_for_block F ge b = Some ? id. |
---|
| 490 | #F #ge #b #FFP #id whd in ⊢ (??%? → ?); |
---|
| 491 | generalize in match (refl ? (symbol_for_block F ge b)); |
---|
| 492 | lapply (symbol_of_block_rev' F ge b) |
---|
| 493 | cases (symbol_for_block F ge b) in ⊢ (% → ???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
| 494 | [ #H @⊥ >(H (refl ??)) in FFP; * /2/ |
---|
| 495 | | #id' #_ #E normalize in ⊢ (% → ?); #E' destruct @E |
---|
| 496 | ] qed. |
---|
| 497 | |
---|
| 498 | definition symbol_of_function_block' : ∀F,ge,b,f. find_funct_ptr F ge b = Some ? f → ident ≝ |
---|
| 499 | λF,ge,b,f,FFP. symbol_of_function_block F ge b ?. |
---|
| 500 | >FFP % #E destruct |
---|
| 501 | qed. |
---|
| 502 | |
---|
| 503 | definition find_funct_ptr_id : ∀F:Type[0]. genv_t F → block → option (F × ident) ≝ |
---|
| 504 | λF:Type[0].λge:genv_t F.λb:block. |
---|
| 505 | match find_funct_ptr F ge b return λx:option F. ? = x → option (F × ident) with |
---|
| 506 | [ None ⇒ λ_. None ? |
---|
| 507 | | Some f ⇒ λFFP. Some ? 〈f,symbol_of_function_block' F ge b f FFP〉 |
---|
| 508 | ] (refl ??). |
---|
| 509 | |
---|
| 510 | lemma find_funct_ptr_id_drop : ∀F,ge,b,f,id. |
---|
| 511 | find_funct_ptr_id F ge b = Some ? 〈f,id〉 → |
---|
| 512 | find_funct_ptr F ge b = Some ? f. |
---|
| 513 | #F #ge #b #f #id whd in ⊢ (??%? → ?); |
---|
| 514 | generalize in match (refl ??); |
---|
| 515 | cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %); |
---|
| 516 | [ #X #E normalize in E; destruct |
---|
| 517 | | #f' #ID #E whd in E:(??%?); destruct % |
---|
| 518 | ] qed. |
---|
| 519 | |
---|
| 520 | coercion ffpi_drop : |
---|
| 521 | ∀F,ge,b,f,id. |
---|
| 522 | ∀FFP:find_funct_ptr_id F ge b = Some ? 〈f,id〉. |
---|
| 523 | find_funct_ptr F ge b = Some ? f ≝ find_funct_ptr_id_drop |
---|
| 524 | on _FFP:eq (option ?) ?? to eq (option ?) ??. |
---|
| 525 | |
---|
| 526 | lemma find_funct_ptr_id_inv : ∀F,ge,b,f,id. |
---|
| 527 | find_funct_ptr_id F ge b = Some ? 〈f,id〉 → |
---|
| 528 | find_funct_ptr F ge b = Some ? f ∧ |
---|
| 529 | symbol_for_block F ge b = Some ? id. |
---|
| 530 | #F #ge #b #f #id whd in ⊢ (??%? → ?); |
---|
| 531 | generalize in match (refl ??); |
---|
| 532 | cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %); |
---|
| 533 | [ #X #E normalize in E; destruct |
---|
| 534 | | #f' #FFP #E whd in E:(??%?); % |
---|
| 535 | [ destruct % |
---|
| 536 | | @(symbol_of_function_block_ok F ge b ? id) |
---|
| 537 | [ >FFP % #E' destruct |
---|
| 538 | | destruct % |
---|
| 539 | ] |
---|
| 540 | ] |
---|
| 541 | ] qed. |
---|
| 542 | |
---|
| 543 | lemma make_find_funct_ptr_id : ∀F,ge,b,f,id. |
---|
| 544 | find_funct_ptr F ge b = Some ? f → |
---|
| 545 | symbol_for_block F ge b = Some ? id → |
---|
| 546 | find_funct_ptr_id F ge b = Some ? 〈f,id〉. |
---|
| 547 | #F #ge #b #f #id #FFP #SYM |
---|
| 548 | whd in ⊢ (??%?); generalize in match (refl ??); |
---|
| 549 | >FFP in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); |
---|
| 550 | #FFP' whd in ⊢ (??%?); |
---|
| 551 | @eq_f @eq_f |
---|
| 552 | whd in ⊢ (??%?); |
---|
| 553 | generalize in match (refl ? (symbol_for_block F ge b)); |
---|
| 554 | >SYM in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); |
---|
| 555 | #SYM' whd in ⊢ (??%?); % |
---|
| 556 | qed. |
---|
| 557 | |
---|
| 558 | definition symbol_of_function_val : ∀F,ge,v. find_funct F ge v ≠ None ? → ident ≝ |
---|
| 559 | λF,ge,v. |
---|
| 560 | match v return λv. find_funct F ge v ≠ None ? → ident with |
---|
| 561 | [ Vptr p ⇒ λH. symbol_of_function_block F ge (pblock p) ? |
---|
| 562 | | _ ⇒ λH. ⊥ |
---|
| 563 | ]. |
---|
| 564 | try (cases H #H' cases (H' (refl ??))) |
---|
| 565 | lapply H |
---|
| 566 | whd in match (find_funct ???); |
---|
| 567 | @eq_offset_elim |
---|
| 568 | [ #_ #H' @H' |
---|
| 569 | | #X * #H' cases (H' (refl ??)) |
---|
| 570 | ] qed. |
---|
| 571 | |
---|
| 572 | definition symbol_of_function_val' : ∀F,ge,v,f. find_funct F ge v = Some ? f → ident ≝ |
---|
| 573 | λF,ge,v,f,FF. symbol_of_function_val F ge v ?. |
---|
| 574 | >FF % #E destruct |
---|
| 575 | qed. |
---|
| 576 | |
---|
| 577 | definition find_funct_id : ∀F:Type[0]. genv_t F → val → option (F × ident) ≝ |
---|
| 578 | λF:Type[0].λge:genv_t F.λv:val. |
---|
| 579 | match find_funct F ge v return λx:option F. ? = x → option (F × ident) with |
---|
| 580 | [ None ⇒ λ_. None ? |
---|
| 581 | | Some f ⇒ λFF. Some ? 〈f,symbol_of_function_val' F ge v f FF〉 |
---|
| 582 | ] (refl ??). |
---|
| 583 | |
---|
| 584 | lemma find_funct_id_drop : ∀F,ge,v,f,id. |
---|
| 585 | find_funct_id F ge v = Some ? 〈f,id〉 → |
---|
| 586 | find_funct F ge v = Some ? f. |
---|
| 587 | #F #ge #v #f #id whd in ⊢ (??%? → ?); |
---|
| 588 | generalize in match (refl ??); |
---|
| 589 | cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
| 590 | [ #X #E normalize in E; destruct |
---|
| 591 | | #f' #ID #E whd in E:(??%?); destruct assumption |
---|
| 592 | ] qed. |
---|
| 593 | |
---|
| 594 | coercion ffi_drop : |
---|
| 595 | ∀F,ge,v,f,id. |
---|
| 596 | ∀FF:find_funct_id F ge v = Some ? 〈f,id〉. |
---|
| 597 | find_funct F ge v = Some ? f ≝ find_funct_id_drop |
---|
| 598 | on _FF:eq (option ?) ?? to eq (option ?) ??. |
---|
| 599 | |
---|
| 600 | lemma find_funct_id_ptr : ∀F,ge,v,f,id. |
---|
| 601 | find_funct_id F ge v = Some ? 〈f,id〉 → |
---|
| 602 | ∃b. v = Vptr (mk_pointer b zero_offset) ∧ |
---|
[2895] | 603 | find_symbol F ge id = Some ? b ∧ |
---|
[2722] | 604 | find_funct_ptr_id F ge b = Some ? 〈f,id〉. |
---|
| 605 | #F #ge #v #f #id whd in ⊢ (??%? → ?); |
---|
| 606 | generalize in match (refl ??); |
---|
| 607 | cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %); |
---|
| 608 | [ #X #E normalize in E; destruct |
---|
| 609 | | #f' #FF #E whd in E:(??%?); |
---|
[2895] | 610 | cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} % [ % |
---|
| 611 | [ @E1 |
---|
| 612 | | @symbol_of_block_rev |
---|
| 613 | @symbol_of_function_block_ok [ >FFP % #E2 destruct ] |
---|
| 614 | destruct % |
---|
| 615 | ] ] |
---|
[2722] | 616 | whd in ⊢ (??%?); |
---|
| 617 | generalize in match (refl ??); |
---|
| 618 | >FFP in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); |
---|
| 619 | #FFP' whd in ⊢ (??%?); <E |
---|
| 620 | @eq_f @eq_f >E1 in FF E ⊢ %; #FF #E % |
---|
| 621 | ] qed. |
---|
| 622 | |
---|
| 623 | lemma find_funct_ptr_id_conv : ∀F,ge,b,f,id. |
---|
| 624 | find_funct_ptr_id F ge b = Some ? 〈f,id〉 → |
---|
| 625 | find_funct_id F ge (Vptr (mk_pointer b zero_offset)) = Some ? 〈f,id〉. |
---|
| 626 | #F #ge * * [2,3:#b] #f #id |
---|
| 627 | whd in ⊢ (??%? → ??%?); #E destruct |
---|
| 628 | @E |
---|
| 629 | qed. |
---|
| 630 | |
---|
[1986] | 631 | (* |
---|
[3] | 632 | (* * ** Properties of the operations. *) |
---|
[125] | 633 | |
---|
[3] | 634 | find_funct_inv: |
---|
[487] | 635 | ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F. |
---|
[467] | 636 | find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero; |
---|
[3] | 637 | find_funct_find_funct_ptr: |
---|
[487] | 638 | ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block. |
---|
[467] | 639 | find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b; |
---|
[2471] | 640 | *) |
---|
| 641 | lemma find_symbol_exists: |
---|
| 642 | ∀F,V. ∀init. ∀p: program F V. ∀id. |
---|
| 643 | Exists ? (λx. x = id) (map … (λx. \fst x) (prog_funct ?? p) @ map … (λx. \fst (\fst x)) (prog_vars ?? p)) → |
---|
| 644 | ∃b. find_symbol ? (globalenv … init p) id = Some ? b. |
---|
| 645 | #F #V #init * #vars #fns #main #id |
---|
| 646 | whd in match (globalenv ????); |
---|
| 647 | whd in match (globalenv_allocmem ????); |
---|
| 648 | whd in match (prog_var_names ???); |
---|
| 649 | generalize in match (F ?) in fns ⊢ %; -F #F #fns |
---|
| 650 | #EX |
---|
| 651 | cut (Exists ident (λx.x = id) (map … (λx.\fst (\fst x)) vars) ∨ |
---|
| 652 | ∃b. find_symbol ? (add_functs F (empty F) fns) id = Some ? b) |
---|
| 653 | [ cases (Exists_append … EX) |
---|
| 654 | [ -EX #EX %2 |
---|
| 655 | elim fns in EX ⊢ %; |
---|
| 656 | [ * |
---|
| 657 | | * #id' #f #tl #IH * |
---|
| 658 | [ #E destruct |
---|
| 659 | change with (foldr ?????) in match (add_functs F (empty F) ?); |
---|
| 660 | change with (lookup ????) in match (find_symbol ???); |
---|
| 661 | whd in match (foldr ?????); |
---|
| 662 | % [2: @lookup_add_hit | skip ] |
---|
| 663 | | #TL |
---|
| 664 | change with (foldr ?????) in match (add_functs F (empty F) ?); |
---|
| 665 | change with (lookup ????) in match (find_symbol ???); |
---|
| 666 | whd in match (foldr ?????); |
---|
| 667 | cases (identifier_eq ? id id') |
---|
| 668 | [ #E destruct |
---|
| 669 | % [2: @lookup_add_hit | skip ] |
---|
| 670 | | #NE >lookup_add_miss // |
---|
| 671 | whd in match (drop_fn ???); |
---|
| 672 | >lookup_remove_miss // @IH @TL |
---|
| 673 | ] |
---|
| 674 | ] |
---|
| 675 | ] |
---|
| 676 | | #EX %1 @EX |
---|
| 677 | ] |
---|
| 678 | ] |
---|
| 679 | -EX |
---|
| 680 | generalize in match (add_functs F (empty F) fns); |
---|
| 681 | generalize in match empty_mem; |
---|
| 682 | elim vars |
---|
| 683 | [ #m #ge * [ * | // ] |
---|
| 684 | | * * #id' #r' #v' #tl #IH #m #ge * |
---|
| 685 | [ * |
---|
| 686 | [ #E destruct |
---|
| 687 | (* Found one, but it might be shadowed later *) |
---|
[2608] | 688 | whd in match (foldl ?????); normalize nodelta |
---|
| 689 | cases (alloc ???) (* cases (alloc ????) *) #m' #b normalize nodelta |
---|
[2471] | 690 | cut (find_symbol F (add_symbol F id b ge) id = Some ? b) |
---|
| 691 | [ change with (lookup ????) in ⊢ (??%?); |
---|
| 692 | whd in match add_symbol; normalize nodelta |
---|
| 693 | @lookup_add_hit ] |
---|
| 694 | #F @IH %2 %{b} @F |
---|
[2608] | 695 | | #TL whd in match (foldl ?????); normalize nodelta |
---|
| 696 | cases (alloc ???) (*cases (alloc ????)*) #m' #b' |
---|
[2471] | 697 | @IH %1 @TL |
---|
| 698 | ] |
---|
| 699 | | #H whd in match (foldl ?????); normalize nodelta |
---|
[2608] | 700 | cases (alloc ???) (* cases (alloc ????) *) #m' #b' normalize nodelta |
---|
[2471] | 701 | @IH %2 |
---|
| 702 | cases (identifier_eq ? id id') |
---|
| 703 | [ #E destruct %{b'} |
---|
| 704 | whd in match add_symbol; normalize nodelta |
---|
| 705 | @lookup_add_hit |
---|
| 706 | | #NE cases H #b #H' %{b} |
---|
| 707 | whd in match add_symbol; normalize nodelta |
---|
| 708 | change with (lookup ???? = ?) >lookup_add_miss // |
---|
| 709 | whd in match (drop_fn ???); >lookup_remove_miss // @H' |
---|
| 710 | ] |
---|
| 711 | ] |
---|
| 712 | ] qed. |
---|
[3] | 713 | |
---|
[2471] | 714 | (* |
---|
[3] | 715 | find_funct_ptr_exists: |
---|
[487] | 716 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F. |
---|
[3] | 717 | list_norepet ? (prog_funct_names ?? p) → |
---|
| 718 | list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) → |
---|
| 719 | in_list ? 〈id, f〉 (prog_funct ?? p) → |
---|
[467] | 720 | ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 |
---|
[3] | 721 | ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f; |
---|
| 722 | |
---|
| 723 | find_funct_ptr_inversion: |
---|
[487] | 724 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
[3] | 725 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 726 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 727 | find_funct_inversion: |
---|
[487] | 728 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
[3] | 729 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 730 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 731 | find_funct_ptr_symbol_inversion: |
---|
[487] | 732 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F. |
---|
[467] | 733 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → |
---|
[3] | 734 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 735 | in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 736 | |
---|
| 737 | find_funct_ptr_prop: |
---|
[487] | 738 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
[3] | 739 | (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → |
---|
| 740 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 741 | P f; |
---|
| 742 | find_funct_prop: |
---|
[487] | 743 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
[3] | 744 | (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → |
---|
| 745 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 746 | P f; |
---|
| 747 | |
---|
| 748 | initmem_nullptr: |
---|
[487] | 749 | ∀F,V: Type[0]. ∀p: program F V. |
---|
[3] | 750 | let m ≝ init_mem ?? p in |
---|
| 751 | valid_block m nullptr ∧ |
---|
[467] | 752 | (blocks m) nullptr = empty_block 0 0 Any; |
---|
| 753 | (* initmem_inject_neutral: |
---|
[487] | 754 | ∀F,V: Type[0]. ∀p: program F V. |
---|
[467] | 755 | mem_inject_neutral (init_mem ?? p);*) |
---|
[3] | 756 | find_funct_ptr_negative: |
---|
[487] | 757 | ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F. |
---|
[3] | 758 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0; |
---|
| 759 | find_symbol_not_fresh: |
---|
[487] | 760 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. |
---|
[467] | 761 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p); |
---|
[3] | 762 | find_symbol_not_nullptr: |
---|
[487] | 763 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. |
---|
[467] | 764 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr; |
---|
[3] | 765 | global_addresses_distinct: |
---|
[487] | 766 | ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2. |
---|
[3] | 767 | id1≠id2 → |
---|
| 768 | find_symbol ? (globalenv ?? p) id1 = Some ? b1 → |
---|
| 769 | find_symbol ? (globalenv ?? p) id2 = Some ? b2 → |
---|
[467] | 770 | b1≠b2; |
---|
[3] | 771 | |
---|
| 772 | (* * Commutation properties between program transformations |
---|
| 773 | and operations over global environments. *) |
---|
[467] | 774 | |
---|
[3] | 775 | find_funct_ptr_rev_transf: |
---|
[487] | 776 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 777 | ∀b : block. ∀tf : B. |
---|
| 778 | find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf → |
---|
| 779 | ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf; |
---|
| 780 | find_funct_rev_transf: |
---|
[487] | 781 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 782 | ∀v : val. ∀tf : B. |
---|
| 783 | find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → |
---|
[467] | 784 | ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf; |
---|
[125] | 785 | |
---|
[3] | 786 | (* * Commutation properties between partial program transformations |
---|
| 787 | and operations over global environments. *) |
---|
| 788 | |
---|
| 789 | find_funct_ptr_transf_partial: |
---|
[487] | 790 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 791 | transform_partial_program … transf p = OK ? p' → |
---|
| 792 | ∀b: block. ∀f: A. |
---|
| 793 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 794 | ∃f'. |
---|
| 795 | find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f'; |
---|
| 796 | find_funct_transf_partial: |
---|
[487] | 797 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 798 | transform_partial_program … transf p = OK ? p' → |
---|
| 799 | ∀v: val. ∀f: A. |
---|
| 800 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 801 | ∃f'. |
---|
| 802 | find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f'; |
---|
| 803 | find_symbol_transf_partial: |
---|
[487] | 804 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 805 | transform_partial_program … transf p = OK ? p' → |
---|
| 806 | ∀s: ident. |
---|
| 807 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
| 808 | init_mem_transf_partial: |
---|
[487] | 809 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 810 | transform_partial_program … transf p = OK ? p' → |
---|
| 811 | init_mem ?? p' = init_mem ?? p; |
---|
| 812 | find_funct_ptr_rev_transf_partial: |
---|
[487] | 813 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 814 | transform_partial_program … transf p = OK ? p' → |
---|
| 815 | ∀b : block. ∀tf : B. |
---|
| 816 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
| 817 | ∃f : A. |
---|
| 818 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf; |
---|
| 819 | find_funct_rev_transf_partial: |
---|
[487] | 820 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 821 | transform_partial_program … transf p = OK ? p' → |
---|
| 822 | ∀v : val. ∀tf : B. |
---|
| 823 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 824 | ∃f : A. |
---|
[467] | 825 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*; |
---|
[3] | 826 | |
---|
| 827 | find_funct_ptr_transf_partial2: |
---|
[487] | 828 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 829 | ∀p: program A V. ∀p': program B W. |
---|
| 830 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 831 | ∀b: block. ∀f: A. |
---|
| 832 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 833 | ∃f'. |
---|
| 834 | find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f'; |
---|
| 835 | find_funct_transf_partial2: |
---|
[487] | 836 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 837 | ∀p: program A V. ∀p': program B W. |
---|
| 838 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 839 | ∀v: val. ∀f: A. |
---|
| 840 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 841 | ∃f'. |
---|
| 842 | find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f'; |
---|
| 843 | find_symbol_transf_partial2: |
---|
[487] | 844 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 845 | ∀p: program A V. ∀p': program B W. |
---|
| 846 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 847 | ∀s: ident. |
---|
| 848 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
| 849 | init_mem_transf_partial2: |
---|
[487] | 850 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 851 | ∀p: program A V. ∀p': program B W. |
---|
| 852 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 853 | init_mem ?? p' = init_mem ?? p; |
---|
| 854 | find_funct_ptr_rev_transf_partial2: |
---|
[487] | 855 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 856 | ∀p: program A V. ∀p': program B W. |
---|
| 857 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 858 | ∀b: block. ∀tf: B. |
---|
| 859 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
| 860 | ∃f : A. |
---|
| 861 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf; |
---|
| 862 | find_funct_rev_transf_partial2: |
---|
[487] | 863 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 864 | ∀p: program A V. ∀p': program B W. |
---|
| 865 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 866 | ∀v: val. ∀tf: B. |
---|
| 867 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 868 | ∃f : A. |
---|
| 869 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ; |
---|
| 870 | |
---|
| 871 | (* * Commutation properties between matching between programs |
---|
| 872 | and operations over global environments. *) |
---|
[2105] | 873 | *) *) |
---|
[3] | 874 | |
---|
[2105] | 875 | (* First, show that nextfunction only depends on the number of functions: *) |
---|
| 876 | |
---|
| 877 | let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝ |
---|
| 878 | match n with |
---|
| 879 | [ O ⇒ p |
---|
| 880 | | S m ⇒ succ (nat_plus_pos m p) |
---|
| 881 | ]. |
---|
| 882 | |
---|
| 883 | lemma nextfunction_length : ∀A,l,ge. |
---|
| 884 | nextfunction A (add_functs … ge l) = nat_plus_pos (|l|) (nextfunction A ge). |
---|
| 885 | #A #l elim l // #h #t #IH #ge |
---|
| 886 | whd in ⊢ (??%%); >IH // |
---|
| 887 | qed. |
---|
| 888 | |
---|
[2608] | 889 | lemma alloc_pair : ∀m,m',l,h,l',h'(*,r*). ∀P:mem×block (*(Σb:block. block_region b = r)*) → mem×block(*(Σb:block. block_region b = r)*) → Type[0]. |
---|
[2439] | 890 | nextblock m = nextblock m' → |
---|
| 891 | (∀m1,m2,b. nextblock m1 = nextblock m2 → P 〈m1,b〉 〈m2,b〉) → |
---|
[2608] | 892 | P (alloc m l h (*r*)) (alloc m' l' h' (*r*)). |
---|
| 893 | * #ct #nx #NX * #ct' #nx' #NX' #l #h #l' #h' (* #r *) #P #N destruct #H @H % |
---|
[2439] | 894 | qed. |
---|
| 895 | |
---|
| 896 | lemma vars_irrelevant_to_find_funct_ptr : |
---|
| 897 | ∀F,G,V,W. |
---|
| 898 | ∀P:F → G → Prop. |
---|
| 899 | ∀init,init',b,vars,vars',ge,ge',m,m',f. |
---|
| 900 | (find_funct_ptr F ge b = Some ? f → ∃f'. find_funct_ptr G ge' b = Some ? f' ∧ P f f') → |
---|
| 901 | symbols F ge = symbols G ge' → |
---|
| 902 | nextblock m = nextblock m' → |
---|
| 903 | All2 … (λx,y. \fst x = \fst y) vars vars' → |
---|
| 904 | find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = Some ? f → |
---|
| 905 | ∃f'.find_funct_ptr G (\fst (add_globals G W init' 〈ge',m'〉 vars')) b = Some ? f' ∧ P f f'. |
---|
| 906 | #F #G #V #W #P #init #init' |
---|
[2608] | 907 | * * [ 2,3(*,5,6*): #blk ] [ 2: | 1,3: #vars #vars' #ge #ge' #m #m' #f #H1 #H2 #H3 #H4 #H5 whd in H5:(??%?); destruct ] |
---|
[2439] | 908 | #vars elim vars |
---|
| 909 | [ * [ #ge #ge' #m #m' #f #H #_ #_ #_ @H |
---|
| 910 | | #x #tl #ge #ge' #m #m' #f #_ #_ #_ * |
---|
| 911 | ] |
---|
| 912 | | * * #id #r #v #tl #IH * |
---|
| 913 | [ #ge #ge' #m #m' #f #_ #_ #_ * |
---|
| 914 | | * * #id' #r' #v' #tl' |
---|
| 915 | #ge #ge' #m #m' #f #FFP1 #Esym #Enext * #E destruct #MATCH |
---|
| 916 | whd in match (add_globals ?????); whd in match (add_globals G ????); |
---|
| 917 | whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?)); |
---|
| 918 | @(alloc_pair … Enext) #m1 #m2 #b #Enext' |
---|
| 919 | whd in ⊢ (??(??(???(????%?))?)? → ??(λ_.?(??(??(???(????%?))?)?)?)); |
---|
| 920 | #FFP |
---|
| 921 | @(IH … MATCH FFP) |
---|
| 922 | [ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 923 | whd in ⊢ (??(???%)? → ??(λ_.?(??(???%)?)?)); |
---|
| 924 | >Esym |
---|
| 925 | cases (lookup … id') |
---|
| 926 | [ @FFP1 |
---|
[2608] | 927 | | * * (* * *) try @FFP1 #p try @FFP1 |
---|
[2439] | 928 | normalize |
---|
| 929 | cases (decidable_eq_pos blk p) |
---|
| 930 | [ #E destruct >lookup_opt_pm_set_hit #E destruct |
---|
| 931 | | #NE >(lookup_opt_pm_set_miss … NE) >(lookup_opt_pm_set_miss … NE) |
---|
| 932 | @FFP1 |
---|
| 933 | ] |
---|
| 934 | ] |
---|
| 935 | | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
| 936 | whd in match (add_symbol ????); whd in match (drop_fn ???); |
---|
| 937 | >Esym % |
---|
| 938 | | assumption |
---|
| 939 | ] |
---|
| 940 | ] |
---|
| 941 | ] qed. |
---|
| 942 | |
---|
[2105] | 943 | (* Now link functions in related programs, but without dealing with the type |
---|
| 944 | casts yet. *) |
---|
| 945 | |
---|
[2439] | 946 | lemma symbols_drop_fn_eq : ∀A,B,ge,ge',id. |
---|
| 947 | symbols A ge = symbols B ge' → |
---|
| 948 | symbols A (drop_fn A id ge) = symbols B (drop_fn B id ge'). |
---|
| 949 | #A #B #ge #ge' #id #E |
---|
| 950 | whd in ⊢ (??(??%)(??%)); |
---|
| 951 | >E % |
---|
| 952 | qed. |
---|
| 953 | |
---|
| 954 | lemma ge_add_functs : ∀A,B,fns,fns'. |
---|
| 955 | All2 ?? (λx,y. \fst x = \fst y) fns fns' → |
---|
| 956 | symbols A (add_functs A (empty ?) fns) = symbols B (add_functs B (empty ?) fns') ∧ |
---|
| 957 | nextfunction A (add_functs A (empty ?) fns) = nextfunction B (add_functs B (empty ?) fns'). |
---|
| 958 | #A #B |
---|
| 959 | #fns elim fns |
---|
| 960 | [ * [ #_ % % | #h #t * ] |
---|
| 961 | | * #id #a #tl #IH * * #id' #b #tl' * #E destruct #TL |
---|
| 962 | whd in match (add_functs ???); whd in match (add_functs B ??); |
---|
| 963 | cases (IH ? TL) #S #N >N % [2: % ] |
---|
| 964 | >(symbols_drop_fn_eq A B (foldr ??? (empty A) tl) (foldr ?? (add_funct B) (empty B) tl')) |
---|
| 965 | [ % |
---|
| 966 | | @S |
---|
| 967 | ] |
---|
| 968 | ] qed. |
---|
| 969 | |
---|
| 970 | lemma lookup_drop_fn_different : ∀F,ge,id,b,f. |
---|
| 971 | lookup_opt ? b (functions ? (drop_fn F id ge)) = Some ? f → |
---|
[2608] | 972 | lookup … (symbols ? ge) id ≠ Some ? (mk_block (*Code*) (neg b)). |
---|
[2439] | 973 | #F #ge #id #b #f |
---|
| 974 | whd in match (drop_fn F id ge); |
---|
| 975 | cases (lookup … id) |
---|
| 976 | [ #_ % #E destruct |
---|
[2608] | 977 | | * * (* * *) [2,3(*,5,6*): #b'] normalize |
---|
| 978 | [ 2: cases (decidable_eq_pos b b') |
---|
[2439] | 979 | [ #E destruct >lookup_opt_pm_set_hit #E destruct |
---|
| 980 | | #NE #_ @(not_to_not … NE) #E destruct // |
---|
| 981 | ] |
---|
| 982 | | *: #_ % #E destruct |
---|
| 983 | ] |
---|
[2608] | 984 | ] qed. |
---|
[2439] | 985 | |
---|
| 986 | lemma lookup_drop_fn_irrelevant : ∀F,ge,id,b. |
---|
[2608] | 987 | lookup … (symbols ? ge) id ≠ Some ? (mk_block (* Code *) (neg b)) → |
---|
[2439] | 988 | lookup_opt ? b (functions ? (drop_fn F id ge)) = lookup_opt ? b (functions ? ge). |
---|
| 989 | #F #ge #id #b |
---|
| 990 | whd in match (drop_fn F id ge); |
---|
| 991 | cases (lookup … id) |
---|
| 992 | [ // |
---|
[2608] | 993 | | * * (* * *) // |
---|
[2439] | 994 | #b' normalize #NE |
---|
| 995 | @lookup_opt_pm_set_miss |
---|
| 996 | @(not_to_not … NE) |
---|
| 997 | #E destruct % |
---|
| 998 | ] qed. |
---|
| 999 | |
---|
[2105] | 1000 | lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P. |
---|
[2439] | 1001 | All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') → |
---|
| 1002 | All2 … (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p') → |
---|
[2105] | 1003 | find_funct_ptr … (globalenv A V initV p) b = Some ? f → |
---|
| 1004 | ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'. |
---|
| 1005 | #A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P |
---|
[2439] | 1006 | #Mfns |
---|
[2608] | 1007 | cases b * (* * *) [ 2,3 (*,5,6*) (*,8,9,11,12,14,15,17,18*): #bp ] |
---|
| 1008 | [ 2: (*12:*) | *: #_ #F whd in F:(??%?); destruct ] |
---|
[2439] | 1009 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
| 1010 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
| 1011 | @vars_irrelevant_to_find_funct_ptr |
---|
| 1012 | [ letin varnames ≝ (map ??? vars) |
---|
| 1013 | generalize in match fns' in Mfns ⊢ %; |
---|
| 1014 | elim fns |
---|
| 1015 | [ #fns' #Mfns whd in ⊢ (??%? → ?); #E destruct |
---|
| 1016 | | * #id #fn #tl #IH * * #id' #fn' #tl' * * #E #Phd destruct #Mtl |
---|
| 1017 | whd in ⊢ (??%? → ?); |
---|
[2105] | 1018 | whd in match (functions ??); |
---|
[2439] | 1019 | change with (add_functs ???) in match (foldr ?????); |
---|
| 1020 | cases (ge_add_functs ?? tl tl' ?) [2: @(All2_mp … Mtl) * #idA #a * #idB #b * // ] |
---|
| 1021 | #SYMS #NEXT |
---|
| 1022 | cases (decidable_eq_pos bp (nextfunction … (add_functs ? (empty ?) tl))) |
---|
| 1023 | [ #E destruct >lookup_opt_insert_hit #E destruct |
---|
| 1024 | %{fn'} % // whd in ⊢ (??%?); |
---|
| 1025 | whd in match (functions ??); |
---|
| 1026 | change with (add_functs ???) in match (foldr ???? tl'); |
---|
| 1027 | >NEXT >lookup_opt_insert_hit @refl |
---|
| 1028 | | #NE >lookup_opt_insert_miss // |
---|
| 1029 | #FFP cases (IH tl' Mtl ?) |
---|
| 1030 | [ #fn'' * #FFP' #P' %{fn''} % |
---|
| 1031 | [ whd in ⊢ (??%?); |
---|
| 1032 | >lookup_opt_insert_miss [2: <NEXT // ] |
---|
| 1033 | lapply (lookup_drop_fn_different ????? FFP) |
---|
| 1034 | >SYMS |
---|
| 1035 | #L >lookup_drop_fn_irrelevant // @FFP' |
---|
| 1036 | | @P' |
---|
| 1037 | ] |
---|
| 1038 | | @(drop_fn_lfn … FFP) |
---|
| 1039 | ] |
---|
[2105] | 1040 | ] |
---|
| 1041 | ] |
---|
[2439] | 1042 | | cases (ge_add_functs ?? fns fns' ?) [2: @(All2_mp … Mfns) * #idA #a * #idB #b * // ] |
---|
| 1043 | #S #_ @S |
---|
| 1044 | | @refl |
---|
[2105] | 1045 | ] qed. |
---|
| 1046 | |
---|
[2226] | 1047 | (* lazy proof *) |
---|
| 1048 | lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P. |
---|
| 1049 | find_funct_ptr … (globalenv A V initV p) b = Some ? f → |
---|
| 1050 | All ? (λx. P (\snd x)) (prog_funct ?? p) → |
---|
| 1051 | P f. |
---|
| 1052 | #A #V #b #p #f #initV #P #FFP #ALL |
---|
[2439] | 1053 | cut (All2 ?? (λx,y. \fst x = \fst y ∧ P (\snd x)) (prog_funct ?? p) (prog_funct ?? p)) |
---|
[2226] | 1054 | [ elim (prog_funct … p) in ALL ⊢ %; |
---|
| 1055 | [ // | #h #t #IH * #Hh #Ht % /2/ ] ] |
---|
[2439] | 1056 | cut (All2 ?? (λx,y. \fst x = \fst y) (prog_vars ?? p) (prog_vars ?? p)) |
---|
| 1057 | [ elim (prog_vars … p) [ // | * #x #x' #tl #TL /2/ ] ] |
---|
| 1058 | #VARS2 #FNS2 |
---|
| 1059 | cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FNS2 VARS2 FFP) |
---|
[2226] | 1060 | #x * // |
---|
| 1061 | qed. |
---|
| 1062 | |
---|
| 1063 | |
---|
[2105] | 1064 | discriminator Prod. |
---|
| 1065 | |
---|
| 1066 | (* Now prove the full version. *) |
---|
| 1067 | |
---|
| 1068 | lemma find_funct_ptr_match: |
---|
| 1069 | ∀M:matching.∀initV,initW. |
---|
| 1070 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 1071 | ∀MATCH:match_program … M p p'. |
---|
| 1072 | ∀b: block. ∀f: m_A M (prog_var_names … p). |
---|
| 1073 | find_funct_ptr … (globalenv … initV p) b = Some ? f → |
---|
| 1074 | ∃tf : m_B M (prog_var_names … p'). |
---|
| 1075 | find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). |
---|
| 1076 | [ 2: >(matching_vars … (mp_vars … MATCH)) % ] |
---|
| 1077 | * #A #B #V #W #match_fn #match_var #initV #initW |
---|
| 1078 | #p #p' * #Mvars #Mfn #Mmain |
---|
| 1079 | #b #f #FFP |
---|
[2439] | 1080 | @(find_funct_ptr_All2 A B V W ????????? FFP) |
---|
| 1081 | [ lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars) |
---|
| 1082 | #E |
---|
| 1083 | @(All2_mp … Mfn) |
---|
| 1084 | * #id #f * #id' #f' |
---|
| 1085 | <E in f' ⊢ %; #f' -Mmain -b -Mfn -Mvars -initV -initW -E |
---|
| 1086 | normalize #H @(match_funct_entry_inv … H) |
---|
| 1087 | #vs #id1 #f1 #f2 #M % // |
---|
| 1088 | | @(All2_mp … Mvars) |
---|
| 1089 | * #x #x' * #y #y' #M inversion M #id #r #v1 #v2 #M' #E1 #E2 #_ destruct // |
---|
[2105] | 1090 | qed. |
---|
| 1091 | |
---|
| 1092 | lemma |
---|
| 1093 | find_funct_ptr_transf_partial2: |
---|
| 1094 | ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W. |
---|
| 1095 | ∀p: program A V. ∀p': program B W. |
---|
| 1096 | transform_partial_program2 … p transf_fun transf_var = OK ? p' → |
---|
| 1097 | ∀b: block. ∀f: A ?. |
---|
| 1098 | find_funct_ptr ? (globalenv … iV p) b = Some ? f → |
---|
| 1099 | ∃f'. |
---|
| 1100 | find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'. |
---|
| 1101 | #A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP |
---|
| 1102 | cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP) |
---|
| 1103 | [2: @iW |
---|
| 1104 | | #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E |
---|
| 1105 | #TF %{f'} % // |
---|
| 1106 | -FFP -TPP2 -FFP' >TF -TF >E in f' ⊢ %; #f' % |
---|
| 1107 | qed. |
---|
| 1108 | |
---|
| 1109 | lemma match_funct_entry_id : ∀M,vs,vs',f,g. |
---|
| 1110 | match_funct_entry M vs vs' f g → \fst f = \fst g. |
---|
| 1111 | #M #vs #vs' #f #g * // |
---|
| 1112 | qed. |
---|
| 1113 | |
---|
[2722] | 1114 | lemma symbols_match: |
---|
[2105] | 1115 | ∀M:matching. |
---|
| 1116 | ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
| 1117 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 1118 | match_program … M p p' → |
---|
[2722] | 1119 | symbols ? (globalenv … initW p') = symbols ? (globalenv … initV p). |
---|
[2105] | 1120 | * #A #B #V #W #match_fun #match_var #initV #initW #initsize |
---|
[2722] | 1121 | * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain |
---|
[2105] | 1122 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
| 1123 | whd in match (globalenv ????); whd in match (globalenv_allocmem ????); |
---|
| 1124 | change with (add_globals ?????) in match (foldl ?????); |
---|
| 1125 | change with (add_globals ?????) in match (foldl ? (ident×region×V) ???); |
---|
[2722] | 1126 | @sym_eq |
---|
[2107] | 1127 | @(proj1 … (add_globals_match … Mvars)) |
---|
| 1128 | [ @(matching_fns_get_same_blocks … Mfns) |
---|
[2105] | 1129 | #f #g @match_funct_entry_id |
---|
[2107] | 1130 | | * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ] |
---|
[2105] | 1131 | ] qed. |
---|
[2722] | 1132 | |
---|
| 1133 | lemma |
---|
| 1134 | find_symbol_match: |
---|
| 1135 | ∀M:matching. |
---|
| 1136 | ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → |
---|
| 1137 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 1138 | match_program … M p p' → |
---|
| 1139 | ∀s: ident. |
---|
| 1140 | find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s. |
---|
| 1141 | #M #initV #initW #initsize #p1 #p2 #MATCH #s |
---|
| 1142 | whd in ⊢ (??%%); >(symbols_match M … initsize … MATCH) % |
---|
| 1143 | qed. |
---|
[2105] | 1144 | |
---|
| 1145 | lemma |
---|
| 1146 | find_symbol_transf_partial2: |
---|
| 1147 | ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W. |
---|
| 1148 | (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) → |
---|
| 1149 | ∀p: program A V. ∀p': program B W. |
---|
| 1150 | transform_partial_program2 … p transf_fun transf_var = OK ? p' → |
---|
| 1151 | ∀s: ident. |
---|
| 1152 | find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s. |
---|
| 1153 | #A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s |
---|
| 1154 | @(find_symbol_match … (transform_partial_program2_match … TPP2)) |
---|
| 1155 | #v0 #w0 * #id #r #v #w @sizeOK |
---|
| 1156 | qed. |
---|
| 1157 | |
---|
| 1158 | lemma |
---|
| 1159 | find_funct_ptr_transf: |
---|
| 1160 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
| 1161 | ∀b: block. ∀f: A ?. |
---|
| 1162 | find_funct_ptr ? (globalenv … iV p) b = Some ? f → |
---|
| 1163 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f). |
---|
| 1164 | #A #B #V #iV * #vars #fns #main #tf #b #f #FFP |
---|
| 1165 | cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP) |
---|
| 1166 | [ 2: @iV |
---|
| 1167 | | #f' * #FFP' |
---|
[2117] | 1168 | whd in ⊢ (???(match % with [_⇒?]) → ?); (* XXX this line only required to workaround unification bug *) |
---|
[2105] | 1169 | generalize in match (matching_vars ????); |
---|
| 1170 | whd in match (prog_var_names ???); whd in match (prog_vars ???); |
---|
| 1171 | #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' % |
---|
| 1172 | ] qed. |
---|
| 1173 | |
---|
| 1174 | lemma |
---|
| 1175 | find_funct_transf: |
---|
| 1176 | ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. |
---|
| 1177 | ∀v: val. ∀f: A ?. |
---|
| 1178 | find_funct ? (globalenv … iV p) v = Some ? f → |
---|
| 1179 | find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f). |
---|
| 1180 | #A #B #V #iV #tf #p #v #f #FF |
---|
| 1181 | cases (find_funct_find_funct_ptr ???? FF) |
---|
[2176] | 1182 | #b * #E destruct #FFP |
---|
[2105] | 1183 | change with (find_funct_ptr ???) in ⊢ (??%?); |
---|
| 1184 | @(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *) |
---|
| 1185 | qed. |
---|
| 1186 | |
---|
| 1187 | lemma |
---|
| 1188 | find_symbol_transf: |
---|
| 1189 | ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. |
---|
| 1190 | ∀s: ident. |
---|
| 1191 | find_symbol ? (globalenv … iV (transform_program … p transf)) s = |
---|
| 1192 | find_symbol ? (globalenv … iV p) s. |
---|
| 1193 | #A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?)) |
---|
| 1194 | #v0 #w0 * // |
---|
| 1195 | qed. |
---|
| 1196 | |
---|
[2107] | 1197 | lemma store_init_data_symbols : ∀A,B,ge,ge',m,b,o,d. |
---|
| 1198 | symbols A ge = symbols … ge' → |
---|
| 1199 | store_init_data A ge m b o d = store_init_data B ge' m b o d. |
---|
| 1200 | #A #B #ge #ge' #m #b #o #d #SYM |
---|
| 1201 | whd in ⊢ (??%%); |
---|
[2176] | 1202 | cases d try #d' try @refl |
---|
| 1203 | #n whd in ⊢ (??%%); |
---|
[2107] | 1204 | whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl |
---|
| 1205 | qed. |
---|
[2105] | 1206 | |
---|
[2107] | 1207 | lemma store_init_data_list_symbols : ∀A,B,ge,ge',b. |
---|
| 1208 | symbols A ge = symbols … ge' → |
---|
| 1209 | ∀d,m,o. store_init_data_list A ge m b o d = store_init_data_list B ge' m b o d. |
---|
| 1210 | #A #B #ge #ge' #b #SYM #d elim d |
---|
| 1211 | [ // |
---|
| 1212 | | #hd #tl #IH #m #o |
---|
| 1213 | whd in ⊢ (??%%); |
---|
| 1214 | >(store_init_data_symbols … SYM) |
---|
| 1215 | cases (store_init_data ??????) |
---|
| 1216 | [ % |
---|
| 1217 | | #m' @IH |
---|
| 1218 | ] |
---|
| 1219 | ] qed. |
---|
| 1220 | |
---|
| 1221 | lemma init_globals_match : ∀A,B,V,W. ∀P:ident × region × V → ident × region × W → Prop. |
---|
| 1222 | ∀iV,iW. (∀v,w. P v w → \fst v = \fst w ∧ iV (\snd v) = iW (\snd w)) → |
---|
| 1223 | ∀ge:genv_t A. ∀ge':genv_t B. |
---|
| 1224 | symbols … ge = symbols … ge' → |
---|
| 1225 | ∀m. ∀vars,vars'. |
---|
| 1226 | All2 … P vars vars' → |
---|
| 1227 | init_globals A V iV ge m vars = init_globals B W iW ge' m vars'. |
---|
| 1228 | #A #B #V #W #P #iV #iW #varsOK #ge #ge' #SYM #m #vars |
---|
| 1229 | whd in ⊢ (? → ? → ??%%); |
---|
| 1230 | generalize in match (OK ? m); |
---|
| 1231 | elim vars |
---|
| 1232 | [ #rm * |
---|
| 1233 | [ #_ % |
---|
| 1234 | | #h #t * |
---|
| 1235 | ] |
---|
| 1236 | | * #idr #v #tl #IH #rm |
---|
| 1237 | * [ * ] |
---|
| 1238 | * #idr' #w #tl' |
---|
| 1239 | * #p cases (varsOK … p) #E1 #E2 destruct #TL |
---|
| 1240 | whd in ⊢ (??%%); cases idr' #id #r cases rm #m' |
---|
| 1241 | whd in ⊢ (??(????%?)(????%?)); |
---|
| 1242 | [ whd in match (find_symbol ?? id); |
---|
| 1243 | whd in match (find_symbol B ? id); |
---|
| 1244 | >SYM cases (lookup ??? id) |
---|
| 1245 | [ 2: #b whd in ⊢ (??(????%?)(????%?)); >E2 >(store_init_data_list_symbols … SYM) ] |
---|
| 1246 | ] @IH // |
---|
| 1247 | ] qed. |
---|
| 1248 | |
---|
| 1249 | lemma |
---|
| 1250 | init_mem_match: |
---|
| 1251 | ∀M:matching. |
---|
| 1252 | ∀iV,iW. (∀v,w. match_varinfo M v w → iV v = iW w) → |
---|
| 1253 | ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). |
---|
| 1254 | match_program … M p p' → |
---|
| 1255 | init_mem … iW p' = init_mem … iV p. |
---|
| 1256 | * #A #B #V #W #match_fn #match_var #iV #iW #iSAME #p #p' * #Mvars #Mfns #Mmain |
---|
| 1257 | whd in ⊢ (??%%); |
---|
| 1258 | change with (add_globals ?????) in match (globalenv_allocmem ??? p'); |
---|
| 1259 | change with (add_globals ?????) in match (globalenv_allocmem ??? p); |
---|
| 1260 | cases (add_globals_match (A ?) (B ?) V W iV iW ?? (prog_vars … p) ??? (prog_vars … p') ? Mvars) |
---|
| 1261 | [ 8: @(matching_fns_get_same_blocks … Mfns) |
---|
| 1262 | #f0 #g0 * // |
---|
| 1263 | | cases (add_globals ?????) #ge1 #m1 |
---|
| 1264 | cases (add_globals ?????) #ge2 #m2 |
---|
| 1265 | #SYM #MEM destruct @sym_eq @(init_globals_match … Mvars) |
---|
| 1266 | [ #v0 #w0 * #id #r #v #w /3/ |
---|
| 1267 | | @SYM |
---|
| 1268 | ] |
---|
| 1269 | | 4: #v0 #w0 * #id #r #v #w #V % // >iSAME // |
---|
| 1270 | | *: skip |
---|
| 1271 | ] qed. |
---|
| 1272 | |
---|
| 1273 | lemma |
---|
| 1274 | init_mem_transf: |
---|
| 1275 | ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. |
---|
| 1276 | init_mem … iV (transform_program … p transf) = init_mem … iV p. |
---|
| 1277 | #A #B #C #iV #transf #p |
---|
| 1278 | @(init_mem_match … (transform_program_match … transf ?)) |
---|
| 1279 | // |
---|
| 1280 | qed. |
---|
[2319] | 1281 | |
---|
| 1282 | lemma |
---|
| 1283 | init_mem_transf_gen: |
---|
| 1284 | ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V. |
---|
| 1285 | init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p. |
---|
| 1286 | #tag #A #B #C #iV #g #transf #p |
---|
| 1287 | @(init_mem_match … (transform_program_gen_match … transf ?)) |
---|
| 1288 | // |
---|
| 1289 | qed. |
---|
[2107] | 1290 | |
---|
| 1291 | |
---|
| 1292 | (* Package up transform_program results for global envs nicely. *) |
---|
| 1293 | |
---|
[2105] | 1294 | record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ { |
---|
| 1295 | rg_find_symbol: ∀s. |
---|
| 1296 | find_symbol … ge s = find_symbol … ge' s; |
---|
[2722] | 1297 | rg_symbol_for : ∀b. |
---|
| 1298 | symbol_for_block … ge b = symbol_for_block … ge' b; |
---|
[2105] | 1299 | rg_find_funct: ∀v,f. |
---|
| 1300 | find_funct … ge v = Some ? f → |
---|
| 1301 | find_funct … ge' v = Some ? (t f); |
---|
| 1302 | rg_find_funct_ptr: ∀b,f. |
---|
| 1303 | find_funct_ptr … ge b = Some ? f → |
---|
| 1304 | find_funct_ptr … ge' b = Some ? (t f) |
---|
| 1305 | }. |
---|
| 1306 | |
---|
[2722] | 1307 | lemma rg_find_funct_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀v,f,id. |
---|
| 1308 | find_funct_id … ge v = Some ? 〈f,id〉 → |
---|
| 1309 | find_funct_id … ge' v = Some ? 〈t f,id〉. |
---|
| 1310 | #A #B #t #ge #ge' #RG #v #f #id #FFI |
---|
| 1311 | cases (find_funct_id_ptr ????? FFI) |
---|
[2895] | 1312 | #b * * #E1 #FS #FFPI |
---|
[2722] | 1313 | cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM |
---|
| 1314 | lapply (rg_find_funct_ptr … RG … FFP) #FFP' |
---|
| 1315 | >(rg_symbol_for … RG b) in SYM; #SYM' |
---|
| 1316 | lapply (make_find_funct_ptr_id … FFP' SYM') |
---|
| 1317 | >E1 @find_funct_ptr_id_conv |
---|
| 1318 | qed. |
---|
| 1319 | |
---|
| 1320 | lemma rg_find_funct_ptr_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀b,f,id. |
---|
| 1321 | find_funct_ptr_id … ge b = Some ? 〈f,id〉 → |
---|
| 1322 | find_funct_ptr_id … ge' b = Some ? 〈t f,id〉. |
---|
| 1323 | #A #B #t #ge #ge' #RG #b #f #id #FFPI |
---|
| 1324 | cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM |
---|
| 1325 | lapply (rg_find_funct_ptr … RG … FFP) #FFP' |
---|
| 1326 | >(rg_symbol_for … RG b) in SYM; #SYM' |
---|
| 1327 | @(make_find_funct_ptr_id … FFP' SYM') |
---|
| 1328 | qed. |
---|
| 1329 | |
---|
| 1330 | |
---|
| 1331 | |
---|
[2105] | 1332 | theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs. |
---|
| 1333 | related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)). |
---|
| 1334 | #A #B #V #iV #p #tf % |
---|
| 1335 | [ #s @sym_eq @(find_symbol_transf A B V iV tf p) |
---|
[2722] | 1336 | | #b whd in ⊢ (??%%); >(symbols_match … (transform_program_match … tf ?)) |
---|
| 1337 | [ % | #v #w * #id #r #v1 #v2 #E destruct % | skip ] |
---|
[2105] | 1338 | | @(find_funct_transf A B V iV tf p) |
---|
| 1339 | | @(find_funct_ptr_transf A B V iV p tf) |
---|
| 1340 | ] qed. |
---|
| 1341 | |
---|
[2645] | 1342 | record related_globals_gen (tag:identifierTag) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ { |
---|
[2319] | 1343 | rgg_find_symbol: ∀s. |
---|
| 1344 | find_symbol … ge s = find_symbol … ge' s; |
---|
[2722] | 1345 | rgg_symbol_for : ∀b. |
---|
| 1346 | symbol_for_block … ge b = symbol_for_block … ge' b; |
---|
[2319] | 1347 | rgg_find_funct_ptr: ∀b,f. |
---|
| 1348 | find_funct_ptr … ge b = Some ? f → |
---|
| 1349 | ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f)); |
---|
| 1350 | rgg_find_funct: ∀v,f. |
---|
| 1351 | find_funct … ge v = Some ? f → |
---|
| 1352 | ∃g. find_funct … ge' v = Some ? (\fst (t g f)) |
---|
| 1353 | }. |
---|
[2105] | 1354 | |
---|
[2722] | 1355 | lemma rgg_find_funct_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀v,f,id. |
---|
| 1356 | find_funct_id … ge v = Some ? 〈f,id〉 → |
---|
| 1357 | ∃g. find_funct_id … ge' v = Some ? 〈\fst (t g f),id〉. |
---|
| 1358 | #tag #A #B #t #ge #ge' #RG #v #f #id #FFI |
---|
| 1359 | cases (find_funct_id_ptr ????? FFI) |
---|
[2895] | 1360 | #b * * #E1 #FS #FFPI |
---|
[2722] | 1361 | cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM |
---|
| 1362 | cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g} |
---|
| 1363 | >(rgg_symbol_for … RG b) in SYM; #SYM' |
---|
| 1364 | lapply (make_find_funct_ptr_id … FFP' SYM') |
---|
| 1365 | >E1 @find_funct_ptr_id_conv |
---|
| 1366 | qed. |
---|
| 1367 | |
---|
| 1368 | lemma rgg_find_funct_ptr_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀b,f,id. |
---|
| 1369 | find_funct_ptr_id … ge b = Some ? 〈f,id〉 → |
---|
| 1370 | ∃g. find_funct_ptr_id … ge' b = Some ? 〈\fst (t g f),id〉. |
---|
| 1371 | #tag #A #B #t #ge #ge' #RG #b #f #id #FFPI |
---|
| 1372 | cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM |
---|
| 1373 | cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g} |
---|
| 1374 | >(rgg_symbol_for … RG b) in SYM; #SYM' |
---|
| 1375 | @(make_find_funct_ptr_id … FFP' SYM') |
---|
| 1376 | qed. |
---|
| 1377 | |
---|
[2601] | 1378 | include "utilities/extra_bool.ma". |
---|
[2319] | 1379 | |
---|
| 1380 | theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag). |
---|
| 1381 | 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))). |
---|
| 1382 | #tag #A #B #V #iV #g #p #tf % |
---|
| 1383 | [ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p)) |
---|
| 1384 | #v #w * // |
---|
[2722] | 1385 | | #b whd in ⊢ (??%%); >(symbols_match … (transform_program_gen_match … tf p)) |
---|
| 1386 | [ % | #v #w * #id #r #v1 #v2 #E destruct % | skip ] |
---|
[2319] | 1387 | | #b #f #FFP |
---|
| 1388 | cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP) |
---|
| 1389 | [ 2: @iV |
---|
| 1390 | | #fn' * #FFP' |
---|
| 1391 | generalize in match (matching_vars ????); |
---|
| 1392 | whd in match (prog_var_names ???); whd in match (prog_vars ???); |
---|
| 1393 | #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' % |
---|
| 1394 | | skip |
---|
| 1395 | ] |
---|
[2468] | 1396 | | * [ 4: #ptr #fn whd in match (find_funct ???); |
---|
[2319] | 1397 | @if_elim #Eoff #FFP |
---|
| 1398 | [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP) |
---|
| 1399 | [ 2: @iV |
---|
| 1400 | | #fn' * #FFP' |
---|
| 1401 | generalize in match (matching_vars ????); |
---|
| 1402 | whd in match (prog_var_names ???); whd in match (prog_vars ???); |
---|
| 1403 | #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' |
---|
| 1404 | %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' % |
---|
| 1405 | ] |
---|
| 1406 | | destruct |
---|
| 1407 | ] |
---|
| 1408 | | *: normalize #A #B try #C try #D destruct |
---|
| 1409 | ] |
---|
| 1410 | ] qed. |
---|
| 1411 | |
---|
| 1412 | |
---|
[2105] | 1413 | (* |
---|
| 1414 | |
---|
[3] | 1415 | find_funct_ptr_match: |
---|
[487] | 1416 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 1417 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 1418 | match_program … match_fun match_var p p' → |
---|
| 1419 | ∀b: block. ∀f: A. |
---|
| 1420 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 1421 | ∃tf : B. |
---|
| 1422 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf; |
---|
| 1423 | find_funct_ptr_rev_match: |
---|
[487] | 1424 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 1425 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 1426 | match_program … match_fun match_var p p' → |
---|
| 1427 | ∀b: block. ∀tf: B. |
---|
| 1428 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
| 1429 | ∃f : A. |
---|
| 1430 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf; |
---|
| 1431 | find_funct_match: |
---|
[487] | 1432 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 1433 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 1434 | match_program … match_fun match_var p p' → |
---|
| 1435 | ∀v: val. ∀f: A. |
---|
| 1436 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 1437 | ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf; |
---|
| 1438 | find_funct_rev_match: |
---|
[487] | 1439 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 1440 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 1441 | match_program … match_fun match_var p p' → |
---|
| 1442 | ∀v: val. ∀tf: B. |
---|
| 1443 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 1444 | ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf; |
---|
| 1445 | find_symbol_match: |
---|
[487] | 1446 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 1447 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 1448 | match_program … match_fun match_var p p' → |
---|
| 1449 | ∀s: ident. |
---|
| 1450 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
[2107] | 1451 | *) |
---|
[125] | 1452 | (* |
---|
| 1453 | Definition find_funct_ptr ? (g: genv) (b: block) : option F := |
---|
| 1454 | ZMap.get b g.(functions). |
---|
| 1455 | |
---|
| 1456 | Definition find_funct (g: genv) (v: val) : option F := |
---|
| 1457 | match v with |
---|
| 1458 | | Vptr b ofs => |
---|
| 1459 | if Int.eq ofs Int.zero then find_funct_ptr ? g b else None |
---|
| 1460 | | _ => |
---|
| 1461 | None |
---|
| 1462 | end. |
---|
| 1463 | |
---|
| 1464 | Definition find_symbol ? (g: genv) (symb: ident) : option block := |
---|
| 1465 | PTree.get symb g.(symbols). |
---|
| 1466 | |
---|
| 1467 | Lemma find_funct_inv: |
---|
| 1468 | forall (ge: t) (v: val) (f: F), |
---|
| 1469 | find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero. |
---|
| 1470 | Proof. |
---|
| 1471 | intros until f. unfold find_funct. destruct v; try (intros; discriminate). |
---|
| 1472 | generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros. |
---|
| 1473 | exists b. congruence. |
---|
| 1474 | discriminate. |
---|
| 1475 | Qed. |
---|
| 1476 | |
---|
| 1477 | Lemma find_funct_find_funct_ptr: |
---|
| 1478 | forall (ge: t) (b: block), |
---|
| 1479 | find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. |
---|
| 1480 | Proof. |
---|
| 1481 | intros. simpl. |
---|
| 1482 | generalize (Int.eq_spec Int.zero Int.zero). |
---|
| 1483 | case (Int.eq Int.zero Int.zero); intros. |
---|
| 1484 | auto. tauto. |
---|
| 1485 | Qed. |
---|
| 1486 | *) |
---|
| 1487 | |
---|
| 1488 | (* |
---|
[487] | 1489 | ##[ #A B C transf p b f; elim p; #fns main vars; |
---|
| 1490 | elim fns; |
---|
| 1491 | ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct; |
---|
| 1492 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?); |
---|
[24] | 1493 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1494 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 1495 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 1496 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1497 | ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH; |
---|
| 1498 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 1499 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?); |
---|
| 1500 | ##[ #H; destruct (H); //; |
---|
[24] | 1501 | ##| #H; napply IH; napply H; |
---|
| 1502 | ##] |
---|
| 1503 | ##] |
---|
| 1504 | ##] |
---|
| 1505 | ##] |
---|
[487] | 1506 | ##| #A B C transf p v f; elim v; |
---|
| 1507 | ##[ whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
| 1508 | ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
| 1509 | ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero); |
---|
| 1510 | whd in ⊢ (??%? → ??%?); |
---|
| 1511 | ##[ elim p; #fns main vars; elim fns; |
---|
| 1512 | ##[ whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
| 1513 | ##| #h t; elim h; #f fn IH; |
---|
| 1514 | whd in ⊢ (??%? → ??%?); |
---|
[24] | 1515 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1516 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 1517 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 1518 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1519 | ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH; |
---|
| 1520 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 1521 | ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H; |
---|
| 1522 | ##[ destruct (H); //; |
---|
[24] | 1523 | ##| napply IH; napply H; |
---|
| 1524 | ##] |
---|
| 1525 | ##] |
---|
| 1526 | ##] |
---|
| 1527 | ##] |
---|
[487] | 1528 | ##| #H; destruct; |
---|
[24] | 1529 | ##] |
---|
| 1530 | ##] |
---|
[487] | 1531 | ##| #A B C transf p id; elim p; #fns main vars; |
---|
| 1532 | elim fns; |
---|
| 1533 | ##[ normalize; // |
---|
| 1534 | ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH; |
---|
| 1535 | elim (ident_eq fid id); #e; |
---|
| 1536 | ##[ whd in ⊢ (??%%); |
---|
[24] | 1537 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1538 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 1539 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 1540 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1541 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 1542 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 1543 | ##| // |
---|
| 1544 | ##] |
---|
| 1545 | ##] |
---|
[487] | 1546 | ##| whd in ⊢ (??%%); nrewrite > IH; napply refl; |
---|
[24] | 1547 | ##] |
---|
| 1548 | ##] |
---|
| 1549 | ##| //; |
---|
[487] | 1550 | ##| #A B C transf p b tf; elim p; #fns main vars; |
---|
| 1551 | elim fns; |
---|
| 1552 | ##[ normalize; #H; destruct; |
---|
| 1553 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
[24] | 1554 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1555 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 1556 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 1557 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1558 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 1559 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 1560 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 1561 | ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; |
---|
[24] | 1562 | ##| #H; napply IH; napply H; |
---|
| 1563 | ##] |
---|
| 1564 | ##] |
---|
| 1565 | ##] |
---|
| 1566 | ##] |
---|
[487] | 1567 | ##| #A B C transf p v tf; elim p; #fns main vars; elim v; |
---|
| 1568 | ##[ normalize; #H; destruct; |
---|
| 1569 | ##| ##2,3: #x; normalize; #H; destruct; |
---|
| 1570 | ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero); |
---|
| 1571 | ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 1572 | elim fns; |
---|
| 1573 | ##[ normalize; #H; destruct; |
---|
| 1574 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
[24] | 1575 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1576 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 1577 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 1578 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 1579 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 1580 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 1581 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 1582 | ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; |
---|
[24] | 1583 | ##| #H; napply IH; napply H; |
---|
| 1584 | ##] |
---|
| 1585 | ##] |
---|
| 1586 | ##] |
---|
| 1587 | ##] |
---|
[487] | 1588 | ##| normalize; #H; destruct; |
---|
[24] | 1589 | ##] |
---|
| 1590 | ##] |
---|
[487] | 1591 | ##] qed. |
---|
[24] | 1592 | |
---|
[3] | 1593 | |
---|
| 1594 | Lemma functions_globalenv: |
---|
| 1595 | forall (p: program F V), |
---|
| 1596 | functions (globalenv p) = functions (add_functs empty p.(prog_funct)). |
---|
| 1597 | Proof. |
---|
| 1598 | assert (forall init vars, |
---|
| 1599 | functions (fst (add_globals init vars)) = functions (fst init)). |
---|
| 1600 | induction vars; simpl. |
---|
| 1601 | reflexivity. |
---|
| 1602 | destruct a as [[id1 init1] info1]. destruct (add_globals init vars). |
---|
| 1603 | simpl. exact IHvars. |
---|
| 1604 | |
---|
| 1605 | unfold add_globals; simpl. |
---|
| 1606 | intros. unfold globalenv; unfold globalenv_initmem. |
---|
| 1607 | rewrite H. reflexivity. |
---|
| 1608 | Qed. |
---|
| 1609 | |
---|
| 1610 | Lemma initmem_nullptr: |
---|
| 1611 | forall (p: program F V), |
---|
| 1612 | let m := init_mem p in |
---|
| 1613 | valid_block m nullptr /\ |
---|
| 1614 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef). |
---|
| 1615 | Proof. |
---|
| 1616 | pose (P := fun m => valid_block m nullptr /\ |
---|
| 1617 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)). |
---|
| 1618 | assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))). |
---|
| 1619 | induction vars; simpl; intros. |
---|
| 1620 | auto. |
---|
| 1621 | destruct a as [[id1 in1] inf1]. |
---|
| 1622 | destruct (add_globals init vars) as [g st]. |
---|
| 1623 | simpl in *. destruct IHvars. split. |
---|
| 1624 | red; simpl. red in H0. omega. |
---|
| 1625 | simpl. rewrite update_o. auto. unfold block. red in H0. omega. |
---|
| 1626 | |
---|
| 1627 | intro. unfold init_mem, globalenv_initmem. apply H. |
---|
| 1628 | red; simpl. split. compute. auto. reflexivity. |
---|
| 1629 | Qed. |
---|
| 1630 | |
---|
| 1631 | Lemma initmem_inject_neutral: |
---|
| 1632 | forall (p: program F V), |
---|
| 1633 | mem_inject_neutral (init_mem p). |
---|
| 1634 | Proof. |
---|
| 1635 | assert (forall g0 vars g1 m, |
---|
| 1636 | add_globals (g0, Mem.empty) vars = (g1, m) → |
---|
| 1637 | mem_inject_neutral m). |
---|
| 1638 | Opaque alloc_init_data. |
---|
| 1639 | induction vars; simpl. |
---|
| 1640 | intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H). |
---|
| 1641 | simpl in H1. rewrite Mem.getN_init in H1. |
---|
| 1642 | replace v with Vundef. auto. destruct chunk; simpl in H1; auto. |
---|
| 1643 | destruct a as [[id1 init1] info1]. |
---|
| 1644 | caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. |
---|
| 1645 | caseEq (alloc_init_data m1 init1). intros m2 b ALLOC. |
---|
| 1646 | intros. inv H. |
---|
| 1647 | eapply Mem.alloc_init_data_neutral; eauto. |
---|
| 1648 | intros. caseEq (globalenv_initmem p). intros g m EQ. |
---|
| 1649 | unfold init_mem; rewrite EQ; simpl. |
---|
| 1650 | unfold globalenv_initmem in EQ. eauto. |
---|
| 1651 | Qed. |
---|
| 1652 | |
---|
| 1653 | Remark nextfunction_add_functs_neg: |
---|
| 1654 | forall fns, nextfunction (add_functs empty fns) < 0. |
---|
| 1655 | Proof. |
---|
| 1656 | induction fns; simpl; intros. omega. unfold Zpred. omega. |
---|
| 1657 | Qed. |
---|
| 1658 | |
---|
| 1659 | Theorem find_funct_ptr_negative: |
---|
| 1660 | forall (p: program F V) (b: block) (f: F), |
---|
| 1661 | find_funct_ptr ? (globalenv p) b = Some ? f → b < 0. |
---|
| 1662 | Proof. |
---|
| 1663 | intros until f. |
---|
| 1664 | assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0). |
---|
| 1665 | induction fns; simpl. |
---|
| 1666 | rewrite ZMap.gi. congruence. |
---|
| 1667 | rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro. |
---|
| 1668 | intro. rewrite e. apply nextfunction_add_functs_neg. |
---|
| 1669 | auto. |
---|
| 1670 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
| 1671 | intros. eauto. |
---|
| 1672 | Qed. |
---|
| 1673 | |
---|
| 1674 | Remark find_symbol_add_functs_negative: |
---|
| 1675 | forall (fns: list (ident * F)) s b, |
---|
| 1676 | (symbols (add_functs empty fns)) ! s = Some ? b → b < 0. |
---|
| 1677 | Proof. |
---|
| 1678 | induction fns; simpl; intros until b. |
---|
| 1679 | rewrite PTree.gempty. congruence. |
---|
| 1680 | rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro. |
---|
| 1681 | intro EQ; inversion EQ. apply nextfunction_add_functs_neg. |
---|
| 1682 | eauto. |
---|
| 1683 | Qed. |
---|
| 1684 | |
---|
| 1685 | Remark find_symbol_add_symbols_not_fresh: |
---|
| 1686 | forall fns vars g m s b, |
---|
| 1687 | add_globals (add_functs empty fns, Mem.empty) vars = (g, m) → |
---|
| 1688 | (symbols g)!s = Some ? b → |
---|
| 1689 | b < nextblock m. |
---|
| 1690 | Proof. |
---|
| 1691 | induction vars; simpl; intros until b. |
---|
| 1692 | intros. inversion H. subst g m. simpl. |
---|
| 1693 | generalize (find_symbol_add_functs_negative fns s H0). omega. |
---|
| 1694 | Transparent alloc_init_data. |
---|
| 1695 | destruct a as [[id1 init1] info1]. |
---|
| 1696 | caseEq (add_globals (add_functs empty fns, Mem.empty) vars). |
---|
| 1697 | intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. |
---|
| 1698 | unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro. |
---|
| 1699 | intro EQ; inversion EQ. omega. |
---|
| 1700 | intro. generalize (IHvars _ _ _ _ ADG H). omega. |
---|
| 1701 | Qed. |
---|
| 1702 | |
---|
| 1703 | Theorem find_symbol_not_fresh: |
---|
| 1704 | forall (p: program F V) (id: ident) (b: block), |
---|
| 1705 | find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p). |
---|
| 1706 | Proof. |
---|
| 1707 | intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. |
---|
| 1708 | caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty) |
---|
| 1709 | (prog_vars p)); intros g m EQ. |
---|
| 1710 | simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto. |
---|
| 1711 | Qed. |
---|
| 1712 | |
---|
| 1713 | Lemma find_symbol_exists: |
---|
| 1714 | forall (p: program F V) |
---|
| 1715 | (id: ident) (init: list init_data) (v: V), |
---|
| 1716 | In (id, init, v) (prog_vars p) → |
---|
| 1717 | ∃b. find_symbol ? (globalenv p) id = Some ? b. |
---|
| 1718 | Proof. |
---|
| 1719 | intros until v. |
---|
| 1720 | assert (forall initm vl, In (id, init, v) vl → |
---|
| 1721 | ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b). |
---|
| 1722 | induction vl; simpl; intros. |
---|
| 1723 | elim H. |
---|
| 1724 | destruct a as [[id0 init0] v0]. |
---|
| 1725 | caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. |
---|
| 1726 | rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto. |
---|
| 1727 | elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. |
---|
| 1728 | intros. unfold globalenv, find_symbol, globalenv_initmem. auto. |
---|
| 1729 | Qed. |
---|
| 1730 | |
---|
| 1731 | Remark find_symbol_above_nextfunction: |
---|
| 1732 | forall (id: ident) (b: block) (fns: list (ident * F)), |
---|
| 1733 | let g := add_functs empty fns in |
---|
| 1734 | PTree.get id g.(symbols) = Some ? b → |
---|
| 1735 | b > g.(nextfunction). |
---|
| 1736 | Proof. |
---|
| 1737 | induction fns; simpl. |
---|
| 1738 | rewrite PTree.gempty. congruence. |
---|
| 1739 | rewrite PTree.gsspec. case (peq id (fst a)); intro. |
---|
| 1740 | intro EQ. inversion EQ. unfold Zpred. omega. |
---|
| 1741 | intros. generalize (IHfns H). unfold Zpred; omega. |
---|
| 1742 | Qed. |
---|
| 1743 | |
---|
| 1744 | Remark find_symbol_add_globals: |
---|
| 1745 | forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)), |
---|
| 1746 | ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) → |
---|
| 1747 | find_symbol ? (fst (add_globals ge_m vars)) id = |
---|
| 1748 | find_symbol ? (fst ge_m) id. |
---|
| 1749 | Proof. |
---|
| 1750 | unfold find_symbol; induction vars; simpl; intros. |
---|
| 1751 | auto. |
---|
| 1752 | destruct a as [[id0 init0] var0]. simpl in *. |
---|
| 1753 | caseEq (add_globals ge_m vars); intros ge' m' EQ. |
---|
| 1754 | simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. |
---|
| 1755 | apply IHvars. tauto. intuition congruence. |
---|
| 1756 | Qed. |
---|
| 1757 | |
---|
| 1758 | Lemma find_funct_ptr_exists: |
---|
| 1759 | forall (p: program F V) (id: ident) (f: F), |
---|
| 1760 | list_norepet (prog_funct_names p) → |
---|
| 1761 | list_disjoint (prog_funct_names p) (prog_var_names p) → |
---|
| 1762 | In (id, f) (prog_funct p) → |
---|
| 1763 | ∃b. find_symbol ? (globalenv p) id = Some ? b |
---|
| 1764 | /\ find_funct_ptr ? (globalenv p) b = Some ? f. |
---|
| 1765 | Proof. |
---|
| 1766 | intros until f. |
---|
| 1767 | assert (forall (fns: list (ident * F)), |
---|
| 1768 | list_norepet (map (@fst ident F) fns) → |
---|
| 1769 | In (id, f) fns → |
---|
| 1770 | ∃b. find_symbol ? (add_functs empty fns) id = Some ? b |
---|
| 1771 | /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f). |
---|
| 1772 | unfold find_symbol, find_funct_ptr. induction fns; intros. |
---|
| 1773 | elim H0. |
---|
| 1774 | destruct a as [id0 f0]; simpl in *. inv H. |
---|
| 1775 | unfold add_funct; simpl. |
---|
| 1776 | rewrite PTree.gsspec. destruct (peq id id0). |
---|
| 1777 | subst id0. econstructor; split. eauto. |
---|
| 1778 | replace f0 with f. apply ZMap.gss. |
---|
| 1779 | elim H0; intro. congruence. elim H3. |
---|
| 1780 | change id with (@fst ident F (id, f)). apply List.in_map. auto. |
---|
| 1781 | exploit IHfns; eauto. elim H0; intro. congruence. auto. |
---|
| 1782 | intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto. |
---|
| 1783 | generalize (find_symbol_above_nextfunction _ _ X). |
---|
| 1784 | unfold block; unfold ZIndexed.t; intro; omega. |
---|
| 1785 | |
---|
| 1786 | intros. exploit H; eauto. intros [b [X Y]]. |
---|
| 1787 | exists b; split. |
---|
| 1788 | unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. |
---|
| 1789 | assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. |
---|
| 1790 | unfold prog_funct_names. change id with (fst (id, f)). |
---|
| 1791 | apply List.in_map; auto. |
---|
| 1792 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
| 1793 | assumption. |
---|
| 1794 | Qed. |
---|
| 1795 | |
---|
| 1796 | Lemma find_funct_ptr_inversion: |
---|
| 1797 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
| 1798 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1799 | ∃id. In (id, f) (prog_funct p). |
---|
| 1800 | Proof. |
---|
| 1801 | intros until f. |
---|
| 1802 | assert (forall fns: list (ident * F), |
---|
| 1803 | find_funct_ptr ? (add_functs empty fns) b = Some ? f → |
---|
| 1804 | ∃id. In (id, f) fns). |
---|
| 1805 | unfold find_funct_ptr. induction fns; simpl. |
---|
| 1806 | rewrite ZMap.gi. congruence. |
---|
| 1807 | destruct a as [id0 f0]; simpl. |
---|
| 1808 | rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))). |
---|
| 1809 | intro. inv H. exists id0; auto. |
---|
| 1810 | intro. exploit IHfns; eauto. intros [id A]. exists id; auto. |
---|
| 1811 | unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto. |
---|
| 1812 | Qed. |
---|
| 1813 | |
---|
| 1814 | Lemma find_funct_ptr_prop: |
---|
| 1815 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
| 1816 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
| 1817 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1818 | P f. |
---|
| 1819 | Proof. |
---|
| 1820 | intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto. |
---|
| 1821 | Qed. |
---|
| 1822 | |
---|
| 1823 | Lemma find_funct_inversion: |
---|
| 1824 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
| 1825 | find_funct (globalenv p) v = Some ? f → |
---|
| 1826 | ∃id. In (id, f) (prog_funct p). |
---|
| 1827 | Proof. |
---|
| 1828 | intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H. |
---|
| 1829 | rewrite find_funct_find_funct_ptr ? in H. |
---|
| 1830 | eapply find_funct_ptr_inversion; eauto. |
---|
| 1831 | Qed. |
---|
| 1832 | |
---|
| 1833 | Lemma find_funct_prop: |
---|
| 1834 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
| 1835 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
| 1836 | find_funct (globalenv p) v = Some ? f → |
---|
| 1837 | P f. |
---|
| 1838 | Proof. |
---|
| 1839 | intros. exploit find_funct_inversion; eauto. intros [id A]. eauto. |
---|
| 1840 | Qed. |
---|
| 1841 | |
---|
| 1842 | Lemma find_funct_ptr_symbol_inversion: |
---|
| 1843 | forall (p: program F V) (id: ident) (b: block) (f: F), |
---|
| 1844 | find_symbol ? (globalenv p) id = Some ? b → |
---|
| 1845 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1846 | In (id, f) p.(prog_funct). |
---|
| 1847 | Proof. |
---|
| 1848 | intros until f. |
---|
| 1849 | assert (forall fns, |
---|
| 1850 | let g := add_functs empty fns in |
---|
| 1851 | PTree.get id g.(symbols) = Some ? b → |
---|
| 1852 | ZMap.get b g.(functions) = Some ? f → |
---|
| 1853 | In (id, f) fns). |
---|
| 1854 | induction fns; simpl. |
---|
| 1855 | rewrite ZMap.gi. congruence. |
---|
| 1856 | set (g := add_functs empty fns). |
---|
| 1857 | rewrite PTree.gsspec. rewrite ZMap.gsspec. |
---|
| 1858 | case (peq id (fst a)); intro. |
---|
| 1859 | intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. |
---|
| 1860 | intro EQ2. left. destruct a. simpl in *. congruence. |
---|
| 1861 | intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto. |
---|
| 1862 | generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega. |
---|
| 1863 | assert (forall g0 m0, b < 0 → |
---|
| 1864 | forall vars g m, |
---|
| 1865 | add_globals (g0, m0) vars = (g, m) → |
---|
| 1866 | PTree.get id g.(symbols) = Some ? b → |
---|
| 1867 | PTree.get id g0.(symbols) = Some ? b). |
---|
| 1868 | induction vars; simpl. |
---|
| 1869 | intros. inv H1. auto. |
---|
| 1870 | destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). |
---|
| 1871 | intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1. |
---|
| 1872 | unfold add_symbol; intros A B. rewrite <- B. simpl. |
---|
| 1873 | rewrite PTree.gsspec. case (peq id id1); intros. |
---|
| 1874 | assert (b > 0). inv H1. apply nextblock_pos. |
---|
| 1875 | omegaContradiction. |
---|
| 1876 | eauto. |
---|
| 1877 | intros. |
---|
| 1878 | generalize (find_funct_ptr_negative _ _ H2). intro. |
---|
| 1879 | pose (g := add_functs empty (prog_funct p)). |
---|
| 1880 | apply H. |
---|
| 1881 | apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). |
---|
| 1882 | auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. |
---|
| 1883 | reflexivity. assumption. rewrite <- functions_globalenv. assumption. |
---|
| 1884 | Qed. |
---|
| 1885 | |
---|
| 1886 | Theorem find_symbol_not_nullptr: |
---|
| 1887 | forall (p: program F V) (id: ident) (b: block), |
---|
| 1888 | find_symbol ? (globalenv p) id = Some ? b → b <> nullptr. |
---|
| 1889 | Proof. |
---|
| 1890 | intros until b. |
---|
| 1891 | assert (forall fns, |
---|
| 1892 | find_symbol ? (add_functs empty fns) id = Some ? b → |
---|
| 1893 | b <> nullptr). |
---|
| 1894 | unfold find_symbol; induction fns; simpl. |
---|
| 1895 | rewrite PTree.gempty. congruence. |
---|
| 1896 | destruct a as [id1 f1]. simpl. rewrite PTree.gsspec. |
---|
| 1897 | destruct (peq id id1); intros. |
---|
| 1898 | inversion H. generalize (nextfunction_add_functs_neg fns). |
---|
| 1899 | unfold block, nullptr; omega. |
---|
| 1900 | auto. |
---|
| 1901 | set (g0 := add_functs empty p.(prog_funct)). |
---|
| 1902 | assert (forall vars g m, |
---|
| 1903 | add_globals (g0, Mem.empty) vars = (g, m) → |
---|
| 1904 | find_symbol ? g id = Some ? b → |
---|
| 1905 | b <> nullptr). |
---|
| 1906 | induction vars; simpl; intros until m. |
---|
| 1907 | intros. inversion H0. subst g. apply H with (prog_funct p). auto. |
---|
| 1908 | destruct a as [[id1 init1] info1]. |
---|
| 1909 | caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2. |
---|
| 1910 | inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec. |
---|
| 1911 | destruct (peq id id1); intros. |
---|
| 1912 | inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega. |
---|
| 1913 | eauto. |
---|
| 1914 | intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto. |
---|
| 1915 | Qed. |
---|
| 1916 | |
---|
| 1917 | Theorem global_addresses_distinct: |
---|
| 1918 | forall (p: program F V) id1 id2 b1 b2, |
---|
| 1919 | id1<>id2 → |
---|
| 1920 | find_symbol ? (globalenv p) id1 = Some ? b1 → |
---|
| 1921 | find_symbol ? (globalenv p) id2 = Some ? b2 → |
---|
| 1922 | b1<>b2. |
---|
| 1923 | Proof. |
---|
| 1924 | intros. |
---|
| 1925 | assert (forall fns, |
---|
| 1926 | find_symbol ? (add_functs empty fns) id1 = Some ? b1 → |
---|
| 1927 | find_symbol ? (add_functs empty fns) id2 = Some ? b2 → |
---|
| 1928 | b1 <> b2). |
---|
| 1929 | unfold find_symbol. induction fns; simpl; intros. |
---|
| 1930 | rewrite PTree.gempty in H2. discriminate. |
---|
| 1931 | destruct a as [id f]; simpl in *. |
---|
| 1932 | rewrite PTree.gsspec in H2. |
---|
| 1933 | destruct (peq id1 id). subst id. inv H2. |
---|
| 1934 | rewrite PTree.gso in H3; auto. |
---|
| 1935 | generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega. |
---|
| 1936 | rewrite PTree.gsspec in H3. |
---|
| 1937 | destruct (peq id2 id). subst id. inv H3. |
---|
| 1938 | generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega. |
---|
| 1939 | eauto. |
---|
| 1940 | set (ge0 := add_functs empty p.(prog_funct)). |
---|
| 1941 | assert (forall (vars: list (ident * list init_data * V)) ge m, |
---|
| 1942 | add_globals (ge0, Mem.empty) vars = (ge, m) → |
---|
| 1943 | find_symbol ? ge id1 = Some ? b1 → |
---|
| 1944 | find_symbol ? ge id2 = Some ? b2 → |
---|
| 1945 | b1 <> b2). |
---|
| 1946 | unfold find_symbol. induction vars; simpl. |
---|
| 1947 | intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto. |
---|
| 1948 | intros ge m. destruct a as [[id init] info]. |
---|
| 1949 | caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B. |
---|
| 1950 | unfold add_symbol. simpl. intros. |
---|
| 1951 | rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3. |
---|
| 1952 | rewrite PTree.gso in H4; auto. |
---|
| 1953 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega. |
---|
| 1954 | rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4. |
---|
| 1955 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega. |
---|
| 1956 | eauto. |
---|
| 1957 | set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)). |
---|
| 1958 | apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m). |
---|
| 1959 | fold ge_m. apply surjective_pairing. auto. auto. |
---|
| 1960 | Qed. |
---|
| 1961 | |
---|
| 1962 | End GENV. |
---|
| 1963 | |
---|
| 1964 | (* Global environments and program transformations. *) |
---|
| 1965 | |
---|
| 1966 | Section MATCH_PROGRAM. |
---|
| 1967 | |
---|
| 1968 | Variable A B V W: Type. |
---|
| 1969 | Variable match_fun: A → B → Prop. |
---|
| 1970 | Variable match_var: V → W → Prop. |
---|
| 1971 | Variable p: program A V. |
---|
| 1972 | Variable p': program B W. |
---|
| 1973 | Hypothesis match_prog: |
---|
| 1974 | match_program match_fun match_var p p'. |
---|
| 1975 | |
---|
| 1976 | Lemma add_functs_match: |
---|
| 1977 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
[487] | 1978 | list_forall2 (match_funct_etry match_fun) fns tfns → |
---|
[3] | 1979 | let r := add_functs (empty A) fns in |
---|
| 1980 | let tr := add_functs (empty B) tfns in |
---|
| 1981 | nextfunction tr = nextfunction r /\ |
---|
| 1982 | symbols tr = symbols r /\ |
---|
| 1983 | forall (b: block) (f: A), |
---|
| 1984 | ZMap.get b (functions r) = Some ? f → |
---|
| 1985 | ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf. |
---|
| 1986 | Proof. |
---|
| 1987 | induction 1; simpl. |
---|
| 1988 | |
---|
| 1989 | split. reflexivity. split. reflexivity. |
---|
| 1990 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
| 1991 | |
---|
| 1992 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
| 1993 | simpl. red in H. destruct H. |
---|
| 1994 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
| 1995 | rewrite X. rewrite Y. |
---|
| 1996 | split. auto. |
---|
| 1997 | split. congruence. |
---|
| 1998 | intros b f. |
---|
| 1999 | repeat (rewrite ZMap.gsspec). |
---|
| 2000 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
| 2001 | intro EQ; inv EQ. exists fn2; auto. |
---|
| 2002 | auto. |
---|
| 2003 | Qed. |
---|
| 2004 | |
---|
| 2005 | Lemma add_functs_rev_match: |
---|
| 2006 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
[487] | 2007 | list_forall2 (match_funct_etry match_fun) fns tfns → |
---|
[3] | 2008 | let r := add_functs (empty A) fns in |
---|
| 2009 | let tr := add_functs (empty B) tfns in |
---|
| 2010 | nextfunction tr = nextfunction r /\ |
---|
| 2011 | symbols tr = symbols r /\ |
---|
| 2012 | forall (b: block) (tf: B), |
---|
| 2013 | ZMap.get b (functions tr) = Some ? tf → |
---|
| 2014 | ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf. |
---|
| 2015 | Proof. |
---|
| 2016 | induction 1; simpl. |
---|
| 2017 | |
---|
| 2018 | split. reflexivity. split. reflexivity. |
---|
| 2019 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
| 2020 | |
---|
| 2021 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
| 2022 | simpl. red in H. destruct H. |
---|
| 2023 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
| 2024 | rewrite X. rewrite Y. |
---|
| 2025 | split. auto. |
---|
| 2026 | split. congruence. |
---|
| 2027 | intros b f. |
---|
| 2028 | repeat (rewrite ZMap.gsspec). |
---|
| 2029 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
| 2030 | intro EQ; inv EQ. exists fn1; auto. |
---|
| 2031 | auto. |
---|
| 2032 | Qed. |
---|
| 2033 | |
---|
| 2034 | Lemma mem_add_globals_match: |
---|
| 2035 | forall (g1: genv A) (g2: genv B) (m: mem) |
---|
| 2036 | (vars: list (ident * list init_data * V)) |
---|
| 2037 | (tvars: list (ident * list init_data * W)), |
---|
[487] | 2038 | list_forall2 (match_var_etry match_var) vars tvars → |
---|
[3] | 2039 | snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). |
---|
| 2040 | Proof. |
---|
| 2041 | induction 1; simpl. |
---|
| 2042 | auto. |
---|
| 2043 | destruct a1 as [[id1 init1] info1]. |
---|
| 2044 | destruct b1 as [[id2 init2] info2]. |
---|
| 2045 | red in H. destruct H as [X [Y Z]]. subst id2 init2. |
---|
| 2046 | generalize IHlist_forall2. |
---|
| 2047 | destruct (add_globals (g1, m) al). |
---|
| 2048 | destruct (add_globals (g2, m) bl). |
---|
| 2049 | simpl. intro. subst m1. auto. |
---|
| 2050 | Qed. |
---|
| 2051 | |
---|
| 2052 | Lemma symbols_add_globals_match: |
---|
| 2053 | forall (g1: genv A) (g2: genv B) (m: mem), |
---|
| 2054 | symbols g1 = symbols g2 → |
---|
| 2055 | forall (vars: list (ident * list init_data * V)) |
---|
| 2056 | (tvars: list (ident * list init_data * W)), |
---|
[487] | 2057 | list_forall2 (match_var_etry match_var) vars tvars → |
---|
[3] | 2058 | symbols (fst (add_globals (g1, m) vars)) = |
---|
| 2059 | symbols (fst (add_globals (g2, m) tvars)). |
---|
| 2060 | Proof. |
---|
| 2061 | induction 2; simpl. |
---|
| 2062 | auto. |
---|
| 2063 | destruct a1 as [[id1 init1] info1]. |
---|
| 2064 | destruct b1 as [[id2 init2] info2]. |
---|
| 2065 | red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. |
---|
| 2066 | generalize IHlist_forall2. |
---|
| 2067 | generalize (mem_add_globals_match g1 g2 m H1). |
---|
| 2068 | destruct (add_globals (g1, m) al). |
---|
| 2069 | destruct (add_globals (g2, m) bl). |
---|
| 2070 | simpl. intros. congruence. |
---|
| 2071 | Qed. |
---|
| 2072 | |
---|
| 2073 | Theorem find_funct_ptr_match: |
---|
| 2074 | forall (b: block) (f: A), |
---|
| 2075 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 2076 | ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf. |
---|
| 2077 | Proof. |
---|
| 2078 | intros until f. destruct match_prog as [X [Y Z]]. |
---|
| 2079 | destruct (add_functs_match X) as [P [Q R]]. |
---|
| 2080 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
| 2081 | auto. |
---|
| 2082 | Qed. |
---|
| 2083 | |
---|
| 2084 | Theorem find_funct_ptr_rev_match: |
---|
| 2085 | forall (b: block) (tf: B), |
---|
| 2086 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 2087 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf. |
---|
| 2088 | Proof. |
---|
| 2089 | intros until tf. destruct match_prog as [X [Y Z]]. |
---|
| 2090 | destruct (add_functs_rev_match X) as [P [Q R]]. |
---|
| 2091 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
| 2092 | auto. |
---|
| 2093 | Qed. |
---|
| 2094 | |
---|
| 2095 | Theorem find_funct_match: |
---|
| 2096 | forall (v: val) (f: A), |
---|
| 2097 | find_funct (globalenv p) v = Some ? f → |
---|
| 2098 | ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf. |
---|
| 2099 | Proof. |
---|
| 2100 | intros until f. unfold find_funct. |
---|
| 2101 | case v; try (intros; discriminate). |
---|
| 2102 | intros b ofs. |
---|
| 2103 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
| 2104 | apply find_funct_ptr_match. |
---|
| 2105 | Qed. |
---|
| 2106 | |
---|
| 2107 | Theorem find_funct_rev_match: |
---|
| 2108 | forall (v: val) (tf: B), |
---|
| 2109 | find_funct (globalenv p') v = Some ? tf → |
---|
| 2110 | ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf. |
---|
| 2111 | Proof. |
---|
| 2112 | intros until tf. unfold find_funct. |
---|
| 2113 | case v; try (intros; discriminate). |
---|
| 2114 | intros b ofs. |
---|
| 2115 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
| 2116 | apply find_funct_ptr_rev_match. |
---|
| 2117 | Qed. |
---|
| 2118 | |
---|
| 2119 | Lemma symbols_init_match: |
---|
| 2120 | symbols (globalenv p') = symbols (globalenv p). |
---|
| 2121 | Proof. |
---|
| 2122 | unfold globalenv. unfold globalenv_initmem. |
---|
| 2123 | destruct match_prog as [X [Y Z]]. |
---|
| 2124 | destruct (add_functs_match X) as [P [Q R]]. |
---|
| 2125 | simpl. symmetry. apply symbols_add_globals_match. auto. auto. |
---|
| 2126 | Qed. |
---|
| 2127 | |
---|
| 2128 | Theorem find_symbol_match: |
---|
| 2129 | forall (s: ident), |
---|
| 2130 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 2131 | Proof. |
---|
| 2132 | intros. unfold find_symbol. |
---|
| 2133 | rewrite symbols_init_match. auto. |
---|
| 2134 | Qed. |
---|
| 2135 | |
---|
| 2136 | Theorem init_mem_match: |
---|
| 2137 | init_mem p' = init_mem p. |
---|
| 2138 | Proof. |
---|
| 2139 | unfold init_mem. unfold globalenv_initmem. |
---|
| 2140 | destruct match_prog as [X [Y Z]]. |
---|
| 2141 | symmetry. apply mem_add_globals_match. auto. |
---|
| 2142 | Qed. |
---|
| 2143 | |
---|
| 2144 | End MATCH_PROGRAM. |
---|
| 2145 | |
---|
| 2146 | Section TRANSF_PROGRAM_PARTIAL2. |
---|
| 2147 | |
---|
| 2148 | Variable A B V W: Type. |
---|
| 2149 | Variable transf_fun: A → res B. |
---|
| 2150 | Variable transf_var: V → res W. |
---|
| 2151 | Variable p: program A V. |
---|
| 2152 | Variable p': program B W. |
---|
| 2153 | Hypothesis transf_OK: |
---|
| 2154 | transform_partial_program2 transf_fun transf_var p = OK ? p'. |
---|
| 2155 | |
---|
| 2156 | Remark prog_match: |
---|
| 2157 | match_program |
---|
| 2158 | (fun fd tfd => transf_fun fd = OK ? tfd) |
---|
| 2159 | (fun info tinfo => transf_var info = OK ? tinfo) |
---|
| 2160 | p p'. |
---|
| 2161 | Proof. |
---|
| 2162 | apply transform_partial_program2_match; auto. |
---|
| 2163 | Qed. |
---|
| 2164 | |
---|
| 2165 | Theorem find_funct_ptr_transf_partial2: |
---|
| 2166 | forall (b: block) (f: A), |
---|
| 2167 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 2168 | ∃f'. |
---|
| 2169 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'. |
---|
| 2170 | Proof. |
---|
| 2171 | intros. |
---|
| 2172 | exploit find_funct_ptr_match. eexact prog_match. eauto. |
---|
| 2173 | intros [tf [X Y]]. exists tf; auto. |
---|
| 2174 | Qed. |
---|
| 2175 | |
---|
| 2176 | Theorem find_funct_ptr_rev_transf_partial2: |
---|
| 2177 | forall (b: block) (tf: B), |
---|
| 2178 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 2179 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf. |
---|
| 2180 | Proof. |
---|
| 2181 | intros. |
---|
| 2182 | exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. |
---|
| 2183 | Qed. |
---|
| 2184 | |
---|
| 2185 | Theorem find_funct_transf_partial2: |
---|
| 2186 | forall (v: val) (f: A), |
---|
| 2187 | find_funct (globalenv p) v = Some ? f → |
---|
| 2188 | ∃f'. |
---|
| 2189 | find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'. |
---|
| 2190 | Proof. |
---|
| 2191 | intros. |
---|
| 2192 | exploit find_funct_match. eexact prog_match. eauto. |
---|
| 2193 | intros [tf [X Y]]. exists tf; auto. |
---|
| 2194 | Qed. |
---|
| 2195 | |
---|
| 2196 | Theorem find_funct_rev_transf_partial2: |
---|
| 2197 | forall (v: val) (tf: B), |
---|
| 2198 | find_funct (globalenv p') v = Some ? tf → |
---|
| 2199 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf. |
---|
| 2200 | Proof. |
---|
| 2201 | intros. |
---|
| 2202 | exploit find_funct_rev_match. eexact prog_match. eauto. auto. |
---|
| 2203 | Qed. |
---|
| 2204 | |
---|
| 2205 | Theorem find_symbol_transf_partial2: |
---|
| 2206 | forall (s: ident), |
---|
| 2207 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 2208 | Proof. |
---|
| 2209 | intros. eapply find_symbol_match. eexact prog_match. |
---|
| 2210 | Qed. |
---|
| 2211 | |
---|
| 2212 | Theorem init_mem_transf_partial2: |
---|
| 2213 | init_mem p' = init_mem p. |
---|
| 2214 | Proof. |
---|
| 2215 | intros. eapply init_mem_match. eexact prog_match. |
---|
| 2216 | Qed. |
---|
| 2217 | |
---|
| 2218 | End TRANSF_PROGRAM_PARTIAL2. |
---|
| 2219 | |
---|
| 2220 | Section TRANSF_PROGRAM_PARTIAL. |
---|
| 2221 | |
---|
| 2222 | Variable A B V: Type. |
---|
| 2223 | Variable transf: A → res B. |
---|
| 2224 | Variable p: program A V. |
---|
| 2225 | Variable p': program B V. |
---|
| 2226 | Hypothesis transf_OK: transform_partial_program transf p = OK ? p'. |
---|
| 2227 | |
---|
| 2228 | Remark transf2_OK: |
---|
| 2229 | transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'. |
---|
| 2230 | Proof. |
---|
| 2231 | rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. |
---|
| 2232 | destruct (map_partial prefix_funct_name transf (prog_funct p)); auto. |
---|
| 2233 | rewrite map_partial_identity; auto. |
---|
| 2234 | Qed. |
---|
| 2235 | |
---|
| 2236 | Theorem find_funct_ptr_transf_partial: |
---|
| 2237 | forall (b: block) (f: A), |
---|
| 2238 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 2239 | ∃f'. |
---|
| 2240 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'. |
---|
| 2241 | Proof. |
---|
| 2242 | exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 2243 | Qed. |
---|
| 2244 | |
---|
| 2245 | Theorem find_funct_ptr_rev_transf_partial: |
---|
| 2246 | forall (b: block) (tf: B), |
---|
| 2247 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 2248 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf. |
---|
| 2249 | Proof. |
---|
| 2250 | exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 2251 | Qed. |
---|
| 2252 | |
---|
| 2253 | Theorem find_funct_transf_partial: |
---|
| 2254 | forall (v: val) (f: A), |
---|
| 2255 | find_funct (globalenv p) v = Some ? f → |
---|
| 2256 | ∃f'. |
---|
| 2257 | find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'. |
---|
| 2258 | Proof. |
---|
| 2259 | exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 2260 | Qed. |
---|
| 2261 | |
---|
| 2262 | Theorem find_funct_rev_transf_partial: |
---|
| 2263 | forall (v: val) (tf: B), |
---|
| 2264 | find_funct (globalenv p') v = Some ? tf → |
---|
| 2265 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf. |
---|
| 2266 | Proof. |
---|
| 2267 | exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 2268 | Qed. |
---|
| 2269 | |
---|
| 2270 | Theorem find_symbol_transf_partial: |
---|
| 2271 | forall (s: ident), |
---|
| 2272 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 2273 | Proof. |
---|
| 2274 | exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 2275 | Qed. |
---|
| 2276 | |
---|
| 2277 | Theorem init_mem_transf_partial: |
---|
| 2278 | init_mem p' = init_mem p. |
---|
| 2279 | Proof. |
---|
| 2280 | exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 2281 | Qed. |
---|
| 2282 | |
---|
| 2283 | End TRANSF_PROGRAM_PARTIAL. |
---|
| 2284 | |
---|
| 2285 | Section TRANSF_PROGRAM. |
---|
| 2286 | |
---|
| 2287 | Variable A B V: Type. |
---|
| 2288 | Variable transf: A → B. |
---|
| 2289 | Variable p: program A V. |
---|
| 2290 | Let tp := transform_program transf p. |
---|
| 2291 | |
---|
| 2292 | Remark transf_OK: |
---|
| 2293 | transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp. |
---|
| 2294 | Proof. |
---|
| 2295 | unfold tp, transform_program, transform_partial_program. |
---|
| 2296 | rewrite map_partial_total. reflexivity. |
---|
| 2297 | Qed. |
---|
| 2298 | |
---|
| 2299 | Theorem find_funct_ptr_transf: |
---|
| 2300 | forall (b: block) (f: A), |
---|
| 2301 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 2302 | find_funct_ptr ? (globalenv tp) b = Some ? (transf f). |
---|
| 2303 | Proof. |
---|
| 2304 | intros. |
---|
| 2305 | destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
| 2306 | as [f' [X Y]]. congruence. |
---|
| 2307 | Qed. |
---|
| 2308 | |
---|
| 2309 | Theorem find_funct_ptr_rev_transf: |
---|
| 2310 | forall (b: block) (tf: B), |
---|
| 2311 | find_funct_ptr ? (globalenv tp) b = Some ? tf → |
---|
| 2312 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf. |
---|
| 2313 | Proof. |
---|
| 2314 | intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto. |
---|
| 2315 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
| 2316 | Qed. |
---|
| 2317 | |
---|
| 2318 | Theorem find_funct_transf: |
---|
| 2319 | forall (v: val) (f: A), |
---|
| 2320 | find_funct (globalenv p) v = Some ? f → |
---|
| 2321 | find_funct (globalenv tp) v = Some ? (transf f). |
---|
| 2322 | Proof. |
---|
| 2323 | intros. |
---|
| 2324 | destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
| 2325 | as [f' [X Y]]. congruence. |
---|
| 2326 | Qed. |
---|
| 2327 | |
---|
| 2328 | Theorem find_funct_rev_transf: |
---|
| 2329 | forall (v: val) (tf: B), |
---|
| 2330 | find_funct (globalenv tp) v = Some ? tf → |
---|
| 2331 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf. |
---|
| 2332 | Proof. |
---|
| 2333 | intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto. |
---|
| 2334 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
| 2335 | Qed. |
---|
| 2336 | |
---|
| 2337 | Theorem find_symbol_transf: |
---|
| 2338 | forall (s: ident), |
---|
| 2339 | find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s. |
---|
| 2340 | Proof. |
---|
| 2341 | exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). |
---|
| 2342 | Qed. |
---|
| 2343 | |
---|
| 2344 | Theorem init_mem_transf: |
---|
| 2345 | init_mem tp = init_mem p. |
---|
| 2346 | Proof. |
---|
| 2347 | exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK). |
---|
| 2348 | Qed. |
---|
| 2349 | |
---|
| 2350 | End TRANSF_PROGRAM. |
---|
| 2351 | |
---|
| 2352 | End Genv. |
---|
| 2353 | *) |
---|
[485] | 2354 | |
---|