[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".*) |
---|
[700] | 39 | include "common/Mem.ma". |
---|
[3] | 40 | |
---|
| 41 | (* FIXME: unimplemented stuff in AST.ma |
---|
[487] | 42 | axiom transform_partial_program: ∀A,B,V:Type[0]. (A → res B) → program A V → res (program B V). |
---|
| 43 | axiom transform_partial_program2: ∀A,B,V,W:Type[0]. (A → res B) → (V → res W) → program A V → res (program B W). |
---|
| 44 | axiom match_program: ∀A,B,V,W:Type[0]. program A V → program B W → Prop. |
---|
[3] | 45 | *) |
---|
| 46 | |
---|
[487] | 47 | record GENV : Type[2] ≝ { |
---|
[3] | 48 | (* * ** Types and operations *) |
---|
| 49 | |
---|
[487] | 50 | genv_t : Type[0] → Type[0]; |
---|
[3] | 51 | (* * The type of global environments. The parameter [F] is the type |
---|
| 52 | of function descriptions. *) |
---|
| 53 | |
---|
[487] | 54 | globalenv: ∀F,V: Type[0]. program F V → res (genv_t F); |
---|
[3] | 55 | (* * Return the global environment for the given program. *) |
---|
| 56 | |
---|
[487] | 57 | init_mem: ∀F,V: Type[0]. program F V → res mem; |
---|
[3] | 58 | (* * Return the initial memory state for the given program. *) |
---|
| 59 | |
---|
[487] | 60 | find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F; |
---|
[3] | 61 | (* * Return the function description associated with the given address, |
---|
| 62 | if any. *) |
---|
| 63 | |
---|
[487] | 64 | find_funct: ∀F: Type[0]. genv_t F → val → option F; |
---|
[3] | 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 | |
---|
[496] | 68 | find_symbol: ∀F: Type[0]. genv_t F → ident → option 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: |
---|
[487] | 74 | ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F. |
---|
[467] | 75 | find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero; |
---|
[3] | 76 | find_funct_find_funct_ptr: |
---|
[487] | 77 | ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block. |
---|
[467] | 78 | find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b; |
---|
[3] | 79 | |
---|
| 80 | find_symbol_exists: |
---|
[487] | 81 | ∀F,V: Type[0]. ∀p: program F V. |
---|
[467] | 82 | ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V. |
---|
| 83 | in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) → |
---|
[3] | 84 | ∃b. find_symbol ? (globalenv ?? p) id = Some ? b; |
---|
| 85 | find_funct_ptr_exists: |
---|
[487] | 86 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F. |
---|
[3] | 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) → |
---|
[467] | 90 | ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 |
---|
[3] | 91 | ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f; |
---|
| 92 | |
---|
| 93 | find_funct_ptr_inversion: |
---|
[487] | 94 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
[3] | 95 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 96 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 97 | find_funct_inversion: |
---|
[487] | 98 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
[3] | 99 | find_funct ? (globalenv ?? p) v = Some ? f → |
---|
| 100 | ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 101 | find_funct_ptr_symbol_inversion: |
---|
[487] | 102 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F. |
---|
[467] | 103 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → |
---|
[3] | 104 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → |
---|
| 105 | in_list ? 〈id, f〉 (prog_funct ?? p); |
---|
| 106 | |
---|
| 107 | find_funct_ptr_prop: |
---|
[487] | 108 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. |
---|
[3] | 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: |
---|
[487] | 113 | ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. |
---|
[3] | 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: |
---|
[487] | 119 | ∀F,V: Type[0]. ∀p: program F V. |
---|
[3] | 120 | let m ≝ init_mem ?? p in |
---|
| 121 | valid_block m nullptr ∧ |
---|
[467] | 122 | (blocks m) nullptr = empty_block 0 0 Any; |
---|
| 123 | (* initmem_inject_neutral: |
---|
[487] | 124 | ∀F,V: Type[0]. ∀p: program F V. |
---|
[467] | 125 | mem_inject_neutral (init_mem ?? p);*) |
---|
[3] | 126 | find_funct_ptr_negative: |
---|
[487] | 127 | ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F. |
---|
[3] | 128 | find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0; |
---|
| 129 | find_symbol_not_fresh: |
---|
[487] | 130 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. |
---|
[467] | 131 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p); |
---|
[3] | 132 | find_symbol_not_nullptr: |
---|
[487] | 133 | ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. |
---|
[467] | 134 | find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr; |
---|
[3] | 135 | global_addresses_distinct: |
---|
[487] | 136 | ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2. |
---|
[3] | 137 | id1≠id2 → |
---|
| 138 | find_symbol ? (globalenv ?? p) id1 = Some ? b1 → |
---|
| 139 | find_symbol ? (globalenv ?? p) id2 = Some ? b2 → |
---|
[467] | 140 | b1≠b2; |
---|
[3] | 141 | |
---|
| 142 | (* * Commutation properties between program transformations |
---|
| 143 | and operations over global environments. *) |
---|
[467] | 144 | |
---|
[3] | 145 | find_funct_ptr_transf: |
---|
[487] | 146 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 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: |
---|
[487] | 151 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 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: |
---|
[487] | 156 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 157 | ∀s: ident. |
---|
| 158 | find_symbol ? (globalenv ?? (transform_program … transf p)) s = |
---|
| 159 | find_symbol ? (globalenv ?? p) s; |
---|
| 160 | init_mem_transf: |
---|
[487] | 161 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 162 | init_mem ?? (transform_program … transf p) = init_mem ?? p; |
---|
| 163 | find_funct_ptr_rev_transf: |
---|
[487] | 164 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 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: |
---|
[487] | 169 | ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. |
---|
[3] | 170 | ∀v : val. ∀tf : B. |
---|
| 171 | find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → |
---|
[467] | 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: |
---|
[487] | 178 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 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: |
---|
[487] | 185 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 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: |
---|
[487] | 192 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 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: |
---|
[487] | 197 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 198 | transform_partial_program … transf p = OK ? p' → |
---|
| 199 | init_mem ?? p' = init_mem ?? p; |
---|
| 200 | find_funct_ptr_rev_transf_partial: |
---|
[487] | 201 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 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: |
---|
[487] | 208 | ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. |
---|
[3] | 209 | transform_partial_program … transf p = OK ? p' → |
---|
| 210 | ∀v : val. ∀tf : B. |
---|
| 211 | find_funct ? (globalenv ?? p') v = Some ? tf → |
---|
| 212 | ∃f : A. |
---|
[467] | 213 | find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*; |
---|
[3] | 214 | |
---|
| 215 | find_funct_ptr_transf_partial2: |
---|
[487] | 216 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 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: |
---|
[487] | 224 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 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: |
---|
[487] | 232 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 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: |
---|
[487] | 238 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 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: |
---|
[487] | 243 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 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: |
---|
[487] | 251 | ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. |
---|
[3] | 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: |
---|
[487] | 263 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 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: |
---|
[487] | 271 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 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: |
---|
[487] | 279 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 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: |
---|
[487] | 286 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 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: |
---|
[487] | 293 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 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: |
---|
[487] | 299 | ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. |
---|
[3] | 300 | ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. |
---|
| 301 | match_program … match_fun match_var p p' → |
---|
[467] | 302 | init_mem ?? p' = init_mem ?? p*)*) |
---|
[3] | 303 | }. |
---|
| 304 | |
---|
[24] | 305 | |
---|
[487] | 306 | let rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l : A ≝ |
---|
[24] | 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 *) |
---|
[487] | 316 | record genv (F:Type[0]) : Type[0] ≝ { |
---|
[3] | 317 | functions: block → option F; |
---|
| 318 | nextfunction: Z; |
---|
[496] | 319 | symbols: ident → option 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 | |
---|
[487] | 329 | Variable F: Type[0]. (* The type of functions *) |
---|
[125] | 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 | |
---|
[487] | 341 | definition add_funct : ∀F:Type[0]. (ident × F) → genv F → genv F ≝ |
---|
[125] | 342 | λF,name_fun,g. |
---|
[498] | 343 | let blk_id ≝ nextfunction ? g in |
---|
| 344 | let b ≝ mk_block Code blk_id in |
---|
| 345 | mk_genv F ((*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b')) |
---|
| 346 | (Zpred blk_id) |
---|
| 347 | ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? g i) ]). |
---|
[125] | 348 | |
---|
[496] | 349 | definition add_symbol : ∀F:Type[0]. ident → block → genv F → genv F ≝ |
---|
| 350 | λF,name,b,g. |
---|
[125] | 351 | mk_genv F (functions ? g) |
---|
| 352 | (nextfunction ? g) |
---|
[496] | 353 | ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? b | inr _ ⇒ symbols ? g i ]). |
---|
[125] | 354 | (* |
---|
| 355 | Definition find_funct_ptr ? (g: genv) (b: block) : option F := |
---|
| 356 | ZMap.get b g.(functions). |
---|
| 357 | |
---|
| 358 | Definition find_funct (g: genv) (v: val) : option F := |
---|
| 359 | match v with |
---|
| 360 | | Vptr b ofs => |
---|
| 361 | if Int.eq ofs Int.zero then find_funct_ptr ? g b else None |
---|
| 362 | | _ => |
---|
| 363 | None |
---|
| 364 | end. |
---|
| 365 | |
---|
| 366 | Definition find_symbol ? (g: genv) (symb: ident) : option block := |
---|
| 367 | PTree.get symb g.(symbols). |
---|
| 368 | |
---|
| 369 | Lemma find_funct_inv: |
---|
| 370 | forall (ge: t) (v: val) (f: F), |
---|
| 371 | find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero. |
---|
| 372 | Proof. |
---|
| 373 | intros until f. unfold find_funct. destruct v; try (intros; discriminate). |
---|
| 374 | generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros. |
---|
| 375 | exists b. congruence. |
---|
| 376 | discriminate. |
---|
| 377 | Qed. |
---|
| 378 | |
---|
| 379 | Lemma find_funct_find_funct_ptr: |
---|
| 380 | forall (ge: t) (b: block), |
---|
| 381 | find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. |
---|
| 382 | Proof. |
---|
| 383 | intros. simpl. |
---|
| 384 | generalize (Int.eq_spec Int.zero Int.zero). |
---|
| 385 | case (Int.eq Int.zero Int.zero); intros. |
---|
| 386 | auto. tauto. |
---|
| 387 | Qed. |
---|
| 388 | *) |
---|
| 389 | (* Construct environment and initial memory store *) |
---|
[487] | 390 | definition empty_mem ≝ empty. (* XXX*) |
---|
| 391 | definition empty : ∀F. genv F ≝ |
---|
[125] | 392 | λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?). |
---|
| 393 | (* mkgenv (ZMap.init None) (-1) (PTree.empty block).*) |
---|
| 394 | |
---|
[487] | 395 | definition add_functs : ∀F:Type[0]. genv F → list (ident × F) → genv F ≝ |
---|
[125] | 396 | λF,init,fns. |
---|
| 397 | foldr ?? (add_funct F) init fns. |
---|
| 398 | |
---|
[485] | 399 | (* init *) |
---|
| 400 | |
---|
[496] | 401 | definition store_init_data : ∀F.genv F → mem → block → Z → init_data → option mem ≝ |
---|
| 402 | λF,ge,m,b,p,id. |
---|
| 403 | (* store checks that the address came from something capable of representing |
---|
| 404 | addresses of the memory region in question - here there are no real |
---|
| 405 | pointers, so use the real region. *) |
---|
[498] | 406 | let r ≝ block_region m b in |
---|
[485] | 407 | match id with |
---|
| 408 | [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n) |
---|
| 409 | | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n) |
---|
| 410 | | Init_int32 n ⇒ store Mint32 m r b p (Vint n) |
---|
| 411 | | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n) |
---|
| 412 | | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n) |
---|
| 413 | | Init_addrof r' symb ofs ⇒ |
---|
| 414 | match (*find_symbol ge symb*) symbols ? ge symb with |
---|
| 415 | [ None ⇒ None ? |
---|
[500] | 416 | | Some b' ⇒ |
---|
| 417 | match pointer_compat_dec b' r' with |
---|
[583] | 418 | [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs)) |
---|
[500] | 419 | | inr _ ⇒ None ? |
---|
| 420 | ] |
---|
[485] | 421 | ] |
---|
| 422 | | Init_space n ⇒ Some ? m |
---|
| 423 | | Init_null r' ⇒ store (Mpointer r') m r b p (Vnull r') |
---|
| 424 | ]. |
---|
| 425 | |
---|
[744] | 426 | definition size_init_data : init_data → nat ≝ |
---|
[485] | 427 | λi_data.match i_data with |
---|
| 428 | [ Init_int8 _ ⇒ 1 |
---|
| 429 | | Init_int16 _ ⇒ 2 |
---|
| 430 | | Init_int32 _ ⇒ 4 |
---|
| 431 | | Init_float32 _ ⇒ 4 |
---|
| 432 | | Init_float64 _ ⇒ 8 |
---|
[744] | 433 | | Init_space n ⇒ max n 0 |
---|
[485] | 434 | | Init_null r ⇒ size_pointer r |
---|
| 435 | | Init_addrof r _ _ ⇒ size_pointer r]. |
---|
| 436 | |
---|
[487] | 437 | let rec store_init_data_list (F:Type[0]) (ge:genv F) |
---|
[496] | 438 | (m: mem) (b: block) (p: Z) (idl: list init_data) |
---|
[485] | 439 | on idl : option mem ≝ |
---|
| 440 | match idl with |
---|
| 441 | [ nil ⇒ Some ? m |
---|
| 442 | | cons id idl' ⇒ |
---|
[496] | 443 | match store_init_data F ge m b p id with |
---|
[485] | 444 | [ None ⇒ None ? |
---|
[496] | 445 | | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl' |
---|
[485] | 446 | ] |
---|
| 447 | ]. |
---|
| 448 | |
---|
[758] | 449 | definition size_init_data_list : list init_data → nat ≝ |
---|
| 450 | λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data. |
---|
[485] | 451 | |
---|
| 452 | (* Nonessential properties that may require arithmetic |
---|
| 453 | nremark size_init_data_list_pos: |
---|
| 454 | ∀i_data. OZ ≤ size_init_data_list i_data. |
---|
[487] | 455 | #i_data;elim i_data;//; |
---|
| 456 | #a;#tl;cut (OZ ≤ size_init_data a) |
---|
| 457 | ##[cases a;normalize;//; |
---|
| 458 | #x;cases x;normalize;//; |
---|
[485] | 459 | ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl)); |
---|
[487] | 460 | cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m) |
---|
| 461 | ##[cases (size_init_data a) in Hsize IH; |
---|
[485] | 462 | ##[##1,2:/3/ |
---|
[487] | 463 | ##|normalize;#n;#Hfalse;elim Hfalse] |
---|
| 464 | ##|#Hdisc;cases Hdisc |
---|
[485] | 465 | ##[#Heq;nrewrite > Heq;//; |
---|
[487] | 466 | ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2; |
---|
[485] | 467 | (* TODO: arithmetics *) napply daemon] |
---|
| 468 | ##] |
---|
| 469 | ##] |
---|
[487] | 470 | qed. |
---|
[485] | 471 | *) |
---|
| 472 | |
---|
[487] | 473 | definition alloc_init_data : mem → list init_data → region → mem × block ≝ |
---|
[496] | 474 | λm,i_data,r. |
---|
[498] | 475 | let b ≝ mk_block r (nextblock m) in |
---|
| 476 | 〈mk_mem (update_block ? b |
---|
[496] | 477 | (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef)) |
---|
[485] | 478 | (blocks m)) |
---|
| 479 | (Zsucc (nextblock m)) |
---|
| 480 | (succ_nextblock_pos m), |
---|
[498] | 481 | b〉. |
---|
[485] | 482 | |
---|
| 483 | (* init *) |
---|
| 484 | |
---|
[797] | 485 | axiom InitDataStoreFailed : String. |
---|
| 486 | |
---|
[487] | 487 | definition add_globals : ∀F,V:Type[0]. |
---|
[480] | 488 | genv F × mem → list (ident × (list init_data) × region × V) → |
---|
[485] | 489 | res (genv F × mem) ≝ |
---|
| 490 | λF,V,init_env,vars. |
---|
| 491 | foldl ?? |
---|
| 492 | (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V. |
---|
[487] | 493 | match id_init with [ pair id_init1 info ⇒ |
---|
| 494 | match id_init1 with [ pair id_init2 r ⇒ |
---|
| 495 | match id_init2 with [ pair id init ⇒ |
---|
[485] | 496 | do 〈g,st〉 ← g_st; |
---|
[487] | 497 | match alloc_init_data st init r with [ pair st' b ⇒ |
---|
[496] | 498 | let g' ≝ add_symbol ? id b g in |
---|
[797] | 499 | do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init); |
---|
[485] | 500 | OK ? 〈g', st''〉 |
---|
| 501 | ] ] ] ]) |
---|
| 502 | (OK ? init_env) vars. |
---|
[125] | 503 | |
---|
[487] | 504 | definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝ |
---|
[125] | 505 | λF,V,p. |
---|
| 506 | add_globals F V |
---|
[485] | 507 | 〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉 |
---|
| 508 | (prog_vars ?? p). |
---|
[125] | 509 | |
---|
[487] | 510 | definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝ |
---|
[125] | 511 | λF,V,p. |
---|
[485] | 512 | do 〈g,m〉 ← globalenv_initmem F V p; |
---|
| 513 | OK ? g. |
---|
[487] | 514 | definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝ |
---|
[125] | 515 | λF,V,p. |
---|
[485] | 516 | do 〈g,m〉 ← globalenv_initmem F V p; |
---|
| 517 | OK ? m. |
---|
[125] | 518 | |
---|
[485] | 519 | |
---|
| 520 | |
---|
| 521 | |
---|
[487] | 522 | definition Genv : GENV ≝ mk_GENV |
---|
[3] | 523 | genv (* genv_t *) |
---|
[125] | 524 | globalenv_ |
---|
| 525 | init_mem_ |
---|
[3] | 526 | (λF,ge. functions ? ge) (* find_funct_ptr *) |
---|
[583] | 527 | (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq_offset o zero_offset then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *) |
---|
[3] | 528 | (λF,ge. symbols ? ge) (* find_symbol *) |
---|
[125] | 529 | (* ? |
---|
[24] | 530 | ? |
---|
| 531 | ? |
---|
| 532 | ? |
---|
| 533 | ? |
---|
[125] | 534 | ?*) |
---|
[3] | 535 | . |
---|
[125] | 536 | (* |
---|
[487] | 537 | ##[ #A B C transf p b f; elim p; #fns main vars; |
---|
| 538 | elim fns; |
---|
| 539 | ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct; |
---|
| 540 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?); |
---|
[24] | 541 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 542 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 543 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 544 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 545 | ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH; |
---|
| 546 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 547 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?); |
---|
| 548 | ##[ #H; destruct (H); //; |
---|
[24] | 549 | ##| #H; napply IH; napply H; |
---|
| 550 | ##] |
---|
| 551 | ##] |
---|
| 552 | ##] |
---|
| 553 | ##] |
---|
[487] | 554 | ##| #A B C transf p v f; elim v; |
---|
| 555 | ##[ whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
| 556 | ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
| 557 | ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero); |
---|
| 558 | whd in ⊢ (??%? → ??%?); |
---|
| 559 | ##[ elim p; #fns main vars; elim fns; |
---|
| 560 | ##[ whd in ⊢ (??%? → ??%?); #H; destruct; |
---|
| 561 | ##| #h t; elim h; #f fn IH; |
---|
| 562 | whd in ⊢ (??%? → ??%?); |
---|
[24] | 563 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 564 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 565 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 566 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 567 | ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH; |
---|
| 568 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 569 | ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H; |
---|
| 570 | ##[ destruct (H); //; |
---|
[24] | 571 | ##| napply IH; napply H; |
---|
| 572 | ##] |
---|
| 573 | ##] |
---|
| 574 | ##] |
---|
| 575 | ##] |
---|
[487] | 576 | ##| #H; destruct; |
---|
[24] | 577 | ##] |
---|
| 578 | ##] |
---|
[487] | 579 | ##| #A B C transf p id; elim p; #fns main vars; |
---|
| 580 | elim fns; |
---|
| 581 | ##[ normalize; // |
---|
| 582 | ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH; |
---|
| 583 | elim (ident_eq fid id); #e; |
---|
| 584 | ##[ whd in ⊢ (??%%); |
---|
[24] | 585 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 586 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 587 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 588 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 589 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 590 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 591 | ##| // |
---|
| 592 | ##] |
---|
| 593 | ##] |
---|
[487] | 594 | ##| whd in ⊢ (??%%); nrewrite > IH; napply refl; |
---|
[24] | 595 | ##] |
---|
| 596 | ##] |
---|
| 597 | ##| //; |
---|
[487] | 598 | ##| #A B C transf p b tf; elim p; #fns main vars; |
---|
| 599 | elim fns; |
---|
| 600 | ##[ normalize; #H; destruct; |
---|
| 601 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
[24] | 602 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 603 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 604 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 605 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 606 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 607 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 608 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 609 | ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; |
---|
[24] | 610 | ##| #H; napply IH; napply H; |
---|
| 611 | ##] |
---|
| 612 | ##] |
---|
| 613 | ##] |
---|
| 614 | ##] |
---|
[487] | 615 | ##| #A B C transf p v tf; elim p; #fns main vars; elim v; |
---|
| 616 | ##[ normalize; #H; destruct; |
---|
| 617 | ##| ##2,3: #x; normalize; #H; destruct; |
---|
| 618 | ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero); |
---|
| 619 | ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 620 | elim fns; |
---|
| 621 | ##[ normalize; #H; destruct; |
---|
| 622 | ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
[24] | 623 | nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 624 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; |
---|
| 625 | nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
[24] | 626 | ##| nrewrite > (?:nextfunction ?? = length ? t); |
---|
[487] | 627 | ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; |
---|
| 628 | whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] |
---|
| 629 | ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); |
---|
| 630 | ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; |
---|
[24] | 631 | ##| #H; napply IH; napply H; |
---|
| 632 | ##] |
---|
| 633 | ##] |
---|
| 634 | ##] |
---|
| 635 | ##] |
---|
[487] | 636 | ##| normalize; #H; destruct; |
---|
[24] | 637 | ##] |
---|
| 638 | ##] |
---|
[487] | 639 | ##] qed. |
---|
[24] | 640 | |
---|
[3] | 641 | |
---|
| 642 | Lemma functions_globalenv: |
---|
| 643 | forall (p: program F V), |
---|
| 644 | functions (globalenv p) = functions (add_functs empty p.(prog_funct)). |
---|
| 645 | Proof. |
---|
| 646 | assert (forall init vars, |
---|
| 647 | functions (fst (add_globals init vars)) = functions (fst init)). |
---|
| 648 | induction vars; simpl. |
---|
| 649 | reflexivity. |
---|
| 650 | destruct a as [[id1 init1] info1]. destruct (add_globals init vars). |
---|
| 651 | simpl. exact IHvars. |
---|
| 652 | |
---|
| 653 | unfold add_globals; simpl. |
---|
| 654 | intros. unfold globalenv; unfold globalenv_initmem. |
---|
| 655 | rewrite H. reflexivity. |
---|
| 656 | Qed. |
---|
| 657 | |
---|
| 658 | Lemma initmem_nullptr: |
---|
| 659 | forall (p: program F V), |
---|
| 660 | let m := init_mem p in |
---|
| 661 | valid_block m nullptr /\ |
---|
| 662 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef). |
---|
| 663 | Proof. |
---|
| 664 | pose (P := fun m => valid_block m nullptr /\ |
---|
| 665 | m.(blocks) nullptr = mkblock 0 0 (fun y => Undef)). |
---|
| 666 | assert (forall init, P (snd init) → forall vars, P (snd (add_globals init vars))). |
---|
| 667 | induction vars; simpl; intros. |
---|
| 668 | auto. |
---|
| 669 | destruct a as [[id1 in1] inf1]. |
---|
| 670 | destruct (add_globals init vars) as [g st]. |
---|
| 671 | simpl in *. destruct IHvars. split. |
---|
| 672 | red; simpl. red in H0. omega. |
---|
| 673 | simpl. rewrite update_o. auto. unfold block. red in H0. omega. |
---|
| 674 | |
---|
| 675 | intro. unfold init_mem, globalenv_initmem. apply H. |
---|
| 676 | red; simpl. split. compute. auto. reflexivity. |
---|
| 677 | Qed. |
---|
| 678 | |
---|
| 679 | Lemma initmem_inject_neutral: |
---|
| 680 | forall (p: program F V), |
---|
| 681 | mem_inject_neutral (init_mem p). |
---|
| 682 | Proof. |
---|
| 683 | assert (forall g0 vars g1 m, |
---|
| 684 | add_globals (g0, Mem.empty) vars = (g1, m) → |
---|
| 685 | mem_inject_neutral m). |
---|
| 686 | Opaque alloc_init_data. |
---|
| 687 | induction vars; simpl. |
---|
| 688 | intros. inv H. red; intros. destruct (load_inv _ _ _ _ _ H). |
---|
| 689 | simpl in H1. rewrite Mem.getN_init in H1. |
---|
| 690 | replace v with Vundef. auto. destruct chunk; simpl in H1; auto. |
---|
| 691 | destruct a as [[id1 init1] info1]. |
---|
| 692 | caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. |
---|
| 693 | caseEq (alloc_init_data m1 init1). intros m2 b ALLOC. |
---|
| 694 | intros. inv H. |
---|
| 695 | eapply Mem.alloc_init_data_neutral; eauto. |
---|
| 696 | intros. caseEq (globalenv_initmem p). intros g m EQ. |
---|
| 697 | unfold init_mem; rewrite EQ; simpl. |
---|
| 698 | unfold globalenv_initmem in EQ. eauto. |
---|
| 699 | Qed. |
---|
| 700 | |
---|
| 701 | Remark nextfunction_add_functs_neg: |
---|
| 702 | forall fns, nextfunction (add_functs empty fns) < 0. |
---|
| 703 | Proof. |
---|
| 704 | induction fns; simpl; intros. omega. unfold Zpred. omega. |
---|
| 705 | Qed. |
---|
| 706 | |
---|
| 707 | Theorem find_funct_ptr_negative: |
---|
| 708 | forall (p: program F V) (b: block) (f: F), |
---|
| 709 | find_funct_ptr ? (globalenv p) b = Some ? f → b < 0. |
---|
| 710 | Proof. |
---|
| 711 | intros until f. |
---|
| 712 | assert (forall fns, ZMap.get b (functions (add_functs empty fns)) = Some ? f → b < 0). |
---|
| 713 | induction fns; simpl. |
---|
| 714 | rewrite ZMap.gi. congruence. |
---|
| 715 | rewrite ZMap.gsspec. case (ZIndexed.eq b (nextfunction (add_functs empty fns))); intro. |
---|
| 716 | intro. rewrite e. apply nextfunction_add_functs_neg. |
---|
| 717 | auto. |
---|
| 718 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
| 719 | intros. eauto. |
---|
| 720 | Qed. |
---|
| 721 | |
---|
| 722 | Remark find_symbol_add_functs_negative: |
---|
| 723 | forall (fns: list (ident * F)) s b, |
---|
| 724 | (symbols (add_functs empty fns)) ! s = Some ? b → b < 0. |
---|
| 725 | Proof. |
---|
| 726 | induction fns; simpl; intros until b. |
---|
| 727 | rewrite PTree.gempty. congruence. |
---|
| 728 | rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro. |
---|
| 729 | intro EQ; inversion EQ. apply nextfunction_add_functs_neg. |
---|
| 730 | eauto. |
---|
| 731 | Qed. |
---|
| 732 | |
---|
| 733 | Remark find_symbol_add_symbols_not_fresh: |
---|
| 734 | forall fns vars g m s b, |
---|
| 735 | add_globals (add_functs empty fns, Mem.empty) vars = (g, m) → |
---|
| 736 | (symbols g)!s = Some ? b → |
---|
| 737 | b < nextblock m. |
---|
| 738 | Proof. |
---|
| 739 | induction vars; simpl; intros until b. |
---|
| 740 | intros. inversion H. subst g m. simpl. |
---|
| 741 | generalize (find_symbol_add_functs_negative fns s H0). omega. |
---|
| 742 | Transparent alloc_init_data. |
---|
| 743 | destruct a as [[id1 init1] info1]. |
---|
| 744 | caseEq (add_globals (add_functs empty fns, Mem.empty) vars). |
---|
| 745 | intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. |
---|
| 746 | unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro. |
---|
| 747 | intro EQ; inversion EQ. omega. |
---|
| 748 | intro. generalize (IHvars _ _ _ _ ADG H). omega. |
---|
| 749 | Qed. |
---|
| 750 | |
---|
| 751 | Theorem find_symbol_not_fresh: |
---|
| 752 | forall (p: program F V) (id: ident) (b: block), |
---|
| 753 | find_symbol ? (globalenv p) id = Some ? b → b < nextblock (init_mem p). |
---|
| 754 | Proof. |
---|
| 755 | intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. |
---|
| 756 | caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty) |
---|
| 757 | (prog_vars p)); intros g m EQ. |
---|
| 758 | simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto. |
---|
| 759 | Qed. |
---|
| 760 | |
---|
| 761 | Lemma find_symbol_exists: |
---|
| 762 | forall (p: program F V) |
---|
| 763 | (id: ident) (init: list init_data) (v: V), |
---|
| 764 | In (id, init, v) (prog_vars p) → |
---|
| 765 | ∃b. find_symbol ? (globalenv p) id = Some ? b. |
---|
| 766 | Proof. |
---|
| 767 | intros until v. |
---|
| 768 | assert (forall initm vl, In (id, init, v) vl → |
---|
| 769 | ∃b. PTree.get id (symbols (fst (add_globals initm vl))) = Some ? b). |
---|
| 770 | induction vl; simpl; intros. |
---|
| 771 | elim H. |
---|
| 772 | destruct a as [[id0 init0] v0]. |
---|
| 773 | caseEq (add_globals initm vl). intros g1 m1 EQ. simpl. |
---|
| 774 | rewrite PTree.gsspec. destruct (peq id id0). econstructor; eauto. |
---|
| 775 | elim H; intro. congruence. generalize (IHvl H0). rewrite EQ. auto. |
---|
| 776 | intros. unfold globalenv, find_symbol, globalenv_initmem. auto. |
---|
| 777 | Qed. |
---|
| 778 | |
---|
| 779 | Remark find_symbol_above_nextfunction: |
---|
| 780 | forall (id: ident) (b: block) (fns: list (ident * F)), |
---|
| 781 | let g := add_functs empty fns in |
---|
| 782 | PTree.get id g.(symbols) = Some ? b → |
---|
| 783 | b > g.(nextfunction). |
---|
| 784 | Proof. |
---|
| 785 | induction fns; simpl. |
---|
| 786 | rewrite PTree.gempty. congruence. |
---|
| 787 | rewrite PTree.gsspec. case (peq id (fst a)); intro. |
---|
| 788 | intro EQ. inversion EQ. unfold Zpred. omega. |
---|
| 789 | intros. generalize (IHfns H). unfold Zpred; omega. |
---|
| 790 | Qed. |
---|
| 791 | |
---|
| 792 | Remark find_symbol_add_globals: |
---|
| 793 | forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)), |
---|
| 794 | ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) → |
---|
| 795 | find_symbol ? (fst (add_globals ge_m vars)) id = |
---|
| 796 | find_symbol ? (fst ge_m) id. |
---|
| 797 | Proof. |
---|
| 798 | unfold find_symbol; induction vars; simpl; intros. |
---|
| 799 | auto. |
---|
| 800 | destruct a as [[id0 init0] var0]. simpl in *. |
---|
| 801 | caseEq (add_globals ge_m vars); intros ge' m' EQ. |
---|
| 802 | simpl. rewrite PTree.gso. rewrite EQ in IHvars. simpl in IHvars. |
---|
| 803 | apply IHvars. tauto. intuition congruence. |
---|
| 804 | Qed. |
---|
| 805 | |
---|
| 806 | Lemma find_funct_ptr_exists: |
---|
| 807 | forall (p: program F V) (id: ident) (f: F), |
---|
| 808 | list_norepet (prog_funct_names p) → |
---|
| 809 | list_disjoint (prog_funct_names p) (prog_var_names p) → |
---|
| 810 | In (id, f) (prog_funct p) → |
---|
| 811 | ∃b. find_symbol ? (globalenv p) id = Some ? b |
---|
| 812 | /\ find_funct_ptr ? (globalenv p) b = Some ? f. |
---|
| 813 | Proof. |
---|
| 814 | intros until f. |
---|
| 815 | assert (forall (fns: list (ident * F)), |
---|
| 816 | list_norepet (map (@fst ident F) fns) → |
---|
| 817 | In (id, f) fns → |
---|
| 818 | ∃b. find_symbol ? (add_functs empty fns) id = Some ? b |
---|
| 819 | /\ find_funct_ptr ? (add_functs empty fns) b = Some ? f). |
---|
| 820 | unfold find_symbol, find_funct_ptr. induction fns; intros. |
---|
| 821 | elim H0. |
---|
| 822 | destruct a as [id0 f0]; simpl in *. inv H. |
---|
| 823 | unfold add_funct; simpl. |
---|
| 824 | rewrite PTree.gsspec. destruct (peq id id0). |
---|
| 825 | subst id0. econstructor; split. eauto. |
---|
| 826 | replace f0 with f. apply ZMap.gss. |
---|
| 827 | elim H0; intro. congruence. elim H3. |
---|
| 828 | change id with (@fst ident F (id, f)). apply List.in_map. auto. |
---|
| 829 | exploit IHfns; eauto. elim H0; intro. congruence. auto. |
---|
| 830 | intros [b [X Y]]. exists b; split. auto. rewrite ZMap.gso. auto. |
---|
| 831 | generalize (find_symbol_above_nextfunction _ _ X). |
---|
| 832 | unfold block; unfold ZIndexed.t; intro; omega. |
---|
| 833 | |
---|
| 834 | intros. exploit H; eauto. intros [b [X Y]]. |
---|
| 835 | exists b; split. |
---|
| 836 | unfold globalenv, globalenv_initmem. rewrite find_symbol_add_globals. |
---|
| 837 | assumption. apply list_disjoint_notin with (prog_funct_names p). assumption. |
---|
| 838 | unfold prog_funct_names. change id with (fst (id, f)). |
---|
| 839 | apply List.in_map; auto. |
---|
| 840 | unfold find_funct_ptr. rewrite functions_globalenv. |
---|
| 841 | assumption. |
---|
| 842 | Qed. |
---|
| 843 | |
---|
| 844 | Lemma find_funct_ptr_inversion: |
---|
| 845 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
| 846 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 847 | ∃id. In (id, f) (prog_funct p). |
---|
| 848 | Proof. |
---|
| 849 | intros until f. |
---|
| 850 | assert (forall fns: list (ident * F), |
---|
| 851 | find_funct_ptr ? (add_functs empty fns) b = Some ? f → |
---|
| 852 | ∃id. In (id, f) fns). |
---|
| 853 | unfold find_funct_ptr. induction fns; simpl. |
---|
| 854 | rewrite ZMap.gi. congruence. |
---|
| 855 | destruct a as [id0 f0]; simpl. |
---|
| 856 | rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))). |
---|
| 857 | intro. inv H. exists id0; auto. |
---|
| 858 | intro. exploit IHfns; eauto. intros [id A]. exists id; auto. |
---|
| 859 | unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto. |
---|
| 860 | Qed. |
---|
| 861 | |
---|
| 862 | Lemma find_funct_ptr_prop: |
---|
| 863 | forall (P: F → Prop) (p: program F V) (b: block) (f: F), |
---|
| 864 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
| 865 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 866 | P f. |
---|
| 867 | Proof. |
---|
| 868 | intros. exploit find_funct_ptr_inversion; eauto. intros [id A]. eauto. |
---|
| 869 | Qed. |
---|
| 870 | |
---|
| 871 | Lemma find_funct_inversion: |
---|
| 872 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
| 873 | find_funct (globalenv p) v = Some ? f → |
---|
| 874 | ∃id. In (id, f) (prog_funct p). |
---|
| 875 | Proof. |
---|
| 876 | intros. exploit find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H. |
---|
| 877 | rewrite find_funct_find_funct_ptr ? in H. |
---|
| 878 | eapply find_funct_ptr_inversion; eauto. |
---|
| 879 | Qed. |
---|
| 880 | |
---|
| 881 | Lemma find_funct_prop: |
---|
| 882 | forall (P: F → Prop) (p: program F V) (v: val) (f: F), |
---|
| 883 | (forall id f, In (id, f) (prog_funct p) → P f) → |
---|
| 884 | find_funct (globalenv p) v = Some ? f → |
---|
| 885 | P f. |
---|
| 886 | Proof. |
---|
| 887 | intros. exploit find_funct_inversion; eauto. intros [id A]. eauto. |
---|
| 888 | Qed. |
---|
| 889 | |
---|
| 890 | Lemma find_funct_ptr_symbol_inversion: |
---|
| 891 | forall (p: program F V) (id: ident) (b: block) (f: F), |
---|
| 892 | find_symbol ? (globalenv p) id = Some ? b → |
---|
| 893 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 894 | In (id, f) p.(prog_funct). |
---|
| 895 | Proof. |
---|
| 896 | intros until f. |
---|
| 897 | assert (forall fns, |
---|
| 898 | let g := add_functs empty fns in |
---|
| 899 | PTree.get id g.(symbols) = Some ? b → |
---|
| 900 | ZMap.get b g.(functions) = Some ? f → |
---|
| 901 | In (id, f) fns). |
---|
| 902 | induction fns; simpl. |
---|
| 903 | rewrite ZMap.gi. congruence. |
---|
| 904 | set (g := add_functs empty fns). |
---|
| 905 | rewrite PTree.gsspec. rewrite ZMap.gsspec. |
---|
| 906 | case (peq id (fst a)); intro. |
---|
| 907 | intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. |
---|
| 908 | intro EQ2. left. destruct a. simpl in *. congruence. |
---|
| 909 | intro. unfold ZIndexed.eq. rewrite zeq_false. intro. eauto. |
---|
| 910 | generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega. |
---|
| 911 | assert (forall g0 m0, b < 0 → |
---|
| 912 | forall vars g m, |
---|
| 913 | add_globals (g0, m0) vars = (g, m) → |
---|
| 914 | PTree.get id g.(symbols) = Some ? b → |
---|
| 915 | PTree.get id g0.(symbols) = Some ? b). |
---|
| 916 | induction vars; simpl. |
---|
| 917 | intros. inv H1. auto. |
---|
| 918 | destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). |
---|
| 919 | intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1. |
---|
| 920 | unfold add_symbol; intros A B. rewrite <- B. simpl. |
---|
| 921 | rewrite PTree.gsspec. case (peq id id1); intros. |
---|
| 922 | assert (b > 0). inv H1. apply nextblock_pos. |
---|
| 923 | omegaContradiction. |
---|
| 924 | eauto. |
---|
| 925 | intros. |
---|
| 926 | generalize (find_funct_ptr_negative _ _ H2). intro. |
---|
| 927 | pose (g := add_functs empty (prog_funct p)). |
---|
| 928 | apply H. |
---|
| 929 | apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). |
---|
| 930 | auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. |
---|
| 931 | reflexivity. assumption. rewrite <- functions_globalenv. assumption. |
---|
| 932 | Qed. |
---|
| 933 | |
---|
| 934 | Theorem find_symbol_not_nullptr: |
---|
| 935 | forall (p: program F V) (id: ident) (b: block), |
---|
| 936 | find_symbol ? (globalenv p) id = Some ? b → b <> nullptr. |
---|
| 937 | Proof. |
---|
| 938 | intros until b. |
---|
| 939 | assert (forall fns, |
---|
| 940 | find_symbol ? (add_functs empty fns) id = Some ? b → |
---|
| 941 | b <> nullptr). |
---|
| 942 | unfold find_symbol; induction fns; simpl. |
---|
| 943 | rewrite PTree.gempty. congruence. |
---|
| 944 | destruct a as [id1 f1]. simpl. rewrite PTree.gsspec. |
---|
| 945 | destruct (peq id id1); intros. |
---|
| 946 | inversion H. generalize (nextfunction_add_functs_neg fns). |
---|
| 947 | unfold block, nullptr; omega. |
---|
| 948 | auto. |
---|
| 949 | set (g0 := add_functs empty p.(prog_funct)). |
---|
| 950 | assert (forall vars g m, |
---|
| 951 | add_globals (g0, Mem.empty) vars = (g, m) → |
---|
| 952 | find_symbol ? g id = Some ? b → |
---|
| 953 | b <> nullptr). |
---|
| 954 | induction vars; simpl; intros until m. |
---|
| 955 | intros. inversion H0. subst g. apply H with (prog_funct p). auto. |
---|
| 956 | destruct a as [[id1 init1] info1]. |
---|
| 957 | caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2. |
---|
| 958 | inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec. |
---|
| 959 | destruct (peq id id1); intros. |
---|
| 960 | inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega. |
---|
| 961 | eauto. |
---|
| 962 | intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto. |
---|
| 963 | Qed. |
---|
| 964 | |
---|
| 965 | Theorem global_addresses_distinct: |
---|
| 966 | forall (p: program F V) id1 id2 b1 b2, |
---|
| 967 | id1<>id2 → |
---|
| 968 | find_symbol ? (globalenv p) id1 = Some ? b1 → |
---|
| 969 | find_symbol ? (globalenv p) id2 = Some ? b2 → |
---|
| 970 | b1<>b2. |
---|
| 971 | Proof. |
---|
| 972 | intros. |
---|
| 973 | assert (forall fns, |
---|
| 974 | find_symbol ? (add_functs empty fns) id1 = Some ? b1 → |
---|
| 975 | find_symbol ? (add_functs empty fns) id2 = Some ? b2 → |
---|
| 976 | b1 <> b2). |
---|
| 977 | unfold find_symbol. induction fns; simpl; intros. |
---|
| 978 | rewrite PTree.gempty in H2. discriminate. |
---|
| 979 | destruct a as [id f]; simpl in *. |
---|
| 980 | rewrite PTree.gsspec in H2. |
---|
| 981 | destruct (peq id1 id). subst id. inv H2. |
---|
| 982 | rewrite PTree.gso in H3; auto. |
---|
| 983 | generalize (find_symbol_above_nextfunction _ _ H3). unfold block. omega. |
---|
| 984 | rewrite PTree.gsspec in H3. |
---|
| 985 | destruct (peq id2 id). subst id. inv H3. |
---|
| 986 | generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega. |
---|
| 987 | eauto. |
---|
| 988 | set (ge0 := add_functs empty p.(prog_funct)). |
---|
| 989 | assert (forall (vars: list (ident * list init_data * V)) ge m, |
---|
| 990 | add_globals (ge0, Mem.empty) vars = (ge, m) → |
---|
| 991 | find_symbol ? ge id1 = Some ? b1 → |
---|
| 992 | find_symbol ? ge id2 = Some ? b2 → |
---|
| 993 | b1 <> b2). |
---|
| 994 | unfold find_symbol. induction vars; simpl. |
---|
| 995 | intros. inv H3. subst ge. apply H2 with (p.(prog_funct)); auto. |
---|
| 996 | intros ge m. destruct a as [[id init] info]. |
---|
| 997 | caseEq (add_globals (ge0, Mem.empty) vars). intros ge1 m1 A B. inv B. |
---|
| 998 | unfold add_symbol. simpl. intros. |
---|
| 999 | rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3. |
---|
| 1000 | rewrite PTree.gso in H4; auto. |
---|
| 1001 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega. |
---|
| 1002 | rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4. |
---|
| 1003 | generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega. |
---|
| 1004 | eauto. |
---|
| 1005 | set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)). |
---|
| 1006 | apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m). |
---|
| 1007 | fold ge_m. apply surjective_pairing. auto. auto. |
---|
| 1008 | Qed. |
---|
| 1009 | |
---|
| 1010 | End GENV. |
---|
| 1011 | |
---|
| 1012 | (* Global environments and program transformations. *) |
---|
| 1013 | |
---|
| 1014 | Section MATCH_PROGRAM. |
---|
| 1015 | |
---|
| 1016 | Variable A B V W: Type. |
---|
| 1017 | Variable match_fun: A → B → Prop. |
---|
| 1018 | Variable match_var: V → W → Prop. |
---|
| 1019 | Variable p: program A V. |
---|
| 1020 | Variable p': program B W. |
---|
| 1021 | Hypothesis match_prog: |
---|
| 1022 | match_program match_fun match_var p p'. |
---|
| 1023 | |
---|
| 1024 | Lemma add_functs_match: |
---|
| 1025 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
[487] | 1026 | list_forall2 (match_funct_etry match_fun) fns tfns → |
---|
[3] | 1027 | let r := add_functs (empty A) fns in |
---|
| 1028 | let tr := add_functs (empty B) tfns in |
---|
| 1029 | nextfunction tr = nextfunction r /\ |
---|
| 1030 | symbols tr = symbols r /\ |
---|
| 1031 | forall (b: block) (f: A), |
---|
| 1032 | ZMap.get b (functions r) = Some ? f → |
---|
| 1033 | ∃tf. ZMap.get b (functions tr) = Some ? tf /\ match_fun f tf. |
---|
| 1034 | Proof. |
---|
| 1035 | induction 1; simpl. |
---|
| 1036 | |
---|
| 1037 | split. reflexivity. split. reflexivity. |
---|
| 1038 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
| 1039 | |
---|
| 1040 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
| 1041 | simpl. red in H. destruct H. |
---|
| 1042 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
| 1043 | rewrite X. rewrite Y. |
---|
| 1044 | split. auto. |
---|
| 1045 | split. congruence. |
---|
| 1046 | intros b f. |
---|
| 1047 | repeat (rewrite ZMap.gsspec). |
---|
| 1048 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
| 1049 | intro EQ; inv EQ. exists fn2; auto. |
---|
| 1050 | auto. |
---|
| 1051 | Qed. |
---|
| 1052 | |
---|
| 1053 | Lemma add_functs_rev_match: |
---|
| 1054 | forall (fns: list (ident * A)) (tfns: list (ident * B)), |
---|
[487] | 1055 | list_forall2 (match_funct_etry match_fun) fns tfns → |
---|
[3] | 1056 | let r := add_functs (empty A) fns in |
---|
| 1057 | let tr := add_functs (empty B) tfns in |
---|
| 1058 | nextfunction tr = nextfunction r /\ |
---|
| 1059 | symbols tr = symbols r /\ |
---|
| 1060 | forall (b: block) (tf: B), |
---|
| 1061 | ZMap.get b (functions tr) = Some ? tf → |
---|
| 1062 | ∃f. ZMap.get b (functions r) = Some ? f /\ match_fun f tf. |
---|
| 1063 | Proof. |
---|
| 1064 | induction 1; simpl. |
---|
| 1065 | |
---|
| 1066 | split. reflexivity. split. reflexivity. |
---|
| 1067 | intros b f; repeat (rewrite ZMap.gi). intros; discriminate. |
---|
| 1068 | |
---|
| 1069 | destruct a1 as [id1 fn1]. destruct b1 as [id2 fn2]. |
---|
| 1070 | simpl. red in H. destruct H. |
---|
| 1071 | destruct IHlist_forall2 as [X [Y Z]]. |
---|
| 1072 | rewrite X. rewrite Y. |
---|
| 1073 | split. auto. |
---|
| 1074 | split. congruence. |
---|
| 1075 | intros b f. |
---|
| 1076 | repeat (rewrite ZMap.gsspec). |
---|
| 1077 | destruct (ZIndexed.eq b (nextfunction (add_functs (empty A) al))). |
---|
| 1078 | intro EQ; inv EQ. exists fn1; auto. |
---|
| 1079 | auto. |
---|
| 1080 | Qed. |
---|
| 1081 | |
---|
| 1082 | Lemma mem_add_globals_match: |
---|
| 1083 | forall (g1: genv A) (g2: genv B) (m: mem) |
---|
| 1084 | (vars: list (ident * list init_data * V)) |
---|
| 1085 | (tvars: list (ident * list init_data * W)), |
---|
[487] | 1086 | list_forall2 (match_var_etry match_var) vars tvars → |
---|
[3] | 1087 | snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). |
---|
| 1088 | Proof. |
---|
| 1089 | induction 1; simpl. |
---|
| 1090 | auto. |
---|
| 1091 | destruct a1 as [[id1 init1] info1]. |
---|
| 1092 | destruct b1 as [[id2 init2] info2]. |
---|
| 1093 | red in H. destruct H as [X [Y Z]]. subst id2 init2. |
---|
| 1094 | generalize IHlist_forall2. |
---|
| 1095 | destruct (add_globals (g1, m) al). |
---|
| 1096 | destruct (add_globals (g2, m) bl). |
---|
| 1097 | simpl. intro. subst m1. auto. |
---|
| 1098 | Qed. |
---|
| 1099 | |
---|
| 1100 | Lemma symbols_add_globals_match: |
---|
| 1101 | forall (g1: genv A) (g2: genv B) (m: mem), |
---|
| 1102 | symbols g1 = symbols g2 → |
---|
| 1103 | forall (vars: list (ident * list init_data * V)) |
---|
| 1104 | (tvars: list (ident * list init_data * W)), |
---|
[487] | 1105 | list_forall2 (match_var_etry match_var) vars tvars → |
---|
[3] | 1106 | symbols (fst (add_globals (g1, m) vars)) = |
---|
| 1107 | symbols (fst (add_globals (g2, m) tvars)). |
---|
| 1108 | Proof. |
---|
| 1109 | induction 2; simpl. |
---|
| 1110 | auto. |
---|
| 1111 | destruct a1 as [[id1 init1] info1]. |
---|
| 1112 | destruct b1 as [[id2 init2] info2]. |
---|
| 1113 | red in H0. destruct H0 as [X [Y Z]]. subst id2 init2. |
---|
| 1114 | generalize IHlist_forall2. |
---|
| 1115 | generalize (mem_add_globals_match g1 g2 m H1). |
---|
| 1116 | destruct (add_globals (g1, m) al). |
---|
| 1117 | destruct (add_globals (g2, m) bl). |
---|
| 1118 | simpl. intros. congruence. |
---|
| 1119 | Qed. |
---|
| 1120 | |
---|
| 1121 | Theorem find_funct_ptr_match: |
---|
| 1122 | forall (b: block) (f: A), |
---|
| 1123 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1124 | ∃tf. find_funct_ptr ? (globalenv p') b = Some ? tf /\ match_fun f tf. |
---|
| 1125 | Proof. |
---|
| 1126 | intros until f. destruct match_prog as [X [Y Z]]. |
---|
| 1127 | destruct (add_functs_match X) as [P [Q R]]. |
---|
| 1128 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
| 1129 | auto. |
---|
| 1130 | Qed. |
---|
| 1131 | |
---|
| 1132 | Theorem find_funct_ptr_rev_match: |
---|
| 1133 | forall (b: block) (tf: B), |
---|
| 1134 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 1135 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ match_fun f tf. |
---|
| 1136 | Proof. |
---|
| 1137 | intros until tf. destruct match_prog as [X [Y Z]]. |
---|
| 1138 | destruct (add_functs_rev_match X) as [P [Q R]]. |
---|
| 1139 | unfold find_funct_ptr. repeat rewrite functions_globalenv. |
---|
| 1140 | auto. |
---|
| 1141 | Qed. |
---|
| 1142 | |
---|
| 1143 | Theorem find_funct_match: |
---|
| 1144 | forall (v: val) (f: A), |
---|
| 1145 | find_funct (globalenv p) v = Some ? f → |
---|
| 1146 | ∃tf. find_funct (globalenv p') v = Some ? tf /\ match_fun f tf. |
---|
| 1147 | Proof. |
---|
| 1148 | intros until f. unfold find_funct. |
---|
| 1149 | case v; try (intros; discriminate). |
---|
| 1150 | intros b ofs. |
---|
| 1151 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
| 1152 | apply find_funct_ptr_match. |
---|
| 1153 | Qed. |
---|
| 1154 | |
---|
| 1155 | Theorem find_funct_rev_match: |
---|
| 1156 | forall (v: val) (tf: B), |
---|
| 1157 | find_funct (globalenv p') v = Some ? tf → |
---|
| 1158 | ∃f. find_funct (globalenv p) v = Some ? f /\ match_fun f tf. |
---|
| 1159 | Proof. |
---|
| 1160 | intros until tf. unfold find_funct. |
---|
| 1161 | case v; try (intros; discriminate). |
---|
| 1162 | intros b ofs. |
---|
| 1163 | case (Int.eq ofs Int.zero); try (intros; discriminate). |
---|
| 1164 | apply find_funct_ptr_rev_match. |
---|
| 1165 | Qed. |
---|
| 1166 | |
---|
| 1167 | Lemma symbols_init_match: |
---|
| 1168 | symbols (globalenv p') = symbols (globalenv p). |
---|
| 1169 | Proof. |
---|
| 1170 | unfold globalenv. unfold globalenv_initmem. |
---|
| 1171 | destruct match_prog as [X [Y Z]]. |
---|
| 1172 | destruct (add_functs_match X) as [P [Q R]]. |
---|
| 1173 | simpl. symmetry. apply symbols_add_globals_match. auto. auto. |
---|
| 1174 | Qed. |
---|
| 1175 | |
---|
| 1176 | Theorem find_symbol_match: |
---|
| 1177 | forall (s: ident), |
---|
| 1178 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 1179 | Proof. |
---|
| 1180 | intros. unfold find_symbol. |
---|
| 1181 | rewrite symbols_init_match. auto. |
---|
| 1182 | Qed. |
---|
| 1183 | |
---|
| 1184 | Theorem init_mem_match: |
---|
| 1185 | init_mem p' = init_mem p. |
---|
| 1186 | Proof. |
---|
| 1187 | unfold init_mem. unfold globalenv_initmem. |
---|
| 1188 | destruct match_prog as [X [Y Z]]. |
---|
| 1189 | symmetry. apply mem_add_globals_match. auto. |
---|
| 1190 | Qed. |
---|
| 1191 | |
---|
| 1192 | End MATCH_PROGRAM. |
---|
| 1193 | |
---|
| 1194 | Section TRANSF_PROGRAM_PARTIAL2. |
---|
| 1195 | |
---|
| 1196 | Variable A B V W: Type. |
---|
| 1197 | Variable transf_fun: A → res B. |
---|
| 1198 | Variable transf_var: V → res W. |
---|
| 1199 | Variable p: program A V. |
---|
| 1200 | Variable p': program B W. |
---|
| 1201 | Hypothesis transf_OK: |
---|
| 1202 | transform_partial_program2 transf_fun transf_var p = OK ? p'. |
---|
| 1203 | |
---|
| 1204 | Remark prog_match: |
---|
| 1205 | match_program |
---|
| 1206 | (fun fd tfd => transf_fun fd = OK ? tfd) |
---|
| 1207 | (fun info tinfo => transf_var info = OK ? tinfo) |
---|
| 1208 | p p'. |
---|
| 1209 | Proof. |
---|
| 1210 | apply transform_partial_program2_match; auto. |
---|
| 1211 | Qed. |
---|
| 1212 | |
---|
| 1213 | Theorem find_funct_ptr_transf_partial2: |
---|
| 1214 | forall (b: block) (f: A), |
---|
| 1215 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1216 | ∃f'. |
---|
| 1217 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf_fun f = OK ? f'. |
---|
| 1218 | Proof. |
---|
| 1219 | intros. |
---|
| 1220 | exploit find_funct_ptr_match. eexact prog_match. eauto. |
---|
| 1221 | intros [tf [X Y]]. exists tf; auto. |
---|
| 1222 | Qed. |
---|
| 1223 | |
---|
| 1224 | Theorem find_funct_ptr_rev_transf_partial2: |
---|
| 1225 | forall (b: block) (tf: B), |
---|
| 1226 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 1227 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf_fun f = OK ? tf. |
---|
| 1228 | Proof. |
---|
| 1229 | intros. |
---|
| 1230 | exploit find_funct_ptr_rev_match. eexact prog_match. eauto. auto. |
---|
| 1231 | Qed. |
---|
| 1232 | |
---|
| 1233 | Theorem find_funct_transf_partial2: |
---|
| 1234 | forall (v: val) (f: A), |
---|
| 1235 | find_funct (globalenv p) v = Some ? f → |
---|
| 1236 | ∃f'. |
---|
| 1237 | find_funct (globalenv p') v = Some ? f' /\ transf_fun f = OK ? f'. |
---|
| 1238 | Proof. |
---|
| 1239 | intros. |
---|
| 1240 | exploit find_funct_match. eexact prog_match. eauto. |
---|
| 1241 | intros [tf [X Y]]. exists tf; auto. |
---|
| 1242 | Qed. |
---|
| 1243 | |
---|
| 1244 | Theorem find_funct_rev_transf_partial2: |
---|
| 1245 | forall (v: val) (tf: B), |
---|
| 1246 | find_funct (globalenv p') v = Some ? tf → |
---|
| 1247 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf_fun f = OK ? tf. |
---|
| 1248 | Proof. |
---|
| 1249 | intros. |
---|
| 1250 | exploit find_funct_rev_match. eexact prog_match. eauto. auto. |
---|
| 1251 | Qed. |
---|
| 1252 | |
---|
| 1253 | Theorem find_symbol_transf_partial2: |
---|
| 1254 | forall (s: ident), |
---|
| 1255 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 1256 | Proof. |
---|
| 1257 | intros. eapply find_symbol_match. eexact prog_match. |
---|
| 1258 | Qed. |
---|
| 1259 | |
---|
| 1260 | Theorem init_mem_transf_partial2: |
---|
| 1261 | init_mem p' = init_mem p. |
---|
| 1262 | Proof. |
---|
| 1263 | intros. eapply init_mem_match. eexact prog_match. |
---|
| 1264 | Qed. |
---|
| 1265 | |
---|
| 1266 | End TRANSF_PROGRAM_PARTIAL2. |
---|
| 1267 | |
---|
| 1268 | Section TRANSF_PROGRAM_PARTIAL. |
---|
| 1269 | |
---|
| 1270 | Variable A B V: Type. |
---|
| 1271 | Variable transf: A → res B. |
---|
| 1272 | Variable p: program A V. |
---|
| 1273 | Variable p': program B V. |
---|
| 1274 | Hypothesis transf_OK: transform_partial_program transf p = OK ? p'. |
---|
| 1275 | |
---|
| 1276 | Remark transf2_OK: |
---|
| 1277 | transform_partial_program2 transf (fun x => OK ? x) p = OK ? p'. |
---|
| 1278 | Proof. |
---|
| 1279 | rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. |
---|
| 1280 | destruct (map_partial prefix_funct_name transf (prog_funct p)); auto. |
---|
| 1281 | rewrite map_partial_identity; auto. |
---|
| 1282 | Qed. |
---|
| 1283 | |
---|
| 1284 | Theorem find_funct_ptr_transf_partial: |
---|
| 1285 | forall (b: block) (f: A), |
---|
| 1286 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1287 | ∃f'. |
---|
| 1288 | find_funct_ptr ? (globalenv p') b = Some ? f' /\ transf f = OK ? f'. |
---|
| 1289 | Proof. |
---|
| 1290 | exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1291 | Qed. |
---|
| 1292 | |
---|
| 1293 | Theorem find_funct_ptr_rev_transf_partial: |
---|
| 1294 | forall (b: block) (tf: B), |
---|
| 1295 | find_funct_ptr ? (globalenv p') b = Some ? tf → |
---|
| 1296 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = OK ? tf. |
---|
| 1297 | Proof. |
---|
| 1298 | exact (@find_funct_ptr_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1299 | Qed. |
---|
| 1300 | |
---|
| 1301 | Theorem find_funct_transf_partial: |
---|
| 1302 | forall (v: val) (f: A), |
---|
| 1303 | find_funct (globalenv p) v = Some ? f → |
---|
| 1304 | ∃f'. |
---|
| 1305 | find_funct (globalenv p') v = Some ? f' /\ transf f = OK ? f'. |
---|
| 1306 | Proof. |
---|
| 1307 | exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1308 | Qed. |
---|
| 1309 | |
---|
| 1310 | Theorem find_funct_rev_transf_partial: |
---|
| 1311 | forall (v: val) (tf: B), |
---|
| 1312 | find_funct (globalenv p') v = Some ? tf → |
---|
| 1313 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = OK ? tf. |
---|
| 1314 | Proof. |
---|
| 1315 | exact (@find_funct_rev_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1316 | Qed. |
---|
| 1317 | |
---|
| 1318 | Theorem find_symbol_transf_partial: |
---|
| 1319 | forall (s: ident), |
---|
| 1320 | find_symbol ? (globalenv p') s = find_symbol ? (globalenv p) s. |
---|
| 1321 | Proof. |
---|
| 1322 | exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1323 | Qed. |
---|
| 1324 | |
---|
| 1325 | Theorem init_mem_transf_partial: |
---|
| 1326 | init_mem p' = init_mem p. |
---|
| 1327 | Proof. |
---|
| 1328 | exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). |
---|
| 1329 | Qed. |
---|
| 1330 | |
---|
| 1331 | End TRANSF_PROGRAM_PARTIAL. |
---|
| 1332 | |
---|
| 1333 | Section TRANSF_PROGRAM. |
---|
| 1334 | |
---|
| 1335 | Variable A B V: Type. |
---|
| 1336 | Variable transf: A → B. |
---|
| 1337 | Variable p: program A V. |
---|
| 1338 | Let tp := transform_program transf p. |
---|
| 1339 | |
---|
| 1340 | Remark transf_OK: |
---|
| 1341 | transform_partial_program (fun x => OK ? (transf x)) p = OK ? tp. |
---|
| 1342 | Proof. |
---|
| 1343 | unfold tp, transform_program, transform_partial_program. |
---|
| 1344 | rewrite map_partial_total. reflexivity. |
---|
| 1345 | Qed. |
---|
| 1346 | |
---|
| 1347 | Theorem find_funct_ptr_transf: |
---|
| 1348 | forall (b: block) (f: A), |
---|
| 1349 | find_funct_ptr ? (globalenv p) b = Some ? f → |
---|
| 1350 | find_funct_ptr ? (globalenv tp) b = Some ? (transf f). |
---|
| 1351 | Proof. |
---|
| 1352 | intros. |
---|
| 1353 | destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
| 1354 | as [f' [X Y]]. congruence. |
---|
| 1355 | Qed. |
---|
| 1356 | |
---|
| 1357 | Theorem find_funct_ptr_rev_transf: |
---|
| 1358 | forall (b: block) (tf: B), |
---|
| 1359 | find_funct_ptr ? (globalenv tp) b = Some ? tf → |
---|
| 1360 | ∃f. find_funct_ptr ? (globalenv p) b = Some ? f /\ transf f = tf. |
---|
| 1361 | Proof. |
---|
| 1362 | intros. exploit find_funct_ptr_rev_transf_partial. eexact transf_OK. eauto. |
---|
| 1363 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
| 1364 | Qed. |
---|
| 1365 | |
---|
| 1366 | Theorem find_funct_transf: |
---|
| 1367 | forall (v: val) (f: A), |
---|
| 1368 | find_funct (globalenv p) v = Some ? f → |
---|
| 1369 | find_funct (globalenv tp) v = Some ? (transf f). |
---|
| 1370 | Proof. |
---|
| 1371 | intros. |
---|
| 1372 | destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK ? _ _ H) |
---|
| 1373 | as [f' [X Y]]. congruence. |
---|
| 1374 | Qed. |
---|
| 1375 | |
---|
| 1376 | Theorem find_funct_rev_transf: |
---|
| 1377 | forall (v: val) (tf: B), |
---|
| 1378 | find_funct (globalenv tp) v = Some ? tf → |
---|
| 1379 | ∃f. find_funct (globalenv p) v = Some ? f /\ transf f = tf. |
---|
| 1380 | Proof. |
---|
| 1381 | intros. exploit find_funct_rev_transf_partial. eexact transf_OK. eauto. |
---|
| 1382 | intros [f [X Y]]. exists f; split. auto. congruence. |
---|
| 1383 | Qed. |
---|
| 1384 | |
---|
| 1385 | Theorem find_symbol_transf: |
---|
| 1386 | forall (s: ident), |
---|
| 1387 | find_symbol ? (globalenv tp) s = find_symbol ? (globalenv p) s. |
---|
| 1388 | Proof. |
---|
| 1389 | exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). |
---|
| 1390 | Qed. |
---|
| 1391 | |
---|
| 1392 | Theorem init_mem_transf: |
---|
| 1393 | init_mem tp = init_mem p. |
---|
| 1394 | Proof. |
---|
| 1395 | exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK). |
---|
| 1396 | Qed. |
---|
| 1397 | |
---|
| 1398 | End TRANSF_PROGRAM. |
---|
| 1399 | |
---|
| 1400 | End Genv. |
---|
| 1401 | *) |
---|
[485] | 1402 | |
---|