Changeset 125 for C-semantics/Globalenvs.ma
- Timestamp:
- Sep 24, 2010, 10:31:32 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/Globalenvs.ma
r124 r125 66 66 a value, which must be a pointer with offset 0. *) 67 67 68 find_symbol: ∀F: Type. genv_t F → ident → option block;68 find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*; 69 69 (* * Return the address of the given global symbol, if any. *) 70 70 71 71 (* * ** Properties of the operations. *) 72 (* 72 73 73 find_funct_inv: 74 74 ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F. … … 142 142 (* * Commutation properties between program transformations 143 143 and operations over global environments. *) 144 *) *)144 *) 145 145 find_funct_ptr_transf: 146 146 ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. … … 171 171 find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → 172 172 ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf 173 (* 173 174 174 (* * Commutation properties between partial program transformations 175 175 and operations over global environments. *) … … 310 310 ]. 311 311 312 (* Functions are given negative block numbers *) 313 312 314 (* XXX: temporary definition 313 315 NB: only global functions, no global variables *) … … 315 317 functions: block → option F; 316 318 nextfunction: Z; 317 symbols: ident → option block319 symbols: ident → option (memory_space × block) 318 320 }. 321 (* 322 (** The rest of this library is a straightforward implementation of 323 the module signature above. *) 324 325 Module Genv: GENV. 326 327 Section GENV. 328 329 Variable F: Type. (* The type of functions *) 330 Variable V: Type. (* The type of information over variables *) 331 332 Record genv : Type := mkgenv { 333 functions: ZMap.t (option F); (* mapping function ptr → function *) 334 nextfunction: Z; 335 symbols: PTree.t block (* mapping symbol → block *) 336 }. 337 338 Definition t := genv. 339 *) 340 341 ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝ 342 λF,name_fun,g. 343 let b ≝ nextfunction ? g in 344 mk_genv F ((*ZMap.set*) λb'. if eqZb b b' then (Some ? (\snd name_fun)) else (functions ? g b')) 345 (Zpred b) 346 ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]). 347 348 ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝ 349 λF,name,bsp,b,g. 350 mk_genv F (functions ? g) 351 (nextfunction ? g) 352 ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]). 353 (* 354 Definition find_funct_ptr ? (g: genv) (b: block) : option F := 355 ZMap.get b g.(functions). 356 357 Definition find_funct (g: genv) (v: val) : option F := 358 match v with 359 | Vptr b ofs => 360 if Int.eq ofs Int.zero then find_funct_ptr ? g b else None 361 | _ => 362 None 363 end. 364 365 Definition find_symbol ? (g: genv) (symb: ident) : option block := 366 PTree.get symb g.(symbols). 367 368 Lemma find_funct_inv: 369 forall (ge: t) (v: val) (f: F), 370 find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero. 371 Proof. 372 intros until f. unfold find_funct. destruct v; try (intros; discriminate). 373 generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros. 374 exists b. congruence. 375 discriminate. 376 Qed. 377 378 Lemma find_funct_find_funct_ptr: 379 forall (ge: t) (b: block), 380 find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b. 381 Proof. 382 intros. simpl. 383 generalize (Int.eq_spec Int.zero Int.zero). 384 case (Int.eq Int.zero Int.zero); intros. 385 auto. tauto. 386 Qed. 387 *) 388 (* Construct environment and initial memory store *) 389 ndefinition empty_mem ≝ empty. (* XXX*) 390 ndefinition empty : ∀F. genv F ≝ 391 λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?). 392 (* mkgenv (ZMap.init None) (-1) (PTree.empty block).*) 393 394 ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝ 395 λF,init,fns. 396 foldr ?? (add_funct F) init fns. 397 398 ndefinition add_globals : ∀F,V:Type. 399 genv F × mem → list (ident × (list init_data) × memory_space × V) → 400 genv F × mem ≝ 401 λF,V,init,vars. 402 foldr ?? 403 (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem. 404 match id_init with [ mk_pair id_init1 info ⇒ 405 match id_init1 with [ mk_pair id_init2 bsp ⇒ 406 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 ≝ 414 λF,V,p. 415 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 ≝ 420 λF,V,p. 421 \fst (globalenv_initmem F V p). 422 ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝ 423 λF,V,p. 424 \snd (globalenv_initmem F V p). 319 425 320 426 ndefinition Genv : GENV ≝ mk_GENV 321 427 genv (* genv_t *) 322 (λF,V,p. foldr ?? 323 (λf,ge. match f with [ mk_pair id def ⇒ 324 let b ≝ nextfunction ? ge in 325 mk_genv ? (λb'. if eqZb b b' then Some ? def else (functions ? ge b')) 326 (Zsucc b) 327 (λi. match ident_eq id i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? ge i)]) 328 ]) 329 (mk_genv ? (λ_.None ?) 0 (λ_.None ?)) (prog_funct ?? p)) (* globalenv *) 330 (λF,V,p. empty) (* init_mem *) 428 globalenv_ 429 init_mem_ 331 430 (λF,ge. functions ? ge) (* find_funct_ptr *) 332 431 (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *) 333 432 (λF,ge. symbols ? ge) (* find_symbol *) 433 (* ? 334 434 ? 335 435 ? 336 436 ? 337 437 ? 338 ? 339 ? 438 ?*) 340 439 . 440 (* 341 441 ##[ #A B C transf p b f; nelim p; #fns main vars; 342 442 nelim fns; 343 ##[ n normalize; #H; ndestruct;443 ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct; 344 444 ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?); 345 445 nrewrite > (?:nextfunction ?? = length ? t); … … 443 543 ##] nqed. 444 544 445 (*446 (** The rest of this library is a straightforward implementation of447 the module signature above. *)448 449 Module Genv: GENV.450 451 Section GENV.452 453 Variable F: Type. (* The type of functions *)454 Variable V: Type. (* The type of information over variables *)455 456 Record genv : Type := mkgenv {457 functions: ZMap.t (option F); (* mapping function ptr → function *)458 nextfunction: Z;459 symbols: PTree.t block (* mapping symbol → block *)460 }.461 462 Definition t := genv.463 464 Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=465 let b := g.(nextfunction) in466 mkgenv (ZMap.set b (Some ? (snd name_fun)) g.(functions))467 (Zpred b)468 (PTree.set (fst name_fun) b g.(symbols)).469 470 Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=471 mkgenv g.(functions)472 g.(nextfunction)473 (PTree.set name b g.(symbols)).474 475 Definition find_funct_ptr ? (g: genv) (b: block) : option F :=476 ZMap.get b g.(functions).477 478 Definition find_funct (g: genv) (v: val) : option F :=479 match v with480 | Vptr b ofs =>481 if Int.eq ofs Int.zero then find_funct_ptr ? g b else None482 | _ =>483 None484 end.485 486 Definition find_symbol ? (g: genv) (symb: ident) : option block :=487 PTree.get symb g.(symbols).488 489 Lemma find_funct_inv:490 forall (ge: t) (v: val) (f: F),491 find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.492 Proof.493 intros until f. unfold find_funct. destruct v; try (intros; discriminate).494 generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.495 exists b. congruence.496 discriminate.497 Qed.498 499 Lemma find_funct_find_funct_ptr:500 forall (ge: t) (b: block),501 find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.502 Proof.503 intros. simpl.504 generalize (Int.eq_spec Int.zero Int.zero).505 case (Int.eq Int.zero Int.zero); intros.506 auto. tauto.507 Qed.508 509 (* Construct environment and initial memory store *)510 511 Definition empty : genv :=512 mkgenv (ZMap.init None) (-1) (PTree.empty block).513 514 Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=515 List.fold_right add_funct init fns.516 517 Definition add_globals518 (init: genv * mem) (vars: list (ident * list init_data * V))519 : genv * mem :=520 List.fold_right521 (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>522 match id_init, g_st with523 | ((id, init), info), (g, st) =>524 let (st', b) := Mem.alloc_init_data st init in525 (add_symbol id b g, st')526 end)527 init vars.528 529 Definition globalenv_initmem (p: program F V) : (genv * mem) :=530 add_globals531 (add_functs empty p.(prog_funct), Mem.empty)532 p.(prog_vars).533 534 Definition globalenv (p: program F V) : genv :=535 fst (globalenv_initmem p).536 Definition init_mem (p: program F V) : mem :=537 snd (globalenv_initmem p).538 545 539 546 Lemma functions_globalenv:
Note: See TracChangeset
for help on using the changeset viewer.