Changeset 2185 for src

Timestamp:

Jul 13, 2012, 7:59:43 PM (9 years ago)

Author:

campbell

Message:

Use bitvectors for offsets.

Location:

src

Files:

• common/FrontEndMem.ma (modified) (1 diff)
• common/GenMem.ma (modified) (2 diffs)
• common/Globalenvs.ma (modified) (2 diffs)
• common/Pointers.ma (modified) (3 diffs)
• joint/BEMem.ma (modified) (2 diffs)
• joint/semantics.ma (modified) (3 diffs)

src/common/FrontEndMem.ma

@@ -50 +50 @@
 
 definition valid_pointer : mem → pointer → bool ≝
-λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
-  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
-  Zleb (offv (poff ptr)) (high_bound m (pblock ptr)).
+λm,ptr.
+  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
+  Zltb (block_id (pblock ptr)) (nextblock m) ∧
+  Zleb (low_bound m (pblock ptr)) off ∧
+  Zleb off (high_bound m (pblock ptr)).
 

src/common/GenMem.ma

@@ -178 +178 @@
 //; qed.
 
+(* XXX note that this won't allow access to negative offsets, and we don't
+   currently provide any other means to access them.  We could choose to get
+   rid of them entirely. *)
 
 (* This function should be moved to common/GenMem.ma and replaces in_bounds *)
@@ -186 +189 @@
   if Zltb (block_id b) (nextblock … m) then
    let content ≝ blocks … m b in
-   let off ≝ offv (poff ptr) in
+   let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
    if andb (Zleb (low … content) off) (Zltb off (high … content)) then
     Some … (F b content off)

src/common/Globalenvs.ma

@@ -82 +82 @@
      addresses of the memory region in question - here there are no real
      pointers, so use the real region. *)
-  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset p) in
+  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in
   match id with
   [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
@@ -236 +236 @@
 | #f #fn #E normalize in E; destruct
 | (*#r*) #f #E normalize in E; destruct
-| * (*#pty*) #b (*#c*) * #off #f #E whd in E:(??%?);
-  cases off in E ⊢ %; [ 2,3: #x ]
+| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
+  @eq_offset_elim #Eoff
   #E whd in E:(??%?); destruct
   (*%{pty}*) %{b} (*%{c}*) % // @E

src/common/Pointers.ma

@@ -68 +68 @@
    the option of extending blocks backwards. *)
 
+definition offset_size ≝ 8*size_pointer.
+
 (* CSC: why do we need this awful indirection? *)
-record offset : Type[0] ≝ { offv : Z }.
+record offset : Type[0] ≝ { offv : BitVector offset_size }.
 
-definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
+definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y).
 
 lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
@@ -77 +79 @@
 qed.
 
+lemma eq_offset_elim : ∀P : bool → Prop.∀o1,o2.
+  (o1 = o2 → P true) → (o1 ≠ o2 → P false) → P (eq_offset o1 o2).
+#P * #o1 * #o2 #T #F
+change with (eq_bv ???) in ⊢ (?%);
+@eq_bv_elim
+[ /2/
+| * #FF @F % #E destruct /2/
+] qed.
+
+definition offset_of_Z : Z → offset ≝
+λz. mk_offset (bitvector_of_Z … z).
 definition shift_offset : ∀n. offset → BitVector n → offset ≝
-  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
+  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
-  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
+  λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
-  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
+  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
-  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
+  λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
 definition sub_offset : ∀n. offset → offset → BitVector n ≝
-  λn,x,y. bitvector_of_Z ? (offv x - offv y).
-definition zero_offset ≝ mk_offset OZ.
+  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
+definition zero_offset ≝ mk_offset (zero ?).
 definition lt_offset : offset → offset → bool ≝
-  λx,y. Zltb (offv x) (offv y).
+  λx,y. lt_u ? (offv x) (offv y).
 
 (*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
@@ -132 +145 @@
 whd in match (eq_pointer ??);
 @eq_block_elim #block_eq
-[ change with (eqZb ??) in match (eq_offset ??);
-  @eqZb_elim #offset_eq
+[ @eq_offset_elim #offset_eq
   [ destruct @Ptrue %
   ]

src/joint/BEMem.ma

@@ -118 +118 @@
 *)
 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
-** #a0 #a1 ***** #z #o 
+** #a0 #a1 ***** #z #o
 #Hr
 (*
@@ -127 +127 @@
 destruct normalize
 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
-@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
+change with (eq_bv ???) in match (eq_v ?????);
+@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
 #_ #_ normalize %
 qed.

src/joint/semantics.ma

@@ -228 +228 @@
       let l' ≝ joint_if_entry … fn in
       let st ≝ set_regs p regs st in
-      let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) (mk_offset 0) in
+      let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) zero_offset in
       ! newpc ← address_of_label … ge pointer_in_fn l' ;
       let st ≝ set_pc … newpc st in
@@ -401 +401 @@
  (* Invariant: a -1 block is unused in common/Globalenvs *)
  let b ≝ mk_block Code (-1) in
- let ptr ≝ mk_pointer b (mk_offset 0) in
+ let ptr ≝ mk_pointer b zero_offset in
  let addr ≝ address_of_code_pointer ptr in
   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
@@ -416 +416 @@
   let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
   let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
-  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset 0) in
-  let spp ≝ mk_pointer spb (mk_offset external_ram_size) in
-  let ispp ≝ mk_pointer ispb (mk_offset 47) in
+  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) zero_offset in
+  let spp ≝ mk_pointer spb (offset_of_Z external_ram_size) in
+  let ispp ≝ mk_pointer ispb (offset_of_Z 47) in
   do sp ← address_of_pointer spp ;
   let main ≝ prog_main … p in