| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.CodeGen
Contents
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
- compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()
- compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
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
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
| Eq CgSRealType Source # | |
Defined in Data.SBV.Compilers.CodeGen | |
| Show CgSRealType Source # | |
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 () -> 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"."Nothingfor 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"."Nothingfor 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.