Grisette.Internal.SymPrim.SomeBV

Documentation

data SomeBV bv where

Non-indexed bitvectors.

The creation of SomeBV can be done with the bv function with a positive bit width and a value:

>>> bv 4 0xf :: SomeBV IntN
0xf

Operations on two SomeBV values require the bitwidths to be the same. So you should check for the bit width (via finiteBitSize) before performing operations:

>>> bv 4 0x3 + bv 4 0x3 :: SomeBV IntN
0x6
>>> bv 4 0x3 + bv 8 0x3 :: SomeBV IntN
*** Exception: BitwidthMismatch

One exception is that the equality testing (both concrete and symbolic via SymEq) does not require the bitwidths to be the same. Different bitwidths means the values are not equal:

>>> (bv 4 0x3 :: SomeBV IntN) == (bv 8 0x3)
False

Constructors

SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv

Instances

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSym () (bv n), Mergeable (SomeBV bv)) => GenSym Int (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Int -> m (Union (SomeBV bv))

(forall (n :: Nat). (KnownNat n, 1 <= n) => GenSymSimple () (bv n), Mergeable (SomeBV bv)) => GenSymSimple Int (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Int -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => Lift (bv n)) => Lift (SomeBV bv :: Type)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

lift :: Quote m => SomeBV bv -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => SomeBV bv -> Code m (SomeBV bv)

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeDivision 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeDivision 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeDivision mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeDivision mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDivision

Methods

withBaseSafeDivision :: (SafeDivision (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeLinearArith 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeLinearArith 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeLinearArith mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymRotate 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymRotate 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymRotate mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymRotate

Methods

withBaseSafeSymRotate :: (SafeSymRotate (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymShift 'Sym (Either BitwidthMismatch ArithException) SomeSymIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeSymIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching 'Sym m) => UnifiedSafeSymShift 'Sym (Either BitwidthMismatch ArithException) SomeSymWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeSymWordN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either BitwidthMismatch ArithException) SomeIntN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeIntN m => r) -> r

(MonadError (Either BitwidthMismatch ArithException) m, UnifiedBranching mode m) => UnifiedSafeSymShift mode (Either BitwidthMismatch ArithException) SomeWordN m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeSymShift

Methods

withBaseSafeSymShift :: (SafeSymShift (Either BitwidthMismatch ArithException) SomeWordN m => r) -> r

(forall (n :: Nat). (KnownNat n, 1 <= n) => Bits (bv n)) => Bits (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.&.) :: SomeBV bv -> SomeBV bv -> SomeBV bv

(.|.) :: SomeBV bv -> SomeBV bv -> SomeBV bv

xor :: SomeBV bv -> SomeBV bv -> SomeBV bv

complement :: SomeBV bv -> SomeBV bv

shift :: SomeBV bv -> Int -> SomeBV bv

rotate :: SomeBV bv -> Int -> SomeBV bv

zeroBits :: SomeBV bv

bit :: Int -> SomeBV bv

setBit :: SomeBV bv -> Int -> SomeBV bv

clearBit :: SomeBV bv -> Int -> SomeBV bv

complementBit :: SomeBV bv -> Int -> SomeBV bv

testBit :: SomeBV bv -> Int -> Bool

bitSizeMaybe :: SomeBV bv -> Maybe Int

bitSize :: SomeBV bv -> Int

isSigned :: SomeBV bv -> Bool

shiftL :: SomeBV bv -> Int -> SomeBV bv

unsafeShiftL :: SomeBV bv -> Int -> SomeBV bv

shiftR :: SomeBV bv -> Int -> SomeBV bv

unsafeShiftR :: SomeBV bv -> Int -> SomeBV bv

rotateL :: SomeBV bv -> Int -> SomeBV bv

rotateR :: SomeBV bv -> Int -> SomeBV bv

popCount :: SomeBV bv -> Int

(forall (n :: Nat). (KnownNat n, 1 <= n) => FiniteBits (bv n)) => FiniteBits (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

finiteBitSize :: SomeBV bv -> Int

countLeadingZeros :: SomeBV bv -> Int

countTrailingZeros :: SomeBV bv -> Int

(forall (n :: Nat). (KnownNat n, 1 <= n) => Enum (bv n)) => Enum (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

succ :: SomeBV bv -> SomeBV bv

pred :: SomeBV bv -> SomeBV bv

toEnum :: Int -> SomeBV bv

fromEnum :: SomeBV bv -> Int

enumFrom :: SomeBV bv -> [SomeBV bv]

enumFromThen :: SomeBV bv -> SomeBV bv -> [SomeBV bv]

enumFromTo :: SomeBV bv -> SomeBV bv -> [SomeBV bv]

enumFromThenTo :: SomeBV bv -> SomeBV bv -> SomeBV bv -> [SomeBV bv]

(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => Num (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(+) :: SomeBV bv -> SomeBV bv -> SomeBV bv

(-) :: SomeBV bv -> SomeBV bv -> SomeBV bv

(*) :: SomeBV bv -> SomeBV bv -> SomeBV bv

negate :: SomeBV bv -> SomeBV bv

abs :: SomeBV bv -> SomeBV bv

signum :: SomeBV bv -> SomeBV bv

fromInteger :: Integer -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => Integral (bv n)) => Integral (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

quot :: SomeBV bv -> SomeBV bv -> SomeBV bv

rem :: SomeBV bv -> SomeBV bv -> SomeBV bv

div :: SomeBV bv -> SomeBV bv -> SomeBV bv

mod :: SomeBV bv -> SomeBV bv -> SomeBV bv

quotRem :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)

divMod :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)

toInteger :: SomeBV bv -> Integer

(forall (n :: Nat). (KnownNat n, 1 <= n) => Real (bv n)) => Real (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toRational :: SomeBV bv -> Rational

(forall (n :: Nat). (KnownNat n, 1 <= n) => Show (bv n)) => Show (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

showsPrec :: Int -> SomeBV bv -> ShowS

show :: SomeBV bv -> String

showList :: [SomeBV bv] -> ShowS

(forall (n :: Nat). (KnownNat n, 1 <= n) => NFData (bv n)) => NFData (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rnf :: SomeBV bv -> ()

(forall (n :: Nat). (KnownNat n, 1 <= n) => Eq (bv n)) => Eq (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(==) :: SomeBV bv -> SomeBV bv -> Bool

(/=) :: SomeBV bv -> SomeBV bv -> Bool

(forall (n :: Nat). (KnownNat n, 1 <= n) => Ord (bv n)) => Ord (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

compare :: SomeBV bv -> SomeBV bv -> Ordering

(<) :: SomeBV bv -> SomeBV bv -> Bool

(<=) :: SomeBV bv -> SomeBV bv -> Bool

(>) :: SomeBV bv -> SomeBV bv -> Bool

(>=) :: SomeBV bv -> SomeBV bv -> Bool

max :: SomeBV bv -> SomeBV bv -> SomeBV bv

min :: SomeBV bv -> SomeBV bv -> SomeBV bv

SizedBV bv => BV (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv

bvZext :: Int -> SomeBV bv -> SomeBV bv

bvSext :: Int -> SomeBV bv -> SomeBV bv

bvExt :: Int -> SomeBV bv -> SomeBV bv

bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv

bv :: Integral a => Int -> a -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => EvalSym (bv n)) => EvalSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

evalSym :: Bool -> Model -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => ExtractSym (bv n)) => ExtractSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

extractSym :: SomeBV bv -> SymbolSet

(forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n)) => ITEOp (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) => Mergeable (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

rootStrategy :: MergingStrategy (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => PPrint (bv n)) => PPrint (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

pformat :: SomeBV bv -> Doc ann

pformatPrec :: Int -> SomeBV bv -> Doc ann

pformatList :: [SomeBV bv] -> Doc ann

(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstSym (bv n)) => SubstSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

substSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymEq (bv n)) => SymEq (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.==) :: SomeBV bv -> SomeBV bv -> SymBool

(./=) :: SomeBV bv -> SomeBV bv -> SymBool

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymOrd (bv n)) => SymOrd (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

(.<) :: SomeBV bv -> SomeBV bv -> SymBool

(.<=) :: SomeBV bv -> SomeBV bv -> SymBool

(.>) :: SomeBV bv -> SomeBV bv -> SymBool

(.>=) :: SomeBV bv -> SomeBV bv -> SymBool

symCompare :: SomeBV bv -> SomeBV bv -> Union Ordering

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymRotate (bv n)) => SymRotate (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symRotate :: SomeBV bv -> SomeBV bv -> SomeBV bv

symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => SymShift (bv n)) => SymShift (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

symShift :: SomeBV bv -> SomeBV bv -> SomeBV bv

symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv

(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n)) => AllSyms (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]

allSyms :: SomeBV bv -> [SomeSym]

(forall (n :: Nat). (KnownNat n, 1 <= n) => Hashable (bv n)) => Hashable (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

hashWithSalt :: Int -> SomeBV bv -> Int

hash :: SomeBV bv -> Int

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (SomeBV bv) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => SomeBV bv -> m (Union (SomeBV bv))

(forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (SomeBV bv) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n), SignConversion (ubv 1) (sbv 1)) => SignConversion (SomeBV ubv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSigned :: SomeBV ubv -> SomeBV sbv

toUnsigned :: SomeBV sbv -> SomeBV ubv

(forall (n :: Nat). (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) => ToCon (SomeBV sbv) (SomeBV cbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toCon :: SomeBV sbv -> Maybe (SomeBV cbv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) => ToSym (SomeBV cbv) (SomeBV sbv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

toSym :: SomeBV cbv -> SomeBV sbv

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSym () (bv m), Mergeable (SomeBV bv)) => GenSym (Proxy n) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

fresh :: MonadFresh m => Proxy n -> m (Union (SomeBV bv))

(KnownNat n, 1 <= n, forall (m :: Nat). (KnownNat m, 1 <= m) => GenSymSimple () (bv m), Mergeable (SomeBV bv)) => GenSymSimple (Proxy n) (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

simpleFresh :: MonadFresh m => Proxy n -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeDivision e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeDivision (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeLinearArith e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeLinearArith (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeNeg :: SomeBV bv -> m (SomeBV bv)

safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymRotate e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymRotate (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeSymShift e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeSymShift (Either BitwidthMismatch e) (SomeBV bv) m

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)

Constructing and pattern matching on SomeBV

unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv

Construct a SomeBV with a given run-time bitwidth and a polymorphic value for the underlying bitvector.

conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv

Construct a symbolic SomeBV with a given concrete SomeBV. Similar to con but for SomeBV.

>>> a = bv 8 0x12 :: SomeIntN
>>> conBV a :: SomeSymIntN
0x12

conBVView :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv)

View pattern for symbolic SomeBV to see if it contains a concrete value and extract it. Similar to conView but for SomeBV.

>>> conBVView (bv 8 0x12 :: SomeSymIntN)
Just 0x12
>>> conBVView (ssymBV 4 "a" :: SomeSymIntN)
Nothing

pattern ConBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv

Pattern synonym for symbolic SomeBV to see if it contains a concrete value and extract it. Similar to Con but for SomeBV.

>>> case (bv 8 0x12 :: SomeSymIntN) of { ConBV c -> c; _ -> error "impossible" }
0x12

symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv

Construct a symbolic SomeBV with a given run-time bitwidth and a symbol. Similar to sym but for SomeBV.

>>> symBV 8 "a" :: SomeSymIntN
a

ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv

Construct a symbolic SomeBV with a given run-time bitwidth and an identifier. Similar to ssym but for SomeBV.

>>> ssymBV 8 "a" :: SomeSymIntN
a

isymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv

Construct a symbolic SomeBV with a given run-time bitwidth, an identifier and an index. Similar to isym but for SomeBV.

>>> isymBV 8 "a" 1 :: SomeSymIntN
a@1

arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv)

Generate an arbitrary SomeBV with a given run-time bitwidth.

Synonyms

pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN

Pattern synonym for SomeBV for concrete signed bitvectors.

type SomeIntN = SomeBV IntN

Type synonym for SomeBV for concrete signed bitvectors.

pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN

Pattern synonym for SomeBV for concrete unsigned bitvectors.

type SomeWordN = SomeBV WordN

Type synonym for SomeBV for concrete unsigned bitvectors.

pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN

Pattern synonym for SomeBV for symbolic signed bitvectors.

type SomeSymIntN = SomeBV SymIntN

Type synonym for SomeBV for symbolic signed bitvectors.

pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN

Pattern synonym for SomeBV for symbolic unsigned bitvectors.

type SomeSymWordN = SomeBV SymWordN

Type synonym for SomeBV for symbolic unsigned bitvectors.

Helpers for manipulating SomeBV

unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r

Lift a unary operation on sized bitvectors that returns anything to SomeBV.

unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv

Lift a unary operation on sized bitvectors that returns a bitvector to SomeBV. The result will also be wrapped with SomeBV.

binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r

Lift a binary operation on sized bitvectors that returns anything to SomeBV. Crash if the bitwidths do not match.

binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv

Lift a binary operation on sized bitvectors that returns a bitvector to SomeBV. The result will also be wrapped with SomeBV. Crash if the bitwidths do not match.

binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)

Lift a binary operation on sized bitvectors that returns two bitvectors to SomeBV. The results will also be wrapped with SomeBV. Crash if the bitwidths do not match.

binSomeBVSafe :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> SomeBV bv -> SomeBV bv -> m r

Lift a binary operation on sized bitvectors that returns anything wrapped with ExceptT to SomeBV. If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

binSomeBVSafeR1 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv)

Lift a binary operation on sized bitvectors that returns a bitvector wrapped with ExceptT to SomeBV. The result will also be wrapped with SomeBV.

If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.

binSomeBVSafeR2 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)

Lift a binary operation on sized bitvectors that returns two bitvectors wrapped with ExceptT to SomeBV. The results will also be wrapped with SomeBV.

If the bitwidths do not match, throw an BitwidthMismatch error to the monadic context.