 Timestamp:
 Jan 11, 2013, 9:36:21 PM (8 years ago)
 Location:
 src/Clight
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2572 r2578 648 648 qed. 649 649 650 (*  *) 651 (* Some more stuff on bitvectors. *) 652 (*  *) 653 650 654 axiom commutative_multiplication : 651 655 ∀n. ∀v1,v2:BitVector n. 652 656 multiplication ? v1 v2 = multiplication ? v2 v1. 653 657 654 658 lemma commutative_short_multiplication : 655 659 ∀n. ∀v1,v2:BitVector n. … … 670 674 axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?). 671 675 676 (* lemma eq_v_to_eq_Z : ∀n. ∀v1,v2:BitVector n. (Z_of_bitvector … v1) = (Z_of_bitvector eq_bv … v1 v2. *) 672 677 673 678 
src/Clight/memoryInjections.ma
r2572 r2578 34 34 (*  *) 35 35 36 definition Zoub ≝ Z_of_unsigned_bitvector. 37 definition boZ ≝ bitvector_of_Z. 38 39 (* Offsets are just bitvectors packed inside some useless and annoying constructor. *) 40 definition Zoo ≝ λx. Zoub ? (offv x). 41 definition boo ≝ λx. mk_offset (boZ ? x). 36 (* Offsets are just bitvectors packed inside some annoying constructor. *) 37 definition Zoo ≝ λx. Z_of_unsigned_bitvector ? (offv x). 38 definition boo ≝ λx. mk_offset (bitvector_of_Z ? x). 42 39 43 40 (*  *) … … 65 62 lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b. 66 63 #a #b @(eq_block_elim … a b) /2/ qed. 64 65 lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b). 66 * #ra #ida * #rb #idb 67 cases ra cases rb 68 [ 2: %2 % #H destruct 69  3: %2 % #H destruct 70  *: cases (decidable_eq_Z_Type ida idb) 71 [ 1,3: * %1 @refl 72  2,4: #Hneq %2 % #H destruct (H) cases Hneq #H @H @refl ] 73 ] qed. 67 74 68 75 lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2. … … 218 225 ] 219 226  *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ] 220 ] qed. 227 ] qed. 221 228 222 229 (* Well in fact a valid pointer can be valid even after a free. Ah. *) … … 286 293 ]. 287 294 295 (* Definition of embedding compatibility. *) 296 definition embedding_compatible : embedding → embedding → Prop ≝ 297 λE,E'. 298 ∀b:block. E b = None ? ∨ 299 E b = E' b. 300 288 301 (* We parameterise the "equivalence" relation on values with an embedding. *) 289 302 (* Frontend values. *) … … 320 333 λm,b. 321 334 high_bound m b ≤ low_bound m b. 335 336 (* Definition of a 16 bit bitvectorimplementable Z *) 337 definition z_implementable_bv : Z → Prop ≝ 338 λz:Z. 339 0 ≤ z ∧ z < Z_two_power_nat 16. 340 341 (* Characterizing implementable blocks *) 342 definition block_implementable_bv ≝ 343 λm:mem.λb:block. 344 z_implementable_bv (low_bound m b) ∧ 345 z_implementable_bv (high_bound m b). (* FIXME this is slightly restrictive. We could allow the high bound to be 2^16.*) 346 347 (* Characterizing blocks compatible with an embedding. This condition ensures 348 * that we do not stray out of memory. *) 349 (* 350 definition block_ok_with_embedding ≝ λE:embedding.λb,m. 351 ∀b',delta. 352 E b = Some ? 〈b', delta〉 → 353 (high_bound m b) + (Zoo delta) < Z_two_power_nat 16. *) 354 355 (* We have to prove that the blocks we allocate are compatible with a given embedding. 356 This amounts to proving that the embedding cannot shift the new block outside the 2^16 bound. 357 Notice that the following def. only constraints block mapped through the embedding. 358 *) 359 definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝ 360 λE.λb.λm,m'. 361 match E b with 362 [ None ⇒ True 363  Some loc ⇒ 364 let 〈b', delta〉 ≝ loc in 365 block_implementable_bv m b ∧ 366 block_implementable_bv m' b' ∧ 367 (high_bound m b) + (Zoo delta) < Z_two_power_nat 16 368 ]. 369 322 370 323 371 (* Adapted from Compcert's Memory *) … … 326 374 ∀b1,b2,b1',b2',delta1,delta2. 327 375 b1 ≠ b2 → 328 block_region b1 = block_region b2 →376 (* block_region b1 = block_region b2 → *) (* let's be generous with this one *) 329 377 E b1 = Some ? 〈b1',delta1〉 → 330 378 E b2 = Some ? 〈b2',delta2〉 → 331 (b1' ≠ b2') ∨ 332 block_is_empty m b1' ∨ 333 block_is_empty m b2' ∨ 334 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 335 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1). 336 379 match block_decidable_eq b1' b2' with 380 [ inl Heq ⇒ 381 (* block_is_empty m b1' ∨ *) 382 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 383 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) 384  inr Hneq ⇒ True 385 ]. 386 387 388 (* Adapted from Compcert's "Memory" *) 389 337 390 (* Definition of a memory injection *) 338 391 record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝ … … 341 394 (* Invalid blocks are not mapped *) 342 395 (* mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; *) 343 (* Valid pointers are mapped to valid pointers *)396 (* Valid pointers are mapped to valid pointers *) 344 397 mi_valid_pointers : ∀p,p'. 345 398 valid_pointer m1 p = true → … … 347 400 valid_pointer m2 p' = true; 348 401 (* Blocks in the codomain are valid *) 349 (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)402 mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; 350 403 (* Regions are preserved *) 351 404 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; 352 405 (* subblocks do not overlap (nonaliasing property) *) 353 mi_nonalias : non_aliasing E m1 406 mi_nonalias : non_aliasing E m1; 407 (* mapped blocks are bitvectorimplementable *) 408 (* mi_implementable : 409 ∀b,b',o'. 410 E b = Some ? 〈b',o'〉 → 411 block_implementable_bv m1 b ∧ 412 block_implementable_bv m2 b'; *) 413 (* The offset produced by the embedding shifts data within the 2^16 bound ... 414 * We need this to rule out the following case: consider a huge block taking up 415 * all the space [0; 2^16[. We can come up with an embedding that keeps the same block 416 * but which shifts the data by some value, effectively rotating all the data around the 417 * 2^16 offset limit. Valid pointers stay valid, the block is implementable ... But we 418 * obviously can't prove that the semantics of pointer comparisons is preserved. *) 419 mi_nowrap : 420 ∀b. block_in_bounds_if_mapped E b m1 m2 354 421 }. 355 422 … … 363 430 normalize in Hptr_trans; destruct 364 431  2: * #b #o #p' #_ normalize #Habsurd destruct 365  3: #b #b' #o' #Habsurd destruct 366  4: normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct ] 367 qed. 432  3: #b #b' #off #Habsurd destruct 433  4: #b #b' #o' #Habsurd destruct 434  5: whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct 435  6: #b whd @I 436 ] qed. 368 437 369 438 (*  *) 370 439 (* End of the definitions on memory injections. Now, on to proving some lemmas. *) 440 (*  *) 441 442 443 444 (**** Lemmas on value_eq. *) 371 445 372 446 (* particulars inversions. *) … … 419 493 qed. 420 494 495 (* embedding compatibility preserves value equivalence *) 496 (* This is lemma 65 of Leroy&Blazy. *) 497 lemma embedding_compatibility_value_eq : 498 ∀E,E'. embedding_compatible E E' → ∀v1,v2. value_eq E v1 v2 → value_eq E' v1 v2. 499 #E #E' #Hcompat #v1 #v2 #Hvalue_eq 500 @(value_eq_inversion … Hvalue_eq) try // 501 #p1 #p2 whd in match (pointer_translation ??); cases p1 #b1 #o1 normalize nodelta 502 cases (Hcompat b1) 503 [ #Hnone >Hnone normalize nodelta #Habsurd destruct 504  #Heq >Heq #Hres %4 @Hres ] 505 qed. 506 507 508 509 510 (**** Lemmas on pointer validity wrt loads. *) 421 511 422 512 (* If we succeed to load something by value from a 〈b,off〉 location, … … 492 582 qed. 493 583 584 585 586 (**** Lemmas related to memory injections. *) 587 494 588 (* Making explicit the contents of memory_inj for load_value_of_type. 495 589 * Equivalent to Lemma 59 of Leroy & Blazy *) … … 512 606 qed. 513 607 514 (*  *) 608 515 609 (* Lemmas pertaining to memory allocation *) 516 610 … … 577 671 ∀H:memory_inj E m1 m2. 578 672 alloc m2 z1 z2 r = 〈m2', new_block〉 → 673 block_implementable_bv m2' new_block → 579 674 memory_inj E m1 m2'. 580 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc 675 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc #Himpl 581 676 % 582 677 [ whd … … 612 707 #Hbid_neq >Hbid_neq 613 708 cases (eq_region br' r) normalize #H @H 709  #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H 710 @(alloc_valid_block_conservation … Halloc … H) 614 711  @(mi_region … Hmemory_inj) 615  @(mi_nonalias … Hmemory_inj) 616 qed. 712  @(mi_nonalias … Hmemory_inj) 713  #b lapply (mi_nowrap … Hmemory_inj b) 714 whd in ⊢ (% → %); 715 lapply (mi_nodangling … Hmemory_inj b) 716 cases (E b) normalize nodelta try // 717 * #B #OFF normalize nodelta #Hguard 718 * * #H1 #H2 #Hinbounds @conj try @conj try assumption 719 @(eq_block_elim … new_block B) 720 [ #H destruct try // 721  #H cases m2 in Halloc H2; #contents #nextblock #notnull 722 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) * 723 >unfold_low_bound >unfold_high_bound #HA #HB 724 @conj 725 >unfold_low_bound >unfold_high_bound 726 whd in match (update_block ?????); 727 >(not_eq_block … (sym_neq ??? H)) normalize nodelta 728 try assumption ] 729 ] qed. 730 (* 731  @(eq_block_elim … new_block B) 732 [ 2: #H cases m2 in Halloc Hinbounds; #contents #nextblock #notnull 733 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 734 >unfold_high_bound in Himpl ⊢ %; 735 whd in ⊢ (% → % → %); 736 >unfold_low_bound >unfold_high_bound 737 whd in match (update_block ?????); >eq_block_b_b 738 normalize nodelta * #HA #HB 739 >unfold_high_bound 740 whd in match (update_block ?????) in ⊢ (% → %); 741 >(not_eq_block … (sym_neq ??? H)) normalize nodelta 742 try // 743  (* absurd case *) #Heq destruct (Heq) 744 lapply (Hguard ?? (refl ??)) #Hvalid 745 (* hence new_block ≠ B *) 746 cases m2 in Halloc Hvalid; #contents #nextblock #notnull 747 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 748 whd in ⊢ (% → ?); #Habsurd 749 lapply (irreflexive_Zlt nextblock) * 750 #H @False_ind @H @Habsurd 751 ] 752 ] 753 ] 754 qed. *) 755 756 757 (* TODO: these axioms are not enough for memory injections. We need the updated embedding as a byproduct 758 * of the allocation. *) 617 759 618 760 (* Allocating in m1 such that the resulting block has no image in m2 preserves … … 686 828 normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl 687 829 %4 @Htrans ] 688 #Hload <Hfree 830 #Hload <Hfree 689 831 (* routine *) 690 832 @cthulhu … … 727 869 #E #m1 #m2 #m1' #Hinj #b #Hfree 728 870 cases Hinj 729 #Hload_sim #Hvalid #H region #Hnonalias871 #Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable 730 872 % try assumption 731 873 [ @(free_load_sim_ptr_m1 … Hload_sim … Hfree) 732 874  #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation) 733 875 <Hfree in Hvalid_m1'; @valid_free_to_valid 734  @(free_non_aliasing_m1 … Hinj … Hfree) ] 735 qed. 876  @(free_non_aliasing_m1 … Hinj … Hfree) 877  #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?); 878 cases (E bb) normalize nodelta try // 879 * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj 880 try // 881 @(eq_block_elim … b bb) 882 [ 2,4: 883 #Hneq destruct (Hfree) 884 whd in match (free ??); 885 whd >unfold_low_bound >unfold_high_bound 886 whd in match (update_block ?????); >(not_eq_block … (sym_neq ??? Hneq)) 887 try @conj normalize nodelta cases HA try // 888  1,3: 889 #H destruct whd in match (free ??); 890 whd [ >unfold_low_bound ] >unfold_high_bound 891 whd in match (update_block ?????); >eq_block_b_b 892 normalize nodelta try @conj try // % try // 893 ] 894 ] qed. 895 896 (* 897 #b0 #b' #o' #Hembed lapply (Himplementable b0 b' o' Hembed) * 898 #HA #HB @conj try // 899 cases m1 in Hfree HA; #contents1 #nextblock1 #Hpos1 900 whd in ⊢ ((??%%) → ? → ?); #Heq destruct (Heq) 901 whd in ⊢ (% → %); * 902 whd in match (low_bound ??) in ⊢ (% → % → %); 903 whd in match (high_bound ??) in ⊢ (% → % → %); #HA #HB 904 @(eq_block_elim … b0 b) 905 [ #H whd in match (update_block ?????); >H >eq_block_b_b @conj 906 normalize nodelta 907 normalize @conj try // 908  #H whd in match (update_block ?????); >(not_eq_block … H) @conj 909 try // ] ] 910 qed.*) 736 911 737 912 (* Lifting lemma 47 to memory injs *) … … 745 920 #E #m1 #m2 #m2' #Hinj #b #Hfree #b1_not_mapped 746 921 % cases Hinj try // 747 #Hload_sim #Hvalid #H region #Hnonalias922 #Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl 748 923 [ (* We succed performing a load from m1. Case analysis: if byvalue, cannot map to freed block [b] 749 924 (otherwise contradiction), hence simulation proceeds through Hinj. … … 757 932 if (pblock p') ≠ b then straightforward simulation *) 758 933 @cthulhu 759  @Hregion ] 760 qed. 934  #bb #b' #o' #Hembed 935 lapply (Hnodangling bb b' o' Hembed) #Hvalid_before_free 936 (* cf case above *) 937 @cthulhu 938  @Hregion 939  #bb lapply (Himpl bb) 940 whd in ⊢ (% → %); cases (E bb) normalize nodelta try // 941 * #BLO #OFF normalize nodelta * * destruct (Hfree) 942 #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption 943 cases Hbb try // #Hlow_bb #Hhigh_bb 944 [ >unfold_low_bound 945  *: >unfold_high_bound ] 946 whd in match (update_block ?????); 947 @(eq_block_elim … BLO b) 948 #H [ 1,3,5: destruct (H) normalize nodelta try // 949 @conj try // 950  *: normalize nodelta cases HBLO try // ] 951 ] qed. 952 761 953 762 954 (* Lemma 64 of L&B on [freelist] *) … … 969 1161 cases storety 970 1162 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 971  #structname #fieldspec  #unionname #fieldspec  #id ] #Hout #storeval #Hstore whd1163  #structname #fieldspec  #unionname #fieldspec  #id ] #Hout #storeval #Hstore whd 972 1164 #b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value 973 1165 whd in Hstore:(??%?); … … 1024 1216 #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % 1025 1217 lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // 1026 cases Hinj #Hsim' #Hvalid #Hregion #Hnonalias try assumption 1027 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid 1028 cases ty in Hstore; 1029 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1030  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1031 whd in ⊢ ((??%?) → ?); 1032 [ 1,4,5,6,7: #Habsurd destruct ] 1033 cases (fe_to_be_values ??) 1034 [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid Hvalid destruct @refl 1035  *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_ 1036 @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh 1037 @conj try @conj try assumption >Hnext try // 1038 cases (Hbounds (pblock p')) #HA #HB 1039 whd in match (low_bound ??); whd in match (high_bound ??); 1040 >HA >HB try assumption 1218 cases Hinj #Hsim' #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption 1219 [ 1220 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid 1221 cases ty in Hstore; 1222 [  #sz' #sg'  #ptr_ty'  #array_ty' #array_sz'  #domain' #codomain' 1223  #structname' #fieldspec'  #unionname' #fieldspec'  #id' ] 1224 whd in ⊢ ((??%?) → ?); 1225 [ 1,4,5,6,7: #Habsurd destruct ] 1226 cases (fe_to_be_values ??) 1227 [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid Hvalid destruct @refl 1228  *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_ 1229 @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh 1230 @conj try @conj try assumption >Hnext try // 1231 cases (Hbounds (pblock p')) #HA #HB 1232 whd in match (low_bound ??); whd in match (high_bound ??); 1233 >HA >HB try assumption 1234 ] 1235  lapply (mem_bounds_after_store_value_of_type … Hstore) 1236 * #Hnext_eq #Hb 1237 #b #b' #o' cases (Hb b') #Hlow_eq #Hhigh_eq #Hembed 1238 lapply (mi_nodangling … Hinj … Hembed) 1239 whd in match (valid_block ??) in ⊢ (% → %); 1240 >(Hnext_eq) try // 1241  #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %); 1242 cases (E b) try // 1243 * #BLO #OFF normalize nodelta * * 1244 #Hb #HBLO #Hbound try @conj try @conj try assumption 1245 lapply (mem_bounds_after_store_value_of_type … Hstore) * 1246 #_ #Hbounds 1247 cases (Hbounds BLO) #Hlow #Hhigh whd % 1248 [ >unfold_low_bound  >unfold_high_bound ] 1249 >Hlow >Hhigh cases HBLO try // 1041 1250 ] qed. 1042 1251 … … 1202 1411 The memory model of Cerco is in a sense much more realistic. When storing a frontend 1203 1412 value fv, the story is the following : 1204 1) the value fv is marsh elled into a list of backend values (bytesized) which correspond1413 1) the value fv is marshalled into a list of backend values (bytesized) which correspond 1205 1414 to the actual size of the data inmemory. This list is then stored asis at the 1206 1415 location 〈block, offset〉. … … 1297 1506 load_sim_ptr E m1' m2. 1298 1507 #E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore 1299 cases Hinj #Hsim #Hvalid #H region_eq #Hnonalias1508 cases Hinj #Hsim #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl 1300 1509 cases ty in Hstore; 1301 1510 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain … … 1309 1518 destruct ] 1310 1519 #Heq <Heq in Hload; #Hload 1311 (* Three times the same proof, but computing the indices is a PITA *)1520 (* Three times the same proof, but computing the indices for the subcases is a PITA *) 1312 1521 [ 1: 1313 1522 cases ty' in Hload; … … 1337 1546 #Hload @(Hsim … Hembed' … Hload) 1338 1547 @(load_by_value_success_valid_pointer … Hload) // 1339 ] qed. 1548 ] qed. 1340 1549 1341 1550 lemma store_value_of_type_memory_inj : … … 1349 1558 % 1350 1559 [ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore) 1351  2: (* trivial *) @cthulhu 1352  3: (* easy *) @cthulhu 1353  4: (* writing doesn't alter the bound, straightforward *) @cthulhu ] 1354 qed. 1560  *: (* writing doesn't alter the bound, straightforward *) @cthulhu ] 1561 qed. (* TODO *) 1355 1562 1356 1563 (*  *) … … 1882 2089 ] qed. 1883 2090 1884 1885 (* /!\ Here is the source of all sadness (op = lt) /!\ *) 1886 axiom cmp_offset_translation : ∀op,delta,x,y. 1887 cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). 1888 1889 (* 5 Nov. 2012 : the rest of the stuff doesn't checks anymore. Not a big deal, it was here 1890 * for historical purposes, and for potential inspiration for Clight to Cminor. I leave the 1891 * code commented for future reference. 1892 *) 1893 1894 (* 2091 (* /!\ Warning TODO Warning /!\ *) 2092 2093 (* Note that x and y are bounded below and above, similarly for the shifted offsets. 2094 This is enough to prove that there is no "wraparoundtheend" problem, 2095 /provided we know that the block bounds are implementable by 2^16 bitvectors/. 2096 We axiomatize it for now. Notice that this axiom is in fact not provable and implies False. 2097 In order to be true, we need to prove that the (x+delta) and (y+delta) do not overflow. 2098 This is provable from the fact that the original pointers in which the offsets reside are "valid". 2099 This in turn is ensured by the memory injection. 2100 /DO NOT USE IT ELSEWHERE, this is just a temporary stopgap./ *) 2101 axiom cmp_offset_translation : 2102 ∀op,delta,x,y. 2103 (Zoo x) + (Zoo delta) < Z_two_power_nat 16 → 2104 (Zoo y) + (Zoo delta) < Z_two_power_nat 16 → 2105 cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). 2106 2107 (* TODO: move in frontend_misc *) 2108 lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y. 2109 #x #y /3 by absurd, nmk/ 2110 qed. 2111 2112 lemma Zlt_translate : ∀x,y,delta:Z. x < y → x + delta < y + delta. 2113 #x #y #delta /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle/ 2114 qed. 2115 2116 lemma Zlt_weaken : ∀x,y,delta:Z. delta ≥ 0 → x < y → x < y + delta. 2117 #x #y #delta cases delta try // #p 2118 [ 2: #Habsurd @(False_ind … Habsurd) ] 2119 /3 by Zlt_to_Zle_to_Zlt, Zplus_le_pos/ 2120 qed. 2121 2122 lemma Zlt_sum_weaken : ∀a,a',b,c:Z. a+b < c → a' < a → a'+b < c. 2123 #a #a' #b #c /3 by transitive_Zlt, Zlt_translate/ qed. 2124 2125 (* TODO: move in frontend_misc. This axiom states that for small bitvectors, bitvector addition 2126 * commutes with conversion to Z, i.e. there is no overflow. *) 2127 axiom Z_addition_bv_commute : 2128 ∀n. ∀v1,v2:BitVector n. 2129 (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2) < Z_two_power_nat n → 2130 Z_of_unsigned_bitvector ? (addition_n ? v1 v2) = 2131 (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2). 2132 2133 lemma valid_pointer_of_implementable_block_is_implementable : 2134 ∀m,b. 2135 block_implementable_bv m b → 2136 ∀o. valid_pointer m (mk_pointer b o) = true → 2137 Zoo o < Z_two_power_nat 16. 2138 #m #b whd in ⊢ (% → ?); * #Hlow #Hhigh 2139 * #o #Hvalid cases (valid_pointer_to_Prop … Hvalid) * #_ 2140 #Hlow' #Hhigh' 2141 cases Hlow Hlow #Hlow0 #Hlow16 2142 cases Hhigh Hhigh #Hhigh0 #Hhigh16 2143 whd in match (Zoo ?); 2144 @(transitive_Zlt … Hhigh' Hhigh16) 2145 qed. 2146 1895 2147 lemma cmp_value_eq : 1896 2148 ∀E,v1,v2,v1',v2',ty,ty',m1,m2. 1897 2149 value_eq E v1 v2 → 1898 2150 value_eq E v1' v2' → 1899 memory_inj E m1 m2 → 1900 ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1 →2151 memory_inj E m1 m2 → 2152 ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1 → 1901 2153 ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). 1902 2154 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 … … 1906 2158 [ 1: #tsz #tsg 1907 2159 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 1908 [ 1: #v #Habsurd destruct (Habsurd) 1909  3: #f #Habsurd destruct (Habsurd) 1910  4: #Habsurd destruct (Habsurd) 1911  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 2160 [ 1: #Habsurd destruct (Habsurd) 2161  3: #Habsurd destruct (Habsurd) 2162  4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 1912 2163 #sz #i 1913 2164 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1914 [ 1: #v #Habsurd destruct (Habsurd) 1915  3: #f #Habsurd destruct (Habsurd) 1916  4: #Habsurd destruct (Habsurd) 1917  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 2165 [ 1: #Habsurd destruct (Habsurd) 2166  3: #Habsurd destruct (Habsurd) 2167  4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 1918 2168 #sz' #i' cases tsg normalize nodelta 1919 2169 @intsize_eq_elim_elim … … 1924 2174  2: cases (cmpu_int ????) whd in match (of_bool ?); ] 1925 2175 /3 by ex_intro, conj, vint_eq/ ] 1926  3: #fsz 2176  3: #ty1 #ty2 #Habsurd destruct (Habsurd) 2177  2: lapply Hinj Hinj 2178 generalize in match (mk_mem contmap1 ??); #m1 2179 generalize in match (mk_mem contmap2 ??); #m2 2180 #Hinj #optn #typ 1927 2181 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 1928 [ 1: # v #Habsurd destruct (Habsurd)2182 [ 1: #Habsurd destruct (Habsurd) 1929 2183  2: #sz #i #Habsurd destruct (Habsurd) 1930  4: #Habsurd destruct (Habsurd) 1931  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 1932 #f 2184  4: #p1 #p2 #Hembed ] 1933 2185 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1934 [ 1: #v #Habsurd destruct (Habsurd) 1935  2: #sz #i #Habsurd destruct (Habsurd) 1936  4: #Habsurd destruct (Habsurd) 1937  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 1938 #f' 1939 #Heq destruct (Heq) cases (Fcmp op f f') 1940 /3 by ex_intro, conj, vint_eq/ 1941  4: #ty1 #ty2 #Habsurd destruct (Habsurd) 1942  2: #optn #typ 1943 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 1944 [ 1: #v #Habsurd destruct (Habsurd) 1945  2: #sz #i #Habsurd destruct (Habsurd) 1946  3: #f #Habsurd destruct (Habsurd) 1947  5: #p1 #p2 #Hembed ] 1948 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 1949 [ 1,6: #v #Habsurd destruct (Habsurd) 1950  2,7: #sz #i #Habsurd destruct (Habsurd) 1951  3,8: #f #Habsurd destruct (Habsurd) 1952  5,10: #p1' #p2' #Hembed' ] 2186 [ 1,5: #Habsurd destruct (Habsurd) 2187  2,6: #sz #i #Habsurd destruct (Habsurd) 2188  4,8: #q1 #q2 #Hembed' ] 1953 2189 [ 2,3: cases op whd in match (sem_cmp_mismatch ?); 1954 2190 #Heq destruct (Heq) … … 1959 2195 [ 2,4: %{Vfalse} @conj try @refl @vint_eq 1960 2196  1,3: %{Vtrue} @conj try @refl @vint_eq ] ] 1961 lapply (mi_valid_pointers … Hinj p1' p2') 1962 lapply (mi_valid_pointers … Hinj p1 p2) 1963 cases (valid_pointer (mk_mem ???) p1') 1964 [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 1965 cases (valid_pointer (mk_mem ???) p1) 1966 [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 1967 #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2 1968 >Hvalid1 >Hvalid2 normalize nodelta H1 H2 1969 elim p1 in Hembed; #b1 #o1 1970 elim p1' in Hembed'; #b1' #o1' 2197 #Hvalid 2198 lapply (if_opt_inversion ???? Hvalid) Hvalid * #Hconj 2199 lapply (andb_inversion … Hconj) Hconj * #Hvalid #Hvalid' 2200 lapply (mi_valid_pointers … Hinj q1 q2 Hvalid' Hembed') #Hvalid2' >Hvalid2' 2201 lapply (mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) #Hvalid2 >Hvalid2 2202 normalize nodelta 2203 (* >(mi_valid_pointers … Hinj p1' p2' Hvalid' Hembed') 2204 >(mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) normalize nodelta *) 2205 elim p1 in Hvalid Hembed; #bp1 #op1 2206 elim q1 in Hvalid' Hembed'; #bq1 #oq1 2207 #Hvalid' #Htmp #Hvalid lapply Htmp Htmp 1971 2208 whd in match (pointer_translation ??); 1972 2209 whd in match (pointer_translation ??); 1973 @(eq_block_elim … b1 b1') 1974 [ 1: #Heq destruct (Heq) 1975 cases (E b1') normalize nodelta 1976 [ 1: #Habsurd destruct (Habsurd) ] 1977 * #eb1' #eo1' normalize nodelta 2210 @(eq_block_elim … bp1 bq1) 2211 [ 1: #Heq destruct (Heq) normalize nodelta 2212 lapply (mi_nowrap … Hinj bq1) 2213 whd in ⊢ (% → ?); 2214 cases (E bq1) normalize nodelta 2215 [ #_ #Habsurd destruct ] 2216 * #BLO #OFF normalize nodelta * * 2217 #Hbq1_implementable #HBLO_implementable #Hno_wrap 1978 2218 #Heq1 #Heq2 #Heq3 destruct 1979 2219 >eq_block_b_b normalize nodelta 1980 <cmp_offset_translation 1981 cases (cmp_offset ???) normalize nodelta 1982 /3 by ex_intro, conj, vint_eq/ 1983  2: #Hneq lapply (mi_disjoint … Hinj b1 b1') 1984 cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 1985 * #eb1 #eo1 1986 cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] 1987 * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct 1988 lapply (H ???? Hneq (refl ??) (refl ??)) 1989 #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta 1990 elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) 1991 /3 by ex_intro, conj, vint_eq/ 1992 ] 1993 ] qed. *) 1994 1995 (* 1996 lemma binary_operation_value_eq : 1997 ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2. 1998 value_eq E v1 v2 → 1999 value_eq E v1' v2' → 2000 memory_inj E m1 m2 → 2001 ∀r1. 2002 sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 → 2003 ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2. 2004 #E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1 2005 cases op 2006 whd in match (sem_binary_operation ??????); 2007 whd in match (sem_binary_operation ??????); 2008 [ 1: @add_value_eq try assumption 2009  2: @sub_value_eq try assumption 2010  3: @mul_value_eq try assumption 2011  4: @div_value_eq try assumption 2012  5: @mod_value_eq try assumption 2013  6: @and_value_eq try assumption 2014  7: @or_value_eq try assumption 2015  8: @xor_value_eq try assumption 2016  9: @shl_value_eq try assumption 2017  10: @shr_value_eq try assumption 2018  *: @cmp_value_eq try assumption 2019 ] qed. *) 2020 2021 (* 2022 lemma cast_value_eq : 2023 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 → 2024 ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res → 2025 ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'. 2026 #E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res 2027 @(value_eq_inversion … Hvalue_eq) 2028 [ 1: #v normalize #Habsurd destruct (Habsurd) 2029  2: #vsz #vi whd in match (exec_cast ????); 2030 cases ty 2031 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 2032 normalize nodelta 2033 [ 1,3,7,8,9: #Habsurd destruct (Habsurd) 2034  2: @intsize_eq_elim_elim 2035 [ 1: #Hneq #Habsurd destruct (Habsurd) 2036  2: #Heq destruct (Heq) normalize nodelta 2037 cases cast_ty 2038 [ 1:  2: #csz #csg  3: #cfl  4: #cptrty  5: #carrayty #cn 2039  6: #ctl #cretty  7: #cid #cfl  8: #cid #cfl  9: #ccomptrty ] 2040 normalize nodelta 2041 [ 1,7,8,9: #Habsurd destruct (Habsurd) 2042  2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/ 2043  3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/ 2044  4,5,6: whd in match (try_cast_null ?????); normalize nodelta 2045 @eq_bv_elim 2046 [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta 2047 whd in match (m_bind ?????); 2048 #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 2049  2,4,6: #Hneq >eq_intsize_identity normalize nodelta 2050 whd in match (m_bind ?????); 2051 #Habsurd destruct (Habsurd) ] ] 2052 ] 2053  4,5,6: whd in match (try_cast_null ?????); normalize nodelta 2054 @eq_bv_elim 2055 [ 1,3,5: #Heq destruct (Heq) normalize nodelta 2056 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) 2057  2,4,6: #Hneq normalize nodelta 2058 whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ] 2059 ] 2060  3: #f whd in match (exec_cast ????); 2061 cases ty 2062 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n 2063  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 2064 normalize nodelta 2065 [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 2066 cases cast_ty 2067 [ 1:  2: #csz #csg  3: #cfl  4: #cptrty  5: #carrayty #cn 2068  6: #ctl #cretty  7: #cid #cfl  8: #cid #cfl  9: #ccomptrty ] 2069 normalize nodelta 2070 [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 2071 #Heq destruct (Heq) 2072 [ 1: /3 by ex_intro, conj, vint_eq/ 2073  2: /3 by ex_intro, conj, vfloat_eq/ ] 2074  4: whd in match (exec_cast ????); 2075 cases ty 2076 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n 2077  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 2078 normalize 2079 [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] 2080 cases cast_ty normalize nodelta 2081 [ 1,10,19: #Habsurd destruct (Habsurd) 2082  2,11,20: #csz #csg #Habsurd destruct (Habsurd) 2083  3,12,21: #cfl #Habsurd destruct (Habsurd) 2084  4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 2085  5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 2086  6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ 2087  7,16,25: #cid #cfl #Habsurd destruct (Habsurd) 2088  8,17,26: #cid #cfl #Habsurd destruct (Habsurd) 2089  9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] 2090  5: #p1 #p2 #Hembed whd in match (exec_cast ????); 2091 cases ty 2092 [ 1:  2: #sz #sg  3: #fl  4: #ptrty  5: #arrayty #n 2093  6: #tl #retty  7: #id #fl  8: #id #fl  9: #comptrty ] 2094 normalize 2095 [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] 2096 cases cast_ty normalize nodelta 2097 [ 1,10,19: #Habsurd destruct (Habsurd) 2098  2,11,20: #csz #csg #Habsurd destruct (Habsurd) 2099  3,12,21: #cfl #Habsurd destruct (Habsurd) 2100  4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption 2101  5,14,23: #carrayty #cn #Heq destruct (Heq) 2102 %{(Vptr p2)} @conj try @refl @vptr_eq assumption 2103  6,15,24: #ctl #cretty #Heq destruct (Heq) 2104 %{(Vptr p2)} @conj try @refl @vptr_eq assumption 2105  7,16,25: #cid #cfl #Habsurd destruct (Habsurd) 2106  8,17,26: #cid #cfl #Habsurd destruct (Habsurd) 2107  9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] 2108 qed. 2109 2110 lemma bool_of_val_value_eq : 2111 ∀E,v1,v2. value_eq E v1 v2 → 2112 ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b. 2113 #E #v1 #v2 #Hvalue_eq #ty #b 2114 @(value_eq_inversion … Hvalue_eq) // 2115 [ 1: #v #H normalize in H; destruct (H) 2116  2: #p1 #p2 #Hembed #H @H ] qed. 2117 2118 *) 2119 (* 2120 lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext. 2121 ∀E:embedding. 2122 ∀Hext:memory_ext E m1 m2. 2123 switch_removal_globals E ? fundef_switch_removal ge ge' → 2124 disjoint_extension en1 m1 en2 m2 ext E Hext → 2125 ext_fresh_for_genv ext ge → 2126 (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ 2127 (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). 2128 #ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv 2129 @expr_lvalue_ind_combined 2130 [ 1: #csz #cty #i #a1 2131 whd in match (exec_expr ????); elim cty 2132 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 2133 normalize nodelta 2134 [ 2: cases (eq_intsize csz sz) normalize nodelta 2135 [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ 2136  2: #Habsurd destruct (Habsurd) ] 2137  4,5,6: #_ #H destruct (H) 2138  *: #H destruct (H) ] 2139  2: #ty #fl #a1 2140 whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/ 2141  3: * 2142 [ 1: #sz #i  2: #fl  3: #var_id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8: #cast_ty #e1 2143  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14: #cost #e1 ] 2144 #ty whd in ⊢ (% → ?); #Hind try @I 2145 whd in match (Plvalue ???); 2146 [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 2147 cases (exec_lvalue' ge en1 m1 ? ty) in Hind; 2148 [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2149  1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 * 2150 elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2 2151 #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq 2152 whd in match (load_value_of_type' ???); 2153 whd in match (load_value_of_type' ???); 2154 lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq) 2155 cases (load_value_of_type ty m1 bl1 o1) 2156 [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) 2157  2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq) 2158 elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload 2159 normalize /4 by ex_intro, conj/ 2160 ] ] ] 2161  4: #v #ty whd * * #b1 #o1 #tr1 2162 whd in match (exec_lvalue' ?????); 2163 whd in match (exec_lvalue' ?????); 2164 lapply (Hdisjoint v) 2165 lapply (Hext_fresh_for_genv v) 2166 cases (mem_assoc_env v ext) #Hglobal 2167 [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1 2168 >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?); 2169 >(Hglobal (refl ??)) normalize 2170 #Habsurd destruct (Habsurd) 2171  2: normalize nodelta 2172 cases (lookup ?? en1 v) normalize nodelta 2173 [ 1: #Hlookup2 >Hlookup2 normalize nodelta 2174 lapply (rg_find_symbol … Hrelated v) 2175 cases (find_symbol ???) normalize 2176 [ 1: #_ #Habsurd destruct (Habsurd) 2177  2: #block cases (lookup ?? (symbols clight_fundef ge') v) 2178 [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse) 2179  2: #block' normalize #Hvalue_eq #Heq destruct (Heq) 2180 %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl 2181 normalize /2/ 2182 ] ] 2183  2: #block 2184 cases (lookup ?? en2 v) normalize nodelta 2185 [ 1: #Hfalse @(False_ind … Hfalse) 2186  2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq) 2187 %{〈b, zero_offset, E0〉} @conj try @refl 2188 normalize /2/ 2189 ] ] ] 2190  5: #e #ty whd in ⊢ (% → %); 2191 whd in match (exec_lvalue' ?????); 2192 whd in match (exec_lvalue' ?????); 2193 cases (exec_expr ge en1 m1 e) 2194 [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta 2195 * elim v1 normalize nodelta 2196 [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd) 2197  2: #sz #i #_ #_ #a1 #Habsurd destruct (Habsurd) 2198  3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd) 2199  4: #_ #_ #a1 #Habsurd destruct (Habsurd) 2200  5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq 2201 >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2 2202 #Hvalue_eq normalize 2203 cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2204 * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace) 2205 * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize 2206 %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl 2207 normalize @conj // ] 2208  2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] 2209  6: #ty #e #ty' 2210 #Hsim @(exec_lvalue_expr_elim … Hsim) 2211 cases ty 2212 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 2213 * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/ 2214 #tr #H @conj try @refl try assumption 2215  7: #ty #op #e 2216 #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq 2217 lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq) 2218 cases (sem_unary_operation op v1 (typeof e)) normalize nodelta 2219 [ 1: #_ @I 2220  2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq 2221 normalize /2/ ] 2222  8: #ty #op #e1 #e2 #Hsim1 #Hsim2 2223 @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq 2224 cases (exec_expr ge en1 m1 e2) in Hsim2; 2225 [ 2: #error // ] 2226 * #val #trace normalize in ⊢ (% → ?); #Hsim2 2227 elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2 2228 whd in match (m_bind ?????); whd in match (m_bind ?????); 2229 lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext)) 2230 cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1) 2231 [ 1: #_ // ] 2232 #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq #Hvalue_eq_opval 2233 >Hopval_eq normalize destruct /2 by conj/ 2234  9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) 2235 #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty) 2236 cases (exec_cast m1 v1 (typeof e) cast_ty) 2237 [ 2: #error #_ normalize @I 2238  1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????); 2239 * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta 2240 @conj // ] 2241  10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 2242 @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq 2243 lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1)) 2244 cases (exec_bool_of_val ? (typeof e1)) #b 2245 [ 2: #_ normalize @I ] 2246 #H lapply (H ? (refl ??)) #Hexec >Hexec normalize 2247 cases b normalize nodelta 2248 [ 1: (* true branch *) 2249 cases (exec_expr ge en1 m1 e2) in Hsim2; 2250 [ 2: #error normalize #_ @I 2251  1: * #e2v #e2tr normalize #H elim (H ? (refl ??)) 2252 * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize 2253 destruct @conj try // ] 2254  2: (* false branch *) 2255 cases (exec_expr ge en1 m1 e3) in Hsim3; 2256 [ 2: #error normalize #_ @I 2257  1: * #e3v #e3tr normalize #H elim (H ? (refl ??)) 2258 * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize 2259 destruct @conj // ] ] 2260  11,12: #ty #e1 #e2 #Hsim1 #Hsim2 2261 @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq 2262 lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1)) 2263 cases (exec_bool_of_val v1 (typeof e1)) 2264 [ 2,4: #error #_ normalize @I ] 2265 #b cases b #H lapply (H ? (refl ??)) #Heq >Heq 2266 whd in match (m_bind ?????); 2267 whd in match (m_bind ?????); 2268 [ 2,3: normalize @conj try @refl try @vint_eq ] 2269 cases (exec_expr ge en1 m1 e2) in Hsim2; 2270 [ 2,4: #error #_ normalize @I ] 2271 * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??)) 2272 * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta 2273 lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2)) 2274 cases (exec_bool_of_val v2 (typeof e2)) 2275 [ 2,4: #error #_ normalize @I ] 2276 #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta 2277 destruct @conj try @conj // 2278 cases b2 whd in match (of_bool ?); @vint_eq 2279  13: #ty #ty' cases ty 2280 [ 1:  2: #sz #sg  3: #fl  4: #ty  5: #ty #n 2281  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ] 2282 whd in match (exec_expr ????); whd 2283 * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉} 2284 @conj try @refl @conj // 2285  14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta 2286 whd in match (exec_lvalue' ?????); 2287 whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); 2288 whd in match (typeof ?); 2289 cases aggregty in Hsim; 2290 [ 1:  2: #sz' #sg'  3: #fl'  4: #ty'  5: #ty' #n' 2291  6: #tl' #ty'  7: #id' #fl'  8: #id' #fl'  9: #ty' ] 2292 normalize nodelta #Hsim 2293 [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ] 2294 whd in match (m_bind ?????); 2295 whd in match (m_bind ?????); 2296 whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); 2297 cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; 2298 [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2299 * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??)) 2300 * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq 2301 whd in match (exec_lvalue ????); >Hexec normalize nodelta 2302 [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj // 2303 normalize @conj // ] 2304 cases (field_offset i fl') 2305 [ 2: #error normalize #Habsurd destruct (Habsurd) ] 2306 #offset whd in match (m_bind ?????); #Heq destruct (Heq) 2307 whd in match (m_bind ?????); 2308 %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj 2309 destruct // normalize nodelta @conj try @refl @vptr_eq 2310 H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq 2311 whd in match (pointer_translation ??); 2312 whd in match (pointer_translation ??); 2313 cases (E b) 2314 [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] 2315 * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq) 2316 cut (offset_plus (mk_offset (addition_n offset_size 2317 (offv o1) 2318 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o' 2319 = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset))) 2320 [ whd in match (shift_offset ???) in ⊢ (???%); 2321 whd in match (offset_plus ??) in ⊢ (??%%); 2322 /3 by associative_addition_n, commutative_addition_n, refl/ ] 2323 #Heq >Heq @refl 2324  15: #ty #l #e #Hsim 2325 @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj // 2326  16: * 2327 [ 1: #sz #i  2: #fl  3: #var_id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8: #cast_ty #e1 2328  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14: #cost #e1 ] 2329 #ty normalize in ⊢ (% → ?); 2330 [ 3,4,13: @False_ind 2331  *: #_ normalize #a1 #Habsurd destruct (Habsurd) ] 2332 ] qed. *) 2220 lapply (cmp_offset_translation op OFF op1 oq1 ??) 2221 [ @(Zlt_sum_weaken … Hno_wrap) 2222 cases (valid_pointer_to_Prop … Hvalid') * #_ #_ try // 2223  @(Zlt_sum_weaken … Hno_wrap) 2224 cases (valid_pointer_to_Prop … Hvalid) * #_ #_ try // ] 2225 #Heq <Heq 2226 cases (cmp_offset op op1 oq1) 2227 normalize nodelta 2228 try /3 by ex_intro, conj, refl, vint_eq/ 2229  2: #Hneq lapply (mi_nonalias … Hinj bp1 bq1) 2230 normalize nodelta 2231 lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?); 2232 lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?); 2233 cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2234 * #BLOq #DELTAq normalize nodelta 2235 cases (E bp1) [ 1: #_ #_ #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] 2236 * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct 2237 cases op 2238 whd in ⊢ ((??%?) → ?); #H' destruct (H') 2239 whd in match (sem_cmp_mismatch ?); 2240 lapply (H ???? Hneq (refl ??) (refl ??)) H 2241 cases (block_decidable_eq BLOp BLOq) normalize nodelta 2242 #H 2243 [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2 2244  4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ] 2245 destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %; 2246 #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1 2247 * * #Himplp1 #_ #Hnowrap_p1 #Hvalid2 #Hvalid2' 2248 lapply (valid_pointer_to_Prop … Hvalid) 2249 lapply (valid_pointer_to_Prop … Hvalid') 2250 * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp 2251 >eq_block_b_b normalize nodelta 2252 * 2253 #Hdisjoint 2254 whd in match (cmp_offset); normalize nodelta 2255 whd in match (eq_offset); normalize nodelta 2256 whd in match (offset_plus ??); 2257 whd in match (offset_plus ??); 2258 lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2) 2259 lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2') 2260 #Himpl1 #Himpl2 2261 [ 1,3: 2262 (* We show the nonequality of the rhs by exhibiting disjointness of blocks. This is made 2263 * painful by invariants on nonoverflowing offsets. We exhibit [a]+[b] < [c]+[d], then 2264 * cut [a+b]<[c+d] (using a subcut for needed consistency hypotheses) and conclude easily 2265 * [a+b] ≠ [c+d]. *) 2266 cut ((Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp)) 2267 < (Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq))) 2268 [ 1,3: 2269 @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bp1 + Zoo DELTAp) ?) 2270 [ 1,3: @Zlt_translate assumption 2271  2,4: @(transitive_Zle ? (low_bound m1 bq1+Zoo DELTAq) ?) try assumption 2272 @monotonic_Zle_Zplus_l try assumption ] 2273 ] 2274 #Hlt_stepA 2275 cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp)) 2276 < Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq))) 2277 [ 1,3: 2278 >Z_addition_bv_commute 2279 [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ] 2280 >Z_addition_bv_commute 2281 [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ] 2282 try assumption ] Hlt_stepA 2283  2,4: 2284 cut ((Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq)) 2285 < (Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp))) 2286 [ 1,3: 2287 @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bq1 + Zoo DELTAq) ?) 2288 [ 1,3: @Zlt_translate assumption 2289  2,4: @(transitive_Zle ? (low_bound m1 bp1+Zoo DELTAp) ?) try assumption 2290 @monotonic_Zle_Zplus_l try assumption ] 2291 ] 2292 #Hlt_stepA 2293 cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq)) 2294 < Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp))) 2295 [ 1,3: 2296 >Z_addition_bv_commute 2297 [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ] 2298 >Z_addition_bv_commute 2299 [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ] 2300 try assumption ] Hlt_stepA 2301 ] 2302 generalize in match (addition_n ? (offv op1) ?); #lhs 2303 generalize in match (addition_n ? (offv oq1) ?); #rhs 2304 #Hlt_stepB lapply (Zlt_to_Zneq … Hlt_stepB) 2305 @(eq_bv_elim … lhs rhs) 2306 [ 1,3,5,7: #Heq destruct * #H @(False_ind … (H (refl ??))) 2307  2,4,6,8: #Hneq #_ /3 by ex_intro, conj, vint_eq/ ] 2308 ] 2309 ] qed. 2310 
src/Clight/toCminorCorrectness.ma
r2572 r2578 1053 1053 qed. 1054 1054 1055 (* 1055 1056 lemma pointer_translation_cmp_offset : 1056 1057 ∀E,p1,p2,p1',p2',op. … … 1071 1072  @cthulhu (* !!!! TODO !!!! *) 1072 1073  @cthulhu (* !!!! TODO !!!! *) 1073 ] qed. 1074 ] qed. *) 1074 1075 1075 1076 (* The two following lemmas are just noise. *) … … 1130 1131 (we might wrap up the rhs and end SNAFU). 1131 1132 *) 1133 1132 1134 lemma eval_expr_sim : 1133 ∀(inv:clight_cminor_inv). 1134 ∀(f:function). 1135 ∀(vars:var_types). 1136 ∀stacksize. 1137 characterise_vars (globals inv) f = 〈vars, stacksize〉 → 1138 ∀(cl_env:cl_env). 1139 (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) → 1140 ∀(cl_m:mem). 1141 ∀(cm_env:cm_env). 1142 ∀(sp:block). 1143 ∀(cm_m:mem). 1144 ∀E:embedding. 1145 ∀minj:memory_inj E cl_m cm_m. 1146 memory_matching E cl_m cm_m cl_env cm_env inv sp vars → 1135 (* [cl_cm_inv] maps CL globals to CM globals, including functions *) 1136 ∀cl_cm_inv : clight_cminor_inv. 1137 (* current function (defines local environment) *) 1138 ∀f : function. 1139 (* [alloctype] maps variables to their allocation type (global, stack, register) *) 1140 ∀alloctype : var_types. 1141 ∀stacksize : ℕ. 1142 ∀alloc_hyp : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉. 1143 (* environments *) 1144 ∀cl_env : cl_env. 1145 ∀cm_env : cm_env. 1146 (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *) 1147 ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉. 1148 (* CL and CM memories *) 1149 ∀cl_m : mem. 1150 ∀cm_m : mem. 1151 (* memory injection and matching *) 1152 ∀embed : embedding. 1153 ∀injection : memory_inj embed cl_m cm_m. 1154 ∀stackptr : block. 1155 ∀matching : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype. 1147 1156 (* clight expr to cminor expr *) 1148 1157 (∀(e:expr). 1149 1158 ∀(e':CMexpr (typ_of_type (typeof e))). 1150 1159 ∀Hexpr_vars. 1151 translate_expr varse = OK ? («e', Hexpr_vars») →1160 translate_expr alloctype e = OK ? («e', Hexpr_vars») → 1152 1161 ∀cl_val,trace,Hyp_present. 1153 exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →1154 ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present spcm_m = OK ? 〈trace, cm_val〉 ∧1155 value_eq Ecl_val cm_val) ∧1162 exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 → 1163 ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧ 1164 value_eq embed cl_val cm_val) ∧ 1156 1165 (* clight /lvalue/ to cminor /expr/ *) 1157 1166 (∀ed,ty. 1158 1167 ∀(e':CMexpr ASTptr). 1159 1168 ∀Hexpr_vars. 1160 translate_addr vars(Expr ed ty) = OK ? («e', Hexpr_vars») →1169 translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») → 1161 1170 ∀cl_blo,cl_off,trace,Hyp_present. 1162 exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →1163 ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present spcm_m = OK ? 〈trace, cm_val〉 ∧1164 value_eq E(Vptr (mk_pointer cl_blo cl_off)) cm_val).1165 #inv #f #vars #stacksize #Hcharacterise #cl_env # Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj#Hlocal_matching1171 exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 → 1172 ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧ 1173 value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val). 1174 #inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching 1166 1175 @expr_lvalue_ind_combined 1167 1176 [ 7: (* binary ops *) … … 1626 1635 #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs 1627 1636 * #Hyp_present_lhs #Hyp_present_rhs 1628 #Hind_rhs #Hind_lhs 1637 #Hind_rhs #Hind_lhs 1629 1638 lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs) 1630 1639 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs … … 1667 1676 lapply (opt_to_res_inversion ???? Hsem) Hsem 1668 1677 whd in match (typeof ?); whd in match (sem_binary_operation ??????); 1669 #Hsem_cmp lapply (sem_cmp_ptr_inversion … Hsem_cmp) Hsem_cmp 1678 #Hsem_cmp (* cut > *) 1679 #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs 1680 * #Hyp_present_lhs #Hyp_present_rhs 1681 #Hind_rhs #Hind_lhs 1682 lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) 1683 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs 1684 lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) 1685 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs 1686 lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp) 1687 Hvalue_eq_lhs Hvalue_eq_rhs 1688 * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res %{cm_val} @conj try assumption 1689 lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) Hsem_cmp_cm Hsem_cmp 1670 1690 * 1671 1691 [ 2,4,6,8,10,12: … … 1679 1699  *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct 1680 1700 ] ] ] 1681 1682 (* #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); *)1683 #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs1684 * #Hyp_present_lhs #Hyp_present_rhs1685 #Hind_rhs #Hind_lhs1686 lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)1687 * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs Hind_rhs1688 lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)1689 * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs Hind_lhs1690 1701 whd in match (eval_expr ???????); 1691 1702 whd in match (eval_expr ???????); 1703 whd in Hsem_cmp:(??%?); 1704 destruct (Hsem_cmp) 1692 1705 >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta 1693 1706 >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta 1694 1707 whd in match (m_bind ?????); 1695 Heval_lhs Heval_rhs Hyp_present_rhs Hyp_present_lhs1696 Hexpr_vars_lhs Hexpr_vars_rhs1697 1708 whd in match (eval_binop ???????); 1698 [ 1,2,3,4,5,6: 1699 whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1700 >(value_eq_null_inversion … Hvalue_eq_lhs) 1701 >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta 1702 whd in match (eval_unop ????); 1703 whd in match (opt_to_res ???); 1704 whd in match (m_bind ?????); 1705 (* same glitch with integer widths *) 1709 [ 1,2,3,4,5,6: 1710 (* qed modulo integer width glitch *) 1706 1711 @cthulhu 1707  7,8,9,10,11,12: 1708 whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1709 >(value_eq_null_inversion … Hvalue_eq_lhs) normalize nodelta 1710 cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' 1711 * #Hcm_rhs_val #Hpointer_translation >Hcm_rhs_val normalize nodelta 1712 whd in match (eval_unop ????); 1713 whd in match (opt_to_res ???); 1714 whd in match (m_bind ?????); 1715 (* same glitch with integer widths *) 1716 @cthulhu 1717  13,14,15,16,17,18: 1718 whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1719 >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta 1720 cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' 1721 * #Hcm_lhs_val #Hpointer_translation >Hcm_lhs_val normalize nodelta 1722 whd in match (eval_unop ????); 1723 whd in match (opt_to_res ???); 1724 whd in match (m_bind ?????); 1725 (* same glitch with integer widths *) 1726 @cthulhu 1727  *: 1728 cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' * #Hcm_lhs #Hptr_translation_lhs 1729 cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' * #Hcm_rhs #Hptr_translation_rhs 1730 destruct (Hcm_lhs Hcm_rhs) normalize nodelta 1731 Hvalue_eq_lhs Hvalue_eq_rhs Hexec_lhs Hexec_rhs 1732 >(mi_valid_pointers … Hinj … Hvalid_p1 … Hptr_translation_lhs) 1733 >(mi_valid_pointers … Hinj … Hvalid_p2 … Hptr_translation_rhs) normalize nodelta 1734 lapply Heq_block_outcome Heq_block_outcome 1735 @(match eq_block (pblock p1) (pblock p2) 1736 return λb. (eq_block (pblock p1) (pblock p2)) = b → ? 1737 with 1738 [ true ⇒ λH. ? 1739  false ⇒ λH. ? 1740 ] (refl ? (eq_block (pblock p1) (pblock p2)))) normalize nodelta 1741 [ 1,3,5,7,9,11: 1742 (* block equality in the Clight memory *) 1743 (* entails block equality in the Cminor memory *) 1744 >(pointer_translation_eq_block … Hptr_translation_lhs Hptr_translation_rhs H) normalize nodelta 1745 #Hsem_cmp whd in Hsem_cmp:(??%?); destruct (Hsem_cmp) 1746 whd in match (eval_unop ????); 1747 whd in match (opt_to_res ???); 1748 whd in match (m_bind ?????); 1749 (* TODO !!! In order to finish this, we need an invariant on the fact that we don't blow the stack during 1750 * transformation *) 1751 @cthulhu 1752  *: (* TBF. In the case of block inequality, we will have to use the no_aliasing property of the memory injection. *) 1753 @cthulhu 1754 ] 1755 ] 1712  *: >Hvalid_p1 >Hvalid_p2 normalize nodelta 1713 lapply Heq_block_outcome Heq_block_outcome 1714 @(eq_block_elim … (pblock p1) (pblock p2)) 1715 normalize nodelta 1716 [ 1,3,5,7,9,11: 1717 #Hbocks_eq #Heq_cmp destruct (Heq_cmp) 1718 whd in match (eval_unop ????); 1719 whd in match (m_bind ?????); 1720 cases (cmp_offset ???) normalize nodelta 1721 (* glitch *) 1722 @cthulhu 1723  *: 1724 #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 1725 whd in match (eval_unop ????); 1726 whd in match (m_bind ?????); 1727 @cthulhu 1728 ] 1729 ] 1756 1730 ] 1757 ]1758 1731 ] 1732 1759 1733  1: (* Integer constant *) 1760 1734 #csz #ty cases ty
Note: See TracChangeset
for help on using the changeset viewer.