Copyright | (c) Sirui Lu 2024 |
---|---|
License | BSD-3-Clause (see the LICENSE file) |
Maintainer | siruilu@cs.washington.edu |
Stability | Experimental |
Portability | GHC only |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- data SomeBV bv where
- unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv
- conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
- 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)
- 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
- symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv
- ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv
- 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
- arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv)
- pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN
- type SomeIntN = SomeBV IntN
- pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN
- type SomeWordN = SomeBV WordN
- pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
- type SomeSymIntN = SomeBV SymIntN
- pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
- type SomeSymWordN = SomeBV SymWordN
- unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r
- unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv
- binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r
- binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv
- binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
- 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
- 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)
- 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)
Documentation
Non-indexed bitvectors.
Instances
Constructing and pattern matching on SomeBV
unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv Source #
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 Source #
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) Source #
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 Source #
symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv Source #
ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv Source #
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 Source #
arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv) Source #
Generate an arbitrary SomeBV
with a given run-time bitwidth.
Synonyms
pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN Source #
Pattern synonym for SomeBV
with concrete signed bitvectors.
pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN Source #
Pattern synonym for SomeBV
with concrete unsigned bitvectors.
pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN Source #
Pattern synonym for SomeBV
with symbolic signed bitvectors.
pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN Source #
Pattern synonym for SomeBV
with symbolic unsigned bitvectors.
type SomeSymWordN = SomeBV SymWordN Source #
Type synonym for SomeBV
with symbolic unsigned bitvectors.
Helpers for manipulating SomeBV
unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r Source #
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 Source #
binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r Source #
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 Source #
binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source #
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 Source #
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) Source #
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) Source #
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.