[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 | (* * Dynamic semantics for the Clight language *) |
---|
| 17 | |
---|
[474] | 18 | (*include "Coqlib.ma".*) |
---|
| 19 | (*include "Errors.ma".*) |
---|
| 20 | (*include "Integers.ma".*) |
---|
| 21 | (*include "Floats.ma".*) |
---|
| 22 | (*include "Values.ma".*) |
---|
| 23 | (*include "AST.ma".*) |
---|
| 24 | (*include "Mem.ma".*) |
---|
[700] | 25 | include "common/Globalenvs.ma". |
---|
| 26 | include "Clight/Csyntax.ma". |
---|
| 27 | include "common/Maps.ma". |
---|
[474] | 28 | (*include "Events.ma".*) |
---|
[700] | 29 | include "common/Smallstep.ma". |
---|
[3] | 30 | |
---|
| 31 | (* * * Semantics of type-dependent operations *) |
---|
| 32 | |
---|
| 33 | (* * Interpretation of values as truth values. |
---|
| 34 | Non-zero integers, non-zero floats and non-null pointers are |
---|
| 35 | considered as true. The integer zero (which also represents |
---|
| 36 | the null pointer) and the float 0.0 are false. *) |
---|
| 37 | |
---|
[487] | 38 | inductive is_false: val → type → Prop ≝ |
---|
[3] | 39 | | is_false_int: ∀sz,sg. |
---|
| 40 | is_false (Vint zero) (Tint sz sg) |
---|
[484] | 41 | | is_false_pointer: ∀r,r',t. |
---|
| 42 | is_false (Vnull r) (Tpointer r' t) |
---|
[3] | 43 | | is_false_float: ∀sz. |
---|
| 44 | is_false (Vfloat Fzero) (Tfloat sz). |
---|
| 45 | |
---|
[487] | 46 | inductive is_true: val → type → Prop ≝ |
---|
[3] | 47 | | is_true_int_int: ∀n,sz,sg. |
---|
| 48 | n ≠ zero → |
---|
| 49 | is_true (Vint n) (Tint sz sg) |
---|
[500] | 50 | | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t. |
---|
| 51 | is_true (Vptr r b pc ofs) (Tpointer s t) |
---|
[3] | 52 | | is_true_float: ∀f,sz. |
---|
| 53 | f ≠ Fzero → |
---|
| 54 | is_true (Vfloat f) (Tfloat sz). |
---|
| 55 | |
---|
[487] | 56 | inductive bool_of_val : val → type → val → Prop ≝ |
---|
[3] | 57 | | bool_of_val_true: ∀v,ty. |
---|
| 58 | is_true v ty → |
---|
| 59 | bool_of_val v ty Vtrue |
---|
| 60 | | bool_of_val_false: ∀v,ty. |
---|
| 61 | is_false v ty → |
---|
| 62 | bool_of_val v ty Vfalse. |
---|
| 63 | |
---|
| 64 | (* * The following [sem_] functions compute the result of an operator |
---|
| 65 | application. Since operators are overloaded, the result depends |
---|
| 66 | both on the static types of the arguments and on their run-time values. |
---|
| 67 | Unlike in C, automatic conversions between integers and floats |
---|
| 68 | are not performed. For instance, [e1 + e2] is undefined if [e1] |
---|
| 69 | is a float and [e2] an integer. The Clight producer must have explicitly |
---|
| 70 | promoted [e2] to a float. *) |
---|
| 71 | |
---|
[487] | 72 | let rec sem_neg (v: val) (ty: type) : option val ≝ |
---|
[3] | 73 | match ty with |
---|
| 74 | [ Tint _ _ ⇒ |
---|
| 75 | match v with |
---|
[648] | 76 | [ Vint n ⇒ Some ? (Vint (two_complement_negation wordsize n)) |
---|
| 77 | | _ ⇒ None ? |
---|
[3] | 78 | ] |
---|
| 79 | | Tfloat _ ⇒ |
---|
| 80 | match v with |
---|
| 81 | [ Vfloat f ⇒ Some ? (Vfloat (Fneg f)) |
---|
| 82 | | _ ⇒ None ? |
---|
| 83 | ] |
---|
| 84 | | _ ⇒ None ? |
---|
| 85 | ]. |
---|
| 86 | |
---|
[487] | 87 | let rec sem_notint (v: val) : option val ≝ |
---|
[3] | 88 | match v with |
---|
[582] | 89 | [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *) |
---|
[3] | 90 | | _ ⇒ None ? |
---|
| 91 | ]. |
---|
| 92 | |
---|
[487] | 93 | let rec sem_notbool (v: val) (ty: type) : option val ≝ |
---|
[3] | 94 | match ty with |
---|
| 95 | [ Tint _ _ ⇒ |
---|
| 96 | match v with |
---|
| 97 | [ Vint n ⇒ Some ? (of_bool (eq n zero)) |
---|
| 98 | | _ ⇒ None ? |
---|
| 99 | ] |
---|
[124] | 100 | | Tpointer _ _ ⇒ |
---|
[3] | 101 | match v with |
---|
[502] | 102 | [ Vptr _ _ _ _ ⇒ Some ? Vfalse |
---|
| 103 | | Vnull _ ⇒ Some ? Vtrue |
---|
[3] | 104 | | _ ⇒ None ? |
---|
| 105 | ] |
---|
| 106 | | Tfloat _ ⇒ |
---|
| 107 | match v with |
---|
| 108 | [ Vfloat f ⇒ Some ? (of_bool (Fcmp Ceq f Fzero)) |
---|
| 109 | | _ ⇒ None ? |
---|
| 110 | ] |
---|
| 111 | | _ ⇒ None ? |
---|
| 112 | ]. |
---|
| 113 | |
---|
[487] | 114 | let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 115 | match classify_add t1 t2 with |
---|
| 116 | [ add_case_ii ⇒ (**r integer addition *) |
---|
| 117 | match v1 with |
---|
| 118 | [ Vint n1 ⇒ match v2 with |
---|
[582] | 119 | [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2)) |
---|
[3] | 120 | | _ ⇒ None ? ] |
---|
| 121 | | _ ⇒ None ? ] |
---|
| 122 | | add_case_ff ⇒ (**r float addition *) |
---|
| 123 | match v1 with |
---|
| 124 | [ Vfloat n1 ⇒ match v2 with |
---|
| 125 | [ Vfloat n2 ⇒ Some ? (Vfloat (Fadd n1 n2)) |
---|
| 126 | | _ ⇒ None ? ] |
---|
| 127 | | _ ⇒ None ? ] |
---|
| 128 | | add_case_pi ty ⇒ (**r pointer plus integer *) |
---|
| 129 | match v1 with |
---|
[500] | 130 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
[583] | 131 | [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2))) |
---|
[3] | 132 | | _ ⇒ None ? ] |
---|
[484] | 133 | | Vnull r ⇒ match v2 with |
---|
| 134 | [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? |
---|
| 135 | | _ ⇒ None ? ] |
---|
[3] | 136 | | _ ⇒ None ? ] |
---|
| 137 | | add_case_ip ty ⇒ (**r integer plus pointer *) |
---|
| 138 | match v1 with |
---|
| 139 | [ Vint n1 ⇒ match v2 with |
---|
[583] | 140 | [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1))) |
---|
[3] | 141 | | _ ⇒ None ? ] |
---|
| 142 | | _ ⇒ None ? ] |
---|
| 143 | | add_default ⇒ None ? |
---|
| 144 | ]. |
---|
| 145 | |
---|
[487] | 146 | let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 147 | match classify_sub t1 t2 with |
---|
| 148 | [ sub_case_ii ⇒ (**r integer subtraction *) |
---|
| 149 | match v1 with |
---|
| 150 | [ Vint n1 ⇒ match v2 with |
---|
[582] | 151 | [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2)) |
---|
[3] | 152 | | _ ⇒ None ? ] |
---|
| 153 | | _ ⇒ None ? ] |
---|
| 154 | | sub_case_ff ⇒ (**r float subtraction *) |
---|
| 155 | match v1 with |
---|
| 156 | [ Vfloat f1 ⇒ match v2 with |
---|
| 157 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2)) |
---|
| 158 | | _ ⇒ None ? ] |
---|
| 159 | | _ ⇒ None ? ] |
---|
| 160 | | sub_case_pi ty ⇒ (**r pointer minus integer *) |
---|
| 161 | match v1 with |
---|
[500] | 162 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
[583] | 163 | [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2))) |
---|
[3] | 164 | | _ ⇒ None ? ] |
---|
| 165 | | _ ⇒ None ? ] |
---|
| 166 | | sub_case_pp ty ⇒ (**r pointer minus pointer *) |
---|
| 167 | match v1 with |
---|
[500] | 168 | [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with |
---|
| 169 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
[496] | 170 | if eq_block b1 b2 then |
---|
[3] | 171 | if eq (repr (sizeof ty)) zero then None ? |
---|
[583] | 172 | else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty)))) |
---|
[3] | 173 | else None ? |
---|
| 174 | | _ ⇒ None ? ] |
---|
[484] | 175 | | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ] |
---|
[3] | 176 | | _ ⇒ None ? ] |
---|
| 177 | | sub_default ⇒ None ? |
---|
| 178 | ]. |
---|
[124] | 179 | |
---|
[487] | 180 | let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 181 | match classify_mul t1 t2 with |
---|
| 182 | [ mul_case_ii ⇒ |
---|
| 183 | match v1 with |
---|
| 184 | [ Vint n1 ⇒ match v2 with |
---|
[717] | 185 | [ Vint n2 ⇒ Some ? (Vint (mul n1 n2)) |
---|
| 186 | (* [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*) |
---|
[3] | 187 | | _ ⇒ None ? ] |
---|
| 188 | | _ ⇒ None ? ] |
---|
| 189 | | mul_case_ff ⇒ |
---|
| 190 | match v1 with |
---|
| 191 | [ Vfloat f1 ⇒ match v2 with |
---|
| 192 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2)) |
---|
| 193 | | _ ⇒ None ? ] |
---|
| 194 | | _ ⇒ None ? ] |
---|
| 195 | | mul_default ⇒ |
---|
| 196 | None ? |
---|
| 197 | ]. |
---|
| 198 | |
---|
[487] | 199 | let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 200 | match classify_div t1 t2 with |
---|
| 201 | [ div_case_I32unsi ⇒ |
---|
| 202 | match v1 with |
---|
| 203 | [ Vint n1 ⇒ match v2 with |
---|
[638] | 204 | [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2)) |
---|
| 205 | (* [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*) |
---|
[3] | 206 | | _ ⇒ None ? ] |
---|
| 207 | | _ ⇒ None ? ] |
---|
| 208 | | div_case_ii ⇒ |
---|
| 209 | match v1 with |
---|
| 210 | [ Vint n1 ⇒ match v2 with |
---|
[638] | 211 | [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2)) |
---|
| 212 | (* [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*) |
---|
[3] | 213 | | _ ⇒ None ? ] |
---|
| 214 | | _ ⇒ None ? ] |
---|
| 215 | | div_case_ff ⇒ |
---|
| 216 | match v1 with |
---|
| 217 | [ Vfloat f1 ⇒ match v2 with |
---|
| 218 | [ Vfloat f2 ⇒ Some ? (Vfloat(Fdiv f1 f2)) |
---|
| 219 | | _ ⇒ None ? ] |
---|
| 220 | | _ ⇒ None ? ] |
---|
| 221 | | div_default ⇒ |
---|
| 222 | None ? |
---|
| 223 | ]. |
---|
| 224 | |
---|
[487] | 225 | let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 226 | match classify_mod t1 t2 with |
---|
| 227 | [ mod_case_I32unsi ⇒ |
---|
| 228 | match v1 with |
---|
| 229 | [ Vint n1 ⇒ match v2 with |
---|
[638] | 230 | [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2)) |
---|
| 231 | (* [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*) |
---|
[3] | 232 | | _ ⇒ None ? ] |
---|
| 233 | | _ ⇒ None ? ] |
---|
| 234 | | mod_case_ii ⇒ |
---|
| 235 | match v1 with |
---|
| 236 | [ Vint n1 ⇒ match v2 with |
---|
[638] | 237 | [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2)) |
---|
| 238 | (* [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*) |
---|
[3] | 239 | | _ ⇒ None ? ] |
---|
| 240 | | _ ⇒ None ? ] |
---|
| 241 | | mod_default ⇒ |
---|
| 242 | None ? |
---|
| 243 | ]. |
---|
| 244 | |
---|
[487] | 245 | let rec sem_and (v1,v2: val) : option val ≝ |
---|
[3] | 246 | match v1 with |
---|
| 247 | [ Vint n1 ⇒ match v2 with |
---|
[582] | 248 | [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2)) |
---|
[3] | 249 | | _ ⇒ None ? ] |
---|
| 250 | | _ ⇒ None ? |
---|
| 251 | ]. |
---|
| 252 | |
---|
[487] | 253 | let rec sem_or (v1,v2: val) : option val ≝ |
---|
[3] | 254 | match v1 with |
---|
| 255 | [ Vint n1 ⇒ match v2 with |
---|
[582] | 256 | [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2)) |
---|
[3] | 257 | | _ ⇒ None ? ] |
---|
| 258 | | _ ⇒ None ? |
---|
| 259 | ]. |
---|
| 260 | |
---|
[487] | 261 | let rec sem_xor (v1,v2: val) : option val ≝ |
---|
[3] | 262 | match v1 with |
---|
| 263 | [ Vint n1 ⇒ match v2 with |
---|
[582] | 264 | [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2)) |
---|
[3] | 265 | | _ ⇒ None ? ] |
---|
| 266 | | _ ⇒ None ? |
---|
| 267 | ]. |
---|
| 268 | |
---|
[487] | 269 | let rec sem_shl (v1,v2: val): option val ≝ |
---|
[3] | 270 | match v1 with |
---|
| 271 | [ Vint n1 ⇒ match v2 with |
---|
| 272 | [ Vint n2 ⇒ |
---|
| 273 | if ltu n2 iwordsize then Some ? (Vint(shl n1 n2)) else None ? |
---|
| 274 | | _ ⇒ None ? ] |
---|
| 275 | | _ ⇒ None ? ]. |
---|
| 276 | |
---|
[487] | 277 | let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ |
---|
[3] | 278 | match classify_shr t1 t2 with |
---|
| 279 | [ shr_case_I32unsi ⇒ |
---|
| 280 | match v1 with |
---|
| 281 | [ Vint n1 ⇒ match v2 with |
---|
| 282 | [ Vint n2 ⇒ |
---|
| 283 | if ltu n2 iwordsize then Some ? (Vint (shru n1 n2)) else None ? |
---|
| 284 | | _ ⇒ None ? ] |
---|
| 285 | | _ ⇒ None ? ] |
---|
| 286 | | shr_case_ii => |
---|
| 287 | match v1 with |
---|
| 288 | [ Vint n1 ⇒ match v2 with |
---|
| 289 | [ Vint n2 ⇒ |
---|
| 290 | if ltu n2 iwordsize then Some ? (Vint (shr n1 n2)) else None ? |
---|
| 291 | | _ ⇒ None ? ] |
---|
| 292 | | _ ⇒ None ? ] |
---|
| 293 | | shr_default ⇒ |
---|
| 294 | None ? |
---|
| 295 | ]. |
---|
| 296 | |
---|
[487] | 297 | let rec sem_cmp_mismatch (c: comparison): option val ≝ |
---|
[3] | 298 | match c with |
---|
| 299 | [ Ceq => Some ? Vfalse |
---|
| 300 | | Cne => Some ? Vtrue |
---|
| 301 | | _ => None ? |
---|
| 302 | ]. |
---|
| 303 | |
---|
[487] | 304 | let rec sem_cmp_match (c: comparison): option val ≝ |
---|
[484] | 305 | match c with |
---|
| 306 | [ Ceq => Some ? Vtrue |
---|
| 307 | | Cne => Some ? Vfalse |
---|
| 308 | | _ => None ? |
---|
| 309 | ]. |
---|
| 310 | |
---|
[487] | 311 | let rec sem_cmp (c:comparison) |
---|
[3] | 312 | (v1: val) (t1: type) (v2: val) (t2: type) |
---|
| 313 | (m: mem): option val ≝ |
---|
| 314 | match classify_cmp t1 t2 with |
---|
| 315 | [ cmp_case_I32unsi ⇒ |
---|
| 316 | match v1 with |
---|
| 317 | [ Vint n1 ⇒ match v2 with |
---|
| 318 | [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2)) |
---|
| 319 | | _ ⇒ None ? ] |
---|
| 320 | | _ ⇒ None ? ] |
---|
| 321 | | cmp_case_ipip ⇒ |
---|
| 322 | match v1 with |
---|
| 323 | [ Vint n1 ⇒ match v2 with |
---|
| 324 | [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) |
---|
| 325 | | _ ⇒ None ? |
---|
| 326 | ] |
---|
[500] | 327 | | Vptr r1 b1 p1 ofs1 ⇒ |
---|
[3] | 328 | match v2 with |
---|
[500] | 329 | [ Vptr r2 b2 p2 ofs2 ⇒ |
---|
[583] | 330 | if valid_pointer m r1 b1 ofs1 |
---|
| 331 | ∧ valid_pointer m r2 b2 ofs2 then |
---|
[496] | 332 | if eq_block b1 b2 |
---|
[583] | 333 | then Some ? (of_bool (cmp_offset c ofs1 ofs2)) |
---|
[3] | 334 | else sem_cmp_mismatch c |
---|
| 335 | else None ? |
---|
[484] | 336 | | Vnull r2 ⇒ sem_cmp_mismatch c |
---|
[3] | 337 | | _ ⇒ None ? ] |
---|
[484] | 338 | | Vnull r1 ⇒ |
---|
| 339 | match v2 with |
---|
[500] | 340 | [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c |
---|
[484] | 341 | | Vnull r2 ⇒ sem_cmp_match c |
---|
| 342 | | _ ⇒ None ? |
---|
| 343 | ] |
---|
[3] | 344 | | _ ⇒ None ? ] |
---|
| 345 | | cmp_case_ff ⇒ |
---|
| 346 | match v1 with |
---|
| 347 | [ Vfloat f1 ⇒ |
---|
| 348 | match v2 with |
---|
| 349 | [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2)) |
---|
| 350 | | _ ⇒ None ? ] |
---|
| 351 | | _ ⇒ None ? ] |
---|
| 352 | | cmp_default ⇒ None ? |
---|
| 353 | ]. |
---|
| 354 | |
---|
[487] | 355 | definition sem_unary_operation |
---|
[3] | 356 | : unary_operation → val → type → option val ≝ |
---|
| 357 | λop,v,ty. |
---|
| 358 | match op with |
---|
| 359 | [ Onotbool => sem_notbool v ty |
---|
| 360 | | Onotint => sem_notint v |
---|
| 361 | | Oneg => sem_neg v ty |
---|
| 362 | ]. |
---|
| 363 | |
---|
[487] | 364 | let rec sem_binary_operation |
---|
[3] | 365 | (op: binary_operation) |
---|
| 366 | (v1: val) (t1: type) (v2: val) (t2:type) |
---|
| 367 | (m: mem): option val ≝ |
---|
| 368 | match op with |
---|
| 369 | [ Oadd ⇒ sem_add v1 t1 v2 t2 |
---|
| 370 | | Osub ⇒ sem_sub v1 t1 v2 t2 |
---|
| 371 | | Omul ⇒ sem_mul v1 t1 v2 t2 |
---|
| 372 | | Omod ⇒ sem_mod v1 t1 v2 t2 |
---|
| 373 | | Odiv ⇒ sem_div v1 t1 v2 t2 |
---|
| 374 | | Oand ⇒ sem_and v1 v2 |
---|
| 375 | | Oor ⇒ sem_or v1 v2 |
---|
| 376 | | Oxor ⇒ sem_xor v1 v2 |
---|
| 377 | | Oshl ⇒ sem_shl v1 v2 |
---|
| 378 | | Oshr ⇒ sem_shr v1 t1 v2 t2 |
---|
| 379 | | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m |
---|
| 380 | | One ⇒ sem_cmp Cne v1 t1 v2 t2 m |
---|
| 381 | | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m |
---|
| 382 | | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m |
---|
| 383 | | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m |
---|
| 384 | | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m |
---|
| 385 | ]. |
---|
| 386 | |
---|
| 387 | (* * Semantic of casts. [cast v1 t1 t2 v2] holds if value [v1], |
---|
| 388 | viewed with static type [t1], can be cast to type [t2], |
---|
| 389 | resulting in value [v2]. *) |
---|
| 390 | |
---|
[487] | 391 | let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝ |
---|
[3] | 392 | match sz with |
---|
| 393 | [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i | Unsigned ⇒ zero_ext 8 i ] |
---|
| 394 | | I16 ⇒ match sg with [ Signed => sign_ext 16 i | Unsigned ⇒ zero_ext 16 i ] |
---|
| 395 | | I32 ⇒ i |
---|
| 396 | ]. |
---|
| 397 | |
---|
[487] | 398 | let rec cast_int_float (si : signedness) (i: int) : float ≝ |
---|
[3] | 399 | match si with |
---|
| 400 | [ Signed ⇒ floatofint i |
---|
| 401 | | Unsigned ⇒ floatofintu i |
---|
| 402 | ]. |
---|
| 403 | |
---|
[487] | 404 | let rec cast_float_int (si : signedness) (f: float) : int ≝ |
---|
[3] | 405 | match si with |
---|
| 406 | [ Signed ⇒ intoffloat f |
---|
| 407 | | Unsigned ⇒ intuoffloat f |
---|
| 408 | ]. |
---|
| 409 | |
---|
[487] | 410 | let rec cast_float_float (sz: floatsize) (f: float) : float ≝ |
---|
[3] | 411 | match sz with |
---|
| 412 | [ F32 ⇒ singleoffloat f |
---|
| 413 | | F64 ⇒ f |
---|
| 414 | ]. |
---|
| 415 | |
---|
[487] | 416 | inductive type_region : type → region → Prop ≝ |
---|
[484] | 417 | | type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s |
---|
| 418 | | type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s |
---|
[155] | 419 | (* XXX Is the following necessary? *) |
---|
[484] | 420 | | type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. |
---|
[124] | 421 | |
---|
[487] | 422 | inductive cast : mem → val → type → type → val → Prop ≝ |
---|
[124] | 423 | | cast_ii: ∀m,i,sz2,sz1,si1,si2. (**r int to int *) |
---|
| 424 | cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2) |
---|
[3] | 425 | (Vint (cast_int_int sz2 si2 i)) |
---|
[124] | 426 | | cast_fi: ∀m,f,sz1,sz2,si2. (**r float to int *) |
---|
| 427 | cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2) |
---|
[3] | 428 | (Vint (cast_int_int sz2 si2 (cast_float_int si2 f))) |
---|
[124] | 429 | | cast_if: ∀m,i,sz1,sz2,si1. (**r int to float *) |
---|
| 430 | cast m (Vint i) (Tint sz1 si1) (Tfloat sz2) |
---|
[3] | 431 | (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) |
---|
[124] | 432 | | cast_ff: ∀m,f,sz1,sz2. (**r float to float *) |
---|
| 433 | cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) |
---|
[3] | 434 | (Vfloat (cast_float_float sz2 f)) |
---|
[500] | 435 | | cast_pp: ∀m,r,r',ty,ty',b,pc,ofs. |
---|
[484] | 436 | type_region ty r → |
---|
| 437 | type_region ty' r' → |
---|
[500] | 438 | ∀pc':pointer_compat b r'. |
---|
| 439 | cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs) |
---|
[484] | 440 | | cast_ip_z: ∀m,sz,sg,ty',r. |
---|
| 441 | type_region ty' r → |
---|
| 442 | cast m (Vint zero) (Tint sz sg) ty' (Vnull r) |
---|
| 443 | | cast_pp_z: ∀m,ty,ty',r,r'. |
---|
| 444 | type_region ty r → |
---|
| 445 | type_region ty' r' → |
---|
| 446 | cast m (Vnull r) ty ty' (Vnull r'). |
---|
[127] | 447 | |
---|
[3] | 448 | (* * * Operational semantics *) |
---|
| 449 | |
---|
| 450 | (* * The semantics uses two environments. The global environment |
---|
| 451 | maps names of functions and global variables to memory block references, |
---|
| 452 | and function pointers to their definitions. (See module [Globalenvs].) *) |
---|
| 453 | |
---|
[725] | 454 | definition genv ≝ (genv_t Genv) clight_fundef. |
---|
[3] | 455 | |
---|
| 456 | (* * The local environment maps local variables to block references. |
---|
| 457 | The current value of the variable is stored in the associated memory |
---|
| 458 | block. *) |
---|
| 459 | |
---|
[487] | 460 | definition env ≝ (tree_t ? PTree) block. (* map variable -> location *) |
---|
[3] | 461 | |
---|
[487] | 462 | definition empty_env: env ≝ (empty …). |
---|
[3] | 463 | |
---|
| 464 | (* * [load_value_of_type ty m b ofs] computes the value of a datum |
---|
| 465 | of type [ty] residing in memory [m] at block [b], offset [ofs]. |
---|
| 466 | If the type [ty] indicates an access by value, the corresponding |
---|
| 467 | memory load is performed. If the type [ty] indicates an access by |
---|
| 468 | reference, the pointer [Vptr b ofs] is returned. *) |
---|
| 469 | |
---|
[583] | 470 | let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ |
---|
[3] | 471 | match access_mode ty with |
---|
[500] | 472 | [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs) |
---|
| 473 | | By_reference r ⇒ |
---|
| 474 | match pointer_compat_dec b r with |
---|
| 475 | [ inl p ⇒ Some ? (Vptr r b p ofs) |
---|
| 476 | | inr _ ⇒ None ? |
---|
| 477 | ] |
---|
[3] | 478 | | By_nothing ⇒ None ? |
---|
| 479 | ]. |
---|
[500] | 480 | cases b // |
---|
| 481 | qed. |
---|
[3] | 482 | |
---|
| 483 | (* * Symmetrically, [store_value_of_type ty m b ofs v] returns the |
---|
| 484 | memory state after storing the value [v] in the datum |
---|
| 485 | of type [ty] residing in memory [m] at block [b], offset [ofs]. |
---|
| 486 | This is allowed only if [ty] indicates an access by value. *) |
---|
| 487 | |
---|
[583] | 488 | let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ |
---|
[3] | 489 | match access_mode ty_dest with |
---|
[500] | 490 | [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v |
---|
[498] | 491 | | By_reference _ ⇒ None ? |
---|
[3] | 492 | | By_nothing ⇒ None ? |
---|
| 493 | ]. |
---|
[500] | 494 | cases loc // |
---|
| 495 | qed. |
---|
[3] | 496 | |
---|
| 497 | (* * Allocation of function-local variables. |
---|
| 498 | [alloc_variables e1 m1 vars e2 m2] allocates one memory block |
---|
| 499 | for each variable declared in [vars], and associates the variable |
---|
| 500 | name with this block. [e1] and [m1] are the initial local environment |
---|
| 501 | and memory state. [e2] and [m2] are the final local environment |
---|
| 502 | and memory state. *) |
---|
| 503 | |
---|
[487] | 504 | inductive alloc_variables: env → mem → |
---|
[3] | 505 | list (ident × type) → |
---|
| 506 | env → mem → Prop ≝ |
---|
| 507 | | alloc_variables_nil: |
---|
| 508 | ∀e,m. |
---|
| 509 | alloc_variables e m (nil ?) e m |
---|
| 510 | | alloc_variables_cons: |
---|
| 511 | ∀e,m,id,ty,vars,m1,b1,m2,e2. |
---|
[125] | 512 | alloc m 0 (sizeof ty) Any = 〈m1, b1〉 → |
---|
| 513 | alloc_variables (set … id b1 e) m1 vars e2 m2 → |
---|
[3] | 514 | alloc_variables e m (〈id, ty〉 :: vars) e2 m2. |
---|
| 515 | |
---|
| 516 | (* * Initialization of local variables that are parameters to a function. |
---|
| 517 | [bind_parameters e m1 params args m2] stores the values [args] |
---|
| 518 | in the memory blocks corresponding to the variables [params]. |
---|
| 519 | [m1] is the initial memory state and [m2] the final memory state. *) |
---|
| 520 | |
---|
[487] | 521 | inductive bind_parameters: env → |
---|
[3] | 522 | mem → list (ident × type) → list val → |
---|
| 523 | mem → Prop ≝ |
---|
| 524 | | bind_parameters_nil: |
---|
| 525 | ∀e,m. |
---|
| 526 | bind_parameters e m (nil ?) (nil ?) m |
---|
| 527 | | bind_parameters_cons: |
---|
[125] | 528 | ∀e,m,id,ty,params,v1,vl,b,m1,m2. |
---|
| 529 | get ??? id e = Some ? b → |
---|
[583] | 530 | store_value_of_type ty m b zero_offset v1 = Some ? m1 → |
---|
[3] | 531 | bind_parameters e m1 params vl m2 → |
---|
| 532 | bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. |
---|
| 533 | |
---|
| 534 | (* * Return the list of blocks in the codomain of [e]. *) |
---|
| 535 | |
---|
[487] | 536 | definition blocks_of_env : env → list block ≝ λe. |
---|
[125] | 537 | map ?? (λx. snd ?? x) (elements ??? e). |
---|
[3] | 538 | |
---|
| 539 | (* * Selection of the appropriate case of a [switch], given the value [n] |
---|
| 540 | of the selector expression. *) |
---|
| 541 | |
---|
[487] | 542 | let rec select_switch (n: int) (sl: labeled_statements) |
---|
[3] | 543 | on sl : labeled_statements ≝ |
---|
| 544 | match sl with |
---|
| 545 | [ LSdefault _ ⇒ sl |
---|
| 546 | | LScase c s sl' ⇒ if eq c n then sl else select_switch n sl' |
---|
| 547 | ]. |
---|
| 548 | |
---|
| 549 | (* * Turn a labeled statement into a sequence *) |
---|
| 550 | |
---|
[487] | 551 | let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝ |
---|
[3] | 552 | match sl with |
---|
| 553 | [ LSdefault s ⇒ s |
---|
| 554 | | LScase c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl') |
---|
| 555 | ]. |
---|
| 556 | |
---|
| 557 | (* |
---|
| 558 | Section SEMANTICS. |
---|
| 559 | |
---|
| 560 | Variable ge: genv. |
---|
| 561 | |
---|
| 562 | (** ** Evaluation of expressions *) |
---|
| 563 | |
---|
| 564 | Section EXPR. |
---|
| 565 | |
---|
| 566 | Variable e: env. |
---|
| 567 | Variable m: mem. |
---|
| 568 | *) |
---|
| 569 | (* * [eval_expr ge e m a v] defines the evaluation of expression [a] |
---|
| 570 | in r-value position. [v] is the value of the expression. |
---|
| 571 | [e] is the current environment and [m] is the current memory state. *) |
---|
| 572 | |
---|
[487] | 573 | inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ |
---|
[3] | 574 | | eval_Econst_int: ∀i,ty. |
---|
[175] | 575 | eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0 |
---|
[3] | 576 | | eval_Econst_float: ∀f,ty. |
---|
[175] | 577 | eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 |
---|
[498] | 578 | | eval_Elvalue: ∀a,ty,loc,ofs,v,tr. |
---|
| 579 | eval_lvalue ge e m (Expr a ty) loc ofs tr → |
---|
| 580 | load_value_of_type ty m loc ofs = Some ? v → |
---|
[175] | 581 | eval_expr ge e m (Expr a ty) v tr |
---|
[496] | 582 | | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr. |
---|
[498] | 583 | eval_lvalue ge e m a loc ofs tr → |
---|
[500] | 584 | ∀pc:pointer_compat loc r. |
---|
| 585 | eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr |
---|
[3] | 586 | | eval_Esizeof: ∀ty',ty. |
---|
[175] | 587 | eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0 |
---|
| 588 | | eval_Eunop: ∀op,a,ty,v1,v,tr. |
---|
| 589 | eval_expr ge e m a v1 tr → |
---|
| 590 | sem_unary_operation op v1 (typeof a) = Some ? v → |
---|
| 591 | eval_expr ge e m (Expr (Eunop op a) ty) v tr |
---|
| 592 | | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
| 593 | eval_expr ge e m a1 v1 tr1 → |
---|
| 594 | eval_expr ge e m a2 v2 tr2 → |
---|
| 595 | sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v → |
---|
| 596 | eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2) |
---|
| 597 | | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2. |
---|
| 598 | eval_expr ge e m a1 v1 tr1 → |
---|
| 599 | is_true v1 (typeof a1) → |
---|
| 600 | eval_expr ge e m a2 v2 tr2 → |
---|
| 601 | eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2) |
---|
| 602 | | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2. |
---|
| 603 | eval_expr ge e m a1 v1 tr1 → |
---|
| 604 | is_false v1 (typeof a1) → |
---|
| 605 | eval_expr ge e m a3 v3 tr2 → |
---|
| 606 | eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2) |
---|
| 607 | | eval_Eorbool_1: ∀a1,a2,ty,v1,tr. |
---|
| 608 | eval_expr ge e m a1 v1 tr → |
---|
| 609 | is_true v1 (typeof a1) → |
---|
| 610 | eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr |
---|
| 611 | | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
| 612 | eval_expr ge e m a1 v1 tr1 → |
---|
| 613 | is_false v1 (typeof a1) → |
---|
| 614 | eval_expr ge e m a2 v2 tr2 → |
---|
| 615 | bool_of_val v2 (typeof a2) v → |
---|
| 616 | eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2) |
---|
| 617 | | eval_Eandbool_1: ∀a1,a2,ty,v1,tr. |
---|
| 618 | eval_expr ge e m a1 v1 tr → |
---|
| 619 | is_false v1 (typeof a1) → |
---|
| 620 | eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr |
---|
| 621 | | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
| 622 | eval_expr ge e m a1 v1 tr1 → |
---|
| 623 | is_true v1 (typeof a1) → |
---|
| 624 | eval_expr ge e m a2 v2 tr2 → |
---|
| 625 | bool_of_val v2 (typeof a2) v → |
---|
| 626 | eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2) |
---|
| 627 | | eval_Ecast: ∀a,ty,ty',v1,v,tr. |
---|
| 628 | eval_expr ge e m a v1 tr → |
---|
| 629 | cast m v1 (typeof a) ty v → |
---|
| 630 | eval_expr ge e m (Expr (Ecast ty a) ty') v tr |
---|
| 631 | | eval_Ecost: ∀a,ty,v,l,tr. |
---|
| 632 | eval_expr ge e m a v tr → |
---|
| 633 | eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l) |
---|
[3] | 634 | |
---|
[496] | 635 | (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a] |
---|
[3] | 636 | in l-value position. The result is the memory location [b, ofs] |
---|
[496] | 637 | that contains the value of the expression [a]. The memory location should |
---|
| 638 | be representable in a pointer of region r. *) |
---|
[3] | 639 | |
---|
[583] | 640 | with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝ |
---|
[125] | 641 | | eval_Evar_local: ∀id,l,ty. |
---|
| 642 | (* XXX notation? e!id*) get ??? id e = Some ? l → |
---|
[583] | 643 | eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 |
---|
[498] | 644 | | eval_Evar_global: ∀id,l,ty. |
---|
[175] | 645 | (* XXX e!id *) get ??? id e = None ? → |
---|
[498] | 646 | find_symbol ?? ge id = Some ? l → |
---|
[583] | 647 | eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 |
---|
[500] | 648 | | eval_Ederef: ∀a,ty,r,l,p,ofs,tr. |
---|
| 649 | eval_expr ge e m a (Vptr r l p ofs) tr → |
---|
[498] | 650 | eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr |
---|
| 651 | (* Aside: note that each block of memory is entirely contained within one |
---|
| 652 | memory region; hence adding a field offset will not produce a location |
---|
| 653 | outside of the original location's region. *) |
---|
| 654 | | eval_Efield_struct: ∀a,i,ty,l,ofs,id,fList,delta,tr. |
---|
| 655 | eval_lvalue ge e m a l ofs tr → |
---|
[175] | 656 | typeof a = Tstruct id fList → |
---|
| 657 | field_offset i fList = OK ? delta → |
---|
[583] | 658 | eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr |
---|
[498] | 659 | | eval_Efield_union: ∀a,i,ty,l,ofs,id,fList,tr. |
---|
| 660 | eval_lvalue ge e m a l ofs tr → |
---|
[175] | 661 | typeof a = Tunion id fList → |
---|
[498] | 662 | eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr. |
---|
[3] | 663 | |
---|
[487] | 664 | let rec eval_expr_ind (ge:genv) (e:env) (m:mem) |
---|
[226] | 665 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
| 666 | (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) |
---|
| 667 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
[498] | 668 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
[500] | 669 | (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H)) |
---|
[226] | 670 | (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) |
---|
| 671 | (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) |
---|
| 672 | (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) |
---|
| 673 | (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) |
---|
| 674 | (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) |
---|
| 675 | (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
| 676 | (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
| 677 | (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
| 678 | (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
| 679 | (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) |
---|
| 680 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
| 681 | (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ |
---|
| 682 | match ev with |
---|
| 683 | [ eval_Econst_int i ty ⇒ eci i ty |
---|
| 684 | | eval_Econst_float f ty ⇒ ecF f ty |
---|
[498] | 685 | | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 |
---|
[500] | 686 | | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H |
---|
[226] | 687 | | eval_Esizeof ty' ty ⇒ esz ty' ty |
---|
| 688 | | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) |
---|
| 689 | | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2) |
---|
| 690 | | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) |
---|
| 691 | | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3) |
---|
| 692 | | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1) |
---|
| 693 | | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) |
---|
| 694 | | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1) |
---|
| 695 | | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) |
---|
| 696 | | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) |
---|
| 697 | | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H) |
---|
| 698 | ]. |
---|
| 699 | |
---|
[487] | 700 | inverter eval_expr_inv_ind for eval_expr : Prop. |
---|
[226] | 701 | |
---|
[487] | 702 | let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem) |
---|
[498] | 703 | (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
| 704 | (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H)) |
---|
| 705 | (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
[500] | 706 | (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) |
---|
[498] | 707 | (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) |
---|
| 708 | (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) |
---|
[583] | 709 | (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝ |
---|
[226] | 710 | match ev with |
---|
| 711 | [ eval_Evar_local id l ty H ⇒ lvl id l ty H |
---|
[498] | 712 | | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 |
---|
[500] | 713 | | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H |
---|
[498] | 714 | | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) |
---|
| 715 | | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) |
---|
[226] | 716 | ]. |
---|
| 717 | |
---|
[3] | 718 | (* |
---|
[226] | 719 | ninverter eval_lvalue_inv_ind for eval_lvalue : Prop. |
---|
| 720 | *) |
---|
| 721 | |
---|
[487] | 722 | definition eval_lvalue_inv_ind : |
---|
[226] | 723 | ∀x1: genv. |
---|
| 724 | ∀x2: env. |
---|
| 725 | ∀x3: mem. |
---|
| 726 | ∀x4: expr. |
---|
| 727 | ∀x6: block. |
---|
[583] | 728 | ∀x7: offset. |
---|
[226] | 729 | ∀x8: trace. |
---|
| 730 | ∀P: |
---|
| 731 | ∀_z1430: expr. |
---|
[583] | 732 | ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop. |
---|
[226] | 733 | ∀_H1: ?. |
---|
| 734 | ∀_H2: ?. |
---|
| 735 | ∀_H3: ?. |
---|
| 736 | ∀_H4: ?. |
---|
| 737 | ∀_H5: ?. |
---|
[498] | 738 | ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8. |
---|
| 739 | P x4 x6 x7 x8 |
---|
[226] | 740 | := |
---|
| 741 | (λx1:genv. |
---|
| 742 | (λx2:env. |
---|
| 743 | (λx3:mem. |
---|
| 744 | (λx4:expr. |
---|
| 745 | (λx6:block. |
---|
[583] | 746 | (λx7:offset. |
---|
[226] | 747 | (λx8:trace. |
---|
| 748 | (λP:∀_z1430: expr. |
---|
| 749 | ∀_z1428: block. |
---|
[583] | 750 | ∀_z1427: offset. ∀_z1426: trace. Prop. |
---|
[226] | 751 | (λH1:?. |
---|
| 752 | (λH2:?. |
---|
| 753 | (λH3:?. |
---|
| 754 | (λH4:?. |
---|
| 755 | (λH5:?. |
---|
[498] | 756 | (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8. |
---|
[226] | 757 | ((λHcut:∀z1435: eq expr x4 x4. |
---|
| 758 | ∀z1433: eq block x6 x6. |
---|
[583] | 759 | ∀z1432: eq offset x7 x7. |
---|
[226] | 760 | ∀z1431: eq trace x8 x8. |
---|
[498] | 761 | P x4 x6 x7 x8. |
---|
[226] | 762 | (Hcut (refl expr x4) |
---|
[498] | 763 | (refl block x6) |
---|
[583] | 764 | (refl offset x7) (refl trace x8))) |
---|
[498] | 765 | ?))))))))))))))). |
---|
| 766 | [ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm) |
---|
[487] | 767 | [ @H1 | @H2 | @H3 | @H4 | @H5 ] |
---|
| 768 | | *: skip |
---|
| 769 | ] qed. |
---|
[226] | 770 | |
---|
[487] | 771 | let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem) |
---|
[226] | 772 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
[498] | 773 | (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
[226] | 774 | (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) |
---|
| 775 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
[498] | 776 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
[500] | 777 | (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc)) |
---|
[226] | 778 | (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) |
---|
| 779 | (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) |
---|
| 780 | (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) |
---|
| 781 | (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) |
---|
| 782 | (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) |
---|
| 783 | (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
| 784 | (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
| 785 | (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
| 786 | (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
| 787 | (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) |
---|
| 788 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
[498] | 789 | (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) |
---|
| 790 | (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
[500] | 791 | (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) |
---|
[498] | 792 | (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) |
---|
| 793 | (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) |
---|
[226] | 794 | |
---|
| 795 | (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ |
---|
| 796 | match ev with |
---|
| 797 | [ eval_Econst_int i ty ⇒ eci i ty |
---|
| 798 | | eval_Econst_float f ty ⇒ ecF f ty |
---|
[498] | 799 | | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1) |
---|
[500] | 800 | | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H) |
---|
[226] | 801 | | eval_Esizeof ty' ty ⇒ esz ty' ty |
---|
| 802 | | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) |
---|
| 803 | | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2) |
---|
| 804 | | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) |
---|
| 805 | | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3) |
---|
| 806 | | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1) |
---|
| 807 | | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) |
---|
| 808 | | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1) |
---|
| 809 | | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) |
---|
| 810 | | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) |
---|
| 811 | | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H) |
---|
| 812 | ] |
---|
| 813 | and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem) |
---|
| 814 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
[498] | 815 | (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
[226] | 816 | (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) |
---|
| 817 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
[498] | 818 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
[500] | 819 | (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc)) |
---|
[226] | 820 | (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) |
---|
| 821 | (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) |
---|
| 822 | (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) |
---|
| 823 | (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) |
---|
| 824 | (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) |
---|
| 825 | (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
| 826 | (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
| 827 | (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) |
---|
| 828 | (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) |
---|
| 829 | (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) |
---|
| 830 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
[498] | 831 | (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) |
---|
| 832 | (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
[500] | 833 | (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) |
---|
[498] | 834 | (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) |
---|
| 835 | (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) |
---|
[583] | 836 | (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝ |
---|
[226] | 837 | match ev with |
---|
| 838 | [ eval_Evar_local id l ty H ⇒ lvl id l ty H |
---|
[498] | 839 | | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 |
---|
[500] | 840 | | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr r l pc ofs) tr H) |
---|
[498] | 841 | | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) |
---|
| 842 | | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) |
---|
[226] | 843 | ]. |
---|
| 844 | |
---|
[487] | 845 | definition combined_expr_lvalue_ind ≝ |
---|
[226] | 846 | λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. |
---|
| 847 | conj ?? |
---|
| 848 | (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu) |
---|
| 849 | (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu). |
---|
| 850 | |
---|
| 851 | (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] |
---|
| 852 | in l-value position. The result is the memory location [b, ofs] |
---|
| 853 | that contains the value of the expression [a]. *) |
---|
| 854 | |
---|
| 855 | (* |
---|
| 856 | Scheme eval_expr_ind22 := Minimality for eval_expr Sort Prop |
---|
[3] | 857 | with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop. |
---|
| 858 | *) |
---|
| 859 | |
---|
| 860 | (* * [eval_exprlist ge e m al vl] evaluates a list of r-value |
---|
| 861 | expressions [al] to their values [vl]. *) |
---|
| 862 | |
---|
[487] | 863 | inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ |
---|
[3] | 864 | | eval_Enil: |
---|
[175] | 865 | eval_exprlist ge e m (nil ?) (nil ?) E0 |
---|
| 866 | | eval_Econs: ∀a,bl,v,vl,tr1,tr2. |
---|
| 867 | eval_expr ge e m a v tr1 → |
---|
| 868 | eval_exprlist ge e m bl vl tr2 → |
---|
| 869 | eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2). |
---|
[3] | 870 | |
---|
| 871 | (*End EXPR.*) |
---|
| 872 | |
---|
| 873 | (* * ** Transition semantics for statements and functions *) |
---|
| 874 | |
---|
| 875 | (* * Continuations *) |
---|
| 876 | |
---|
[487] | 877 | inductive cont: Type[0] := |
---|
[3] | 878 | | Kstop: cont |
---|
| 879 | | Kseq: statement -> cont -> cont |
---|
| 880 | (**r [Kseq s2 k] = after [s1] in [s1;s2] *) |
---|
| 881 | | Kwhile: expr -> statement -> cont -> cont |
---|
| 882 | (**r [Kwhile e s k] = after [s] in [while (e) s] *) |
---|
| 883 | | Kdowhile: expr -> statement -> cont -> cont |
---|
| 884 | (**r [Kdowhile e s k] = after [s] in [do s while (e)] *) |
---|
| 885 | | Kfor2: expr -> statement -> statement -> cont -> cont |
---|
| 886 | (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) |
---|
| 887 | | Kfor3: expr -> statement -> statement -> cont -> cont |
---|
| 888 | (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) |
---|
| 889 | | Kswitch: cont -> cont |
---|
| 890 | (**r catches [break] statements arising out of [switch] *) |
---|
[583] | 891 | | Kcall: option (block × offset × type) -> (**r where to store result *) |
---|
| 892 | function -> (**r calling function *) |
---|
| 893 | env -> (**r local env of calling function *) |
---|
[3] | 894 | cont -> cont. |
---|
| 895 | |
---|
| 896 | (* * Pop continuation until a call or stop *) |
---|
| 897 | |
---|
[487] | 898 | let rec call_cont (k: cont) : cont := |
---|
[3] | 899 | match k with |
---|
| 900 | [ Kseq s k => call_cont k |
---|
| 901 | | Kwhile e s k => call_cont k |
---|
| 902 | | Kdowhile e s k => call_cont k |
---|
| 903 | | Kfor2 e2 e3 s k => call_cont k |
---|
| 904 | | Kfor3 e2 e3 s k => call_cont k |
---|
| 905 | | Kswitch k => call_cont k |
---|
| 906 | | _ => k |
---|
| 907 | ]. |
---|
| 908 | |
---|
[487] | 909 | definition is_call_cont : cont → Prop ≝ λk. |
---|
[3] | 910 | match k with |
---|
| 911 | [ Kstop => True |
---|
| 912 | | Kcall _ _ _ _ => True |
---|
| 913 | | _ => False |
---|
| 914 | ]. |
---|
| 915 | |
---|
| 916 | (* * States *) |
---|
| 917 | |
---|
[487] | 918 | inductive state: Type[0] := |
---|
[3] | 919 | | State: |
---|
| 920 | ∀f: function. |
---|
| 921 | ∀s: statement. |
---|
| 922 | ∀k: cont. |
---|
| 923 | ∀e: env. |
---|
| 924 | ∀m: mem. state |
---|
| 925 | | Callstate: |
---|
[725] | 926 | ∀fd: clight_fundef. |
---|
[3] | 927 | ∀args: list val. |
---|
| 928 | ∀k: cont. |
---|
| 929 | ∀m: mem. state |
---|
| 930 | | Returnstate: |
---|
| 931 | ∀res: val. |
---|
| 932 | ∀k: cont. |
---|
| 933 | ∀m: mem. state. |
---|
| 934 | |
---|
| 935 | (* * Find the statement and manufacture the continuation |
---|
| 936 | corresponding to a label *) |
---|
| 937 | |
---|
[487] | 938 | let rec find_label (lbl: label) (s: statement) (k: cont) |
---|
[3] | 939 | on s: option (statement × cont) := |
---|
| 940 | match s with |
---|
| 941 | [ Ssequence s1 s2 => |
---|
| 942 | match find_label lbl s1 (Kseq s2 k) with |
---|
| 943 | [ Some sk => Some ? sk |
---|
| 944 | | None => find_label lbl s2 k |
---|
| 945 | ] |
---|
| 946 | | Sifthenelse a s1 s2 => |
---|
| 947 | match find_label lbl s1 k with |
---|
| 948 | [ Some sk => Some ? sk |
---|
| 949 | | None => find_label lbl s2 k |
---|
| 950 | ] |
---|
| 951 | | Swhile a s1 => |
---|
| 952 | find_label lbl s1 (Kwhile a s1 k) |
---|
| 953 | | Sdowhile a s1 => |
---|
| 954 | find_label lbl s1 (Kdowhile a s1 k) |
---|
| 955 | | Sfor a1 a2 a3 s1 => |
---|
| 956 | match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with |
---|
| 957 | [ Some sk => Some ? sk |
---|
| 958 | | None => |
---|
| 959 | match find_label lbl s1 (Kfor2 a2 a3 s1 k) with |
---|
| 960 | [ Some sk => Some ? sk |
---|
| 961 | | None => find_label lbl a3 (Kfor3 a2 a3 s1 k) |
---|
| 962 | ] |
---|
| 963 | ] |
---|
| 964 | | Sswitch e sl => |
---|
| 965 | find_label_ls lbl sl (Kswitch k) |
---|
| 966 | | Slabel lbl' s' => |
---|
| 967 | match ident_eq lbl lbl' with |
---|
| 968 | [ inl _ ⇒ Some ? 〈s', k〉 |
---|
| 969 | | inr _ ⇒ find_label lbl s' k |
---|
| 970 | ] |
---|
| 971 | | _ => None ? |
---|
| 972 | ] |
---|
| 973 | |
---|
| 974 | and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) |
---|
| 975 | on sl: option (statement × cont) := |
---|
| 976 | match sl with |
---|
| 977 | [ LSdefault s => find_label lbl s k |
---|
| 978 | | LScase _ s sl' => |
---|
| 979 | match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with |
---|
| 980 | [ Some sk => Some ? sk |
---|
| 981 | | None => find_label_ls lbl sl' k |
---|
| 982 | ] |
---|
| 983 | ]. |
---|
| 984 | |
---|
| 985 | (* * Transition relation *) |
---|
| 986 | |
---|
[457] | 987 | (* Strip off outer pointer for use when comparing function types. *) |
---|
[487] | 988 | definition fun_typeof ≝ |
---|
[457] | 989 | λe. match typeof e with |
---|
| 990 | [ Tvoid ⇒ Tvoid |
---|
| 991 | | Tint a b ⇒ Tint a b |
---|
| 992 | | Tfloat a ⇒ Tfloat a |
---|
| 993 | | Tpointer _ ty ⇒ ty |
---|
| 994 | | Tarray a b c ⇒ Tarray a b c |
---|
| 995 | | Tfunction a b ⇒ Tfunction a b |
---|
| 996 | | Tstruct a b ⇒ Tstruct a b |
---|
| 997 | | Tunion a b ⇒ Tunion a b |
---|
[481] | 998 | | Tcomp_ptr a b ⇒ Tcomp_ptr a b |
---|
[457] | 999 | ]. |
---|
| 1000 | |
---|
[175] | 1001 | (* XXX: note that cost labels in exprs expose a particular eval order. *) |
---|
[3] | 1002 | |
---|
[487] | 1003 | inductive step (ge:genv) : state → trace → state → Prop ≝ |
---|
[175] | 1004 | |
---|
[498] | 1005 | | step_assign: ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2. |
---|
| 1006 | eval_lvalue ge e m a1 loc ofs tr1 → |
---|
[175] | 1007 | eval_expr ge e m a2 v2 tr2 → |
---|
[498] | 1008 | store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' → |
---|
[3] | 1009 | step ge (State f (Sassign a1 a2) k e m) |
---|
[175] | 1010 | (tr1⧺tr2) (State f Sskip k e m') |
---|
[3] | 1011 | |
---|
[175] | 1012 | | step_call_none: ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2. |
---|
| 1013 | eval_expr ge e m a vf tr1 → |
---|
| 1014 | eval_exprlist ge e m al vargs tr2 → |
---|
| 1015 | find_funct ?? ge vf = Some ? fd → |
---|
[457] | 1016 | type_of_fundef fd = fun_typeof a → |
---|
[3] | 1017 | step ge (State f (Scall (None ?) a al) k e m) |
---|
[175] | 1018 | (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m) |
---|
[3] | 1019 | |
---|
[498] | 1020 | | step_call_some: ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3. |
---|
| 1021 | eval_lvalue ge e m lhs loc ofs tr1 → |
---|
[175] | 1022 | eval_expr ge e m a vf tr2 → |
---|
| 1023 | eval_exprlist ge e m al vargs tr3 → |
---|
| 1024 | find_funct ?? ge vf = Some ? fd → |
---|
[457] | 1025 | type_of_fundef fd = fun_typeof a → |
---|
[3] | 1026 | step ge (State f (Scall (Some ? lhs) a al) k e m) |
---|
[498] | 1027 | (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m) |
---|
[3] | 1028 | |
---|
| 1029 | | step_seq: ∀f,s1,s2,k,e,m. |
---|
| 1030 | step ge (State f (Ssequence s1 s2) k e m) |
---|
| 1031 | E0 (State f s1 (Kseq s2 k) e m) |
---|
| 1032 | | step_skip_seq: ∀f,s,k,e,m. |
---|
| 1033 | step ge (State f Sskip (Kseq s k) e m) |
---|
| 1034 | E0 (State f s k e m) |
---|
| 1035 | | step_continue_seq: ∀f,s,k,e,m. |
---|
| 1036 | step ge (State f Scontinue (Kseq s k) e m) |
---|
| 1037 | E0 (State f Scontinue k e m) |
---|
| 1038 | | step_break_seq: ∀f,s,k,e,m. |
---|
| 1039 | step ge (State f Sbreak (Kseq s k) e m) |
---|
| 1040 | E0 (State f Sbreak k e m) |
---|
| 1041 | |
---|
[175] | 1042 | | step_ifthenelse_true: ∀f,a,s1,s2,k,e,m,v1,tr. |
---|
| 1043 | eval_expr ge e m a v1 tr → |
---|
| 1044 | is_true v1 (typeof a) → |
---|
[3] | 1045 | step ge (State f (Sifthenelse a s1 s2) k e m) |
---|
[175] | 1046 | tr (State f s1 k e m) |
---|
| 1047 | | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr. |
---|
| 1048 | eval_expr ge e m a v1 tr → |
---|
| 1049 | is_false v1 (typeof a) → |
---|
[3] | 1050 | step ge (State f (Sifthenelse a s1 s2) k e m) |
---|
[175] | 1051 | tr (State f s2 k e m) |
---|
[3] | 1052 | |
---|
[175] | 1053 | | step_while_false: ∀f,a,s,k,e,m,v,tr. |
---|
| 1054 | eval_expr ge e m a v tr → |
---|
| 1055 | is_false v (typeof a) → |
---|
[3] | 1056 | step ge (State f (Swhile a s) k e m) |
---|
[175] | 1057 | tr (State f Sskip k e m) |
---|
| 1058 | | step_while_true: ∀f,a,s,k,e,m,v,tr. |
---|
| 1059 | eval_expr ge e m a v tr → |
---|
| 1060 | is_true v (typeof a) → |
---|
[3] | 1061 | step ge (State f (Swhile a s) k e m) |
---|
[175] | 1062 | tr (State f s (Kwhile a s k) e m) |
---|
[3] | 1063 | | step_skip_or_continue_while: ∀f,x,a,s,k,e,m. |
---|
[175] | 1064 | x = Sskip ∨ x = Scontinue → |
---|
[3] | 1065 | step ge (State f x (Kwhile a s k) e m) |
---|
| 1066 | E0 (State f (Swhile a s) k e m) |
---|
| 1067 | | step_break_while: ∀f,a,s,k,e,m. |
---|
| 1068 | step ge (State f Sbreak (Kwhile a s k) e m) |
---|
| 1069 | E0 (State f Sskip k e m) |
---|
| 1070 | |
---|
| 1071 | | step_dowhile: ∀f,a,s,k,e,m. |
---|
| 1072 | step ge (State f (Sdowhile a s) k e m) |
---|
| 1073 | E0 (State f s (Kdowhile a s k) e m) |
---|
[175] | 1074 | | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr. |
---|
| 1075 | x = Sskip ∨ x = Scontinue → |
---|
| 1076 | eval_expr ge e m a v tr → |
---|
| 1077 | is_false v (typeof a) → |
---|
[3] | 1078 | step ge (State f x (Kdowhile a s k) e m) |
---|
[175] | 1079 | tr (State f Sskip k e m) |
---|
| 1080 | | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr. |
---|
| 1081 | x = Sskip ∨ x = Scontinue → |
---|
| 1082 | eval_expr ge e m a v tr → |
---|
| 1083 | is_true v (typeof a) → |
---|
[3] | 1084 | step ge (State f x (Kdowhile a s k) e m) |
---|
[175] | 1085 | tr (State f (Sdowhile a s) k e m) |
---|
[3] | 1086 | | step_break_dowhile: ∀f,a,s,k,e,m. |
---|
| 1087 | step ge (State f Sbreak (Kdowhile a s k) e m) |
---|
| 1088 | E0 (State f Sskip k e m) |
---|
| 1089 | |
---|
| 1090 | | step_for_start: ∀f,a1,a2,a3,s,k,e,m. |
---|
[175] | 1091 | a1 ≠ Sskip → |
---|
[3] | 1092 | step ge (State f (Sfor a1 a2 a3 s) k e m) |
---|
| 1093 | E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) |
---|
[175] | 1094 | | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr. |
---|
| 1095 | eval_expr ge e m a2 v tr → |
---|
| 1096 | is_false v (typeof a2) → |
---|
[3] | 1097 | step ge (State f (Sfor Sskip a2 a3 s) k e m) |
---|
[175] | 1098 | tr (State f Sskip k e m) |
---|
| 1099 | | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr. |
---|
| 1100 | eval_expr ge e m a2 v tr → |
---|
| 1101 | is_true v (typeof a2) → |
---|
[3] | 1102 | step ge (State f (Sfor Sskip a2 a3 s) k e m) |
---|
[175] | 1103 | tr (State f s (Kfor2 a2 a3 s k) e m) |
---|
[3] | 1104 | | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m. |
---|
[175] | 1105 | x = Sskip ∨ x = Scontinue → |
---|
[3] | 1106 | step ge (State f x (Kfor2 a2 a3 s k) e m) |
---|
| 1107 | E0 (State f a3 (Kfor3 a2 a3 s k) e m) |
---|
| 1108 | | step_break_for2: ∀f,a2,a3,s,k,e,m. |
---|
| 1109 | step ge (State f Sbreak (Kfor2 a2 a3 s k) e m) |
---|
| 1110 | E0 (State f Sskip k e m) |
---|
| 1111 | | step_skip_for3: ∀f,a2,a3,s,k,e,m. |
---|
| 1112 | step ge (State f Sskip (Kfor3 a2 a3 s k) e m) |
---|
| 1113 | E0 (State f (Sfor Sskip a2 a3 s) k e m) |
---|
| 1114 | |
---|
| 1115 | | step_return_0: ∀f,k,e,m. |
---|
[175] | 1116 | fn_return f = Tvoid → |
---|
[3] | 1117 | step ge (State f (Sreturn (None ?)) k e m) |
---|
| 1118 | E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))) |
---|
[175] | 1119 | | step_return_1: ∀f,a,k,e,m,v,tr. |
---|
| 1120 | fn_return f ≠ Tvoid → |
---|
| 1121 | eval_expr ge e m a v tr → |
---|
[3] | 1122 | step ge (State f (Sreturn (Some ? a)) k e m) |
---|
[175] | 1123 | tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e))) |
---|
[3] | 1124 | | step_skip_call: ∀f,k,e,m. |
---|
[175] | 1125 | is_call_cont k → |
---|
| 1126 | fn_return f = Tvoid → |
---|
[3] | 1127 | step ge (State f Sskip k e m) |
---|
| 1128 | E0 (Returnstate Vundef k (free_list m (blocks_of_env e))) |
---|
| 1129 | |
---|
[175] | 1130 | | step_switch: ∀f,a,sl,k,e,m,n,tr. |
---|
| 1131 | eval_expr ge e m a (Vint n) tr → |
---|
[3] | 1132 | step ge (State f (Sswitch a sl) k e m) |
---|
[175] | 1133 | tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m) |
---|
[3] | 1134 | | step_skip_break_switch: ∀f,x,k,e,m. |
---|
[175] | 1135 | x = Sskip ∨ x = Sbreak → |
---|
[3] | 1136 | step ge (State f x (Kswitch k) e m) |
---|
| 1137 | E0 (State f Sskip k e m) |
---|
| 1138 | | step_continue_switch: ∀f,k,e,m. |
---|
| 1139 | step ge (State f Scontinue (Kswitch k) e m) |
---|
| 1140 | E0 (State f Scontinue k e m) |
---|
| 1141 | |
---|
| 1142 | | step_label: ∀f,lbl,s,k,e,m. |
---|
| 1143 | step ge (State f (Slabel lbl s) k e m) |
---|
| 1144 | E0 (State f s k e m) |
---|
| 1145 | |
---|
| 1146 | | step_goto: ∀f,lbl,k,e,m,s',k'. |
---|
[175] | 1147 | find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 → |
---|
[3] | 1148 | step ge (State f (Sgoto lbl) k e m) |
---|
| 1149 | E0 (State f s' k' e m) |
---|
| 1150 | |
---|
| 1151 | | step_internal_function: ∀f,vargs,k,m,e,m1,m2. |
---|
[175] | 1152 | alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 → |
---|
| 1153 | bind_parameters e m1 (fn_params f) vargs m2 → |
---|
[725] | 1154 | step ge (Callstate (CL_Internal f) vargs k m) |
---|
[3] | 1155 | E0 (State f (fn_body f) k e m2) |
---|
| 1156 | |
---|
| 1157 | | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t. |
---|
[175] | 1158 | event_match (external_function id targs tres) vargs t vres → |
---|
[725] | 1159 | step ge (Callstate (CL_External id targs tres) vargs k m) |
---|
[3] | 1160 | t (Returnstate vres k m) |
---|
| 1161 | |
---|
| 1162 | | step_returnstate_0: ∀v,f,e,k,m. |
---|
| 1163 | step ge (Returnstate v (Kcall (None ?) f e k) m) |
---|
| 1164 | E0 (State f Sskip k e m) |
---|
| 1165 | |
---|
[498] | 1166 | | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty. |
---|
| 1167 | store_value_of_type ty m loc ofs v = Some ? m' → |
---|
| 1168 | step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m) |
---|
[175] | 1169 | E0 (State f Sskip k e m') |
---|
| 1170 | |
---|
| 1171 | | step_cost: ∀f,lbl,s,k,e,m. |
---|
| 1172 | step ge (State f (Scost lbl s) k e m) |
---|
| 1173 | (Echarge lbl) (State f s k e m). |
---|
[3] | 1174 | (* |
---|
| 1175 | (** * Alternate big-step semantics *) |
---|
| 1176 | |
---|
| 1177 | (** ** Big-step semantics for terminating statements and functions *) |
---|
| 1178 | |
---|
| 1179 | (** The execution of a statement produces an ``outcome'', indicating |
---|
| 1180 | how the execution terminated: either normally or prematurely |
---|
| 1181 | through the execution of a [break], [continue] or [return] statement. *) |
---|
| 1182 | |
---|
[487] | 1183 | inductive outcome: Type[0] := |
---|
[3] | 1184 | | Out_break: outcome (**r terminated by [break] *) |
---|
| 1185 | | Out_continue: outcome (**r terminated by [continue] *) |
---|
| 1186 | | Out_normal: outcome (**r terminated normally *) |
---|
| 1187 | | Out_return: option val -> outcome. (**r terminated by [return] *) |
---|
| 1188 | |
---|
[487] | 1189 | inductive out_normal_or_continue : outcome -> Prop := |
---|
[3] | 1190 | | Out_normal_or_continue_N: out_normal_or_continue Out_normal |
---|
| 1191 | | Out_normal_or_continue_C: out_normal_or_continue Out_continue. |
---|
| 1192 | |
---|
[487] | 1193 | inductive out_break_or_return : outcome -> outcome -> Prop := |
---|
[3] | 1194 | | Out_break_or_return_B: out_break_or_return Out_break Out_normal |
---|
| 1195 | | Out_break_or_return_R: ∀ov. |
---|
| 1196 | out_break_or_return (Out_return ov) (Out_return ov). |
---|
| 1197 | |
---|
| 1198 | Definition outcome_switch (out: outcome) : outcome := |
---|
| 1199 | match out with |
---|
| 1200 | | Out_break => Out_normal |
---|
| 1201 | | o => o |
---|
| 1202 | end. |
---|
| 1203 | |
---|
| 1204 | Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := |
---|
| 1205 | match out, t with |
---|
| 1206 | | Out_normal, Tvoid => v = Vundef |
---|
| 1207 | | Out_return None, Tvoid => v = Vundef |
---|
| 1208 | | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v |
---|
| 1209 | | _, _ => False |
---|
| 1210 | end. |
---|
| 1211 | |
---|
| 1212 | (** [exec_stmt ge e m1 s t m2 out] describes the execution of |
---|
| 1213 | the statement [s]. [out] is the outcome for this execution. |
---|
| 1214 | [m1] is the initial memory state, [m2] the final memory state. |
---|
| 1215 | [t] is the trace of input/output events performed during this |
---|
| 1216 | evaluation. *) |
---|
| 1217 | |
---|
[487] | 1218 | inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := |
---|
[3] | 1219 | | exec_Sskip: ∀e,m. |
---|
| 1220 | exec_stmt e m Sskip |
---|
| 1221 | E0 m Out_normal |
---|
| 1222 | | exec_Sassign: ∀e,m,a1,a2,loc,ofs,v2,m'. |
---|
| 1223 | eval_lvalue e m a1 loc ofs -> |
---|
| 1224 | eval_expr e m a2 v2 -> |
---|
| 1225 | store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> |
---|
| 1226 | exec_stmt e m (Sassign a1 a2) |
---|
| 1227 | E0 m' Out_normal |
---|
| 1228 | | exec_Scall_none: ∀e,m,a,al,vf,vargs,f,t,m',vres. |
---|
| 1229 | eval_expr e m a vf -> |
---|
| 1230 | eval_exprlist e m al vargs -> |
---|
| 1231 | Genv.find_funct ge vf = Some f -> |
---|
| 1232 | type_of_fundef f = typeof a -> |
---|
| 1233 | eval_funcall m f vargs t m' vres -> |
---|
| 1234 | exec_stmt e m (Scall None a al) |
---|
| 1235 | t m' Out_normal |
---|
| 1236 | | exec_Scall_some: ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t,m',vres,m''. |
---|
| 1237 | eval_lvalue e m lhs loc ofs -> |
---|
| 1238 | eval_expr e m a vf -> |
---|
| 1239 | eval_exprlist e m al vargs -> |
---|
| 1240 | Genv.find_funct ge vf = Some f -> |
---|
| 1241 | type_of_fundef f = typeof a -> |
---|
| 1242 | eval_funcall m f vargs t m' vres -> |
---|
| 1243 | store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' -> |
---|
| 1244 | exec_stmt e m (Scall (Some lhs) a al) |
---|
| 1245 | t m'' Out_normal |
---|
| 1246 | | exec_Sseq_1: ∀e,m,s1,s2,t1,m1,t2,m2,out. |
---|
| 1247 | exec_stmt e m s1 t1 m1 Out_normal -> |
---|
| 1248 | exec_stmt e m1 s2 t2 m2 out -> |
---|
| 1249 | exec_stmt e m (Ssequence s1 s2) |
---|
| 1250 | (t1 ** t2) m2 out |
---|
| 1251 | | exec_Sseq_2: ∀e,m,s1,s2,t1,m1,out. |
---|
| 1252 | exec_stmt e m s1 t1 m1 out -> |
---|
| 1253 | out <> Out_normal -> |
---|
| 1254 | exec_stmt e m (Ssequence s1 s2) |
---|
| 1255 | t1 m1 out |
---|
| 1256 | | exec_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t,m',out. |
---|
| 1257 | eval_expr e m a v1 -> |
---|
| 1258 | is_true v1 (typeof a) -> |
---|
| 1259 | exec_stmt e m s1 t m' out -> |
---|
| 1260 | exec_stmt e m (Sifthenelse a s1 s2) |
---|
| 1261 | t m' out |
---|
| 1262 | | exec_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t,m',out. |
---|
| 1263 | eval_expr e m a v1 -> |
---|
| 1264 | is_false v1 (typeof a) -> |
---|
| 1265 | exec_stmt e m s2 t m' out -> |
---|
| 1266 | exec_stmt e m (Sifthenelse a s1 s2) |
---|
| 1267 | t m' out |
---|
| 1268 | | exec_Sreturn_none: ∀e,m. |
---|
| 1269 | exec_stmt e m (Sreturn None) |
---|
| 1270 | E0 m (Out_return None) |
---|
| 1271 | | exec_Sreturn_some: ∀e,m,a,v. |
---|
| 1272 | eval_expr e m a v -> |
---|
| 1273 | exec_stmt e m (Sreturn (Some a)) |
---|
| 1274 | E0 m (Out_return (Some v)) |
---|
| 1275 | | exec_Sbreak: ∀e,m. |
---|
| 1276 | exec_stmt e m Sbreak |
---|
| 1277 | E0 m Out_break |
---|
| 1278 | | exec_Scontinue: ∀e,m. |
---|
| 1279 | exec_stmt e m Scontinue |
---|
| 1280 | E0 m Out_continue |
---|
| 1281 | | exec_Swhile_false: ∀e,m,a,s,v. |
---|
| 1282 | eval_expr e m a v -> |
---|
| 1283 | is_false v (typeof a) -> |
---|
| 1284 | exec_stmt e m (Swhile a s) |
---|
| 1285 | E0 m Out_normal |
---|
| 1286 | | exec_Swhile_stop: ∀e,m,a,v,s,t,m',out',out. |
---|
| 1287 | eval_expr e m a v -> |
---|
| 1288 | is_true v (typeof a) -> |
---|
| 1289 | exec_stmt e m s t m' out' -> |
---|
| 1290 | out_break_or_return out' out -> |
---|
| 1291 | exec_stmt e m (Swhile a s) |
---|
| 1292 | t m' out |
---|
| 1293 | | exec_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2,m2,out. |
---|
| 1294 | eval_expr e m a v -> |
---|
| 1295 | is_true v (typeof a) -> |
---|
| 1296 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1297 | out_normal_or_continue out1 -> |
---|
| 1298 | exec_stmt e m1 (Swhile a s) t2 m2 out -> |
---|
| 1299 | exec_stmt e m (Swhile a s) |
---|
| 1300 | (t1 ** t2) m2 out |
---|
| 1301 | | exec_Sdowhile_false: ∀e,m,s,a,t,m1,out1,v. |
---|
| 1302 | exec_stmt e m s t m1 out1 -> |
---|
| 1303 | out_normal_or_continue out1 -> |
---|
| 1304 | eval_expr e m1 a v -> |
---|
| 1305 | is_false v (typeof a) -> |
---|
| 1306 | exec_stmt e m (Sdowhile a s) |
---|
| 1307 | t m1 Out_normal |
---|
| 1308 | | exec_Sdowhile_stop: ∀e,m,s,a,t,m1,out1,out. |
---|
| 1309 | exec_stmt e m s t m1 out1 -> |
---|
| 1310 | out_break_or_return out1 out -> |
---|
| 1311 | exec_stmt e m (Sdowhile a s) |
---|
| 1312 | t m1 out |
---|
| 1313 | | exec_Sdowhile_loop: ∀e,m,s,a,m1,m2,t1,t2,out,out1,v. |
---|
| 1314 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1315 | out_normal_or_continue out1 -> |
---|
| 1316 | eval_expr e m1 a v -> |
---|
| 1317 | is_true v (typeof a) -> |
---|
| 1318 | exec_stmt e m1 (Sdowhile a s) t2 m2 out -> |
---|
| 1319 | exec_stmt e m (Sdowhile a s) |
---|
| 1320 | (t1 ** t2) m2 out |
---|
| 1321 | | exec_Sfor_start: ∀e,m,s,a1,a2,a3,out,m1,m2,t1,t2. |
---|
| 1322 | a1 <> Sskip -> |
---|
| 1323 | exec_stmt e m a1 t1 m1 Out_normal -> |
---|
| 1324 | exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> |
---|
| 1325 | exec_stmt e m (Sfor a1 a2 a3 s) |
---|
| 1326 | (t1 ** t2) m2 out |
---|
| 1327 | | exec_Sfor_false: ∀e,m,s,a2,a3,v. |
---|
| 1328 | eval_expr e m a2 v -> |
---|
| 1329 | is_false v (typeof a2) -> |
---|
| 1330 | exec_stmt e m (Sfor Sskip a2 a3 s) |
---|
| 1331 | E0 m Out_normal |
---|
| 1332 | | exec_Sfor_stop: ∀e,m,s,a2,a3,v,m1,t,out1,out. |
---|
| 1333 | eval_expr e m a2 v -> |
---|
| 1334 | is_true v (typeof a2) -> |
---|
| 1335 | exec_stmt e m s t m1 out1 -> |
---|
| 1336 | out_break_or_return out1 out -> |
---|
| 1337 | exec_stmt e m (Sfor Sskip a2 a3 s) |
---|
| 1338 | t m1 out |
---|
| 1339 | | exec_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,m3,t1,t2,t3,out1,out. |
---|
| 1340 | eval_expr e m a2 v -> |
---|
| 1341 | is_true v (typeof a2) -> |
---|
| 1342 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1343 | out_normal_or_continue out1 -> |
---|
| 1344 | exec_stmt e m1 a3 t2 m2 Out_normal -> |
---|
| 1345 | exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out -> |
---|
| 1346 | exec_stmt e m (Sfor Sskip a2 a3 s) |
---|
| 1347 | (t1 ** t2 ** t3) m3 out |
---|
| 1348 | | exec_Sswitch: ∀e,m,a,t,n,sl,m1,out. |
---|
| 1349 | eval_expr e m a (Vint n) -> |
---|
| 1350 | exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out -> |
---|
| 1351 | exec_stmt e m (Sswitch a sl) |
---|
| 1352 | t m1 (outcome_switch out) |
---|
| 1353 | |
---|
| 1354 | (** [eval_funcall m1 fd args t m2 res] describes the invocation of |
---|
| 1355 | function [fd] with arguments [args]. [res] is the value returned |
---|
| 1356 | by the call. *) |
---|
| 1357 | |
---|
| 1358 | with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := |
---|
| 1359 | | eval_funcall_internal: ∀m,f,vargs,t,e,m1,m2,m3,out,vres. |
---|
| 1360 | alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> |
---|
| 1361 | bind_parameters e m1 f.(fn_params) vargs m2 -> |
---|
| 1362 | exec_stmt e m2 f.(fn_body) t m3 out -> |
---|
| 1363 | outcome_result_value out f.(fn_return) vres -> |
---|
| 1364 | eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres |
---|
| 1365 | | eval_funcall_external: ∀m,id,targs,tres,vargs,t,vres. |
---|
| 1366 | event_match (external_function id targs tres) vargs t vres -> |
---|
| 1367 | eval_funcall m (External id targs tres) vargs t m vres. |
---|
| 1368 | |
---|
| 1369 | Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop |
---|
| 1370 | with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. |
---|
| 1371 | |
---|
| 1372 | (** ** Big-step semantics for diverging statements and functions *) |
---|
| 1373 | |
---|
| 1374 | (** Coinductive semantics for divergence. |
---|
| 1375 | [execinf_stmt ge e m s t] holds if the execution of statement [s] |
---|
| 1376 | diverges, i.e. loops infinitely. [t] is the possibly infinite |
---|
| 1377 | trace of observable events performed during the execution. *) |
---|
| 1378 | |
---|
[487] | 1379 | Coinductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := |
---|
[3] | 1380 | | execinf_Scall_none: ∀e,m,a,al,vf,vargs,f,t. |
---|
| 1381 | eval_expr e m a vf -> |
---|
| 1382 | eval_exprlist e m al vargs -> |
---|
| 1383 | Genv.find_funct ge vf = Some f -> |
---|
| 1384 | type_of_fundef f = typeof a -> |
---|
| 1385 | evalinf_funcall m f vargs t -> |
---|
| 1386 | execinf_stmt e m (Scall None a al) t |
---|
| 1387 | | execinf_Scall_some: ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t. |
---|
| 1388 | eval_lvalue e m lhs loc ofs -> |
---|
| 1389 | eval_expr e m a vf -> |
---|
| 1390 | eval_exprlist e m al vargs -> |
---|
| 1391 | Genv.find_funct ge vf = Some f -> |
---|
| 1392 | type_of_fundef f = typeof a -> |
---|
| 1393 | evalinf_funcall m f vargs t -> |
---|
| 1394 | execinf_stmt e m (Scall (Some lhs) a al) t |
---|
| 1395 | | execinf_Sseq_1: ∀e,m,s1,s2,t. |
---|
| 1396 | execinf_stmt e m s1 t -> |
---|
| 1397 | execinf_stmt e m (Ssequence s1 s2) t |
---|
| 1398 | | execinf_Sseq_2: ∀e,m,s1,s2,t1,m1,t2. |
---|
| 1399 | exec_stmt e m s1 t1 m1 Out_normal -> |
---|
| 1400 | execinf_stmt e m1 s2 t2 -> |
---|
| 1401 | execinf_stmt e m (Ssequence s1 s2) (t1 *** t2) |
---|
| 1402 | | execinf_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t. |
---|
| 1403 | eval_expr e m a v1 -> |
---|
| 1404 | is_true v1 (typeof a) -> |
---|
| 1405 | execinf_stmt e m s1 t -> |
---|
| 1406 | execinf_stmt e m (Sifthenelse a s1 s2) t |
---|
| 1407 | | execinf_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t. |
---|
| 1408 | eval_expr e m a v1 -> |
---|
| 1409 | is_false v1 (typeof a) -> |
---|
| 1410 | execinf_stmt e m s2 t -> |
---|
| 1411 | execinf_stmt e m (Sifthenelse a s1 s2) t |
---|
| 1412 | | execinf_Swhile_body: ∀e,m,a,v,s,t. |
---|
| 1413 | eval_expr e m a v -> |
---|
| 1414 | is_true v (typeof a) -> |
---|
| 1415 | execinf_stmt e m s t -> |
---|
| 1416 | execinf_stmt e m (Swhile a s) t |
---|
| 1417 | | execinf_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2. |
---|
| 1418 | eval_expr e m a v -> |
---|
| 1419 | is_true v (typeof a) -> |
---|
| 1420 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1421 | out_normal_or_continue out1 -> |
---|
| 1422 | execinf_stmt e m1 (Swhile a s) t2 -> |
---|
| 1423 | execinf_stmt e m (Swhile a s) (t1 *** t2) |
---|
| 1424 | | execinf_Sdowhile_body: ∀e,m,s,a,t. |
---|
| 1425 | execinf_stmt e m s t -> |
---|
| 1426 | execinf_stmt e m (Sdowhile a s) t |
---|
| 1427 | | execinf_Sdowhile_loop: ∀e,m,s,a,m1,t1,t2,out1,v. |
---|
| 1428 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1429 | out_normal_or_continue out1 -> |
---|
| 1430 | eval_expr e m1 a v -> |
---|
| 1431 | is_true v (typeof a) -> |
---|
| 1432 | execinf_stmt e m1 (Sdowhile a s) t2 -> |
---|
| 1433 | execinf_stmt e m (Sdowhile a s) (t1 *** t2) |
---|
| 1434 | | execinf_Sfor_start_1: ∀e,m,s,a1,a2,a3,t. |
---|
| 1435 | execinf_stmt e m a1 t -> |
---|
| 1436 | execinf_stmt e m (Sfor a1 a2 a3 s) t |
---|
| 1437 | | execinf_Sfor_start_2: ∀e,m,s,a1,a2,a3,m1,t1,t2. |
---|
| 1438 | a1 <> Sskip -> |
---|
| 1439 | exec_stmt e m a1 t1 m1 Out_normal -> |
---|
| 1440 | execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 -> |
---|
| 1441 | execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2) |
---|
| 1442 | | execinf_Sfor_body: ∀e,m,s,a2,a3,v,t. |
---|
| 1443 | eval_expr e m a2 v -> |
---|
| 1444 | is_true v (typeof a2) -> |
---|
| 1445 | execinf_stmt e m s t -> |
---|
| 1446 | execinf_stmt e m (Sfor Sskip a2 a3 s) t |
---|
| 1447 | | execinf_Sfor_next: ∀e,m,s,a2,a3,v,m1,t1,t2,out1. |
---|
| 1448 | eval_expr e m a2 v -> |
---|
| 1449 | is_true v (typeof a2) -> |
---|
| 1450 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1451 | out_normal_or_continue out1 -> |
---|
| 1452 | execinf_stmt e m1 a3 t2 -> |
---|
| 1453 | execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2) |
---|
| 1454 | | execinf_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,t1,t2,t3,out1. |
---|
| 1455 | eval_expr e m a2 v -> |
---|
| 1456 | is_true v (typeof a2) -> |
---|
| 1457 | exec_stmt e m s t1 m1 out1 -> |
---|
| 1458 | out_normal_or_continue out1 -> |
---|
| 1459 | exec_stmt e m1 a3 t2 m2 Out_normal -> |
---|
| 1460 | execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 -> |
---|
| 1461 | execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3) |
---|
| 1462 | | execinf_Sswitch: ∀e,m,a,t,n,sl. |
---|
| 1463 | eval_expr e m a (Vint n) -> |
---|
| 1464 | execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t -> |
---|
| 1465 | execinf_stmt e m (Sswitch a sl) t |
---|
| 1466 | |
---|
| 1467 | (** [evalinf_funcall ge m fd args t] holds if the invocation of function |
---|
| 1468 | [fd] on arguments [args] diverges, with observable trace [t]. *) |
---|
| 1469 | |
---|
| 1470 | with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := |
---|
| 1471 | | evalinf_funcall_internal: ∀m,f,vargs,t,e,m1,m2. |
---|
| 1472 | alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> |
---|
| 1473 | bind_parameters e m1 f.(fn_params) vargs m2 -> |
---|
| 1474 | execinf_stmt e m2 f.(fn_body) t -> |
---|
| 1475 | evalinf_funcall m (Internal f) vargs t. |
---|
| 1476 | |
---|
| 1477 | End SEMANTICS. |
---|
| 1478 | *) |
---|
| 1479 | (* * * Whole-program semantics *) |
---|
| 1480 | |
---|
| 1481 | (* * Execution of whole programs are described as sequences of transitions |
---|
| 1482 | from an initial state to a final state. An initial state is a [Callstate] |
---|
| 1483 | corresponding to the invocation of the ``main'' function of the program |
---|
| 1484 | without arguments and with an empty continuation. *) |
---|
| 1485 | |
---|
[487] | 1486 | inductive initial_state (p: clight_program): state -> Prop := |
---|
[485] | 1487 | | initial_state_intro: ∀b,f,ge,m0. |
---|
| 1488 | globalenv Genv ?? p = OK ? ge → |
---|
| 1489 | init_mem Genv ?? p = OK ? m0 → |
---|
[496] | 1490 | find_symbol ?? ge (prog_main ?? p) = Some ? b → |
---|
[485] | 1491 | find_funct_ptr ?? ge b = Some ? f → |
---|
[3] | 1492 | initial_state p (Callstate f (nil ?) Kstop m0). |
---|
| 1493 | |
---|
| 1494 | (* * A final state is a [Returnstate] with an empty continuation. *) |
---|
| 1495 | |
---|
[487] | 1496 | inductive final_state: state -> int -> Prop := |
---|
[3] | 1497 | | final_state_intro: ∀r,m. |
---|
| 1498 | final_state (Returnstate (Vint r) Kstop m) r. |
---|
| 1499 | |
---|
| 1500 | (* * Execution of a whole program: [exec_program p beh] |
---|
| 1501 | holds if the application of [p]'s main function to no arguments |
---|
| 1502 | in the initial memory state for [p] has [beh] as observable |
---|
| 1503 | behavior. *) |
---|
| 1504 | |
---|
[487] | 1505 | definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. |
---|
[485] | 1506 | ∀ge. globalenv ??? p = OK ? ge → |
---|
| 1507 | program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. |
---|
[3] | 1508 | (* |
---|
| 1509 | (** Big-step execution of a whole program. *) |
---|
| 1510 | |
---|
[487] | 1511 | inductive bigstep_program_terminates (p: program): trace -> int -> Prop := |
---|
[3] | 1512 | | bigstep_program_terminates_intro: ∀b,f,m1,t,r. |
---|
| 1513 | let ge := Genv.globalenv p in |
---|
| 1514 | let m0 := Genv.init_mem p in |
---|
| 1515 | Genv.find_symbol ge p.(prog_main) = Some b -> |
---|
| 1516 | Genv.find_funct_ptr ge b = Some f -> |
---|
| 1517 | eval_funcall ge m0 f nil t m1 (Vint r) -> |
---|
| 1518 | bigstep_program_terminates p t r. |
---|
| 1519 | |
---|
[487] | 1520 | inductive bigstep_program_diverges (p: program): traceinf -> Prop := |
---|
[3] | 1521 | | bigstep_program_diverges_intro: ∀b,f,t. |
---|
| 1522 | let ge := Genv.globalenv p in |
---|
| 1523 | let m0 := Genv.init_mem p in |
---|
| 1524 | Genv.find_symbol ge p.(prog_main) = Some b -> |
---|
| 1525 | Genv.find_funct_ptr ge b = Some f -> |
---|
| 1526 | evalinf_funcall ge m0 f nil t -> |
---|
| 1527 | bigstep_program_diverges p t. |
---|
| 1528 | |
---|
| 1529 | (** * Implication from big-step semantics to transition semantics *) |
---|
| 1530 | |
---|
| 1531 | Section BIGSTEP_TO_TRANSITIONS. |
---|
| 1532 | |
---|
| 1533 | Variable prog: program. |
---|
| 1534 | Let ge : genv := Genv.globalenv prog. |
---|
| 1535 | |
---|
| 1536 | Definition exec_stmt_eval_funcall_ind |
---|
| 1537 | (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop) |
---|
| 1538 | (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) := |
---|
| 1539 | fun a b c d e f g h i j k l m n o p q r s t u v w x y => |
---|
| 1540 | conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y) |
---|
| 1541 | (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). |
---|
| 1542 | |
---|
[487] | 1543 | inductive outcome_state_match |
---|
[3] | 1544 | (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := |
---|
| 1545 | | osm_normal: |
---|
| 1546 | outcome_state_match e m f k Out_normal (State f Sskip k e m) |
---|
| 1547 | | osm_break: |
---|
| 1548 | outcome_state_match e m f k Out_break (State f Sbreak k e m) |
---|
| 1549 | | osm_continue: |
---|
| 1550 | outcome_state_match e m f k Out_continue (State f Scontinue k e m) |
---|
| 1551 | | osm_return_none: ∀k'. |
---|
| 1552 | call_cont k' = call_cont k -> |
---|
| 1553 | outcome_state_match e m f k |
---|
| 1554 | (Out_return None) (State f (Sreturn None) k' e m) |
---|
| 1555 | | osm_return_some: ∀a,v,k'. |
---|
| 1556 | call_cont k' = call_cont k -> |
---|
| 1557 | eval_expr ge e m a v -> |
---|
| 1558 | outcome_state_match e m f k |
---|
| 1559 | (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m). |
---|
| 1560 | |
---|
| 1561 | Lemma is_call_cont_call_cont: |
---|
| 1562 | ∀k. is_call_cont k -> call_cont k = k. |
---|
| 1563 | Proof. |
---|
| 1564 | destruct k; simpl; intros; contradiction || auto. |
---|
| 1565 | Qed. |
---|
| 1566 | |
---|
| 1567 | Lemma exec_stmt_eval_funcall_steps: |
---|
| 1568 | (∀e,m,s,t,m',out. |
---|
| 1569 | exec_stmt ge e m s t m' out -> |
---|
| 1570 | ∀f,k. exists S, |
---|
| 1571 | star step ge (State f s k e m) t S |
---|
| 1572 | /\ outcome_state_match e m' f k out S) |
---|
| 1573 | /\ |
---|
| 1574 | (∀m,fd,args,t,m',res. |
---|
| 1575 | eval_funcall ge m fd args t m' res -> |
---|
| 1576 | ∀k. |
---|
| 1577 | is_call_cont k -> |
---|
| 1578 | star step ge (Callstate fd args k m) t (Returnstate res k m')). |
---|
| 1579 | Proof. |
---|
| 1580 | apply exec_stmt_eval_funcall_ind; intros. |
---|
| 1581 | |
---|
| 1582 | (* skip *) |
---|
| 1583 | econstructor; split. apply star_refl. constructor. |
---|
| 1584 | |
---|
| 1585 | (* assign *) |
---|
| 1586 | econstructor; split. apply star_one. econstructor; eauto. constructor. |
---|
| 1587 | |
---|
| 1588 | (* call none *) |
---|
| 1589 | econstructor; split. |
---|
| 1590 | eapply star_left. econstructor; eauto. |
---|
| 1591 | eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq. |
---|
| 1592 | constructor. |
---|
| 1593 | |
---|
| 1594 | (* call some *) |
---|
| 1595 | econstructor; split. |
---|
| 1596 | eapply star_left. econstructor; eauto. |
---|
| 1597 | eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq. |
---|
| 1598 | constructor. |
---|
| 1599 | |
---|
| 1600 | (* sequence 2 *) |
---|
| 1601 | destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1. |
---|
| 1602 | destruct (H2 f k) as [S2 [A2 B2]]. |
---|
| 1603 | econstructor; split. |
---|
| 1604 | eapply star_left. econstructor. |
---|
| 1605 | eapply star_trans. eexact A1. |
---|
| 1606 | eapply star_left. constructor. eexact A2. |
---|
| 1607 | reflexivity. reflexivity. traceEq. |
---|
| 1608 | auto. |
---|
| 1609 | |
---|
| 1610 | (* sequence 1 *) |
---|
| 1611 | destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. |
---|
| 1612 | set (S2 := |
---|
| 1613 | match out with |
---|
| 1614 | | Out_break => State f Sbreak k e m1 |
---|
| 1615 | | Out_continue => State f Scontinue k e m1 |
---|
| 1616 | | _ => S1 |
---|
| 1617 | end). |
---|
| 1618 | exists S2; split. |
---|
| 1619 | eapply star_left. econstructor. |
---|
| 1620 | eapply star_trans. eexact A1. |
---|
| 1621 | unfold S2; inv B1. |
---|
| 1622 | congruence. |
---|
| 1623 | apply star_one. apply step_break_seq. |
---|
| 1624 | apply star_one. apply step_continue_seq. |
---|
| 1625 | apply star_refl. |
---|
| 1626 | apply star_refl. |
---|
| 1627 | reflexivity. traceEq. |
---|
| 1628 | unfold S2; inv B1; congruence || econstructor; eauto. |
---|
| 1629 | |
---|
| 1630 | (* ifthenelse true *) |
---|
| 1631 | destruct (H2 f k) as [S1 [A1 B1]]. |
---|
| 1632 | exists S1; split. |
---|
| 1633 | eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq. |
---|
| 1634 | auto. |
---|
| 1635 | |
---|
| 1636 | (* ifthenelse false *) |
---|
| 1637 | destruct (H2 f k) as [S1 [A1 B1]]. |
---|
| 1638 | exists S1; split. |
---|
| 1639 | eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq. |
---|
| 1640 | auto. |
---|
| 1641 | |
---|
| 1642 | (* return none *) |
---|
| 1643 | econstructor; split. apply star_refl. constructor. auto. |
---|
| 1644 | |
---|
| 1645 | (* return some *) |
---|
| 1646 | econstructor; split. apply star_refl. econstructor; eauto. |
---|
| 1647 | |
---|
| 1648 | (* break *) |
---|
| 1649 | econstructor; split. apply star_refl. constructor. |
---|
| 1650 | |
---|
| 1651 | (* continue *) |
---|
| 1652 | econstructor; split. apply star_refl. constructor. |
---|
| 1653 | |
---|
| 1654 | (* while false *) |
---|
| 1655 | econstructor; split. |
---|
| 1656 | apply star_one. eapply step_while_false; eauto. |
---|
| 1657 | constructor. |
---|
| 1658 | |
---|
| 1659 | (* while stop *) |
---|
| 1660 | destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. |
---|
| 1661 | set (S2 := |
---|
| 1662 | match out' with |
---|
| 1663 | | Out_break => State f Sskip k e m' |
---|
| 1664 | | _ => S1 |
---|
| 1665 | end). |
---|
| 1666 | exists S2; split. |
---|
| 1667 | eapply star_left. eapply step_while_true; eauto. |
---|
| 1668 | eapply star_trans. eexact A1. |
---|
| 1669 | unfold S2. inversion H3; subst. |
---|
| 1670 | inv B1. apply star_one. constructor. |
---|
| 1671 | apply star_refl. |
---|
| 1672 | reflexivity. traceEq. |
---|
| 1673 | unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. |
---|
| 1674 | |
---|
| 1675 | (* while loop *) |
---|
| 1676 | destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. |
---|
| 1677 | destruct (H5 f k) as [S2 [A2 B2]]. |
---|
| 1678 | exists S2; split. |
---|
| 1679 | eapply star_left. eapply step_while_true; eauto. |
---|
| 1680 | eapply star_trans. eexact A1. |
---|
| 1681 | eapply star_left. |
---|
| 1682 | inv H3; inv B1; apply step_skip_or_continue_while; auto. |
---|
| 1683 | eexact A2. |
---|
| 1684 | reflexivity. reflexivity. traceEq. |
---|
| 1685 | auto. |
---|
| 1686 | |
---|
| 1687 | (* dowhile false *) |
---|
| 1688 | destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. |
---|
| 1689 | exists (State f Sskip k e m1); split. |
---|
| 1690 | eapply star_left. constructor. |
---|
| 1691 | eapply star_right. eexact A1. |
---|
| 1692 | inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto. |
---|
| 1693 | reflexivity. traceEq. |
---|
| 1694 | constructor. |
---|
| 1695 | |
---|
| 1696 | (* dowhile stop *) |
---|
| 1697 | destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. |
---|
| 1698 | set (S2 := |
---|
| 1699 | match out1 with |
---|
| 1700 | | Out_break => State f Sskip k e m1 |
---|
| 1701 | | _ => S1 |
---|
| 1702 | end). |
---|
| 1703 | exists S2; split. |
---|
| 1704 | eapply star_left. apply step_dowhile. |
---|
| 1705 | eapply star_trans. eexact A1. |
---|
| 1706 | unfold S2. inversion H1; subst. |
---|
| 1707 | inv B1. apply star_one. constructor. |
---|
| 1708 | apply star_refl. |
---|
| 1709 | reflexivity. traceEq. |
---|
| 1710 | unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. |
---|
| 1711 | |
---|
| 1712 | (* dowhile loop *) |
---|
| 1713 | destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. |
---|
| 1714 | destruct (H5 f k) as [S2 [A2 B2]]. |
---|
| 1715 | exists S2; split. |
---|
| 1716 | eapply star_left. apply step_dowhile. |
---|
| 1717 | eapply star_trans. eexact A1. |
---|
| 1718 | eapply star_left. |
---|
| 1719 | inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. |
---|
| 1720 | eexact A2. |
---|
| 1721 | reflexivity. reflexivity. traceEq. |
---|
| 1722 | auto. |
---|
| 1723 | |
---|
| 1724 | (* for start *) |
---|
| 1725 | destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1. |
---|
| 1726 | destruct (H3 f k) as [S2 [A2 B2]]. |
---|
| 1727 | exists S2; split. |
---|
| 1728 | eapply star_left. apply step_for_start; auto. |
---|
| 1729 | eapply star_trans. eexact A1. |
---|
| 1730 | eapply star_left. constructor. eexact A2. |
---|
| 1731 | reflexivity. reflexivity. traceEq. |
---|
| 1732 | auto. |
---|
| 1733 | |
---|
| 1734 | (* for false *) |
---|
| 1735 | econstructor; split. |
---|
| 1736 | eapply star_one. eapply step_for_false; eauto. |
---|
| 1737 | constructor. |
---|
| 1738 | |
---|
| 1739 | (* for stop *) |
---|
| 1740 | destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. |
---|
| 1741 | set (S2 := |
---|
| 1742 | match out1 with |
---|
| 1743 | | Out_break => State f Sskip k e m1 |
---|
| 1744 | | _ => S1 |
---|
| 1745 | end). |
---|
| 1746 | exists S2; split. |
---|
| 1747 | eapply star_left. eapply step_for_true; eauto. |
---|
| 1748 | eapply star_trans. eexact A1. |
---|
| 1749 | unfold S2. inversion H3; subst. |
---|
| 1750 | inv B1. apply star_one. constructor. |
---|
| 1751 | apply star_refl. |
---|
| 1752 | reflexivity. traceEq. |
---|
| 1753 | unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. |
---|
| 1754 | |
---|
| 1755 | (* for loop *) |
---|
| 1756 | destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. |
---|
| 1757 | destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2. |
---|
| 1758 | destruct (H7 f k) as [S3 [A3 B3]]. |
---|
| 1759 | exists S3; split. |
---|
| 1760 | eapply star_left. eapply step_for_true; eauto. |
---|
| 1761 | eapply star_trans. eexact A1. |
---|
| 1762 | eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1). |
---|
| 1763 | inv H3; inv B1. |
---|
| 1764 | apply star_one. constructor. auto. |
---|
| 1765 | apply star_one. constructor. auto. |
---|
| 1766 | eapply star_trans. eexact A2. |
---|
| 1767 | eapply star_left. constructor. |
---|
| 1768 | eexact A3. |
---|
| 1769 | reflexivity. reflexivity. reflexivity. reflexivity. traceEq. |
---|
| 1770 | auto. |
---|
| 1771 | |
---|
| 1772 | (* switch *) |
---|
| 1773 | destruct (H1 f (Kswitch k)) as [S1 [A1 B1]]. |
---|
| 1774 | set (S2 := |
---|
| 1775 | match out with |
---|
| 1776 | | Out_normal => State f Sskip k e m1 |
---|
| 1777 | | Out_break => State f Sskip k e m1 |
---|
| 1778 | | Out_continue => State f Scontinue k e m1 |
---|
| 1779 | | _ => S1 |
---|
| 1780 | end). |
---|
| 1781 | exists S2; split. |
---|
| 1782 | eapply star_left. eapply step_switch; eauto. |
---|
| 1783 | eapply star_trans. eexact A1. |
---|
| 1784 | unfold S2; inv B1. |
---|
| 1785 | apply star_one. constructor. auto. |
---|
| 1786 | apply star_one. constructor. auto. |
---|
| 1787 | apply star_one. constructor. |
---|
| 1788 | apply star_refl. |
---|
| 1789 | apply star_refl. |
---|
| 1790 | reflexivity. traceEq. |
---|
| 1791 | unfold S2. inv B1; simpl; econstructor; eauto. |
---|
| 1792 | |
---|
| 1793 | (* call internal *) |
---|
| 1794 | destruct (H2 f k) as [S1 [A1 B1]]. |
---|
| 1795 | eapply star_left. eapply step_internal_function; eauto. |
---|
| 1796 | eapply star_right. eexact A1. |
---|
| 1797 | inv B1; simpl in H3; try contradiction. |
---|
| 1798 | (* Out_normal *) |
---|
| 1799 | assert (fn_return f = Tvoid /\ vres = Vundef). |
---|
| 1800 | destruct (fn_return f); auto || contradiction. |
---|
| 1801 | destruct H5. subst vres. apply step_skip_call; auto. |
---|
| 1802 | (* Out_return None *) |
---|
| 1803 | assert (fn_return f = Tvoid /\ vres = Vundef). |
---|
| 1804 | destruct (fn_return f); auto || contradiction. |
---|
| 1805 | destruct H6. subst vres. |
---|
| 1806 | rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. |
---|
| 1807 | apply step_return_0; auto. |
---|
| 1808 | (* Out_return Some *) |
---|
| 1809 | destruct H3. subst vres. |
---|
| 1810 | rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. |
---|
| 1811 | eapply step_return_1; eauto. |
---|
| 1812 | reflexivity. traceEq. |
---|
| 1813 | |
---|
| 1814 | (* call external *) |
---|
| 1815 | apply star_one. apply step_external_function; auto. |
---|
| 1816 | Qed. |
---|
| 1817 | |
---|
| 1818 | Lemma exec_stmt_steps: |
---|
| 1819 | ∀e,m,s,t,m',out. |
---|
| 1820 | exec_stmt ge e m s t m' out -> |
---|
| 1821 | ∀f,k. exists S, |
---|
| 1822 | star step ge (State f s k e m) t S |
---|
| 1823 | /\ outcome_state_match e m' f k out S. |
---|
| 1824 | Proof (proj1 exec_stmt_eval_funcall_steps). |
---|
| 1825 | |
---|
| 1826 | Lemma eval_funcall_steps: |
---|
| 1827 | ∀m,fd,args,t,m',res. |
---|
| 1828 | eval_funcall ge m fd args t m' res -> |
---|
| 1829 | ∀k. |
---|
| 1830 | is_call_cont k -> |
---|
| 1831 | star step ge (Callstate fd args k m) t (Returnstate res k m'). |
---|
| 1832 | Proof (proj2 exec_stmt_eval_funcall_steps). |
---|
| 1833 | |
---|
| 1834 | Definition order (x y: unit) := False. |
---|
| 1835 | |
---|
| 1836 | Lemma evalinf_funcall_forever: |
---|
| 1837 | ∀m,fd,args,T,k. |
---|
| 1838 | evalinf_funcall ge m fd args T -> |
---|
| 1839 | forever_N step order ge tt (Callstate fd args k m) T. |
---|
| 1840 | Proof. |
---|
| 1841 | cofix CIH_FUN. |
---|
| 1842 | assert (∀e,m,s,T,f,k. |
---|
| 1843 | execinf_stmt ge e m s T -> |
---|
| 1844 | forever_N step order ge tt (State f s k e m) T). |
---|
| 1845 | cofix CIH_STMT. |
---|
| 1846 | intros. inv H. |
---|
| 1847 | |
---|
| 1848 | (* call none *) |
---|
| 1849 | eapply forever_N_plus. |
---|
| 1850 | apply plus_one. eapply step_call_none; eauto. |
---|
| 1851 | apply CIH_FUN. eauto. traceEq. |
---|
| 1852 | (* call some *) |
---|
| 1853 | eapply forever_N_plus. |
---|
| 1854 | apply plus_one. eapply step_call_some; eauto. |
---|
| 1855 | apply CIH_FUN. eauto. traceEq. |
---|
| 1856 | |
---|
| 1857 | (* seq 1 *) |
---|
| 1858 | eapply forever_N_plus. |
---|
| 1859 | apply plus_one. econstructor. |
---|
| 1860 | apply CIH_STMT; eauto. traceEq. |
---|
| 1861 | (* seq 2 *) |
---|
| 1862 | destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]. |
---|
| 1863 | inv B1. |
---|
| 1864 | eapply forever_N_plus. |
---|
| 1865 | eapply plus_left. constructor. eapply star_trans. eexact A1. |
---|
| 1866 | apply star_one. constructor. reflexivity. reflexivity. |
---|
| 1867 | apply CIH_STMT; eauto. traceEq. |
---|
| 1868 | |
---|
| 1869 | (* ifthenelse true *) |
---|
| 1870 | eapply forever_N_plus. |
---|
| 1871 | apply plus_one. eapply step_ifthenelse_true; eauto. |
---|
| 1872 | apply CIH_STMT; eauto. traceEq. |
---|
| 1873 | (* ifthenelse false *) |
---|
| 1874 | eapply forever_N_plus. |
---|
| 1875 | apply plus_one. eapply step_ifthenelse_false; eauto. |
---|
| 1876 | apply CIH_STMT; eauto. traceEq. |
---|
| 1877 | |
---|
| 1878 | (* while body *) |
---|
| 1879 | eapply forever_N_plus. |
---|
| 1880 | eapply plus_one. eapply step_while_true; eauto. |
---|
| 1881 | apply CIH_STMT; eauto. traceEq. |
---|
| 1882 | (* while loop *) |
---|
| 1883 | destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]]. |
---|
| 1884 | eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1). |
---|
| 1885 | eapply plus_left. eapply step_while_true; eauto. |
---|
| 1886 | eapply star_right. eexact A1. |
---|
| 1887 | inv H3; inv B1; apply step_skip_or_continue_while; auto. |
---|
| 1888 | reflexivity. reflexivity. |
---|
| 1889 | apply CIH_STMT; eauto. traceEq. |
---|
| 1890 | |
---|
| 1891 | (* dowhile body *) |
---|
| 1892 | eapply forever_N_plus. |
---|
| 1893 | eapply plus_one. eapply step_dowhile. |
---|
| 1894 | apply CIH_STMT; eauto. |
---|
| 1895 | traceEq. |
---|
| 1896 | |
---|
| 1897 | (* dowhile loop *) |
---|
| 1898 | destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]]. |
---|
| 1899 | eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1). |
---|
| 1900 | eapply plus_left. eapply step_dowhile. |
---|
| 1901 | eapply star_right. eexact A1. |
---|
| 1902 | inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. |
---|
| 1903 | reflexivity. reflexivity. |
---|
| 1904 | apply CIH_STMT. eauto. |
---|
| 1905 | traceEq. |
---|
| 1906 | |
---|
| 1907 | (* for start 1 *) |
---|
| 1908 | assert (a1 <> Sskip). red; intros; subst. inv H0. |
---|
| 1909 | eapply forever_N_plus. |
---|
| 1910 | eapply plus_one. apply step_for_start; auto. |
---|
| 1911 | apply CIH_STMT; eauto. |
---|
| 1912 | traceEq. |
---|
| 1913 | |
---|
| 1914 | (* for start 2 *) |
---|
| 1915 | destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]. |
---|
| 1916 | inv B1. |
---|
| 1917 | eapply forever_N_plus. |
---|
| 1918 | eapply plus_left. eapply step_for_start; eauto. |
---|
| 1919 | eapply star_right. eexact A1. |
---|
| 1920 | apply step_skip_seq. |
---|
| 1921 | reflexivity. reflexivity. |
---|
| 1922 | apply CIH_STMT; eauto. |
---|
| 1923 | traceEq. |
---|
| 1924 | |
---|
| 1925 | (* for body *) |
---|
| 1926 | eapply forever_N_plus. |
---|
| 1927 | apply plus_one. eapply step_for_true; eauto. |
---|
| 1928 | apply CIH_STMT; eauto. |
---|
| 1929 | traceEq. |
---|
| 1930 | |
---|
| 1931 | (* for next *) |
---|
| 1932 | destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. |
---|
| 1933 | eapply forever_N_plus. |
---|
| 1934 | eapply plus_left. eapply step_for_true; eauto. |
---|
| 1935 | eapply star_trans. eexact A1. |
---|
| 1936 | apply star_one. |
---|
| 1937 | inv H3; inv B1; apply step_skip_or_continue_for2; auto. |
---|
| 1938 | reflexivity. reflexivity. |
---|
| 1939 | apply CIH_STMT; eauto. |
---|
| 1940 | traceEq. |
---|
| 1941 | |
---|
| 1942 | (* for body *) |
---|
| 1943 | destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. |
---|
| 1944 | destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]]. |
---|
| 1945 | inv B2. |
---|
| 1946 | eapply forever_N_plus. |
---|
| 1947 | eapply plus_left. eapply step_for_true; eauto. |
---|
| 1948 | eapply star_trans. eexact A1. |
---|
| 1949 | eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto. |
---|
| 1950 | eapply star_right. eexact A2. |
---|
| 1951 | constructor. |
---|
| 1952 | reflexivity. reflexivity. reflexivity. reflexivity. |
---|
| 1953 | apply CIH_STMT; eauto. |
---|
| 1954 | traceEq. |
---|
| 1955 | |
---|
| 1956 | (* switch *) |
---|
| 1957 | eapply forever_N_plus. |
---|
| 1958 | eapply plus_one. eapply step_switch; eauto. |
---|
| 1959 | apply CIH_STMT; eauto. |
---|
| 1960 | traceEq. |
---|
| 1961 | |
---|
| 1962 | (* call internal *) |
---|
| 1963 | intros. inv H0. |
---|
| 1964 | eapply forever_N_plus. |
---|
| 1965 | eapply plus_one. econstructor; eauto. |
---|
| 1966 | apply H; eauto. |
---|
| 1967 | traceEq. |
---|
| 1968 | Qed. |
---|
| 1969 | |
---|
| 1970 | Theorem bigstep_program_terminates_exec: |
---|
| 1971 | ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). |
---|
| 1972 | Proof. |
---|
| 1973 | intros. inv H. unfold ge0, m0 in *. |
---|
| 1974 | econstructor. |
---|
| 1975 | econstructor. eauto. eauto. |
---|
| 1976 | apply eval_funcall_steps. eauto. red; auto. |
---|
| 1977 | econstructor. |
---|
| 1978 | Qed. |
---|
| 1979 | |
---|
| 1980 | Theorem bigstep_program_diverges_exec: |
---|
| 1981 | ∀T. bigstep_program_diverges prog T -> |
---|
| 1982 | exec_program prog (Reacts T) \/ |
---|
| 1983 | exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. |
---|
| 1984 | Proof. |
---|
| 1985 | intros. inv H. |
---|
| 1986 | set (st := Callstate f nil Kstop m0). |
---|
| 1987 | assert (forever step ge0 st T). |
---|
| 1988 | eapply forever_N_forever with (order := order). |
---|
| 1989 | red; intros. constructor; intros. red in H. elim H. |
---|
| 1990 | eapply evalinf_funcall_forever; eauto. |
---|
| 1991 | destruct (forever_silent_or_reactive _ _ _ _ _ _ H) |
---|
| 1992 | as [A | [t [s' [T' [B [C D]]]]]]. |
---|
| 1993 | left. econstructor. econstructor. eauto. eauto. auto. |
---|
| 1994 | right. exists t. split. |
---|
| 1995 | econstructor. econstructor; eauto. eauto. auto. |
---|
| 1996 | subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. |
---|
| 1997 | Qed. |
---|
| 1998 | |
---|
| 1999 | End BIGSTEP_TO_TRANSITIONS. |
---|
| 2000 | |
---|
| 2001 | |
---|
| 2002 | |
---|
| 2003 | *) |
---|
| 2004 | |
---|
| 2005 | |
---|