{-# LANGUAGE ScopedTypeVariables #-} -- | The Dispatch module : does all the IO, and offers an unified interface to both -- the interpreter and the compiler. -- -- Also communicates with GCC in order to compile the C code, and then transmits -- the results of the execution of that C code. This functionnality is mostly -- used to check automatically the equivalence between the interpreter and the -- compiler. The Dispatch module only parses the command-line arguments before -- calling that module. module Language.Copilot.Dispatch (dispatch, BackEnd(..), AtomToC(..), Interpreted(..), Iterations, Verbose(..)) where import Language.Copilot.Core import Language.Copilot.Analyser import Language.Copilot.Interpreter import Language.Copilot.AtomToC import Language.Copilot.Compiler import Language.Copilot.PrettyPrinter () import qualified Language.Atom as A import qualified Data.Map as M import Data.List ((\\)) import System.Directory import System.Process import System.IO import Control.Monad data AtomToC = AtomToC { cName :: Name -- ^ Name of the C file to generate , gccOpts :: String -- ^ Options to pass to the compiler , getPeriod :: Maybe Period -- ^ The optional period , interpreted :: Interpreted -- ^ Interpret the program or not , outputDir :: String -- ^ Where to put the executable , compiler :: String -- ^ Which compiler to use , prePostCode :: Maybe (String, String) -- ^ Code to replace the default initialization and main , triggers :: [(Var, String)] -- ^ A list of Copilot variable C function -- name pairs. The C funciton is called if -- the Copilot stream becomes True. The -- Stream must be of Booleans and the C -- function must be of type void @foo(void)@. , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we -- don't know how large external arrays are, so -- we cannot declare them. Passing in pairs -- containing the name of the array and it's -- size allows them to be declared." } data BackEnd = Opts AtomToC | Interpreter data Interpreted = Interpreted | NotInterpreted type Iterations = Int data Verbose = OnlyErrors | DefaultVerbose | Verbose deriving Eq -- | This function is the core of /Copilot/ : -- it glues together analyser, interpreter and compiler, and does all the IO. -- It can be called either from interface (which justs decodes the command-line argument) -- or directly from the interactive prompt in ghci. -- @streams@ is a specification, -- @inputExts@ allows the user to give at runtime values for -- the monitored variables. Useful for testing on randomly generated values and specifications, -- or for the interpreted version. -- @be@ chooses between compilation or interpretation, -- and if compilation is chosen (AtomToC) holds a few additionnal informations. -- see description of @'BackEnd'@ -- @iterations@ just gives the number of periods the specification must be executed. -- If you would rather execute it by hand, then just choose AtomToC for backEnd and 0 for iterations -- @verbose@ determines what is output. dispatch :: StreamableMaps Spec -> Sends -> Vars -> BackEnd -> Iterations -> Verbose -> IO () dispatch streams sends inputExts backEnd iterations verbose = do hSetBuffering stdout LineBuffering mapM_ putStrLn preludeText isValid <- case check streams of Just x -> putStrLn (show x) >> return False Nothing -> return True when isValid $ -- because haskell is lazy, will only get computed if later used let interpretedLines = showVars (interpretStreams streams trueInputExts) iterations in case backEnd of Interpreter -> do when (not allInputsPresents) $ error errMsg mapM_ putStrLn interpretedLines Opts opts -> let isInterpreted = case (interpreted opts) of Interpreted -> True NotInterpreted -> False dirName = outputDir opts in do putStrLn $ "Trying to create the directory " ++ dirName ++ "(if missing) ..." createDirectoryIfMissing False dirName checkTriggerVars streams (triggers opts) -- copilotToC streams sends allExts trueInputExts -- (cName opts) (getPeriod opts) (prePostCode opts) -- (triggers opts) isVerbose copilotToC streams sends allExts trueInputExts opts isVerbose let copy ext = copyFile (cName opts ++ ext) (dirName ++ cName opts ++ ext) let delete ext = do f0 <- canonicalizePath (cName opts ++ ext) f1 <- canonicalizePath (dirName ++ cName opts ++ ext) if f0 == f1 then return () else removeFile (cName opts ++ ext) putStrLn $ "Moving " ++ cName opts ++ ".c and " ++ cName opts ++ ".h to " ++ dirName ++ " ..." copy ".c" copy ".h" delete ".c" delete ".h" when (prePostCode opts == Nothing) $ gccCall (Opts opts) when ((isInterpreted || isExecuted) && not allInputsPresents) $ error errMsg when isExecuted $ execute streams (dirName ++ cName opts) trueInputExts isInterpreted interpretedLines iterations isSilent where errMsg = "The interpreter does not have values for some of the external variables." isVerbose = verbose == Verbose isSilent = verbose == OnlyErrors isExecuted = iterations /= 0 allExts = getExternalVars streams (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts -- Check that each trigger references an actual Copilot variable of type Bool. checkTriggerVars :: StreamableMaps Spec -> [(Var, String)] -> IO () checkTriggerVars streams trigs = if null badDefs then if null badTypes then return () else error $ "Copilot error in defining triggers: the variables " ++ show (map fst badTypes) ++ " are of a type other than Bool." else error $ "Copilot error in defining triggers: the variables " ++ show badDefs ++ " are given triggers but " ++ "don't define streams in-scope." where badDefs = map fst trigs \\ getVars streams listAtomTypes :: Streamable a => Var -> Spec a -> [(Var, A.Type)] -> [(Var, A.Type)] listAtomTypes v s ls = let t = getAtomType s in if t /= A.Bool && v `elem` (map fst trigs) then (v, t):ls else ls badTypes = foldStreamableMaps listAtomTypes streams [] copilotToC :: StreamableMaps Spec -> Sends -> [(A.Type, Var, ExtVars)] -> Vars -> AtomToC -> Bool -> IO () copilotToC streams sends allExts trueInputExts opts isVerbose = let (p', program) = copilotToAtom streams sends (getPeriod opts) (triggers opts) cFileName = cName opts (preCode, postCode) = case (prePostCode opts) of Nothing -> getPrePostCode cFileName streams allExts (arrDecs opts) trueInputExts p' Just (pre, post) -> (pre, post) atomConfig = A.defaults {A.cCode = \_ _ _ -> (preCode, postCode), A.cRuleCoverage = False, A.cAssert = False, A.cStateName = "copilotState" ++ cFileName} in do putStrLn $ "Compiling Copilot specs to C ..." (sched, _, _, _, _) <- A.compile cFileName atomConfig program if isVerbose then putStrLn $ A.reportSchedule sched else return () putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h" -- copilotToC streams sends allExts trueInputExts cFileName p prePostC trigs isVerbose = -- let (p', program) = copilotToAtom streams sends p trigs -- (preCode, postCode) = -- case prePostC of -- Nothing -> getPrePostCode cFileName streams allExts trueInputExts p' -- Just (pre, post) -> (pre, post) -- atomConfig = A.defaults -- {A.cCode = \_ _ _ -> (preCode, postCode), -- A.cRuleCoverage = False, -- A.cAssert = False, -- A.cStateName = "copilotState" ++ cFileName} -- in do -- putStrLn $ "Compiling Copilot specs to C ..." -- (sched, _, _, _, _) <- A.compile cFileName atomConfig program -- if isVerbose -- then putStrLn $ A.reportSchedule sched -- else return () -- putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h" gccCall :: BackEnd -> IO () gccCall backend = case backend of Interpreter -> error "Impossible: gccCall called with Interpreter." Opts opts -> let dirName = outputDir opts programName = cName opts in do let command = (compiler opts) ++ " " ++ dirName ++ cName opts ++ ".c" ++ " -o " ++ dirName ++ programName ++ " " ++ gccOpts opts putStrLn "Calling the C compiler ..." putStrLn command _ <- system command return () execute :: StreamableMaps Spec -> String -> Vars -> Bool -> [String] -> Iterations -> Bool -> IO () execute streams programName trueInputExts isInterpreted interpretedLines iterations isSilent = do (Just hin, Just hout, _, _) <- createProcess processConfig hSetBuffering hout LineBuffering hSetBuffering hin LineBuffering when isInterpreted (do putStrLn "\n *** Checking the randomly-generated Copilot specification: ***\n" putStrLn $ show streams) let inputVar v (val:vals) ioVars = do hPutStr hin (showAsC val ++ " \n") hFlush hin vars <- ioVars return $ updateSubMap (\m -> M.insert v vals m) vars inputVar _ [] _ = error "Impossible : empty inputVar" executePeriod _ [] 0 = putStrLn "Execution complete." executePeriod _ [] _ = error "Impossible : empty ExecutePeriod" executePeriod inputExts (inLine:inLines) n = when (n > 0) $ do nextInputExts <- foldStreamableMaps inputVar inputExts (return emptySM) line <- hGetLine hout let nextPeriod = (when (not isSilent) $ putStrLn line) >> executePeriod nextInputExts inLines (n - 1) -- Checking the compiler and interpreter. if isInterpreted then if inLine == line then nextPeriod else error $ unlines [ "Failure: interpreter /= compiler" , " program name: " ++ programName , " interpreter: " ++ inLine , " compiler: " ++ line ] else nextPeriod -- useful for initializing the sampling temporary variables firstInputExts <- foldStreamableMaps inputVar trueInputExts (return emptySM) executePeriod firstInputExts interpretedLines iterations where processConfig = (shell $ programName ++ " " ++ show iterations) {std_in = CreatePipe, std_out = CreatePipe, std_err = UseHandle stdout} showVars :: Vars -> Int-> [String] showVars interpretedVars n = showVarsLine interpretedVars 0 where showVarsLine inVs i = if i == n then [] else let (string, inVs') = foldStreamableMaps prettyShow inVs ("", emptySM) endString = showVarsLine inVs' (i + 1) beginString = "period: " ++ show i ++ " " ++ string in beginString:endString prettyShow v l (s, vs) = let s' = v ++ ": " ++ showAsC (head l) ++ " " ++ s vs' = updateSubMap (\ m -> M.insert v (tail l) m) vs in (s', vs') preludeText :: [String] preludeText = [ "" , "=========================================================================" , " CoPilot, a stream language for generating hard real-time C monitors. " , "=========================================================================" , "Copyright, Galois, Inc. 2010" , "BSD3 License" , "Website: http://leepike.github.com/Copilot/" , "Maintainer: Lee Pike (remove dashes)." , "Usage: > help" , "=========================================================================" , "" ]