Changeset 744 for src/ASM/Arithmetic.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r724 r744  
    149149  λb, c: BitVector n.
    150150    addition_n n b (two_complement_negation n c).
    151    
    152 definition multiplication ≝
    153   λn: nat.
    154   λb, c: BitVector n.
    155     let b_nat ≝ nat_of_bitvector ? b in
    156     let c_nat ≝ nat_of_bitvector ? c in
    157     let result ≝ b_nat * c_nat in
    158       bitvector_of_nat (n + n) result.
    159      
    160 definition division_u ≝
    161   λn: nat.
    162   λb, c: BitVector n.
    163     let b_nat ≝ nat_of_bitvector ? b in
    164     let c_nat ≝ nat_of_bitvector ? c in
    165     match c_nat with
    166     [ O ⇒ None ?
    167     | _ ⇒
    168       let result ≝ b_nat ÷ c_nat in
    169         Some ? (bitvector_of_nat n result)
     151
     152let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
     153match b with
     154[ VEmpty ⇒ acc
     155| VCons m' hd tl ⇒
     156    let acc' ≝ if hd then addition_n ? c acc else acc in
     157    mult_aux m' n tl (shift_right_1 ?? c false) acc'
     158].
     159
     160definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
     161  λn: nat.
     162  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
     163  [ O ⇒ λ_.λ_.[[ ]]
     164  | S m ⇒
     165    λb, c : BitVector (S m).
     166    let c' ≝ pad (S m) (S m) c in
     167      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
     168  ].
     169
     170(* Division:  001...000 divided by 000...010
     171     Shift the divisor as far left as possible,
     172                                  100...000
     173      then try subtracting it at each
     174      bit position, shifting left as we go.
     175              001...000 - 100...000 X ⇒ 0
     176              001...000 - 010...000 X ⇒ 0
     177              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
     178              ...
     179      Then pad out the remaining bits at the front
     180         00..001...
     181*)
     182inductive fbs_diff : nat → Type[0] ≝
     183| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
     184
     185let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
     186match b return λn.λ_. option (fbs_diff n) with
     187[ VEmpty ⇒ None ?
     188| VCons m h t ⇒
     189    if h then Some ? (fbs_diff' O m)
     190    else match first_bit_set m t with
     191         [ None ⇒ None ?
     192         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
     193         ]
     194].
     195
     196let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
     197match m with
     198[ O ⇒ 〈[[ ]], q〉
     199| S m' ⇒
     200    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
     201    let bit ≝ head' … flags in
     202    let q'' ≝ if bit then q' else q in
     203    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
     204    〈bit:::tl, md〉
     205].
     206
     207definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
     208  λn: nat.
     209  λb, c: BitVector (S n).
     210
     211    match first_bit_set ? c with
     212    [ None ⇒ None ?
     213    | Some fbs' ⇒
     214        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
     215          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
     216          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
     217        ]
    170218    ].
     219
     220definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
     221λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
    171222     
    172223definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
     
    177228        let b_sign_bit ≝ get_index_v ? ? b O ? in
    178229        let c_sign_bit ≝ get_index_v ? ? c O ? in
    179         let b_as_nat ≝ nat_of_bitvector ? b in
    180         let c_as_nat ≝ nat_of_bitvector ? c in
    181         match c_as_nat with
    182         [ O ⇒ None ?
    183         | S o ⇒
    184           match b_sign_bit with
     230        match b_sign_bit with
     231        [ true ⇒
     232          let neg_b ≝ two_complement_negation ? b in
     233          match c_sign_bit with
    185234          [ true ⇒
    186             let temp_b ≝ b_as_nat - (2^p) in
    187             match c_sign_bit with
    188             [ true ⇒
    189               let temp_c ≝ c_as_nat - (2^p) in
    190                 Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
    191             | false ⇒
    192               let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
    193                 Some ? (bitvector_of_nat ? result)
    194             ]
     235              (* I was worrying slightly about -2^(n-1), whose negation can't
     236                 be represented in an n bit signed number.  However, it's
     237                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
     238                 so it's fine. *)
     239              division_u ? neg_b (two_complement_negation ? c)
    195240          | false ⇒
    196             match c_sign_bit with
    197             [ true ⇒
    198               let temp_c ≝ c_as_nat - (2^p) in
    199               let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
    200                 Some ? (bitvector_of_nat ? result)
    201             | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
    202             ]
     241              match division_u ? neg_b c with
     242              [ None ⇒ None ?
     243              | Some r ⇒ Some ? (two_complement_negation ? r)
     244              ]
     245          ]
     246        | false ⇒
     247          match c_sign_bit with
     248          [ true ⇒
     249              match division_u ? b (two_complement_negation ? c) with
     250              [ None ⇒ None ?
     251              | Some r ⇒ Some ? (two_complement_negation ? r)
     252              ]
     253          | false ⇒ division_u ? b c
    203254          ]
    204255        ]
    205     ].
     256   ].
    206257    //
    207258qed.
    208259
    209 definition modulus_u ≝
    210   λn.
    211   λb, c: BitVector n.
    212     let b_nat ≝ nat_of_bitvector ? b in
    213     let c_nat ≝ nat_of_bitvector ? c in
    214     match c_nat with
    215     [ O ⇒ None ?
    216     | _ ⇒
    217       let result ≝ modulus b_nat c_nat in
    218       Some ? (bitvector_of_nat n result)
    219     ].
     260definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
     261λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
    220262           
    221263definition modulus_s ≝
Note: See TracChangeset for help on using the changeset viewer.