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/Globalenvs.ma

    r480 r485  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type. program F V → genv_t F;
     54  globalenv: ∀F,V: Type. program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type. program F V → mem;
     57  init_mem: ∀F,V: Type. program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    396396  foldr ?? (add_funct F) init fns.
    397397
     398(* init *)
     399
     400ndefinition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝
     401λF,ge,m,r,b,p,id.
     402  match id with
     403  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
     404  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
     405  | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
     406  | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
     407  | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     408  | Init_addrof r' symb ofs ⇒
     409      match (*find_symbol ge symb*) symbols ? ge symb with
     410      [ None ⇒ None ?
     411      | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' (snd ?? b') ofs)
     412      ]
     413  | Init_space n ⇒ Some ? m
     414  | Init_null r' ⇒ store (Mpointer r') m r b p (Vnull r')
     415  ].
     416
     417ndefinition size_init_data : init_data → Z ≝
     418 λi_data.match i_data with
     419  [ Init_int8 _ ⇒ 1
     420  | Init_int16 _ ⇒ 2
     421  | Init_int32 _ ⇒ 4
     422  | Init_float32 _ ⇒ 4
     423  | Init_float64 _ ⇒ 8
     424  | Init_space n ⇒ Zmax n 0
     425  | Init_null r ⇒ size_pointer r
     426  | Init_addrof r _ _ ⇒ size_pointer r].
     427
     428nlet rec store_init_data_list (F:Type) (ge:genv F)
     429                              (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data)
     430                              on idl : option mem ≝
     431  match idl with
     432  [ nil ⇒ Some ? m
     433  | cons id idl' ⇒
     434      match store_init_data F ge m r b p id with
     435      [ None ⇒ None ?
     436      | Some m' ⇒ store_init_data_list F ge m' r b (p + size_init_data id) idl'
     437      ]
     438  ].
     439
     440ndefinition size_init_data_list : list init_data → Z ≝
     441  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
     442
     443(* Nonessential properties that may require arithmetic
     444nremark size_init_data_list_pos:
     445  ∀i_data. OZ ≤ size_init_data_list i_data.
     446#i_data;nelim i_data;//;
     447#a;#tl;ncut (OZ ≤ size_init_data a)
     448##[ncases a;nnormalize;//;
     449   #x;ncases x;nnormalize;//;
     450##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
     451   ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
     452   ##[ncases (size_init_data a) in Hsize IH;
     453      ##[##1,2:/3/
     454      ##|nnormalize;#n;#Hfalse;nelim Hfalse]
     455   ##|#Hdisc;ncases Hdisc
     456      ##[#Heq;nrewrite > Heq;//;
     457      ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
     458         (* TODO: arithmetics *) napply daemon]
     459   ##]
     460##]
     461nqed.
     462*)
     463
     464ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
     465  λm,i_data,bcl.
     466  〈mk_mem (update ? (nextblock m)
     467                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef) bcl)
     468                 (blocks m))
     469         (Zsucc (nextblock m))
     470         (succ_nextblock_pos m),
     471   (nextblock m)〉.
     472
     473(* init *)
     474
    398475ndefinition add_globals : ∀F,V:Type.
    399476       genv F × mem → list (ident × (list init_data) × region × V) →
    400        genv F × mem
    401 λF,V,init,vars.
    402   foldr ??
    403     (λid_init: ident × (list init_data) × region × V. λg_st: genv F × mem.
     477       res (genv F × mem)
     478λF,V,init_env,vars.
     479  foldl ??
     480    (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    404481      match id_init with [ mk_pair id_init1 info ⇒
    405       match id_init1 with [ mk_pair id_init2 bsp
     482      match id_init1 with [ mk_pair id_init2 r
    406483      match id_init2 with [ mk_pair id init ⇒
    407       match g_st with [ mk_pair g st ⇒
    408         match alloc_init_data st init bsp with [ mk_pair st' b ⇒
    409           〈add_symbol ? id bsp b g, st'〉
    410         ] ] ] ] ])
    411     init vars.
    412 
    413 ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝
     484        do 〈g,st〉 ← g_st;
     485        match alloc_init_data st init r with [ mk_pair st' b ⇒
     486          let g' ≝ add_symbol ? id r b g in
     487          do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init);
     488            OK ? 〈g', st''〉
     489        ] ] ] ])
     490    (OK ? init_env) vars.
     491
     492ndefinition globalenv_initmem : ∀F,V:Type. program F V → res (genv F × mem) ≝
    414493λF,V,p.
    415494  add_globals F V
    416     〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
    417     (prog_vars ?? p).
    418 
    419 ndefinition globalenv_ : ∀F,V:Type. program F V → genv F
     495   〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     496   (prog_vars ?? p).
     497
     498ndefinition globalenv_ : ∀F,V:Type. program F V → res (genv F)
    420499λF,V,p.
    421   \fst (globalenv_initmem F V p).
    422 ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝
     500  do 〈g,m〉 ← globalenv_initmem F V p;
     501    OK ? g.
     502ndefinition init_mem_ : ∀F,V:Type. program F V → res (mem) ≝
    423503λF,V,p.
    424   \snd (globalenv_initmem F V p).
     504  do 〈g,m〉 ← globalenv_initmem F V p;
     505    OK ? m.
     506
     507
     508
    425509
    426510ndefinition Genv : GENV ≝ mk_GENV
     
    13041388End Genv.
    13051389*)
     1390
Note: See TracChangeset for help on using the changeset viewer.