[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". |
---|
[474] | 27 | (*include "Events.ma".*) |
---|
[700] | 28 | include "common/Smallstep.ma". |
---|
[1872] | 29 | include "Clight/ClassifyOp.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. |
---|
[961] | 40 | is_false (Vint sz (zero ?)) (Tint sz sg) |
---|
[2176] | 41 | | is_false_pointer: ∀t. |
---|
| 42 | is_false Vnull (Tpointer t) |
---|
[3] | 43 | | is_false_float: ∀sz. |
---|
| 44 | is_false (Vfloat Fzero) (Tfloat sz). |
---|
| 45 | |
---|
[487] | 46 | inductive is_true: val → type → Prop ≝ |
---|
[961] | 47 | | is_true_int_int: ∀sz,sg,n. |
---|
| 48 | n ≠ (zero ?) → |
---|
| 49 | is_true (Vint sz n) (Tint sz sg) |
---|
[2176] | 50 | | is_true_pointer_pointer: ∀ptr,t. |
---|
| 51 | is_true (Vptr ptr) (Tpointer 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 |
---|
[961] | 74 | [ Tint sz _ ⇒ |
---|
[3] | 75 | match v with |
---|
[961] | 76 | [ Vint sz' n ⇒ if eq_intsize sz sz' |
---|
| 77 | then Some ? (Vint ? (two_complement_negation ? n)) |
---|
| 78 | else None ? |
---|
[648] | 79 | | _ ⇒ None ? |
---|
[3] | 80 | ] |
---|
| 81 | | Tfloat _ ⇒ |
---|
| 82 | match v with |
---|
| 83 | [ Vfloat f ⇒ Some ? (Vfloat (Fneg f)) |
---|
| 84 | | _ ⇒ None ? |
---|
| 85 | ] |
---|
| 86 | | _ ⇒ None ? |
---|
| 87 | ]. |
---|
| 88 | |
---|
[487] | 89 | let rec sem_notint (v: val) : option val ≝ |
---|
[3] | 90 | match v with |
---|
[961] | 91 | [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *) |
---|
[3] | 92 | | _ ⇒ None ? |
---|
| 93 | ]. |
---|
| 94 | |
---|
[487] | 95 | let rec sem_notbool (v: val) (ty: type) : option val ≝ |
---|
[3] | 96 | match ty with |
---|
[961] | 97 | [ Tint sz _ ⇒ |
---|
[3] | 98 | match v with |
---|
[961] | 99 | [ Vint sz' n ⇒ if eq_intsize sz sz' |
---|
| 100 | then Some ? (of_bool (eq_bv ? n (zero ?))) |
---|
| 101 | else None ? |
---|
[3] | 102 | | _ ⇒ None ? |
---|
| 103 | ] |
---|
[2176] | 104 | | Tpointer _ ⇒ |
---|
[3] | 105 | match v with |
---|
[1545] | 106 | [ Vptr _ ⇒ Some ? Vfalse |
---|
[2176] | 107 | | Vnull ⇒ Some ? Vtrue |
---|
[3] | 108 | | _ ⇒ None ? |
---|
| 109 | ] |
---|
| 110 | | Tfloat _ ⇒ |
---|
| 111 | match v with |
---|
| 112 | [ Vfloat f ⇒ Some ? (of_bool (Fcmp Ceq f Fzero)) |
---|
| 113 | | _ ⇒ None ? |
---|
| 114 | ] |
---|
| 115 | | _ ⇒ None ? |
---|
| 116 | ]. |
---|
| 117 | |
---|
[487] | 118 | let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 119 | match classify_add t1 t2 with |
---|
[1872] | 120 | [ add_case_ii _ _ ⇒ (**r integer addition *) |
---|
[3] | 121 | match v1 with |
---|
[961] | 122 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 123 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 124 | (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?) |
---|
[3] | 125 | | _ ⇒ None ? ] |
---|
| 126 | | _ ⇒ None ? ] |
---|
[1872] | 127 | | add_case_ff _ ⇒ (**r float addition *) |
---|
[3] | 128 | match v1 with |
---|
| 129 | [ Vfloat n1 ⇒ match v2 with |
---|
| 130 | [ Vfloat n2 ⇒ Some ? (Vfloat (Fadd n1 n2)) |
---|
| 131 | | _ ⇒ None ? ] |
---|
| 132 | | _ ⇒ None ? ] |
---|
[2176] | 133 | | add_case_pi _ ty _ _ ⇒ (**r pointer plus integer *) |
---|
[3] | 134 | match v1 with |
---|
[1545] | 135 | [ Vptr ptr1 ⇒ match v2 with |
---|
| 136 | [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2)) |
---|
[3] | 137 | | _ ⇒ None ? ] |
---|
[2176] | 138 | | Vnull ⇒ match v2 with |
---|
| 139 | [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? |
---|
[484] | 140 | | _ ⇒ None ? ] |
---|
[3] | 141 | | _ ⇒ None ? ] |
---|
[2176] | 142 | | add_case_ip _ _ _ ty ⇒ (**r integer plus pointer *) |
---|
[3] | 143 | match v1 with |
---|
[961] | 144 | [ Vint sz1 n1 ⇒ match v2 with |
---|
[1545] | 145 | [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1)) |
---|
[2176] | 146 | | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? |
---|
[3] | 147 | | _ ⇒ None ? ] |
---|
| 148 | | _ ⇒ None ? ] |
---|
[1872] | 149 | | add_default _ _ ⇒ None ? |
---|
[3] | 150 | ]. |
---|
| 151 | |
---|
[487] | 152 | let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[3] | 153 | match classify_sub t1 t2 with |
---|
[1872] | 154 | [ sub_case_ii _ _ ⇒ (**r integer subtraction *) |
---|
[3] | 155 | match v1 with |
---|
[961] | 156 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 157 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 158 | (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?) |
---|
[3] | 159 | | _ ⇒ None ? ] |
---|
| 160 | | _ ⇒ None ? ] |
---|
[1872] | 161 | | sub_case_ff _ ⇒ (**r float subtraction *) |
---|
[3] | 162 | match v1 with |
---|
| 163 | [ Vfloat f1 ⇒ match v2 with |
---|
| 164 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2)) |
---|
| 165 | | _ ⇒ None ? ] |
---|
| 166 | | _ ⇒ None ? ] |
---|
[2176] | 167 | | sub_case_pi _ ty _ _ ⇒ (**r pointer minus integer *) |
---|
[3] | 168 | match v1 with |
---|
[1545] | 169 | [ Vptr ptr1 ⇒ match v2 with |
---|
| 170 | [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2)) |
---|
[3] | 171 | | _ ⇒ None ? ] |
---|
[2176] | 172 | | Vnull ⇒ match v2 with |
---|
| 173 | [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? |
---|
[776] | 174 | | _ ⇒ None ? ] |
---|
[3] | 175 | | _ ⇒ None ? ] |
---|
[2176] | 176 | | sub_case_pp _ _ ty _ ⇒ (**r pointer minus pointer *) |
---|
[3] | 177 | match v1 with |
---|
[1545] | 178 | [ Vptr ptr1 ⇒ match v2 with |
---|
| 179 | [ Vptr ptr2 ⇒ |
---|
| 180 | if eq_block (pblock ptr1) (pblock ptr2) then |
---|
[961] | 181 | if eqb (sizeof ty) 0 then None ? |
---|
[1545] | 182 | else match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with |
---|
[744] | 183 | [ None ⇒ None ? |
---|
[961] | 184 | | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *) |
---|
[744] | 185 | ] |
---|
[3] | 186 | else None ? |
---|
| 187 | | _ ⇒ None ? ] |
---|
[2176] | 188 | | Vnull ⇒ match v2 with [ Vnull ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ] |
---|
[3] | 189 | | _ ⇒ None ? ] |
---|
[1872] | 190 | | sub_default _ _ ⇒ None ? |
---|
[3] | 191 | ]. |
---|
[124] | 192 | |
---|
[487] | 193 | let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[1872] | 194 | match classify_aop t1 t2 with |
---|
| 195 | [ aop_case_ii _ _ ⇒ |
---|
[3] | 196 | match v1 with |
---|
[961] | 197 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 198 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
[2177] | 199 | (λn1. Some ? (Vint sz2 (short_multiplication ? n1 n2))) (None ?) |
---|
[3] | 200 | | _ ⇒ None ? ] |
---|
| 201 | | _ ⇒ None ? ] |
---|
[1872] | 202 | | aop_case_ff _ ⇒ |
---|
[3] | 203 | match v1 with |
---|
| 204 | [ Vfloat f1 ⇒ match v2 with |
---|
| 205 | [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2)) |
---|
| 206 | | _ ⇒ None ? ] |
---|
| 207 | | _ ⇒ None ? ] |
---|
[1872] | 208 | | aop_default _ _ ⇒ |
---|
[3] | 209 | None ? |
---|
| 210 | ]. |
---|
| 211 | |
---|
[487] | 212 | let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[1872] | 213 | match classify_aop t1 t2 with |
---|
| 214 | [ aop_case_ii _ sg ⇒ |
---|
[3] | 215 | match v1 with |
---|
[961] | 216 | [ Vint sz1 n1 ⇒ match v2 with |
---|
[1872] | 217 | [ Vint sz2 n2 ⇒ |
---|
| 218 | match sg with |
---|
| 219 | [ Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
[961] | 220 | (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?) |
---|
[1872] | 221 | | Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 222 | (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?) |
---|
| 223 | ] |
---|
[3] | 224 | | _ ⇒ None ? ] |
---|
| 225 | | _ ⇒ None ? ] |
---|
[1872] | 226 | | aop_case_ff _ ⇒ |
---|
[3] | 227 | match v1 with |
---|
| 228 | [ Vfloat f1 ⇒ match v2 with |
---|
| 229 | [ Vfloat f2 ⇒ Some ? (Vfloat(Fdiv f1 f2)) |
---|
| 230 | | _ ⇒ None ? ] |
---|
| 231 | | _ ⇒ None ? ] |
---|
[1872] | 232 | | aop_default _ _ ⇒ |
---|
[3] | 233 | None ? |
---|
| 234 | ]. |
---|
| 235 | |
---|
[487] | 236 | let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ |
---|
[1872] | 237 | match classify_aop t1 t2 with |
---|
| 238 | [ aop_case_ii sz sg ⇒ |
---|
[3] | 239 | match v1 with |
---|
[961] | 240 | [ Vint sz1 n1 ⇒ match v2 with |
---|
[1872] | 241 | [ Vint sz2 n2 ⇒ |
---|
| 242 | match sg with |
---|
| 243 | [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
[961] | 244 | (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?) |
---|
[1872] | 245 | | Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 246 | (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?) |
---|
| 247 | ] |
---|
[3] | 248 | | _ ⇒ None ? ] |
---|
| 249 | | _ ⇒ None ? ] |
---|
[1872] | 250 | | _ ⇒ |
---|
[3] | 251 | None ? |
---|
| 252 | ]. |
---|
| 253 | |
---|
[487] | 254 | let rec sem_and (v1,v2: val) : option val ≝ |
---|
[3] | 255 | match v1 with |
---|
[961] | 256 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 257 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 258 | (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?) |
---|
[3] | 259 | | _ ⇒ None ? ] |
---|
| 260 | | _ ⇒ None ? |
---|
| 261 | ]. |
---|
| 262 | |
---|
[487] | 263 | let rec sem_or (v1,v2: val) : option val ≝ |
---|
[3] | 264 | match v1 with |
---|
[961] | 265 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 266 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 267 | (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?) |
---|
[3] | 268 | | _ ⇒ None ? ] |
---|
| 269 | | _ ⇒ None ? |
---|
| 270 | ]. |
---|
| 271 | |
---|
[487] | 272 | let rec sem_xor (v1,v2: val) : option val ≝ |
---|
[3] | 273 | match v1 with |
---|
[961] | 274 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 275 | [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 276 | (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?) |
---|
[3] | 277 | | _ ⇒ None ? ] |
---|
| 278 | | _ ⇒ None ? |
---|
| 279 | ]. |
---|
| 280 | |
---|
[487] | 281 | let rec sem_shl (v1,v2: val): option val ≝ |
---|
[3] | 282 | match v1 with |
---|
[961] | 283 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 284 | [ Vint sz2 n2 ⇒ |
---|
| 285 | if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) |
---|
| 286 | then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false)) |
---|
| 287 | else None ? |
---|
[3] | 288 | | _ ⇒ None ? ] |
---|
| 289 | | _ ⇒ None ? ]. |
---|
| 290 | |
---|
[487] | 291 | let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ |
---|
[1872] | 292 | match classify_aop t1 t2 with |
---|
| 293 | [ aop_case_ii _ sg ⇒ |
---|
[3] | 294 | match v1 with |
---|
[961] | 295 | [ Vint sz1 n1 ⇒ match v2 with |
---|
| 296 | [ Vint sz2 n2 ⇒ |
---|
[1872] | 297 | match sg with |
---|
| 298 | [ Unsigned ⇒ |
---|
[961] | 299 | if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) |
---|
| 300 | then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false)) |
---|
| 301 | else None ? |
---|
[1872] | 302 | | Signed ⇒ |
---|
[961] | 303 | if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) |
---|
| 304 | then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1))) |
---|
| 305 | else None ? |
---|
[1872] | 306 | ] |
---|
[3] | 307 | | _ ⇒ None ? ] |
---|
| 308 | | _ ⇒ None ? ] |
---|
[1872] | 309 | | _ ⇒ |
---|
[3] | 310 | None ? |
---|
| 311 | ]. |
---|
| 312 | |
---|
[487] | 313 | let rec sem_cmp_mismatch (c: comparison): option val ≝ |
---|
[3] | 314 | match c with |
---|
[1872] | 315 | [ Ceq ⇒ Some ? Vfalse |
---|
| 316 | | Cne ⇒ Some ? Vtrue |
---|
| 317 | | _ ⇒ None ? |
---|
[3] | 318 | ]. |
---|
| 319 | |
---|
[487] | 320 | let rec sem_cmp_match (c: comparison): option val ≝ |
---|
[484] | 321 | match c with |
---|
[1872] | 322 | [ Ceq ⇒ Some ? Vtrue |
---|
| 323 | | Cne ⇒ Some ? Vfalse |
---|
| 324 | | _ ⇒ None ? |
---|
[484] | 325 | ]. |
---|
| 326 | |
---|
[487] | 327 | let rec sem_cmp (c:comparison) |
---|
[3] | 328 | (v1: val) (t1: type) (v2: val) (t2: type) |
---|
[2263] | 329 | (m: mem) on m: option val ≝ |
---|
[3] | 330 | match classify_cmp t1 t2 with |
---|
[1872] | 331 | [ cmp_case_ii _ sg ⇒ |
---|
[3] | 332 | match v1 with |
---|
[961] | 333 | [ Vint sz1 n1 ⇒ match v2 with |
---|
[1872] | 334 | [ Vint sz2 n2 ⇒ |
---|
| 335 | match sg with |
---|
| 336 | [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
[961] | 337 | (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?) |
---|
[1872] | 338 | | Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 |
---|
| 339 | (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?) |
---|
| 340 | ] |
---|
[3] | 341 | | _ ⇒ None ? |
---|
| 342 | ] |
---|
[816] | 343 | | _ ⇒ None ? |
---|
| 344 | ] |
---|
[2176] | 345 | | cmp_case_pp _ _ ⇒ |
---|
[816] | 346 | match v1 with |
---|
[1545] | 347 | [ Vptr ptr1 ⇒ |
---|
[3] | 348 | match v2 with |
---|
[1545] | 349 | [ Vptr ptr2 ⇒ |
---|
| 350 | if valid_pointer m ptr1 |
---|
| 351 | ∧ valid_pointer m ptr2 then |
---|
| 352 | if eq_block (pblock ptr1) (pblock ptr2) |
---|
| 353 | then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2))) |
---|
[3] | 354 | else sem_cmp_mismatch c |
---|
| 355 | else None ? |
---|
[2176] | 356 | | Vnull ⇒ sem_cmp_mismatch c |
---|
[3] | 357 | | _ ⇒ None ? ] |
---|
[2176] | 358 | | Vnull ⇒ |
---|
[484] | 359 | match v2 with |
---|
[1545] | 360 | [ Vptr ptr2 ⇒ sem_cmp_mismatch c |
---|
[2176] | 361 | | Vnull ⇒ sem_cmp_match c |
---|
[484] | 362 | | _ ⇒ None ? |
---|
| 363 | ] |
---|
[3] | 364 | | _ ⇒ None ? ] |
---|
[1872] | 365 | | cmp_case_ff _ ⇒ |
---|
[3] | 366 | match v1 with |
---|
| 367 | [ Vfloat f1 ⇒ |
---|
| 368 | match v2 with |
---|
| 369 | [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2)) |
---|
| 370 | | _ ⇒ None ? ] |
---|
| 371 | | _ ⇒ None ? ] |
---|
[1872] | 372 | | cmp_default _ _ ⇒ None ? |
---|
[3] | 373 | ]. |
---|
| 374 | |
---|
[487] | 375 | definition sem_unary_operation |
---|
[3] | 376 | : unary_operation → val → type → option val ≝ |
---|
| 377 | λop,v,ty. |
---|
| 378 | match op with |
---|
| 379 | [ Onotbool => sem_notbool v ty |
---|
| 380 | | Onotint => sem_notint v |
---|
| 381 | | Oneg => sem_neg v ty |
---|
| 382 | ]. |
---|
| 383 | |
---|
[487] | 384 | let rec sem_binary_operation |
---|
[3] | 385 | (op: binary_operation) |
---|
| 386 | (v1: val) (t1: type) (v2: val) (t2:type) |
---|
| 387 | (m: mem): option val ≝ |
---|
| 388 | match op with |
---|
| 389 | [ Oadd ⇒ sem_add v1 t1 v2 t2 |
---|
| 390 | | Osub ⇒ sem_sub v1 t1 v2 t2 |
---|
| 391 | | Omul ⇒ sem_mul v1 t1 v2 t2 |
---|
| 392 | | Omod ⇒ sem_mod v1 t1 v2 t2 |
---|
| 393 | | Odiv ⇒ sem_div v1 t1 v2 t2 |
---|
| 394 | | Oand ⇒ sem_and v1 v2 |
---|
| 395 | | Oor ⇒ sem_or v1 v2 |
---|
| 396 | | Oxor ⇒ sem_xor v1 v2 |
---|
| 397 | | Oshl ⇒ sem_shl v1 v2 |
---|
| 398 | | Oshr ⇒ sem_shr v1 t1 v2 t2 |
---|
| 399 | | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m |
---|
| 400 | | One ⇒ sem_cmp Cne v1 t1 v2 t2 m |
---|
| 401 | | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m |
---|
| 402 | | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m |
---|
| 403 | | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m |
---|
| 404 | | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m |
---|
| 405 | ]. |
---|
| 406 | |
---|
| 407 | (* * Semantic of casts. [cast v1 t1 t2 v2] holds if value [v1], |
---|
| 408 | viewed with static type [t1], can be cast to type [t2], |
---|
| 409 | resulting in value [v2]. *) |
---|
| 410 | |
---|
[964] | 411 | let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize) (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝ |
---|
[961] | 412 | match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ]. |
---|
[3] | 413 | |
---|
[961] | 414 | let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝ |
---|
[3] | 415 | match si with |
---|
[961] | 416 | [ Signed ⇒ floatofint ? i |
---|
| 417 | | Unsigned ⇒ floatofintu ? i |
---|
[3] | 418 | ]. |
---|
| 419 | |
---|
[961] | 420 | let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz) ≝ |
---|
[3] | 421 | match si with |
---|
[961] | 422 | [ Signed ⇒ intoffloat ? f |
---|
| 423 | | Unsigned ⇒ intuoffloat ? f |
---|
[3] | 424 | ]. |
---|
| 425 | |
---|
[487] | 426 | let rec cast_float_float (sz: floatsize) (f: float) : float ≝ |
---|
[3] | 427 | match sz with |
---|
| 428 | [ F32 ⇒ singleoffloat f |
---|
| 429 | | F64 ⇒ f |
---|
| 430 | ]. |
---|
| 431 | |
---|
[2176] | 432 | (* Only for full 8051 memory spaces |
---|
[487] | 433 | inductive type_region : type → region → Prop ≝ |
---|
[484] | 434 | | type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s |
---|
| 435 | | type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s |
---|
[2176] | 436 | (* Is the following necessary? *) |
---|
[484] | 437 | | type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. |
---|
[2176] | 438 | *) |
---|
[124] | 439 | |
---|
[2176] | 440 | inductive type_ptr : type → Prop ≝ |
---|
| 441 | | type_pointer : ∀t. type_ptr (Tpointer t) |
---|
| 442 | | type_array : ∀t,n. type_ptr (Tarray t n) |
---|
| 443 | | type_fun : ∀tys,ty. type_ptr (Tfunction tys ty). |
---|
| 444 | |
---|
[487] | 445 | inductive cast : mem → val → type → type → val → Prop ≝ |
---|
[961] | 446 | | cast_ii: ∀m,sz2,sz1,si1,si2,i. (**r int to int *) |
---|
| 447 | cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2) |
---|
[964] | 448 | (Vint sz2 (cast_int_int sz1 si1 sz2 i)) |
---|
[124] | 449 | | cast_fi: ∀m,f,sz1,sz2,si2. (**r float to int *) |
---|
| 450 | cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2) |
---|
[961] | 451 | (Vint sz2 (cast_float_int sz2 si2 f)) |
---|
| 452 | | cast_if: ∀m,sz1,sz2,si1,i. (**r int to float *) |
---|
| 453 | cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2) |
---|
| 454 | (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i))) |
---|
[124] | 455 | | cast_ff: ∀m,f,sz1,sz2. (**r float to float *) |
---|
| 456 | cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) |
---|
[3] | 457 | (Vfloat (cast_float_float sz2 f)) |
---|
[2176] | 458 | | cast_pp: ∀m,ty,ty',ptr. |
---|
| 459 | (* type_region ty (ptype ptr) → |
---|
[484] | 460 | type_region ty' r' → |
---|
[1545] | 461 | ∀pc':pointer_compat (pblock ptr) r'. |
---|
[2176] | 462 | cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))*) |
---|
| 463 | type_ptr ty → |
---|
| 464 | type_ptr ty' → |
---|
| 465 | cast m (Vptr ptr) ty ty' (Vptr ptr) |
---|
| 466 | | cast_ip_z: ∀m,sz,sg,ty'. |
---|
| 467 | (* type_region ty' r →*) |
---|
| 468 | type_ptr ty' → |
---|
| 469 | cast m (Vint sz (zero ?)) (Tint sz sg) ty' Vnull |
---|
| 470 | | cast_pp_z: ∀m,ty,ty'. |
---|
| 471 | (* type_region ty r → |
---|
| 472 | type_region ty' r' →*) |
---|
| 473 | type_ptr ty → |
---|
| 474 | type_ptr ty' → |
---|
| 475 | cast m Vnull ty ty' Vnull. |
---|
[127] | 476 | |
---|
[3] | 477 | (* * * Operational semantics *) |
---|
| 478 | |
---|
| 479 | (* * The semantics uses two environments. The global environment |
---|
| 480 | maps names of functions and global variables to memory block references, |
---|
| 481 | and function pointers to their definitions. (See module [Globalenvs].) *) |
---|
| 482 | |
---|
[1986] | 483 | definition genv ≝ genv_t clight_fundef. |
---|
[3] | 484 | |
---|
| 485 | (* * The local environment maps local variables to block references. |
---|
| 486 | The current value of the variable is stored in the associated memory |
---|
| 487 | block. *) |
---|
| 488 | |
---|
[1058] | 489 | definition env ≝ identifier_map SymbolTag block. (* map variable -> location *) |
---|
[3] | 490 | |
---|
[1058] | 491 | definition empty_env: env ≝ (empty_map …). |
---|
[3] | 492 | |
---|
| 493 | (* * [load_value_of_type ty m b ofs] computes the value of a datum |
---|
| 494 | of type [ty] residing in memory [m] at block [b], offset [ofs]. |
---|
| 495 | If the type [ty] indicates an access by value, the corresponding |
---|
| 496 | memory load is performed. If the type [ty] indicates an access by |
---|
| 497 | reference, the pointer [Vptr b ofs] is returned. *) |
---|
| 498 | |
---|
[583] | 499 | let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ |
---|
[3] | 500 | match access_mode ty with |
---|
[2176] | 501 | [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer b ofs)) |
---|
| 502 | | By_reference ⇒ Some ? (Vptr (mk_pointer b ofs)) |
---|
| 503 | (* match pointer_compat_dec b r with |
---|
[1545] | 504 | [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs)) |
---|
[500] | 505 | | inr _ ⇒ None ? |
---|
[2176] | 506 | ]*) |
---|
[1872] | 507 | | By_nothing _ ⇒ None ? |
---|
[3] | 508 | ]. |
---|
[2176] | 509 | (*cases b // |
---|
| 510 | qed.*) |
---|
[3] | 511 | |
---|
| 512 | (* * Symmetrically, [store_value_of_type ty m b ofs v] returns the |
---|
| 513 | memory state after storing the value [v] in the datum |
---|
| 514 | of type [ty] residing in memory [m] at block [b], offset [ofs]. |
---|
| 515 | This is allowed only if [ty] indicates an access by value. *) |
---|
| 516 | |
---|
[583] | 517 | let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ |
---|
[3] | 518 | match access_mode ty_dest with |
---|
[2176] | 519 | [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer loc ofs)) v |
---|
| 520 | | By_reference ⇒ None ? |
---|
[1872] | 521 | | By_nothing _ ⇒ None ? |
---|
[3] | 522 | ]. |
---|
[2176] | 523 | (*cases loc // |
---|
| 524 | qed.*) |
---|
[3] | 525 | |
---|
| 526 | (* * Allocation of function-local variables. |
---|
| 527 | [alloc_variables e1 m1 vars e2 m2] allocates one memory block |
---|
| 528 | for each variable declared in [vars], and associates the variable |
---|
| 529 | name with this block. [e1] and [m1] are the initial local environment |
---|
| 530 | and memory state. [e2] and [m2] are the final local environment |
---|
| 531 | and memory state. *) |
---|
| 532 | |
---|
[487] | 533 | inductive alloc_variables: env → mem → |
---|
[3] | 534 | list (ident × type) → |
---|
| 535 | env → mem → Prop ≝ |
---|
| 536 | | alloc_variables_nil: |
---|
| 537 | ∀e,m. |
---|
| 538 | alloc_variables e m (nil ?) e m |
---|
| 539 | | alloc_variables_cons: |
---|
| 540 | ∀e,m,id,ty,vars,m1,b1,m2,e2. |
---|
[2176] | 541 | alloc m 0 (sizeof ty) XData = 〈m1, b1〉 → |
---|
[1874] | 542 | alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 → |
---|
[3] | 543 | alloc_variables e m (〈id, ty〉 :: vars) e2 m2. |
---|
| 544 | |
---|
| 545 | (* * Initialization of local variables that are parameters to a function. |
---|
| 546 | [bind_parameters e m1 params args m2] stores the values [args] |
---|
| 547 | in the memory blocks corresponding to the variables [params]. |
---|
| 548 | [m1] is the initial memory state and [m2] the final memory state. *) |
---|
| 549 | |
---|
[487] | 550 | inductive bind_parameters: env → |
---|
[3] | 551 | mem → list (ident × type) → list val → |
---|
| 552 | mem → Prop ≝ |
---|
| 553 | | bind_parameters_nil: |
---|
| 554 | ∀e,m. |
---|
| 555 | bind_parameters e m (nil ?) (nil ?) m |
---|
| 556 | | bind_parameters_cons: |
---|
[125] | 557 | ∀e,m,id,ty,params,v1,vl,b,m1,m2. |
---|
[1058] | 558 | lookup ?? e id = Some ? b → |
---|
[583] | 559 | store_value_of_type ty m b zero_offset v1 = Some ? m1 → |
---|
[3] | 560 | bind_parameters e m1 params vl m2 → |
---|
| 561 | bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. |
---|
| 562 | |
---|
| 563 | (* * Return the list of blocks in the codomain of [e]. *) |
---|
| 564 | |
---|
[487] | 565 | definition blocks_of_env : env → list block ≝ λe. |
---|
[1058] | 566 | map ?? (λx. snd ?? x) (elements ?? e). |
---|
[3] | 567 | |
---|
| 568 | (* * Selection of the appropriate case of a [switch], given the value [n] |
---|
| 569 | of the selector expression. *) |
---|
[961] | 570 | (* FIXME: now that we have several sizes of integer, it isn't clear whether we |
---|
| 571 | should allow case labels to be of a different size to the switch expression. *) |
---|
| 572 | let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements) |
---|
[3] | 573 | on sl : labeled_statements ≝ |
---|
| 574 | match sl with |
---|
| 575 | [ LSdefault _ ⇒ sl |
---|
[961] | 576 | | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n |
---|
| 577 | (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl') |
---|
[3] | 578 | ]. |
---|
| 579 | |
---|
| 580 | (* * Turn a labeled statement into a sequence *) |
---|
| 581 | |
---|
[487] | 582 | let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝ |
---|
[3] | 583 | match sl with |
---|
| 584 | [ LSdefault s ⇒ s |
---|
[961] | 585 | | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl') |
---|
[3] | 586 | ]. |
---|
| 587 | |
---|
| 588 | (* |
---|
| 589 | Section SEMANTICS. |
---|
| 590 | |
---|
| 591 | Variable ge: genv. |
---|
| 592 | |
---|
| 593 | (** ** Evaluation of expressions *) |
---|
| 594 | |
---|
| 595 | Section EXPR. |
---|
| 596 | |
---|
| 597 | Variable e: env. |
---|
| 598 | Variable m: mem. |
---|
| 599 | *) |
---|
| 600 | (* * [eval_expr ge e m a v] defines the evaluation of expression [a] |
---|
| 601 | in r-value position. [v] is the value of the expression. |
---|
| 602 | [e] is the current environment and [m] is the current memory state. *) |
---|
| 603 | |
---|
[487] | 604 | inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ |
---|
[961] | 605 | | eval_Econst_int: ∀sz,sg,i. |
---|
| 606 | eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0 |
---|
[3] | 607 | | eval_Econst_float: ∀f,ty. |
---|
[175] | 608 | eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 |
---|
[498] | 609 | | eval_Elvalue: ∀a,ty,loc,ofs,v,tr. |
---|
| 610 | eval_lvalue ge e m (Expr a ty) loc ofs tr → |
---|
| 611 | load_value_of_type ty m loc ofs = Some ? v → |
---|
[175] | 612 | eval_expr ge e m (Expr a ty) v tr |
---|
[2176] | 613 | | eval_Eaddrof: ∀a,ty,loc,ofs,tr. |
---|
[498] | 614 | eval_lvalue ge e m a loc ofs tr → |
---|
[2176] | 615 | (* ∀pc:pointer_compat loc r.*) |
---|
| 616 | eval_expr ge e m (Expr (Eaddrof a) (Tpointer ty)) (Vptr (mk_pointer loc ofs)) tr |
---|
[961] | 617 | | eval_Esizeof: ∀ty',sz,sg. |
---|
| 618 | eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0 |
---|
[175] | 619 | | eval_Eunop: ∀op,a,ty,v1,v,tr. |
---|
| 620 | eval_expr ge e m a v1 tr → |
---|
| 621 | sem_unary_operation op v1 (typeof a) = Some ? v → |
---|
| 622 | eval_expr ge e m (Expr (Eunop op a) ty) v tr |
---|
| 623 | | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
| 624 | eval_expr ge e m a1 v1 tr1 → |
---|
| 625 | eval_expr ge e m a2 v2 tr2 → |
---|
| 626 | sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v → |
---|
| 627 | eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2) |
---|
| 628 | | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2. |
---|
| 629 | eval_expr ge e m a1 v1 tr1 → |
---|
| 630 | is_true v1 (typeof a1) → |
---|
| 631 | eval_expr ge e m a2 v2 tr2 → |
---|
| 632 | eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2) |
---|
| 633 | | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2. |
---|
| 634 | eval_expr ge e m a1 v1 tr1 → |
---|
| 635 | is_false v1 (typeof a1) → |
---|
| 636 | eval_expr ge e m a3 v3 tr2 → |
---|
| 637 | eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2) |
---|
| 638 | | eval_Eorbool_1: ∀a1,a2,ty,v1,tr. |
---|
| 639 | eval_expr ge e m a1 v1 tr → |
---|
| 640 | is_true v1 (typeof a1) → |
---|
| 641 | eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr |
---|
| 642 | | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
| 643 | eval_expr ge e m a1 v1 tr1 → |
---|
| 644 | is_false v1 (typeof a1) → |
---|
| 645 | eval_expr ge e m a2 v2 tr2 → |
---|
| 646 | bool_of_val v2 (typeof a2) v → |
---|
| 647 | eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2) |
---|
| 648 | | eval_Eandbool_1: ∀a1,a2,ty,v1,tr. |
---|
| 649 | eval_expr ge e m a1 v1 tr → |
---|
| 650 | is_false v1 (typeof a1) → |
---|
| 651 | eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr |
---|
| 652 | | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. |
---|
| 653 | eval_expr ge e m a1 v1 tr1 → |
---|
| 654 | is_true v1 (typeof a1) → |
---|
| 655 | eval_expr ge e m a2 v2 tr2 → |
---|
| 656 | bool_of_val v2 (typeof a2) v → |
---|
| 657 | eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2) |
---|
| 658 | | eval_Ecast: ∀a,ty,ty',v1,v,tr. |
---|
| 659 | eval_expr ge e m a v1 tr → |
---|
| 660 | cast m v1 (typeof a) ty v → |
---|
| 661 | eval_expr ge e m (Expr (Ecast ty a) ty') v tr |
---|
| 662 | | eval_Ecost: ∀a,ty,v,l,tr. |
---|
| 663 | eval_expr ge e m a v tr → |
---|
| 664 | eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l) |
---|
[3] | 665 | |
---|
[496] | 666 | (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a] |
---|
[3] | 667 | in l-value position. The result is the memory location [b, ofs] |
---|
[496] | 668 | that contains the value of the expression [a]. The memory location should |
---|
| 669 | be representable in a pointer of region r. *) |
---|
[3] | 670 | |
---|
[583] | 671 | with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝ |
---|
[125] | 672 | | eval_Evar_local: ∀id,l,ty. |
---|
[1058] | 673 | (* XXX notation? e!id*) lookup ?? e id = Some ? l → |
---|
[583] | 674 | eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 |
---|
[498] | 675 | | eval_Evar_global: ∀id,l,ty. |
---|
[1058] | 676 | (* XXX e!id *) lookup ?? e id = None ? → |
---|
[1986] | 677 | find_symbol … ge id = Some ? l → |
---|
[583] | 678 | eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 |
---|
[2176] | 679 | | eval_Ederef: ∀a,ty,l,ofs,tr. |
---|
| 680 | eval_expr ge e m a (Vptr (mk_pointer l ofs)) tr → |
---|
[498] | 681 | eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr |
---|
| 682 | (* Aside: note that each block of memory is entirely contained within one |
---|
| 683 | memory region; hence adding a field offset will not produce a location |
---|
| 684 | outside of the original location's region. *) |
---|
| 685 | | eval_Efield_struct: ∀a,i,ty,l,ofs,id,fList,delta,tr. |
---|
| 686 | eval_lvalue ge e m a l ofs tr → |
---|
[175] | 687 | typeof a = Tstruct id fList → |
---|
| 688 | field_offset i fList = OK ? delta → |
---|
[961] | 689 | eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr |
---|
[498] | 690 | | eval_Efield_union: ∀a,i,ty,l,ofs,id,fList,tr. |
---|
| 691 | eval_lvalue ge e m a l ofs tr → |
---|
[175] | 692 | typeof a = Tunion id fList → |
---|
[498] | 693 | eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr. |
---|
[3] | 694 | |
---|
[487] | 695 | let rec eval_expr_ind (ge:genv) (e:env) (m:mem) |
---|
[226] | 696 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
[961] | 697 | (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i)) |
---|
[226] | 698 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
[498] | 699 | (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) |
---|
[2176] | 700 | (ead:∀a,ty,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty loc ofs tr H)) |
---|
[961] | 701 | (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) |
---|
[226] | 702 | (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)) |
---|
| 703 | (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)) |
---|
| 704 | (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)) |
---|
| 705 | (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)) |
---|
| 706 | (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)) |
---|
| 707 | (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)) |
---|
| 708 | (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)) |
---|
| 709 | (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)) |
---|
| 710 | (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)) |
---|
| 711 | (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) |
---|
| 712 | (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ |
---|
| 713 | match ev with |
---|
[961] | 714 | [ eval_Econst_int sz sg i ⇒ eci sz sg i |
---|
[226] | 715 | | eval_Econst_float f ty ⇒ ecF f ty |
---|
[498] | 716 | | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 |
---|
[2176] | 717 | | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H |
---|
[961] | 718 | | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg |
---|
[226] | 719 | | 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) |
---|
| 720 | | 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) |
---|
| 721 | | 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) |
---|
| 722 | | 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) |
---|
| 723 | | 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) |
---|
| 724 | | 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) |
---|
| 725 | | 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) |
---|
| 726 | | 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) |
---|
| 727 | | 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) |
---|
| 728 | | 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) |
---|
| 729 | ]. |
---|
[1672] | 730 | (* |
---|
[487] | 731 | inverter eval_expr_inv_ind for eval_expr : Prop. |
---|
[1672] | 732 | *) |
---|
[487] | 733 | let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem) |
---|
[498] | 734 | (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
| 735 | (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H)) |
---|
| 736 | (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
[2176] | 737 | (lde:∀a,ty,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty l ofs tr H)) |
---|
[498] | 738 | (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)) |
---|
| 739 | (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] | 740 | (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] | 741 | match ev with |
---|
| 742 | [ eval_Evar_local id l ty H ⇒ lvl id l ty H |
---|
[498] | 743 | | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 |
---|
[2176] | 744 | | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H |
---|
[498] | 745 | | 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) |
---|
| 746 | | 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] | 747 | ]. |
---|
| 748 | |
---|
[3] | 749 | (* |
---|
[226] | 750 | ninverter eval_lvalue_inv_ind for eval_lvalue : Prop. |
---|
| 751 | *) |
---|
[1672] | 752 | (* |
---|
[487] | 753 | definition eval_lvalue_inv_ind : |
---|
[226] | 754 | ∀x1: genv. |
---|
| 755 | ∀x2: env. |
---|
| 756 | ∀x3: mem. |
---|
| 757 | ∀x4: expr. |
---|
| 758 | ∀x6: block. |
---|
[583] | 759 | ∀x7: offset. |
---|
[226] | 760 | ∀x8: trace. |
---|
| 761 | ∀P: |
---|
| 762 | ∀_z1430: expr. |
---|
[583] | 763 | ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop. |
---|
[226] | 764 | ∀_H1: ?. |
---|
| 765 | ∀_H2: ?. |
---|
| 766 | ∀_H3: ?. |
---|
| 767 | ∀_H4: ?. |
---|
| 768 | ∀_H5: ?. |
---|
[498] | 769 | ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8. |
---|
| 770 | P x4 x6 x7 x8 |
---|
[226] | 771 | := |
---|
| 772 | (λx1:genv. |
---|
| 773 | (λx2:env. |
---|
| 774 | (λx3:mem. |
---|
| 775 | (λx4:expr. |
---|
| 776 | (λx6:block. |
---|
[583] | 777 | (λx7:offset. |
---|
[226] | 778 | (λx8:trace. |
---|
| 779 | (λP:∀_z1430: expr. |
---|
| 780 | ∀_z1428: block. |
---|
[583] | 781 | ∀_z1427: offset. ∀_z1426: trace. Prop. |
---|
[226] | 782 | (λH1:?. |
---|
| 783 | (λH2:?. |
---|
| 784 | (λH3:?. |
---|
| 785 | (λH4:?. |
---|
| 786 | (λH5:?. |
---|
[498] | 787 | (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8. |
---|
[226] | 788 | ((λHcut:∀z1435: eq expr x4 x4. |
---|
| 789 | ∀z1433: eq block x6 x6. |
---|
[583] | 790 | ∀z1432: eq offset x7 x7. |
---|
[226] | 791 | ∀z1431: eq trace x8 x8. |
---|
[498] | 792 | P x4 x6 x7 x8. |
---|
[226] | 793 | (Hcut (refl expr x4) |
---|
[498] | 794 | (refl block x6) |
---|
[583] | 795 | (refl offset x7) (refl trace x8))) |
---|
[498] | 796 | ?))))))))))))))). |
---|
| 797 | [ @(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] | 798 | [ @H1 | @H2 | @H3 | @H4 | @H5 ] |
---|
| 799 | | *: skip |
---|
| 800 | ] qed. |
---|
[1672] | 801 | *) |
---|
[487] | 802 | let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem) |
---|
[226] | 803 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
[498] | 804 | (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
[961] | 805 | (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i)) |
---|
[226] | 806 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
[498] | 807 | (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)) |
---|
[2176] | 808 | (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H)) |
---|
[961] | 809 | (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) |
---|
[226] | 810 | (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)) |
---|
| 811 | (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)) |
---|
| 812 | (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)) |
---|
| 813 | (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)) |
---|
| 814 | (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)) |
---|
| 815 | (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)) |
---|
| 816 | (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)) |
---|
| 817 | (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)) |
---|
| 818 | (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)) |
---|
| 819 | (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] | 820 | (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) |
---|
| 821 | (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
[2176] | 822 | (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H)) |
---|
[498] | 823 | (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)) |
---|
| 824 | (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] | 825 | |
---|
| 826 | (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ |
---|
| 827 | match ev with |
---|
[961] | 828 | [ eval_Econst_int sz sg i ⇒ eci sz sg i |
---|
[226] | 829 | | eval_Econst_float f ty ⇒ ecF f ty |
---|
[498] | 830 | | 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) |
---|
[2176] | 831 | | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc 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) |
---|
[961] | 832 | | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg |
---|
[226] | 833 | | 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) |
---|
| 834 | | 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) |
---|
| 835 | | 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) |
---|
| 836 | | 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) |
---|
| 837 | | 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) |
---|
| 838 | | 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) |
---|
| 839 | | 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) |
---|
| 840 | | 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) |
---|
| 841 | | 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) |
---|
| 842 | | 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) |
---|
| 843 | ] |
---|
| 844 | and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem) |
---|
| 845 | (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) |
---|
[498] | 846 | (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) |
---|
[961] | 847 | (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i)) |
---|
[226] | 848 | (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) |
---|
[498] | 849 | (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)) |
---|
[2176] | 850 | (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H)) |
---|
[961] | 851 | (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) |
---|
[226] | 852 | (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)) |
---|
| 853 | (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)) |
---|
| 854 | (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)) |
---|
| 855 | (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)) |
---|
| 856 | (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)) |
---|
| 857 | (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)) |
---|
| 858 | (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)) |
---|
| 859 | (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)) |
---|
| 860 | (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)) |
---|
| 861 | (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] | 862 | (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) |
---|
| 863 | (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) |
---|
[2176] | 864 | (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H)) |
---|
[498] | 865 | (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)) |
---|
| 866 | (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] | 867 | (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] | 868 | match ev with |
---|
| 869 | [ eval_Evar_local id l ty H ⇒ lvl id l ty H |
---|
[498] | 870 | | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 |
---|
[2176] | 871 | | eval_Ederef a ty l ofs tr H ⇒ lde a ty l 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 (mk_pointer l ofs)) tr H) |
---|
[498] | 872 | | 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) |
---|
| 873 | | 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] | 874 | ]. |
---|
| 875 | |
---|
[487] | 876 | definition combined_expr_lvalue_ind ≝ |
---|
[226] | 877 | λ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. |
---|
| 878 | conj ?? |
---|
| 879 | (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) |
---|
| 880 | (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). |
---|
| 881 | |
---|
| 882 | (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] |
---|
| 883 | in l-value position. The result is the memory location [b, ofs] |
---|
| 884 | that contains the value of the expression [a]. *) |
---|
| 885 | |
---|
| 886 | (* |
---|
| 887 | Scheme eval_expr_ind22 := Minimality for eval_expr Sort Prop |
---|
[3] | 888 | with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop. |
---|
| 889 | *) |
---|
| 890 | |
---|
| 891 | (* * [eval_exprlist ge e m al vl] evaluates a list of r-value |
---|
| 892 | expressions [al] to their values [vl]. *) |
---|
| 893 | |
---|
[487] | 894 | inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ |
---|
[3] | 895 | | eval_Enil: |
---|
[175] | 896 | eval_exprlist ge e m (nil ?) (nil ?) E0 |
---|
| 897 | | eval_Econs: ∀a,bl,v,vl,tr1,tr2. |
---|
| 898 | eval_expr ge e m a v tr1 → |
---|
| 899 | eval_exprlist ge e m bl vl tr2 → |
---|
| 900 | eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2). |
---|
[3] | 901 | |
---|
| 902 | (*End EXPR.*) |
---|
| 903 | |
---|
| 904 | (* * ** Transition semantics for statements and functions *) |
---|
| 905 | |
---|
| 906 | (* * Continuations *) |
---|
| 907 | |
---|
[487] | 908 | inductive cont: Type[0] := |
---|
[3] | 909 | | Kstop: cont |
---|
| 910 | | Kseq: statement -> cont -> cont |
---|
| 911 | (**r [Kseq s2 k] = after [s1] in [s1;s2] *) |
---|
| 912 | | Kwhile: expr -> statement -> cont -> cont |
---|
| 913 | (**r [Kwhile e s k] = after [s] in [while (e) s] *) |
---|
| 914 | | Kdowhile: expr -> statement -> cont -> cont |
---|
| 915 | (**r [Kdowhile e s k] = after [s] in [do s while (e)] *) |
---|
| 916 | | Kfor2: expr -> statement -> statement -> cont -> cont |
---|
| 917 | (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) |
---|
| 918 | | Kfor3: expr -> statement -> statement -> cont -> cont |
---|
| 919 | (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) |
---|
| 920 | | Kswitch: cont -> cont |
---|
| 921 | (**r catches [break] statements arising out of [switch] *) |
---|
[583] | 922 | | Kcall: option (block × offset × type) -> (**r where to store result *) |
---|
| 923 | function -> (**r calling function *) |
---|
| 924 | env -> (**r local env of calling function *) |
---|
[3] | 925 | cont -> cont. |
---|
| 926 | |
---|
| 927 | (* * Pop continuation until a call or stop *) |
---|
| 928 | |
---|
[487] | 929 | let rec call_cont (k: cont) : cont := |
---|
[3] | 930 | match k with |
---|
| 931 | [ Kseq s k => call_cont k |
---|
| 932 | | Kwhile e s k => call_cont k |
---|
| 933 | | Kdowhile e s k => call_cont k |
---|
| 934 | | Kfor2 e2 e3 s k => call_cont k |
---|
| 935 | | Kfor3 e2 e3 s k => call_cont k |
---|
| 936 | | Kswitch k => call_cont k |
---|
| 937 | | _ => k |
---|
| 938 | ]. |
---|
| 939 | |
---|
[487] | 940 | definition is_call_cont : cont → Prop ≝ λk. |
---|
[3] | 941 | match k with |
---|
| 942 | [ Kstop => True |
---|
| 943 | | Kcall _ _ _ _ => True |
---|
| 944 | | _ => False |
---|
| 945 | ]. |
---|
| 946 | |
---|
| 947 | (* * States *) |
---|
| 948 | |
---|
[487] | 949 | inductive state: Type[0] := |
---|
[3] | 950 | | State: |
---|
| 951 | ∀f: function. |
---|
| 952 | ∀s: statement. |
---|
| 953 | ∀k: cont. |
---|
| 954 | ∀e: env. |
---|
| 955 | ∀m: mem. state |
---|
| 956 | | Callstate: |
---|
[725] | 957 | ∀fd: clight_fundef. |
---|
[3] | 958 | ∀args: list val. |
---|
| 959 | ∀k: cont. |
---|
| 960 | ∀m: mem. state |
---|
| 961 | | Returnstate: |
---|
| 962 | ∀res: val. |
---|
| 963 | ∀k: cont. |
---|
[1713] | 964 | ∀m: mem. state |
---|
| 965 | | Finalstate: |
---|
| 966 | ∀r: int. |
---|
| 967 | state. |
---|
[3] | 968 | |
---|
| 969 | (* * Find the statement and manufacture the continuation |
---|
| 970 | corresponding to a label *) |
---|
| 971 | |
---|
[487] | 972 | let rec find_label (lbl: label) (s: statement) (k: cont) |
---|
[3] | 973 | on s: option (statement × cont) := |
---|
| 974 | match s with |
---|
| 975 | [ Ssequence s1 s2 => |
---|
| 976 | match find_label lbl s1 (Kseq s2 k) with |
---|
| 977 | [ Some sk => Some ? sk |
---|
| 978 | | None => find_label lbl s2 k |
---|
| 979 | ] |
---|
| 980 | | Sifthenelse a s1 s2 => |
---|
| 981 | match find_label lbl s1 k with |
---|
| 982 | [ Some sk => Some ? sk |
---|
| 983 | | None => find_label lbl s2 k |
---|
| 984 | ] |
---|
| 985 | | Swhile a s1 => |
---|
| 986 | find_label lbl s1 (Kwhile a s1 k) |
---|
| 987 | | Sdowhile a s1 => |
---|
| 988 | find_label lbl s1 (Kdowhile a s1 k) |
---|
| 989 | | Sfor a1 a2 a3 s1 => |
---|
| 990 | match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with |
---|
| 991 | [ Some sk => Some ? sk |
---|
| 992 | | None => |
---|
| 993 | match find_label lbl s1 (Kfor2 a2 a3 s1 k) with |
---|
| 994 | [ Some sk => Some ? sk |
---|
| 995 | | None => find_label lbl a3 (Kfor3 a2 a3 s1 k) |
---|
| 996 | ] |
---|
| 997 | ] |
---|
| 998 | | Sswitch e sl => |
---|
| 999 | find_label_ls lbl sl (Kswitch k) |
---|
| 1000 | | Slabel lbl' s' => |
---|
| 1001 | match ident_eq lbl lbl' with |
---|
| 1002 | [ inl _ ⇒ Some ? 〈s', k〉 |
---|
| 1003 | | inr _ ⇒ find_label lbl s' k |
---|
| 1004 | ] |
---|
[1914] | 1005 | | Scost c s' ⇒ |
---|
| 1006 | find_label lbl s' k |
---|
[3] | 1007 | | _ => None ? |
---|
| 1008 | ] |
---|
| 1009 | |
---|
| 1010 | and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) |
---|
| 1011 | on sl: option (statement × cont) := |
---|
| 1012 | match sl with |
---|
| 1013 | [ LSdefault s => find_label lbl s k |
---|
[961] | 1014 | | LScase _ _ s sl' => |
---|
[3] | 1015 | match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with |
---|
| 1016 | [ Some sk => Some ? sk |
---|
| 1017 | | None => find_label_ls lbl sl' k |
---|
| 1018 | ] |
---|
| 1019 | ]. |
---|
| 1020 | |
---|
| 1021 | (* * Transition relation *) |
---|
| 1022 | |
---|
[457] | 1023 | (* Strip off outer pointer for use when comparing function types. *) |
---|
[487] | 1024 | definition fun_typeof ≝ |
---|
[457] | 1025 | λe. match typeof e with |
---|
| 1026 | [ Tvoid ⇒ Tvoid |
---|
| 1027 | | Tint a b ⇒ Tint a b |
---|
| 1028 | | Tfloat a ⇒ Tfloat a |
---|
[2176] | 1029 | | Tpointer ty ⇒ ty |
---|
| 1030 | | Tarray a b ⇒ Tarray a b |
---|
[457] | 1031 | | Tfunction a b ⇒ Tfunction a b |
---|
| 1032 | | Tstruct a b ⇒ Tstruct a b |
---|
| 1033 | | Tunion a b ⇒ Tunion a b |
---|
[2176] | 1034 | | Tcomp_ptr a ⇒ Tcomp_ptr a |
---|
[457] | 1035 | ]. |
---|
| 1036 | |
---|
[175] | 1037 | (* XXX: note that cost labels in exprs expose a particular eval order. *) |
---|
[3] | 1038 | |
---|
[487] | 1039 | inductive step (ge:genv) : state → trace → state → Prop ≝ |
---|
[175] | 1040 | |
---|
[498] | 1041 | | step_assign: ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2. |
---|
| 1042 | eval_lvalue ge e m a1 loc ofs tr1 → |
---|
[175] | 1043 | eval_expr ge e m a2 v2 tr2 → |
---|
[498] | 1044 | store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' → |
---|
[3] | 1045 | step ge (State f (Sassign a1 a2) k e m) |
---|
[175] | 1046 | (tr1⧺tr2) (State f Sskip k e m') |
---|
[3] | 1047 | |
---|
[175] | 1048 | | step_call_none: ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2. |
---|
| 1049 | eval_expr ge e m a vf tr1 → |
---|
| 1050 | eval_exprlist ge e m al vargs tr2 → |
---|
[1986] | 1051 | find_funct … ge vf = Some ? fd → |
---|
[457] | 1052 | type_of_fundef fd = fun_typeof a → |
---|
[3] | 1053 | step ge (State f (Scall (None ?) a al) k e m) |
---|
[175] | 1054 | (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m) |
---|
[3] | 1055 | |
---|
[498] | 1056 | | step_call_some: ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3. |
---|
| 1057 | eval_lvalue ge e m lhs loc ofs tr1 → |
---|
[175] | 1058 | eval_expr ge e m a vf tr2 → |
---|
| 1059 | eval_exprlist ge e m al vargs tr3 → |
---|
[1986] | 1060 | find_funct … ge vf = Some ? fd → |
---|
[457] | 1061 | type_of_fundef fd = fun_typeof a → |
---|
[3] | 1062 | step ge (State f (Scall (Some ? lhs) a al) k e m) |
---|
[498] | 1063 | (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m) |
---|
[3] | 1064 | |
---|
| 1065 | | step_seq: ∀f,s1,s2,k,e,m. |
---|
| 1066 | step ge (State f (Ssequence s1 s2) k e m) |
---|
| 1067 | E0 (State f s1 (Kseq s2 k) e m) |
---|
| 1068 | | step_skip_seq: ∀f,s,k,e,m. |
---|
| 1069 | step ge (State f Sskip (Kseq s k) e m) |
---|
| 1070 | E0 (State f s k e m) |
---|
| 1071 | | step_continue_seq: ∀f,s,k,e,m. |
---|
| 1072 | step ge (State f Scontinue (Kseq s k) e m) |
---|
| 1073 | E0 (State f Scontinue k e m) |
---|
| 1074 | | step_break_seq: ∀f,s,k,e,m. |
---|
| 1075 | step ge (State f Sbreak (Kseq s k) e m) |
---|
| 1076 | E0 (State f Sbreak k e m) |
---|
| 1077 | |
---|
[175] | 1078 | | step_ifthenelse_true: ∀f,a,s1,s2,k,e,m,v1,tr. |
---|
| 1079 | eval_expr ge e m a v1 tr → |
---|
| 1080 | is_true v1 (typeof a) → |
---|
[3] | 1081 | step ge (State f (Sifthenelse a s1 s2) k e m) |
---|
[175] | 1082 | tr (State f s1 k e m) |
---|
| 1083 | | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr. |
---|
| 1084 | eval_expr ge e m a v1 tr → |
---|
| 1085 | is_false v1 (typeof a) → |
---|
[3] | 1086 | step ge (State f (Sifthenelse a s1 s2) k e m) |
---|
[175] | 1087 | tr (State f s2 k e m) |
---|
[3] | 1088 | |
---|
[175] | 1089 | | step_while_false: ∀f,a,s,k,e,m,v,tr. |
---|
| 1090 | eval_expr ge e m a v tr → |
---|
| 1091 | is_false v (typeof a) → |
---|
[3] | 1092 | step ge (State f (Swhile a s) k e m) |
---|
[175] | 1093 | tr (State f Sskip k e m) |
---|
| 1094 | | step_while_true: ∀f,a,s,k,e,m,v,tr. |
---|
| 1095 | eval_expr ge e m a v tr → |
---|
| 1096 | is_true v (typeof a) → |
---|
[3] | 1097 | step ge (State f (Swhile a s) k e m) |
---|
[175] | 1098 | tr (State f s (Kwhile a s k) e m) |
---|
[3] | 1099 | | step_skip_or_continue_while: ∀f,x,a,s,k,e,m. |
---|
[175] | 1100 | x = Sskip ∨ x = Scontinue → |
---|
[3] | 1101 | step ge (State f x (Kwhile a s k) e m) |
---|
| 1102 | E0 (State f (Swhile a s) k e m) |
---|
| 1103 | | step_break_while: ∀f,a,s,k,e,m. |
---|
| 1104 | step ge (State f Sbreak (Kwhile a s k) e m) |
---|
| 1105 | E0 (State f Sskip k e m) |
---|
| 1106 | |
---|
| 1107 | | step_dowhile: ∀f,a,s,k,e,m. |
---|
| 1108 | step ge (State f (Sdowhile a s) k e m) |
---|
| 1109 | E0 (State f s (Kdowhile a s k) e m) |
---|
[175] | 1110 | | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr. |
---|
| 1111 | x = Sskip ∨ x = Scontinue → |
---|
| 1112 | eval_expr ge e m a v tr → |
---|
| 1113 | is_false v (typeof a) → |
---|
[3] | 1114 | step ge (State f x (Kdowhile a s k) e m) |
---|
[175] | 1115 | tr (State f Sskip k e m) |
---|
| 1116 | | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr. |
---|
| 1117 | x = Sskip ∨ x = Scontinue → |
---|
| 1118 | eval_expr ge e m a v tr → |
---|
| 1119 | is_true v (typeof a) → |
---|
[3] | 1120 | step ge (State f x (Kdowhile a s k) e m) |
---|
[175] | 1121 | tr (State f (Sdowhile a s) k e m) |
---|
[3] | 1122 | | step_break_dowhile: ∀f,a,s,k,e,m. |
---|
| 1123 | step ge (State f Sbreak (Kdowhile a s k) e m) |
---|
| 1124 | E0 (State f Sskip k e m) |
---|
| 1125 | |
---|
| 1126 | | step_for_start: ∀f,a1,a2,a3,s,k,e,m. |
---|
[175] | 1127 | a1 ≠ Sskip → |
---|
[3] | 1128 | step ge (State f (Sfor a1 a2 a3 s) k e m) |
---|
| 1129 | E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) |
---|
[175] | 1130 | | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr. |
---|
| 1131 | eval_expr ge e m a2 v tr → |
---|
| 1132 | is_false v (typeof a2) → |
---|
[3] | 1133 | step ge (State f (Sfor Sskip a2 a3 s) k e m) |
---|
[175] | 1134 | tr (State f Sskip k e m) |
---|
| 1135 | | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr. |
---|
| 1136 | eval_expr ge e m a2 v tr → |
---|
| 1137 | is_true v (typeof a2) → |
---|
[3] | 1138 | step ge (State f (Sfor Sskip a2 a3 s) k e m) |
---|
[175] | 1139 | tr (State f s (Kfor2 a2 a3 s k) e m) |
---|
[3] | 1140 | | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m. |
---|
[175] | 1141 | x = Sskip ∨ x = Scontinue → |
---|
[3] | 1142 | step ge (State f x (Kfor2 a2 a3 s k) e m) |
---|
| 1143 | E0 (State f a3 (Kfor3 a2 a3 s k) e m) |
---|
| 1144 | | step_break_for2: ∀f,a2,a3,s,k,e,m. |
---|
| 1145 | step ge (State f Sbreak (Kfor2 a2 a3 s k) e m) |
---|
| 1146 | E0 (State f Sskip k e m) |
---|
| 1147 | | step_skip_for3: ∀f,a2,a3,s,k,e,m. |
---|
| 1148 | step ge (State f Sskip (Kfor3 a2 a3 s k) e m) |
---|
| 1149 | E0 (State f (Sfor Sskip a2 a3 s) k e m) |
---|
| 1150 | |
---|
| 1151 | | step_return_0: ∀f,k,e,m. |
---|
[175] | 1152 | fn_return f = Tvoid → |
---|
[3] | 1153 | step ge (State f (Sreturn (None ?)) k e m) |
---|
[1988] | 1154 | E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))) |
---|
[175] | 1155 | | step_return_1: ∀f,a,k,e,m,v,tr. |
---|
| 1156 | fn_return f ≠ Tvoid → |
---|
| 1157 | eval_expr ge e m a v tr → |
---|
[3] | 1158 | step ge (State f (Sreturn (Some ? a)) k e m) |
---|
[1988] | 1159 | tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e))) |
---|
[3] | 1160 | | step_skip_call: ∀f,k,e,m. |
---|
[175] | 1161 | is_call_cont k → |
---|
| 1162 | fn_return f = Tvoid → |
---|
[3] | 1163 | step ge (State f Sskip k e m) |
---|
[1988] | 1164 | E0 (Returnstate Vundef k (free_list m (blocks_of_env e))) |
---|
[3] | 1165 | |
---|
[961] | 1166 | | step_switch: ∀f,a,sl,k,e,m,sz,n,tr. |
---|
| 1167 | eval_expr ge e m a (Vint sz n) tr → |
---|
[3] | 1168 | step ge (State f (Sswitch a sl) k e m) |
---|
[961] | 1169 | tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m) |
---|
[3] | 1170 | | step_skip_break_switch: ∀f,x,k,e,m. |
---|
[175] | 1171 | x = Sskip ∨ x = Sbreak → |
---|
[3] | 1172 | step ge (State f x (Kswitch k) e m) |
---|
| 1173 | E0 (State f Sskip k e m) |
---|
| 1174 | | step_continue_switch: ∀f,k,e,m. |
---|
| 1175 | step ge (State f Scontinue (Kswitch k) e m) |
---|
| 1176 | E0 (State f Scontinue k e m) |
---|
| 1177 | |
---|
| 1178 | | step_label: ∀f,lbl,s,k,e,m. |
---|
| 1179 | step ge (State f (Slabel lbl s) k e m) |
---|
| 1180 | E0 (State f s k e m) |
---|
| 1181 | |
---|
| 1182 | | step_goto: ∀f,lbl,k,e,m,s',k'. |
---|
[175] | 1183 | find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 → |
---|
[3] | 1184 | step ge (State f (Sgoto lbl) k e m) |
---|
| 1185 | E0 (State f s' k' e m) |
---|
| 1186 | |
---|
| 1187 | | step_internal_function: ∀f,vargs,k,m,e,m1,m2. |
---|
[175] | 1188 | alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 → |
---|
| 1189 | bind_parameters e m1 (fn_params f) vargs m2 → |
---|
[725] | 1190 | step ge (Callstate (CL_Internal f) vargs k m) |
---|
[3] | 1191 | E0 (State f (fn_body f) k e m2) |
---|
| 1192 | |
---|
| 1193 | | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t. |
---|
[175] | 1194 | event_match (external_function id targs tres) vargs t vres → |
---|
[725] | 1195 | step ge (Callstate (CL_External id targs tres) vargs k m) |
---|
[3] | 1196 | t (Returnstate vres k m) |
---|
| 1197 | |
---|
| 1198 | | step_returnstate_0: ∀v,f,e,k,m. |
---|
| 1199 | step ge (Returnstate v (Kcall (None ?) f e k) m) |
---|
| 1200 | E0 (State f Sskip k e m) |
---|
| 1201 | |
---|
[498] | 1202 | | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty. |
---|
| 1203 | store_value_of_type ty m loc ofs v = Some ? m' → |
---|
| 1204 | step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m) |
---|
[175] | 1205 | E0 (State f Sskip k e m') |
---|
| 1206 | |
---|
| 1207 | | step_cost: ∀f,lbl,s,k,e,m. |
---|
| 1208 | step ge (State f (Scost lbl s) k e m) |
---|
[1713] | 1209 | (Echarge lbl) (State f s k e m) |
---|
| 1210 | |
---|
| 1211 | | step_final: ∀r,m. |
---|
| 1212 | step ge (Returnstate (Vint I32 r) Kstop m) |
---|
| 1213 | E0 (Finalstate r). |
---|
[1147] | 1214 | |
---|
[3] | 1215 | (* |
---|
| 1216 | End SEMANTICS. |
---|
| 1217 | *) |
---|
[1147] | 1218 | |
---|
[3] | 1219 | (* * * Whole-program semantics *) |
---|
| 1220 | |
---|
| 1221 | (* * Execution of whole programs are described as sequences of transitions |
---|
| 1222 | from an initial state to a final state. An initial state is a [Callstate] |
---|
| 1223 | corresponding to the invocation of the ``main'' function of the program |
---|
| 1224 | without arguments and with an empty continuation. *) |
---|
| 1225 | |
---|
[487] | 1226 | inductive initial_state (p: clight_program): state -> Prop := |
---|
[485] | 1227 | | initial_state_intro: ∀b,f,ge,m0. |
---|
[1986] | 1228 | globalenv … (fst ??) p = ge → |
---|
| 1229 | init_mem … (fst ??) p = OK ? m0 → |
---|
| 1230 | find_symbol … ge (prog_main ?? p) = Some ? b → |
---|
| 1231 | find_funct_ptr … ge b = Some ? f → |
---|
[3] | 1232 | initial_state p (Callstate f (nil ?) Kstop m0). |
---|
| 1233 | |
---|
| 1234 | (* * A final state is a [Returnstate] with an empty continuation. *) |
---|
| 1235 | |
---|
[487] | 1236 | inductive final_state: state -> int -> Prop := |
---|
[1713] | 1237 | | final_state_intro: ∀r. |
---|
| 1238 | final_state (Finalstate r) r. |
---|
[3] | 1239 | |
---|
| 1240 | (* * Execution of a whole program: [exec_program p beh] |
---|
| 1241 | holds if the application of [p]'s main function to no arguments |
---|
| 1242 | in the initial memory state for [p] has [beh] as observable |
---|
| 1243 | behavior. *) |
---|
| 1244 | |
---|
[487] | 1245 | definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. |
---|
[1986] | 1246 | ∀ge. globalenv … (fst ??) p = ge → |
---|
[485] | 1247 | program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. |
---|
[3] | 1248 | |
---|