Changeset 2176 for src/common/Pointers.ma
 Timestamp:
 Jul 12, 2012, 1:28:28 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Pointers.ma
r1882 r2176 43 43 qed. 44 44 45 (* This is only required for full 8051 memory spaces. 46 45 47 (* Characterise the memory regions which the pointer representations can 46 48 address. … … 61 63 definition is_pointer_compat : block → region → bool ≝ 62 64 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true  inr _ ⇒ false ]. 65 *) 63 66 64 67 (* Offsets into the block. We allow integers like CompCert so that we have … … 91 94 (*CSC: use this definition everywhere in Values.ma and Mem.ma. *) 92 95 record pointer: Type[0] ≝ { 93 ptype: region; 96 (* ptype: region;*) 94 97 pblock: block; 95 pok: pointer_compat pblock ptype; 98 (* pok: pointer_compat pblock ptype;*) 96 99 poff: offset 97 100 }. 98 101 102 (* As we don't have full memory space support, grab the region from the block 103 instead. *) 104 definition ptype : pointer → region ≝ λp. block_region (pblock p). 105 99 106 definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝ 100 λn,p,i. mk_pointer ( ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).107 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i). 101 108 102 109 (* multiply shift by a nat (i.e., sizeof) without danger of overflow *) 103 110 definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝ 104 λn,p,i,j. mk_pointer ( ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).111 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j). 105 112 106 113 definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝ 107 λn,p,i. mk_pointer ( ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).114 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i). 108 115 109 116 definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝ 110 λn,p,i,j. mk_pointer ( ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).117 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j). 111 118 112 119 definition eq_pointer: pointer → pointer → bool ≝ 113 120 λp1,p2. 114 eq_region (ptype p1) (ptype p2) ∧(eq_block (pblock p1) (pblock p2)) ∧121 (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧ 115 122 eq_offset (poff p1) (poff p2). 116 123 … … 121 128 lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1. 122 129 (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1). 123 #P * # r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1130 #P * #b0 * #o0 * #b1 * #o1 124 131 #Ptrue #Pfalse 125 132 whd in match (eq_pointer ??); 126 @eq_region_elim #reg_eq 127 [ @eq_block_elim #block_eq 128 [ change with (eqZb ??) in match (eq_offset ??); 129 @eqZb_elim #offset_eq 130 [ destruct @Ptrue % 131 ] 133 @eq_block_elim #block_eq 134 [ change with (eqZb ??) in match (eq_offset ??); 135 @eqZb_elim #offset_eq 136 [ destruct @Ptrue % 132 137 ] 133 138 ]
Note: See TracChangeset
for help on using the changeset viewer.