bv-sized-0.7.0: a BitVector datatype that is parameterized by the vector width

Copyright(c) Galois Inc. 2018
LicenseBSD-3
Maintainerbenselfridge@galois.com
Stabilityexperimental
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Data.BitVector.Sized.BitLayout

Contents

Description

This module defines a BitLayout datatype which encodes a chunk-to-chunk mapping (no overlaps) from a smaller bit vector into a larger one. BitLayouts are especially useful for defining the encoding and decoding of opcodes/operands in an instruction.

Synopsis

Chunk

data Chunk (w :: Nat) :: * where Source #

Chunk type, parameterized by chunk width. The internal Int is the position of the least significant bit of the chunk, and the type-level nat w is the width of the chunk.

>>> chunk 2 :: Chunk 5
Chunk 5 2

Intuitively, the above chunk index captures the notion of embedding a BitVector 5 (bit vector of width 5) into a larger BitVector at index 2, preserving the order of the input bits. So an 5-bit input like 10011 would map to some larger bit vector containing the input starting at position 2, like 000001001100.

Multiple Chunks comprise a BitLayout; see below.

Constructors

Chunk :: NatRepr w -> Int -> Chunk w 
Instances
ShowF Chunk Source # 
Instance details

Defined in Data.BitVector.Sized.BitLayout

Methods

withShow :: p Chunk -> q tp -> (Show (Chunk tp) -> a) -> a #

showF :: Chunk tp -> String #

showsPrecF :: Int -> Chunk tp -> String -> String #

Show (Chunk w) Source # 
Instance details

Defined in Data.BitVector.Sized.BitLayout

Methods

showsPrec :: Int -> Chunk w -> ShowS #

show :: Chunk w -> String #

showList :: [Chunk w] -> ShowS #

Pretty (Chunk w) Source # 
Instance details

Defined in Data.BitVector.Sized.BitLayout

Pretty (Some Chunk) Source # 
Instance details

Defined in Data.BitVector.Sized.BitLayout

chunk :: KnownNat w => Int -> Chunk w Source #

Construct a Chunk in a context where the chunk width is known at compile time.

BitLayout

data BitLayout (t :: Nat) (s :: Nat) :: * Source #

BitLayout type, parameterized by target width and source width. t is the target width, s is the source width. s should always be less than or equal to t.

To construct a BitLayout, use the empty constructor and the <: operator, like so:

>>> empty :: BitLayout 32 0
BitLayout 32 0 (fromList [])
>>> let layout = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)
>>> layout
BitLayout 32 12 (fromList [Chunk 5 7,Chunk 7 25])
>>> :type it
it :: BitLayout 32 12

In the above example bitLayout defines a chunk-by-chunk mapping from a bit vector of width 12 to one of width 32. We imagine the input vector of width 12 listed like so:

0bAXXXXXBCXXXD
  |-----||---|
     7     5

Here, bits A, B, C, and D are just labeled as such to illustrate their place after the mapping. The BitLayout 32 12 defined above as the layout variable would map that 12-bit vector to the following 32-bit vector:

     (Bit 25)          (Bit 5)
        |                 |
        |                 |
        v                 v
0bAXXXXXB0000000000000CXXXD0000000
  |-----|             |---|
     7                  5

To use a BitLayout to achieve a bidirectional mapping like the one described above, you can either use the Lens interface or the functions inject and extract, which give an explicit setter and getter, respectively.

Example use of inject/extract:

>>> let bl = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)
>>> let sVec = bitVector 0b111111100001 :: BitVector 12
>>> sVec
0xfe1
>>> inject bl (bitVector 0) (bitVector 0b111111100001)
0xfe000080
>>> extract bl $ inject bl (bitVector 0) (bitVector 0b111111100001)
0xfe1
Instances
Show (BitLayout t s) Source # 
Instance details

Defined in Data.BitVector.Sized.BitLayout

Methods

showsPrec :: Int -> BitLayout t s -> ShowS #

show :: BitLayout t s -> String #

showList :: [BitLayout t s] -> ShowS #

Pretty (BitLayout t s) Source # 
Instance details

Defined in Data.BitVector.Sized.BitLayout

empty :: KnownNat t => BitLayout t 0 Source #

Construct an empty BitLayout.

singleChunk :: (KnownNat w, KnownNat w') => Int -> BitLayout w w' Source #

Construct a BitLayout with one chunk.

(<:) infixr 6 Source #

Arguments

:: Chunk r

chunk to add

-> BitLayout t s

layout we are adding the chunk to

-> BitLayout t (r + s) 

Add a Chunk to a BitLayout. If the Chunk does not fit, either because the resulting BitLayout would be too long or because it would overlap with a Chunk that is already in the BitLayout, we throw an error.

inject Source #

Arguments

:: BitLayout t s

The layout

-> BitVector t

The larger vector to inject into

-> BitVector s

The smaller vector to be injected

-> BitVector t 

Use a BitLayout to inject a smaller vector into a larger one.

extract Source #

Arguments

:: BitLayout t s

The layout

-> BitVector t

The larger vector to extract from

-> BitVector s 

Use a BitLayout to extract a smaller vector from a larger one.

Lenses

layoutsLens :: forall ws. List (BitLayout 32) ws -> Simple Lens (BitVector 32) (List BitVector ws) Source #

Lens for a parameterized List of BitLayouts.

Utilities

bitLayoutAssignmentList :: BitLayout t s -> [Int] Source #

From a BitLayout, get a list representing the position of each bit from the source to the target. The list

[3,4,5,10,11,12,13]

means that bit 0 of the source is placed in bit 3 of the target, bit 1 of the source is placed in bit 4 of the target, etc.