sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Tools.CodeGen

Contents

- Code generation from symbolic programs
  - Setting code-generation options
  - Designating inputs
  - Designating outputs
  - Designating return values
  - Code generation with uninterpreted functions
  - Code generation with `SInteger` and `SReal` types
  - Compilation to C

Description

Code-generation from SBV programs.

Synopsis

- data SBVCodeGen a
- cgSym :: Symbolic a -> SBVCodeGen a
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- cgOverwriteFiles :: Bool -> SBVCodeGen ()
- cgShowU8UsingHex :: Bool -> SBVCodeGen ()
- cgInput :: SymVal a => String -> SBVCodeGen (SBV a)
- cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a]
- cgOutput :: String -> SBV a -> SBVCodeGen ()
- cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen ()
- cgReturn :: SBV a -> SBVCodeGen ()
- cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
  - = CgFloat
  - | CgDouble
  - | CgLongDouble
- compileToC :: Maybe FilePath -> String -> SBVCodeGen a -> IO a
- compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen a)] -> IO [a]

# Code generation from symbolic programs

The SBV library can generate straight-line executable code in C. (While other target languages are certainly possible, currently only C is supported.) The generated code will perform no run-time memory-allocations, (no calls to `malloc`), so its memory usage can be predicted ahead of time. Also, the functions will execute precisely the same instructions in all calls, so they have predictable timing properties as well. The generated code has no loops or jumps, and is typically quite fast. While the generated code can be large due to complete unrolling, these characteristics make them suitable for use in hard real-time systems, as well as in traditional computing.

data SBVCodeGen a Source #

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

#### Instances

Instances details

Monad SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods (>>=) :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b (>>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b return :: a -> SBVCodeGen a
Functor SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b (<$) :: a -> SBVCodeGen b -> SBVCodeGen a
MonadFail SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods fail :: String -> SBVCodeGen a
Applicative SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods pure :: a -> SBVCodeGen a (<*>) :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b liftA2 :: (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c (*>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b (<*) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a
MonadIO SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods liftIO :: IO a -> SBVCodeGen a
MonadSymbolic SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods symbolicEnv :: SBVCodeGen State Source #
MonadState CgState SBVCodeGen Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods get :: SBVCodeGen CgState put :: CgState -> SBVCodeGen () state :: (CgState -> (a, CgState)) -> SBVCodeGen a

cgSym :: Symbolic a -> SBVCodeGen a Source #

Reach into symbolic monad from code-generation

## Setting code-generation options

cgPerformRTCs :: Bool -> SBVCodeGen () Source #

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: `False`.

cgSetDriverValues :: [Integer] -> SBVCodeGen () Source #

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

cgGenerateDriver :: Bool -> SBVCodeGen () Source #

Should we generate a driver program? Default: `True`. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See `compileToCLib`.)

cgGenerateMakefile :: Bool -> SBVCodeGen () Source #

Should we generate a Makefile? Default: `True`.

cgOverwriteFiles :: Bool -> SBVCodeGen () Source #

If passed `True`, then we will not ask the user if we're overwriting files as we generate the C code. Otherwise, we'll prompt.

cgShowU8UsingHex :: Bool -> SBVCodeGen () Source #

If passed `True`, then we will show 'SWord 8' type in hex. Otherwise we'll show it in decimal. All signed types are shown decimal, and all unsigned larger types are shown hexadecimal otherwise.

## Designating inputs

cgInput :: SymVal a => String -> SBVCodeGen (SBV a) Source #

Creates an atomic input in the generated code.

cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a] Source #

Creates an array input in the generated code.

## Designating outputs

cgOutput :: String -> SBV a -> SBVCodeGen () Source #

Creates an atomic output in the generated code.

cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen () Source #

Creates an array output in the generated code.

## Designating return values

cgReturn :: SBV a -> SBVCodeGen () Source #

Creates a returned (unnamed) value in the generated code.

cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen () Source #

Creates a returned (unnamed) array value in the generated code.

## Code generation with uninterpreted functions

cgAddPrototype :: [String] -> SBVCodeGen () Source #

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

cgAddDecl :: [String] -> SBVCodeGen () Source #

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

cgAddLDFlags :: [String] -> SBVCodeGen () Source #

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

cgIgnoreSAssert :: Bool -> SBVCodeGen () Source #

Ignore assertions (those generated by `sAssert` calls) in the generated C code

## Code generation with `SInteger` and `SReal` types

The types `SInteger` and `SReal` are unbounded quantities that have no direct counterparts in the C language. Therefore, it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to overflow/underflows for `SInteger`, and rounding for `SReal`, so there is an implicit loss of precision.

If the user does not specify these mappings, then SBV will refuse to compile programs that involve these types.

cgIntegerSize :: Int -> SBVCodeGen () Source #

Sets number of bits to be used for representing the `SInteger` type in the generated C code. The argument must be one of `8`, `16`, `32`, or `64`. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

cgSRealType :: CgSRealType -> SBVCodeGen () Source #

Sets the C type to be used for representing the `SReal` type in the generated C code. The setting can be one of C's `"float"`, `"double"`, or `"long double"`, types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

data CgSRealType Source #

Possible mappings for the `SReal` type when translated to C. Used in conjunction with the function `cgSRealType`. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

CgFloat

    float

CgDouble

    double

CgLongDouble

    long double

#### Instances

Instances details

Eq CgSRealType Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods (==) :: CgSRealType -> CgSRealType -> Bool (/=) :: CgSRealType -> CgSRealType -> Bool
Show CgSRealType Source # |
Instance details Defined in Data.SBV.Compilers.CodeGen Methods showsPrec :: Int -> CgSRealType -> ShowS show :: CgSRealType -> String showList :: [CgSRealType] -> ShowS

## Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen a -> IO a Source #

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

- The first argument is the directory name under which the files will be saved. To save files in the current directory pass ``Just` "."`. Use `Nothing` for printing to stdout.
- The second argument is the name of the C function to generate.
- The final argument is the function to be compiled.

Compilation will also generate a `Makefile`, a header file, and a driver (test) program, etc. As a result, we return whatever the code-gen function returns. Most uses should simply have `()` as the return type here, but the value can be useful if you want to chain the result of one compilation act to the next.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen a)] -> IO [a] Source #

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

- The first argument is the directory name under which the files will be saved. To save files in the current directory pass ``Just` "."`. Use `Nothing` for printing to stdout.
- The second argument is the name of the archive to generate.
- The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of `compileToC`, except in a list.