Grisette.Core.Data.Class.BitVector

Bit vector operations

class BVConcat bv1 bv2 bv3 | bv1 bv2 -> bv3 where

Bitwise concatenation (bvconcat) of the given bit vector values.

Methods

bvconcat :: bv1 -> bv2 -> bv3

Bitwise concatenation of the given bit vector values.

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

Instances

(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) => BVConcat (IntN n) (IntN m) (IntN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvconcat :: IntN n -> IntN m -> IntN w

(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) => BVConcat (WordN n) (WordN m) (WordN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvconcat :: WordN n -> WordN m -> WordN w

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w')

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w')

class BVExtend bv1 (n :: Nat) bv2 | bv1 n -> bv2 where

Bitwise extension of the given bit vector values.

Methods

bvzeroExtend

Arguments

:: proxy n

Desired output width

-> bv1

Bit vector to extend

-> bv2

Bitwise zero extension of the given bit vector values.

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

bvsignExtend

Arguments

:: proxy n

Desired output width

-> bv1

Bit vector to extend

-> bv2

Bitwise signed extension of the given bit vector values.

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

bvextend

Arguments

:: proxy n

Desired output width

-> bv1

Bit vector to extend

-> bv2

Bitwise extension of the given bit vector values. Signedness is determined by the input bit vector type.

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

Instances

(KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (IntN n) r (IntN r)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvzeroExtend :: proxy r -> IntN n -> IntN r

bvsignExtend :: proxy r -> IntN n -> IntN r

bvextend :: proxy r -> IntN n -> IntN r

(KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (WordN n) r (WordN r)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvzeroExtend :: proxy r -> WordN n -> WordN r

bvsignExtend :: proxy r -> WordN n -> WordN r

bvextend :: proxy r -> WordN n -> WordN r

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', w <= w', (w + 1) <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (IntN w)) w' (Sym (IntN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w')

bvsignExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w')

bvextend :: proxy w' -> Sym (IntN w) -> Sym (IntN w')

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', (w + 1) <= w', w <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (WordN w)) w' (Sym (WordN w'))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w')

bvsignExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w')

bvextend :: proxy w' -> Sym (WordN w) -> Sym (WordN w')

class BVSelect bv1 (ix :: Nat) (w :: Nat) bv2 | bv1 w -> bv2 where

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

Methods

bvselect

Arguments

:: proxy ix

Index to start selecting from

-> proxy w

Desired output width, 0 <= ix and ix + w < n must hold where n is the size of the input bit vector

-> bv1

Bit vector to select from

-> bv2

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

The indices are counting from zero from the least significant bit.

>>> bvselect (Proxy @1) (Proxy @3) (con 0b001010 :: SymIntN 6)
0b101

Instances

(KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, (ix + w) <= n) => BVSelect (IntN n) ix w (IntN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvselect :: proxy ix -> proxy w -> IntN n -> IntN w

(KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, (ix + w) <= n) => BVSelect (WordN n) ix w (WordN w)

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvselect :: proxy ix -> proxy w -> WordN n -> WordN w

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (IntN ow)) ix w (Sym (IntN w))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w)

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (WordN ow)) ix w (Sym (WordN w))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w)

bvextract

Arguments

:: forall proxy i j bv1 bv2. BVSelect bv1 j ((i - j) + 1) bv2

=> proxy i

The start position to extract from, 0 <= i < n must hold where n is the size of the output bit vector

-> proxy j

The end position to extract from, 0 <= j <= i must hold

-> bv1

Bit vector to extract from

-> bv2

Extract a smaller bit vector from a larger one from bits i down to j.

The indices are counting from zero from the least significant bit. >>> bvextract (Proxy 3) (Proxy 1) (con 0b001010 :: SymIntN 6) 0b101