grisette-0.3.1.1: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.BitVector

Description

 
Synopsis

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

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

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

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) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q 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) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q 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) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q 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) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymWordN n -> SymWordN w 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

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

Convert bitvectors from and to signed

Methods

toSigned :: ubv -> sbv Source #

Convert unsigned bitvector to signed

toUnsigned :: sbv -> ubv Source #

Convert signed bitvector to unsigned