1----------------------------------------------------------------------------- 2-- | 3-- Module : Data.SBV.Compilers.CodeGen 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Code generation utilities 10----------------------------------------------------------------------------- 11 12{-# LANGUAGE CPP #-} 13{-# LANGUAGE FlexibleInstances #-} 14{-# LANGUAGE GeneralizedNewtypeDeriving #-} 15 16{-# OPTIONS_GHC -Wall -Werror #-} 17 18module Data.SBV.Compilers.CodeGen ( 19 -- * The codegen monad 20 SBVCodeGen(..), cgSym 21 22 -- * Specifying inputs, SBV variants 23 , cgInput, cgInputArr 24 , cgOutput, cgOutputArr 25 , cgReturn, cgReturnArr 26 27 -- * Specifying inputs, SVal variants 28 , svCgInput, svCgInputArr 29 , svCgOutput, svCgOutputArr 30 , svCgReturn, svCgReturnArr 31 32 -- * Settings 33 , cgPerformRTCs, cgSetDriverValues 34 , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles, cgShowU8UsingHex 35 , cgIntegerSize, cgSRealType, CgSRealType(..) 36 37 -- * Infrastructure 38 , CgTarget(..), CgConfig(..), CgState(..), CgPgmBundle(..), CgPgmKind(..), CgVal(..) 39 , defaultCgConfig, initCgState, isCgDriver, isCgMakefile 40 41 -- * Generating collateral 42 , cgGenerateDriver, cgGenerateMakefile, codeGen, renderCgPgmBundle 43 ) where 44 45import Control.Monad (filterM, replicateM, unless) 46import Control.Monad.Trans (MonadIO(liftIO), lift) 47import Control.Monad.State.Lazy (MonadState, StateT(..), modify') 48import Data.Char (toLower, isSpace) 49import Data.List (nub, isPrefixOf, intercalate, (\\)) 50import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist) 51import System.FilePath ((</>)) 52import System.IO (hFlush, stdout) 53 54import Text.PrettyPrint.HughesPJ (Doc, vcat) 55import qualified Text.PrettyPrint.HughesPJ as P (render) 56 57import Data.SBV.Core.Data 58import Data.SBV.Core.Symbolic (MonadSymbolic(..), svToSymSV, svMkSymVar, outputSVal, VarContext(..)) 59 60#if MIN_VERSION_base(4,11,0) 61import Control.Monad.Fail as Fail 62#endif 63 64-- | Abstract over code generation for different languages 65class CgTarget a where 66 targetName :: a -> String 67 translate :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle 68 69-- | Options for code-generation. 70data CgConfig = CgConfig { 71 cgRTC :: Bool -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc. 72 , cgInteger :: Maybe Int -- ^ Bit-size to use for representing SInteger (if any) 73 , cgReal :: Maybe CgSRealType -- ^ Type to use for representing SReal (if any) 74 , cgDriverVals :: [Integer] -- ^ Values to use for the driver program generated, useful for generating non-random drivers. 75 , cgGenDriver :: Bool -- ^ If 'True', will generate a driver program 76 , cgGenMakefile :: Bool -- ^ If 'True', will generate a makefile 77 , cgIgnoreAsserts :: Bool -- ^ If 'True', will ignore 'Data.SBV.sAssert' calls 78 , cgOverwriteGenerated :: Bool -- ^ If 'True', will overwrite the generated files without prompting. 79 , cgShowU8InHex :: Bool -- ^ If 'True', then 8-bit unsigned values will be shown in hex as well, otherwise decimal. (Other types always shown in hex.) 80 } 81 82-- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random. 83defaultCgConfig :: CgConfig 84defaultCgConfig = CgConfig { cgRTC = False 85 , cgInteger = Nothing 86 , cgReal = Nothing 87 , cgDriverVals = [] 88 , cgGenDriver = True 89 , cgGenMakefile = True 90 , cgIgnoreAsserts = False 91 , cgOverwriteGenerated = False 92 , cgShowU8InHex = False 93 } 94 95-- | Abstraction of target language values 96data CgVal = CgAtomic SV 97 | CgArray [SV] 98 99-- | Code-generation state 100data CgState = CgState { 101 cgInputs :: [(String, CgVal)] 102 , cgOutputs :: [(String, CgVal)] 103 , cgReturns :: [CgVal] 104 , cgPrototypes :: [String] -- extra stuff that goes into the header 105 , cgDecls :: [String] -- extra stuff that goes into the top of the file 106 , cgLDFlags :: [String] -- extra options that go to the linker 107 , cgFinalConfig :: CgConfig 108 } 109 110-- | Initial configuration for code-generation 111initCgState :: CgState 112initCgState = CgState { 113 cgInputs = [] 114 , cgOutputs = [] 115 , cgReturns = [] 116 , cgPrototypes = [] 117 , cgDecls = [] 118 , cgLDFlags = [] 119 , cgFinalConfig = defaultCgConfig 120 } 121 122-- | The code-generation monad. Allows for precise layout of input values 123-- reference parameters (for returning composite values in languages such as C), 124-- and return values. 125newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a) 126 deriving ( Applicative, Functor, Monad, MonadIO, MonadState CgState 127 , MonadSymbolic 128#if MIN_VERSION_base(4,11,0) 129 , Fail.MonadFail 130#endif 131 ) 132 133-- | Reach into symbolic monad from code-generation 134cgSym :: Symbolic a -> SBVCodeGen a 135cgSym = SBVCodeGen . lift 136 137-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: 'False'. 138cgPerformRTCs :: Bool -> SBVCodeGen () 139cgPerformRTCs b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgRTC = b } }) 140 141-- | Sets number of bits to be used for representing the 'SInteger' type in the generated C code. 142-- The argument must be one of @8@, @16@, @32@, or @64@. Note that this is essentially unsafe as 143-- the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as 144-- typical in most C implementations. 145cgIntegerSize :: Int -> SBVCodeGen () 146cgIntegerSize i 147 | i `notElem` [8, 16, 32, 64] 148 = error $ "SBV.cgIntegerSize: Argument must be one of 8, 16, 32, or 64. Received: " ++ show i 149 | True 150 = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgInteger = Just i }}) 151 152-- | Possible mappings for the 'SReal' type when translated to C. Used in conjunction 153-- with the function 'cgSRealType'. Note that the particular characteristics of the 154-- mapped types depend on the platform and the compiler used for compiling the generated 155-- C program. See <http://en.wikipedia.org/wiki/C_data_types> for details. 156data CgSRealType = CgFloat -- ^ @float@ 157 | CgDouble -- ^ @double@ 158 | CgLongDouble -- ^ @long double@ 159 deriving Eq 160 161-- 'Show' instance for 'cgSRealType' displays values as they would be used in a C program 162instance Show CgSRealType where 163 show CgFloat = "float" 164 show CgDouble = "double" 165 show CgLongDouble = "long double" 166 167-- | Sets the C type to be used for representing the 'SReal' type in the generated C code. 168-- The setting can be one of C's @"float"@, @"double"@, or @"long double"@, types, depending 169-- on the precision needed. Note that this is essentially unsafe as the semantics of 170-- infinite precision SReal values becomes reduced to the corresponding floating point type in 171-- C, and hence it is subject to rounding errors. 172cgSRealType :: CgSRealType -> SBVCodeGen () 173cgSRealType rt = modify' (\s -> s {cgFinalConfig = (cgFinalConfig s) { cgReal = Just rt }}) 174 175-- | Should we generate a driver program? Default: 'True'. When a library is generated, it will have 176-- a driver if any of the constituent functions has a driver. (See 'Data.SBV.Tools.CodeGen.compileToCLib'.) 177cgGenerateDriver :: Bool -> SBVCodeGen () 178cgGenerateDriver b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenDriver = b } }) 179 180-- | Should we generate a Makefile? Default: 'True'. 181cgGenerateMakefile :: Bool -> SBVCodeGen () 182cgGenerateMakefile b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenMakefile = b } }) 183 184-- | Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values. 185cgSetDriverValues :: [Integer] -> SBVCodeGen () 186cgSetDriverValues vs = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } }) 187 188-- | Ignore assertions (those generated by 'Data.SBV.sAssert' calls) in the generated C code 189cgIgnoreSAssert :: Bool -> SBVCodeGen () 190cgIgnoreSAssert b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgIgnoreAsserts = b } }) 191 192-- | Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions. 193cgAddPrototype :: [String] -> SBVCodeGen () 194cgAddPrototype ss = modify' (\s -> let old = cgPrototypes s 195 new = if null old then ss else old ++ [""] ++ ss 196 in s { cgPrototypes = new }) 197 198-- | If passed 'True', then we will not ask the user if we're overwriting files as we generate 199-- the C code. Otherwise, we'll prompt. 200cgOverwriteFiles :: Bool -> SBVCodeGen () 201cgOverwriteFiles b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgOverwriteGenerated = b } }) 202 203-- | If passed 'True', then we will show 'SWord 8' type in hex. Otherwise we'll show it in decimal. All signed 204-- types are shown decimal, and all unsigned larger types are shown hexadecimal otherwise. 205cgShowU8UsingHex :: Bool -> SBVCodeGen () 206cgShowU8UsingHex b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgShowU8InHex = b } }) 207 208 209-- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions. 210cgAddDecl :: [String] -> SBVCodeGen () 211cgAddDecl ss = modify' (\s -> s { cgDecls = cgDecls s ++ ss }) 212 213-- | Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in. 214cgAddLDFlags :: [String] -> SBVCodeGen () 215cgAddLDFlags ss = modify' (\s -> s { cgLDFlags = cgLDFlags s ++ ss }) 216 217-- | Creates an atomic input in the generated code. 218svCgInput :: Kind -> String -> SBVCodeGen SVal 219svCgInput k nm = do r <- symbolicEnv >>= liftIO . svMkSymVar (NonQueryVar (Just ALL)) k Nothing 220 sv <- svToSymSV r 221 modify' (\s -> s { cgInputs = (nm, CgAtomic sv) : cgInputs s }) 222 return r 223 224-- | Creates an array input in the generated code. 225svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] 226svCgInputArr k sz nm 227 | sz < 1 = error $ "SBV.cgInputArr: Array inputs must have at least one element, given " ++ show sz ++ " for " ++ show nm 228 | True = do rs <- symbolicEnv >>= liftIO . replicateM sz . svMkSymVar (NonQueryVar (Just ALL)) k Nothing 229 sws <- mapM svToSymSV rs 230 modify' (\s -> s { cgInputs = (nm, CgArray sws) : cgInputs s }) 231 return rs 232 233-- | Creates an atomic output in the generated code. 234svCgOutput :: String -> SVal -> SBVCodeGen () 235svCgOutput nm v = do _ <- outputSVal v 236 sv <- svToSymSV v 237 modify' (\s -> s { cgOutputs = (nm, CgAtomic sv) : cgOutputs s }) 238 239-- | Creates an array output in the generated code. 240svCgOutputArr :: String -> [SVal] -> SBVCodeGen () 241svCgOutputArr nm vs 242 | sz < 1 = error $ "SBV.cgOutputArr: Array outputs must have at least one element, received " ++ show sz ++ " for " ++ show nm 243 | True = do mapM_ outputSVal vs 244 sws <- mapM svToSymSV vs 245 modify' (\s -> s { cgOutputs = (nm, CgArray sws) : cgOutputs s }) 246 where sz = length vs 247 248-- | Creates a returned (unnamed) value in the generated code. 249svCgReturn :: SVal -> SBVCodeGen () 250svCgReturn v = do _ <- outputSVal v 251 sv <- svToSymSV v 252 modify' (\s -> s { cgReturns = CgAtomic sv : cgReturns s }) 253 254-- | Creates a returned (unnamed) array value in the generated code. 255svCgReturnArr :: [SVal] -> SBVCodeGen () 256svCgReturnArr vs 257 | sz < 1 = error $ "SBV.cgReturnArr: Array returns must have at least one element, received " ++ show sz 258 | True = do mapM_ outputSVal vs 259 sws <- mapM svToSymSV vs 260 modify' (\s -> s { cgReturns = CgArray sws : cgReturns s }) 261 where sz = length vs 262 263-- | Creates an atomic input in the generated code. 264cgInput :: SymVal a => String -> SBVCodeGen (SBV a) 265cgInput nm = do r <- forall_ 266 sv <- sbvToSymSV r 267 modify' (\s -> s { cgInputs = (nm, CgAtomic sv) : cgInputs s }) 268 return r 269 270-- | Creates an array input in the generated code. 271cgInputArr :: SymVal a => Int -> String -> SBVCodeGen [SBV a] 272cgInputArr sz nm 273 | sz < 1 = error $ "SBV.cgInputArr: Array inputs must have at least one element, given " ++ show sz ++ " for " ++ show nm 274 | True = do rs <- mapM (const forall_) [1..sz] 275 sws <- mapM sbvToSymSV rs 276 modify' (\s -> s { cgInputs = (nm, CgArray sws) : cgInputs s }) 277 return rs 278 279-- | Creates an atomic output in the generated code. 280cgOutput :: String -> SBV a -> SBVCodeGen () 281cgOutput nm v = do _ <- output v 282 sv <- sbvToSymSV v 283 modify' (\s -> s { cgOutputs = (nm, CgAtomic sv) : cgOutputs s }) 284 285-- | Creates an array output in the generated code. 286cgOutputArr :: SymVal a => String -> [SBV a] -> SBVCodeGen () 287cgOutputArr nm vs 288 | sz < 1 = error $ "SBV.cgOutputArr: Array outputs must have at least one element, received " ++ show sz ++ " for " ++ show nm 289 | True = do mapM_ output vs 290 sws <- mapM sbvToSymSV vs 291 modify' (\s -> s { cgOutputs = (nm, CgArray sws) : cgOutputs s }) 292 where sz = length vs 293 294-- | Creates a returned (unnamed) value in the generated code. 295cgReturn :: SBV a -> SBVCodeGen () 296cgReturn v = do _ <- output v 297 sv <- sbvToSymSV v 298 modify' (\s -> s { cgReturns = CgAtomic sv : cgReturns s }) 299 300-- | Creates a returned (unnamed) array value in the generated code. 301cgReturnArr :: SymVal a => [SBV a] -> SBVCodeGen () 302cgReturnArr vs 303 | sz < 1 = error $ "SBV.cgReturnArr: Array returns must have at least one element, received " ++ show sz 304 | True = do mapM_ output vs 305 sws <- mapM sbvToSymSV vs 306 modify' (\s -> s { cgReturns = CgArray sws : cgReturns s }) 307 where sz = length vs 308 309-- | Representation of a collection of generated programs. 310data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] 311 312-- | Different kinds of "files" we can produce. Currently this is quite "C" specific. 313data CgPgmKind = CgMakefile [String] -- list of flags to pass to linker 314 | CgHeader [Doc] 315 | CgSource 316 | CgDriver 317 318-- | Is this a driver program? 319isCgDriver :: CgPgmKind -> Bool 320isCgDriver CgDriver = True 321isCgDriver _ = False 322 323-- | Is this a make file? 324isCgMakefile :: CgPgmKind -> Bool 325isCgMakefile CgMakefile{} = True 326isCgMakefile _ = False 327 328-- A simple way to print bundles, mostly for debugging purposes. 329instance Show CgPgmBundle where 330 show (CgPgmBundle _ fs) = intercalate "\n" $ map showFile fs 331 where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String 332 showFile (f, (_, ds)) = "== BEGIN: " ++ show f ++ " ================\n" 333 ++ render' (vcat ds) 334 ++ "== END: " ++ show f ++ " ==================" 335 336-- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection 337-- of makefiles, source code, headers, etc. 338codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen a -> IO (a, CgConfig, CgPgmBundle) 339codeGen l cgConfig nm (SBVCodeGen comp) = do 340 ((retVal, st'), res) <- runSymbolic CodeGen $ runStateT comp initCgState { cgFinalConfig = cgConfig } 341 let st = st' { cgInputs = reverse (cgInputs st') 342 , cgOutputs = reverse (cgOutputs st') 343 } 344 allNamedVars = map fst (cgInputs st ++ cgOutputs st) 345 dupNames = allNamedVars \\ nub allNamedVars 346 unless (null dupNames) $ 347 error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames 348 349 return (retVal, cgFinalConfig st, translate l (cgFinalConfig st) nm st res) 350 351-- | Render a code-gen bundle to a directory or to stdout 352renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO () 353renderCgPgmBundle Nothing (_ , bundle) = print bundle 354renderCgPgmBundle (Just dirName) (cfg, CgPgmBundle _ files) = do 355 356 b <- doesDirectoryExist dirName 357 unless b $ do unless overWrite $ putStrLn $ "Creating directory " ++ show dirName ++ ".." 358 createDirectoryIfMissing True dirName 359 360 dups <- filterM (\fn -> doesFileExist (dirName </> fn)) (map fst files) 361 362 goOn <- case (overWrite, dups) of 363 (True, _) -> return True 364 (_, []) -> return True 365 _ -> do putStrLn $ "Code generation would overwrite the following " ++ (if length dups == 1 then "file:" else "files:") 366 mapM_ (\fn -> putStrLn ('\t' : fn)) dups 367 putStr "Continue? [yn] " 368 hFlush stdout 369 resp <- getLine 370 return $ map toLower resp `isPrefixOf` "yes" 371 372 if goOn then do mapM_ renderFile files 373 unless overWrite $ putStrLn "Done." 374 else putStrLn "Aborting." 375 376 where overWrite = cgOverwriteGenerated cfg 377 378 renderFile (f, (_, ds)) = do let fn = dirName </> f 379 unless overWrite $ putStrLn $ "Generating: " ++ show fn ++ ".." 380 writeFile fn (render' (vcat ds)) 381 382-- | An alternative to Pretty's @render@, which might have "leading" white-space in empty lines. This version 383-- eliminates such whitespace. 384render' :: Doc -> String 385render' = unlines . map clean . lines . P.render 386 where clean x | all isSpace x = "" 387 | True = x 388