Changeset 1545 for src/common/Values.ma
 Timestamp:
 Nov 23, 2011, 6:03:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Values.ma
r1510 r1545 39 39  Vfloat: float → val 40 40  Vnull: region → val 41  Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset→ val.41  Vptr: pointer → val. 42 42 43 43 definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?). … … 54 54  VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz) 55 55  VTnull: ∀r. val_typ (Vnull r) (ASTptr r) 56  VTptr: ∀r,b,c,o. val_typ (Vptr r b c o) (ASTptr r).56  VTptr: ∀r,b,c,o. val_typ (Vptr (mk_pointer r b c o)) (ASTptr r). 57 57 58 58 (* … … 64 64 *) 65 65 definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse. 66 (* 67 definition has_type ≝ λv: val. λt: typ. 68 match v with 69 [ Vundef ⇒ True 70  Vint _ ⇒ match t with [ ASTint ⇒ True  _ ⇒ False ] 71  Vfloat _ ⇒ match t with [ ASTfloat ⇒ True  _ ⇒ False ] 72  Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True  _ ⇒ False ] 73  _ ⇒ False 74 ]. 75 76 let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝ 77 match vl with 78 [ nil ⇒ match tl with [ nil ⇒ True  _ ⇒ False ] 79  cons v1 vs ⇒ match tl with [ nil ⇒ False  cons t1 ts ⇒ 80 has_type v1 t1 ∧ has_type_list vs ts ] 81 ]. 82 *) 66 83 67 (* * Truth values. Pointers and nonzero integers are treated as [True]. 84 68 The integer 0 (also used to represent the null pointer) is [False]. … … 88 72 match v with 89 73 [ Vint _ n ⇒ n ≠ (zero ?) 90  Vptr _ b _ ofs⇒ True74  Vptr _ ⇒ True 91 75  _ ⇒ False 92 76 ]. … … 105 89 ∀sz. bool_of_val (Vzero sz) false 106 90  bool_of_val_ptr: 107 ∀ r,b,p,ofs. bool_of_val (Vptr r b p ofs) true91 ∀p. bool_of_val (Vptr p) true 108 92  bool_of_val_null: 109 93 ∀r. bool_of_val (Vnull r) true. … … 115 99 [ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?))) 116 100  Vnull _ ⇒ OK ? false 117  Vptr _ _ _ _⇒ OK ? true101  Vptr _ ⇒ OK ? true 118 102  _ ⇒ Error ? (msg ValueNotABoolean) 119 103 ]. … … 170 154 match v with 171 155 [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?)) 172  Vptr _ b _ ofs⇒ Vfalse156  Vptr _ ⇒ Vfalse 173 157  Vnull _ ⇒ Vtrue 174 158  _ ⇒ Vundef … … 200 184 (λn1. Vint sz2 (addition_n ? n1 n2)) 201 185 Vundef 202  Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2n1)203  _ ⇒ Vundef ] 204  Vptr r b1 p ofs1⇒ match v2 with205 [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1n2)186  Vptr ptr ⇒ Vptr (shift_pointer ? ptr n1) 187  _ ⇒ Vundef ] 188  Vptr ptr ⇒ match v2 with 189 [ Vint _ n2 ⇒ Vptr (shift_pointer ? ptr n2) 206 190  _ ⇒ Vundef ] 207 191  _ ⇒ Vundef ]. … … 216 200 Vundef 217 201  _ ⇒ Vundef ] 218  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 219 [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2) 220  Vptr r2 b2 p2 ofs2 ⇒ 221 if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef 202  Vptr ptr1 ⇒ match v2 with 203 [ Vint sz2 n2 ⇒ Vptr (neg_shift_pointer ? ptr1 n2) 204  Vptr ptr2 ⇒ 205 if eq_block (pblock ptr1) (pblock ptr2) 206 then Vint I32 (sub_offset ? (poff ptr1) (poff ptr2)) 207 else Vundef 222 208  _ ⇒ Vundef ] 223 209  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32  _ ⇒ Vundef ] … … 430 416 Vundef 431 417  _ ⇒ Vundef ] 432  Vptr r1 b1 p1 ofs1 ⇒ match v2 with433 [ Vptr r2 b2 p2 ofs2 ⇒434 if eq_block b1 b2435 then of_bool (cmp_offset c ofs1 ofs2)418  Vptr ptr1 ⇒ match v2 with 419 [ Vptr ptr2 ⇒ 420 if eq_block (pblock ptr1) (pblock ptr2) 421 then of_bool (cmp_offset c (poff ptr1) (poff ptr2)) 436 422 else cmp_mismatch c 437 423  Vnull r2 ⇒ cmp_mismatch c 438 424  _ ⇒ Vundef ] 439 425  Vnull r1 ⇒ match v2 with 440 [ Vptr _ _ _ _⇒ cmp_mismatch c426 [ Vptr _ ⇒ cmp_mismatch c 441 427  Vnull r2 ⇒ cmp_match c 442 428  _ ⇒ Vundef … … 451 437 Vundef 452 438  _ ⇒ Vundef ] 453  Vptr r1 b1 p1 ofs1 ⇒ match v2 with454 [ Vptr r2 b2 p2 ofs2 ⇒455 if eq_block b1 b2456 then of_bool (cmp_offset c ofs1 ofs2)439  Vptr ptr1 ⇒ match v2 with 440 [ Vptr ptr2 ⇒ 441 if eq_block (pblock ptr1) (pblock ptr2) 442 then of_bool (cmp_offset c (poff ptr1) (poff ptr2)) 457 443 else cmp_mismatch c 458 444  Vnull r2 ⇒ cmp_mismatch c 459 445  _ ⇒ Vundef ] 460 446  Vnull r1 ⇒ match v2 with 461 [ Vptr _ _ _ _⇒ cmp_mismatch c447 [ Vptr _ ⇒ cmp_mismatch c 462 448  Vnull r2 ⇒ cmp_match c 463 449  _ ⇒ Vundef … … 495 481  _ ⇒ Vundef 496 482 ] 497  Vptr r b p ofs⇒483  Vptr ptr ⇒ 498 484 match chunk with 499 [ Mpointer r ' ⇒ if eq_region r r' then Vptr r b p ofselse Vundef485 [ Mpointer r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef 500 486  _ ⇒ Vundef 501 487 ]
Note: See TracChangeset
for help on using the changeset viewer.