Data.SBV.Tools.CodeGen

Code-generation from SBV programs.

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

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

Methods

(>>=) :: SBVCodeGen a -> (a -> SBVCodeGen b) -> SBVCodeGen b

(>>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b

return :: a -> SBVCodeGen a

fail :: String -> SBVCodeGen a

Functor SBVCodeGen

Methods

fmap :: (a -> b) -> SBVCodeGen a -> SBVCodeGen b

(<$) :: a -> SBVCodeGen b -> SBVCodeGen a

Applicative SBVCodeGen

Methods

pure :: a -> SBVCodeGen a

(<*>) :: SBVCodeGen (a -> b) -> SBVCodeGen a -> SBVCodeGen b

(*>) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b

(<*) :: SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen a

MonadIO SBVCodeGen

Methods

liftIO :: IO a -> SBVCodeGen a

MonadState CgState SBVCodeGen

Methods

get :: SBVCodeGen CgState

put :: CgState -> SBVCodeGen ()

state :: (CgState -> (a, CgState)) -> SBVCodeGen a

Setting code-generation options

cgPerformRTCs :: Bool -> SBVCodeGen ()

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

cgSetDriverValues :: [Integer] -> SBVCodeGen ()

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 ()

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 ()

Should we generate a Makefile? Default: True.

Designating inputs

cgInput :: SymWord a => String -> SBVCodeGen (SBV a)

Creates an atomic input in the generated code.

cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]

Creates an array input in the generated code.

Designating outputs

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

Creates an atomic output in the generated code.

cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()

Creates an array output in the generated code.

Designating return values

cgReturn :: SBV a -> SBVCodeGen ()

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

cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen ()

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

Code generation with uninterpreted functions

cgAddPrototype :: [String] -> SBVCodeGen ()

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

cgAddDecl :: [String] -> SBVCodeGen ()

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

cgAddLDFlags :: [String] -> SBVCodeGen ()

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

cgIgnoreSAssert :: Bool -> SBVCodeGen ()

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 ()

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 ()

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

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

Eq CgSRealType

Methods

(==) :: CgSRealType -> CgSRealType -> Bool

(/=) :: CgSRealType -> CgSRealType -> Bool

Show CgSRealType

Methods

showsPrec :: Int -> CgSRealType -> ShowS

show :: CgSRealType -> String

showList :: [CgSRealType] -> ShowS

Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()

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 ()

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.