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/common/Pointers.ma

    r2569 r2608  
    11include "ASM/BitVectorZ.ma".
    2 include "common/AST.ma". (* For the regions *)
     2include "common/AST.ma". (* For the /s/regions/size_pointer/ *)
    33include "utilities/extralib.ma".
     4include "basics/deqsets.ma".
    45
    56
     
    2021
    2122record block : Type[0] ≝
    22 { block_region : region
    23 ; block_id : Z
     23{ (* block_region : region ; *)
     24 block_id : Z
    2425}.
     26
     27definition block_region : block → region ≝
     28  λb.
     29  if Zltb (block_id b) OZ then
     30    Code
     31  else
     32    XData.
    2533
    2634definition eq_block ≝
    2735λb1,b2.
    28   eq_region (block_region b1) (block_region b2) ∧
     36(*  eq_region (block_region b1) (block_region b2) ∧*)
    2937  eqZb (block_id b1) (block_id b2)
    3038.
     
    3341  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
    3442  P (eq_block b1 b2).
     43#P * #i1 *#i2 #H1 #H2 whd in match (eq_block ??);
     44@(eqZb_elim … i1 i2)
     45[ #H @H1 >H @refl
     46| * #Hneq @H2 % #H @Hneq destruct (H) @refl ]
     47qed.
     48(*
    3549#P * #r1 #i1 * #r2 #i2 #H1 #H2
    3650whd in ⊢ (?%); @eq_region_elim #H3
    3751[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    3852| @H2 % #E destruct elim H3 /2/
    39 ] qed.
     53] qed. *)
    4054
    4155lemma eq_block_b_b : ∀b. eq_block b b = true.
    42 * * #z whd in ⊢ (??%?); >eqZb_z_z @refl
     56* #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4357qed.
    4458
Note: See TracChangeset for help on using the changeset viewer.