----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Compilers.C -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- Compilation of symbolic programs to C ----------------------------------------------------------------------------- {-# LANGUAGE PatternGuards #-} module Data.SBV.Compilers.C(compileToC, compileToCLib, compileToC', compileToCLib') where import Control.DeepSeq (rnf) import Data.Char (isSpace) import Data.List (nub, intercalate) import Data.Maybe (isJust, isNothing, fromJust) import qualified Data.Foldable as F (toList) import qualified Data.Set as Set (member, union, unions, empty, toList, singleton, fromList) import System.FilePath (takeBaseName, replaceExtension) import System.Random import Text.PrettyPrint.HughesPJ import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum (shex, showCFloat, showCDouble) import Data.SBV.Compilers.CodeGen import GHC.Stack.Compat import GHC.SrcLoc.Compat --------------------------------------------------------------------------- -- * API --------------------------------------------------------------------------- -- | 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. compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO () compileToC mbDirName nm f = compileToC' nm f >>= renderCgPgmBundle mbDirName -- | Lower level version of 'compileToC', producing a 'CgPgmBundle' compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle compileToC' nm f = do rands <- randoms `fmap` newStdGen codeGen SBVToC (defaultCgConfig { cgDriverVals = rands }) nm f -- | 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. compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO () compileToCLib mbDirName libName comps = compileToCLib' libName comps >>= renderCgPgmBundle mbDirName -- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle' compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle compileToCLib' libName comps = mergeToLib libName `fmap` mapM (uncurry compileToC') comps --------------------------------------------------------------------------- -- * Implementation --------------------------------------------------------------------------- -- token for the target language data SBVToC = SBVToC instance CgTarget SBVToC where targetName _ = "C" translate _ = cgen -- Unexpected input, or things we will probably never support die :: String -> a die msg = error $ "SBV->C: Unexpected: " ++ msg -- Unsupported features, or features TBD tbd :: String -> a tbd msg = error $ "SBV->C: Not yet supported: " ++ msg cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle cgen cfg nm st sbvProg -- we rnf the main pg and the sig to make sure any exceptions in type conversion pop-out early enough -- this is purely cosmetic, of course.. = rnf (render sig) `seq` rnf (render (vcat body)) `seq` result where result = CgPgmBundle bundleKind $ filt [ ("Makefile", (CgMakefile flags, [genMake (cgGenDriver cfg) nm nmd flags])) , (nm ++ ".h", (CgHeader [sig], [genHeader bundleKind nm [sig] extProtos])) , (nmd ++ ".c", (CgDriver, genDriver cfg randVals nm ins outs mbRet)) , (nm ++ ".c", (CgSource, body)) ] body = genCProg cfg nm sig sbvProg ins outs mbRet extDecls bundleKind = (cgInteger cfg, cgReal cfg) randVals = cgDriverVals cfg filt xs = [c | c@(_, (k, _)) <- xs, need k] where need k | isCgDriver k = cgGenDriver cfg | isCgMakefile k = cgGenMakefile cfg | True = True nmd = nm ++ "_driver" sig = pprCFunHeader nm ins outs mbRet ins = cgInputs st outs = cgOutputs st mbRet = case cgReturns st of [] -> Nothing [CgAtomic o] -> Just o [CgArray _] -> tbd "Non-atomic return values" _ -> tbd "Multiple return values" extProtos = case cgPrototypes st of [] -> empty xs -> vcat $ text "/* User given prototypes: */" : map text xs extDecls = case cgDecls st of [] -> empty xs -> vcat $ text "/* User given declarations: */" : map text xs flags = cgLDFlags st -- | Pretty print a functions type. If there is only one output, we compile it -- as a function that returns that value. Otherwise, we compile it as a void function -- that takes return values as pointers to be updated. pprCFunHeader :: String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc pprCFunHeader fn ins outs mbRet = retType <+> text fn <> parens (fsep (punctuate comma (map mkParam ins ++ map mkPParam outs))) where retType = case mbRet of Nothing -> text "void" Just sw -> pprCWord False sw mkParam, mkPParam :: (String, CgVal) -> Doc mkParam (n, CgAtomic sw) = pprCWord True sw <+> text n mkParam (_, CgArray []) = die "mkParam: CgArray with no elements!" mkParam (n, CgArray (sw:_)) = pprCWord True sw <+> text "*" <> text n mkPParam (n, CgAtomic sw) = pprCWord False sw <+> text "*" <> text n mkPParam (_, CgArray []) = die "mPkParam: CgArray with no elements!" mkPParam (n, CgArray (sw:_)) = pprCWord False sw <+> text "*" <> text n -- | Renders as "const SWord8 s0", etc. the first parameter is the width of the typefield declSW :: Int -> SW -> Doc declSW w sw = text "const" <+> pad (showCType sw) <+> text (show sw) where pad s = text $ s ++ replicate (w - length s) ' ' -- | Return the proper declaration and the result as a pair. No consts declSWNoConst :: Int -> SW -> (Doc, Doc) declSWNoConst w sw = (text " " <+> pad (showCType sw), text (show sw)) where pad s = text $ s ++ replicate (w - length s) ' ' -- | Renders as "s0", etc, or the corresponding constant showSW :: CgConfig -> [(SW, CW)] -> SW -> Doc showSW cfg consts sw | sw == falseSW = text "false" | sw == trueSW = text "true" | Just cw <- sw `lookup` consts = mkConst cfg cw | True = text $ show sw -- | Words as it would map to a C word pprCWord :: HasKind a => Bool -> a -> Doc pprCWord cnst v = (if cnst then text "const" else empty) <+> text (showCType v) -- | Almost a "show", but map "SWord1" to "SBool" -- which is used for extracting one-bit words. showCType :: HasKind a => a -> String showCType i = case kindOf i of KBounded False 1 -> "SBool" k -> show k -- | The printf specifier for the type specifier :: CgConfig -> SW -> Doc specifier cfg sw = case kindOf sw of KBool -> spec (False, 1) KBounded b i -> spec (b, i) KUnbounded -> spec (True, fromJust (cgInteger cfg)) KReal -> specF (fromJust (cgReal cfg)) KFloat -> specF CgFloat KDouble -> specF CgDouble KUserSort s _ -> die $ "uninterpreted sort: " ++ s where spec :: (Bool, Int) -> Doc spec (False, 1) = text "%d" spec (False, 8) = text "%\"PRIu8\"" spec (True, 8) = text "%\"PRId8\"" spec (False, 16) = text "0x%04\"PRIx16\"U" spec (True, 16) = text "%\"PRId16\"" spec (False, 32) = text "0x%08\"PRIx32\"UL" spec (True, 32) = text "%\"PRId32\"L" spec (False, 64) = text "0x%016\"PRIx64\"ULL" spec (True, 64) = text "%\"PRId64\"LL" spec (s, sz) = die $ "Format specifier at type " ++ (if s then "SInt" else "SWord") ++ show sz specF :: CgSRealType -> Doc specF CgFloat = text "%.6g" -- float.h: __FLT_DIG__ specF CgDouble = text "%.15g" -- float.h: __DBL_DIG__ specF CgLongDouble = text "%Lf" -- | Make a constant value of the given type. We don't check for out of bounds here, as it should not be needed. -- There are many options here, using binary, decimal, etc. We simply use decimal for values 8-bits or less, -- and hex otherwise. mkConst :: CgConfig -> CW -> Doc mkConst cfg (CW KReal (CWAlgReal (AlgRational _ r))) = double (fromRational r :: Double) <> sRealSuffix (fromJust (cgReal cfg)) where sRealSuffix CgFloat = text "F" sRealSuffix CgDouble = empty sRealSuffix CgLongDouble = text "L" mkConst cfg (CW KUnbounded (CWInteger i)) = showSizedConst i (True, fromJust (cgInteger cfg)) mkConst _ (CW (KBounded sg sz) (CWInteger i)) = showSizedConst i (sg, sz) mkConst _ (CW KBool (CWInteger i)) = showSizedConst i (False, 1) mkConst _ (CW KFloat (CWFloat f)) = text $ showCFloat f mkConst _ (CW KDouble (CWDouble d)) = text $ showCDouble d mkConst _ cw = die $ "mkConst: " ++ show cw showSizedConst :: Integer -> (Bool, Int) -> Doc showSizedConst i (False, 1) = text (if i == 0 then "false" else "true") showSizedConst i (False, 8) = integer i showSizedConst i (True, 8) = integer i showSizedConst i t@(False, 16) = text (shex False True t i) <> text "U" showSizedConst i t@(True, 16) = text (shex False True t i) showSizedConst i t@(False, 32) = text (shex False True t i) <> text "UL" showSizedConst i t@(True, 32) = text (shex False True t i) <> text "L" showSizedConst i t@(False, 64) = text (shex False True t i) <> text "ULL" showSizedConst i t@(True, 64) = text (shex False True t i) <> text "LL" showSizedConst i (True, 1) = die $ "Signed 1-bit value " ++ show i showSizedConst i (s, sz) = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz -- | Generate a makefile. The first argument is True if we have a driver. genMake :: Bool -> String -> String -> [String] -> Doc genMake ifdr fn dn ldFlags = foldr1 ($$) [l | (True, l) <- lns] where ifld = not (null ldFlags) ld | ifld = text "${LDFLAGS}" | True = empty lns = [ (True, text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!") , (True, text "") , (True, text "# include any user-defined .mk file in the current directory.") , (True, text "-include *.mk") , (True, text "") , (True, text "CC?=gcc") , (True, text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer") , (ifld, text "LDFLAGS?=" <> text (unwords ldFlags)) , (True, text "") , (ifdr, text "all:" <+> nmd) , (ifdr, text "") , (True, nmo <> text (": " ++ ppSameLine (hsep [nmc, nmh]))) , (True, text "\t${CC} ${CCFLAGS}" <+> text "-c $< -o $@") , (True, text "") , (ifdr, nmdo <> text ":" <+> nmdc) , (ifdr, text "\t${CC} ${CCFLAGS}" <+> text "-c $< -o $@") , (ifdr, text "") , (ifdr, nmd <> text (": " ++ ppSameLine (hsep [nmo, nmdo]))) , (ifdr, text "\t${CC} ${CCFLAGS}" <+> text "$^ -o $@" <+> ld) , (ifdr, text "") , (True, text "clean:") , (True, text "\trm -f *.o") , (True, text "") , (ifdr, text "veryclean: clean") , (ifdr, text "\trm -f" <+> nmd) , (ifdr, text "") ] nm = text fn nmd = text dn nmh = nm <> text ".h" nmc = nm <> text ".c" nmo = nm <> text ".o" nmdc = nmd <> text ".c" nmdo = nmd <> text ".o" -- | Generate the header genHeader :: (Maybe Int, Maybe CgSRealType) -> String -> [Doc] -> Doc -> Doc genHeader (ik, rk) fn sigs protos = text "/* Header file for" <+> nm <> text ". Automatically generated by SBV. Do not edit! */" $$ text "" $$ text "#ifndef" <+> tag $$ text "#define" <+> tag $$ text "" $$ text "#include " $$ text "#include " $$ text "#include " $$ text "#include " $$ text "#include " $$ text "#include " $$ text "#include " $$ text "" $$ text "/* The boolean type */" $$ text "typedef bool SBool;" $$ text "" $$ text "/* The float type */" $$ text "typedef float SFloat;" $$ text "" $$ text "/* The double type */" $$ text "typedef double SDouble;" $$ text "" $$ text "/* Unsigned bit-vectors */" $$ text "typedef uint8_t SWord8 ;" $$ text "typedef uint16_t SWord16;" $$ text "typedef uint32_t SWord32;" $$ text "typedef uint64_t SWord64;" $$ text "" $$ text "/* Signed bit-vectors */" $$ text "typedef int8_t SInt8 ;" $$ text "typedef int16_t SInt16;" $$ text "typedef int32_t SInt32;" $$ text "typedef int64_t SInt64;" $$ text "" $$ imapping $$ rmapping $$ text ("/* Entry point prototype" ++ plu ++ ": */") $$ vcat (map (<> semi) sigs) $$ text "" $$ protos $$ text "#endif /*" <+> tag <+> text "*/" $$ text "" where nm = text fn tag = text "__" <> nm <> text "__HEADER_INCLUDED__" plu = if length sigs /= 1 then "s" else "" imapping = case ik of Nothing -> empty Just i -> text "/* User requested mapping for SInteger. */" $$ text "/* NB. Loss of precision: Target type is subject to modular arithmetic. */" $$ text ("typedef SInt" ++ show i ++ " SInteger;") $$ text "" rmapping = case rk of Nothing -> empty Just t -> text "/* User requested mapping for SReal. */" $$ text "/* NB. Loss of precision: Target type is subject to rounding. */" $$ text ("typedef " ++ show t ++ " SReal;") $$ text "" sepIf :: Bool -> Doc sepIf b = if b then text "" else empty -- | Generate an example driver program genDriver :: CgConfig -> [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc] genDriver cfg randVals fn inps outs mbRet = [pre, header, body, post] where pre = text "/* Example driver program for" <+> nm <> text ". */" $$ text "/* Automatically generated by SBV. Edit as you see fit! */" $$ text "" $$ text "#include " header = text "#include" <+> doubleQuotes (nm <> text ".h") $$ text "" $$ text "int main(void)" $$ text "{" body = text "" $$ nest 2 ( vcat (map mkInp pairedInputs) $$ vcat (map mkOut outs) $$ sepIf (not (null [() | (_, _, CgArray{}) <- pairedInputs]) || not (null outs)) $$ call $$ text "" $$ (case mbRet of Just sw -> text "printf" <> parens (printQuotes (fcall <+> text "=" <+> specifier cfg sw <> text "\\n") <> comma <+> resultVar) <> semi Nothing -> text "printf" <> parens (printQuotes (fcall <+> text "->\\n")) <> semi) $$ vcat (map display outs) ) post = text "" $+$ nest 2 (text "return 0" <> semi) $$ text "}" $$ text "" nm = text fn pairedInputs = matchRands (map abs randVals) inps matchRands _ [] = [] matchRands [] _ = die "Run out of driver values!" matchRands (r:rs) ((n, CgAtomic sw) : cs) = ([mkRVal sw r], n, CgAtomic sw) : matchRands rs cs matchRands _ ((n, CgArray []) : _ ) = die $ "Unsupported empty array input " ++ show n matchRands rs ((n, a@(CgArray sws@(sw:_))) : cs) | length frs /= l = die "Run out of driver values!" | True = (map (mkRVal sw) frs, n, a) : matchRands srs cs where l = length sws (frs, srs) = splitAt l rs mkRVal sw r = mkConst cfg $ mkConstCW (kindOf sw) r mkInp (_, _, CgAtomic{}) = empty -- constant, no need to declare mkInp (_, n, CgArray []) = die $ "Unsupported empty array value for " ++ show n mkInp (vs, n, CgArray sws@(sw:_)) = pprCWord True sw <+> text n <> brackets (int (length sws)) <+> text "= {" $$ nest 4 (fsep (punctuate comma (align vs))) $$ text "};" $$ text "" $$ text "printf" <> parens (printQuotes (text "Contents of input array" <+> text n <> text ":\\n")) <> semi $$ display (n, CgArray sws) $$ text "" mkOut (v, CgAtomic sw) = pprCWord False sw <+> text v <> semi mkOut (v, CgArray []) = die $ "Unsupported empty array value for " ++ show v mkOut (v, CgArray sws@(sw:_)) = pprCWord False sw <+> text v <> brackets (int (length sws)) <> semi resultVar = text "__result" call = case mbRet of Nothing -> fcall <> semi Just sw -> pprCWord True sw <+> resultVar <+> text "=" <+> fcall <> semi fcall = nm <> parens (fsep (punctuate comma (map mkCVal pairedInputs ++ map mkOVal outs))) mkCVal ([v], _, CgAtomic{}) = v mkCVal (vs, n, CgAtomic{}) = die $ "Unexpected driver value computed for " ++ show n ++ render (hcat vs) mkCVal (_, n, CgArray{}) = text n mkOVal (n, CgAtomic{}) = text "&" <> text n mkOVal (n, CgArray{}) = text n display (n, CgAtomic sw) = text "printf" <> parens (printQuotes (text " " <+> text n <+> text "=" <+> specifier cfg sw <> text "\\n") <> comma <+> text n) <> semi display (n, CgArray []) = die $ "Unsupported empty array value for " ++ show n display (n, CgArray sws@(sw:_)) = text "int" <+> nctr <> semi $$ text "for(" <> nctr <+> text "= 0;" <+> nctr <+> text "<" <+> int (length sws) <+> text "; ++" <> nctr <> text ")" $$ nest 2 (text "printf" <> parens (printQuotes (text " " <+> entrySpec <+> text "=" <+> spec <> text "\\n") <> comma <+> nctr <+> comma <> entry) <> semi) where nctr = text n <> text "_ctr" entry = text n <> text "[" <> nctr <> text "]" entrySpec = text n <> text "[%d]" spec = specifier cfg sw -- | 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 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." | isNothing (cgReal cfg) && KReal `Set.member` kindInfo = error $ "SBV->C: SReal values are not supported by the C compiler." ++ "\nUse 'cgSRealType' to specify a custom type for SReal representation." | not (null usorts) = error $ "SBV->C: Cannot compile functions with uninterpreted sorts: " ++ intercalate ", " usorts | not (null cstrs) = tbd "Explicit constraints" | not (null arrs) = tbd "User specified arrays" | needsExistentials (map fst ins) = error "SBV->C: Cannot compile functions with existentially quantified variables." | True = [pre, header, post] 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") post = text "" $$ vcat (map codeSeg cgs) $$ extDecls $$ proto $$ text "{" $$ text "" $$ nest 2 ( vcat (concatMap (genIO True . (\v -> (isAlive v, v))) inVars) $$ 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 ) $$ text "}" $$ text "" nm = text fn assignments = F.toList asgns codeSeg (fnm, ls) = text "/* User specified custom code for" <+> doubleQuotes (text fnm) <+> text "*/" $$ vcat (map text ls) $$ text "" typeWidth = getMax 0 $ [len (kindOf s) | (s, _) <- assignments] ++ [len (kindOf s) | (_, (s, _)) <- ins] where len (KReal{}) = 5 len (KFloat{}) = 6 -- SFloat len (KDouble{}) = 7 -- SDouble len (KUnbounded{}) = 8 len KBool = 5 -- SBool len (KBounded False n) = 5 + length (show n) -- SWordN len (KBounded True n) = 4 + length (show n) -- SIntN len (KUserSort s _) = die $ "Uninterpreted sort: " ++ s getMax 8 _ = 8 -- 8 is the max we can get with SInteger, so don't bother looking any further getMax m [] = m getMax m (x:xs) = getMax (m `max` x) xs consts = (falseSW, falseCW) : (trueSW, trueCW) : preConsts isConst s = isJust (lookup s consts) -- TODO: The following is brittle. We should really have a function elsewhere -- that walks the SBVExprs and collects the SWs together. usedVariables = Set.unions (retSWs : map usedCgVal outVars ++ map usedAsgn assignments) where retSWs = maybe Set.empty Set.singleton mbRet usedCgVal (_, CgAtomic s) = Set.singleton s usedCgVal (_, CgArray ss) = Set.fromList ss usedAsgn (_, SBVApp o ss) = Set.union (opSWs o) (Set.fromList ss) opSWs (LkUp _ a b) = Set.fromList [a, b] opSWs (IEEEFP (FP_Cast _ _ s)) = Set.singleton s opSWs _ = Set.empty isAlive :: (String, CgVal) -> Bool isAlive (_, CgAtomic sw) = sw `Set.member` usedVariables isAlive (_, _) = True genIO :: Bool -> (Bool, (String, CgVal)) -> [Doc] genIO True (alive, (cNm, CgAtomic sw)) = [declSW typeWidth sw <+> text "=" <+> text cNm <> semi | alive] genIO False (alive, (cNm, CgAtomic sw)) = [text "*" <> text cNm <+> text "=" <+> showSW cfg consts sw <> semi | alive] genIO isInp (_, (cNm, CgArray sws)) = zipWith genElt sws [(0::Int)..] where genElt sw i | isInp = declSW typeWidth sw <+> text "=" <+> text entry <> semi | True = text entry <+> text "=" <+> showSW cfg consts sw <> semi where entry = cNm ++ "[" ++ show i ++ "]" mkRet sw = text "return" <+> showSW cfg consts sw <> semi genTbl :: ((Int, Kind, Kind), [SW]) -> (Int, Doc) genTbl ((i, _, k), elts) = (location, static <+> text "const" <+> text (show k) <+> text ("table" ++ show i) <> text "[] = {" $$ nest 4 (fsep (punctuate comma (align (map (showSW cfg consts) elts)))) $$ text "};") where static = if location == -1 then text "static" else empty location = maximum (-1 : map getNodeId elts) getNodeId s@(SW _ (NodeId n)) | isConst s = -1 | True = n 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 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 where same f = (f, f) named fnm dnm f = (f fnm, f dnm) castToUnsigned f to = parens (text "!isnan" <> parens a <+> text "&&" <+> text "signbit" <> parens a) <+> text "?" <+> cvt1 <+> text ":" <+> cvt2 where [a] = map snd fpArgs absA = text (if f == KFloat then "fabsf" else "fabs") <> parens a cvt1 = parens (text "-" <+> parens (parens (text (show to)) <+> absA)) cvt2 = parens (parens (text (show to)) <+> a) cvt (FP_Cast f to m) = case checkRM (m `lookup` consts) of Nothing -> if f `elem` [KFloat, KDouble] && not (hasSign to) then castToUnsigned f to else cast $ \[a] -> parens (text (show to)) <+> a Just (Left msg) -> die msg Just (Right msg) -> tbd msg cvt (FP_Reinterpret f t) = case (f, t) of (KBounded False 32, KFloat) -> cast $ cpy "sizeof(SFloat)" (KBounded False 64, KDouble) -> cast $ cpy "sizeof(SDouble)" (KFloat, KBounded False 32) -> cast $ cpy "sizeof(SWord32)" (KDouble, KBounded False 64) -> cast $ cpy "sizeof(SWord64)" _ -> die $ "Reinterpretation from : " ++ show f ++ " to " ++ show t where cpy sz = \[a] -> let alhs = text "&" <> var arhs = text "&" <> a in text "memcpy" <> parens (fsep (punctuate comma [alhs, arhs, text sz])) cvt FP_Abs = dispatch $ named "fabsf" "fabs" $ \nm _ [a] -> text nm <> parens a cvt FP_Neg = dispatch $ same $ \_ [a] -> text "-" <> a cvt FP_Add = dispatch $ same $ \_ [a, b] -> a <+> text "+" <+> b cvt FP_Sub = dispatch $ same $ \_ [a, b] -> a <+> text "-" <+> b cvt FP_Mul = dispatch $ same $ \_ [a, b] -> a <+> text "*" <+> b cvt FP_Div = dispatch $ same $ \_ [a, b] -> a <+> text "/" <+> b cvt FP_FMA = dispatch $ named "fmaf" "fma" $ \nm _ [a, b, c] -> text nm <> parens (fsep (punctuate comma [a, b, c])) cvt FP_Sqrt = dispatch $ named "sqrtf" "sqrt" $ \nm _ [a] -> text nm <> parens a cvt FP_Rem = dispatch $ named "fmodf" "fmod" $ \nm _ [a, b] -> text nm <> parens (fsep (punctuate comma [a, b])) cvt FP_RoundToIntegral = dispatch $ named "rintf" "rint" $ \nm _ [a] -> text nm <> parens a cvt FP_Min = dispatch $ named "fminf" "fmin" $ \nm k [a, b] -> wrapMinMax k a b (text nm <> parens (fsep (punctuate comma [a, b]))) cvt FP_Max = dispatch $ named "fmaxf" "fmax" $ \nm k [a, b] -> wrapMinMax k a b (text nm <> parens (fsep (punctuate comma [a, b]))) cvt FP_ObjEqual = let mkIte x y z = x <+> text "?" <+> y <+> text ":" <+> z chkNaN x = text "isnan" <> parens x signbit x = text "signbit" <> parens x eq x y = parens (x <+> text "==" <+> y) eqZero x = eq x (text "0") negZero x = parens (signbit x <+> text "&&" <+> eqZero x) in dispatch $ same $ \_ [a, b] -> mkIte (chkNaN a) (chkNaN b) (mkIte (negZero a) (negZero b) (mkIte (negZero b) (negZero a) (eq a b))) cvt FP_IsNormal = dispatch $ same $ \_ [a] -> text "isnormal" <> parens a cvt FP_IsSubnormal = dispatch $ same $ \_ [a] -> text "FP_SUBNORMAL == fpclassify" <> parens a cvt FP_IsZero = dispatch $ same $ \_ [a] -> text "FP_ZERO == fpclassify" <> parens a cvt FP_IsInfinite = dispatch $ same $ \_ [a] -> text "isinf" <> parens a cvt FP_IsNaN = dispatch $ same $ \_ [a] -> text "isnan" <> parens a cvt FP_IsNegative = dispatch $ same $ \_ [a] -> text "!isnan" <> parens a <+> text "&&" <+> text "signbit" <> parens a cvt FP_IsPositive = dispatch $ same $ \_ [a] -> text "!isnan" <> parens a <+> text "&&" <+> text "!signbit" <> parens a -- grab the rounding-mode, if present, and make sure it's RoundNearestTiesToEven. Otherwise skip. fpArgs = case as of [] -> [] ((m, _):args) -> case kindOf m of KUserSort "RoundingMode" _ -> case checkRM (m `lookup` consts) of Nothing -> args Just (Left msg) -> die msg Just (Right msg) -> tbd msg _ -> as -- Check that the RM is RoundNearestTiesToEven. -- If we start supporting other rounding-modes, this would be the point where we'd insert the rounding-mode set/reset code -- instead of merely returning OK or not checkRM (Just cv@(CW (KUserSort "RoundingMode" _) v)) = case v of CWUserSort (_, "RoundNearestTiesToEven") -> Nothing CWUserSort (_, s) -> Just (Right $ "handleIEEE: Unsupported rounding-mode: " ++ show s ++ " for: " ++ show w) _ -> Just (Left $ "handleIEEE: Unexpected value for rounding-mode: " ++ show cv ++ " for: " ++ show w) checkRM (Just cv) = Just (Left $ "handleIEEE: Expected rounding-mode, but got: " ++ show cv ++ " for: " ++ show w) checkRM Nothing = Just (Right $ "handleIEEE: Non-constant rounding-mode for: " ++ show w) pickOp _ [] = die $ "Cannot determine float/double kind for op: " ++ show w pickOp (fOp, dOp) args@((a,_):_) = case kindOf a of KFloat -> fOp KFloat (map snd args) KDouble -> dOp KDouble (map snd args) k -> die $ "handleIEEE: Expected double/float args, but got: " ++ show k ++ " for: " ++ show w dispatch (fOp, dOp) = pickOp (fOp, dOp) fpArgs cast f = f (map snd fpArgs) -- In SMT-Lib, fpMin/fpMax is underspecified when given +0/-0 as the two arguments. (In any order.) -- In C, the second argument is returned. (I think, might depend on the architecture, optimizations etc.). -- We'll translate it so that we deterministically return +0. -- There's really no good choice here. wrapMinMax k a b s = parens cond <+> text "?" <+> zero <+> text ":" <+> s where zero = text $ if k == KFloat then showCFloat 0 else showCDouble 0 cond = parens (text "FP_ZERO == fpclassify" <> parens a) -- a is zero <+> text "&&" <+> parens (text "FP_ZERO == fpclassify" <> parens b) -- b is zero <+> text "&&" <+> parens (text "signbit" <> parens a <+> text "!=" <+> text "signbit" <> parens b) -- a and b differ in sign ppExpr :: CgConfig -> [(SW, CW)] -> SBVExpr -> Doc -> (Doc, Doc) -> Doc ppExpr cfg consts (SBVApp op opArgs) lhs (typ, var) | doNotAssign op = typ <+> var <> semi <+> rhs | True = lhs <+> text "=" <+> rhs where doNotAssign (IEEEFP (FP_Reinterpret{})) = True -- generates a memcpy instead; no simple assignment doNotAssign _ = False -- generates simple assignment rhs = p op (map (showSW cfg consts) opArgs) rtc = cgRTC cfg cBinOps = [ (Plus, "+"), (Times, "*"), (Minus, "-") , (Equal, "=="), (NotEqual, "!="), (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") , (And, "&"), (Or, "|"), (XOr, "^") ] p :: Op -> [Doc] -> Doc p (ArrRead _) _ = tbd "User specified arrays (ArrRead)" p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)" p (Label s) [a] = a <+> text "/*" <+> text s <+> text "*/" p (IEEEFP w) as = handleIEEE w consts (zip opArgs as) var p (IntCast _ to) [a] = parens (text (show to)) <+> a p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) p (Extract i j) [a] = extract i j (head opArgs) a p Join [a, b] = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b)) p (Rol i) [a] = rotate True i a (head opArgs) p (Ror i) [a] = rotate False i a (head opArgs) p (Shl i) [a] = shift True i a (head opArgs) p (Shr i) [a] = shift False i a (head opArgs) p Not [a] = case kindOf (head opArgs) of -- be careful about booleans, bitwise complement is not correct for them! KBool -> text "!" <> a _ -> text "~" <> a p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c p (LkUp (t, k, _, len) ind def) [] | not rtc = lkUp -- ignore run-time-checks per user request | needsCheckL && needsCheckR = cndLkUp checkBoth | needsCheckL = cndLkUp checkLeft | needsCheckR = cndLkUp checkRight | True = lkUp where [index, defVal] = map (showSW cfg consts) [ind, def] lkUp = text "table" <> int t <> brackets (showSW cfg consts ind) cndLkUp cnd = cnd <+> text "?" <+> defVal <+> text ":" <+> lkUp checkLeft = index <+> text "< 0" checkRight = index <+> text ">=" <+> int len checkBoth = parens (checkLeft <+> text "||" <+> checkRight) canOverflow True sz = (2::Integer)^(sz-1)-1 >= fromIntegral len canOverflow False sz = (2::Integer)^sz -1 >= fromIntegral len (needsCheckL, needsCheckR) = case k of KBool -> (False, canOverflow False (1::Int)) KBounded sg sz -> (sg, canOverflow sg sz) KReal -> die "array index with real value" KFloat -> die "array index with float value" KDouble -> die "array index with double value" KUnbounded -> case cgInteger cfg of Nothing -> (True, True) -- won't matter, it'll be rejected later Just i -> (True, canOverflow True i) KUserSort s _ -> die $ "Uninterpreted sort: " ++ s -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior. -- Brief googling suggests C99 does indeed truncate toward 0, but other C compilers might differ. p Quot [a, b] = let k = kindOf (head opArgs) z = mkConst cfg $ mkConstCW k (0::Integer) in protectDiv0 k "/" z a b p Rem [a, b] = protectDiv0 (kindOf (head opArgs)) "%" a a b p UNeg [a] = parens (text "-" <+> a) p Abs [a] = let f = case kindOf (head opArgs) of KFloat -> text "fabsf" KDouble -> text "fabs" _ -> text "abs" in f <> parens a -- for And/Or, translate to boolean versions if on boolean kind p And [a, b] | kindOf (head opArgs) == KBool = a <+> text "&&" <+> b p Or [a, b] | kindOf (head opArgs) == KBool = a <+> text "||" <+> b p o [a, b] | Just co <- lookup o cBinOps = a <+> text co <+> b p o args = die $ "Received operator " ++ show o ++ " applied to " ++ show args -- Div0 needs to protect, but only when the arguments are not float/double. (Div by 0 for those are well defined to be Inf/NaN etc.) protectDiv0 k divOp def a b = case k of KFloat -> res KDouble -> res _ -> wrap where res = a <+> text divOp <+> b wrap = parens (b <+> text "== 0") <+> text "?" <+> def <+> text ":" <+> parens res shift toLeft i a s | i < 0 = shift (not toLeft) (-i) a s | i == 0 = a | True = case kindOf s of KBounded _ sz | i >= sz -> mkConst cfg $ mkConstCW (kindOf s) (0::Integer) KReal -> tbd $ "Shift for real quantity: " ++ show (toLeft, i, s) _ -> a <+> text cop <+> int i where cop | toLeft = "<<" | True = ">>" rotate toLeft i a s | i < 0 = rotate (not toLeft) (-i) a s | i == 0 = a | True = case kindOf s of KBounded True _ -> tbd $ "Rotation of signed quantities: " ++ show (toLeft, i, s) KBounded False sz | i >= sz -> rotate toLeft (i `mod` sz) a s KBounded False sz -> parens (a <+> text cop <+> int i) <+> text "|" <+> parens (a <+> text cop' <+> int (sz - i)) KUnbounded -> shift toLeft i a s -- For SInteger, rotate is the same as shift in Haskell _ -> tbd $ "Rotation for unbounded quantity: " ++ show (toLeft, i, s) where (cop, cop') | toLeft = ("<<", ">>") | True = (">>", "<<") -- TBD: below we only support the values for extract that are "easy" to implement. These should cover -- almost all instances actually generated by SBV, however. extract hi lo i a -- Isolate the bit-extraction case | hi == lo, KBounded _ sz <- kindOf i, hi < sz, hi >= 0 = text "(SBool)" <+> parens (parens (a <+> text ">>" <+> int hi) <+> text "& 1") extract hi lo i a = case (hi, lo, kindOf i) of (63, 32, KBounded False 64) -> text "(SWord32)" <+> parens (a <+> text ">> 32") (31, 0, KBounded False 64) -> text "(SWord32)" <+> a (31, 16, KBounded False 32) -> text "(SWord16)" <+> parens (a <+> text ">> 16") (15, 0, KBounded False 32) -> text "(SWord16)" <+> a (15, 8, KBounded False 16) -> text "(SWord8)" <+> parens (a <+> text ">> 8") ( 7, 0, KBounded False 16) -> text "(SWord8)" <+> a (63, 0, KBounded False 64) -> text "(SInt64)" <+> a (63, 0, KBounded True 64) -> text "(SWord64)" <+> a (31, 0, KBounded False 32) -> text "(SInt32)" <+> a (31, 0, KBounded True 32) -> text "(SWord32)" <+> a (15, 0, KBounded False 16) -> text "(SInt16)" <+> a (15, 0, KBounded True 16) -> text "(SWord16)" <+> a ( 7, 0, KBounded False 8) -> text "(SInt8)" <+> a ( 7, 0, KBounded True 8) -> text "(SWord8)" <+> a ( _, _, k ) -> tbd $ "extract with " ++ show (hi, lo, k, i) -- TBD: ditto here for join, just like extract above join (i, j, a, b) = case (kindOf i, kindOf j) of (KBounded False 8, KBounded False 8) -> parens (parens (text "(SWord16)" <+> a) <+> text "<< 8") <+> text "|" <+> parens (text "(SWord16)" <+> b) (KBounded False 16, KBounded False 16) -> parens (parens (text "(SWord32)" <+> a) <+> text "<< 16") <+> text "|" <+> parens (text "(SWord32)" <+> b) (KBounded False 32, KBounded False 32) -> parens (parens (text "(SWord64)" <+> a) <+> text "<< 32") <+> text "|" <+> parens (text "(SWord64)" <+> b) (k1, k2) -> tbd $ "join with " ++ show ((k1, i), (k2, j)) -- same as doubleQuotes, except we have to make sure there are no line breaks.. -- Otherwise breaks the generated code.. sigh printQuotes :: Doc -> Doc printQuotes d = text $ '"' : ppSameLine d ++ "\"" -- Remove newlines.. Useful when generating Makefile and such ppSameLine :: Doc -> String ppSameLine = trim . render where trim "" = "" trim ('\n':cs) = ' ' : trim (dropWhile isSpace cs) trim (c:cs) = c : trim cs -- Align a bunch of docs to occupy the exact same length by padding in the left by space -- this is ugly and inefficient, but easy to code.. align :: [Doc] -> [Doc] align ds = map (text . pad) ss where ss = map render ds l = maximum (0 : map length ss) pad s = replicate (l - length s) ' ' ++ s -- | Merge a bunch of bundles to generate code for a library mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle mergeToLib libName bundles | length nubKinds /= 1 = error $ "Cannot merge programs with differing SInteger/SReal mappings. Received the following kinds:\n" ++ unlines (map show nubKinds) | True = CgPgmBundle bundleKind $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake] where kinds = [k | CgPgmBundle k _ <- bundles] nubKinds = nub kinds bundleKind = head nubKinds files = concat [fs | CgPgmBundle _ fs <- bundles] sigs = concat [ss | (_, (CgHeader ss, _)) <- files] anyMake = not (null [() | (_, (CgMakefile{}, _)) <- files]) drivers = [ds | (_, (CgDriver, ds)) <- files] anyDriver = not (null drivers) mkFlags = nub (concat [xs | (_, (CgMakefile xs, _)) <- files]) sources = [(f, (CgSource, [pre, libHInclude, post])) | (f, (CgSource, [pre, _, post])) <- files] sourceNms = map fst sources libHeader = (libName ++ ".h", (CgHeader sigs, [genHeader bundleKind libName sigs empty])) libHInclude = text "#include" <+> text (show (libName ++ ".h")) libMake = ("Makefile", (CgMakefile mkFlags, [genLibMake anyDriver libName sourceNms mkFlags])) libDriver = (libName ++ "_driver.c", (CgDriver, mergeDrivers libName libHInclude (zip (map takeBaseName sourceNms) drivers))) -- | Create a Makefile for the library genLibMake :: Bool -> String -> [String] -> [String] -> Doc genLibMake ifdr libName fs ldFlags = foldr1 ($$) [l | (True, l) <- lns] where ifld = not (null ldFlags) ld | ifld = text "${LDFLAGS}" | True = empty lns = [ (True, text "# Makefile for" <+> nm <> text ". Automatically generated by SBV. Do not edit!") , (True, text "") , (True, text "# include any user-defined .mk file in the current directory.") , (True, text "-include *.mk") , (True, text "") , (True, text "CC?=gcc") , (True, text "CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer") , (ifld, text "LDFLAGS?=" <> text (unwords ldFlags)) , (True, text "AR?=ar") , (True, text "ARFLAGS?=cr") , (True, text "") , (not ifdr, text ("all: " ++ liba)) , (ifdr, text ("all: " ++ unwords [liba, libd])) , (True, text "") , (True, text liba <> text (": " ++ unwords os)) , (True, text "\t${AR} ${ARFLAGS} $@ $^") , (True, text "") , (ifdr, text libd <> text (": " ++ unwords [libd ++ ".c", libh])) , (ifdr, text ("\t${CC} ${CCFLAGS} $< -o $@ " ++ liba) <+> ld) , (ifdr, text "") , (True, vcat (zipWith mkObj os fs)) , (True, text "clean:") , (True, text "\trm -f *.o") , (True, text "") , (True, text "veryclean: clean") , (not ifdr, text "\trm -f" <+> text liba) , (ifdr, text "\trm -f" <+> text (unwords [liba, libd])) , (True, text "") ] nm = text libName liba = libName ++ ".a" libh = libName ++ ".h" libd = libName ++ "_driver" os = map (`replaceExtension` ".o") fs mkObj o f = text o <> text (": " ++ unwords [f, libh]) $$ text "\t${CC} ${CCFLAGS} -c $< -o $@" $$ text "" -- | Create a driver for a library mergeDrivers :: String -> Doc -> [(FilePath, [Doc])] -> [Doc] mergeDrivers libName inc ds = pre : concatMap mkDFun ds ++ [callDrivers (map fst ds)] where pre = text "/* Example driver program for" <+> text libName <> text ". */" $$ text "/* Automatically generated by SBV. Edit as you see fit! */" $$ text "" $$ text "#include " $$ inc mkDFun (f, [_pre, _header, body, _post]) = [header, body, post] where header = text "" $$ text ("void " ++ f ++ "_driver(void)") $$ text "{" post = text "}" mkDFun (f, _) = die $ "mergeDrivers: non-conforming driver program for " ++ show f callDrivers fs = text "" $$ text "int main(void)" $$ text "{" $+$ nest 2 (vcat (map call fs)) $$ nest 2 (text "return 0;") $$ text "}" call f = text psep $$ text ptag $$ text psep $$ text (f ++ "_driver();") $$ text "" where tag = "** Driver run for " ++ f ++ ":" ptag = "printf(\"" ++ tag ++ "\\n\");" lsep = replicate (length tag) '=' psep = "printf(\"" ++ lsep ++ "\\n\");" {-# ANN module ("HLint: ignore Redundant lambda" :: String) #-}