Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module provides a convenient lens from a larger bitvector into a smaller one:
>>>
v = bvView @4 @'[3, 0, 1]
v
is the "view" into a BV 4
that you get by extracting the bits at
indices 3
, 0
, and 1
(in order of most-significant to least-significant
bit). If
bv = 0bABCD
then the view v
defined above refers to the bits 0bADC
, a bitvector of
width 3. We can see this by creating a concrete bitvector, and using the view
to get and set bits:
>>>
bv = BV.mkBV (knownNat @4) 0b1100
>>>
printBV = putStrLn . BV.ppBin knownNat
>>>
printBV $ bv ^. bvViewL v
0b100:[3]>>>
printBV $ bv & bvViewL v .~ BV.mkBV knownNat 0b101
0b1110:[4]
This is very useful for defining sub-fields of an instruction word. Consider the encoding for the RISC-V instruction JAL:
[ imm[20] | imm[10:1] | imm[11] | imm[19:12] | rd[4:0] | opcode=1101111 ] 31 21 20 12 7 0
Notice how the 7-bit opcode
and 5-bit rd
are laid out consecutively in
the 32-bit instruction word, but the imm
field has its bits jumbled up
throughout the rest of the instruction. We can create a view of the three
fields like so:
>>>
opcode = bvView @32 @(Slice 0 7)
>>>
rd = bvView :: BVView 32 (Slice 7 5)
>>>
imm = bvView :: BVView 32 ('[31] ++ Slice 12 8 ++ '[20] ++ Slice 21 10)
The Slice
and ++
operators are useful for shortening the above
definitions. Expanded out, the types of the above definitions are:
>>>
:t opcode
opcode :: BVView 32 '[6, 5, 4, 3, 2, 1, 0]>>>
:t rd
rd :: BVView 32 '[11, 10, 9, 8, 7]>>>
:t imm
imm :: BVView 32 '[31, 19, 18, 17, 16, 15, 14, 13, 12, 20, 30, 29, 28, 27, 26, 25, 24, 23, 22, 21]
The type system prevents you from creating an invalid view (for instance, where a bit index is repeated or out of range):
>>>
v = bvView @32 @('[5] ++ Slice 3 4)
<interactive>:37:5: error: • Invalid index list: '[5, 6, 5, 4, 3] (repeated index 5) • In the expression: bvView @32 @('[5] ++ Slice 3 4) In an equation for ‘v’: v = bvView @32 @('[5] ++ Slice 3 4)>>>
v = bvView @32 @(Slice 30 4)
<interactive>:1:5: error: • Invalid index 33 into BV 32 index must be strictly smaller than bitvector width • In the expression: bvView @32 @(Slice 30 4) In an equation for ‘v’: v = bvView @32 @(Slice 30 4) <interactive>:1:5: error: • Invalid index 32 into BV 32 index must be strictly smaller than bitvector width • In the expression: bvView @32 @(Slice 30 4) In an equation for ‘v’: v = bvView @32 @(Slice 30 4)
WARNING: Don't attempt to use this library unless all your type-level
indices are known at compile time. If you try abstracting over BVView
,
you're gonna have a bad time.
Synopsis
- data BVIx w ix
- bvIx :: forall w ix. (KnownNat ix, ValidIx w ix) => BVIx w ix
- bvIxL :: KnownNat w => BVIx w ix -> Lens' (BV w) (BV 1)
- data BVView (w :: Nat) (ixs :: [Nat])
- bvView :: forall w ixs. (KnownRepr (BVView w) ixs, ValidView ixs) => BVView w ixs
- bvViewL :: forall w ixs. KnownNat w => BVView w ixs -> Lens' (BV w) (BV (Length ixs))
- data BVViews (w :: Nat) (ixss :: [[Nat]])
- bvViews :: forall w ixss. (KnownRepr (BVViews w) ixss, ValidViews ixss) => BVViews w ixss
- bvViewsL :: forall w ixss. KnownNat w => BVViews w ixss -> Lens' (BV w) (List BV (Lengths ixss))
- type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
- type family Slice (i :: Nat) (w :: Nat) :: [Nat] where ...
- type family Slice' (i :: Nat) (w :: Nat) :: [Nat] where ...
- type family Length (l :: [k]) :: Nat where ...
- type family Lengths (kss :: [[k]]) :: [Nat] where ...
BVIx
Index of a single bit of a BV
.
Instances
TestEquality (BVIx w :: Nat -> Type) Source # | |
Defined in Data.BitVector.Sized.Lens | |
OrdF (BVIx w :: Nat -> Type) Source # | |
Defined in Data.BitVector.Sized.Lens compareF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # ltF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # geqF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # gtF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # | |
ShowF (BVIx w :: Nat -> Type) Source # | |
(KnownNat ix, ValidIx w ix) => KnownRepr (BVIx w :: Nat -> Type) (ix :: Nat) Source # | |
Defined in Data.BitVector.Sized.Lens | |
Show (BVIx w ix) Source # | |
bvIx :: forall w ix. (KnownNat ix, ValidIx w ix) => BVIx w ix Source #
Construct a BVIx
when the index is known at compile time.
>>>
bvIx @32 @7
BVIx 7>>>
:type it
it :: BVIx 7
BVView
data BVView (w :: Nat) (ixs :: [Nat]) Source #
A list of BVIx
with no repeated elements. This essentially gives us a
reordering of some subset of the bits in a bitvector.
bvView :: forall w ixs. (KnownRepr (BVView w) ixs, ValidView ixs) => BVView w ixs Source #
Construct a BVView
when the width and indices are known at compile time.
>>>
bvView @32 @(Slice 9 3)
BVView (BVIx 11 :< BVIx 10 :< BVIx 9 :< Nil)>>>
:type it
it :: BVView 32 '[11, 10, 9]>>>
bvView @32 @'[5, 7, 5]
<interactive>:19:1: error: • Invalid index list: '[5, 7, 5] (repeated index 5) • In the expression: bvView @32 @'[5, 7, 5] In an equation for ‘it’: it = bvView @32 @'[5, 7, 5]
bvViewL :: forall w ixs. KnownNat w => BVView w ixs -> Lens' (BV w) (BV (Length ixs)) Source #
Get a lens from a BVView
.
BVViews
data BVViews (w :: Nat) (ixss :: [[Nat]]) Source #
A list of BVViews
where each BVView
is disjoint from the others. This
is basically a decomposition of a bitvector into disjoint fields.
bvViews :: forall w ixss. (KnownRepr (BVViews w) ixss, ValidViews ixss) => BVViews w ixss Source #
Construct a BVViews
when the type is fully known at compile time.
>>>
bvViews @32 @'[Slice 9 3, Slice' 14 2]
BVViews (BVView (BVIx 11 :< BVIx 10 :< BVIx 9 :< Nil) :< BVView (BVIx 14 :< BVIx 15 :< Nil) :< Nil)>>>
:type it
it :: BVViews 32 '[ '[11, 10, 9], '[14, 15]]>>>
bvViews @32 @'[Slice 0 3, Slice 2 2]
<interactive>:3:1: error: • Invalid index lists '[ '[2, 1, 0], '[3, 2]] Lists '[2, 1, 0] and '[3, 2] are not disjoint (their intersection is '[2]) • In the expression: bvViews @32 @'[Slice 0 3, Slice 2 2] In an equation for ‘it’: it = bvViews @32 @'[Slice 0 3, Slice 2 2]
bvViewsL :: forall w ixss. KnownNat w => BVViews w ixss -> Lens' (BV w) (List BV (Lengths ixss)) Source #
Get a lens from a BVViews
.
Type families on lists
Various type families that are useful for constructing types when using this library.
type family Slice (i :: Nat) (w :: Nat) :: [Nat] where ... Source #
A "slice" of a bitvector. The first argument is the index of the least significant bit of the slice, and the second argument is the width.
>>>
:kind! Slice 7 4
Slice 7 4 :: [Nat] = '[10, 9, 8, 7]>>>
v = bvView @8 @(Slice 4 2)
>>>
printBV $ BV.mkBV knownNat 0b01101100 & bvViewL v .~ BV.mkBV knownNat 0b01
0b1011100:[8]
type family Slice' (i :: Nat) (w :: Nat) :: [Nat] where ... Source #
A "reversed slice" of a bitvector. The first argument is the index of the least significant bit of the slice, and the second argument is the width. The resulting slice reverses the order of the bits.
>>>
:kind! Slice' 7 4
Slice' 7 4 :: [Nat] = '[7, 8, 9, 10]>>>
v = bvView @8 @(Slice' 4 2)
>>>
printBV $ BV.mkBV knownNat 0b01101100 & bvViewL v .~ BV.mkBV knownNat 0b10
0b1011100:[8]