Changeset 2608 for src/common/Pointers.ma

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:

• src/common/Pointers.ma (modified) (3 diffs)

src/common/Pointers.ma

@@ -1 +1 @@
 include "ASM/BitVectorZ.ma".
-include "common/AST.ma". (* For the regions *)
+include "common/AST.ma". (* For the /s/regions/size_pointer/ *)
 include "utilities/extralib.ma".
+include "basics/deqsets.ma".
 
 
@@ -20 +21 @@
 
 record block : Type[0] ≝
-{ block_region : region
-; block_id : Z
+{ (* block_region : region ; *)
+ block_id : Z
 }.
+
+definition block_region : block → region ≝
+  λb.
+  if Zltb (block_id b) OZ then
+    Code
+  else
+    XData.
 
 definition eq_block ≝
 λb1,b2.
-  eq_region (block_region b1) (block_region b2) ∧
+(*  eq_region (block_region b1) (block_region b2) ∧*)
   eqZb (block_id b1) (block_id b2)
 .
@@ -33 +41 @@
   (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
   P (eq_block b1 b2).
+#P * #i1 *#i2 #H1 #H2 whd in match (eq_block ??);
+@(eqZb_elim … i1 i2)
+[ #H @H1 >H @refl
+| * #Hneq @H2 % #H @Hneq destruct (H) @refl ]
+qed.
+(*
 #P * #r1 #i1 * #r2 #i2 #H1 #H2
 whd in ⊢ (?%); @eq_region_elim #H3
 [ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
 | @H2 % #E destruct elim H3 /2/
-] qed.
+] qed. *)
 
 lemma eq_block_b_b : ∀b. eq_block b b = true.
-* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
+* #z whd in ⊢ (??%?); >eqZb_z_z @refl
 qed.