Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Internal.Core.Data.Class.BitVector

Contents

Bit vector operations

Description

Synopsis

class BV bv where
- bvConcat :: bv -> bv -> bv
- bvZext :: Int -> bv -> bv
- bvSext :: Int -> bv -> bv
- bvExt :: Int -> bv -> bv
- bvSelect :: Int -> Int -> bv -> bv
- bv :: Integral a => Int -> a -> bv
bvExtract :: BV bv => Int -> Int -> bv -> bv
class SizedBV bv where
- sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r)
- sizedBVZext :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVSext :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVExt :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVSelect :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> bv n -> bv w
- sizedBVFromIntegral :: (Integral a, KnownNat n, 1 <= n) => a -> bv n
sizedBVExtract :: forall p i q j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i) => p i -> q j -> bv n -> bv ((i - j) + 1)

Bit vector operations

class BV bv where Source #

Bit vector operations. Including concatenation (bvConcat), extension (bvZext, bvSext, bvExt), and selection (bvSelect).

Methods

bvConcat :: bv -> bv -> bv Source #

Concatenation of two bit vectors.

>>> bvConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))
0b101010

bvZext Source #

Arguments

:: Int	Desired output length
-> bv	Bit vector to extend
-> bv

Zero extension of a bit vector.

>>> bvZext 6 (SomeSymWordN (0b101 :: SymWordN 3))
0b000101

bvSext Source #

Arguments

:: Int	Desired output length
-> bv	Bit vector to extend
-> bv

Sign extension of a bit vector.

>>> bvSext 6 (SomeSymWordN (0b101 :: SymWordN 3))
0b111101

bvExt Source #

Arguments

:: Int	Desired output length
-> bv	Bit vector to extend
-> bv

Extension of a bit vector. Signedness is determined by the input bit vector type.

>>> bvExt 6 (SomeSymIntN (0b101 :: SymIntN 3))
0b111101
>>> bvExt 6 (SomeSymIntN (0b001 :: SymIntN 3))
0b000001
>>> bvExt 6 (SomeSymWordN (0b101 :: SymWordN 3))
0b000101
>>> bvExt 6 (SomeSymWordN (0b001 :: SymWordN 3))
0b000001

bvSelect Source #

Arguments

:: Int	Index of the least significant bit of the slice
-> Int	Desired output width, `ix + w <= n` must hold where `n` is the size of the input bit vector
-> bv	Bit vector to select from
-> bv

Slicing out a smaller bit vector from a larger one, selecting a slice with width w starting from index ix.

The least significant bit is indexed as 0.

>>> bvSelect 1 3 (SomeSymIntN (0b001010 :: SymIntN 6))
0b101

bv Source #

Arguments

:: Integral a
=> Int	Bit width
-> a	Integral value
-> bv

Create a bit vector from an integer. The bit-width is the first argument, which should not be zero.

>>> bv 12 21 :: SomeSymIntN
0x015

Instances

Instances details

SizedBV bv => BV (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv Source # bvZext :: Int -> SomeBV bv -> SomeBV bv Source # bvSext :: Int -> SomeBV bv -> SomeBV bv Source # bvExt :: Int -> SomeBV bv -> SomeBV bv Source # bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv Source # bv :: Integral a => Int -> a -> SomeBV bv Source #

bvExtract Source #

Arguments

:: BV bv
=> Int	The start position to extract from, `i < n` must hold where `n` is the size of the output bit vector
-> Int	The end position to extract from, `j <= i` must hold
-> bv	Bit vector to extract from
-> bv

Slicing out a smaller bit vector from a larger one, extract a slice from bit i down to j.

The least significant bit is indexed as 0.

>>> bvExtract 4 2 (SomeSymIntN (0b010100 :: SymIntN 6))
0b101

class SizedBV bv where Source #

Sized bit vector operations. Including concatenation (sizedBVConcat), extension (sizedBVZext, sizedBVSext, sizedBVExt), and selection (sizedBVSelect).

Minimal complete definition

sizedBVConcat, sizedBVZext, sizedBVSext, sizedBVExt, sizedBVSelect

Methods

sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r) Source #

Concatenation of two bit vectors.

>>> sizedBVConcat (0b101 :: SymIntN 3) (0b010 :: SymIntN 3)
0b101010

sizedBVZext Source #

Arguments

:: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r)
=> proxy r	Desired output width
-> bv l	Bit vector to extend
-> bv r

Zero extension of a bit vector.

>>> sizedBVZext (Proxy @6) (0b101 :: SymIntN 3)
0b000101

sizedBVSext Source #

Arguments

:: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r)
=> proxy r	Desired output width
-> bv l	Bit vector to extend
-> bv r

Signed extension of a bit vector.

>>> sizedBVSext (Proxy @6) (0b101 :: SymIntN 3)
0b111101

sizedBVExt Source #

Arguments

:: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r)
=> proxy r	Desired output width
-> bv l	Bit vector to extend
-> bv r

Extension of a bit vector. Signedness is determined by the input bit vector type.

>>> sizedBVExt (Proxy @6) (0b101 :: SymIntN 3)
0b111101
>>> sizedBVExt (Proxy @6) (0b001 :: SymIntN 3)
0b000001
>>> sizedBVExt (Proxy @6) (0b101 :: SymWordN 3)
0b000101
>>> sizedBVExt (Proxy @6) (0b001 :: SymWordN 3)
0b000001

sizedBVSelect Source #

Arguments

:: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n)
=> p ix	Index of the least significant bit of the slice
-> q w	Desired output width, `ix + w <= n` must hold where `n` is the size of the input bit vector
-> bv n	Bit vector to select from
-> bv w

Slicing out a smaller bit vector from a larger one, selecting a slice with width w starting from index ix.

The least significant bit is indexed as 0.

>>> sizedBVSelect (Proxy @2) (Proxy @3) (con 0b010100 :: SymIntN 6)
0b101

sizedBVFromIntegral :: (Integral a, KnownNat n, 1 <= n) => a -> bv n Source #

default sizedBVFromIntegral :: (Num (bv n), Integral a, KnownNat n, 1 <= n) => a -> bv n Source #

Instances

Instances details

SizedBV IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> IntN n -> IntN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> IntN n Source #
SizedBV WordN Source #
Instance details Defined in Grisette.Internal.SymPrim.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> WordN n -> WordN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> WordN n Source #
SizedBV SymIntN Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymIntN l -> SymIntN r -> SymIntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymIntN n -> SymIntN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymIntN n Source #
SizedBV SymWordN Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymWordN l -> SymWordN r -> SymWordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymWordN n -> SymWordN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymWordN n Source #

sizedBVExtract Source #

Arguments

:: forall p i q j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i)
=> p i	The start position to extract from, `i < n` must hold where `n` is the size of the output bit vector
-> q j	The end position to extract from, `j <= i` must hold
-> bv n	Bit vector to extract from
-> bv ((i - j) + 1)

Slicing out a smaller bit vector from a larger one, extract a slice from bit i down to j.

The least significant bit is indexed as 0.

>>> sizedBVExtract (Proxy @4) (Proxy @2) (con 0b010100 :: SymIntN 6)
0b101