module Language.Copilot.Interface (
Options(), baseOpts, test, interpret, compile, verify, interface
, help , setS, setE, setC, setO, setP, setI, setPP, setN, setV, setR
, setDir, setGCC, setTriggers,
module Language.Copilot.Dispatch
) where
import Language.Copilot.Core
import Language.Copilot.Language (opsF, opsF2, opsF3)
import Language.Copilot.Tests.Random
import Language.Copilot.Dispatch
import Language.Copilot.Help
import Data.Set as Set (fromList, toList)
import Data.List ((\\))
import System.Random
import System.Exit
import System.FilePath (takeBaseName)
import System.Cmd
import Data.Maybe
import Control.Monad
import Control.Monad.Writer (execWriter)
data Options = Options {
optStreams :: Maybe Streams,
optSends :: Sends,
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, String),
optTriggers :: Maybe [(Var, String)]
}
baseOpts :: Options
baseOpts = Options {
optStreams = Nothing,
optSends = emptySM,
optExts = Nothing,
optCompile = Nothing,
optPeriod = Nothing,
optInterpret = False,
optIterations = 0,
optVerbose = DefaultVerbose,
optRandomSeed = Nothing,
optCName = "copilotProgram",
optCompiler = "gcc",
optOutputDir = "./",
optPrePostCode = Nothing,
optTriggers = Nothing
}
test :: Int -> Options -> IO ()
test n opts =
interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ opts
interpret :: Streams -> Int -> Options -> IO ()
interpret streams n opts = interface $ setI $ setN n $ opts {optStreams = Just streams}
compile :: Streams -> Name -> Options -> IO ()
compile streams fileName opts =
interface $ setC "-Wall" $ setO fileName $ opts {optStreams = Just streams}
verify :: FilePath -> IO ()
verify file = 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 " ++ theMain ++ " as the entry point:"
putStrLn cmd
code <- system cmd
case code of
ExitSuccess -> return ()
_ -> do putStrLn $ "cbmc could not be called on file " ++ file ++ "."
putStrLn "Perhaps cbmc is not installed on your system, is"
putStrLn "not in your path, cbmc cannot be called from the"
putStrLn $ "command line on your system, or " ++ file
putStrLn $ "does not exist, or the dispatch function in" ++ file
putStrLn $ "is not called " ++ theMain ++ "."
putStrLn "See <http://www.cprover.org/cbmc/>"
putStrLn "for more information on cbmc."
where theMain = takeBaseName file
cmd = unwords ("cbmc" : args)
args = ["--div-by-zero-check", "--overflow-check", "--bounds-check"
, "--nan-check", "--pointer-check"
, "--function " ++ theMain, file]
setS :: DistributedStreams -> Options -> Options
setS (streams, sends) opts = opts {optStreams = Just streams, optSends = sends}
setE :: Vars -> Options -> Options
setE vs opts = opts {optExts = Just vs}
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}
setPP :: (String, String) -> Options -> Options
setPP pp opts = opts {optPrePostCode = Just pp}
setTriggers :: [(Var, String)] -> Options -> Options
setTriggers triggers opts =
if null repeats
then opts {optTriggers = Just triggers}
else error $ "Error: only one trigger per Copilot variable. Variables "
++ show (Set.fromList repeats) ++ " are given multiple triggers."
where vars = map fst triggers
repeats = vars \\ Set.toList (Set.fromList vars)
interface :: Options -> IO ()
interface opts =
do
seed <- createSeed opts
let (streams, vars) = getStreamsVars opts seed
sends = optSends opts
backEnd = getBackend opts seed
iterations = optIterations opts
verbose = optVerbose opts
when (verbose == Verbose) $
putStrLn $ "Random seed :" ++ show seed
dispatch streams sends 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)
where s' = execWriter s
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,
triggers = optTriggers opts
}
help :: IO ()
help = putStrLn helpStr