sbv-0.9.20: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.

Portability portable experimental erkokl@gmail.com

Data.SBV.Internals

Description

Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module.

Synopsis

# Running symbolic programs manually

data Result Source

Result of running a symbolic computation

Instances

 Show Result NFData Result

Run a symbolic computation and return a `Result`

# Other internal structures useful for low-level programming

data SBV a Source

The Symbolic value. Either a constant (`Left`) or a symbolic value (`Right Cached`). Note that caching is essential for making sure sharing is preserved. The parameter `a` is phantom, but is extremely important in keeping the user interface strongly typed.

Constructors

 SBV !(Bool, Size) !(Either CW (Cached SW))

Instances

 Testable SBool Boolean SBool BVDivisible SWord64 BVDivisible SWord32 BVDivisible SWord16 BVDivisible SWord8 FromBits SInt64 FromBits SInt32 FromBits SInt16 FromBits SInt8 FromBits SWord64 FromBits SWord32 FromBits SWord16 FromBits SWord8 FromBits SBool Polynomial SWord64 Polynomial SWord32 Polynomial SWord16 Polynomial SWord8 Provable SBool Provable Predicate SignCast SWord64 SInt64 SignCast SWord32 SInt32 SignCast SWord16 SInt16 SignCast SWord8 SInt8 Splittable SWord64 SWord32 Splittable SWord32 SWord16 Splittable SWord16 SWord8 (SymWord a, Bounded a) => Bounded (SBV a) (Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) Eq (SBV a) (Ord a, Num a, SymWord a) => Num (SBV a) Show (SBV a) (SymWord a, Arbitrary a) => Arbitrary (SBV a) (Bits a, SymWord a) => Bits (SBV a) NFData a => NFData (SBV a) Outputtable (SBV a) HasSignAndSize (SBV a) HasSignAndSize a => Uninterpreted (SBV a) SymWord a => Mergeable (SBV a) SymWord a => OrdSymbolic (SBV a) EqSymbolic (SBV a) (SymWord a, PrettyNum a) => PrettyNum (SBV a) (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) (SymWord a, EqSymbolic z) => Equality (SBV a -> z) (SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) (SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) (SymWord a, Provable p) => Provable (SBV a -> p)

class HasSignAndSize a whereSource

Methods

sizeOf :: a -> SizeSource

hasSign :: a -> BoolSource

showType :: a -> StringSource

data CW Source

`CW` represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the `FromBits` class). For signed words, the most significant digit is considered to be the sign

Instances

 Eq CW Ord CW Show CW NFData CW HasSignAndSize CW BVDivisible CW PrettyNum CW

mkConstCW :: Integral a => (Bool, Size) -> a -> CWSource

genFree :: (Bool, Size) -> String -> Symbolic (SBV a)Source

genFree_ :: (Bool, Size) -> Symbolic (SBV a)Source

# Compilation to C

Lower level version of `compileToC`, producing a `CgPgmBundle`

Lower level version of `compileToCLib`, producing a `CgPgmBundle`

newtype CgPgmBundle Source

Representation of a collection of generated programs.

Constructors

 CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))]

Instances

 Show CgPgmBundle

data CgPgmKind Source

Different kinds of files we can produce. Currently this is quite C specific.

Constructors

# Integrating with the test framework

Functionality needed for extending SBV's internal test-suite. Only for developers of further libraries on top of SBV.

generateGoldCheck :: FilePath -> Bool -> forall a. Show a => IO a -> FilePath -> IO ()Source

Create a gold file for the test case

showsAs :: Show a => a -> String -> AssertionSource

Checks that a particular result shows as `s`

ioShowsAs :: Show a => IO a -> String -> AssertionSource

Run an IO computation and check that it's result shows as `s`

mkTestSuite :: ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test) -> SBVTestSuiteSource

Wrap over `SBVTestSuite`, avoids exporting the constructor

A Test-suite, parameterized by the gold-check generator/checker

Constructors

 SBVTestSuite ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test)

module Test.HUnit