Changeset 2527
 Timestamp:
 Dec 3, 2012, 6:22:46 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r2510 r2527 395 395 qed. 396 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 variables402 [ #env #env' #var_id * #m * #m' normalize #Heq destruct403 #bl #H %{bl} @H404  * #id #ty #tl #Hind #env #env' #var_id405 * #m * #m'406 whd in match (exec_alloc_variables ???);407 cases (alloc ????) #m * #b' #Hregion normalize nodelta408 @(match identifier_eq ? id var_id with [ inl Heq ⇒ ?  inr Hneq ⇒ ? ])409 [ 2: #Hexec' #bl #Hlookup410 lapply (Hind ?? var_id (ex_intro … (ex_intro … Hexec')) bl ?)411 [ <Hlookup @lookup_add_miss @sym_neq @Hneq ] // ]412 destruct (Heq) #Hexec' #bl' #Hlookup413 @(Hind ?? var_id (ex_intro … (ex_intro … Hexec')) b' ?)414 @lookup_add_hit415 ] qed.416 397 417 398 lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id. … … 478 459 #H cases Hnot_exists #H' @H' @H 479 460 qed. 480 481 482 (* TODO : memory injections + link clight env+mem with local env+stack+mem *) 461 462 lemma intsize_eq_elim_dec : 463 ∀sz1,sz2. 464 ∀P: ∀sz1,sz2. Type[0]. 465 ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨ 466 ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2). 467 * * #P normalize 468 try /3 by or_introl, conj, refl/ 469 %2 @conj try // 470 % #H destruct 471 qed. 472 473 483 474 lemma eval_expr_sim : 484 475 ∀(inv:clight_cminor_inv). … … 508 499 ∀Hexpr_vars. 509 500 translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») → 510 ∀resblo,resoff,trace,Hyp_present. 511 exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 → 512 (* TODO: shift 〈resblo, resoff〉 through E *) 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)〉). 501 ∀cl_blo,cl_off,trace,Hyp_present. 502 exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 503 match E cl_blo with 504 [ Some loc ⇒ 505 let 〈cm_blo, delta〉 ≝ loc in 506 match access_mode ty with 507 [ By_value t ⇒ 508 (∃cm_val. loadv t cm_m (Vptr (mk_pointer cm_blo (offset_plus cl_off delta))) = Some ? cm_val ∧ 509 eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉) 510  By_reference ⇒ 511 eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m 512 = OK ? 〈trace, Vptr (mk_pointer cm_blo (offset_plus cl_off delta))〉 513  By_nothing _ ⇒ True ] 514  None ⇒ False ]). 514 515 #inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env 515 516 #sp #cm_m #E #Hinj #Hlocal_matching … … 523 524 whd in Htranslate:(??%?); 524 525 [ 1,3,4,5,6,7,8: destruct ] 525 (* This intsize_eq_elim' is the proofequivalent of eating a sandwich with 526 sand inside. *) 527 @cthulhu 526 cases (intsize_eq_elim_dec csz sz (λsz0.λsz0'.res (Σe0':expr (typ_of_type (Tint sz0' sg)).expr_vars (typ_of_type (Tint sz0' sg)) e0' (local_id vars)))) 527 [ 2: * #H_err #H_neq_sz 528 lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch))) 529 >Htranslate #Habsurd destruct (Habsurd) ] 530 * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch))) 531 destruct (Heq_sz) 532 >Htranslate Htranslate H_ok #Heq destruct (Heq) 533 whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta 534 #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl // 528 535  2: * 529 [ #sz #i  #var_id  #e1  #e1  #op #e1  #op #e1 #e2  #cast_ty #e1536 [ #sz #i  #var_id  * #ed1 #ty1  #e1  #op #e1  #op #e1 #e2  #cast_ty #e1 530 537  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 531 538 try /2 by I/ … … 693 700 ] 694 701 ] 695  2: (* Deref case. Reduce the deref, exhibit the underlying load. *)696 cases (bind_inversion ????? Hcl_success) Hcl_success697 * #cl_subexpr_val #cl_subexpr_trace *698 whd in ⊢ (? → (???%) → ?);702  2: whd in match (typeof ?) in Hind; 703 lapply (Hind cm_expr Hexpr_vars Htranslate_expr cl_b cl_o cl_t Hyp_present) Hind 704 cases (bind_inversion ????? Hcl_success) Hcl_success * #cl_subexpr_val #cl_trace * 705 #Hexec_expr 699 706 @(match cl_subexpr_val 700 707 return λx. cl_subexpr_val = x → ? … … 704 711  Vnull ⇒ λHval_eq. ? 705 712  Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta 706 [ 1,2,3: #_ #Habsurd destruct ] 707 #Hcl_exec_to_pointer #Heq destruct (Heq) 708 (* Now that we have executed the Clight part, reduce the Cminor one *) 709 whd in Htranslate_expr:(??%?); 710 cases (bind_inversion ????? Htranslate_expr) Htranslate_expr 711 * #cm_expr #Hexpr_vars * #Htranslate_expr 712 whd (* ... *) @cthulhu 713  3: @cthulhu ] 713 whd in ⊢ ((???%) → ?); 714 [ 1,2,3: #Habsurd destruct ] #Heq destruct (Heq) destruct (Hptr_eq) 715 whd in match (exec_lvalue' ?????) in Hind; #Hind 716 cases (bind_inversion ????? Hcl_load_success) Hcl_load_success #cl_val 717 * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 718 lapply (opt_to_res_inversion ???? Hopt_to_res) Hopt_to_res #Hload_success 719 whd in Hexec_expr:(???%); whd in match (exec_lvalue' ?????) in Hind; 720 lapply Hind Hind >Hexec_expr normalize nodelta 721 #Hind lapply (Hind (refl ??)) Hind 722 @(match E (pblock p) 723 return λx. (E (pblock p) = x) → ? 724 with 725 [ None ⇒ λHembed. ? 726  Some loc ⇒ λHembed. ? ] (refl ? (E (pblock p)))) 727 normalize nodelta 728 [ 1: @False_ind ] 729 cases loc in Hembed; normalize nodelta 730 lapply Hload_success Hload_success 731 lapply Hexec_expr Hexec_expr 732 lapply Hyp_present Hyp_present 733 lapply Htranslate_expr Htranslate_expr 734 lapply Hexpr_vars Hexpr_vars 735 lapply cm_expr cm_expr 736 cases ty 737 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 738  #structname #fieldspec  #unionname #fieldspec  #id ] 739 normalize nodelta 740 #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_expr 741 #Hload_success #BL #OFF #Hembed 742 [ 1,6,7: normalize in Hload_success; #_ destruct 743  4,5: whd in match (typ_of_type ?); #Heval >Heval 744 %{(Vptr (mk_pointer BL (offset_plus (poff p) OFF)))} 745 @conj try @refl 746 lapply (load_value_of_type_by_ref … Hload_success ??) try // 747 #Heq >Heq %4 whd in ⊢ (??%%); >Hembed @refl 748  *: * #cm_val * #Hloadv #Heval_expr >Heval_expr 749 lapply (mi_inj … Hinj … (pblock p) (poff p) BL (offset_plus (poff p) OFF) … Hload_success) 750 [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl 751  2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ] 752 * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq' 753 %{cm_val'} @conj try assumption 754 whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success'; 755 #Heq destruct @refl ] 756  3: lapply Hcl_load_success Hcl_load_success lapply Hcl_success Hcl_success 757 lapply (refl ? (typeof e1)) 758 cases (typeof e1) in ⊢ ((???%) → %); 759 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 760  #structname #fieldspec  #unionname #fieldspec  #id ] 761 #Heq_typeof normalize nodelta 762 [ 1,2,3,4,5,8: #Habsurd destruct ] 763 #Hexec_compound_clight 764 lapply (Hind … Htranslate_expr) Hind Htranslate_expr 765 cases (bind_inversion ????? Hexec_compound_clight) Hexec_compound_clight 766 * * #CLB #CLO #CLTR 767 * #Hexec_lvalue #Hfield_offset whd in match (exec_lvalue' ?????); 768 >Hexec_lvalue normalize nodelta >Heq_typeof normalize nodelta 769 whd in match (m_bind ?????); 770 [ 2: normalize in Hfield_offset; destruct (Hfield_offset) 771 #Hind lapply (Hind ??? Hyp_present (refl ??)) Hind 772 @(match E cl_b 773 return λx. (E cl_b = x) → ? 774 with 775 [ None ⇒ λHembed. ? 776  Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) normalize nodelta 777 [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta 778 lapply Hyp_present Hyp_present 779 lapply Hexpr_vars Hexpr_vars 780 lapply cm_expr cm_expr 781 cases ty normalize nodelta 782 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 783  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 784 #cm_expr #Hexpr_vars #Hyp_present 785 [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void) 786 #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res) 787 normalize in ⊢ (% → ?); #Habsurd destruct 788  4,5: whd in match (typ_of_type ?); #Heval >Heval 789 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) 790 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); 791 lapply (opt_to_res_inversion ???? Hopt_to_res) 792 #Hload_success #Heq destruct (Heq) 793 lapply (load_value_of_type_by_ref … Hload_success ??) try // 794 #Hval_eq >Hval_eq 795 %{(Vptr (mk_pointer BLO (offset_plus cl_o OFF)))} 796 @conj try @refl 797 %4 whd in ⊢ (??%%); >Hembed @refl 798  2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr 799 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) 800 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 801 lapply (opt_to_res_inversion ???? Hopt_to_res) 802 #Hload_success 803 lapply (mi_inj … Hinj … cl_b cl_o BLO (offset_plus cl_o OFF) … Hload_success) 804 [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl 805  2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ] 806 * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq' 807 %{cm_val'} @conj try assumption 808 whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success'; 809 #Heq destruct (Heq) @refl ] 810  1: cases (bind_inversion ????? Hfield_offset) Hfield_offset #field_offset * #Hfield_offset_eq 811 #Heq whd in Heq:(???%); destruct (Heq) >Hfield_offset_eq normalize nodelta 812 #Hind lapply (Hind ??? Hyp_present (refl ??)) Hind 813 @(match E cl_b 814 return λx. (E cl_b = x) → ? 815 with 816 [ None ⇒ λHembed. ? 817  Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) 818 normalize nodelta 819 [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta 820 lapply Hyp_present Hyp_present 821 lapply Hexpr_vars Hexpr_vars 822 lapply cm_expr cm_expr 823 cases ty normalize nodelta 824 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 825  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 826 #cm_expr #Hexpr_vars #Hyp_present 827 [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void) 828 #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res) 829 normalize in ⊢ (% → ?); #Habsurd destruct 830  4,5: whd in match (typ_of_type ?); #Heval >Heval 831 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) Hload_success_hyp 832 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); 833 lapply (opt_to_res_inversion ???? Hopt_to_res) 834 #Hload_success #Heq destruct (Heq) 835 lapply (load_value_of_type_by_ref … Hload_success ??) try // 836 #Hval_eq >Hval_eq 837 %{(Vptr (mk_pointer BLO (offset_plus (shift_offset (bitsize_of_intsize I32) CLO (repr I32 field_offset)) OFF)))} 838 @conj try @refl 839 %4 whd in ⊢ (??%%); >Hembed @refl 840  2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr 841 #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) 842 #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 843 lapply (opt_to_res_inversion ???? Hopt_to_res) 844 #Hload_success 845 lapply (mi_inj ??? Hinj 846 cl_b 847 (mk_offset 848 (addition_n offset_size (offv CLO) 849 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) 850 BLO (offset_plus (mk_offset 851 (addition_n offset_size (offv CLO) 852 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) OFF) ? val ?? Hload_success) 853 [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl 854  2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ] 855 * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq' 856 %{cm_val'} @conj try assumption 857 whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success'; 858 #Heq destruct (Heq) @refl ] 859 ] ] 860  3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var 861 whd in Hexec_lvalue_var:(??%?); 862 (* check whether var is local or global *) 863 lapply (Hlocal_matching var) cases (lookup ?? cl_env var) in Hexec_lvalue_var; 864 normalize nodelta 865 [ 1: (* global *) 866 #Hexec_opt 867 cases (bind_inversion ????? Hexec_opt) Hexec_opt #varblock * #Hopt_to_res #Heq 868 whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq) 869 >(opt_to_res_inversion ???? Hopt_to_res) normalize nodelta 870 #Hembed >Hembed normalize nodelta 871 (* Standard stuff. *) 872 @cthulhu 873  2: (* local *) 874 @cthulhu 875 ] 714 876  *: @cthulhu 715 ] qed. 877 ] qed. 716 878 717 879
Note: See TracChangeset
for help on using the changeset viewer.