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

Use bitvectors for offsets.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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  ]
Note: See TracChangeset for help on using the changeset viewer.