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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Tools.CodeGen

Contents

Description

Code-generation from SBV programs.

Synopsis

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
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 #

fail :: String -> 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

MonadState CgState SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

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

Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO () 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.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO () 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.