Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (8 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/switchRemoval.ma

    r2588 r2608  
    11881188  beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res.
    11891189* #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable
    1190 * #br #bid * * #pr #pid #poff #res #Hext
     1190* (* #br *) #bid * * (* #pr *) #pid #poff #res #Hext
    11911191(*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*)
    11921192#Hload
     
    12231223     [ 1: lapply Hvalid normalize //
    12241224     | 2: lapply Hlh normalize
    1225           cases (block_region b) normalize nodelta
    1226           cases (block_region bl) normalize nodelta try //
    12271225          @(eqZb_elim … (block_id b) (block_id bl))
    12281226          [ 1,3: * normalize *
     
    12321230lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b.
    12331231#a #b lapply (eqb_true ? a b) @(eq_block_elim … a b)
    1234 /2 by neq_block_eq_block_false, true_to_andb_true/
     1232#H #I
     1233try /2 by neq_block_eq_block_false, true_to_andb_true/
     1234cases I #J #K @K @H
    12351235qed.
    12361236
     
    13621362     #b normalize >Hcontents_eq @refl
    13631363| 5: #x1 #x2 #acc normalize @conj try @refl
    1364      * * #id normalize nodelta cases (block_region x1)
     1364     * (* * *) #id normalize nodelta cases (block_region x1)
    13651365     cases (block_region x2) normalize nodelta
    13661366     @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta
    13671367     @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl
    1368 | 6: * #r #i * #contents #nextblock #Hpos @conj
     1368| 6: * (* #r *) #i * #contents #nextblock #Hpos @conj
    13691369     [ 1: @refl
    1370      | 2: #b normalize cases (block_region b) normalize
    1371           cases r normalize cases (eqZb (block_id b) i)
     1370     | 2: #b normalize (* cases (block_region b) normalize
     1371          cases r normalize *) cases (eqZb (block_id b) i)
    13721372          normalize @refl
    13731373     ]
     
    16501650     [ 1: normalize cases H //
    16511651     | 2: cases H normalize #Hb_lt #Hb_nonempty2
    1652           cases (block_region b)
    1653           cases (block_region wb) normalize nodelta
    1654           //
     1652          (*
     1653            cases (block_region b)
     1654            cases (block_region wb) *)
    16551655          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta
    16561656          // ]
     
    17051705            (nextblock m) (nextblock_pos m)) b.
    17061706#m #b #wb #offset #v * #Hvalid #Hnonempty % //
    1707 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
    1708 cases br normalize nodelta cases wbr normalize nodelta //
     1707cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize
     1708(* cases br *) normalize nodelta (* cases wbr normalize nodelta // *)
    17091709@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
    17101710qed.
     
    17201720  nonempty_block m b.
    17211721#m #b #wb #offset #v * #Hvalid #Hnonempty % //
    1722 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize
    1723 cases br normalize nodelta cases wbr normalize nodelta //
     1722cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize
     1723(* cases br normalize nodelta cases wbr normalize nodelta // *)
    17241724@(eqZb_elim … bid wbid) // #Heq #Hlt normalize //
    17251725qed.
     
    17641764     @conj
    17651765     [ 1: @nonempty_block_update_ok //
    1766      | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid
    1767           cases br cases wbr normalize nodelta
    1768           @(eqZb_elim … bid wbid) normalize nodelta //
    1769           #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ]
     1766     | 2: normalize (* cases b in HB; #br #bid cases wb #wbr #wbid
     1767          cases br cases wbr normalize nodelta *)
     1768          @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta //
     1769          #Hid_eq cut (b = wb)
     1770          [ cases b in Hid_eq; cases wb #wid #bid #H >H @refl ]
     1771          #Hblock_eq destruct (Hblock_eq) >HB @refl ]
    17701772| 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok
    17711773| 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty)
Note: See TracChangeset for help on using the changeset viewer.