Changeset 744 for src/common/Values.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Values.ma
r718 r744 23 23 include "common/Errors.ma". 24 24 25 include "ASM/ Vector.ma".25 include "ASM/BitVectorZ.ma". 26 26 27 27 include "basics/logic.ma". 28 29 include "utilities/binary/Z.ma". 28 30 29 31 (* To define pointers we need a few details about the memory model. … … 88 90 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y). 89 91 definition shift_offset : offset → int → offset ≝ 90 λo,i. mk_offset (offv o + signedi).92 λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i). 91 93 definition neg_shift_offset : offset → int → offset ≝ 92 λo,i. mk_offset (offv o  signedi).94 λo,i. mk_offset (offv o  Z_of_signed_bitvector ? i). 93 95 definition sub_offset : offset → offset → int ≝ 94 λx,y. repr(offv x  offv y).96 λx,y. bitvector_of_Z ? (offv x  offv y). 95 97 definition zero_offset ≝ mk_offset OZ. 96 98 definition lt_offset : offset → offset → bool ≝ … … 321 323 ]. 322 324 323 definition zero_ext ≝ λnbits: Z. λv: val.325 definition zero_ext ≝ λnbits: nat. λv: val. 324 326 match v with 325 327 [ Vint n ⇒ Vint (zero_ext nbits n) … … 327 329 ]. 328 330 329 definition sign_ext ≝ λnbits: Z. λv:val.331 definition sign_ext ≝ λnbits:nat. λv:val. 330 332 match v with 331 333 [ Vint i ⇒ Vint (sign_ext nbits i) … … 343 345 match v1 with 344 346 [ Vint n1 ⇒ match v2 with 345 [ Vint n2 ⇒ Vint (add n1 n2)347 [ Vint n2 ⇒ Vint (addition_n ? n1 n2) 346 348  Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1) 347 349  _ ⇒ Vundef ] … … 354 356 match v1 with 355 357 [ Vint n1 ⇒ match v2 with 356 [ Vint n2 ⇒ Vint (sub n1 n2)358 [ Vint n2 ⇒ Vint (subtraction ? n1 n2) 357 359  _ ⇒ Vundef ] 358 360  Vptr r1 b1 p1 ofs1 ⇒ match v2 with … … 1205 1207 qed. 1206 1208 1207 (* 1208 Lemma zero_ext_lessdef: 1209 forall n v1 v2, lessdef v1 v2 > lessdef (zero_ext n v1) (zero_ext n v2). 1210 Proof. 1211 intros; inv H; simpl; auto. 1212 Qed. 1213 *) 1209 lemma zero_ext_lessdef: 1210 ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2). 1211 #n #v1 #v2 #H inversion H // #v #E1 #E2 destruct // 1212 qed. 1213 1214 1214 lemma sign_ext_lessdef: 1215 1215 ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
Note: See TracChangeset
for help on using the changeset viewer.