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.Core.Data.Class.BitVector

Contents

Bit vector operations

Description

Synopsis

class SomeBV bv where
- someBVConcat :: bv -> bv -> bv
- someBVZext :: forall p l. KnownNat l => p l -> bv -> bv
- someBVSext :: forall p l. KnownNat l => p l -> bv -> bv
- someBVExt :: forall p l. KnownNat l => p l -> bv -> bv
- someBVSelect :: forall p ix q w. (KnownNat ix, KnownNat w) => p ix -> q w -> bv -> bv
someBVZext' :: forall l bv. SomeBV bv => NatRepr l -> bv -> bv
someBVSext' :: forall l bv. SomeBV bv => NatRepr l -> bv -> bv
someBVExt' :: forall l bv. SomeBV bv => NatRepr l -> bv -> bv
someBVSelect' :: forall ix w bv. SomeBV bv => NatRepr ix -> NatRepr w -> bv -> bv
someBVExtract :: forall p (i :: Nat) q (j :: Nat) bv. (SomeBV bv, KnownNat i, KnownNat j) => p i -> q j -> bv -> bv
someBVExtract' :: forall (i :: Nat) (j :: Nat) bv. SomeBV bv => NatRepr i -> NatRepr j -> 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) => proxy ix -> proxy w -> bv n -> bv w
sizedBVExtract :: forall proxy i j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i) => proxy i -> proxy j -> bv n -> bv ((i - j) + 1)

Bit vector operations

class SomeBV bv where Source #

Bit vector operations. Including concatenation (someBVConcat), extension (someBVZext, someBVSext, someBVExt), and selection (someBVSelect).

Methods

someBVConcat :: bv -> bv -> bv Source #

Concatenation of two bit vectors.

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

someBVZext Source #

Arguments

:: forall p l. KnownNat l
=> p l	Desired output length
-> bv	Bit vector to extend
-> bv

Zero extension of a bit vector.

>>> someBVZext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
0b000101

someBVSext Source #

Arguments

:: forall p l. KnownNat l
=> p l	Desired output length
-> bv	Bit vector to extend
-> bv

Sign extension of a bit vector.

>>> someBVSext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))
0b111101

someBVExt Source #

Arguments

:: forall p l. KnownNat l
=> p l	Desired output length
-> bv	Bit vector to extend
-> bv

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

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

someBVSelect Source #

Arguments

:: forall p ix q w. (KnownNat ix, KnownNat w)
=> 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	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.

>>> someBVSelect (Proxy @1) (Proxy @3) (SomeSymIntN (0b001010 :: SymIntN 6))
0b101

Instances

Instances details

SomeBV SomeIntN Source #
Instance details Defined in Grisette.Core.Data.BV Methods someBVConcat :: SomeIntN -> SomeIntN -> SomeIntN Source # someBVZext :: forall p (l :: Nat). KnownNat l => p l -> SomeIntN -> SomeIntN Source # someBVSext :: forall p (l :: Nat). KnownNat l => p l -> SomeIntN -> SomeIntN Source # someBVExt :: forall p (l :: Nat). KnownNat l => p l -> SomeIntN -> SomeIntN Source # someBVSelect :: forall p (ix :: Nat) q (w :: Nat). (KnownNat ix, KnownNat w) => p ix -> q w -> SomeIntN -> SomeIntN Source #
SomeBV SomeWordN Source #
Instance details Defined in Grisette.Core.Data.BV Methods someBVConcat :: SomeWordN -> SomeWordN -> SomeWordN Source # someBVZext :: forall p (l :: Nat). KnownNat l => p l -> SomeWordN -> SomeWordN Source # someBVSext :: forall p (l :: Nat). KnownNat l => p l -> SomeWordN -> SomeWordN Source # someBVExt :: forall p (l :: Nat). KnownNat l => p l -> SomeWordN -> SomeWordN Source # someBVSelect :: forall p (ix :: Nat) q (w :: Nat). (KnownNat ix, KnownNat w) => p ix -> q w -> SomeWordN -> SomeWordN Source #
SomeBV SomeSymIntN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods someBVConcat :: SomeSymIntN -> SomeSymIntN -> SomeSymIntN Source # someBVZext :: forall p (l :: Nat). KnownNat l => p l -> SomeSymIntN -> SomeSymIntN Source # someBVSext :: forall p (l :: Nat). KnownNat l => p l -> SomeSymIntN -> SomeSymIntN Source # someBVExt :: forall p (l :: Nat). KnownNat l => p l -> SomeSymIntN -> SomeSymIntN Source # someBVSelect :: forall p (ix :: Nat) q (w :: Nat). (KnownNat ix, KnownNat w) => p ix -> q w -> SomeSymIntN -> SomeSymIntN Source #
SomeBV SomeSymWordN Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods someBVConcat :: SomeSymWordN -> SomeSymWordN -> SomeSymWordN Source # someBVZext :: forall p (l :: Nat). KnownNat l => p l -> SomeSymWordN -> SomeSymWordN Source # someBVSext :: forall p (l :: Nat). KnownNat l => p l -> SomeSymWordN -> SomeSymWordN Source # someBVExt :: forall p (l :: Nat). KnownNat l => p l -> SomeSymWordN -> SomeSymWordN Source # someBVSelect :: forall p (ix :: Nat) q (w :: Nat). (KnownNat ix, KnownNat w) => p ix -> q w -> SomeSymWordN -> SomeSymWordN Source #

someBVZext' Source #

Arguments

:: forall l bv. SomeBV bv
=> NatRepr l	Desired output length
-> bv	Bit vector to extend
-> bv

Zero extension of a bit vector.

>>> someBVZext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
0b000101

someBVSext' Source #

Arguments

:: forall l bv. SomeBV bv
=> NatRepr l
-> bv	Desired output length
-> bv	Bit vector to extend

Sign extension of a bit vector.

>>> someBVSext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
0b111101

someBVExt' Source #

Arguments

:: forall l bv. SomeBV bv
=> NatRepr l	Desired output length
-> bv	Bit vector to extend
-> bv

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

>>> someBVExt' (natRepr @6) (SomeSymIntN (0b101 :: SymIntN 3))
0b111101
>>> someBVExt' (natRepr @6) (SomeSymIntN (0b001 :: SymIntN 3))
0b000001
>>> someBVExt' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))
0b000101
>>> someBVExt' (natRepr @6) (SomeSymWordN (0b001 :: SymWordN 3))
0b000001

someBVSelect' Source #

Arguments

:: forall ix w bv. SomeBV bv
=> NatRepr ix	Index of the least significant bit of the slice
-> NatRepr w	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.

>>> someBVSelect' (natRepr @1) (natRepr @3) (SomeSymIntN (0b001010 :: SymIntN 6))
0b101

someBVExtract Source #

Arguments

:: forall p (i :: Nat) q (j :: Nat) bv. (SomeBV bv, KnownNat i, KnownNat j)
=> 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	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.

>>> someBVExtract (Proxy @4) (Proxy @2) (SomeSymIntN (0b010100 :: SymIntN 6))
0b101

someBVExtract' Source #

Arguments

:: forall (i :: Nat) (j :: Nat) bv. SomeBV bv
=> NatRepr i	The start position to extract from, `i < n` must hold where `n` is the size of the output bit vector
-> NatRepr j	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.

>>> someBVExtract' (natRepr @4) (natRepr @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).

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)
=> proxy ix	Index of the least significant bit of the slice
-> proxy 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

Instances details

SizedBV IntN Source #
Instance details 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) 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) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> IntN n -> IntN w Source #
SizedBV WordN Source #
Instance details 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) 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) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> WordN n -> WordN w Source #
SizedBV SymIntN Source #
Instance details 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) 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) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> SymIntN n -> SymIntN w Source #
SizedBV SymWordN Source #
Instance details 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) 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) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> SymWordN n -> SymWordN w Source #

sizedBVExtract Source #

Arguments

:: forall proxy i j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i)
=> proxy i	The start position to extract from, `i < n` must hold where `n` is the size of the output bit vector
-> proxy 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