[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 | |
---|
| 36 | include "Errors.ma". |
---|
| 37 | include "AST.ma". |
---|
| 38 | include "Values.ma". |
---|
| 39 | include "Mem.ma". |
---|
| 40 | |
---|
| 41 | (* FIXME: unimplemented stuff in AST.ma |
---|
| 42 | naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V). |
---|
| 43 | naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W). |
---|
| 44 | naxiom match_program: ∀A,B,V,W:Type. program A V → program B W → Prop. |
---|
| 45 | *) |
---|
| 46 | |
---|
[24] | 47 | nrecord GENV : Type[2] ≝ { |
---|
[3] | 48 | (* * ** Types and operations *) |
---|
| 49 | |
---|
| 50 | genv_t : Type → Type; |
---|
| 51 | (* * The type of global environments. The parameter [F] is the type |
---|
| 52 | of function descriptions. *) |
---|
| 53 | |
---|
| 54 | globalenv: ∀F,V: Type. program F V → genv_t F; |
---|
| 55 | (* * Return the global environment for the given program. *) |
---|
| 56 | |
---|
| 57 | init_mem: ∀F,V: Type. program F V → mem; |
---|
| 58 | (* * Return the initial memory state for the given program. *) |
---|
| 59 | |
---|
| 60 | find_funct_ptr: ∀F: Type. genv_t F → block → option F; |
---|
| 61 | (* * Return the function description associated with the given address, |
---|
| 62 | if any. *) |
---|
| 63 | |
---|
| 64 | find_funct: ∀F: Type. genv_t F → val → option F; |
---|
| 65 | (* * Same as [find_funct_ptr] but the function address is given as |
---|
| 66 | a value, which must be a pointer with offset 0. *) |
---|
| 67 | |
---|
[125] | 68 | find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*; |
---|
[3] | 69 | (* * Return the address of the given global symbol, if any. *) |
---|
[24] | 70 | |
---|
[3] | 71 | (* * ** Properties of the operations. *) |
---|
[125] | 72 | |
---|
[3] | 73 | find_funct_inv: |
---|
| 74 | ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F. |
---|
| 75 | find_funct ? ge v = Some ? f → ∃b. v = Vptr b zero; |
---|
| 76 | find_funct_find_funct_ptr: |
---|
| 77 | ∀F: Type. ∀ge: t F. ∀b: block. |
---|
| 78 | find_funct ? ge (Vptr b zero) = find_funct_ptr ? ge b; |
---|
| 79 | |
---|
| 80 | find_symbol_exists: |
---|
| 81 | ∀F,V: Type. ∀p: program F V. |
---|
| 82 | ∀id: ident. ∀init: list init_data. ∀v: V. |
---|
| 83 | in_list ? 〈〈id, init〉, v〉 (prog_vars ?? p) → |
---|
| 84 | ∃b. find_symbol ? (globalenv ?? p) id = Some ? b; |
---|
| 85 | find_funct_ptr_exists: |
---|
| 86 | ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀f: F. |
---|
| 87 | list_norepet ? (prog_funct_names ?? p) → |
---|
| 88 | list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) → |
---|
| 89 | in_list ? 〈id, f〉 (prog_funct ?? p) → |
---|
| 90 | ∃b. find_symbol ? (globalenv ?? p) id = Some ? b |
---|
| 91 | ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f; |
---|
| 92 | |
---|
| 93 | find_funct_ptr_inversion: |
---|
| 94 | ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
| 95 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 96 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 97 | find_funct_inversion: |
---|
| 98 | ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
| 99 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 100 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 101 | find_funct_ptr_symbol_inversion: |
---|
| 102 | ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block. ∀f: F. |
---|
| 103 | find_symbol ? (globalenv ?? p) id = Some ? b → |
---|
| 104 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 105 | in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 106 | |
---|
| 107 | find_funct_ptr_prop: |
---|
| 108 | ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
| 109 | (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → |
---|
| 110 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 111 | P f; |
---|
| 112 | find_funct_prop: |
---|
| 113 | ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
| 114 | (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → |
---|
| 115 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 116 | P f; |
---|
| 117 | |
---|
| 118 | initmem_nullptr: |
---|
| 119 | ∀F,V: Type. ∀p: program F V. |
---|
| 120 | let m ≝ init_mem ?? p in |
---|
| 121 | valid_block m nullptr ∧ |
---|
| 122 | (blocks m) nullptr = empty_block 0 0; |
---|
| 123 | initmem_inject_neutral: |
---|
| 124 | ∀F,V: Type. ∀p: program F V. |
---|
| 125 | mem_inject_neutral (init_mem ?? p); |
---|
| 126 | find_funct_ptr_negative: |
---|
| 127 | ∀F,V: Type. ∀p: program F V. ∀b: block. ∀f: F. |
---|
| 128 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0; |
---|
| 129 | find_symbol_not_fresh: |
---|
| 130 | ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block. |
---|
| 131 | find_symbol ? (globalenv ?? p) id = Some ? b → b < nextblock (init_mem ?? p); |
---|
| 132 | find_symbol_not_nullptr: |
---|
| 133 | ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block. |
---|
| 134 | find_symbol ? (globalenv ?? p) id = Some ? b → b ≠ nullptr; |
---|
| 135 | global_addresses_distinct: |
---|
| 136 | ∀F,V: Type. ∀p: program F V. ∀id1,id2,b1,b2. |
---|
| 137 | id1≠id2 → |
---|
| 138 | find_symbol ? (globalenv ?? p) id1 = Some ? b1 → |
---|
| 139 | find_symbol ? (globalenv ?? p) id2 = Some ? b2 → |
---|
| 140 | b1≠b2(*; |
---|
| 141 | |
---|
| 142 | (* * Commutation properties between program transformations |
---|
| 143 | and operations over global environments. *) |
---|
[125] | 144 | *) |
---|
[3] | 145 | find_funct_ptr_transf: |
---|
| 146 | ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. |
---|
| 147 | ∀b: block. ∀f: A. |
---|
| 148 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 149 | find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f); |
---|
| 150 | find_funct_transf: |
---|
| 151 | ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. |
---|
| 152 | ∀v: val. ∀f: A. |
---|
| 153 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 154 | find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f); |
---|
| 155 | find_symbol_transf: |
---|
| 156 | ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. |
---|
| 157 | ∀s: ident. |
---|
| 158 | find_symbol ? (globalenv ?? (transform_program … transf p)) s = |
---|
| 159 | find_symbol ? (globalenv ?? p) s; |
---|
| 160 | init_mem_transf: |
---|
| 161 | ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. |
---|
| 162 | init_mem ?? (transform_program … transf p) = init_mem ?? p; |
---|
| 163 | find_funct_ptr_rev_transf: |
---|
| 164 | ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. |
---|
| 165 | ∀b : block. ∀tf : B. |
---|
| 166 | find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf → |
---|
| 167 | ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf; |
---|
| 168 | find_funct_rev_transf: |
---|
| 169 | ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. |
---|
| 170 | ∀v : val. ∀tf : B. |
---|
| 171 | find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → |
---|
[24] | 172 | ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf |
---|
[125] | 173 | |
---|
[3] | 174 | (* * Commutation properties between partial program transformations |
---|
| 175 | and operations over global environments. *) |
---|
| 176 | |
---|
| 177 | find_funct_ptr_transf_partial: |
---|
| 178 | ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
| 179 | transform_partial_program … transf p = OK ? p' → |
---|
| 180 | ∀b: block. ∀f: A. |
---|
| 181 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 182 | ∃f'. |
---|
| 183 | find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f'; |
---|
| 184 | find_funct_transf_partial: |
---|
| 185 | ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
| 186 | transform_partial_program … transf p = OK ? p' → |
---|
| 187 | ∀v: val. ∀f: A. |
---|
| 188 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 189 | ∃f'. |
---|
| 190 | find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f'; |
---|
| 191 | find_symbol_transf_partial: |
---|
| 192 | ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
| 193 | transform_partial_program … transf p = OK ? p' → |
---|
| 194 | ∀s: ident. |
---|
| 195 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
| 196 | init_mem_transf_partial: |
---|
| 197 | ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
| 198 | transform_partial_program … transf p = OK ? p' → |
---|
| 199 | init_mem ?? p' = init_mem ?? p; |
---|
| 200 | find_funct_ptr_rev_transf_partial: |
---|
| 201 | ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
| 202 | transform_partial_program … transf p = OK ? p' → |
---|
| 203 | ∀b : block. ∀tf : B. |
---|
| 204 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
| 205 | ∃f : A. |
---|
| 206 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf; |
---|
| 207 | find_funct_rev_transf_partial: |
---|
| 208 | ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
| 209 | transform_partial_program … transf p = OK ? p' → |
---|
| 210 | ∀v : val. ∀tf : B. |
---|
| 211 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 212 | ∃f : A. |
---|
| 213 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf; |
---|
| 214 | |
---|
| 215 | find_funct_ptr_transf_partial2: |
---|
| 216 | ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
| 217 | ∀p: program A V. ∀p': program B W. |
---|
| 218 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 219 | ∀b: block. ∀f: A. |
---|
| 220 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 221 | ∃f'. |
---|
| 222 | find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f'; |
---|
| 223 | find_funct_transf_partial2: |
---|
| 224 | ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
| 225 | ∀p: program A V. ∀p': program B W. |
---|
| 226 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 227 | ∀v: val. ∀f: A. |
---|
| 228 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 229 | ∃f'. |
---|
| 230 | find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f'; |
---|
| 231 | find_symbol_transf_partial2: |
---|
| 232 | ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
| 233 | ∀p: program A V. ∀p': program B W. |
---|
| 234 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 235 | ∀s: ident. |
---|
| 236 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
| 237 | init_mem_transf_partial2: |
---|
| 238 | ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
| 239 | ∀p: program A V. ∀p': program B W. |
---|
| 240 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 241 | init_mem ?? p' = init_mem ?? p; |
---|
| 242 | find_funct_ptr_rev_transf_partial2: |
---|
| 243 | ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
| 244 | ∀p: program A V. ∀p': program B W. |
---|
| 245 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 246 | ∀b: block. ∀tf: B. |
---|
| 247 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
| 248 | ∃f : A. |
---|
| 249 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf; |
---|
| 250 | find_funct_rev_transf_partial2: |
---|
| 251 | ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
| 252 | ∀p: program A V. ∀p': program B W. |
---|
| 253 | transform_partial_program2 … transf_fun transf_var p = OK ? p' → |
---|
| 254 | ∀v: val. ∀tf: B. |
---|
| 255 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 256 | ∃f : A. |
---|
| 257 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf_fun f = OK ? tf}. ; |
---|
| 258 | |
---|
| 259 | (* * Commutation properties between matching between programs |
---|
| 260 | and operations over global environments. *) |
---|
| 261 | |
---|
| 262 | find_funct_ptr_match: |
---|
| 263 | ∀A,B,V,W: Type. ∀match_fun: A → B → Prop. |
---|
| 264 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 265 | match_program … match_fun match_var p p' → |
---|
| 266 | ∀b: block. ∀f: A. |
---|
| 267 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 268 | ∃tf : B. |
---|
| 269 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf; |
---|
| 270 | find_funct_ptr_rev_match: |
---|
| 271 | ∀A,B,V,W: Type. ∀match_fun: A → B → Prop. |
---|
| 272 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 273 | match_program … match_fun match_var p p' → |
---|
| 274 | ∀b: block. ∀tf: B. |
---|
| 275 | find_funct_ptr ? (globalenv ?? p') b = Some ? tf → |
---|
| 276 | ∃f : A. |
---|
| 277 | find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf; |
---|
| 278 | find_funct_match: |
---|
| 279 | ∀A,B,V,W: Type. ∀match_fun: A → B → Prop. |
---|
| 280 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 281 | match_program … match_fun match_var p p' → |
---|
| 282 | ∀v: val. ∀f: A. |
---|
| 283 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 284 | ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf; |
---|
| 285 | find_funct_rev_match: |
---|
| 286 | ∀A,B,V,W: Type. ∀match_fun: A → B → Prop. |
---|
| 287 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 288 | match_program … match_fun match_var p p' → |
---|
| 289 | ∀v: val. ∀tf: B. |
---|
| 290 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 291 | ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf; |
---|
| 292 | find_symbol_match: |
---|
| 293 | ∀A,B,V,W: Type. ∀match_fun: A → B → Prop. |
---|
| 294 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 295 | match_program … match_fun match_var p p' → |
---|
| 296 | ∀s: ident. |
---|
| 297 | find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; |
---|
| 298 | init_mem_match: |
---|
| 299 | ∀A,B,V,W: Type. ∀match_fun: A → B → Prop. |
---|
| 300 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 301 | match_program … match_fun match_var p p' → |
---|
| 302 | init_mem ?? p' = init_mem ?? p*) |
---|
| 303 | }. |
---|
| 304 | |
---|
[24] | 305 | |
---|
| 306 | nlet rec foldl (A,B:Type) (f:A → B → A) (a:A) (l:list B) on l : A ≝ |
---|
| 307 | match l with |
---|
| 308 | [ nil ⇒ a |
---|
| 309 | | cons h t ⇒ foldl A B f (f a h) t |
---|
| 310 | ]. |
---|
| 311 | |
---|
[125] | 312 | (* Functions are given negative block numbers *) |
---|
| 313 | |
---|
[3] | 314 | (* XXX: temporary definition |
---|
| 315 | NB: only global functions, no global variables *) |
---|
| 316 | nrecord genv (F:Type) : Type ≝ { |
---|
| 317 | functions: block → option F; |
---|
| 318 | nextfunction: Z; |
---|
[125] | 319 | symbols: ident → option (memory_space × block) |
---|
[3] | 320 | }. |
---|
[125] | 321 | (* |
---|
| 322 | (** The rest of this library is a straightforward implementation of |
---|
| 323 | the module signature above. *) |
---|
[3] | 324 | |
---|
[125] | 325 | Module Genv: GENV. |
---|
| 326 | |
---|
| 327 | Section GENV. |
---|
| 328 | |
---|
| 329 | Variable F: Type. (* The type of functions *) |
---|
| 330 | Variable V: Type. (* The type of information over variables *) |
---|
| 331 | |
---|
| 332 | Record genv : Type := mkgenv { |
---|
| 333 | functions: ZMap.t (option F); (* mapping function ptr → function *) |
---|
| 334 | nextfunction: Z; |
---|
| 335 | symbols: PTree.t block (* mapping symbol → block *) |
---|
| 336 | }. |
---|
| 337 | |
---|
| 338 | Definition t := genv. |
---|
| 339 | *) |
---|
| 340 | |
---|
| 341 | ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝ |
---|
| 342 | λF,name_fun,g. |
---|
| 343 | let b ≝ nextfunction ? g in |
---|
| 344 | mk_genv F ((*ZMap.set*) λb'. if eqZb b b' then (Some ? (\snd name_fun)) else (functions ? g b')) |
---|
| 345 | (Zpred b) |
---|
| 346 | ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]). |
---|
| 347 | |
---|
| 348 | ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝ |
---|
| 349 | λF,name,bsp,b,g. |
---|
| 350 | mk_genv F (functions ? g) |
---|
| 351 | (nextfunction ? g) |
---|
| 352 | ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]). |
---|
| 353 | (* |
---|
| 354 | Definition find_funct_ptr ? (g: genv) (b: block) : option F := |
---|
| 355 | ZMap.get b g.(functions). |
---|
| 356 | |
---|
| 357 | Definition find_funct (g: genv) (v: val) : option F := |
---|
| 358 | match v with |
---|
| 359 | | Vptr b ofs => |
---|
| 360 | if Int.eq ofs Int.zero then find_funct_ptr ? g b else None |
---|
| 361 | | _ => |
---|
| 362 | None |
---|
| 363 | end. |
---|
| 364 | |
---|
| 365 | Definition find_symbol ? (g: genv) (symb: ident) : option block := |
---|
| 366 | PTree.get symb g.(symbols). |
---|
| 367 | |
---|
| 368 | Lemma find_funct_inv: |
---|
| 369 | forall (ge: t) (v: val) (f: F), |
---|
| 370 | find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero. |
---|
| 371 | Proof. |
---|
| 372 | intros until f. unfold find_funct. destruct v; try (intros; discriminate). |
---|
| 373 | generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros. |
---|
| 374 | exists b. congruence. |
---|
| 375 | discriminate. |
---|
| 376 | Qed. |
---|
| 377 | |
---|
| 378 | Lemma find_funct_find_funct_ptr: |
---|
| 379 | forall (ge: t) (b: block), |
---|
| 380 | find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. |
---|
| 381 | Proof. |
---|
| 382 | intros. simpl. |
---|
| 383 | generalize (Int.eq_spec Int.zero Int.zero). |
---|
| 384 | case (Int.eq Int.zero Int.zero); intros. |
---|
| 385 | auto. tauto. |
---|
| 386 | Qed. |
---|
| 387 | *) |
---|
| 388 | (* Construct environment and initial memory store *) |
---|
| 389 | ndefinition empty_mem ≝ empty. (* XXX*) |
---|
| 390 | ndefinition empty : ∀F. genv F ≝ |
---|
| 391 | λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?). |
---|
| 392 | (* mkgenv (ZMap.init None) (-1) (PTree.empty block).*) |
---|
| 393 | |
---|
| 394 | ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝ |
---|
| 395 | λF,init,fns. |
---|
| 396 | foldr ?? (add_funct F) init fns. |
---|
| 397 | |
---|
| 398 | ndefinition add_globals : ∀F,V:Type. |
---|
| 399 | genv F × mem → list (ident × (list init_data) × memory_space × V) → |
---|
| 400 | genv F × mem ≝ |
---|
| 401 | λF,V,init,vars. |
---|
| 402 | foldr ?? |
---|
| 403 | (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem. |
---|
| 404 | match id_init with [ mk_pair id_init1 info ⇒ |
---|
| 405 | match id_init1 with [ mk_pair id_init2 bsp ⇒ |
---|
| 406 | match id_init2 with [ mk_pair id init ⇒ |
---|
| 407 | match g_st with [ mk_pair g st ⇒ |
---|
| 408 | match alloc_init_data st init bsp with [ mk_pair st' b ⇒ |
---|
| 409 | 〈add_symbol ? id bsp b g, st'〉 |
---|
| 410 | ] ] ] ] ]) |
---|
| 411 | init vars. |
---|
| 412 | |
---|
| 413 | ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝ |
---|
| 414 | λF,V,p. |
---|
| 415 | add_globals F V |
---|
| 416 | 〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉 |
---|
| 417 | (prog_vars ?? p). |
---|
| 418 | |
---|
| 419 | ndefinition globalenv_ : ∀F,V:Type. program F V → genv F ≝ |
---|
| 420 | λF,V,p. |
---|
| 421 | \fst (globalenv_initmem F V p). |
---|
| 422 | ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝ |
---|
| 423 | λF,V,p. |
---|
| 424 | \snd (globalenv_initmem F V p). |
---|
| 425 | |
---|
[3] | 426 | ndefinition Genv : GENV ≝ mk_GENV |
---|
| 427 | genv (* genv_t *) |
---|
[125] | 428 | globalenv_ |
---|
| 429 | init_mem_ |
---|
[3] | 430 | (λF,ge. functions ? ge) (* find_funct_ptr *) |
---|
[124] | 431 | (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *) |
---|
[3] | 432 | (λF,ge. symbols ? ge) (* find_symbol *) |
---|
[125] | 433 | (* ? |
---|
[24] | 434 | ? |
---|
| 435 | ? |
---|
| 436 | ? |
---|
| 437 | ? |
---|
[125] | 438 | ?*) |
---|
[3] | 439 | . |
---|
[125] | 440 | (* |
---|
[24] | 441 | ##[ #A B C transf p b f; nelim p; #fns main vars; |
---|
| 442 | nelim fns; |
---|
[125] | 443 | ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct; |
---|
[24] | 444 | ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?); |
---|
| 445 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 446 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; |
---|
| 447 | nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 448 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 449 | ##[ ##2: nelim t; ##[ //; ##| #h t IH; nwhd in ⊢ (??%?); nrewrite > IH; |
---|
| 450 | nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 451 | ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??%?); |
---|
| 452 | ##[ #H; ndestruct (H); //; |
---|
| 453 | ##| #H; napply IH; napply H; |
---|
| 454 | ##] |
---|
| 455 | ##] |
---|
| 456 | ##] |
---|
| 457 | ##] |
---|
| 458 | ##| #A B C transf p v f; nelim v; |
---|
| 459 | ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct; |
---|
| 460 | ##| ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct; |
---|
[124] | 461 | ##| #pcl b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero); |
---|
[24] | 462 | nwhd in ⊢ (??%? → ??%?); |
---|
| 463 | ##[ nelim p; #fns main vars; nelim fns; |
---|
| 464 | ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct; |
---|
| 465 | ##| #h t; nelim h; #f fn IH; |
---|
| 466 | nwhd in ⊢ (??%? → ??%?); |
---|
| 467 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 468 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; |
---|
| 469 | nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 470 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 471 | ##[ ##2: nelim t; ##[ //; ##| #h t IH; nwhd in ⊢ (??%?); nrewrite > IH; |
---|
| 472 | nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 473 | ##| napply eqZb_elim; #e; nwhd in ⊢ (??%? → ??%?); #H; |
---|
| 474 | ##[ ndestruct (H); //; |
---|
| 475 | ##| napply IH; napply H; |
---|
| 476 | ##] |
---|
| 477 | ##] |
---|
| 478 | ##] |
---|
| 479 | ##] |
---|
| 480 | ##| #H; ndestruct; |
---|
| 481 | ##] |
---|
| 482 | ##] |
---|
| 483 | ##| #A B C transf p id; nelim p; #fns main vars; |
---|
| 484 | nelim fns; |
---|
| 485 | ##[ nnormalize; // |
---|
| 486 | ##| #h t; nelim h; #fid fd; nwhd in ⊢ (??%% → ??%%); #IH; |
---|
| 487 | nelim (ident_eq fid id); #e; |
---|
| 488 | ##[ nwhd in ⊢ (??%%); |
---|
| 489 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 490 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; |
---|
| 491 | nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 492 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 493 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 494 | nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 495 | ##| // |
---|
| 496 | ##] |
---|
| 497 | ##] |
---|
| 498 | ##| nwhd in ⊢ (??%%); nrewrite > IH; napply refl; |
---|
| 499 | ##] |
---|
| 500 | ##] |
---|
| 501 | ##| //; |
---|
| 502 | ##| #A B C transf p b tf; nelim p; #fns main vars; |
---|
| 503 | nelim fns; |
---|
| 504 | ##[ nnormalize; #H; ndestruct; |
---|
| 505 | ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 506 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 507 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; |
---|
| 508 | nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 509 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 510 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 511 | nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 512 | ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 513 | ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //; |
---|
| 514 | ##| #H; napply IH; napply H; |
---|
| 515 | ##] |
---|
| 516 | ##] |
---|
| 517 | ##] |
---|
| 518 | ##] |
---|
| 519 | ##| #A B C transf p v tf; nelim p; #fns main vars; nelim v; |
---|
| 520 | ##[ nnormalize; #H; ndestruct; |
---|
| 521 | ##| ##2,3: #x; nnormalize; #H; ndestruct; |
---|
[124] | 522 | ##| #pcl b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero); |
---|
[24] | 523 | ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 524 | nelim fns; |
---|
| 525 | ##[ nnormalize; #H; ndestruct; |
---|
| 526 | ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 527 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 528 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; |
---|
| 529 | nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 530 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
| 531 | ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 532 | nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 533 | ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 534 | ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //; |
---|
| 535 | ##| #H; napply IH; napply H; |
---|
| 536 | ##] |
---|
| 537 | ##] |
---|
| 538 | ##] |
---|
| 539 | ##] |
---|
| 540 | ##| nnormalize; #H; ndestruct; |
---|
| 541 | ##] |
---|
| 542 | ##] |
---|
| 543 | ##] nqed. |
---|
| 544 | |
---|
[3] | 545 | |
---|
| 546 | Lemma functions_globalenv: |
---|
| 547 | forall (p: program F V), |
---|
| 548 | functions (globalenv p) = functions (add_functs empty p.(prog_funct)). |
---|
| 549 | Proof. |
---|
| 550 | assert (forall init vars, |
---|
| 551 | functions (fst (add_globals init vars)) = functions (fst init)). |
---|
| 552 | induction vars; simpl. |
---|
| 553 | reflexivity. |
---|
| 554 | destruct a as [[id1 init1] info1]. destruct (add_globals init vars). |
---|
| 555 | simpl. exact IHvars. |
---|
| 556 | |
---|
| 557 | unfold add_globals; simpl. |
---|
| 558 | intros. unfold globalenv; unfold globalenv_initmem. |
---|
| 559 | rewrite H. reflexivity. |
---|
| 560 | Qed. |
---|
| 561 | |
---|
| 562 | Lemma initmem_nullptr: |
---|
| 563 | forall (p: program F V), |
---|
| 564 | let m := init_mem p in |
---|
| 565 | valid_block m nullptr /\ |
---|
| 566 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef). |
---|
| 567 | Proof. |
---|
| 568 | pose (P := fun m => valid_block m nullptr /\ |
---|
| 569 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)). |
---|
| 570 | assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))). |
---|
| 571 | induction vars; simpl; intros. |
---|
| 572 | auto. |
---|
| 573 | destruct a as [[id1 in1] inf1]. |
---|
| 574 | destruct (add_globals init vars) as [g st]. |
---|
| 575 | simpl in *. destruct IHvars. split. |
---|
| 576 | red; simpl. red in H0. omega. |
---|
| 577 | simpl. rewrite update_o. auto. unfold block. red in H0. omega. |
---|
| 578 | |
---|
| 579 | intro. unfold init_mem, globalenv_initmem. apply H. |
---|
| 580 | red; simpl. split. compute. auto. reflexivity. |
---|
| 581 | Qed. |
---|
| 582 | |
---|
| 583 | Lemma initmem_inject_neutral: |
---|
| 584 | forall (p: program F V), |
---|
| 585 | mem_inject_neutral (init_mem p). |
---|
| 586 | Proof. |
---|
| 587 | assert (forall g0 vars g1 m, |
---|
| 588 | add_globals (g0, Mem.empty) vars = (g1, m) → |
---|
| 589 | mem_inject_neutral m). |
---|
| 590 | Opaque alloc_init_data. |
---|
| 591 | induction vars; simpl. |
---|
| 592 | intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H). |
---|
| 593 | simpl in H1. rewrite Mem.getN_init in H1. |
---|
| 594 | replace v with Vundef. auto. destruct chunk; simpl in H1; auto. |
---|
| 595 | destruct a as [[id1 init1] info1]. |
---|
| 596 | caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. |
---|
| 597 | caseEq (alloc_init_data m1 init1). intros m2 b ALLOC. |
---|
| 598 | intros. inv H. |
---|
| 599 | eapply Mem.alloc_init_data_neutral; eauto. |
---|
| 600 | intros. caseEq (globalenv_initmem p). intros g m EQ. |
---|
| 601 | unfold init_mem; rewrite EQ; simpl. |
---|
| 602 | unfold globalenv_initmem in EQ. eauto. |
---|
| 603 | Qed. |
---|
| 604 | |
---|
| 605 | Remark nextfunction_add_functs_neg: |
---|
| 606 | forall fns, nextfunction (add_functs empty fns) < 0. |
---|
| 607 | Proof. |
---|
| 608 | induction fns; simpl; intros. omega. unfold Zpred. omega. |
---|
| 609 | Qed. |
---|
| 610 | |
---|
| 611 | Theorem find_funct_ptr_negative: |
---|
| 612 | forall (p: program F V) (b: block) (f: F), |
---|
| 613 | find_funct_ptr ? (globalenv p) b = Some ? f → b < 0. |
---|
| 614 | Proof. |
---|
| 615 | intros until f. |
---|
| 616 | assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0). |
---|
| 617 | induction fns; simpl. |
---|
| 618 | rewrite ZMap.gi. congruence. |
---|
| 619 | rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro. |
---|
| 620 | intro. rewrite e. apply nextfunction_add_functs_neg. |
---|
| 621 | auto. |
---|
| 622 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
| 623 | intros. eauto. |
---|
| 624 | Qed. |
---|
| 625 | |
---|
| 626 | Remark find_symbol_add_functs_negative: |
---|
| 627 | forall (fns: list (ident * F)) s b, |
---|
| 628 | (symbols (add_functs empty fns)) ! s = Some ? b → b < 0. |
---|
| 629 | Proof. |
---|
| 630 | induction fns; simpl; intros until b. |
---|
| 631 | rewrite PTree.gempty. congruence. |
---|
| 632 | rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro. |
---|
| 633 | intro EQ; inversion EQ. apply nextfunction_add_functs_neg. |
---|
| 634 | eauto. |
---|
| 635 | Qed. |
---|
| 636 | |
---|
| 637 | Remark find_symbol_add_symbols_not_fresh: |
---|
| 638 | forall fns vars g m s b, |
---|
| 639 | add_globals (add_functs empty fns, Mem.empty) vars = (g, m) → |
---|
| 640 | (symbols g)!s = Some ? b → |
---|
| 641 | b < nextblock m. |
---|
| 642 | Proof. |
---|
| 643 | induction vars; simpl; intros until b. |
---|
| 644 | intros. inversion H. subst g m. simpl. |
---|
| 645 | generalize (find_symbol_add_functs_negative fns s H0). omega. |
---|
| 646 | Transparent alloc_init_data. |
---|
| 647 | destruct a as [[id1 init1] info1]. |
---|
| 648 | caseEq (add_globals (add_functs empty fns, Mem.empty) vars). |
---|
| 649 | intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. |
---|
| 650 | unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro. |
---|
| 651 | intro EQ; inversion EQ. omega. |
---|
| 652 | intro. generalize (IHvars _ _ _ _ ADG H). omega. |
---|
| 653 | Qed. |
---|
| 654 | |
---|
| 655 | Theorem find_symbol_not_fresh: |
---|
| 656 | forall (p: program F V) (id: ident) (b: block), |
---|
| 657 | find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p). |
---|
| 658 | Proof. |
---|
| 659 | intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. |
---|
| 660 | caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty) |
---|
| 661 | (prog_vars p)); intros g m EQ. |
---|
| 662 | simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto. |
---|
| 663 | Qed. |
---|
| 664 | |
---|
| 665 | Lemma find_symbol_exists: |
---|
| 666 | forall (p: program F V) |
---|
| 667 | (id: ident) (init: list init_data) (v: V), |
---|
| 668 | In (id, init, v) (prog_vars p) → |
---|
| 669 | ∃b. find_symbol ? (globalenv p) id = Some ? b. |
---|
| 670 | Proof. |
---|
| 671 | intros until v. |
---|
| 672 | assert (forall initm vl, In (id, init, v) vl → |
---|
| 673 | ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b). |
---|
| 674 | induction vl; simpl; intros. |
---|
| 675 | elim H. |
---|
| 676 | destruct a as [[id0 init0] v0]. |
---|
| 677 | caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. |
---|
| 678 | rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto. |
---|
| 679 | elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. |
---|
| 680 | intros. unfold globalenv, find_symbol, globalenv_initmem. auto. |
---|
| 681 | Qed. |
---|
| 682 | |
---|
| 683 | Remark find_symbol_above_nextfunction: |
---|
| 684 | forall (id: ident) (b: block) (fns: list (ident * F)), |
---|
| 685 | let g := add_functs empty fns in |
---|
| 686 | PTree.get id g.(symbols) = Some ? b → |
---|
| 687 | b > g.(nextfunction). |
---|
| 688 | Proof. |
---|
| 689 | induction fns; simpl. |
---|
| 690 | rewrite PTree.gempty. congruence. |
---|
| 691 | rewrite PTree.gsspec. case (peq id (fst a)); intro. |
---|
| 692 | intro EQ. inversion EQ. unfold Zpred. omega. |
---|
| 693 | intros. generalize (IHfns H). unfold Zpred; omega. |
---|
| 694 | Qed. |
---|
| 695 | |
---|
| 696 | Remark find_symbol_add_globals: |
---|
| 697 | forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)), |
---|
| 698 | ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) → |
---|
| 699 | find_symbol ? (fst (add_globals ge_m vars)) id = |
---|
| 700 | find_symbol ? (fst ge_m) id. |
---|
| 701 | Proof. |
---|
| 702 | unfold find_symbol; induction vars; simpl; intros. |
---|
| 703 | auto. |
---|
| 704 | destruct a as [[id0 init0] var0]. simpl in *. |
---|
| 705 | caseEq (add_globals ge_m vars); intros ge' m' EQ. |
---|
| 706 | simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. |
---|
| 707 | apply IHvars. tauto. intuition congruence. |
---|
| 708 | Qed. |
---|
| 709 | |
---|
| 710 | Lemma find_funct_ptr_exists: |
---|
| 711 | forall (p: program F V) (id: ident) (f: F), |
---|
| 712 | list_norepet (prog_funct_names p) → |
---|
| 713 | list_disjoint (prog_funct_names p) (prog_var_names p) → |
---|
| 714 | In (id, f) (prog_funct p) → |
---|
| 715 | ∃b. find_symbol ? (globalenv p) id = Some ? b |
---|
| 716 | /\ find_funct_ptr ? (globalenv p) b = Some ? f. |
---|
| 717 | Proof. |
---|
| 718 | intros until f. |
---|
| 719 | assert (forall (fns: list (ident * F)), |
---|
| 720 | list_norepet (map (@fst ident F) fns) → |
---|
| 721 | In (id, f) fns → |
---|
| 722 | ∃b. find_symbol ? (add_functs empty fns) id = Some ? b |
---|
| 723 | /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f). |
---|
| 724 | unfold find_symbol, find_funct_ptr. induction fns; intros. |
---|
| 725 | elim H0. |
---|
| 726 | destruct a as [id0 f0]; simpl in *. inv H. |
---|
| 727 | unfold add_funct; simpl. |
---|
| 728 | rewrite PTree.gsspec. destruct (peq id id0). |
---|
| 729 | subst id0. econstructor; split. eauto. |
---|
| 730 | replace f0 with f. apply ZMap.gss. |
---|
| 731 | elim H0; intro. congruence. elim H3. |
---|
| 732 | change id with (@fst ident F (id, f)). apply List.in_map. auto. |
---|
| 733 | exploit IHfns; eauto. elim H0; intro. congruence. auto. |
---|
| 734 | intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto. |
---|
| 735 | generalize (find_symbol_above_nextfunction _ _ X). |
---|
| 736 | unfold block; unfold ZIndexed.t; intro; omega. |
---|
| 737 | |
---|
| 738 | intros. exploit H; eauto. intros [b [X Y]]. |
---|
| 739 | exists b; split. |
---|
| 740 | unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. |
---|
| 741 | assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. |
---|
| 742 | unfold prog_funct_names. change id with (fst (id, f)). |
---|
| 743 | apply List.in_map; auto. |
---|
| 744 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
| 745 | assumption. |
---|
| 746 | Qed. |
---|
| 747 | |
---|
| 748 | Lemma find_funct_ptr_inversion: |
---|
| 749 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
| 750 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 751 | ∃id. In (id, f) (prog_funct p). |
---|
| 752 | Proof. |
---|
| 753 | intros until f. |
---|
| 754 | assert (forall fns: list (ident * F), |
---|
| 755 | find_funct_ptr ? (add_functs empty fns) b = Some ? f → |
---|
| 756 | ∃id. In (id, f) fns). |
---|
| 757 | unfold find_funct_ptr. induction fns; simpl. |
---|
| 758 | rewrite ZMap.gi. congruence. |
---|
| 759 | destruct a as [id0 f0]; simpl. |
---|
| 760 | rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))). |
---|
| 761 | intro. inv H. exists id0; auto. |
---|
| 762 | intro. exploit IHfns; eauto. intros [id A]. exists id; auto. |
---|
| 763 | unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto. |
---|
| 764 | Qed. |
---|
| 765 | |
---|
| 766 | Lemma find_funct_ptr_prop: |
---|
| 767 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
| 768 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
| 769 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 770 | P f. |
---|
| 771 | Proof. |
---|
| 772 | intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto. |
---|
| 773 | Qed. |
---|
| 774 | |
---|
| 775 | Lemma find_funct_inversion: |
---|
| 776 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
| 777 | find_funct (globalenv p) v = Some ? f → |
---|
| 778 | ∃id. In (id, f) (prog_funct p). |
---|
| 779 | Proof. |
---|
| 780 | intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H. |
---|
| 781 | rewrite find_funct_find_funct_ptr ? in H. |
---|
| 782 | eapply find_funct_ptr_inversion; eauto. |
---|
| 783 | Qed. |
---|
| 784 | |
---|
| 785 | Lemma find_funct_prop: |
---|
| 786 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
| 787 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
| 788 | find_funct (globalenv p) v = Some ? f → |
---|
| 789 | P f. |
---|
| 790 | Proof. |
---|
| 791 | intros. exploit find_funct_inversion; eauto. intros [id A]. eauto. |
---|
| 792 | Qed. |
---|
| 793 | |
---|
| 794 | Lemma find_funct_ptr_symbol_inversion: |
---|
| 795 | forall (p: program F V) (id: ident) (b: block) (f: F), |
---|
| 796 | find_symbol ? (globalenv p) id = Some ? b → |
---|
| 797 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 798 | In (id, f) p.(prog_funct). |
---|
| 799 | Proof. |
---|
| 800 | intros until f. |
---|
| 801 | assert (forall fns, |
---|
| 802 | let g := add_functs empty fns in |
---|
| 803 | PTree.get id g.(symbols) = Some ? b → |
---|
| 804 | ZMap.get b g.(functions) = Some ? f → |
---|
| 805 | In (id, f) fns). |
---|
| 806 | induction fns; simpl. |
---|
| 807 | rewrite ZMap.gi. congruence. |
---|
| 808 | set (g := add_functs empty fns). |
---|
| 809 | rewrite PTree.gsspec. rewrite ZMap.gsspec. |
---|
| 810 | case (peq id (fst a)); intro. |
---|
| 811 | intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. |
---|
| 812 | intro EQ2. left. destruct a. simpl in *. congruence. |
---|
| 813 | intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto. |
---|
| 814 | generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega. |
---|
| 815 | assert (forall g0 m0, b < 0 → |
---|
| 816 | forall vars g m, |
---|
| 817 | add_globals (g0, m0) vars = (g, m) → |
---|
| 818 | PTree.get id g.(symbols) = Some ? b → |
---|
| 819 | PTree.get id g0.(symbols) = Some ? b). |
---|
| 820 | induction vars; simpl. |
---|
| 821 | intros. inv H1. auto. |
---|
| 822 | destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). |
---|
| 823 | intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1. |
---|
| 824 | unfold add_symbol; intros A B. rewrite <- B. simpl. |
---|
| 825 | rewrite PTree.gsspec. case (peq id id1); intros. |
---|
| 826 | assert (b > 0). inv H1. apply nextblock_pos. |
---|
| 827 | omegaContradiction. |
---|
| 828 | eauto. |
---|
| 829 | intros. |
---|
| 830 | generalize (find_funct_ptr_negative _ _ H2). intro. |
---|
| 831 | pose (g := add_functs empty (prog_funct p)). |
---|
| 832 | apply H. |
---|
| 833 | apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). |
---|
| 834 | auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. |
---|
| 835 | reflexivity. assumption. rewrite <- functions_globalenv. assumption. |
---|
| 836 | Qed. |
---|
| 837 | |
---|
| 838 | Theorem find_symbol_not_nullptr: |
---|
| 839 | forall (p: program F V) (id: ident) (b: block), |
---|
| 840 | find_symbol ? (globalenv p) id = Some ? b → b <> nullptr. |
---|
| 841 | Proof. |
---|
| 842 | intros until b. |
---|
| 843 | assert (forall fns, |
---|
| 844 | find_symbol ? (add_functs empty fns) id = Some ? b → |
---|
| 845 | b <> nullptr). |
---|
| 846 | unfold find_symbol; induction fns; simpl. |
---|
| 847 | rewrite PTree.gempty. congruence. |
---|
| 848 | destruct a as [id1 f1]. simpl. rewrite PTree.gsspec. |
---|
| 849 | destruct (peq id id1); intros. |
---|
| 850 | inversion H. generalize (nextfunction_add_functs_neg fns). |
---|
| 851 | unfold block, nullptr; omega. |
---|
| 852 | auto. |
---|
| 853 | set (g0 := add_functs empty p.(prog_funct)). |
---|
| 854 | assert (forall vars g m, |
---|
| 855 | add_globals (g0, Mem.empty) vars = (g, m) → |
---|
| 856 | find_symbol ? g id = Some ? b → |
---|
| 857 | b <> nullptr). |
---|
| 858 | induction vars; simpl; intros until m. |
---|
| 859 | intros. inversion H0. subst g. apply H with (prog_funct p). auto. |
---|
| 860 | destruct a as [[id1 init1] info1]. |
---|
| 861 | caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2. |
---|
| 862 | inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec. |
---|
| 863 | destruct (peq id id1); intros. |
---|
| 864 | inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega. |
---|
| 865 | eauto. |
---|
| 866 | intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto. |
---|
| 867 | Qed. |
---|
| 868 | |
---|
| 869 | Theorem global_addresses_distinct: |
---|
| 870 | forall (p: program F V) id1 id2 b1 b2, |
---|
| 871 | id1<>id2 → |
---|
| 872 | find_symbol ? (globalenv p) id1 = Some ? b1 → |
---|
| 873 | find_symbol ? (globalenv p) id2 = Some ? b2 → |
---|
| 874 | b1<>b2. |
---|
| 875 | Proof. |
---|
| 876 | intros. |
---|
| 877 | assert (forall fns, |
---|
| 878 | find_symbol ? (add_functs empty fns) id1 = Some ? b1 → |
---|
| 879 | find_symbol ? (add_functs empty fns) id2 = Some ? b2 → |
---|
| 880 | b1 <> b2). |
---|
| 881 | unfold find_symbol. induction fns; simpl; intros. |
---|
| 882 | rewrite PTree.gempty in H2. discriminate. |
---|
| 883 | destruct a as [id f]; simpl in *. |
---|
| 884 | rewrite PTree.gsspec in H2. |
---|
| 885 | destruct (peq id1 id). subst id. inv H2. |
---|
| 886 | rewrite PTree.gso in H3; auto. |
---|
| 887 | generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega. |
---|
| 888 | rewrite PTree.gsspec in H3. |
---|
| 889 | destruct (peq id2 id). subst id. inv H3. |
---|
| 890 | generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega. |
---|
| 891 | eauto. |
---|
| 892 | set (ge0 := add_functs empty p.(prog_funct)). |
---|
| 893 | assert (forall (vars: list (ident * list init_data * V)) ge m, |
---|
| 894 | add_globals (ge0, Mem.empty) vars = (ge, m) → |
---|
| 895 | find_symbol ? ge id1 = Some ? b1 → |
---|
| 896 | find_symbol ? ge id2 = Some ? b2 → |
---|
| 897 | b1 <> b2). |
---|
| 898 | unfold find_symbol. induction vars; simpl. |
---|
| 899 | intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto. |
---|
| 900 | intros ge m. destruct a as [[id init] info]. |
---|
| 901 | caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B. |
---|
| 902 | unfold add_symbol. simpl. intros. |
---|
| 903 | rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3. |
---|
| 904 | rewrite PTree.gso in H4; auto. |
---|
| 905 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega. |
---|
| 906 | rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4. |
---|
| 907 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega. |
---|
| 908 | eauto. |
---|
| 909 | set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)). |
---|
| 910 | apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m). |
---|
| 911 | fold ge_m. apply surjective_pairing. auto. auto. |
---|
| 912 | Qed. |
---|
| 913 | |
---|
| 914 | End GENV. |
---|
| 915 | |
---|
| 916 | (* Global environments and program transformations. *) |
---|
| 917 | |
---|
| 918 | Section MATCH_PROGRAM. |
---|
| 919 | |
---|
| 920 | Variable A B V W: Type. |
---|
| 921 | Variable match_fun: A → B → Prop. |
---|
| 922 | Variable match_var: V → W → Prop. |
---|
| 923 | Variable p: program A V. |
---|
| 924 | Variable p': program B W. |
---|
| 925 | Hypothesis match_prog: |
---|
| 926 | match_program match_fun match_var p p'. |
---|
| 927 | |
---|
| 928 | Lemma add_functs_match: |
---|
| 929 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
| 930 | list_forall2 (match_funct_entry match_fun) fns tfns → |
---|
| 931 | let r := add_functs (empty A) fns in |
---|
| 932 | let tr := add_functs (empty B) tfns in |
---|
| 933 | nextfunction tr = nextfunction r /\ |
---|
| 934 | symbols tr = symbols r /\ |
---|
| 935 | forall (b: block) (f: A), |
---|
| 936 | ZMap.get b (functions r) = Some ? f → |
---|
| 937 | ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf. |
---|
| 938 | Proof. |
---|
| 939 | induction 1; simpl. |
---|
| 940 | |
---|
| 941 | split. reflexivity. split. reflexivity. |
---|
| 942 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
| 943 | |
---|
| 944 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
| 945 | simpl. red in H. destruct H. |
---|
| 946 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
| 947 | rewrite X. rewrite Y. |
---|
| 948 | split. auto. |
---|
| 949 | split. congruence. |
---|
| 950 | intros b f. |
---|
| 951 | repeat (rewrite ZMap.gsspec). |
---|
| 952 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
| 953 | intro EQ; inv EQ. exists fn2; auto. |
---|
| 954 | auto. |
---|
| 955 | Qed. |
---|
| 956 | |
---|
| 957 | Lemma add_functs_rev_match: |
---|
| 958 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
| 959 | list_forall2 (match_funct_entry match_fun) fns tfns → |
---|
| 960 | let r := add_functs (empty A) fns in |
---|
| 961 | let tr := add_functs (empty B) tfns in |
---|
| 962 | nextfunction tr = nextfunction r /\ |
---|
| 963 | symbols tr = symbols r /\ |
---|
| 964 | forall (b: block) (tf: B), |
---|
| 965 | ZMap.get b (functions tr) = Some ? tf → |
---|
| 966 | ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf. |
---|
| 967 | Proof. |
---|
| 968 | induction 1; simpl. |
---|
| 969 | |
---|
| 970 | split. reflexivity. split. reflexivity. |
---|
| 971 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
| 972 | |
---|
| 973 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
| 974 | simpl. red in H. destruct H. |
---|
| 975 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
| 976 | rewrite X. rewrite Y. |
---|
| 977 | split. auto. |
---|
| 978 | split. congruence. |
---|
| 979 | intros b f. |
---|
| 980 | repeat (rewrite ZMap.gsspec). |
---|
| 981 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
| 982 | intro EQ; inv EQ. exists fn1; auto. |
---|
| 983 | auto. |
---|
| 984 | Qed. |
---|
| 985 | |
---|
| 986 | Lemma mem_add_globals_match: |
---|
| 987 | forall (g1: genv A) (g2: genv B) (m: mem) |
---|
| 988 | (vars: list (ident * list init_data * V)) |
---|
| 989 | (tvars: list (ident * list init_data * W)), |
---|
| 990 | list_forall2 (match_var_entry match_var) vars tvars → |
---|
| 991 | snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). |
---|
| 992 | Proof. |
---|
| 993 | induction 1; simpl. |
---|
| 994 | auto. |
---|
| 995 | destruct a1 as [[id1 init1] info1]. |
---|
| 996 | destruct b1 as [[id2 init2] info2]. |
---|
| 997 | red in H. destruct H as [X [Y Z]]. subst id2 init2. |
---|
| 998 | generalize IHlist_forall2. |
---|
| 999 | destruct (add_globals (g1, m) al). |
---|
| 1000 | destruct (add_globals (g2, m) bl). |
---|
| 1001 | simpl. intro. subst m1. auto. |
---|
| 1002 | Qed. |
---|
| 1003 | |
---|
| 1004 | Lemma symbols_add_globals_match: |
---|
| 1005 | forall (g1: genv A) (g2: genv B) (m: mem), |
---|
| 1006 | symbols g1 = symbols g2 → |
---|
| 1007 | forall (vars: list (ident * list init_data * V)) |
---|
| 1008 | (tvars: list (ident * list init_data * W)), |
---|
| 1009 | list_forall2 (match_var_entry match_var) vars tvars → |
---|
| 1010 | symbols (fst (add_globals (g1, m) vars)) = |
---|
| 1011 | symbols (fst (add_globals (g2, m) tvars)). |
---|
| 1012 | Proof. |
---|
| 1013 | induction 2; simpl. |
---|
| 1014 | auto. |
---|
| 1015 | destruct a1 as [[id1 init1] info1]. |
---|
| 1016 | destruct b1 as [[id2 init2] info2]. |
---|
| 1017 | red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. |
---|
| 1018 | generalize IHlist_forall2. |
---|
| 1019 | generalize (mem_add_globals_match g1 g2 m H1). |
---|
| 1020 | destruct (add_globals (g1, m) al). |
---|
| 1021 | destruct (add_globals (g2, m) bl). |
---|
| 1022 | simpl. intros. congruence. |
---|
| 1023 | Qed. |
---|
| 1024 | |
---|
| 1025 | Theorem find_funct_ptr_match: |
---|
| 1026 | forall (b: block) (f: A), |
---|
| 1027 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1028 | ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf. |
---|
| 1029 | Proof. |
---|
| 1030 | intros until f. destruct match_prog as [X [Y Z]]. |
---|
| 1031 | destruct (add_functs_match X) as [P [Q R]]. |
---|
| 1032 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
| 1033 | auto. |
---|
| 1034 | Qed. |
---|
| 1035 | |
---|
| 1036 | Theorem find_funct_ptr_rev_match: |
---|
| 1037 | forall (b: block) (tf: B), |
---|
| 1038 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 1039 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf. |
---|
| 1040 | Proof. |
---|
| 1041 | intros until tf. destruct match_prog as [X [Y Z]]. |
---|
| 1042 | destruct (add_functs_rev_match X) as [P [Q R]]. |
---|
| 1043 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
| 1044 | auto. |
---|
| 1045 | Qed. |
---|
| 1046 | |
---|
| 1047 | Theorem find_funct_match: |
---|
| 1048 | forall (v: val) (f: A), |
---|
| 1049 | find_funct (globalenv p) v = Some ? f → |
---|
| 1050 | ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf. |
---|
| 1051 | Proof. |
---|
| 1052 | intros until f. unfold find_funct. |
---|
| 1053 | case v; try (intros; discriminate). |
---|
| 1054 | intros b ofs. |
---|
| 1055 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
| 1056 | apply find_funct_ptr_match. |
---|
| 1057 | Qed. |
---|
| 1058 | |
---|
| 1059 | Theorem find_funct_rev_match: |
---|
| 1060 | forall (v: val) (tf: B), |
---|
| 1061 | find_funct (globalenv p') v = Some ? tf → |
---|
| 1062 | ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf. |
---|
| 1063 | Proof. |
---|
| 1064 | intros until tf. unfold find_funct. |
---|
| 1065 | case v; try (intros; discriminate). |
---|
| 1066 | intros b ofs. |
---|
| 1067 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
| 1068 | apply find_funct_ptr_rev_match. |
---|
| 1069 | Qed. |
---|
| 1070 | |
---|
| 1071 | Lemma symbols_init_match: |
---|
| 1072 | symbols (globalenv p') = symbols (globalenv p). |
---|
| 1073 | Proof. |
---|
| 1074 | unfold globalenv. unfold globalenv_initmem. |
---|
| 1075 | destruct match_prog as [X [Y Z]]. |
---|
| 1076 | destruct (add_functs_match X) as [P [Q R]]. |
---|
| 1077 | simpl. symmetry. apply symbols_add_globals_match. auto. auto. |
---|
| 1078 | Qed. |
---|
| 1079 | |
---|
| 1080 | Theorem find_symbol_match: |
---|
| 1081 | forall (s: ident), |
---|
| 1082 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 1083 | Proof. |
---|
| 1084 | intros. unfold find_symbol. |
---|
| 1085 | rewrite symbols_init_match. auto. |
---|
| 1086 | Qed. |
---|
| 1087 | |
---|
| 1088 | Theorem init_mem_match: |
---|
| 1089 | init_mem p' = init_mem p. |
---|
| 1090 | Proof. |
---|
| 1091 | unfold init_mem. unfold globalenv_initmem. |
---|
| 1092 | destruct match_prog as [X [Y Z]]. |
---|
| 1093 | symmetry. apply mem_add_globals_match. auto. |
---|
| 1094 | Qed. |
---|
| 1095 | |
---|
| 1096 | End MATCH_PROGRAM. |
---|
| 1097 | |
---|
| 1098 | Section TRANSF_PROGRAM_PARTIAL2. |
---|
| 1099 | |
---|
| 1100 | Variable A B V W: Type. |
---|
| 1101 | Variable transf_fun: A → res B. |
---|
| 1102 | Variable transf_var: V → res W. |
---|
| 1103 | Variable p: program A V. |
---|
| 1104 | Variable p': program B W. |
---|
| 1105 | Hypothesis transf_OK: |
---|
| 1106 | transform_partial_program2 transf_fun transf_var p = OK ? p'. |
---|
| 1107 | |
---|
| 1108 | Remark prog_match: |
---|
| 1109 | match_program |
---|
| 1110 | (fun fd tfd => transf_fun fd = OK ? tfd) |
---|
| 1111 | (fun info tinfo => transf_var info = OK ? tinfo) |
---|
| 1112 | p p'. |
---|
| 1113 | Proof. |
---|
| 1114 | apply transform_partial_program2_match; auto. |
---|
| 1115 | Qed. |
---|
| 1116 | |
---|
| 1117 | Theorem find_funct_ptr_transf_partial2: |
---|
| 1118 | forall (b: block) (f: A), |
---|
| 1119 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1120 | ∃f'. |
---|
| 1121 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'. |
---|
| 1122 | Proof. |
---|
| 1123 | intros. |
---|
| 1124 | exploit find_funct_ptr_match. eexact prog_match. eauto. |
---|
| 1125 | intros [tf [X Y]]. exists tf; auto. |
---|
| 1126 | Qed. |
---|
| 1127 | |
---|
| 1128 | Theorem find_funct_ptr_rev_transf_partial2: |
---|
| 1129 | forall (b: block) (tf: B), |
---|
| 1130 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 1131 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf. |
---|
| 1132 | Proof. |
---|
| 1133 | intros. |
---|
| 1134 | exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. |
---|
| 1135 | Qed. |
---|
| 1136 | |
---|
| 1137 | Theorem find_funct_transf_partial2: |
---|
| 1138 | forall (v: val) (f: A), |
---|
| 1139 | find_funct (globalenv p) v = Some ? f → |
---|
| 1140 | ∃f'. |
---|
| 1141 | find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'. |
---|
| 1142 | Proof. |
---|
| 1143 | intros. |
---|
| 1144 | exploit find_funct_match. eexact prog_match. eauto. |
---|
| 1145 | intros [tf [X Y]]. exists tf; auto. |
---|
| 1146 | Qed. |
---|
| 1147 | |
---|
| 1148 | Theorem find_funct_rev_transf_partial2: |
---|
| 1149 | forall (v: val) (tf: B), |
---|
| 1150 | find_funct (globalenv p') v = Some ? tf → |
---|
| 1151 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf. |
---|
| 1152 | Proof. |
---|
| 1153 | intros. |
---|
| 1154 | exploit find_funct_rev_match. eexact prog_match. eauto. auto. |
---|
| 1155 | Qed. |
---|
| 1156 | |
---|
| 1157 | Theorem find_symbol_transf_partial2: |
---|
| 1158 | forall (s: ident), |
---|
| 1159 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 1160 | Proof. |
---|
| 1161 | intros. eapply find_symbol_match. eexact prog_match. |
---|
| 1162 | Qed. |
---|
| 1163 | |
---|
| 1164 | Theorem init_mem_transf_partial2: |
---|
| 1165 | init_mem p' = init_mem p. |
---|
| 1166 | Proof. |
---|
| 1167 | intros. eapply init_mem_match. eexact prog_match. |
---|
| 1168 | Qed. |
---|
| 1169 | |
---|
| 1170 | End TRANSF_PROGRAM_PARTIAL2. |
---|
| 1171 | |
---|
| 1172 | Section TRANSF_PROGRAM_PARTIAL. |
---|
| 1173 | |
---|
| 1174 | Variable A B V: Type. |
---|
| 1175 | Variable transf: A → res B. |
---|
| 1176 | Variable p: program A V. |
---|
| 1177 | Variable p': program B V. |
---|
| 1178 | Hypothesis transf_OK: transform_partial_program transf p = OK ? p'. |
---|
| 1179 | |
---|
| 1180 | Remark transf2_OK: |
---|
| 1181 | transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'. |
---|
| 1182 | Proof. |
---|
| 1183 | rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. |
---|
| 1184 | destruct (map_partial prefix_funct_name transf (prog_funct p)); auto. |
---|
| 1185 | rewrite map_partial_identity; auto. |
---|
| 1186 | Qed. |
---|
| 1187 | |
---|
| 1188 | Theorem find_funct_ptr_transf_partial: |
---|
| 1189 | forall (b: block) (f: A), |
---|
| 1190 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1191 | ∃f'. |
---|
| 1192 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'. |
---|
| 1193 | Proof. |
---|
| 1194 | exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1195 | Qed. |
---|
| 1196 | |
---|
| 1197 | Theorem find_funct_ptr_rev_transf_partial: |
---|
| 1198 | forall (b: block) (tf: B), |
---|
| 1199 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 1200 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf. |
---|
| 1201 | Proof. |
---|
| 1202 | exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1203 | Qed. |
---|
| 1204 | |
---|
| 1205 | Theorem find_funct_transf_partial: |
---|
| 1206 | forall (v: val) (f: A), |
---|
| 1207 | find_funct (globalenv p) v = Some ? f → |
---|
| 1208 | ∃f'. |
---|
| 1209 | find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'. |
---|
| 1210 | Proof. |
---|
| 1211 | exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1212 | Qed. |
---|
| 1213 | |
---|
| 1214 | Theorem find_funct_rev_transf_partial: |
---|
| 1215 | forall (v: val) (tf: B), |
---|
| 1216 | find_funct (globalenv p') v = Some ? tf → |
---|
| 1217 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf. |
---|
| 1218 | Proof. |
---|
| 1219 | exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1220 | Qed. |
---|
| 1221 | |
---|
| 1222 | Theorem find_symbol_transf_partial: |
---|
| 1223 | forall (s: ident), |
---|
| 1224 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 1225 | Proof. |
---|
| 1226 | exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1227 | Qed. |
---|
| 1228 | |
---|
| 1229 | Theorem init_mem_transf_partial: |
---|
| 1230 | init_mem p' = init_mem p. |
---|
| 1231 | Proof. |
---|
| 1232 | exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1233 | Qed. |
---|
| 1234 | |
---|
| 1235 | End TRANSF_PROGRAM_PARTIAL. |
---|
| 1236 | |
---|
| 1237 | Section TRANSF_PROGRAM. |
---|
| 1238 | |
---|
| 1239 | Variable A B V: Type. |
---|
| 1240 | Variable transf: A → B. |
---|
| 1241 | Variable p: program A V. |
---|
| 1242 | Let tp := transform_program transf p. |
---|
| 1243 | |
---|
| 1244 | Remark transf_OK: |
---|
| 1245 | transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp. |
---|
| 1246 | Proof. |
---|
| 1247 | unfold tp, transform_program, transform_partial_program. |
---|
| 1248 | rewrite map_partial_total. reflexivity. |
---|
| 1249 | Qed. |
---|
| 1250 | |
---|
| 1251 | Theorem find_funct_ptr_transf: |
---|
| 1252 | forall (b: block) (f: A), |
---|
| 1253 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1254 | find_funct_ptr ? (globalenv tp) b = Some ? (transf f). |
---|
| 1255 | Proof. |
---|
| 1256 | intros. |
---|
| 1257 | destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
| 1258 | as [f' [X Y]]. congruence. |
---|
| 1259 | Qed. |
---|
| 1260 | |
---|
| 1261 | Theorem find_funct_ptr_rev_transf: |
---|
| 1262 | forall (b: block) (tf: B), |
---|
| 1263 | find_funct_ptr ? (globalenv tp) b = Some ? tf → |
---|
| 1264 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf. |
---|
| 1265 | Proof. |
---|
| 1266 | intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto. |
---|
| 1267 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
| 1268 | Qed. |
---|
| 1269 | |
---|
| 1270 | Theorem find_funct_transf: |
---|
| 1271 | forall (v: val) (f: A), |
---|
| 1272 | find_funct (globalenv p) v = Some ? f → |
---|
| 1273 | find_funct (globalenv tp) v = Some ? (transf f). |
---|
| 1274 | Proof. |
---|
| 1275 | intros. |
---|
| 1276 | destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
| 1277 | as [f' [X Y]]. congruence. |
---|
| 1278 | Qed. |
---|
| 1279 | |
---|
| 1280 | Theorem find_funct_rev_transf: |
---|
| 1281 | forall (v: val) (tf: B), |
---|
| 1282 | find_funct (globalenv tp) v = Some ? tf → |
---|
| 1283 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf. |
---|
| 1284 | Proof. |
---|
| 1285 | intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto. |
---|
| 1286 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
| 1287 | Qed. |
---|
| 1288 | |
---|
| 1289 | Theorem find_symbol_transf: |
---|
| 1290 | forall (s: ident), |
---|
| 1291 | find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s. |
---|
| 1292 | Proof. |
---|
| 1293 | exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). |
---|
| 1294 | Qed. |
---|
| 1295 | |
---|
| 1296 | Theorem init_mem_transf: |
---|
| 1297 | init_mem tp = init_mem p. |
---|
| 1298 | Proof. |
---|
| 1299 | exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK). |
---|
| 1300 | Qed. |
---|
| 1301 | |
---|
| 1302 | End TRANSF_PROGRAM. |
---|
| 1303 | |
---|
| 1304 | End Genv. |
---|
| 1305 | *) |
---|