Changeset 2483 for src/Clight/memoryInjections.ma
 Timestamp:
 Nov 22, 2012, 5:05:55 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2468 r2483 304 304 ∀b1,off1,b2,off2,ty,v1. 305 305 valid_block m1 b1 → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading byref *) 306 E b1 = Some ? 〈b2,off2〉 → 306 E b1 = Some ? 〈b2,off2〉 → 307 307 load_value_of_type ty m1 b1 off1 = Some ? v1 → 308 308 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). … … 315 315 load_value_of_type ty m1 b1 off1 = Some ? v1 → 316 316 (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2). 317 317 318 definition block_is_empty : mem → block → Prop ≝ 319 λm,b. 320 high_bound m b ≤ low_bound m b. 321 318 322 (* Adapted from Compcert's Memory *) 319 323 definition non_aliasing : embedding → mem → Prop ≝ … … 321 325 ∀b1,b2,b1',b2',delta1,delta2. 322 326 b1 ≠ b2 → 327 block_region b1 = block_region b2 → 323 328 E b1 = Some ? 〈b1',delta1〉 → 324 329 E b2 = Some ? 〈b2',delta2〉 → 325 330 (b1' ≠ b2') ∨ 331 block_is_empty m b1' ∨ 332 block_is_empty m b2' ∨ 326 333 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 327 334 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1). … … 332 339 mi_inj : load_sim_ptr E m1 m2; 333 340 (* Invalid blocks are not mapped *) 334 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;341 (* mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; *) 335 342 (* Valid pointers are mapped to valid pointers*) 336 343 mi_valid_pointers : ∀p,p'. … … 347 354 348 355 (*  *) 356 (* Setting up an empty injection *) 357 (*  *) 358 359 definition empty_injection : memory_inj (λx. None ?) empty empty. 360 % 361 [ 1: whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload 362 normalize in Hptr_trans; destruct 363  2: * #b #o #p' #_ normalize #Habsurd destruct 364  3: #b #b' #o' #Habsurd destruct 365  4: normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct ] 366 qed. 367 368 (*  *) 349 369 (* End of the definitions on memory injections. Now, on to proving some lemmas. *) 370 350 371 351 372 (* A particular inversion. *) … … 445 466 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) 446 467 * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I 447 qed. 468 qed. 448 469 449 470 (* Making explicit the contents of memory_inj for load_value_of_type. … … 525 546 qed. 526 547 527 (* Memory allocation preserves [memory_inj] *) 528 lemma alloc_memory_inj : 548 (* Memory allocation in m2 preserves [memory_inj]. 549 * This is lemma 43 from Leroy&Blazy. *) 550 lemma alloc_memory_inj_m2 : 529 551 ∀E:embedding. 530 552 ∀m1,m2,m2',z1,z2,r,new_block. … … 534 556 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc 535 557 % 536 [ 1: 537 whd 558 [ whd 538 559 #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload 539 560 elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload) … … 553 574 @Hload 554 575  4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 555  2: @(mi_freeblock … Hmemory_inj) 556  3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) 576  #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) 557 577 elim m2 in Halloc; #contentmap #nextblock #Hnextblock 558 578 elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc) … … 568 588 #Hbid_neq >Hbid_neq 569 589 cases (eq_region br' r) normalize #H @H 570  4: @(mi_region … Hmemory_inj) 571  5: @(mi_nonalias … Hmemory_inj) 590  @(mi_region … Hmemory_inj) 591  @(mi_nonalias … Hmemory_inj) 592 qed. 593 594 (* Allocating in m1 such that the resulting block has no image in m2 preserves 595 the injection. This is lemma 44 for Leroy&Blazy. The proof should proceed as 596 in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out 597 absurd cases. *) 598 axiom alloc_memory_inj_m1 : 599 ∀E:embedding. 600 ∀m1,m2,m1',z1,z2,r,new_block. 601 ∀H:memory_inj E m1 m2. 602 alloc m1 z1 z2 r = 〈m1', new_block〉 → 603 E (pi1 … new_block) = None ? → 604 memory_inj E m1' m2. 605 606 (* Embed a fresh block inside an unmapped portion of the target 607 block. *) 608 axiom alloc_memory_inj_m1_to_m2 : 609 ∀E:embedding. 610 ∀m1,m2,m1':mem. 611 ∀z1,z2:Z. 612 ∀b2,new_block. 613 ∀delta:offset. 614 ∀H:memory_inj E m1 m2. 615 alloc m1 z1 z2 (block_region b2) = 〈m1', new_block〉 → 616 E (pi1 … new_block) = Some ? 〈b2, delta〉 → 617 low_bound m2 b2 ≤ z1 + Zoo delta → 618 z2 + Zoo delta ≤ high_bound m2 b2 → 619 (∀b,b',delta'. b ≠ (pi1 … new_block) → 620 E b = Some ? 〈b', delta'〉 → 621 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨ 622 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) → 623 memory_inj E m1' m2. 624 625 (*  *) 626 (* Lemmas pertaining to [free] *) 627 628 (* Lemma 46 by Leroy&Blazy *) 629 lemma free_load_sim_ptr_m1 : 630 ∀E:embedding. 631 ∀m1,m2,m1'. 632 load_sim_ptr E m1 m2 → 633 ∀b. free m1 b = m1' → 634 load_sim_ptr E m1' m2. 635 #E #m1 #m2 #m1' #Hinj #b #Hfree 636 whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans 637 cases ty 638 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 639  #structname #fieldspec  #unionname #fieldspec  #id ] 640 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 641 normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl 642 %4 @Htrans ] 643 #Hload <Hfree in Hload; #Hload lapply (load_value_of_type_free_load_value_of_type … Hload) 644 #Hload' @(Hinj … Hload') // 645 <Hfree in Hvalid; @valid_free_to_valid 646 qed. 647 648 (* lemma 47 of L&B *) 649 lemma free_load_sim_ptr_m2 : 650 ∀E:embedding. 651 ∀m1,m2,m2'. 652 load_sim_ptr E m1 m2 → 653 ∀b. free m2 b = m2' → 654 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 655 load_sim_ptr E m1 m2'. 656 #E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped 657 whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans 658 cases ty 659 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 660  #structname #fieldspec  #unionname #fieldspec  #id ] 661 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 662 normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl 663 %4 @Htrans ] 664 #Hload <Hfree 665 (* routine *) 666 @cthulhu 667 qed. 668 669 lemma free_block_is_empty : 670 ∀m,m',b,b'. 671 block_region b = block_region b' → 672 block_is_empty m b → 673 free m b' = m' → 674 block_is_empty m' b. 675 * #contents #nextblock #Hpos 676 #m' #b #b' #Hregions_eq 677 #HA #HB normalize in HB; <HB whd 678 normalize >Hregions_eq cases (block_region b') normalize nodelta 679 @(eqZb_elim … (block_id b) (block_id b')) 680 [ 1,3: #Heq normalize nodelta // 681  2,4: #Hneq normalize nodelta @HA ] 682 qed. 683 684 (* Lemma 49 in Leroy&Blazy *) 685 axiom free_non_aliasing_m1 : 686 ∀E:embedding. 687 ∀m1,m2,m1'. 688 memory_inj E m1 m2 → 689 ∀b. free m1 b = m1' → 690 non_aliasing E m1'. 691 (* The proof proceeds by a first case analysis to see wether b lives in the 692 same world as the nonaliasing blocks (if not : trivial), in this case 693 we proceed by a case analysis on the nonaliasing hypothesis in memory_inj. *) 694 695 696 (* Extending lemma 46 and 49 to memory injections *) 697 lemma free_memory_inj_m1 : 698 ∀E:embedding. 699 ∀m1,m2,m1'. 700 memory_inj E m1 m2 → 701 ∀b. free m1 b = m1' → 702 memory_inj E m1' m2. 703 #E #m1 #m2 #m1' #Hinj #b #Hfree 704 cases Hinj 705 #Hload_sim #Hvalid #Hregion #Hnonalias 706 % try assumption 707 [ @(free_load_sim_ptr_m1 … Hload_sim … Hfree) 708  #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation) 709 <Hfree in Hvalid_m1'; @valid_free_to_valid 710  @(free_non_aliasing_m1 … Hinj … Hfree) ] 711 qed. 712 713 (* Lifting lemma 47 to memory injs *) 714 lemma free_memory_inj_m2 : 715 ∀E:embedding. 716 ∀m1,m2,m2'. 717 memory_inj E m1 m2 → 718 ∀b. free m2 b = m2' → 719 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 720 memory_inj E m1 m2'. 721 #E #m1 #m2 #m2' #Hinj #b #Hfree #b1_not_mapped 722 % cases Hinj try // 723 #Hload_sim #Hvalid #Hregion #Hnonalias 724 [ (* We succed performing a load from m1. Case analysis: if byvalue, cannot map to freed block [b] 725 (otherwise contradiction), hence simulation proceeds through Hinj. 726 If not byvalue, then simulation proceeds without examining the contents of the memory *) 727 @cthulhu 728  #p #p' #Hvalid #Hptr_trans 729 (* We now through Hinj that valid_pointer m2 p'=true, 730 if (pblock p') = b then using b1_not_mapped and Hptr_trans we 731 know that the original pointer must be either invalid or empty, 732 hence contradiction with Hvalid 733 if (pblock p') ≠ b then straightforward simulation *) 734 @cthulhu 735  @Hregion ] 736 qed. 737 738 (* Lemma 64 of L&B on [freelist] *) 739 lemma freelist_memory_inj_m1_m2 : 740 ∀E:embedding. 741 ∀m1,m2,m1',m2'. 742 memory_inj E m1 m2 → 743 ∀blocklist,b2. 744 (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → 745 free m2 b2 = m2' → 746 free_list m1 blocklist = m1' → 747 memory_inj E m1' m2'. 748 (* nothing particular here, application of various lemmas and induction over blocklist. *) 749 @cthulhu 572 750 qed. 573 751 574 752 (*  *) 575 753 (* Lemma 40 of the paper of Leroy & Blazy on the memory model 576 * and related lemmas *)754 * and storerelated lemmas *) 577 755 578 756 lemma bestorev_beloadv_conservation : … … 643 821 lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2 644 822 // 645 ] qed. 823 ] qed. 824 825 lemma store_value_of_type_load_value_of_type_conservation : 826 ∀ty,mA,mB,wb,wo,v. 827 store_value_of_type ty mA wb wo v = Some ? mB → 828 ∀rb,ro. eq_block wb rb = false → 829 ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. 830 #ty #mA #mB #wb #wo #v #Hstore #rb #ro #Heq_block 831 cases ty in Hstore; 832 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 833  #structname #fieldspec  #unionname #fieldspec  #id ] 834 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct ] 835 whd in ⊢ ((??%?) → ?); #Hstoren 836 @(storen_load_value_of_type_conservation … Hstoren … Heq_block) 837 qed. 646 838 647 839 definition typesize' ≝ λty. typesize (typ_of_type ty). … … 808 1000 #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % 809 1001 lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // 810 cases Hinj #Hsim' #H not_valid #Hvalid #Hregion #Hnonalias try assumption1002 cases Hinj #Hsim' #Hvalid #Hregion #Hnonalias try assumption 811 1003 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid 812 1004 cases ty in Hstore; … … 825 1017 ] qed. 826 1018 1019 827 1020 (*  *) 828 1021 (* Lemma 41 of the paper of Leroy & Blazy on the memory model … … 839 1032 qed. 840 1033 1034 lemma fe_to_be_values_length : 1035 ∀E,v1,v2,ty. 1036 value_eq E v1 v2 → fe_to_be_values ty v1 = fe_to_be_values ty v2. 1037 #E #v1 #v2 #ty #Hvalue_eq 1038 @(value_eq_inversion … Hvalue_eq) // 1039 qed. 1040 841 1041 lemma value_eq_to_be_and_back_again : 842 1042 ∀E,ty,v1,v2. 843 1043 value_eq E v1 v2 → 844 1044 ast_typ_consistent_with_value ty v1 → 845 ast_typ_consistent_with_value ty v2 →846 1045 value_eq E (be_to_fe_value ty (fe_to_be_values ty v1 )) (be_to_fe_value ty (fe_to_be_values ty v2)). 847 1046 #E #ty #v1 #v2 #Hvalue_eq … … 850 1049  2: #sz #i cases ty 851 1050 [ 2: @False_ind 852  1: #sz' #sg #H whd in ⊢ (% → ?); #Heq853 lapply (fe_to_be_to_fe_value … H) #H >H // ]1051  1: #sz' #sg #H lapply H whd in ⊢ (% → ?); #Heq 1052 lapply (fe_to_be_to_fe_value_int … H) #H >H // ] 854 1053  3: #p1 #p2 #Hembed cases ty 855 1054 [ 1: #sz #sg @False_ind 856  2: #_ #_1055  2: #_ 857 1056 cases p1 in Hembed; #b1 #o1 858 1057 cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H … … 864 1063 ] qed. 865 1064 1065 (*  *) 1066 (* Lemma ?? of the paper of Leroy & Blazy on the memory model ? *) 1067 866 1068 lemma storen_parallel_memory_exists : 867 ∀E,m1,m2 ,m1',b1,i,b2,delta,ty,v1,v2.868 memory_inj E m1 m2 → 869 value_eq E v1 v2→870 storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→871 E b1 = Some ? 〈b2, delta〉→1069 ∀E,m1,m2. 1070 memory_inj E m1 m2 → 1071 ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → 1072 ∀v1,v2. value_eq E v1 v2 → 1073 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ 872 1074 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'. 873 @cthulhu qed. 874 (* 875 #E #m1 #m2 #m1' #b1 #i #b2 #delta #ty #v1 #v2 #Hinj #Hvalue_eq 876 @(value_eq_inversion … Hvalue_eq) 877 [ 1: #v #Hstoren *) 878 879 880 lemma storen_parallel_aux : 1075 (* ∧ loadn m2' (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? (fe_to_be_values ty v2).*) 1076 #E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty 1077 lapply (mi_valid_pointers … Hinj) 1078 generalize in match m2; 1079 generalize in match m1; 1080 generalize in match i; 1081 lapply (fe_to_be_values_length … ty Hvalue_eq) 1082 generalize in match (fe_to_be_values ty v2); 1083 generalize in match (fe_to_be_values ty v1); 1084 #l1 elim l1 1085 [ 1: #l2 #Hl2 1086 cut (l2 = []) 1087 [ cases l2 in Hl2; // #hd' #tl' normalize #Habsurd destruct ] 1088 #Hl2_empty >Hl2_empty #o #m1 #m2 #_ normalize /2 by ex_intro/ 1089  2: #hd1 #tl1 #Hind #l2 #Hlength 1090 cut (∃hd2,tl2.l2 = hd2::tl2 ∧ tl1 = tl2) 1091 [ cases l2 in Hlength; 1092 [ normalize #Habsurd destruct 1093  #hd2 #tl2 normalize #H %{hd2} %{tl2} @conj try @refl destruct (H) assumption ] ] 1094 * #hd2 * #tl2 * #Heq2 destruct (Heq2) #Hlen_tl 1095 #o #m1 #m2 #Hvalid_embed #Hstoren 1096 cases (some_inversion ????? Hstoren) #m1_tmp * #Hbestorev #Hstoren_tl 1097 lapply (Hvalid_embed (mk_pointer b1 o) (mk_pointer b2 (offset_plus o delta)) ??) 1098 [ 1: whd in match (pointer_translation ??); 1099 >Hembed normalize nodelta @refl 1100  2: @(bestorev_to_valid_pointer … Hbestorev) ] 1101 #Hvalid_ptr_m2 1102 whd in match (storen ???); 1103 lapply (valid_pointer_to_bestorev_ok m2 (mk_pointer b2 (offset_plus o delta)) hd2 Hvalid_ptr_m2) 1104 * #m2_tmp #Hbestorev2 >Hbestorev2 normalize nodelta 1105 whd in match (shift_pointer ???) in Hstoren_tl ⊢ %; 1106 whd in match (shift_offset ???) in Hstoren_tl ⊢ %; 1107 (* normalize in match (sign_ext ???) in Hstoren_tl ⊢ %;*) 1108 cut (mk_offset (addition_n ? (offv (offset_plus o delta)) (sign_ext 2 offset_size (bitvector_of_nat 2 1))) = 1109 offset_plus (offset_plus o (mk_offset (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) delta) 1110 [ cases o #o' normalize nodelta whd in match (offset_plus ??) in ⊢ (??%%); 1111 whd in match (offset_plus ??) in ⊢ (???(?%)); 1112 /2 by associative_addition_n, commutative_addition_n, refl/ ] 1113 #Heq_cleanup >Heq_cleanup >Heq_cleanup in Hind; #Hind @(Hind … Hstoren_tl) 1114 try assumption 1115 #p #p' #Hvalid_in_m1_tmp #Hp_embed @valid_pointer_of_Prop 1116 lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * 1117 #Hnextblock_eq #Hbounds_eq #Hoffset_in_bounds #Hcontents_at_eq #Hcontents_else_eq 1118 lapply (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * * 1119 #Hnextblock_eq2 #Hbounds_eq2 #Hoffset_in_bounds2 #Hcontents_at_eq2 #Hcontents_else_eq2 1120 cut (valid_pointer m1 p = true) 1121 [ @valid_pointer_of_Prop 1122 cases (valid_pointer_to_Prop … Hvalid_in_m1_tmp) 1123 >Hnextblock_eq cases (Hbounds_eq (pblock p)) #Hlow' #Hhigh' 1124 whd in match (low_bound ??); whd in match (high_bound ??); 1125 >Hlow' >Hhigh' * /3 by conj/ ] 1126 #Hvalid_in_m1 1127 lapply (Hvalid_embed p p' Hvalid_in_m1 Hp_embed) #Hvalid_in_m2 1128 cases (valid_pointer_to_Prop … Hvalid_in_m2) * #Hnextblock2' #Hlow2' #Hhigh2' 1129 @conj try @conj 1130 >Hnextblock_eq2 try assumption 1131 cases (Hbounds_eq2 … (pblock p')) #Hlow2'' #Hhigh2'' 1132 whd in match (low_bound ??); 1133 whd in match (high_bound ??); 1134 >Hlow2'' >Hhigh2'' assumption 1135 ] qed. 1136 1137 lemma storen_parallel_memory_exists_and_preserves_loads : 1138 ∀E,m1,m2. 1139 memory_inj E m1 m2 → 1140 ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → 1141 ∀v1,v2. value_eq E v1 v2 → 1142 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ 1143 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ 1144 loadn m2' (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? (fe_to_be_values ty v2). 1145 #E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty #Hstoren 1146 cases (storen_parallel_memory_exists … Hinj … Hembed … Hvalue_eq i m1' ty Hstoren) 1147 #m2' #Hstoren' %{m2'} @conj try assumption 1148 @(storen_loadn_ok … Hstoren') 1149 // 1150 qed. 1151 1152 (* If E ⊢ m1 ↦ m2 1153 *and* if E b1 = 〈b2,delta〉, 1154 *and* if we write /A PROPER VALUE/ at 〈b1,i〉 successfuly, 1155 *then* we can write /something value_eqcompatible/ in m2 at 〈b2,i+delta〉 successfuly yielding m2' 1156 *and* preserve the injection : E ⊢ m1' ↦ m2' 1157 N.B.: this result cannot be given at the backend level : we could overwrite a pointer 1158 and break the value_eq correspondence between the memories. *) 1159 axiom storen_parallel_aux : 881 1160 ∀E,m1,m2. 882 1161 ∀Hinj:memory_inj E m1 m2. … … 885 1164 ∀ty,i,m1'. 886 1165 ast_typ_consistent_with_value ty v1 → 887 ast_typ_consistent_with_value ty v2 →888 1166 storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → 889 1167 ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ 890 1168 memory_inj E m1' m2'. 891 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hok1 #Hok2 892 #Hstoren lapply (storen_to_valid_pointer_fe_to_be … Hstoren) 893 * * * #Hblocks_eq1 #Hnextblock1 #Hvalid_m1 #Hvalid_m1' 894 lapply (mi_valid_pointers … Hinj … (mk_pointer b1 i) (mk_pointer b2 (offset_plus i delta)) Hvalid_m1 ?) 895 [ 1: whd in ⊢ (??%%); >Hembed @refl ] 896 #Hvalid_m2 897 cases (valid_pointer_to_Prop … Hvalid_m2) * #Hnextblock2 #Hlow2 #Hhigh2 898 @cthulhu 899 qed. 900 901 lemma foo : 1169 (* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to 1170 * explain why, and how we might still be able to prove it given enough time. 1171 I'll be refering to paper by Leroy & Blazy in the J.A.R. 1172 In CompCert, when storing some data of size S in some location 〈block, offset〉, 1173 what happens is that 1174 1) the memory is extended with a map from 〈block,offset〉 to the actual data 1175 2) the memory inteval from 〈block,offset+1〉 to 〈block,offset+S1〉 is invalidated, 1176 meaning that every load in this interval will fail. 1177 This behaviour is documented at page 9 in the aforementioned paper. 1178 The memory model of Cerco is in a sense much more realistic. When storing a frontend 1179 value fv, the story is the following : 1180 1) the value fv is marshelled into a list of backend values (bytesized) which correspond 1181 to the actual size of the data inmemory. This list is then stored asis at the 1182 location 〈block, offset〉. 1183 1184 Now on to the lemma we want to prove. The difficult part is to prove [load_sim E m1' m2'], 1185 i.e. we want to prove that ∀c1,off1,c2,off2,delta. s.t. E c1 = 〈c2, off2〉 1186 load_value_of_type m1' c1 off1 = ⌊vA⌋ → 1187 load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋ ∧ 1188 value_eq E vA vB, 1189 where m1' and m2' are the result of storing some values v1 and v2 in resp. m1 and m2 1190 at some resp. locations 〈b1,i〉 and (pointer_translation E b1 i) (cf statement). 1191 1192 In CompCert, the proof of this statement goes by case analysis on 〈c1,off1〉. 1193 Case 1: 〈b1,i〉 = 〈c1,off1〉 → we read the freshly stored data. 1194 Case 2: b1 = c1 but [i; i+v1] and [c1, c1+vA] describe /disjoint/ areas of the 1195 same block. In this case, we can use the lemma store_value_load_disjoint 1196 on the hypothesis (load_value_of_type m1' c1 off1 = ⌊vA⌋) 1197 yielding (load_value_of_type m1' c1 off1 = load_value_of_type m1 c1 off1) 1198 allowing us to use the load_sim hypothesis on (m1, m2) to obtain 1199 (load_value_of_type m2 c2 (off1+off2) = ⌊vB⌋) 1200 which we can lift back to 1201 (load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋) 1202 using the disjointness hypothesis contained in the original memory injection [Hinj]. 1203 case 4: b1 ≠ c1, nothing difficult 1204 case 3: the intervals [i; i+v1] and [c1, c1+vA] /overalap/ ! 1205 in CompCert, the prof follows simply from the fact that the load 1206 (load_value_of_type m1' c1 off1) will fail because of invalidated memory, 1207 yielding a contradiction. We have no such possibility in Cerco. 1208 1209 I see a possible, convoluted way out of this problem. In the case of an overlap, we 1210 need to proceed to an inversion on load_value_of_type m1' c1 off1 = ⌊vA⌋ and to 1211 actually look at the data beeing written. If we succeeded in proceeding to this load, 1212 this means that the backend values stored are "consistent". 1213 Besides, we need to proceed to a case analysis on what we stored beforehand. 1214 A) If we stored an integer 1215 . of size 8: this means that the overlap actually includes all of the freshly stored 1216 area. This area contains one [BVByte]. If we succeeded in performing an overlapping load, 1217 we either overlapped from the beginning, from the end or from both ends of the stored 1218 area. In all cases, since this area contains a BVByte, all other offsets MUST contain 1219 BVBytes, otherwise we would have a contradiction ... (cumbersome to show but possible) 1220 Hence, we can splice the load in 2 or 3 subloads : 1221 . reuse the Case 2 above (disjoint areas) for the parts of the load that are before 1222 and after the stored area 1223 . reuse the Case 1 above for the stored area 1224 and show the whole successful load 1225 . of size 16,32: we have more freedom but only a finite number of overlap possibilities 1226 in each case. We can enumerate them and proceed along the same lines as in the 8 bit 1227 case. 1228 B) If we stored a pointer (of size 2 bytes, necessarily) 1229 . the bytes of a pointer are stored in order and (/!\ important /!\) are /numbered/. 1230 This means that any successful overlapping load has managed to read a pointer in 1231 the wrong order, which yields a contradiction. 1232 C) If we stored a Vnull, roughly the same reasoning as in the pointer case 1233 D) If we stored a Vundef ... This gets hairy. We must reason on the way fe_to_be_values 1234 and be_to_fe_value works. What we want is to show that the load 1235 [load_value_of_a type m1' c1 off1] yields a Vundef. This can happen in several ways. 1236 . If we try to load something of integer type, we will have a Vundef because 1237 we can show that some of the backend values are BVundef (cf [build_integer]) 1238 . If we try to load a pointer, it will also fail for the same reason. 1239 I'll admit that I'm not too sure about the last case. Also, my reasoning on pointers might 1240 fail if we have "longer that 2 bytes" pointers. 1241 1242 This was a highlevel and sketchy proof, and in the interests of time I decide to axiomatize 1243 it. 1244 *) 1245 1246 (* This is lemma 60 from Leroy&Blazy *) 1247 lemma store_value_of_type_parallel : 902 1248 ∀E,m1,m2. 903 1249 ∀Hinj:memory_inj E m1 m2. 904 1250 ∀v1,v2. value_eq E v1 v2 → 905 1251 ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → 906 ∀ty,i,m1'. store_value_of_type ty m1 b1 i v1 = Some ? m1' → 1252 ∀ty,i,m1'. 1253 type_consistent_with_value ty v1 → 1254 store_value_of_type ty m1 b1 i v1 = Some ? m1' → 907 1255 ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧ 908 memory_inj E m1' m2'. 909 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hstore 910 @cthulhu qed. 1256 memory_inj E m1' m2'. 1257 #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' 1258 cases ty 1259 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1260  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1261 #Hconsistent whd in ⊢ ((??%?) → ?); 1262 [ 1,4,5,6,7: #Habsurd destruct ] 1263 whd in match (store_value_of_type ?????); 1264 @(storen_parallel_aux … Hinj … Hembed … Hconsistent) // 1265 qed. 1266 1267 lemma store_value_of_type_load_sim : 1268 ∀E,m1,m2,m1'. 1269 ∀Hinj:memory_inj E m1 m2. 1270 ∀ty,b,i,v. 1271 E b = None ? → 1272 store_value_of_type ty m1 b i v = Some ? m1' → 1273 load_sim_ptr E m1' m2. 1274 #E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore 1275 cases Hinj #Hsim #Hvalid #Hregion_eq #Hnonalias 1276 cases ty in Hstore; 1277 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1278  #structname #fieldspec  #unionname #fieldspec  #id ] 1279 [ 1,4,5,6,7: #Heq normalize in Heq; destruct ] 1280 #Hstore whd 1281 #b1 #off1 #b2 #off2 #ty' #v1 #Hvalid #Hembed' #Hload 1282 lapply (store_value_of_type_load_value_of_type_conservation … Hstore b1 off1 ? ty') 1283 [ 1,3,5: @(eq_block_elim … b b1) try // #Heq >Heq in Hembed; 1284 #Hembed whd in Hembed':(??%?); >Hembed in Hembed'; #H normalize in H; 1285 destruct ] 1286 #Heq <Heq in Hload; #Hload 1287 (* Three times the same proof, but computing the indices is a PITA *) 1288 [ 1: 1289 cases ty' in Hload; 1290 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1291  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1292 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); 1293 #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} 1294 @conj try @refl %4 assumption ] 1295 #Hload @(Hsim … Hembed' … Hload) 1296 @(load_by_value_success_valid_pointer … Hload) // 1297  2: 1298 cases ty' in Hload; 1299 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1300  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1301 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); 1302 #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} 1303 @conj try @refl %4 assumption ] 1304 #Hload @(Hsim … Hembed' … Hload) 1305 @(load_by_value_success_valid_pointer … Hload) // 1306  3: 1307 cases ty' in Hload; 1308 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1309  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1310 [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); 1311 #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} 1312 @conj try @refl %4 assumption ] 1313 #Hload @(Hsim … Hembed' … Hload) 1314 @(load_by_value_success_valid_pointer … Hload) // 1315 ] qed. 1316 1317 lemma store_value_of_type_memory_inj : 1318 ∀E,m1,m2,m1'. 1319 ∀Hinj:memory_inj E m1 m2. 1320 ∀ty,b,i,v. 1321 E b = None ? → 1322 store_value_of_type ty m1 b i v = Some ? m1' → 1323 memory_inj E m1' m2. 1324 #E #m1 #m2 #m1' #Hinj #ty #b #i #v1 #Hnot_mapped #Hstore 1325 % 1326 [ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore) 1327  2: (* trivial *) @cthulhu 1328  3: (* easy *) @cthulhu 1329  4: (* writing doesn't alter the bound, straightforward *) @cthulhu ] 1330 qed. 911 1331 912 1332 (*  *)
Note: See TracChangeset
for help on using the changeset viewer.