Changeset 744 for src/common


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

Location:
src/common
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r727 r744  
    171171  ].
    172172 
    173 (* FIXME: switch to alias, or rename, or … *)
    174 definition int_eq : int → int → bool ≝ eq.
    175173definition ev_notbool : val → option val ≝ λv.
    176174  match v with
     
    181179  ].
    182180
    183 definition ev_zero_ext ≝ λnbits: Z. λv: val.
     181definition ev_zero_ext ≝ λnbits: nat. λv: val.
    184182  match v with
    185183  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
     
    187185  ].
    188186
    189 definition ev_sign_ext ≝ λnbits:Z. λv:val.
     187definition ev_sign_ext ≝ λnbits:nat. λv:val.
    190188  match v with
    191189  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
     
    203201  match v1 with
    204202  [ Vint n1 ⇒ match v2 with
    205     [ Vint n2 ⇒ Some ? (Vint (add n1 n2))
     203    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
    206204    | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1))
    207205    | _ ⇒ None ? ]
     
    214212  match v1 with
    215213  [ Vint n1 ⇒ match v2 with
    216     [ Vint n2 ⇒ Some ? (Vint (sub n1 n2))
     214    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
    217215    | _ ⇒ None ? ]
    218216  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    234232  match v1 with
    235233  [ Vint n1 ⇒ match v2 with
    236     [ Vint n2 ⇒ Some ? (Vint (divs n1 n2))
     234    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
    237235    | _ ⇒ None ? ]
    238236  | _ ⇒ None ? ].
     
    241239  match v1 with
    242240  [ Vint n1 ⇒ match v2 with
    243     [ Vint n2 ⇒
    244        if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     241    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
    245242    | _ ⇒ None ?
    246243    ]
     
    251248  match v1 with
    252249  [ Vint n1 ⇒ match v2 with
    253     [ Vint n2 ⇒
    254         if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     250    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
    255251    | _ ⇒ None ?
    256252    ]
     
    261257  match v1 with
    262258  [ Vint n1 ⇒ match v2 with
    263     [ Vint n2 ⇒
    264       if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     259    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
    265260    | _ ⇒ None ?
    266261    ]
  • src/common/Globalenvs.ma

    r700 r744  
    424424  ].
    425425
    426 definition size_init_data : init_data → Z
     426definition size_init_data : init_data → nat
    427427 λi_data.match i_data with
    428428  [ Init_int8 _ ⇒ 1
     
    431431  | Init_float32 _ ⇒ 4
    432432  | Init_float64 _ ⇒ 8
    433   | Init_space n ⇒ Zmax n 0
     433  | Init_space n ⇒ max n 0
    434434  | Init_null r ⇒ size_pointer r
    435435  | Init_addrof r _ _ ⇒ size_pointer r].
  • src/common/Integers.ma

    r700 r744  
    1717
    1818include "arithmetics/nat.ma".
    19 include "utilities/binary/Z.ma".
    20 include "utilities/extralib.ma".
     19include "utilities/extranat.ma".
    2120
    2221include "ASM/BitVector.ma".
    23 include "ASM/BitVectorZ.ma".
    2422include "ASM/Arithmetic.ma".
    2523
     
    6866
    6967definition wordsize : nat ≝ 32.
     68(*
    7069definition modulus : Z ≝ Z_two_power_nat wordsize.
    7170definition half_modulus : Z ≝ modulus / 2.
     
    8584  modulus > 0.
    8685//; qed.
    87 
     86*)
    8887(* * Representation of machine integers *)
    8988
     
    9392
    9493definition int : Type[0] ≝ BitVector wordsize.
    95 
     94(*
    9695definition intval: int → Z ≝ Z_of_unsigned_bitvector ?.
    9796definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
     
    111110  then unsigned n
    112111  else unsigned n - modulus.
    113 
     112*)
    114113(* Conversely, [repr] takes a Coq integer and returns the corresponding
    115114  machine integer.  The argument is treated modulo [modulus]. *)
    116 
     115(*
    117116definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z.
     117*)
     118definition repr : nat → int ≝ λn. bitvector_of_nat wordsize n.
    118119
    119120definition zero := repr 0.
    120121definition one  := repr 1.
    121 definition mone := repr (-1).
    122 definition iwordsize := repr (Z_of_nat wordsize).
     122definition mone := subtraction ? zero one.
     123definition iwordsize := repr wordsize.
    123124
    124125lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
     
    135136
    136137definition neg : int → int ≝ two_complement_negation wordsize.
    137 
    138 let rec zero_ext (n:Z) (x:int) on x : int ≝
    139   repr (modZ (unsigned x) (two_p n)).
    140 let rec sign_ext (n:Z) (x:int) on x : int ≝
    141   repr (let p ≝ two_p n in
    142         let y ≝ modZ (unsigned x) p in
    143         if Zltb y (two_p (n-1)) then y else y - p).
    144 
    145 definition add ≝ addition_n wordsize.
    146 definition sub ≝ subtraction wordsize.
    147 (*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*)
    148 definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)).
    149 definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    150   if Zltb x 0 then
    151     if Zltb y 0 then (-x) / (-y) else - ((-x) / y)
    152   else
    153     if Zltb y 0 then -(x / (-y)) else x / y.
    154 
    155 definition Zmod_round : Z → Z → Z ≝ λx,y: Z.
    156   x - (Zdiv_round x y) * y.
    157 
    158 definition divs : int → int → int ≝ λx,y:int.
    159   repr (Zdiv_round (signed x) (signed y)).
    160 definition mods : int → int → int ≝ λx,y:int.
    161   repr (Zmod_round (signed x) (signed y)).
    162 definition divu : int → int → int ≝ λx,y.
    163   repr (unsigned x / unsigned y).
    164 definition modu : int → int → int ≝ λx,y.
    165   repr (unsigned x \mod unsigned y).
    166 
    167 (* * For bitwise operations, we need to convert between Coq integers [Z]
    168   and their bit-level representations.  Bit-level representations are
    169   represented as characteristic functions, that is, functions [f]
    170   of type [nat -> bool] such that [f i] is the value of the [i]-th bit
    171   of the number.  The values of characteristic functions for [i] greater
    172   than 32 are ignored. *)
    173 
    174 definition Z_shift_add ≝ λb: bool. λx: Z.
    175   if b then 2 * x + 1 else 2 * x.
    176 
    177 definition Z_bin_decomp : Z → bool × Z ≝
    178 λx.match x with
    179 [ OZ ⇒ 〈false, OZ〉
    180 | pos p ⇒
    181   match p with
    182   [ p1 q ⇒ 〈true, pos q〉
    183   | p0 q ⇒ 〈false, pos q〉
    184   | one ⇒ 〈true, OZ〉
    185   ]
    186 | neg p ⇒
    187   match p return λ_.bool × Z with
    188   [ p1 q ⇒ 〈true, Zpred (neg q)〉
    189   | p0 q ⇒ 〈false, neg q〉
    190   | one ⇒ 〈true, neg one〉
    191   ]
    192 ].
    193 
    194 let rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝
    195 match n with
    196 [ O ⇒ λi:Z. false
    197 | S m ⇒
    198     match Z_bin_decomp x with [ pair b y ⇒
    199       let f ≝ bits_of_Z m y in
    200       λi:Z. if eqZb i 0 then b else f (Zpred i) ]
    201 ].
    202 
    203 let rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝
    204 match n with
    205 [ O ⇒ OZ
    206 | S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i)))
    207 ].
     138definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)).
     139
     140definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     141λw,n.
     142  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
     143  [ nat_lt n' w' ⇒ λi.
     144      let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     145      switch_bv_plus ??? (pad ?? l)
     146  | _ ⇒ λi.i
     147  ].
     148
     149definition zero_ext : nat → int → int ≝ zero_ext_n wordsize.
     150
     151definition sign_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     152λw,n.
     153  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
     154  [ nat_lt n' w' ⇒ λi.
     155      let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     156      switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]) ?? l)
     157  | _ ⇒ λi.i
     158  ].
     159
     160definition sign_ext : nat → int → int ≝ sign_ext_n wordsize.
    208161
    209162(* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
    210163
    211 definition bitwise_binop ≝ λf: bool -> bool -> bool. λx,y: int.
    212   let fx ≝ bits_of_Z wordsize (unsigned x) in
    213   let fy ≝ bits_of_Z wordsize (unsigned y) in
    214   repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).
    215164
    216165definition i_and : int → int → int ≝ conjunction_bv wordsize.
     
    222171(* * Shifts and rotates. *)
    223172
    224 definition shl : int → int → int ≝ λx,y.
    225   let fx ≝ bits_of_Z wordsize (unsigned x) in
    226   let vy ≝ unsigned y in
    227   repr (Z_of_bits wordsize (λi. fx (i - vy))).
    228 
    229 definition shru : int → int → int ≝ λx,y.
    230   let fx ≝ bits_of_Z wordsize (unsigned x) in
    231   let vy ≝ unsigned y in
    232   repr (Z_of_bits wordsize (λi. fx (i + vy))).
     173definition shl : int → int → int ≝ λx,y. shift_left ?? (nat_of_bitvector … y) x false.
     174definition shru : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x false.
    233175
    234176(* * Arithmetic right shift is defined as signed division by a power of two.
     
    237179  [shrx] rounds towards zero. *)
    238180
    239 definition shr : int → int → int ≝ λx,y.
    240   repr (signed x / two_p (unsigned y)).
    241 
     181definition shr : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x (head' … x).
    242182definition shrx : int → int → int ≝ λx,y.
    243   divs x (shl one y).
     183  match division_s ? x (shl one y) with [ None ⇒ zero | Some i ⇒ i ].
    244184
    245185definition shr_carry ≝ λx,y: int.
    246   sub (shrx x y) (shr x y).
    247 
    248 definition rol : int → int → int ≝ λx,y.
    249   let fx ≝ bits_of_Z wordsize (unsigned x) in
    250   let vy ≝ unsigned y in
    251   repr (Z_of_bits wordsize
    252          (λi. fx (i - vy \mod Z_of_nat wordsize))).
    253 
    254 definition ror : int → int → int ≝ λx,y.
    255   let fx := bits_of_Z wordsize (unsigned x) in
    256   let vy := unsigned y in
    257   repr (Z_of_bits wordsize
    258          (λi. fx (i + vy \mod Z_of_nat wordsize))).
     186  subtraction ? (shrx x y) (shr x y).
     187
     188definition rol : int → int → int ≝ λx,y. rotate_left ?? (nat_of_bitvector ? y) x.
     189definition ror : int → int → int ≝ λx,y. rotate_right ?? (nat_of_bitvector ? y) x.
    259190
    260191definition rolm ≝ λx,a,m: int. i_and (rol x a) m.
     
    487418*)
    488419theorem one_not_zero: one ≠ zero.
    489 % #H
    490 lapply (refl ? (get_index' ? 31 0 one))
    491 >H in ⊢ (???% → ?)
    492 normalize #E destruct
     420% #H @(match eq_dec one zero return λx.match x with [ inl _ ⇒ True | inr _ ⇒ False ] with [ inl _ ⇒ I | inr p ⇒ ?]) normalize
     421cases p #H' @(H' H)
    493422qed.
    494423
     
    705634Qed.
    706635*)
    707 
     636(*
    708637theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus.
    709638#i @intrange
     
    27102639
    27112640
     2641*)
  • src/common/Mem.ma

    r718 r744  
    623623    ]
    624624]
    625 %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval | 3: @Hnext ]
     625%2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl'
     626[ @(absurd ? Hcl' Hcl) | @(absurd ? Hal' Hal) | @(absurd ? Hhi' Hhi)
     627| @(absurd ? Hlo' Hlo) | @(absurd ? Hval Hnext) ]
    626628qed.
    627629
  • src/common/Values.ma

    r718 r744  
    2323include "common/Errors.ma".
    2424
    25 include "ASM/Vector.ma".
     25include "ASM/BitVectorZ.ma".
    2626
    2727include "basics/logic.ma".
     28
     29include "utilities/binary/Z.ma".
    2830
    2931(* To define pointers we need a few details about the memory model.
     
    8890definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    8991definition shift_offset : offset → int → offset ≝
    90   λo,i. mk_offset (offv o + signed i).
     92  λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    9193definition neg_shift_offset : offset → int → offset ≝
    92   λo,i. mk_offset (offv o - signed i).
     94  λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    9395definition sub_offset : offset → offset → int ≝
    94   λx,y. repr (offv x - offv y).
     96  λx,y. bitvector_of_Z ? (offv x - offv y).
    9597definition zero_offset ≝ mk_offset OZ.
    9698definition lt_offset : offset → offset → bool ≝
     
    321323  ].
    322324
    323 definition zero_ext ≝ λnbits: Z. λv: val.
     325definition zero_ext ≝ λnbits: nat. λv: val.
    324326  match v with
    325327  [ Vint n ⇒ Vint (zero_ext nbits n)
     
    327329  ].
    328330
    329 definition sign_ext ≝ λnbits:Z. λv:val.
     331definition sign_ext ≝ λnbits:nat. λv:val.
    330332  match v with
    331333  [ Vint i ⇒ Vint (sign_ext nbits i)
     
    343345  match v1 with
    344346  [ Vint n1 ⇒ match v2 with
    345     [ Vint n2 ⇒ Vint (add n1 n2)
     347    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    346348    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
    347349    | _ ⇒ Vundef ]
     
    354356  match v1 with
    355357  [ Vint n1 ⇒ match v2 with
    356     [ Vint n2 ⇒ Vint (sub n1 n2)
     358    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
    357359    | _ ⇒ Vundef ]
    358360  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    12051207qed.
    12061208
    1207 (*
    1208 Lemma zero_ext_lessdef:
    1209   forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).
    1210 Proof.
    1211   intros; inv H; simpl; auto.
    1212 Qed.
    1213 *)
     1209lemma zero_ext_lessdef:
     1210  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
     1211#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
     1212qed.
     1213
    12141214lemma sign_ext_lessdef:
    12151215  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
Note: See TracChangeset for help on using the changeset viewer.