Skip to content

Commit

Permalink
SBV->C: Support sAssert calls
Browse files Browse the repository at this point in the history 
SBV’s sAssert calls turn into dynamic checks in the generated C code.
(If not desired use the cgIgnoreSAssert to turn it off.)
  • Loading branch information
@LeventErkok
LeventErkok committed Nov 8, 2015
1 parent 65a7c19 commit 9451f69
Show file tree
Hide file tree
Showing 6 changed files with 68 additions and 30 deletions.
5 changes: 4 additions & 1 deletion CHANGES.md
View file
Expand Up @@ -12,6 +12,9 @@
* Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert'
being safe to execute. Any vilations will be flagged.

* SBV->C: Translate 'sAssert' calls to dynamic checks in the generated C code. If this is
not desired, use the 'cgIgnoreSAssert' function to turn it off.

* Add 'isSafe': Which converts a 'SafeResult' to a 'Bool', when we are only interested
in a boolean result.

Expand Down Expand Up @@ -932,7 +935,7 @@ uninterpreted.
can now specify the corresponding C code and SBV will simply
call the "native" functions instead of generating it. This
enables interfacing with other C programs. See the functions:
cgAddPrototype, cgAddDecl, and cgAddLDFlags.
cgAddPrototype, cgAddDecl, cgAddLDFlags

Examples:

Expand Down
2 changes: 1 addition & 1 deletion Data/SBV.hs
View file
Expand Up @@ -267,7 +267,7 @@ module Data.SBV (
, cgReturn, cgReturnArr

-- ** Code generation with uninterpreted functions
, cgAddPrototype, cgAddDecl, cgAddLDFlags
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert

-- ** Code generation with 'SInteger' and 'SReal' types
-- $unboundedCGen
Expand Down
45 changes: 34 additions & 11 deletions Data/SBV/Compilers/C.hs
View file
Expand Up @@ -27,6 +27,9 @@ import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.PrettyNum (shex, showCFloat, showCDouble)
import Data.SBV.Compilers.CodeGen

import GHC.Stack
import GHC.SrcLoc

---------------------------------------------------------------------------
-- * API
---------------------------------------------------------------------------
Expand Down Expand Up @@ -270,6 +273,8 @@ genHeader (ik, rk) fn sigs protos =
$$ text "#ifndef" <+> tag
$$ text "#define" <+> tag
$$ text ""
$$ text "#include <stdio.h>"
$$ text "#include <stdlib.h>"
$$ text "#include <inttypes.h>"
$$ text "#include <stdint.h>"
$$ text "#include <stdbool.h>"
Expand Down Expand Up @@ -399,7 +404,7 @@ genDriver cfg randVals fn inps outs mbRet = [pre, header, body, post]

-- | Generate the C program
genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]
genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs _ _) inVars outVars mbRet extDecls
genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs origAsserts _) inVars outVars mbRet extDecls
| isNothing (cgInteger cfg) && KUnbounded `Set.member` kindInfo
= error $ "SBV->C: Unbounded integers are not supported by the C compiler."
++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."
Expand All @@ -416,7 +421,9 @@ genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (S
= error "SBV->C: Cannot compile functions with existentially quantified variables."
| True
= [pre, header, post]
where usorts = [s | KUserSort s _ <- Set.toList kindInfo, s /= "RoundingMode"] -- No support for any sorts other than RoundingMode!
where asserts | cgIgnoreAsserts cfg = []
| True = origAsserts
usorts = [s | KUserSort s _ <- Set.toList kindInfo, s /= "RoundingMode"] -- No support for any sorts other than RoundingMode!
pre = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */"
$$ text ""
header = text "#include" <+> doubleQuotes (nm <> text ".h")
Expand All @@ -427,7 +434,7 @@ genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (S
$$ text "{"
$$ text ""
$$ nest 2 ( vcat (concatMap (genIO True . (\v -> (isAlive v, v))) inVars)
$$ vcat (merge (map genTbl tbls) (map genAsgn assignments))
$$ vcat (merge (map genTbl tbls) (map genAsgn assignments) (map genAssert asserts))
$$ sepIf (not (null assignments) || not (null tbls))
$$ vcat (concatMap (genIO False) (zip (repeat True) outVars))
$$ maybe empty mkRet mbRet
Expand Down Expand Up @@ -486,14 +493,30 @@ genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (S
genAsgn :: (SW, SBVExpr) -> (Int, Doc)
genAsgn (sw, n) = (getNodeId sw, ppExpr cfg consts n (declSW typeWidth sw) (declSWNoConst typeWidth sw) <> semi)

-- merge tables intermixed with assignments, paying attention to putting tables as
-- early as possible.. Note that the assignment list (second argument) is sorted on its order
merge :: [(Int, Doc)] -> [(Int, Doc)] -> [Doc]
merge [] as = map snd as
merge ts [] = map snd ts
merge ts@((i, t):trest) as@((i', a):arest)
| i < i' = t : merge trest as
| True = a : merge ts arest
-- merge tables intermixed with assignments and assertions, paying attention to putting tables as
-- early as possible and tables right after.. Note that the assignment list (second argument) is sorted on its order
merge :: [(Int, Doc)] -> [(Int, Doc)] -> [(Int, Doc)] -> [Doc]
merge tables asgnments asrts = map snd $ merge2 asrts (merge2 tables asgnments)
where merge2 [] as = as
merge2 ts [] = ts
merge2 ts@((i, t):trest) as@((i', a):arest)
| i < i' = (i, t) : merge2 trest as
| True = (i', a) : merge2 ts arest
genAssert (msg, cs, sw) = (getNodeId sw, doc)
where doc = text "/* ASSERTION:" <+> text msg
$$ maybe empty (vcat . map text) (locInfo (getCallStack `fmap` cs))
$$ text " */"
$$ text "if" <> parens (showSW cfg consts sw)
$$ text "{"
$+$ nest 2 (vcat [errOut, text "exit(-1);"])
$$ text "}"
$$ text ""
errOut = text $ "fprintf(stderr, \"%s:%d:ASSERTION FAILED: " ++ msg ++ "\\n\", __FILE__, __LINE__);"
locInfo (Just ps) = let loc (f, sl) = concat [srcLocFile sl, ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f ]
in case map loc ps of
[] -> Nothing
(f:rs) -> Just $ (" * SOURCE : " ++ f) : map (" * " ++) rs
locInfo _ = Nothing

handleIEEE :: FPOp -> [(SW, CW)] -> [(SW, Doc)] -> Doc -> Doc
handleIEEE w consts as var = cvt w
Expand Down
40 changes: 26 additions & 14 deletions Data/SBV/Compilers/CodeGen.hs
View file
Expand Up @@ -38,17 +38,25 @@ class CgTarget a where

-- | Options for code-generation.
data CgConfig = CgConfig {
cgRTC :: Bool -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.
, cgInteger :: Maybe Int -- ^ Bit-size to use for representing SInteger (if any)
, cgReal :: Maybe CgSRealType -- ^ Type to use for representing SReal (if any)
, cgDriverVals :: [Integer] -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
, cgGenDriver :: Bool -- ^ If 'True', will generate a driver program
, cgGenMakefile :: Bool -- ^ If 'True', will generate a makefile
cgRTC :: Bool -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.
, cgInteger :: Maybe Int -- ^ Bit-size to use for representing SInteger (if any)
, cgReal :: Maybe CgSRealType -- ^ Type to use for representing SReal (if any)
, cgDriverVals :: [Integer] -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
, cgGenDriver :: Bool -- ^ If 'True', will generate a driver program
, cgGenMakefile :: Bool -- ^ If 'True', will generate a makefile
, cgIgnoreAsserts :: Bool -- ^ If 'True', will ignore 'sAssert' calls
}

-- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.
defaultCgConfig :: CgConfig
defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgReal = Nothing, cgDriverVals = [], cgGenDriver = True, cgGenMakefile = True }
defaultCgConfig = CgConfig { cgRTC = False
, cgInteger = Nothing
, cgReal = Nothing
, cgDriverVals = []
, cgGenDriver = True
, cgGenMakefile = True
, cgIgnoreAsserts = False
}

-- | Abstraction of target language values
data CgVal = CgAtomic SW
Expand All @@ -68,13 +76,13 @@ data CgState = CgState {
-- | Initial configuration for code-generation
initCgState :: CgState
initCgState = CgState {
cgInputs = []
, cgOutputs = []
, cgReturns = []
, cgPrototypes = []
, cgDecls = []
, cgLDFlags = []
, cgFinalConfig = defaultCgConfig
cgInputs = []
, cgOutputs = []
, cgReturns = []
, cgPrototypes = []
, cgDecls = []
, cgLDFlags = []
, cgFinalConfig = defaultCgConfig
}

-- | The code-generation monad. Allows for precise layout of input values
Expand Down Expand Up @@ -142,6 +150,10 @@ cgGenerateMakefile b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgG
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
cgSetDriverValues vs = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })

-- | Ignore assertions (those generated by 'sAssert' calls) in the generated C code
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
cgIgnoreSAssert b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgIgnoreAsserts = b } })

-- | Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
cgAddPrototype :: [String] -> SBVCodeGen ()
cgAddPrototype ss = modify (\s -> let old = cgPrototypes s
Expand Down
4 changes: 2 additions & 2 deletions Data/SBV/Dynamic.hs
View file
Expand Up @@ -98,7 +98,7 @@ module Data.SBV.Dynamic
, svCgReturn, svCgReturnArr

-- ** Code generation with uninterpreted functions
, cgAddPrototype, cgAddDecl, cgAddLDFlags
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert

-- ** Code generation with 'SInteger' and 'SReal' types
, cgIntegerSize, cgSRealType, CgSRealType(..)
Expand All @@ -120,7 +120,7 @@ import Data.SBV.Compilers.CodeGen
, svCgOutput, svCgOutputArr
, svCgReturn, svCgReturnArr
, cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
, cgAddPrototype, cgAddDecl, cgAddLDFlags
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert
, cgIntegerSize, cgSRealType, CgSRealType(..)
)
import Data.SBV.Compilers.C (compileToC, compileToCLib)
Expand Down
2 changes: 1 addition & 1 deletion SBVUnitTest/SBVUnitTestBuildTime.hs
View file
Expand Up @@ -2,4 +2,4 @@
module SBVUnitTestBuildTime (buildTime) where

buildTime :: String
buildTime = "Sat Nov 7 18:21:16 PST 2015"
buildTime = "Sun Nov 8 01:01:59 PST 2015"

0 comments on commit 9451f69

Please sign in to comment.