Changeset 583 for Deliverables/D3.1/Csemantics/Values.ma
 Timestamp:
 Feb 22, 2011, 4:23:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Values.ma
r500 r583 60 60 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true  inr _ ⇒ false ]. 61 61 62 record offset : Type[0] ≝ { offv : Z }. 63 64 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y). 65 definition shift_offset : offset → int → offset ≝ 66 λo,i. mk_offset (offv o + signed i). 67 definition neg_shift_offset : offset → int → offset ≝ 68 λo,i. mk_offset (offv o  signed i). 69 definition sub_offset : offset → offset → int ≝ 70 λx,y. repr (offv x  offv y). 71 definition zero_offset ≝ mk_offset OZ. 72 definition lt_offset : offset → offset → bool ≝ 73 λx,y. Zltb (offv x) (offv y). 74 62 75 (* * A value is either: 63 76  a machine integer; … … 76 89  Vfloat: float → val 77 90  Vnull: region → val 78  Vptr: ∀r:region. ∀b:block. pointer_compat b r → int → val.91  Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val. 79 92 80 93 definition Vzero: val ≝ Vint zero. … … 219 232 [ Vint n1 ⇒ match v2 with 220 233 [ Vint n2 ⇒ Vint (add n1 n2) 221  Vptr r b2 p ofs2 ⇒ Vptr r b2 p ( addofs2 n1)234  Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1) 222 235  _ ⇒ Vundef ] 223 236  Vptr r b1 p ofs1 ⇒ match v2 with 224 [ Vint n2 ⇒ Vptr r b1 p ( addofs1 n2)237 [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2) 225 238  _ ⇒ Vundef ] 226 239  _ ⇒ Vundef ]. … … 232 245  _ ⇒ Vundef ] 233 246  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 234 [ Vint n2 ⇒ Vptr r1 b1 p1 ( subofs1 n2)247 [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2) 235 248  Vptr r2 b2 p2 ofs2 ⇒ 236 if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef249 if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef 237 250  _ ⇒ Vundef ] 238 251  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero  _ ⇒ Vundef ] … … 397 410 ]. 398 411 399 (* TODO: consider whether to check pointer representations *) 412 definition cmp_offset ≝ 413 λc: comparison. λx,y:offset. 414 match c with 415 [ Ceq ⇒ eq_offset x y 416  Cne ⇒ ¬eq_offset x y 417  Clt ⇒ lt_offset x y 418  Cle ⇒ ¬lt_offset y x 419  Cgt ⇒ lt_offset y x 420  Cge ⇒ ¬lt_offset x y 421 ]. 422 400 423 definition cmp ≝ λc: comparison. λv1,v2: val. 401 424 match v1 with … … 406 429 [ Vptr r2 b2 p2 ofs2 ⇒ 407 430 if eq_block b1 b2 408 then of_bool (cmp c ofs1 ofs2)431 then of_bool (cmp_offset c ofs1 ofs2) 409 432 else cmp_mismatch c 410 433  Vnull r2 ⇒ cmp_mismatch c … … 425 448 [ Vptr r2 b2 p2 ofs2 ⇒ 426 449 if eq_block b1 b2 427 then of_bool (cmp uc ofs1 ofs2)450 then of_bool (cmp_offset c ofs1 ofs2) 428 451 else cmp_mismatch c 429 452  Vnull r2 ⇒ cmp_mismatch c
Note: See TracChangeset
for help on using the changeset viewer.