Grisette.Core.Data.Class.BitVector

Bit vector operations

class BV bv where

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

Methods

bvConcat :: bv -> bv -> bv

Concatenation of two bit vectors.

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

bvZext

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

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

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

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

Instances

BV SomeIntN

Defined in Grisette.Core.Data.BV

Methods

bvConcat :: SomeIntN -> SomeIntN -> SomeIntN

bvZext :: Int -> SomeIntN -> SomeIntN

bvSext :: Int -> SomeIntN -> SomeIntN

bvExt :: Int -> SomeIntN -> SomeIntN

bvSelect :: Int -> Int -> SomeIntN -> SomeIntN

BV SomeWordN

Defined in Grisette.Core.Data.BV

Methods

bvConcat :: SomeWordN -> SomeWordN -> SomeWordN

bvZext :: Int -> SomeWordN -> SomeWordN

bvSext :: Int -> SomeWordN -> SomeWordN

bvExt :: Int -> SomeWordN -> SomeWordN

bvSelect :: Int -> Int -> SomeWordN -> SomeWordN

BV SomeSymIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvConcat :: SomeSymIntN -> SomeSymIntN -> SomeSymIntN

bvZext :: Int -> SomeSymIntN -> SomeSymIntN

bvSext :: Int -> SomeSymIntN -> SomeSymIntN

bvExt :: Int -> SomeSymIntN -> SomeSymIntN

bvSelect :: Int -> Int -> SomeSymIntN -> SomeSymIntN

BV SomeSymWordN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvConcat :: SomeSymWordN -> SomeSymWordN -> SomeSymWordN

bvZext :: Int -> SomeSymWordN -> SomeSymWordN

bvSext :: Int -> SomeSymWordN -> SomeSymWordN

bvExt :: Int -> SomeSymWordN -> SomeSymWordN

bvSelect :: Int -> Int -> SomeSymWordN -> SomeSymWordN

bvExtract

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

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

Methods

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

Concatenation of two bit vectors.

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

sizedBVZext

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

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

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

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

Instances

SizedBV IntN

Defined in Grisette.Core.Data.BV

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r)

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r

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

SizedBV WordN

Defined in Grisette.Core.Data.BV

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r

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

SizedBV SymIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymIntN l -> SymIntN r -> SymIntN (l + r)

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r

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

SizedBV SymWordN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymWordN l -> SymWordN r -> SymWordN (l + r)

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r

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

sizedBVExtract

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

class BVSignConversion ubv sbv | ubv -> sbv, sbv -> ubv where

Convert bitvectors from and to signed

Methods

toSigned :: ubv -> sbv

Convert unsigned bitvector to signed

toUnsigned :: sbv -> ubv

Convert signed bitvector to unsigned

Instances

BVSignConversion SomeWordN SomeIntN

Defined in Grisette.Core.Data.BV

Methods

toSigned :: SomeWordN -> SomeIntN

toUnsigned :: SomeIntN -> SomeWordN

BVSignConversion SomeSymWordN SomeSymIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSigned :: SomeSymWordN -> SomeSymIntN

toUnsigned :: SomeSymIntN -> SomeSymWordN

(KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n)

Defined in Grisette.Core.Data.BV

Methods

toSigned :: WordN n -> IntN n

toUnsigned :: IntN n -> WordN n

(KnownNat n, 1 <= n) => BVSignConversion (SymWordN n) (SymIntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSigned :: SymWordN n -> SymIntN n

toUnsigned :: SymIntN n -> SymWordN n