Ignore:
Timestamp:
Feb 2, 2011, 12:41:05 PM (9 years ago)
Author:
campbell
Message:

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Mem.ma

    r484 r485  
    719719  [ Vptr psp b ofs ⇒ store chunk m psp b (signed ofs) v
    720720  | _ ⇒ None ? ].
    721 
    722 
    723 (* Build a block filled with the given initialization data. *)
    724 ndefinition contents_init_data_step :
    725   Z → init_data → (Z → contentmap) → contentmap ≝
    726   λpos,data,reccall.
    727   match data with
    728   [ Init_int8 n ⇒
    729       setN 0 pos (Vint n) (reccall (pos + oneZ))
    730   | Init_int16 n ⇒
    731       setN 1 pos (Vint n) (reccall (pos + oneZ))
    732   | Init_int32 n ⇒
    733       setN 3 pos (Vint n) (reccall (pos + oneZ))
    734   | Init_float32 f ⇒
    735       setN 3 pos (Vfloat f) (reccall (pos + oneZ))
    736   | Init_float64 f ⇒
    737       setN 7 pos (Vfloat f) (reccall (pos + oneZ))
    738   | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)
    739   | Init_null r ⇒ setN (pred_size_pointer r) pos (Vnull r) (reccall (pos + oneZ))
    740   | Init_addrof s n ⇒
    741       (* Not handled properly yet *)
    742       reccall (pos + 4)
    743   | Init_pointer x ⇒
    744       (* Not handled properly yet *)
    745       reccall (pos + 4)].
    746 
    747 nlet rec contents_init_data (pos: Z) (i_data: list init_data) on i_data
    748   : contentmap ≝
    749   match i_data with
    750   [ nil ⇒ (λ_.Undef)
    751   | cons data i_data' ⇒
    752       contents_init_data_step pos data (λn.contents_init_data n i_data') ].
    753 
    754 ndefinition size_init_data : init_data → Z ≝
    755  λi_data.match i_data with
    756   [ Init_int8 _ ⇒ 1
    757   | Init_int16 _ ⇒ 2
    758   | Init_int32 _ ⇒ 4
    759   | Init_float32 _ ⇒ 4
    760   | Init_float64 _ ⇒ 8
    761   | Init_space n ⇒ Zmax n 0
    762   | Init_null r ⇒ size_pointer r
    763   | Init_addrof _ _ ⇒ 4
    764   | Init_pointer _ ⇒ Z_of_nat (*** can't use implicit coercion??? *)4].
    765 
    766 ndefinition size_init_data_list : list init_data → Z ≝
    767   λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
    768 
    769 (* Nonessential properties that may require arithmetic
    770 nremark size_init_data_list_pos:
    771   ∀i_data. OZ ≤ size_init_data_list i_data.
    772 #i_data;nelim i_data;//;
    773 #a;#tl;ncut (OZ ≤ size_init_data a)
    774 ##[ncases a;nnormalize;//;
    775    #x;ncases x;nnormalize;//;
    776 ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
    777    ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
    778    ##[ncases (size_init_data a) in Hsize IH;
    779       ##[##1,2:/3/
    780       ##|nnormalize;#n;#Hfalse;nelim Hfalse]
    781    ##|#Hdisc;ncases Hdisc
    782       ##[#Heq;nrewrite > Heq;//;
    783       ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
    784          (* TODO: arithmetics *) napply daemon]
    785    ##]
    786 ##]
    787 nqed.
    788 *)
    789 
    790 ndefinition block_init_data : list init_data → region → block_contents ≝
    791   λi_data,bcl.mk_block_contents
    792     OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.
    793 
    794 ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
    795   λm,i_data,bcl.
    796   〈mk_mem (update ? (nextblock m)
    797                  (block_init_data i_data bcl)
    798                  (blocks m))
    799          (Zsucc (nextblock m))
    800          (succ_nextblock_pos m),
    801    (nextblock m)〉.
    802 
    803 nremark block_init_data_empty:
    804   ∀bcl. block_init_data [ ] bcl = empty_block OZ OZ bcl.
    805 //;
    806 nqed.
    807721
    808722(* * Properties of the memory operations *)
Note: See TracChangeset for help on using the changeset viewer.