Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (7 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/MemProperties.ma

    r2483 r2608  
    227227
    228228lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
    229 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
     229* #contents #next #nextpos * (*#br1*) #bid1 * (*#br2*) #bid2 normalize
    230230@(eqZb_elim … bid1 bid2)
    231 [ 1: #Heq >Heq cases br1 cases br2 normalize
     231[ 1: #Heq >Heq normalize #H
     232     @False_ind @(absurd … (refl ??) H)
     233(*     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
     234     #_ @refl *)
     235| 2: #Hneq #Hneq' @refl ]
     236qed.
     237
     238lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
     239* #contents #next #nextpos * (* #br1 *) #bid1 * (* #br2 *) #bid2 normalize
     240@(eqZb_elim … bid1 bid2)
     241[ 1: #Heq >Heq (* cases br1 cases br2 *) normalize #H
     242     @False_ind @(absurd … (refl ??) H)
     243(*
    232244     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
    233      #_ @refl
    234 | 2: cases br1 cases br2 normalize #_ #_ @refl ]
    235 qed.
    236 
    237 lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
    238 * #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
    239 @(eqZb_elim … bid1 bid2)
    240 [ 1: #Heq >Heq cases br1 cases br2 normalize
    241      [ 1,4: * #H @(False_ind … (H (refl ??))) ]
    242      #_ @refl
    243 | 2: cases br1 cases br2 normalize #_ #_ @refl ]
     245     #_ @refl *)
     246| 2: (* cases br1 cases br2 *) normalize #_ #_ @refl ]
    244247qed.
    245248
    246249lemma beloadv_free_blocks_neq :
    247250  ∀m,block,pblock,poff,res.
    248   beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
    249 * #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
     251  beloadv (free m block) (mk_pointer pblock poff) = Some ? res →
     252  pblock ≠ block.
     253* #contents #next #nextpos * (* #br *) #bid * (* #pbr *) #pbid #poff #res
    250254normalize
    251255cases (Zltb pbid next) normalize nodelta
    252256[ 2: #Habsurd destruct (Habsurd) ]
    253 cases pbr cases br normalize nodelta
    254 [ 2,3: #_ % #Habsurd destruct (Habsurd) ]
     257(*cases pbr cases br normalize nodelta *)
    255258@(eqZb_elim pbid bid) normalize nodelta
    256259#Heq destruct (Heq)
    257 [ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
     260[ 1: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
    258261#_ % #H destruct (H) elim Heq #H @H @refl
    259262qed.
     
    517520destruct try @refl
    518521[ 1:
    519   #b' normalize cases b #br #bid cases b' #br' #bid'
    520   cases br' cases br normalize @(eqZb_elim … bid' bid) #H normalize
     522  #b' normalize cases b (* #br *) #bid cases b' (* #br' *) #bid'
     523  (* cases br' cases br *) normalize @(eqZb_elim … bid' bid) #H normalize
    521524  try /2 by conj, refl/
    522525| 2: @Zleb_true_to_Zle cases ofs in Hle; #o #H @H
    523526| 3: @Zltb_true_to_Zlt cases ofs in Hlt; #o #H @H
    524 | 4: normalize cases b #br #bid cases br normalize >eqZb_z_z normalize
     527| 4: normalize cases b (* #br *) #bid (* cases br *) normalize >eqZb_z_z normalize
    525528     >eqZb_z_z @refl
    526 | 5: #o #Hneq normalize in ⊢ (??%%); cases b * #bid normalize nodelta
     529| 5: #o #Hneq normalize in ⊢ (??%%); cases b #bid normalize nodelta
    527530     >eqZb_z_z normalize nodelta
    528531     @(eqZb_elim … (Z_of_unsigned_bitvector 16 (offv o)) (Z_of_unsigned_bitvector 16 (offv ofs)))
     
    10271030lemma fe_to_be_to_fe_value_ptr :
    10281031  ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)).
    1029 #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta
    1030 cases br normalize nodelta >eqZb_z_z normalize nodelta
     1032#b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid
     1033(* cases br normalize nodelta *) >eqZb_z_z normalize nodelta
    10311034cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq
    10321035<(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl
Note: See TracChangeset for help on using the changeset viewer.