Changeset 1874 for src/common
 Timestamp:
 Apr 4, 2012, 6:48:25 PM (9 years ago)
 Location:
 src/common
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndVal.ma
r1873 r1874 1 1 include "common/Values.ma". 2 2 include "joint/BEValues.ma". 3 include "common/Mem.ma".4 3 5 4 (* Transform between lists of "backend" (i.e., byte by byte) values and the … … 7 6 resolve the sizes; they are not strictly checked. *) 8 7 9 let rec make_parts (r:region) (n:nat) (H:le n (size_pointerr)) on n : list (part r) ≝10 match n return λn.l en ? → ? with11 [ O ⇒ λ _. [ ]12  S m ⇒ λH'. m k_part r n H::(make_parts r m ?)8 let rec make_parts_aux (r:region) (n:nat) (H:lt n (size_pointer r)) (tl:list (part r)) on n : list (part r) ≝ 9 match n return λn.lt n ? → ? with 10 [ O ⇒ λH'. (mk_part r O H')::tl 11  S m ⇒ λH'. make_parts_aux r m ? ((mk_part r n H)::tl) 13 12 ] H. 14 13 /2/ 15 14 qed. 16 15 17 definition make_ be_null : region → list beval≝18 λr. ma p ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?).16 definition make_parts : ∀r:region. list (part r) ≝ 17 λr. make_parts_aux r (pred (size_pointer r)) ? [ ]. 19 18 // 20 19 qed. 20 21 definition make_be_null : region → list beval ≝ 22 λr. map ?? (λp. BVnull r p) (make_parts r). 21 23 22 24 let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝ 
src/common/Globalenvs.ma
r1872 r1874 404 404 addresses of the memory region in question  here there are no real 405 405 pointers, so use the real region. *) 406 let r ≝ block_region m bin406 let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in 407 407 match id with 408 [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m r b p(Vint I8 n)409  Init_int16 n ⇒ store (ASTint I16 Unsigned) m r b p(Vint I16 n)410  Init_int32 n ⇒ store (ASTint I32 Unsigned) m r b p(Vint I32 n)411  Init_float32 n ⇒ store (ASTfloat F32) m r b p(Vfloat n)412  Init_float64 n ⇒ store (ASTfloat F64) m r b p(Vfloat n)408 [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n) 409  Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n) 410  Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n) 411  Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n) 412  Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n) 413 413  Init_addrof r' symb ofs ⇒ 414 414 match (*find_symbol ge symb*) symbols ? ge symb with … … 416 416  Some b' ⇒ 417 417 match pointer_compat_dec b' r' with 418 [ inl pc ⇒ store (ASTptr r') m r b p(Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))418 [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))) 419 419  inr _ ⇒ None ? 420 420 ] 421 421 ] 422 422  Init_space n ⇒ Some ? m 423  Init_null r' ⇒ store (ASTptr r') m r b p(Vnull r')423  Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r') 424 424 ]. 425 cases b // 426 qed. 425 427 426 428 definition size_init_data : init_data → nat ≝ … … 471 473 *) 472 474 475 (* TODO: why doesn't this use alloc? *) 473 476 definition alloc_init_data : mem → list init_data → region → mem × block ≝ 474 477 λm,i_data,r. 475 let b ≝ mk_block r (nextblock m) in476 〈mk_mem (update_block ? b477 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))478 (blocks m))479 (Zsucc (nextblock m))480 (succ_nextblock_pos m),478 let b ≝ mk_block r (nextblock ? m) in 479 〈mk_mem ? (update_block ? b 480 (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef)) 481 (blocks ? m)) 482 (Zsucc (nextblock ? m)) 483 (succ_nextblock_pos ? m), 481 484 b〉. 482 485 … … 520 523 λF,V,init_info,p. 521 524 add_globals … init_info 522 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem 〉525 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?〉 523 526 (prog_vars ?? p). 524 527 
src/common/Mem.ma
r1872 r1874 1 include "joint/BEMem.ma". 2 include "common/FrontEndVal.ma". 3 4 definition mem ≝ bemem. 5 6 let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝ 7 match n with 8 [ O ⇒ Some ? ([ ]) 9  S n' ⇒ 10 match beloadv m ptr with 11 [ None ⇒ None ? 12  Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with 13 [ None ⇒ None ? 14  Some vs ⇒ Some ? (v::vs) ] 15 ] 16 ]. 17 18 definition load : typ → mem → pointer → option val ≝ 19 λt,m,ptr. 20 match loadn m ptr (typesize t) with 21 [ None ⇒ None ? 22  Some vs ⇒ Some ? (be_to_fe_value t vs) 23 ]. 24 25 let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝ 26 match addr with 27 [ Vptr ptr ⇒ load t m ptr 28  _ ⇒ None ? 29 ]. 30 31 let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝ 32 match vs with 33 [ nil ⇒ Some ? m 34  cons v tl ⇒ 35 match bestorev m ptr v with 36 [ None ⇒ None ? 37  Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl 38 ] 39 ]. 40 41 definition store : typ → bemem → pointer → val → option bemem ≝ 42 λt,m,ptr,v. storen m ptr (fe_to_be_values t v). 43 44 definition storev : typ → bemem → val → val → option bemem ≝ 45 λt,m,addr,v. 46 match addr with 47 [ Vptr ptr ⇒ store t m ptr v 48  _ ⇒ None ? ]. 49 50 (* Only used by Clight semantics for pointer comparisons. So in contrast to 51 CompCert, we allow a pointertooneofftheend. *) 52 53 definition valid_pointer : mem → pointer → bool ≝ 54 λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧ 55 Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧ 56 Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)). 57 58 59 (* 1 60 (* *********************************************************************) 2 61 (* *) … … 3518 3577 qed. 3519 3578 *) 3579 *)
Note: See TracChangeset
for help on using the changeset viewer.