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

Copyright (c) Benjamin Selfridge 2018Galois Inc. BSD3 benselfridge@galois.com experimental portable None Haskell2010

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
[2...6]


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

 Source # MethodswithShow :: p f -> q tp -> (Show (f tp) -> a) -> a #showF :: f tp -> String #showsF :: f tp -> String -> String # Show (Chunk w) Source # MethodsshowsPrec :: Int -> Chunk w -> ShowS #show :: Chunk w -> String #showList :: [Chunk w] -> ShowS #

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
[]
>>> let layout = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)
>>> layout
[[25...31],[7...11]]
>>> :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)
>>> bl
[[25...31],[7...11]]
>>> let sVec = bv 0b111111100001 :: BitVector 12
>>> sVec
0xfe1<12>
>>> inject bl (bv 0) (bv 0b111111100001)
0xfe000080<32>
>>> extract bl \$ inject bl (bv 0) (bv 0b111111100001)
0xfe1<12>


Instances

 Show (BitLayout t s) Source # MethodsshowsPrec :: Int -> BitLayout t s -> ShowS #show :: BitLayout t s -> String #showList :: [BitLayout t s] -> ShowS #

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

Construct an empty BitLayout.

(<:) 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.

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.

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.

# Lens

layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s) Source #

Lens for bit layout.