Changeset 2510 for src/Clight
 Timestamp:
 Nov 30, 2012, 4:40:37 PM (8 years ago)
 Location:
 src/Clight
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2500 r2510 285 285 (* General results on lists. *) 286 286 (*  *) 287 288 let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝ 289 match l with 290 [ nil ⇒ false 291  cons hd tl ⇒ 292 let 〈id, ty〉 ≝ hd in 293 match identifier_eq SymbolTag i id with 294 [ inl Hid_eq ⇒ true 295  inr Hid_neq ⇒ mem_assoc_env i tl 296 ] 297 ]. 287 298 288 299 (* If mem succeeds in finding an element, then the list can be partitioned around this element. *) 
src/Clight/switchRemoval.ma
r2488 r2510 757 757 <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl 758 758 ] qed. 759 760 (* Lookup functions in list environments (used to type local variables in functions) *)761 let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝762 match l with763 [ nil ⇒ false764  cons hd tl ⇒765 let 〈id, ty〉 ≝ hd in766 match identifier_eq SymbolTag i id with767 [ inl Hid_eq ⇒ true768  inr Hid_neq ⇒ mem_assoc_env i tl769 ]770 ].771 759 772 760 (*  *) 
src/Clight/toCminor.ma
r2496 r2510 114 114 (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *) 115 115 let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in 116 (* variables in the body of the function are gathered in [mem_vars] *)116 (* variables whose addr is taken in the body of the function are gathered in [mem_vars] *) 117 117 let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in 118 118 (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *) 
src/Clight/toCminorCorrectness.ma
r2500 r2510 281 281 qed. 282 282 283 definition local_matching ≝ 283 (* Perhaps we will have to be more precise on what is allocated, etc. 284 cf [exec_alloc_variables]. For now this is conveniently hidden in 285 the [value_eq E v v'] *) 286 definition memory_matching ≝ 284 287 λE:embedding. 285 288 λm,m':mem. 286 289 λen:cl_env. 287 290 λvenv:cm_env. 291 λcminv:clight_cminor_inv. 288 292 λsp:block. 289 293 λvars:var_types. 290 291 ∀id,cl_blo. lookup SymbolTag ? en id = Some ? cl_blo → 292 match lookup ?? vars id with 293 [ Some kind ⇒ 294 let 〈vtype, type〉 ≝ kind in 295 match vtype with 296 [ Stack n ⇒ 297 E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉 298  Local ⇒ 299 ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v → 300 ∃v'. lookup ?? venv id = Some ? v' ∧ 301 value_eq E v v' 302  _ ⇒ False ] 303  None ⇒ False ]. 294 ∀id. 295 match lookup SymbolTag ? en id with 296 [ None ⇒ 297 match find_symbol ? (ge_cl cminv) id with 298 [ None ⇒ True 299  Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉 300 ] 301  Some cl_blo ⇒ 302 match lookup ?? vars id with 303 [ Some kind ⇒ 304 let 〈vtype, type〉 ≝ kind in 305 match vtype with 306 [ Stack n ⇒ 307 E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉 308  Local ⇒ 309 ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v → 310 ∃v'. lookup ?? venv id = Some ? v' ∧ 311 value_eq E v v' 312  _ ⇒ False ] 313  None ⇒ False ] 314 ]. 304 315 305 316 lemma type_should_eq_inversion : … … 330 341  *: #Hload normalize #_ #H 331 342 lapply (jmeq_to_eq ??? H) #Heq destruct 332 ] qed. 333 334 343 ] qed. 344 345 lemma load_value_of_type_by_value : 346 ∀ty,m,b,off,val. 347 access_mode ty = By_value (typ_of_type ty) → 348 load_value_of_type ty m b off = Some ? val → 349 loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val. 350 * 351 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 352  #structname #fieldspec  #unionname #fieldspec  #id ] 353 #m #b #off #val 354 normalize in match (access_mode ?); 355 [ 1,4,5,6,7: #Habsurd destruct ] 356 #_ 357 #H @H 358 qed. 359 360 include "Clight/CexecSound.ma". 361 362 lemma lookup_exec_alloc : 363 ∀source_variables, initial_env, env, var_id, clb, m, m'. 364 lookup ?? env var_id = Some ? clb → 365 exec_alloc_variables initial_env m source_variables = 〈env,m'〉 → 366 lookup ?? initial_env var_id = Some ? clb ∨ 367 Exists ? (λx. \fst x = var_id) source_variables. 368 #source_variables 369 elim source_variables 370 [ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc; 371 destruct (Hexec_alloc) %1 @Hlookup 372  2: * #id #ty #tail #Hind 373 #init_env #env #var #clb #m #m' #Hlookup 374 whd in ⊢ (??%? → ?); 375 cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta 376 #Hexec_alloc 377 @(match identifier_eq ? id var with [ inl Heq ⇒ ?  inr Hneq ⇒ ? ]) 378 [ 1: destruct (Heq) %2 %1 @refl ] 379 cases (Hind … Hlookup Hexec_alloc) 380 [ @cthulhu (* standard reasoning on positive_maps. check lib. *) 381  #Hexists %2 %2 @Hexists ] 382 ] qed. 383 384 lemma characterise_vars_lookup_local : 385 ∀globals,f,vartypes,stacksize,id,clb,env. 386 characterise_vars globals f = 〈vartypes, stacksize〉 → 387 lookup ?? env id = Some ? clb → 388 (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) → 389 ∃t. local_id vartypes id t. 390 #globals #f #vartypes #stacksize #id #clb #env 391 #Hchar #Hlookup * #m * #m' #Hexec 392 cases (lookup_exec_alloc … Hlookup Hexec) 393 [ normalize in ⊢ (% → ?); #Heq destruct 394  @(characterise_vars_localid … Hchar) ] 395 qed. 396 397 lemma exec_alloc_hit_monotonic : ∀variables,env,env',var_id. 398 (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) → 399 ∀bl. lookup ?? env var_id = Some ? bl → 400 ∃bl'.lookup ?? env' var_id = Some ? bl'. 401 #variables elim variables 402 [ #env #env' #var_id * #m * #m' normalize #Heq destruct 403 #bl #H %{bl} @H 404  * #id #ty #tl #Hind #env #env' #var_id 405 * #m * #m' 406 whd in match (exec_alloc_variables ???); 407 cases (alloc ????) #m * #b' #Hregion normalize nodelta 408 @(match identifier_eq ? id var_id with [ inl Heq ⇒ ?  inr Hneq ⇒ ? ]) 409 [ 2: #Hexec' #bl #Hlookup 410 lapply (Hind ?? var_id (ex_intro … (ex_intro … Hexec')) bl ?) 411 [ <Hlookup @lookup_add_miss @sym_neq @Hneq ] // ] 412 destruct (Heq) #Hexec' #bl' #Hlookup 413 @(Hind ?? var_id (ex_intro … (ex_intro … Hexec')) b' ?) 414 @lookup_add_hit 415 ] qed. 416 417 lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id. 418 (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) → 419 lookup ?? env' var_id = None ? → 420 lookup ?? env var_id = None ? ∧ 421 ¬(Exists (ident×type) (λx:ident×type.\fst x=var_id) variables). 422 #vars elim vars 423 [ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq) 424 #H @conj try @H % // 425  * #id' #ty' #tl #Hind #env #env' #var * #m * #m' 426 whd in ⊢ ((??%?) → ? → ?); 427 cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion 428 normalize nodelta #Hexec #Hlookup 429 lapply (Hind … (ex_intro … (ex_intro … Hexec)) Hlookup) 430 cases env #env cases id' #id' cases var #var normalize 431 @(eqb_elim … id' var) 432 [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq)) 433 #Heq <Heq @conj try @Hlookup' % * 434 [ #Heq' destruct (Heq') cases Hneq #H @H @refl 435  cases Hexists' #H @H ] 436  1: #Heq destruct (Heq) * #Hlookup' #Hexists' 437 lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1 438 >H1 in Hlookup'; #Heq destruct 439 ] 440 ] qed. 441 442 lemma variable_not_in_env_but_in_vartypes_is_global : 443 ∀env,env',f,vars,stacksize,globals,var_id,allocty,ty. 444 (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) → 445 characterise_vars globals f =〈vars,stacksize〉 → 446 lookup ?? env' var_id = None ? → 447 lookup' vars var_id = OK ? 〈allocty, ty〉 → 448 ∃r.allocty = Global r. 449 #env #env' #f #vars #stacksize #globals #var_id #allocty #ty #Hexec_alloc 450 #Hcharacterise #Hlookup_fail #Hlookup_type_ok 451 lapply (characterise_vars_src … Hcharacterise var_id ?) 452 [ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t * 453 #Hlookup >Hlookup #_ #Habsurd destruct ] 454 * 455 [ 1: * #r * #ty' * #Hlookup' #Hex %{r} 456 >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ] 457 * #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta 458 @(match allocty 459 return λx. allocty = x → ? 460 with 461 [ Global r ⇒ λ_. ? 462  Stack st' ⇒ λHalloc. ? 463  Local ⇒ λHalloc. ? 464 ] (refl ? allocty)) 465 [ @False_ind ] normalize nodelta 466 #Heq_typ 467 (* Halloc is in contradiction with Hlookup_fail *) 468 lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail) 469 * #Hlookup' #Hnot_exists 470 lapply (characterise_vars_all … Hcharacterise var_id t ?) 471 [ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ] 472 #Hexists @False_ind 473 cut (Exists (ident×type) (λx:ident×type.\fst x=var_id) (fn_params f@fn_vars f)) 474 [ 1,3: elim (fn_params f @ fn_vars f) in Hexists; // 475 * #id' #ty' #tl #Hind * 476 [ 1,3: * #Heq #_ %1 @Heq 477  *: #H %2 @Hind @H ] ] 478 #H cases Hnot_exists #H' @H' @H 479 qed. 480 335 481 336 482 (* TODO : memory injections + link clight env+mem with local env+stack+mem *) 337 483 lemma eval_expr_sim : 338 484 ∀(inv:clight_cminor_inv). 339 485 ∀(f:function). 486 ∀(vars:var_types). 487 ∀stacksize. 488 characterise_vars (globals inv) f = 〈vars, stacksize〉 → 340 489 ∀(cl_env:cl_env). 490 (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) → 341 491 ∀(cl_m:mem). 342 343 492 ∀(cm_env:cm_env). 344 493 ∀(sp:block). 345 494 ∀(cm_m:mem). 346 ∀(vars:var_types).347 348 495 ∀E:embedding. 349 496 ∀minj:memory_inj E cl_m cm_m. 350 local_matching E cl_m cm_m cl_env cm_env sp vars → 351 352 (*vars = pi1 … (characterise_vars … [globals] [f]) →*) 353 (*local_matching en m venv sp m' → *) 354 497 memory_matching E cl_m cm_m cl_env cm_env inv sp vars → 355 498 (∀(e:expr). 356 499 ∀(e':CMexpr (typ_of_type (typeof e))). … … 361 504 ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧ 362 505 value_eq E cl_val cm_val) ∧ 363 364 506 (∀ed,ty. 365 507 ∀(e':CMexpr (typ_of_type ty)). … … 370 512 (* TODO: shift 〈resblo, resoff〉 through E *) 371 513 eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉). 372 #inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching 514 #inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env 515 #sp #cm_m #E #Hinj #Hlocal_matching 373 516 @expr_lvalue_ind_combined 374 517 [ 1: (* Integer constant *) … … 396 539 whd in Hcl_success:(???%); 397 540 [ 1: (* var case *) 398 399 lapply Hcl_success Hcl_success 541 lapply Hcl_success Hcl_success Hind 400 542 (* Peform case analysis on presence of variable in local Clight env. 401 543 * if success, exec_expr/exec_lvalue tells us that it shoud be local. *) … … 408 550 normalize nodelta 409 551 [ 1: (* global case *) 410 @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *) 552 #Hlookup_global 553 cases (bind_inversion ????? Hlookup_global) Hlookup_global #global_block 554 * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol 555 #Heq whd in Heq:(???%); destruct (Heq) 556 lapply (bind2_eq_inversion ?????? Htranslate_expr) Htranslate_expr 557 * #var_id_alloctype * #var_id_type * #Heq 558 cases (variable_not_in_env_but_in_vartypes_is_global … 559 Hexec_alloc Hcharacterise Hcl_lookup Heq) 560 #r #Heq' destruct (Heq') normalize nodelta 561 lapply Hcl_load_success Hcl_load_success 562 lapply Hyp_present Hyp_present 563 lapply Hexpr_vars Hexpr_vars 564 lapply cm_expr cm_expr inversion (access_mode ty) 565 [ #typ_of_ty   #typ_of_ty ] 566 #Heq_typ_of_type #Heq_access_mode 567 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta 568 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 569 whd in match (eval_expr ???????); 570 whd in match (eval_expr ???????); 571 whd in match (eval_constant ????); 572 <(eq_sym … inv) >Hfind_symbol normalize nodelta 573 cases (bind_inversion ????? Hcl_load_success) #x * 574 #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val) 575 lapply (opt_to_res_inversion ???? Hopt_to_res) 576 #Hcl_load_success 577 [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))} 578 @conj try @refl 579 whd in Hcm_load_success:(??%?); 580 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty 581 >(load_value_of_type_by_ref … Hcl_load_success) 582 try assumption %4 583 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta 584 >Hfind_symbol normalize nodelta #Heq_embedding 585 whd in match (shift_offset ???); 586 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding 587 normalize nodelta @refl 588  1: cut (access_mode ty=By_value (typ_of_type ty)) 589 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt 590 lapply Heq_access_mode <Heqt // ] #Haccess 591 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success) 592 #Hvalid_ptr 593 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success) 594 [ whd in ⊢ (??%?); 595 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta 596 >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ] 597 * #val' * #Hcm_load_success #Hvalue_eq 598 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success) 599 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv 600 normalize %{val'} @conj try @refl assumption ] 411 601  2: (* local case *) 412 602 #Heq destruct (Heq) … … 414 604 * #var_id_alloc_type * #var_id_type * 415 605 generalize in match var_id_alloc_type; * normalize nodelta 416 [ 1: (* Global case. This should be contradictory, right ?417 * If lookup succeeded, then our local shadows any global with the same418 * name, and [characterise_vars] should say so. TODO, this lemma. *)419 @cthulhu606 [ 1: #r #Hlookup_vartype 607 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc) 608 * #typ whd in match (local_id ???); 609 >Hlookup_vartype normalize nodelta @False_ind 420 610  2: (* Stack local *) 421 611 lapply Hcl_load_success Hcl_load_success … … 428 618 #stack_depth #Hlookup_vartype_success normalize nodelta 429 619 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 430 lapply (Hlocal_matching … Hcl_lookup) 431 whd in Hlookup_vartype_success:(??%?); 620 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta 432 621 cases (res_inversion ?????? Hlookup_vartype_success) Hlookup_vartype_success 433 622 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq) … … 437 626 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 438 627 lapply (opt_to_res_inversion ???? Hload_val) Hload_val 439 #Hload_success 440 whd in match (eval_expr ???????); 628 #Hload_success whd in match (eval_expr ???????); 441 629 cut (pointer_translation (mk_pointer cl_b zero_offset) E = 442 Some ? (mk_pointer sp ( offset_of_Z stack_depth)))630 Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth)))) 443 631 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta 444 632 >offset_plus_0 @refl ] 445 #Hpointer_translation 633 #Hpointer_translation 446 634 [ 2: (* Byref *) 447 635 whd in Hload_success:(??%?); … … 451 639 %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))} 452 640 @conj try @refl 453 %4 (* boring and trivial *) 454 @cthulhu 641 %4 whd in match (shift_offset ???); 642 whd in match zero_offset; 643 >commutative_addition_n >addition_n_0 @Hpointer_translation 455 644  1: (* By value *) 645 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0 456 646 lapply (mi_inj … Hinj … Hpointer_translation … Hload_success) 457 647 [ @(load_by_value_success_valid_pointer … Hload_success) 458 lapply (jmeq_to_eq ??? Heq_typ_of_type) 459 #Heq_typ_of_type' 460 (* boring and trivial *) 461 @cthulhu ] 648 lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ] 462 649 * #cm_val * #Hload_in_cm #Hvalue_eq 463 650 %{cm_val} @conj try assumption 464 (* unpack Hload_in_cm using Heq_access_mode as an hypothesis. profit *) 465 @cthulhu ] 651 lapply (load_value_of_type_by_value … Hload_in_cm) 652 [ lapply Heq_access_mode <Heq0 #Heq1 653 @(jmeq_to_eq ??? Heq1) ] 654 #Hloadv <Heq0 655 whd in match (shift_offset ???); >commutative_addition_n >addition_n_0 656 >Hloadv @refl ] 466 657  3: (* Register local variable *) 467 658 #Hlookup_eq … … 488 679 whd in match (eval_expr ???????); 489 680 whd in match (lookup_present ?????); 490 lapply (Hlocal_matching … Hcl_lookup) >Hlookup' normalize nodelta 681 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta 682 >Hlookup' normalize nodelta #Hmatching 491 683 cases (bind_inversion ????? Hcl_load_success) Hcl_load_success 492 #loaded_val * #Hload_val 684 #loaded_val * #Hload_val 493 685 whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 494 686 lapply (opt_to_res_inversion ???? Hload_val) Hload_val 495 #Hload_success #Hlookup_in_cm_env496 cases (H lookup_in_cm_env ?Hload_success) #val'687 #Hload_success 688 cases (Hmatching … Hload_success) #val' 497 689 * #Hlookup_in_cm #Hvalue_eq %{val'} 498 690 cases Hyp_present … … 500 692 (* seems ok *) 501 693 ] 502 ] 694 ] 503 695  2: (* Deref case. Reduce the deref, exhibit the underlying load. *) 504 696 cases (bind_inversion ????? Hcl_success) Hcl_success
Note: See TracChangeset
for help on using the changeset viewer.