Changeset 2435 for src/common/ByteValues.ma
 Timestamp:
 Nov 6, 2012, 4:12:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ByteValues.ma
r2286 r2435 11 11 }. 12 12 13 definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝ 14 λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig). 15 16 coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝ 17 part_from_sig on _n_sig:Σn.n<size_pointer to part. 18 13 19 (* Bytesized values used in the backend. 14 20 Values larger than a single Byte are represented via their parts. … … 21 27  the [BVundef] value denoting an arbitrary bit pattern, such as the 22 28 value of an uninitialized variable 23  the [BVnonzero] value denoting an arbitrary but nonzero bit pattern, 24 which arise in the RTLabs → RTL pass when translating equality comparisons 25 between pointers (which get translated to multiple XORs between pointer 26 parts). 29  [BVXor] is a formal XOR between (possibly null) pointer parts 30  [BVnonzero] is any nonzero value 27 31 *) 28 32 … … 30 34  BVundef: beval 31 35  BVnonzero: beval 36  BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *) 32 37  BVByte: Byte → beval 33 38  BVnull: (*∀r:region.*) part → beval 34  BVptr: block → ∀p:part.Vector Byte (S p)→ beval.39  BVptr: pointer → part → beval. 35 40 36 definition eq_beval: beval → beval → bool ≝ 37 λv1,v2. 38 match v1 with 39 [ BVundef ⇒ match v2 with [ BVundef ⇒ true  _ ⇒ false ] 40  BVnonzero ⇒ match v2 with [ BVnonzero ⇒ true  _ ⇒ false ] 41  BVByte b1 ⇒ match v2 with [ BVByte b2 ⇒ eq_bv … b1 b2  _ ⇒ false ] 42  BVnull p1 ⇒ match v2 with [ BVnull p2 ⇒ eqb p1 p2  _ ⇒ false ] 43  BVptr b1 p1 o1 ⇒ 44 match v2 with 45 [ BVptr b2 p2 o2 ⇒ 46 eq_block … b1 b2 ∧ eqb p1 p2 ∧ 47 (* equivalent to equality if p1 = p2 *) 48 vprefix … (eq_bv 8) o1 o2 49  _ ⇒ false 50 ] 51 ]. 41 definition eq_bv_suffix : ∀n,m,p. 42 BitVector (n + p) → BitVector (m + p) → bool ≝ 43 λn,m,p,v1,v2. 44 let b1 ≝ \snd (vsplit … v1) in 45 let b2 ≝ \snd (vsplit … v2) in 46 eq_bv … b1 b2. 52 47 53 48 include alias "arithmetics/nat.ma". 54 49 55 50 axiom CorruptedPointer: String. 56 57 let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8))58 (l: list beval) on l : res pointer ≝59 match l with60 [ nil ⇒61 If eqb part (size_pointer (*ptype p*)) then with prf do62 return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉))63 else64 Error … [MSG CorruptedPointer]65  cons v tl ⇒66 match v with67 [ BVptr b' part' o' ⇒68 let acc' ≝ vflatten … o' in69 if eq_block b b' ∧70 eqb part part' ∧71 vsuffix … eq_b acc acc' then72 pointer_of_bevals_aux b (S part') acc' tl73 else74 Error … [MSG CorruptedPointer]75  _ ⇒ Error … [MSG CorruptedPointer]76 ]77 ].78 @hide_prf79 >commutative_times_fast80 lapply prf @(eqb_elim part) #H * >H % qed.81 51 82 52 (* CSC: use vectors in place of lists? Or even better products of tuples … … 86 56 match l with 87 57 [ nil ⇒ Error … [MSG CorruptedPointer] 88  cons he tl ⇒ 89 match he with 90 [ BVptr b part o ⇒ 91 if eqb part 0 then 92 pointer_of_bevals_aux b (S part) (vflatten … o) tl 93 else Error … [MSG CorruptedPointer] 94  _ ⇒ Error … [MSG CorruptedPointer] 58  cons bv1 tl ⇒ 59 match tl with 60 [ nil ⇒ Error … [MSG CorruptedPointer] 61  cons bv2 tl' ⇒ 62 match tl' with 63 [ cons _ _ ⇒ Error … [MSG CorruptedPointer] 64  nil ⇒ 65 match bv1 with 66 [ BVptr ptr1 p1 ⇒ 67 match bv2 with 68 [ BVptr ptr2 p2 ⇒ 69 if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧ 70 eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2)) 71 then 72 return ptr2 73 else Error … [MSG CorruptedPointer] 74  _ ⇒ Error … [MSG CorruptedPointer] 75 ] 76  _ ⇒ Error … [MSG CorruptedPointer] 77 ] 95 78 ] 79 ] 96 80 ]. 97 81 98 (* CSC: use vectors in place of lists? Or even better products of tuples 99 (more easily pattern matchable in the finite case)? *) 100 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝ 101 match n with 102 [ O ⇒ λ_.[] 103  S m ⇒ λpr': S m + part = ?. 104 let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in 105 (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ? 106 ]. 107 @hide_prf 108 [3: change with (?*?) in match offset_size; 109 <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8) 110 <distributive_times_plus_fast <plus_n_Sm_fast % 111 ] postfix 112 /3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed. 113 114 definition bevals_of_pointer: pointer → list beval ≝ 115 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) …. 116 @hide_prf @plus_n_O qed. 82 definition bevals_of_pointer ≝ 83 λp:pointer. 84 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer). 117 85 118 86 lemma pointer_of_bevals_bevals_of_pointer: 119 87 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p. 120 * #pbl * #voff 88 #ptr 121 89 whd in match (bevals_of_pointer ?); 122 @vsplit_elim #pre #post123 normalize nodelta124 #EQ >EQ125 whd in match (bevals_of_pointer_aux ????);126 @vsplit_elim #pre' #post'127 normalize nodelta128 >(Vector_O … pre') #EQ' normalize in EQ'; <EQ' pre' post'129 90 whd in ⊢ (??%?); 130 >eq_block_b_b >eqb_n_n 131 >vflatten_rvsplit >vflatten_rvsplit 132 >vsuffix_true 133 [2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ] 134 normalize nodelta % 91 >eq_block_b_b 92 change with (eq_bv ???) in match (eq_bv_suffix ?????); 93 >eq_bv_refl % 135 94 qed. 136 95 … … 146 105 (* Fails if the address is not representable as a pair *) 147 106 definition beval_pair_of_pointer: pointer → res (beval × beval) ≝ 148 λp. OK … (list_to_pair … (bevals_of_pointer p) ?).107 λp. OK … (list_to_pair … (bevals_of_pointer p) (refl …)). 149 108 (* 150 109 λp. match p with [ mk_pointer pty pbl pok poff ⇒ … … 153 112  Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?) 154 113  _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*) 155 % qed.156 114 157 115 definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝ 158 λp. list_to_pair ? (bevals_of_pointer p) ?.116 λp. list_to_pair ? (bevals_of_pointer p) (refl …). 159 117 (* 160 118 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒ … … 162 120 [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ? 163 121  _ ⇒ λpok'.λabs. ⊥] pok] ?. 164 [@(pi2 … p) 7: // 8: %] destruct (abs)*) % 165 qed. 166 122 [@(pi2 … p) 7: // 8: %] destruct (abs)*) 167 123 168 124 axiom NotACodePointer: String. … … 172 128 do p ← pointer_of_bevals [v1;v2] ; 173 129 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with 174 [ Code ⇒ λE.OK ? (mk_Sig … p ?) 175  _ ⇒ λ_.Error … [MSG NotACodePointer]] ?. 176 // qed. 130 [ Code ⇒ λE.OK ? (mk_Sig … p E) 131  _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). 177 132 178 133 axiom ValueNotABoolean: String. … … 181 136 λv.match v with 182 137 [ BVundef ⇒ Error … [MSG ValueNotABoolean] 183  BVnonzero ⇒ OK … true 138  BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can 139 tell the value, we will always 140 call bool_of_beval after a 141 series of XORs has been 142 completed *) 184 143  BVByte b ⇒ OK … (eq_bv … (zero …) b) 185  BVnull y ⇒ OK … false 186  BVptr p q o ⇒ OK ? true ]. 144  BVnull _ ⇒ OK … false 145  _ ⇒ OK ? true 146 ]. 187 147 188 148 definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *) … … 210 170  BBundef : bebit 211 171  BBptrcarry : 212 (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit. 213 214 definition eq_bebit: bebit → bebit → bool ≝ 215 λv1,v2. 216 match v1 with 217 [ BBundef ⇒ match v2 with [ BBundef ⇒ true  _ ⇒ false ] 218  BBbit b1 ⇒ match v2 with [ BBbit b2 ⇒ eq_b b1 b2  _ ⇒ false ] 219  BBptrcarry is_add1 b1 p1 o1 by1 ⇒ 220 match v2 with 221 [ BBptrcarry is_add2 b2 p2 o2 by2 ⇒ 222 eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧ 223 (* equivalent to equality if p1 = p2 *) 224 vprefix … (eq_bv 8) o1 o2 ∧ 225 vprefix … (eq_bv 8) by1 by2 226  _ ⇒ false 227 ] 228 ]. 172 (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit. 229 173 230 174 definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
Note: See TracChangeset
for help on using the changeset viewer.