Changeset 485 for Deliverables/D3.1/Csemantics/Globalenvs.ma
 Timestamp:
 Feb 2, 2011, 12:41:05 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Globalenvs.ma
r480 r485 52 52 of function descriptions. *) 53 53 54 globalenv: ∀F,V: Type. program F V → genv_t F;54 globalenv: ∀F,V: Type. program F V → res (genv_t F); 55 55 (* * Return the global environment for the given program. *) 56 56 57 init_mem: ∀F,V: Type. program F V → mem;57 init_mem: ∀F,V: Type. program F V → res mem; 58 58 (* * Return the initial memory state for the given program. *) 59 59 … … 396 396 foldr ?? (add_funct F) init fns. 397 397 398 (* init *) 399 400 ndefinition 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 417 ndefinition 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 428 nlet 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 440 ndefinition 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 444 nremark 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 ##] 461 nqed. 462 *) 463 464 ndefinition 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 398 475 ndefinition add_globals : ∀F,V:Type. 399 476 genv F × mem → list (ident × (list init_data) × region × V) → 400 genv F × mem≝401 λF,V,init ,vars.402 fold r??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. 404 481 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 ⇒ 406 483 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 492 ndefinition globalenv_initmem : ∀F,V:Type. program F V → res (genv F × mem) ≝ 414 493 λF,V,p. 415 494 add_globals F V 416 417 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 498 ndefinition globalenv_ : ∀F,V:Type. program F V → res (genv F) ≝ 420 499 λ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. 502 ndefinition init_mem_ : ∀F,V:Type. program F V → res (mem) ≝ 423 503 λ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 425 509 426 510 ndefinition Genv : GENV ≝ mk_GENV … … 1304 1388 End Genv. 1305 1389 *) 1390
Note: See TracChangeset
for help on using the changeset viewer.