module Data.SBV.Compilers.C(compileToC, compileToCLib, compileToC', compileToCLib') where
import Data.Char (isSpace)
import Data.List (nub)
import Data.Maybe (isJust)
import qualified Data.Foldable as F (toList)
import Text.PrettyPrint.HughesPJ
import System.FilePath (takeBaseName, replaceExtension)
import System.Random
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.PrettyNum(shex)
import Data.SBV.Compilers.CodeGen
compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()
compileToC mbDirName nm f = compileToC' nm f >>= renderCgPgmBundle mbDirName
compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
compileToC' nm f = do rands <- randoms `fmap` newStdGen
codeGen SBVToC (defaultCgConfig { cgDriverVals = rands }) nm f
compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
compileToCLib mbDirName libName comps = compileToCLib' libName comps >>= renderCgPgmBundle mbDirName
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
compileToCLib' libName comps = mergeToLib libName `fmap` mapM (uncurry compileToC') comps
data SBVToC = SBVToC
instance CgTarget SBVToC where
targetName _ = "C"
translate _ = cgen
die :: String -> a
die msg = error $ "SBV->C: Unexpected: " ++ msg
tbd :: String -> a
tbd msg = error $ "SBV->C: Not yet supported: " ++ msg
cgen :: CgConfig -> String -> CgState -> Result -> CgPgmBundle
cgen cfg nm st sbvProg = CgPgmBundle $ filt [ ("Makefile", (CgMakefile flags, [genMake driver nm nmd flags]))
, (nm ++ ".h", (CgHeader [sig], [genHeader nm [sig] extProtos]))
, (nmd ++ ".c", (CgDriver, genDriver randVals nm ins outs mbRet))
, (nm ++ ".c", (CgSource, genCProg rtc nm sig sbvProg ins outs mbRet extDecls))
]
where rtc = cgRTC cfg
randVals = cgDriverVals cfg
driver = cgGenDriver cfg
filt xs = if driver then xs else filter (not . isCgDriver . fst . snd) xs
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 ++ [text ""]
flags = cgLDFlags st
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 (hasSign sw, sizeOf sw)
mkParam, mkPParam :: (String, CgVal) -> Doc
mkParam (n, CgAtomic sw) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord True sgsz <+> text n
mkParam (_, CgArray []) = die "mkParam: CgArray with no elements!"
mkParam (n, CgArray (sw:_)) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord True sgsz <+> text "*" <> text n
mkPParam (n, CgAtomic sw) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord False sgsz <+> text "*" <> text n
mkPParam (_, CgArray []) = die "mPkParam: CgArray with no elements!"
mkPParam (n, CgArray (sw:_)) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord False sgsz <+> text "*" <> text n
declSW :: Int -> SW -> Doc
declSW w sw@(SW sgsz _) = text "const" <+> pad (showCType sgsz) <+> text (show sw)
where pad s = text $ s ++ replicate (w length s) ' '
showSW :: [(SW, CW)] -> SW -> Doc
showSW consts sw
| sw == falseSW = text "0"
| sw == trueSW = text "1"
| Just cw <- sw `lookup` consts = showConst cw
| True = text $ show sw
pprCWord :: Bool -> (Bool, Int) -> Doc
pprCWord cnst sgsz = (if cnst then text "const" else empty) <+> text (showCType sgsz)
showCType :: (Bool, Int) -> String
showCType (False, 1) = "SBool"
showCType (s, sz)
| sz `elem` [8, 16, 32, 64] = t
| True = die $ "Non-regular bitvector type: " ++ t
where t = (if s then "SInt" else "SWord") ++ show sz
specifier :: (Bool, Int) -> Doc
specifier (False, 1) = text "%d"
specifier (False, 8) = text "%\"PRIu8\""
specifier (True, 8) = text "%\"PRId8\""
specifier (False, 16) = text "0x%04\"PRIx16\"U"
specifier (True, 16) = text "%\"PRId16\""
specifier (False, 32) = text "0x%08\"PRIx32\"UL"
specifier (True, 32) = text "%\"PRId32\"L"
specifier (False, 64) = text "0x%016\"PRIx64\"ULL"
specifier (True, 64) = text "%\"PRId64\"LL"
specifier (s, sz) = die $ "Format specifier at type " ++ (if s then "SInt" else "SWord") ++ show sz
mkConst :: Integer -> (Bool, Int) -> Doc
mkConst i (False, 1) = integer i
mkConst i (False, 8) = integer i
mkConst i (True, 8) = integer i
mkConst i t@(False, 16) = text (shex False True t i) <> text "U"
mkConst i t@(True, 16) = text (shex False True t i)
mkConst i t@(False, 32) = text (shex False True t i) <> text "UL"
mkConst i t@(True, 32) = text (shex False True t i) <> text "L"
mkConst i t@(False, 64) = text (shex False True t i) <> text "ULL"
mkConst i t@(True, 64) = text (shex False True t i) <> text "LL"
mkConst i (True, 1) = die $ "Signed 1-bit value " ++ show i
mkConst i (s, sz) = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz
showConst :: CW -> Doc
showConst cw = mkConst (cwVal cw) (hasSign cw, sizeOf cw)
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"
genHeader :: String -> [Doc] -> Doc -> Doc
genHeader 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 <inttypes.h>"
$$ text "#include <stdint.h>"
$$ text ""
$$ text "/* Unsigned bit-vectors */"
$$ text "typedef uint8_t SBool ;"
$$ 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 ""
$$ 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 ""
sepIf :: Bool -> Doc
sepIf b = if b then text "" else empty
genDriver :: [Integer] -> String -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> [Doc]
genDriver 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 <inttypes.h>"
$$ text "#include <stdint.h>"
$$ text "#include <stdio.h>"
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 (hasSign sw, sizeOf 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 ival sgsz
where sgsz@(sg, sz) = (hasSign sw, sizeOf sw)
ival | r >= minVal && r <= maxVal = r
| not sg = r `mod` (2^sz)
| True = (r `mod` (2^sz)) (2^(sz1))
where expSz, expSz', minVal, maxVal :: Integer
expSz = 2^(sz1)
expSz' = 2*expSz
minVal | not sg = 0
| True = expSz
maxVal | not sg = expSz'1
| True = expSz1
mkInp (_, _, CgAtomic{}) = empty
mkInp (_, n, CgArray []) = die $ "Unsupported empty array value for " ++ show n
mkInp (vs, n, CgArray sws@(sw:_)) = pprCWord True (hasSign sw, sizeOf 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) = let sgsz = (hasSign sw, sizeOf sw) in pprCWord False sgsz <+> text v <> semi
mkOut (v, CgArray []) = die $ "Unsupported empty array value for " ++ show v
mkOut (v, CgArray sws@(sw:_)) = pprCWord False (hasSign sw, sizeOf sw) <+> text v <> brackets (int (length sws)) <> semi
resultVar = text "__result"
call = case mbRet of
Nothing -> fcall <> semi
Just sw -> pprCWord True (hasSign sw, sizeOf 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 (hasSign sw, sizeOf 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 (hasSign sw, sizeOf sw)
genCProg :: Bool -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]
genCProg rtc fn proto (Result ins preConsts tbls arrs _ _ asgns _) inVars outVars mbRet extDecls
| 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 pre = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */"
$$ text ""
$$ text "#include <inttypes.h>"
$$ text "#include <stdint.h>"
header = text "#include" <+> doubleQuotes (nm <> text ".h")
post = text ""
$$ extDecls
$$ proto
$$ text "{"
$$ text ""
$$ nest 2 ( vcat (concatMap (genIO True) inVars)
$$ vcat (merge (map genTbl tbls) (map genAsgn assignments))
$$ sepIf (not (null assignments) || not (null tbls))
$$ vcat (concatMap (genIO False) outVars)
$$ maybe empty mkRet mbRet
)
$$ text "}"
$$ text ""
nm = text fn
assignments = F.toList asgns
typeWidth = getMax 0 [len (hasSign s, sizeOf s) | (s, _) <- assignments]
where len (False, 1) = 5
len (False, n) = 5 + length (show n)
len (True, n) = 4 + length (show n)
getMax 7 _ = 7
getMax m [] = m
getMax m (x:xs) = getMax (m `max` x) xs
consts = (falseSW, falseCW) : (trueSW, trueCW) : preConsts
isConst s = isJust (lookup s consts)
genIO :: Bool -> (String, CgVal) -> [Doc]
genIO True (cNm, CgAtomic sw) = [declSW typeWidth sw <+> text "=" <+> text cNm <> semi]
genIO False (cNm, CgAtomic sw) = [text "*" <> text cNm <+> text "=" <+> showSW consts sw <> semi]
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 consts sw <> semi
where entry = cNm ++ "[" ++ show i ++ "]"
mkRet sw = text "return" <+> showSW consts sw <> semi
genTbl :: ((Int, (Bool, Int), (Bool, Int)), [SW]) -> (Int, Doc)
genTbl ((i, _, (sg, sz)), elts) = (location, static <+> pprCWord True (sg, sz) <+> text ("table" ++ show i) <> text "[] = {"
$$ nest 4 (fsep (punctuate comma (align (map (showSW 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, declSW typeWidth sw <+> text "=" <+> ppExpr rtc consts n <> semi)
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
ppExpr :: Bool -> [(SW, CW)] -> SBVExpr -> Doc
ppExpr rtc consts (SBVApp op opArgs) = p op (map (showSW consts) opArgs)
where cBinOps = [ (Plus, "+"), (Times, "*"), (Minus, "-")
, (Equal, "=="), (NotEqual, "!=")
, (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")
, (And, "&"), (Or, "|"), (XOr, "^")
]
p (ArrRead _) _ = tbd "User specified arrays (ArrRead)"
p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)"
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 (let s = head opArgs in (hasSign s, sizeOf s)) a
p Join [a, b] = join (let (s1 : s2 : _) = opArgs in ((hasSign s1, sizeOf s1), (hasSign s2, sizeOf s2), a, b))
p (Rol i) [a] = rotate True i a (let s = head opArgs in (hasSign s, sizeOf s))
p (Ror i) [a] = rotate False i a (let s = head opArgs in (hasSign s, sizeOf s))
p (Shl i) [a] = shift True i a (let s = head opArgs in (hasSign s, sizeOf s))
p (Shr i) [a] = shift False i a (let s = head opArgs in (hasSign s, sizeOf s))
p Not [a]
| s == 1
= parens (text "~" <> a) <+> text "&" <+> text "0x01U"
| True
= text "~" <> a
where s = sizeOf (head opArgs)
p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c
p (LkUp (t, (as, at), _, len) ind def) []
| not rtc = lkUp
| needsCheckL && needsCheckR = cndLkUp checkBoth
| needsCheckL = cndLkUp checkLeft
| needsCheckR = cndLkUp checkRight
| True = lkUp
where [index, defVal] = map (showSW consts) [ind, def]
lkUp = text "table" <> int t <> brackets (showSW consts ind)
cndLkUp cnd = cnd <+> text "?" <+> defVal <+> text ":" <+> lkUp
checkLeft = index <+> text "< 0"
checkRight = index <+> text ">=" <+> int len
checkBoth = parens (checkLeft <+> text "||" <+> checkRight)
(needsCheckL, needsCheckR) | as = (True, (2::Integer)^(at1)1 >= fromIntegral len)
| True = (False, (2::Integer)^at 1 >= fromIntegral len)
p Quot [a, b] = parens (b <+> text "== 0") <+> text "?" <+> text "0" <+> text ":" <+> parens (a <+> text "/" <+> b)
p Rem [a, b] = parens (b <+> text "== 0") <+> text "?" <+> a <+> text ":" <+> parens (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
shift toLeft i a (sg, sz)
| i < 0 = shift (not toLeft) (i) a (sg, sz)
| i == 0 = a
| i >= sz = mkConst 0 (sg, sz)
| True = a <+> text cop <+> int i
where cop | toLeft = "<<"
| True = ">>"
rotate toLeft i a (True, sz)
= tbd $ "Rotation of signed words at size " ++ show (toLeft, i, a, sz)
rotate toLeft i a (False, sz)
| i < 0 = rotate (not toLeft) (i) a (False, sz)
| i == 0 = a
| i >= sz = rotate toLeft (i `mod` sz) a (False, sz)
| True = parens (a <+> text cop <+> int i)
<+> text "|"
<+> parens (a <+> text cop' <+> int (sz i))
where (cop, cop') | toLeft = ("<<", ">>")
| True = (">>", "<<")
extract 63 32 (False, 64) a = text "(SWord32)" <+> parens (a <+> text ">> 32")
extract 31 0 (False, 64) a = text "(SWord32)" <+> a
extract 31 16 (False, 32) a = text "(SWord16)" <+> parens (a <+> text ">> 16")
extract 15 0 (False, 32) a = text "(SWord16)" <+> a
extract 15 8 (False, 16) a = text "(SWord8)" <+> parens (a <+> text ">> 8")
extract 7 0 (False, 16) a = text "(SWord8)" <+> a
extract 63 0 (False, 64) a = text "(SInt64)" <+> a
extract 63 0 (True, 64) a = text "(SWord64)" <+> a
extract 31 0 (False, 32) a = text "(SInt32)" <+> a
extract 31 0 (True, 32) a = text "(SWord32)" <+> a
extract 15 0 (False, 16) a = text "(SInt16)" <+> a
extract 15 0 (True, 16) a = text "(SWord16)" <+> a
extract 7 0 (False, 8) a = text "(SInt8)" <+> a
extract 7 0 (True, 8) a = text "(SWord8)" <+> a
extract i j (sg, sz) _ = tbd $ "extract with " ++ show (i, j, (sg, sz))
join ((False, 8), (False, 8), a, b) = parens (parens (text "(SWord16)" <+> a) <+> text "<< 8") <+> text "|" <+> parens (text "(SWord16)" <+> b)
join ((False, 16), (False, 16), a, b) = parens (parens (text "(SWord32)" <+> a) <+> text "<< 16") <+> text "|" <+> parens (text "(SWord32)" <+> b)
join ((False, 32), (False, 32), a, b) = parens (parens (text "(SWord64)" <+> a) <+> text "<< 32") <+> text "|" <+> parens (text "(SWord64)" <+> b)
join (sgsz1, sgsz2, _, _) = tbd $ "join with " ++ show (sgsz1, sgsz2)
printQuotes :: Doc -> Doc
printQuotes d = text $ '"' : ppSameLine d ++ "\""
ppSameLine :: Doc -> String
ppSameLine = trim . render
where trim "" = ""
trim ('\n':cs) = ' ' : trim (dropWhile isSpace cs)
trim (c:cs) = c : trim cs
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
mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle
mergeToLib libName bundles = CgPgmBundle $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake]
where files = concat [fs | CgPgmBundle fs <- bundles]
sigs = concat [ss | (_, (CgHeader ss, _)) <- 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 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)))
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 ""
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 <inttypes.h>"
$$ text "#include <stdint.h>"
$$ text "#include <stdio.h>"
$$ 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\");"