Changeset 2185


Ignore:
Timestamp:
Jul 13, 2012, 7:59:43 PM (5 years ago)
Author:
campbell
Message:

Use bitvectors for offsets.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndMem.ma

    r1993 r2185  
    5050
    5151definition valid_pointer : mem → pointer → bool ≝
    52 λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
    53   Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
    54   Zleb (offv (poff ptr)) (high_bound m (pblock ptr)).
     52λm,ptr.
     53  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
     54  Zltb (block_id (pblock ptr)) (nextblock m) ∧
     55  Zleb (low_bound m (pblock ptr)) off ∧
     56  Zleb off (high_bound m (pblock ptr)).
    5557
  • src/common/GenMem.ma

    r2180 r2185  
    178178//; qed.
    179179
     180(* XXX note that this won't allow access to negative offsets, and we don't
     181   currently provide any other means to access them.  We could choose to get
     182   rid of them entirely. *)
    180183
    181184(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
     
    186189  if Zltb (block_id b) (nextblock … m) then
    187190   let content ≝ blocks … m b in
    188    let off ≝ offv (poff ptr) in
     191   let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
    189192   if andb (Zleb (low … content) off) (Zltb off (high … content)) then
    190193    Some … (F b content off)
  • src/common/Globalenvs.ma

    r2176 r2185  
    8282     addresses of the memory region in question - here there are no real
    8383     pointers, so use the real region. *)
    84   let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset p) in
     84  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in
    8585  match id with
    8686  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     
    236236| #f #fn #E normalize in E; destruct
    237237| (*#r*) #f #E normalize in E; destruct
    238 | * (*#pty*) #b (*#c*) * #off #f #E whd in E:(??%?);
    239   cases off in E ⊢ %; [ 2,3: #x ]
     238| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
     239  @eq_offset_elim #Eoff
    240240  #E whd in E:(??%?); destruct
    241241  (*%{pty}*) %{b} (*%{c}*) % // @E
  • src/common/Pointers.ma

    r2176 r2185  
    6868   the option of extending blocks backwards. *)
    6969
     70definition offset_size ≝ 8*size_pointer.
     71
    7072(* CSC: why do we need this awful indirection? *)
    71 record offset : Type[0] ≝ { offv : Z }.
     73record offset : Type[0] ≝ { offv : BitVector offset_size }.
    7274
    73 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
     75definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y).
    7476
    7577lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
     
    7779qed.
    7880
     81lemma eq_offset_elim : ∀P : bool → Prop.∀o1,o2.
     82  (o1 = o2 → P true) → (o1 ≠ o2 → P false) → P (eq_offset o1 o2).
     83#P * #o1 * #o2 #T #F
     84change with (eq_bv ???) in ⊢ (?%);
     85@eq_bv_elim
     86[ /2/
     87| * #FF @F % #E destruct /2/
     88] qed.
     89
     90definition offset_of_Z : Z → offset ≝
     91λz. mk_offset (bitvector_of_Z … z).
    7992definition shift_offset : ∀n. offset → BitVector n → offset ≝
    80   λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
     93  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
    8194(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
    8295definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    83   λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
     96  λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
    8497definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
    85   λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
     98  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
    8699definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    87   λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
     100  λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
    88101definition sub_offset : ∀n. offset → offset → BitVector n ≝
    89   λn,x,y. bitvector_of_Z ? (offv x - offv y).
    90 definition zero_offset ≝ mk_offset OZ.
     102  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
     103definition zero_offset ≝ mk_offset (zero ?).
    91104definition lt_offset : offset → offset → bool ≝
    92   λx,y. Zltb (offv x) (offv y).
     105  λx,y. lt_u ? (offv x) (offv y).
    93106
    94107(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
     
    132145whd in match (eq_pointer ??);
    133146@eq_block_elim #block_eq
    134 [ change with (eqZb ??) in match (eq_offset ??);
    135   @eqZb_elim #offset_eq
     147[ @eq_offset_elim #offset_eq
    136148  [ destruct @Ptrue %
    137149  ]
  • src/joint/BEMem.ma

    r2176 r2185  
    118118*)
    119119lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
    120 ** #a0 #a1 ***** #z #o 
     120** #a0 #a1 ***** #z #o
    121121#Hr
    122122(*
     
    127127destruct normalize
    128128@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
    129 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     129change with (eq_bv ???) in match (eq_v ?????);
     130@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
    130131#_ #_ normalize %
    131132qed.
  • src/joint/semantics.ma

    r2176 r2185  
    228228      let l' ≝ joint_if_entry … fn in
    229229      let st ≝ set_regs p regs st in
    230       let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) (mk_offset 0) in
     230      let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) zero_offset in
    231231      ! newpc ← address_of_label … ge pointer_in_fn l' ;
    232232      let st ≝ set_pc … newpc st in
     
    401401 (* Invariant: a -1 block is unused in common/Globalenvs *)
    402402 let b ≝ mk_block Code (-1) in
    403  let ptr ≝ mk_pointer b (mk_offset 0) in
     403 let ptr ≝ mk_pointer b zero_offset in
    404404 let addr ≝ address_of_code_pointer ptr in
    405405  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
     
    416416  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    417417  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    418   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset 0) in
    419   let spp ≝ mk_pointer spb (mk_offset external_ram_size) in
    420   let ispp ≝ mk_pointer ispb (mk_offset 47) in
     418  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) zero_offset in
     419  let spp ≝ mk_pointer spb (offset_of_Z external_ram_size) in
     420  let ispp ≝ mk_pointer ispb (offset_of_Z 47) in
    421421  do sp ← address_of_pointer spp ;
    422422  let main ≝ prog_main … p in
Note: See TracChangeset for help on using the changeset viewer.