Changeset 2275 for src/common
 Timestamp:
 Jul 30, 2012, 1:05:55 PM (8 years ago)
 Location:
 src/common
 Files:

 1 edited
 1 copied
Legend:
 Unmodified
 Added
 Removed

src/common/ByteValues.ma
r2176 r2275 4 4 5 5 include "common/Pointers.ma". 6 include "ASM/I8051.ma". 7 include "ASM/BitVectorTrie.ma". 6 8 7 9 record part (*r: region*): Type[0] ≝ … … 74 76 [ O ⇒ λ_.[] 75 77  S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n). 76 /3/ (*Andrea: by _ cannot be reparsed*) qed. 78 <pr >pr' <plus_n_Sm_fast 79 // qed. 77 80 78 81 definition bevals_of_pointer: pointer → list beval ≝ … … 164 167 definition BVfalse: beval ≝ BVByte (zero …). 165 168 definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse. 169 170 definition hw_register_env ≝ BitVectorTrie beval 6. 171 definition empty_hw_register_env: hw_register_env ≝ Stub …. 172 definition hwreg_retrieve: hw_register_env → Register → beval ≝ 173 λenv,r. lookup … (bitvector_of_register r) env BVundef. 174 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝ 175 λr,v,env. insert … (bitvector_of_register r) v env. 
src/common/ByteValues_paolo.ma
r2233 r2275 4 4 5 5 include "common/Pointers.ma". 6 include "ASM/I8051.ma". 7 include "ASM/BitVectorTrie.ma". 6 8 7 9 record part (*r: region*): Type[0] ≝ … … 24 26 inductive beval: Type[0] ≝ 25 27  BVundef: beval 28  BVnonzero: beval 26 29  BVByte: Byte → beval 27 30  BVnull: (*∀r:region.*) part → beval 28  BVptr: ∀p:pointer. part (*ptype p*) → beval. 31  BVptr: block → ∀p:part.Vector Byte (S p) → beval. 32 33 include "utilities/hide.ma". 29 34 30 35 definition eq_beval: beval → beval → bool ≝ … … 32 37 match v1 with 33 38 [ BVundef ⇒ match v2 with [ BVundef ⇒ true  _ ⇒ false ] 39  BVnonzero ⇒ match v2 with [ BVnonzero ⇒ true  _ ⇒ false ] 34 40  BVByte b1 ⇒ match v2 with [ BVByte b2 ⇒ eq_bv … b1 b2  _ ⇒ false ] 35 41  BVnull p1 ⇒ match v2 with [ BVnull p2 ⇒ eqb p1 p2  _ ⇒ false ] 36  BVptr P1 p1 ⇒ match v2 with [ BVptr P2 p2 ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2  _ ⇒ false ]]. 37 38 axiom CorruptedValue: String. 39 40 let rec pointer_of_bevals_aux (p:pointer) (part: nat) (l: list beval) on l : res pointer ≝ 42  BVptr b1 p1 o1 ⇒ 43 match v2 with 44 [ BVptr b2 p2 o2 ⇒ 45 eq_block … b1 b2 ∧ eqb p1 p2 ∧ 46 (* equivalent to equality if p1 = p2 *) 47 subvector_with … (eq_bv 8) o1 o2 48  _ ⇒ false 49 ] 50 ]. 51 52 include alias "arithmetics/nat.ma". 53 54 lemma commutative_plus_fast : commutative ? plus. 55 #n elim n [ @plus_n_O ] 56 #n' #IH #m <plus_n_Sm_fast <IH % 57 qed. 58 59 lemma distributive_times_plus_fast : distributive ? times plus. 60 #n elim n [ #m #p % ] 61 #n' #IH #m #p normalize 62 >IH 63 >associative_plus in ⊢ (???%); 64 <(associative_plus ? p) in ⊢ (???%); 65 >(commutative_plus_fast ? p) in ⊢ (???%); 66 >(associative_plus p) 67 @associative_plus 68 qed. 69 70 axiom CorruptedPointer: String. 71 72 let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝ 73 match v return λn.λ_ : Vector ? n.Vector ? (n * m) with 74 [ VEmpty ⇒ VEmpty ? 75  VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl 76 ]. 77 78 lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m. 79 #n elim n n 80 [ #m % ] 81 #n #IH #m normalize <IH 82 <associative_plus >(commutative_plus_fast n) 83 >associative_plus >IH % 84 qed. 85 86 lemma commutative_times_fast : commutative ? times. 87 #n elim n n 88 [ #m <times_n_O % ] 89 #n #IH #m normalize <times_n_Sm_fast >IH % 90 qed. 91 92 let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8)) 93 (l: list beval) on l : res pointer ≝ 41 94 match l with 42 95 [ nil ⇒ 43 if eqb part (size_pointer (*ptype p*)) then44 OK … p96 If eqb part (size_pointer (*ptype p*)) then with prf do 97 return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉)) 45 98 else 46 Error … [MSG Corrupted Value]99 Error … [MSG CorruptedPointer] 47 100  cons v tl ⇒ 48 101 match v with 49 [ BVptr p' part' ⇒ 50 if eq_pointer p p' ∧ eqb part part' then 51 pointer_of_bevals_aux p (S part) tl 102 [ BVptr b' part' o' ⇒ 103 let acc' ≝ vflatten … o' in 104 if eq_block b b' ∧ 105 eqb part part' ∧ 106 subvector_with ??? eq_b acc acc' then 107 pointer_of_bevals_aux b (S part') acc' tl 52 108 else 53 Error … [MSG CorruptedValue] 54  _ ⇒ Error … [MSG CorruptedValue]]]. 55 56 axiom NotAPointer: String. 109 Error … [MSG CorruptedPointer] 110  _ ⇒ Error … [MSG CorruptedPointer] 111 ] 112 ]. 113 @hide_prf 114 >commutative_times_fast 115 lapply prf @(eqb_elim part) #H * >H % qed. 57 116 58 117 (* CSC: use vectors in place of lists? Or even better products of tuples … … 61 120 λl. 62 121 match l with 63 [ nil ⇒ Error … [MSG NotAPointer]122 [ nil ⇒ Error … [MSG CorruptedPointer] 64 123  cons he tl ⇒ 65 124 match he with 66 [ BVptr p part ⇒ 67 if eqb part 0 then pointer_of_bevals_aux p 1 tl else Error … [MSG NotAPointer] 68  _ ⇒ Error … [MSG NotAPointer]]]. 69 125 [ BVptr b part o ⇒ 126 if eqb part 0 then 127 pointer_of_bevals_aux b (S part) (vflatten … o) tl 128 else Error … [MSG CorruptedPointer] 129  _ ⇒ Error … [MSG CorruptedPointer] 130 ] 131 ]. 132 133 let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝ 134 match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with 135 [ O ⇒ λ_.VEmpty ? 136  S k ⇒ 137 λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in 138 pre ::: rvsplit … post 139 ]. 70 140 (* CSC: use vectors in place of lists? Or even better products of tuples 71 141 (more easily pattern matchable in the finite case)? *) 72 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (*ptype p*)) on n:list beval ≝142 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝ 73 143 match n with 74 144 [ O ⇒ λ_.[] 75  S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n). 76 /3/ (*Andrea: by _ cannot be reparsed*) qed. 145  S m ⇒ λpr': S m + part = ?. 146 let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in 147 (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ? 148 ]. 149 @hide_prf 150 [3: change with (?*?) in match offset_size; 151 <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8) 152 <distributive_times_plus_fast <plus_n_Sm_fast % 153 ] postfix 154 /3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed. 77 155 78 156 definition bevals_of_pointer: pointer → list beval ≝ 79 157 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) …. 80 // qed. 158 @hide_prf @plus_n_O qed. 159 160 lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v. 161 #A #n elim n n 162 [ #m #v >(Vector_O ? v) % 163  #n #IH #m #v 164 whd in match (rvsplit ????); 165 @vsplit_elim #pre #post #EQ 166 normalize nodelta 167 whd in match (vflatten ????); >IH >EQ % 168 ] 169 qed. 170 171 lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m. 172 v @@ u = v' @@ u' → v = v' ∧ u = u'. 173 #A #n #m #v elim v n 174 [ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} % 175  #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' v' 176 #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''} 177 >EQ' % 178 ] 179 qed. 180 181 lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v. 182 #A #n #m #v elim v n 183 [ % 184  #n #hd #tl #IH 185 whd in match (vflatten ????); 186 whd in match (rvsplit ????); 187 @vsplit_elim #pre #post #EQ 188 elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2 189 normalize nodelta >IH % 190 ] 191 qed. 192 81 193 82 194 lemma pointer_of_bevals_bevals_of_pointer: 83 195 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p. 84 * #pbl #poff 85 try % 86 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) (*[2,3: %]*) 87 whd in ⊢ (??%?);(* >reflexive_eq_pointer >(eqb_n_n 2)*) % 196 * #pbl * #voff 197 whd in match (bevals_of_pointer ?); 198 @vsplit_elim #pre #post 199 normalize nodelta 200 #EQ >EQ 201 whd in match (bevals_of_pointer_aux ????); 202 @vsplit_elim #pre' #post' 203 normalize nodelta 204 >(Vector_O … pre') #EQ' normalize in EQ'; <EQ' pre' post' 205 whd in ⊢ (??%?); 206 >eq_block_b_b >eqb_n_n 207 >vflatten_rvsplit >vflatten_rvsplit 208 >(subvector_with_refl0 … post ? pre) [2: * %] 209 normalize nodelta % 88 210 qed. 89 211 … … 134 256 λv.match v with 135 257 [ BVundef ⇒ Error … [MSG ValueNotABoolean] 258  BVnonzero ⇒ OK … true 136 259  BVByte b ⇒ OK … (eq_bv … (zero …) b) 137 260  BVnull y ⇒ OK … false 138  BVptr p q ⇒ OK ? true ]. 139 140 axiom BadByte: String. 141 142 definition Byte_of_val: beval → res Byte ≝ (*CSC: move elsewhere *) 143 λb.match b with 261  BVptr p q o ⇒ OK ? true ]. 262 263 definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *) 264 λerr,b.match b with 144 265 [ BVByte b ⇒ OK … b 145  _ ⇒ Error … [MSG BadByte]].266  _ ⇒ Error … [MSG err]]. 146 267 147 268 axiom NotAnInt32Val: String. … … 151 272 match l with 152 273 [ nil ⇒ Error ? [MSG NotAnInt32Val] 153  cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in274  cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in 154 275 do 〈b1,l〉 ← first_byte l ; 155 276 do 〈b2,l〉 ← first_byte l ; … … 160 281  _ ⇒ Error ? [MSG NotAnInt32Val] ]. 161 282 162 (* CSC: maybe we should introduce a type of 1bitsized values *) 163 definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]]. 164 definition BVfalse: beval ≝ BVByte (zero …). 165 definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse. 283 inductive bebit : Type[0] ≝ 284  BBbit : bool → bebit 285  BBundef : bebit 286  BBptrcarry : 287 (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit. 288 289 definition eq_bebit: bebit → bebit → bool ≝ 290 λv1,v2. 291 match v1 with 292 [ BBundef ⇒ match v2 with [ BBundef ⇒ true  _ ⇒ false ] 293  BBbit b1 ⇒ match v2 with [ BBbit b2 ⇒ eq_b b1 b2  _ ⇒ false ] 294  BBptrcarry is_add1 b1 p1 o1 by1 ⇒ 295 match v2 with 296 [ BBptrcarry is_add2 b2 p2 o2 by2 ⇒ 297 eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧ 298 (* equivalent to equality if p1 = p2 *) 299 subvector_with … (eq_bv 8) o1 o2 ∧ 300 subvector_with … (eq_bv 8) by1 by2 301  _ ⇒ false 302 ] 303 ]. 304 305 axiom UnsupportedOp : String. 306 307 definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝ 308 λop,a,b. 309 ! a' ← Byte_of_val UnsupportedOp a ; 310 ! b' ← Byte_of_val UnsupportedOp b ; 311 let 〈a'',b''〉 ≝ opaccs eval op a' b' in 312 return 〈BVByte a'', BVByte b''〉. 313 314 definition be_op1 : Op1 → beval → res beval ≝ 315 λop,a. 316 ! a' ← Byte_of_val UnsupportedOp a ; 317 return BVByte (op1 eval op a'). 318 319 definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *) 320 λerr,b.match b with 321 [ BBbit b ⇒ OK … b 322  _ ⇒ Error … [MSG err]]. 323 324 definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝ 325 λop,n,carry. 326 let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit. 327 let 〈res_tl, carry〉 ≝ pr in 328 let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in 329 〈res_hd ::: res_tl, carry'〉 in 330 fold_right2_i … f 〈[[ ]],carry〉 n. 331 332 definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝ 333 λis_add,carry,a1,b2. 334 let op ≝ if is_add then Addc else Sub in 335 match a1 with 336 [ BVByte b1 ⇒ 337 ! carry' ← Bit_of_val UnsupportedOp carry ; 338 let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in 339 return 〈BVByte rslt, BBbit carry''〉 340  BVptr b p o ⇒ 341 match p with 342 [ O ⇒ λ_:0<size_pointer.λo : Vector Byte 1. 343 if eq_bebit carry (BBbit false) then 344 let o' ≝ from_singl … o in 345 let 〈rslt,carry〉 ≝ op2 eval false op b2 o' in 346 let p' : part ≝ mk_part 0 ? in 347 return 〈BVptr b p' [[rslt]], BBptrcarry is_add b p' o [[b2]]〉 348 else 349 Error … [MSG UnsupportedOp] 350  S k ⇒ λSk_ok:S k<size_pointer.λo : Vector Byte (S (S k)). 351 match carry with 352 [ BBptrcarry is_add' b' p' o' by' ⇒ 353 if eq_b is_add is_add' ∧ eq_block b b' ∧ subvector_with … (eq_bv 8) o' o then 354 If eqb k p' then with prf do 355 let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in 356 let 〈rslt,ignore〉 ≝ op2_bytes op … false o (b2 ::: by') in 357 let Sk_part ≝ mk_part (S k) Sk_ok in 358 OK … 〈BVptr b Sk_part rslt, 359 BBptrcarry is_add b Sk_part o (b2 ::: by')〉 360 else Error … [MSG UnsupportedOp] 361 else Error … [MSG UnsupportedOp] 362  _ ⇒ Error … [MSG UnsupportedOp] 363 ] 364 ] (part_no_ok p) o 365  _ ⇒ Error … [MSG UnsupportedOp] 366 ]. 367 @hide_prf [//] 368 lapply prf @eqb_elim #H * >H % 369 qed. 370 371 (* This tables shows what binary ops may be defined on bevals depending on 372 the arguments (columns marked by 1st argument, rows by 2nd). Further 373 checks for definedness are done for pointer parts taking into account 374 blocks, parts and the carry value. 375  BVByte  BVptr  BVnull  BVnonzero  BVundef  376 +++++ 377 BVByte  all  Add, Addc, Sub  none  Or  none  378 +++++ 379 BVptr  Add, Addc  Sub, Xor  Xor  none  none  380 +++++ 381 BVnull  none  Xor  Xor  none  none  382 +++++ 383 BVnonzero  Or  none  none  Or  none  384 +++++ 385 BVundef  none  none  none  none  none  386 + 387 *) 388 definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝ 389 λcarry,op,a1,a2. 390 match a1 with 391 [ BVByte b1 ⇒ 392 match a2 with 393 [ BVByte b2 ⇒ 394 ! carry ← Bit_of_val UnsupportedOp carry ; 395 let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in 396 return 〈BVByte result, BBbit carry〉 397  BVptr bl2 p2 o2 ⇒ 398 match op with 399 [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1 400  Addc ⇒ be_add_sub_byte true carry a2 b1 401  _ ⇒ Error … [MSG UnsupportedOp] 402 ] 403  BVnonzero ⇒ 404 match op with 405 [ Or ⇒ return 〈BVnonzero, carry〉 406  _ ⇒ Error … [MSG UnsupportedOp] 407 ] 408  _ ⇒ Error … [MSG UnsupportedOp] 409 ] 410  BVptr bl1 p1 o1 ⇒ 411 match a2 with 412 [ BVByte b2 ⇒ 413 match op with 414 [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2 415  Addc ⇒ be_add_sub_byte true carry a1 b2 416  Sub ⇒ be_add_sub_byte false carry a1 b2 417  _ ⇒ Error … [MSG UnsupportedOp] 418 ] 419  BVptr bl2 p2 o2 ⇒ 420 match op with 421 [ Sub ⇒ 422 if eq_block bl1 bl2 ∧ eqb p1 p2 then 423 ! carry ← Bit_of_val UnsupportedOp carry ; 424 let by1 ≝ head' … o1 in 425 let by2 ≝ head' … o2 in 426 let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in 427 return 〈BVByte result, BBbit carry〉 428 else Error … [MSG UnsupportedOp] 429  Xor ⇒ 430 if eq_block bl1 bl2 ∧ eqb p1 p2 then 431 if subvector_with … (eq_bv 8) o1 o2 (* equivalent to equality *) then 432 return 〈BVByte (bv_zero …), carry〉 433 else 434 return 〈BVnonzero, carry〉 435 else Error … [MSG UnsupportedOp] 436  _ ⇒ Error … [MSG UnsupportedOp] 437 ] 438  BVnull p2 ⇒ 439 match op with 440 [ Xor ⇒ 441 if eqb p1 p2 then 442 return 〈BVnonzero, carry〉 443 else 444 Error … [MSG UnsupportedOp] 445  _ ⇒ Error … [MSG UnsupportedOp] 446 ] 447  _ ⇒ Error … [MSG UnsupportedOp] 448 ] 449  BVnonzero ⇒ 450 match op with 451 [ Or ⇒ 452 match a2 with 453 [ BVByte _ ⇒ return 〈BVnonzero, carry〉 454  BVnonzero ⇒ return 〈BVnonzero, carry〉 455  _ ⇒ Error … [MSG UnsupportedOp] 456 ] 457  _ ⇒ Error … [MSG UnsupportedOp] 458 ] 459  BVnull p1 ⇒ 460 match op with 461 [ Xor ⇒ 462 match a2 with 463 [ BVptr _ p2 _ ⇒ 464 if eqb p1 p2 then 465 return 〈BVnonzero, carry〉 466 else 467 Error … [MSG UnsupportedOp] 468  BVnull p2 ⇒ 469 if eqb p1 p2 then 470 return 〈BVByte (bv_zero …), carry〉 471 else 472 Error … [MSG UnsupportedOp] 473  _ ⇒ Error … [MSG UnsupportedOp] 474 ] 475  _ ⇒ Error … [MSG UnsupportedOp] 476 ] 477  _ ⇒ Error … [MSG UnsupportedOp] 478 ]. 479 480 record hw_register_env : Type[0] ≝ 481 { reg_env : BitVectorTrie beval 6 482 ; carry_bit : bebit 483 ; other_bit : bebit 484 }. 485 486 definition empty_hw_register_env: hw_register_env ≝ 487 mk_hw_register_env (Stub …) BBundef BBundef. 488 489 definition hwreg_retrieve: hw_register_env → Register → beval ≝ 490 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef. 491 492 definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝ 493 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env)) 494 (carry_bit env) (other_bit env). 495 496 definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝ 497 λv,env.mk_hw_register_env (reg_env env) v (other_bit env). 498 499 definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝ 500 λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v. 501 502
Note: See TracChangeset
for help on using the changeset viewer.