Changeset 961 for src/common/Values.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Values.ma
r891 r961 19 19 include "utilities/Coqlib.ma". 20 20 include "common/AST.ma". 21 include "common/Integers.ma".22 21 include "common/Floats.ma". 23 22 include "common/Errors.ma". … … 27 26 include "basics/logic.ma". 28 27 29 include "utilities/binary/Z.ma".30 28 include "utilities/extralib.ma". 31 29 … … 94 92 95 93 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y). 96 definition shift_offset : offset → int → offset ≝ 97 λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i). 98 definition neg_shift_offset : offset → int → offset ≝ 99 λo,i. mk_offset (offv o  Z_of_signed_bitvector ? i). 100 definition sub_offset : offset → offset → int ≝ 101 λx,y. bitvector_of_Z ? (offv x  offv y). 94 definition shift_offset : ∀n. offset → BitVector n → offset ≝ 95 λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i). 96 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *) 97 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝ 98 λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)). 99 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ 100 λn,o,i. mk_offset (offv o  Z_of_signed_bitvector ? i). 101 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝ 102 λn,o,i,j. mk_offset (offv o  (Z_of_nat i) * (Z_of_signed_bitvector ? j)). 103 definition sub_offset : ∀n. offset → offset → BitVector n ≝ 104 λn,x,y. bitvector_of_Z ? (offv x  offv y). 102 105 definition zero_offset ≝ mk_offset OZ. 103 106 definition lt_offset : offset → offset → bool ≝ … … 117 120 inductive val: Type[0] ≝ 118 121  Vundef: val 119  Vint: int→ val122  Vint: ∀sz:intsize. bvint sz → val 120 123  Vfloat: float → val 121 124  Vnull: region → val 122 125  Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val. 123 126 124 definition Vzero: val ≝ Vint zero. 125 definition Vone: val ≝ Vint one. 126 definition Vmone: val ≝ Vint mone. 127 128 definition Vtrue: val ≝ Vint one. 129 definition Vfalse: val ≝ Vint zero. 127 definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?). 128 definition Vone: intsize → val ≝ λsz. Vint sz (repr sz 1). 129 definition mone ≝ λsz. bitvector_of_Z (bitsize_of_intsize sz) (neg one). 130 definition Vmone: intsize → val ≝ λsz. Vint sz (mone ?). 131 132 (* XXX 32bit booleans are Clight specific. *) 133 definition Vtrue: val ≝ Vone I32. 134 definition Vfalse: val ≝ Vzero I32. 130 135 131 136 (* Values split into bytes. Ideally we'd use some kind of sizeof for the … … 140 145 λv. match v with 141 146 [ Vundef ⇒ True 142  Vint _ ⇒ True147  Vint _ _ ⇒ True 143 148  Vfloat _ ⇒ False 144 149  Vnull r ⇒ ptr_may_be_single r = true … … 148 153 definition may_be_split : val → Prop ≝ 149 154 λv.match v with 150 [ Vint _ ⇒ False155 [ Vint _ _ ⇒ False 151 156  Vnull r ⇒ ptr_may_be_single r = false 152 157  Vptr r _ _ _ ⇒ ptr_may_be_single r = false … … 248 253 definition is_true : val → Prop ≝ λv. 249 254 match v with 250 [ Vint n ⇒ n ≠ zero255 [ Vint _ n ⇒ n ≠ (zero ?) 251 256  Vptr _ b _ ofs ⇒ True 252 257  _ ⇒ False … … 255 260 definition is_false : val → Prop ≝ λv. 256 261 match v with 257 [ Vint n ⇒ n = zero262 [ Vint _ n ⇒ n = (zero ?) 258 263  Vnull _ ⇒ True 259 264  _ ⇒ False … … 262 267 inductive bool_of_val: val → bool → Prop ≝ 263 268  bool_of_val_int_true: 264 ∀ n. n ≠ zero → bool_of_val (Vintn) true269 ∀sz,n. n ≠ zero ? → bool_of_val (Vint sz n) true 265 270  bool_of_val_int_false: 266 bool_of_val (Vint zero) false271 ∀sz. bool_of_val (Vzero sz) false 267 272  bool_of_val_ptr: 268 273 ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true … … 274 279 definition eval_bool_of_val : val → res bool ≝ 275 280 λv. match v with 276 [ Vint i ⇒ OK ? (notb (eq i zero))281 [ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?))) 277 282  Vnull _ ⇒ OK ? false 278 283  Vptr _ _ _ _ ⇒ OK ? true … … 282 287 definition neg : val → val ≝ λv. 283 288 match v with 284 [ Vint n ⇒ Vint (negn)289 [ Vint sz n ⇒ Vint sz (two_complement_negation ? n) 285 290  _ ⇒ Vundef 286 291 ]. … … 298 303 ]. 299 304 300 definition intoffloat : val → val ≝ λv.301 match v with 302 [ Vfloat f ⇒ Vint (intoffloatf)305 definition intoffloat : intsize → val → val ≝ λsz,v. 306 match v with 307 [ Vfloat f ⇒ Vint sz (intoffloat ? f) 303 308  _ ⇒ Vundef 304 309 ]. 305 310 306 definition intuoffloat : val → val ≝ λv.307 match v with 308 [ Vfloat f ⇒ Vint (intuoffloatf)311 definition intuoffloat : intsize → val → val ≝ λsz,v. 312 match v with 313 [ Vfloat f ⇒ Vint sz (intuoffloat ? f) 309 314  _ ⇒ Vundef 310 315 ]. … … 312 317 definition floatofint : val → val ≝ λv. 313 318 match v with 314 [ Vint n ⇒ Vfloat (floatofintn)319 [ Vint sz n ⇒ Vfloat (floatofint ? n) 315 320  _ ⇒ Vundef 316 321 ]. … … 318 323 definition floatofintu : val → val ≝ λv. 319 324 match v with 320 [ Vint n ⇒ Vfloat (floatofintun)325 [ Vint sz n ⇒ Vfloat (floatofintu ? n) 321 326  _ ⇒ Vundef 322 327 ]. … … 324 329 definition notint : val → val ≝ λv. 325 330 match v with 326 [ Vint n ⇒ Vint (xor n mone)331 [ Vint sz n ⇒ Vint sz (exclusive_disjunction_bv ? n (mone ?)) 327 332  _ ⇒ Vundef 328 333 ]. 329 334 330 (* FIXME: switch to alias, or rename, or … *)331 definition int_eq : int → int → bool ≝ eq.332 335 definition notbool : val → val ≝ λv. 333 336 match v with 334 [ Vint n ⇒ of_bool (int_eq n zero)337 [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?)) 335 338  Vptr _ b _ ofs ⇒ Vfalse 336 339  Vnull _ ⇒ Vtrue … … 338 341 ]. 339 342 340 definition zero_ext ≝ λ nbits: nat. λv: val.341 match v with 342 [ Vint n ⇒ Vint (zero_ext nbitsn)343 definition zero_ext ≝ λrsz: intsize. λv: val. 344 match v with 345 [ Vint sz n ⇒ Vint rsz (zero_ext … n) 343 346  _ ⇒ Vundef 344 347 ]. 345 348 346 definition sign_ext ≝ λ nbits:nat. λv:val.347 match v with 348 [ Vint i ⇒ Vint (sign_ext nbitsi)349 definition sign_ext ≝ λrsz:intsize. λv:val. 350 match v with 351 [ Vint sz i ⇒ Vint rsz (sign_ext … i) 349 352  _ ⇒ Vundef 350 353 ]. … … 359 362 definition add ≝ λv1,v2: val. 360 363 match v1 with 361 [ Vint n1 ⇒ match v2 with 362 [ Vint n2 ⇒ Vint (addition_n ? n1 n2) 363  Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1) 364 [ Vint sz1 n1 ⇒ match v2 with 365 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 366 (λn1. Vint sz2 (addition_n ? n1 n2)) 367 Vundef 368  Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1) 364 369  _ ⇒ Vundef ] 365 370  Vptr r b1 p ofs1 ⇒ match v2 with 366 [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2) 367  _ ⇒ Vundef ] 368  _ ⇒ Vundef ]. 371 [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2) 372  _ ⇒ Vundef ] 373  _ ⇒ Vundef ]. 374 375 (* XXX Is I32 the best answer for ptr subtraction? *) 369 376 370 377 definition sub ≝ λv1,v2: val. 371 378 match v1 with 372 [ Vint n1 ⇒ match v2 with 373 [ Vint n2 ⇒ Vint (subtraction ? n1 n2) 379 [ Vint sz1 n1 ⇒ match v2 with 380 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 381 (λn1. Vint sz2 (subtraction ? n1 n2)) 382 Vundef 374 383  _ ⇒ Vundef ] 375 384  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 376 [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offsetofs1 n2)385 [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2) 377 386  Vptr r2 b2 p2 ofs2 ⇒ 378 if eq_block b1 b2 then Vint (sub_offsetofs1 ofs2) else Vundef379  _ ⇒ Vundef ] 380  Vnull r ⇒ match v2 with [ Vnull r' ⇒ V int zero _ ⇒ Vundef ]387 if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef 388  _ ⇒ Vundef ] 389  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32  _ ⇒ Vundef ] 381 390  _ ⇒ Vundef ]. 382 391 383 392 definition mul ≝ λv1, v2: val. 384 393 match v1 with 385 [ Vint n1 ⇒ match v2 with 386 [ Vint n2 ⇒ Vint (mul n1 n2) 394 [ Vint sz1 n1 ⇒ match v2 with 395 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 396 (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2)))) 397 Vundef 387 398  _ ⇒ Vundef ] 388 399  _ ⇒ Vundef ]. … … 418 429 definition v_and ≝ λv1, v2: val. 419 430 match v1 with 420 [ Vint n1 ⇒ match v2 with 421 [ Vint n2 ⇒ Vint (i_and n1 n2) 431 [ Vint sz1 n1 ⇒ match v2 with 432 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 433 (λn1. Vint ? (conjunction_bv ? n1 n2)) 434 Vundef 422 435  _ ⇒ Vundef ] 423 436  _ ⇒ Vundef ]. … … 425 438 definition or ≝ λv1, v2: val. 426 439 match v1 with 427 [ Vint n1 ⇒ match v2 with 428 [ Vint n2 ⇒ Vint (or n1 n2) 440 [ Vint sz1 n1 ⇒ match v2 with 441 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 442 (λn1. Vint ? (inclusive_disjunction_bv ? n1 n2)) 443 Vundef 429 444  _ ⇒ Vundef ] 430 445  _ ⇒ Vundef ]. … … 432 447 definition xor ≝ λv1, v2: val. 433 448 match v1 with 434 [ Vint n1 ⇒ match v2 with 435 [ Vint n2 ⇒ Vint (xor n1 n2) 449 [ Vint sz1 n1 ⇒ match v2 with 450 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 451 (λn1. Vint ? (exclusive_disjunction_bv ? n1 n2)) 452 Vundef 436 453  _ ⇒ Vundef ] 437 454  _ ⇒ Vundef ]. … … 550 567 ]. 551 568 569 definition cmp_int : ∀n. comparison → BitVector n → BitVector n → bool ≝ 570 λn,c,x,y. 571 match c with 572 [ Ceq ⇒ eq_bv ? x y 573  Cne ⇒ notb (eq_bv ? x y) 574  Clt ⇒ lt_s ? x y 575  Cle ⇒ notb (lt_s ? y x) 576  Cgt ⇒ lt_s ? y x 577  Cge ⇒ notb (lt_s ? x y) 578 ]. 579 580 definition cmpu_int : ∀n. comparison → BitVector n → BitVector n → bool ≝ 581 λn,c,x,y. 582 match c with 583 [ Ceq ⇒ eq_bv ? x y 584  Cne ⇒ notb (eq_bv ? x y) 585  Clt ⇒ lt_u ? x y 586  Cle ⇒ notb (lt_u ? y x) 587  Cgt ⇒ lt_u ? y x 588  Cge ⇒ notb (lt_u ? x y) 589 ]. 590 552 591 definition cmp ≝ λc: comparison. λv1,v2: val. 553 592 match v1 with 554 [ Vint n1 ⇒ match v2 with 555 [ Vint n2 ⇒ of_bool (cmp c n1 n2) 593 [ Vint sz1 n1 ⇒ match v2 with 594 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 595 (λn1. of_bool (cmp_int ? c n1 n2)) 596 Vundef 556 597  _ ⇒ Vundef ] 557 598  Vptr r1 b1 p1 ofs1 ⇒ match v2 with … … 571 612 definition cmpu ≝ λc: comparison. λv1,v2: val. 572 613 match v1 with 573 [ Vint n1 ⇒ match v2 with 574 [ Vint n2 ⇒ of_bool (cmpu c n1 n2) 614 [ Vint sz1 n1 ⇒ match v2 with 615 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 616 (λn1. of_bool (cmpu_int ? c n1 n2)) 617 Vundef 575 618  _ ⇒ Vundef ] 576 619  Vptr r1 b1 p1 ofs1 ⇒ match v2 with … … 588 631  _ ⇒ Vundef ]. 589 632 590 definition cmpf ≝ λc: comparison. λ v1,v2: val.633 definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val. 591 634 match v1 with 592 635 [ Vfloat f1 ⇒ match v2 with … … 603 646 is performed and [0xFFFFFFFF] is returned. Type mismatches 604 647 (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *) 648 (* XXX update comment *) 649 (* XXX is this even necessary now? 650 should we be able to extract bytes? *) 605 651 606 652 let rec load_result (chunk: memory_chunk) (v: val) ≝ 607 653 match v with 608 [ Vint n ⇒654 [ Vint sz n ⇒ 609 655 match chunk with 610 [ Mint8signed ⇒ Vint (sign_ext 8 n)611  Mint8unsigned ⇒ Vint (zero_ext 8 n)612  Mint16signed ⇒ Vint (sign_ext 16 n)613  Mint16unsigned ⇒ Vint (zero_ext 16 n)614  Mint32 ⇒ Vint n656 [ Mint8signed ⇒ match sz with [ I8 ⇒ v  _ ⇒ Vundef ] 657  Mint8unsigned ⇒ match sz with [ I8 ⇒ v  _ ⇒ Vundef ] 658  Mint16signed ⇒ match sz with [ I16 ⇒ v  _ ⇒ Vundef ] 659  Mint16unsigned ⇒ match sz with [ I16 ⇒ v  _ ⇒ Vundef ] 660  Mint32 ⇒ match sz with [ I32 ⇒ v  _ ⇒ Vundef ] 615 661  _ ⇒ Vundef 616 662 ]
Note: See TracChangeset
for help on using the changeset viewer.