Changeset 1872 for src/Clight/Csem.ma
 Timestamp:
 Apr 4, 2012, 6:48:23 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csem.ma
r1713 r1872 27 27 (*include "Events.ma".*) 28 28 include "common/Smallstep.ma". 29 include "Clight/ClassifyOp.ma". 29 30 30 31 (* * * Semantics of typedependent operations *) … … 117 118 let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 118 119 match classify_add t1 t2 with 119 [ add_case_ii ⇒ (**r integer addition *)120 [ add_case_ii _ _ ⇒ (**r integer addition *) 120 121 match v1 with 121 122 [ Vint sz1 n1 ⇒ match v2 with … … 124 125  _ ⇒ None ? ] 125 126  _ ⇒ None ? ] 126  add_case_ff ⇒ (**r float addition *)127  add_case_ff _ ⇒ (**r float addition *) 127 128 match v1 with 128 129 [ Vfloat n1 ⇒ match v2 with … … 130 131  _ ⇒ None ? ] 131 132  _ ⇒ None ? ] 132  add_case_pi ty⇒ (**r pointer plus integer *)133  add_case_pi _ _ ty _ _ ⇒ (**r pointer plus integer *) 133 134 match v1 with 134 135 [ Vptr ptr1 ⇒ match v2 with … … 139 140  _ ⇒ None ? ] 140 141  _ ⇒ None ? ] 141  add_case_ip ty ⇒ (**r integer plus pointer *)142  add_case_ip _ _ _ _ ty ⇒ (**r integer plus pointer *) 142 143 match v1 with 143 144 [ Vint sz1 n1 ⇒ match v2 with … … 146 147  _ ⇒ None ? ] 147 148  _ ⇒ None ? ] 148  add_default ⇒ None ?149  add_default _ _ ⇒ None ? 149 150 ]. 150 151 151 152 let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 152 153 match classify_sub t1 t2 with 153 [ sub_case_ii ⇒ (**r integer subtraction *)154 [ sub_case_ii _ _ ⇒ (**r integer subtraction *) 154 155 match v1 with 155 156 [ Vint sz1 n1 ⇒ match v2 with … … 158 159  _ ⇒ None ? ] 159 160  _ ⇒ None ? ] 160  sub_case_ff ⇒ (**r float subtraction *)161  sub_case_ff _ ⇒ (**r float subtraction *) 161 162 match v1 with 162 163 [ Vfloat f1 ⇒ match v2 with … … 164 165  _ ⇒ None ? ] 165 166  _ ⇒ None ? ] 166  sub_case_pi ty⇒ (**r pointer minus integer *)167  sub_case_pi _ _ ty _ _ ⇒ (**r pointer minus integer *) 167 168 match v1 with 168 169 [ Vptr ptr1 ⇒ match v2 with … … 173 174  _ ⇒ None ? ] 174 175  _ ⇒ None ? ] 175  sub_case_pp ty⇒ (**r pointer minus pointer *)176  sub_case_pp _ _ _ ty _ _ ⇒ (**r pointer minus pointer *) 176 177 match v1 with 177 178 [ Vptr ptr1 ⇒ match v2 with … … 187 188  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?))  _ ⇒ None ? ] 188 189  _ ⇒ None ? ] 189  sub_default ⇒ None ?190  sub_default _ _ ⇒ None ? 190 191 ]. 191 192 192 193 let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 193 match classify_ mult1 t2 with194 [ mul_case_ii⇒194 match classify_aop t1 t2 with 195 [ aop_case_ii _ _ ⇒ 195 196 match v1 with 196 197 [ Vint sz1 n1 ⇒ match v2 with … … 199 200  _ ⇒ None ? ] 200 201  _ ⇒ None ? ] 201  mul_case_ff⇒202  aop_case_ff _ ⇒ 202 203 match v1 with 203 204 [ Vfloat f1 ⇒ match v2 with … … 205 206  _ ⇒ None ? ] 206 207  _ ⇒ None ? ] 207  mul_default⇒208  aop_default _ _ ⇒ 208 209 None ? 209 210 ]. 210 211 211 212 let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 212 match classify_div t1 t2 with 213 [ div_case_I32unsi ⇒ 214 match v1 with 215 [ Vint sz1 n1 ⇒ match v2 with 216 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 217 (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?) 218  _ ⇒ None ? ] 219  _ ⇒ None ? ] 220  div_case_ii ⇒ 213 match classify_aop t1 t2 with 214 [ aop_case_ii _ sg ⇒ 221 215 match v1 with 222 216 [ Vint sz1 n1 ⇒ match v2 with 223 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 217 [ Vint sz2 n2 ⇒ 218 match sg with 219 [ Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 224 220 (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?) 221  Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 222 (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?) 223 ] 225 224  _ ⇒ None ? ] 226 225  _ ⇒ None ? ] 227  div_case_ff⇒226  aop_case_ff _ ⇒ 228 227 match v1 with 229 228 [ Vfloat f1 ⇒ match v2 with … … 231 230  _ ⇒ None ? ] 232 231  _ ⇒ None ? ] 233  div_default⇒232  aop_default _ _ ⇒ 234 233 None ? 235 234 ]. 236 235 237 236 let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 238 match classify_ modt1 t2 with239 [ mod_case_I32unsi⇒237 match classify_aop t1 t2 with 238 [ aop_case_ii sz sg ⇒ 240 239 match v1 with 241 240 [ Vint sz1 n1 ⇒ match v2 with 242 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 241 [ Vint sz2 n2 ⇒ 242 match sg with 243 [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 243 244 (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?) 244  _ ⇒ None ? ] 245  _ ⇒ None ? ] 246  mod_case_ii ⇒ 247 match v1 with 248 [ Vint sz1 n1 ⇒ match v2 with 249 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 250 (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?) 251  _ ⇒ None ? ] 252  _ ⇒ None ? ] 253  mod_default ⇒ 245  Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 246 (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?) 247 ] 248  _ ⇒ None ? ] 249  _ ⇒ None ? ] 250  _ ⇒ 254 251 None ? 255 252 ]. … … 293 290 294 291 let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ 295 match classify_ shrt1 t2 with296 [ shr_case_I32unsi ⇒292 match classify_aop t1 t2 with 293 [ aop_case_ii _ sg ⇒ 297 294 match v1 with 298 295 [ Vint sz1 n1 ⇒ match v2 with 299 296 [ Vint sz2 n2 ⇒ 297 match sg with 298 [ Unsigned ⇒ 300 299 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 301 300 then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false)) 302 301 else None ? 303  _ ⇒ None ? ] 304  _ ⇒ None ? ] 305  shr_case_ii => 306 match v1 with 307 [ Vint sz1 n1 ⇒ match v2 with 308 [ Vint sz2 n2 ⇒ 302  Signed ⇒ 309 303 if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1)) 310 304 then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1))) 311 305 else None ? 312  _ ⇒ None ? ] 313  _ ⇒ None ? ] 314  shr_default ⇒ 306 ] 307  _ ⇒ None ? ] 308  _ ⇒ None ? ] 309  _ ⇒ 315 310 None ? 316 311 ]. … … 318 313 let rec sem_cmp_mismatch (c: comparison): option val ≝ 319 314 match c with 320 [ Ceq =>Some ? Vfalse321  Cne =>Some ? Vtrue322  _ =>None ?315 [ Ceq ⇒ Some ? Vfalse 316  Cne ⇒ Some ? Vtrue 317  _ ⇒ None ? 323 318 ]. 324 319 325 320 let rec sem_cmp_match (c: comparison): option val ≝ 326 321 match c with 327 [ Ceq =>Some ? Vtrue328  Cne =>Some ? Vfalse329  _ =>None ?322 [ Ceq ⇒ Some ? Vtrue 323  Cne ⇒ Some ? Vfalse 324  _ ⇒ None ? 330 325 ]. 331 326 … … 334 329 (m: mem): option val ≝ 335 330 match classify_cmp t1 t2 with 336 [ cmp_case_ I32unsi⇒331 [ cmp_case_ii _ sg ⇒ 337 332 match v1 with 338 333 [ Vint sz1 n1 ⇒ match v2 with 339 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 334 [ Vint sz2 n2 ⇒ 335 match sg with 336 [ Unsigned ⇒ intsize_eq_elim ? sz1 sz2 ? n1 340 337 (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?) 341  _ ⇒ None ? ] 342  _ ⇒ None ? ] 343  cmp_case_ii ⇒ 344 match v1 with 345 [ Vint sz1 n1 ⇒ match v2 with 346 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 347 (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?) 338  Signed ⇒ intsize_eq_elim ? sz1 sz2 ? n1 339 (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?) 340 ] 348 341  _ ⇒ None ? 349 342 ] 350 343  _ ⇒ None ? 351 344 ] 352  cmp_case_pp ⇒345  cmp_case_pp _ _ _ ⇒ 353 346 match v1 with 354 347 [ Vptr ptr1 ⇒ … … 370 363 ] 371 364  _ ⇒ None ? ] 372  cmp_case_ff ⇒365  cmp_case_ff _ ⇒ 373 366 match v1 with 374 367 [ Vfloat f1 ⇒ … … 377 370  _ ⇒ None ? ] 378 371  _ ⇒ None ? ] 379  cmp_default ⇒ None ?372  cmp_default _ _ ⇒ None ? 380 373 ]. 381 374 … … 499 492  inr _ ⇒ None ? 500 493 ] 501  By_nothing ⇒ None ?494  By_nothing _ ⇒ None ? 502 495 ]. 503 496 cases b // … … 513 506 [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v 514 507  By_reference _ ⇒ None ? 515  By_nothing ⇒ None ?508  By_nothing _ ⇒ None ? 516 509 ]. 517 510 cases loc //
Note: See TracChangeset
for help on using the changeset viewer.