module Language.Copilot.Interface (
Options(), baseOpts, test, interpret, compile, verify, interface
, help , setE, setC, setO, setP, setI, setCode, setN, setV, setR
, setDir, setGCC, setArrs, setClock, setSim,
module Language.Copilot.Dispatch
) where
import Language.Copilot.Core
import Language.Copilot.Language.RandomOps (opsF, opsF2, opsF3)
import Language.Copilot.Tests.Random
import Language.Copilot.Dispatch
import Language.Copilot.Help
import qualified Language.Atom as A (Clock)
import System.Random
import System.Exit
import System.Cmd
import Data.Maybe
import qualified Data.Map as M (empty)
import Control.Monad (when)
data Options = Options {
optStreams :: Maybe (StreamableMaps Spec),
optExts :: Maybe Vars,
optCompile :: Maybe String,
optPeriod :: Maybe Period,
optInterpret :: Bool,
optIterations :: Int,
optVerbose :: Verbose,
optRandomSeed :: Maybe Int,
optCName :: Name,
optCompiler :: String,
optOutputDir :: String,
optPrePostCode :: (Maybe String, Maybe String),
optSimulate :: Bool,
optTriggers :: Triggers,
optArrs :: [(String, Int)],
optClock :: Maybe A.Clock
}
baseOpts :: Options
baseOpts = Options {
optStreams = Nothing,
optExts = Nothing,
optCompile = Nothing,
optPeriod = Nothing,
optInterpret = False,
optIterations = 0,
optVerbose = DefaultVerbose,
optRandomSeed = Nothing,
optCName = "copilotProgram",
optCompiler = "gcc",
optOutputDir = "./",
optPrePostCode = (Nothing, Nothing),
optSimulate = False,
optTriggers = M.empty,
optArrs = [],
optClock = Nothing
}
test :: Int -> Options -> IO ()
test n opts =
interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ setSim opts
interpret :: Streams -> Int -> Options -> IO ()
interpret streams n opts =
interface $ setI $ setN n $ opts {optStreams = Just (getSpecs streams)}
compile :: Streams -> Name -> Options -> IO ()
compile streams fileName opts =
interface $ setC "-Wall" $ setO fileName
$ setTriggers (getTriggers streams)
$ opts {optStreams = Just (getSpecs streams)}
verify :: FilePath -> Int -> String -> IO ()
verify file n opts = do
putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke."
putStrLn "<http://www.cprover.org/cbmc/>, with the following checks:"
putStrLn " --bounds-check enable array bounds checks"
putStrLn " --div-by-zero-check enable division by zero checks"
putStrLn " --pointer-check enable pointer checks"
putStrLn " --overflow-check enable arithmetic over- and underflow checks"
putStrLn " --nan-check check floating-point for NaN"
putStrLn ""
putStrLn "Assuming main() as the entry point unless specified otherwise (--function f)"
putStrLn cmd
code <- system cmd
case code of
ExitSuccess -> return ()
_ -> do putStrLn ""
putStrLn $ "An error was returned by cbmc. This may have be due to cbmc not finding the file " ++ file ++ ". Perhaps cbmc is not installed on your system, is not in your path, cbmc cannot be called from the command line on your system, or " ++ file ++ " does not exist. See <http://www.cprover.org/cbmc/> for more information on cbmc."
where cmd = unwords ("cbmc" : args)
args = ["--div-by-zero-check", "--overflow-check", "--bounds-check"
, "--nan-check", "--pointer-check"
, "--unwind " ++ show n, opts, file]
setTriggers :: Triggers -> Options -> Options
setTriggers triggers opts = opts {optTriggers = triggers}
setE :: Vars -> Options -> Options
setE vs opts = opts {optExts = Just vs}
setArrs :: [(String,Int)] -> Options -> Options
setArrs ls opts = opts {optArrs = ls}
setClock :: A.Clock -> Options -> Options
setClock clk opts = opts {optClock = Just clk}
setC :: String -> Options -> Options
setC gccOptions opts = opts {optCompile = Just gccOptions}
setP :: Period -> Options -> Options
setP p opts = opts {optPeriod = Just p}
setI :: Options -> Options
setI opts = opts {optInterpret = True}
setN :: Int -> Options -> Options
setN n opts = opts {optIterations = n}
setV :: Verbose -> Options -> Options
setV v opts = opts {optVerbose = v}
setR :: Int -> Options -> Options
setR seed opts = opts {optRandomSeed = Just seed}
setO :: Name -> Options -> Options
setO fileName opts = opts {optCName = fileName}
setGCC :: String -> Options -> Options
setGCC compilerStr opts = opts {optCompiler = compilerStr}
setDir :: String -> Options -> Options
setDir dir opts = opts {optOutputDir = dir}
setCode :: (Maybe String, Maybe String) -> Options -> Options
setCode pp opts = opts {optPrePostCode = pp}
setSim :: Options -> Options
setSim opts = opts {optSimulate = True}
interface :: Options -> IO ()
interface opts =
do
seed <- createSeed opts
let (streams, vars) = getStreamsVars opts seed
triggers = optTriggers opts
backEnd = getBackend opts seed
iterations = optIterations opts
verbose = optVerbose opts
when (verbose == Verbose) $
putStrLn $ "Random seed :" ++ show seed
dispatch (LangElems streams triggers) vars backEnd iterations verbose
createSeed :: Options -> IO Int
createSeed opts =
case optRandomSeed opts of
Nothing ->
do
g <- newStdGen
return . fst . random $ g
Just i -> return i
getStreamsVars :: Options -> Int -> (StreamableMaps Spec, Vars)
getStreamsVars opts seed =
case optStreams opts of
Nothing -> randomStreams opsF opsF2 opsF3 (mkStdGen seed)
Just s ->
case optExts opts of
Nothing -> (s, emptySM)
Just vs -> (s, vs)
getBackend :: Options -> Int -> BackEnd
getBackend opts seed =
case optCompile opts of
Nothing ->
if not $ optInterpret opts
then error "neither interpreted nor compiled: nothing to be done"
else Interpreter
Just gccOptions ->
Opts $ AtomToC {
cName = optCName opts ++ if isJust $ optRandomSeed opts then show seed else "",
gccOpts = gccOptions,
getPeriod = optPeriod opts,
interpreted = if optInterpret opts then Interpreted else NotInterpreted,
outputDir = optOutputDir opts,
compiler = optCompiler opts,
prePostCode = optPrePostCode opts,
sim = optSimulate opts,
arrDecs = optArrs opts,
clock = optClock opts
}
help :: IO ()
help = putStrLn helpStr