diff --git a/Language/Copilot.hs b/Language/Copilot.hs --- a/Language/Copilot.hs +++ b/Language/Copilot.hs @@ -12,6 +12,7 @@ , module Language.Copilot.Libs.Indexes , module Language.Copilot.Libs.LTL , module Language.Copilot.Libs.PTLTL + -- , module Language.Copilot.AdHocC -- , module Language.Copilot.Examples.Examples -- , module Language.Copilot.Examples.LTLExamples -- , module Language.Copilot.Examples.PTLTLExamples @@ -23,7 +24,7 @@ import Language.Copilot.Help import Language.Copilot.AtomToC import Language.Copilot.Compiler -import Language.Copilot.Language (opsF, opsF2, opsF3) +import Language.Copilot.Language -- (opsF, opsF2, opsF3) import Language.Copilot.PrettyPrinter() import Language.Copilot.Tests.Random import Language.Copilot.Dispatch @@ -31,6 +32,7 @@ import Language.Copilot.Libs.Indexes import Language.Copilot.Libs.LTL import Language.Copilot.Libs.PTLTL +-- import Language.Copilot.AdHocC -- import Language.Copilot.Examples.Examples -- import Language.Copilot.Examples.LTLExamples -- import Language.Copilot.Examples.PTLTLExamples diff --git a/Language/Copilot/AdHocC.hs b/Language/Copilot/AdHocC.hs --- a/Language/Copilot/AdHocC.hs +++ b/Language/Copilot/AdHocC.hs @@ -1,10 +1,9 @@ --- TODO-Robin : Improve a lot that -> new package in Hackage ? -- generate C-Code with combinators, high-level, safe haskell. -- | Helper functions for writing free-form C code. module Language.Copilot.AdHocC ( - varDecl, includeBracket, includeQuote, - printf, printfNewline + varDecl, arrDecl, varInit, arrayInit, funcDecl + , includeBracket, includeQuote, printf, printfNewline ) where import Data.List (intersperse) @@ -14,12 +13,39 @@ -- | Takes a type and a list of variable names and declares them. varDecl :: Type -> [String] -> String varDecl t vars = - cType' t ++ " " ++ (unwords (intersperse "," vars)) ++ ";" - where - cType' Bool = "int" - cType' typ = cType typ + cType t ++ " " ++ unwords (intersperse "," vars) ++ ";" +-- | Takes a type and a list of array names and their sizes declares them. +arrDecl :: Type -> [(String,Int)] -> String +arrDecl t arrs = + cType t ++ " " ++ unwords (intersperse "," mkArrs) ++ ";" + where mkArrs = map (\(a,size) -> a ++ "[" ++ show size ++ "]") arrs +-- | Takes a type and a variable and initializes it. It is YOUR responsibility +-- to ensure that @val@ is of type @t@. +varInit :: Show a => Type -> String -> a -> String +varInit t var val = cType t ++ " " ++ var ++ " = " ++ show val ++ ";" + +-- Show a list with braces {} rather than brackets []. +bracesListShow :: Show a => [a] -> String +bracesListShow ls = + "{" ++ (foldl (++) "" $ intersperse "," $ map show ls) ++ "}" + +-- | Takes a type and an array and initializes it. It is YOUR responsibility to +-- ensure that @vals@ is of type @t@. +arrayInit :: Show a => Type -> String -> [a] -> String +arrayInit t var vals = + cType t ++ " " ++ var ++ " = " ++ bracesListShow vals ++ ";" + +-- | Declare function prototypes, given a return type, a function name, and a +-- | list of argument types. Use 'Nothing' for a return type of @void@. +funcDecl :: Maybe Type -> String -> [Type] -> String +funcDecl t fn argTs = makeRet t ++ " " ++ fn ++ "(" ++ makeArgTs ++ ");" + where makeRet Nothing = "void" + makeRet (Just t') = cType t' + makeArgTs | null argTs = "void" + | otherwise = unwords (intersperse "," $ map cType argTs) + -- | Add an include of a library includeBracket :: String -> String includeBracket lib = "#include <" ++ lib ++ ">" @@ -43,3 +69,4 @@ printf, printfNewline :: String -> [String] -> String printfNewline text vars = (printfPre text) ++ newline ++ (printfPost vars) printf text vars = (printfPre text) ++ (printfPost vars) + diff --git a/Language/Copilot/Analyser.hs b/Language/Copilot/Analyser.hs --- a/Language/Copilot/Analyser.hs +++ b/Language/Copilot/Analyser.hs @@ -1,17 +1,18 @@ {-# OPTIONS_GHC -XRelaxedPolyRec #-} --- | This module provides a way to check that a /Copilot/ specification is compilable +-- | This module provides a way to check that a /Copilot/ specification is +-- compilable module Language.Copilot.Analyser( -- * Main error checking functions check, Error(..), SpecSet(..), -- * Varied other things - getExternalVars, getAtomType + getExternalVars, ExtVars(..) {- -- * Dependency Graphs (experimental) Weight, Node(..), DependencyGraph, mkDepGraph, showDG -} ) where - + import Language.Copilot.Core import qualified Language.Atom as A @@ -21,45 +22,103 @@ type Weight = Int -- | Used for representing an error in the specification, detected by @'check'@ -data Error = +data Error = BadSyntax String Var -- ^ the BNF is not respected | BadDrop Int Var -- ^ A drop expression of less than 0 is used - | BadSamplingPhase Var Var Phase -- ^ if an external variable is sampled at phase 0 then there is no time for the stream to be updated - | BadType Var Var -- ^ either a variable is not defined, or not with the good type ; there is no implicit conversion of types in /Copilot/ - | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile /Copilot/ specification can only work if there is no negative weighted closed path in the specification, as described in the original research paper - | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but would need bigger prophecyArrays - | DependsOnFuture [Var] Var Weight-- ^ If an output depends of a future of an input it will be hard to compile to say the least + | BadSamplingPhase Var Var Phase -- ^ if an external variable is sampled at + -- phase 0 then there is no time for the + -- stream to be updated + | BadSamplingArrPhase Var Var Phase -- ^ if an external variable is sampled at + -- phase 0 then there is no time for the + -- stream to be updated + | BadPArrSpec Var Var String -- ^ External array indexes can only take + -- variables or constants as indexes. + | BadType Var Var -- ^ either a variable is not defined, or not with the + -- good type ; there is no implicit conversion of types in + -- /Copilot/ + | NonNegativeWeightedClosedPath [Var] Weight -- ^ The algorithm to compile + -- /Copilot/ specification can + -- only work if there is no + -- negative weighted closed + -- path in the specification, + -- as described in the original + -- research paper + | DependsOnClosePast [Var] Var Weight Weight -- ^ Could be compiled, but + -- would need bigger + -- prophecyArrays + | DependsOnFuture [Var] Var Weight -- ^ If an output depends of a future of + -- an input it will be hard to compile to + -- say the least instance Show Error where - show (BadSyntax s v) = - "Error syntax : " ++ s ++ "is not allowed in that position in stream " ++ v ++ "\n" - show (BadDrop i v) = - "Error : a Drop in stream " ++ v ++ "drops the number " ++ show i ++ - "of elements. " ++ show i ++ " is negative, and Drop only accepts positive arguments. \n" - show (BadSamplingPhase v v' ph) = - "Error : the external variable " ++ v' ++ " is sampled at phase " ++ show ph ++ - " in the stream" ++ v ++ ". Sampling can only occur from phase 1 onwards. \n" + show (BadSyntax s v) = + unlines + ["Error syntax : " ++ s ++ " is not allowed in that position in stream " + ++ v ++ "."] + show (BadDrop i v) = + unlines + [ "Error : a Drop in stream " ++ v ++ " drops the number " ++ show i ++ + "of elements.\n" + , show i ++ " is negative, and Drop only accepts positive arguments.\n" + ] + show (BadSamplingPhase v v' ph) = + unlines + [ "Error : the external variable " ++ v' ++ " is sampled at phase " ++ + show ph ++ " in the stream " ++ v ++ "." + , "Sampling can only occur from phase 1 onwards.\n" + ] + show (BadSamplingArrPhase v arr ph) = + unlines + [ "Error : the external array " ++ arr ++ " is sampled at phase " ++ + show ph ++ " in the stream " ++ v ++ "." + , " Sampling can only occur from phase 1 onwards.\n" + ] + show (BadPArrSpec v arr idx) = + unlines + [ "Error : the index into an external array can only take a " + ++ "variable or a constant. The index\n" + , idx ++ "\n\n in external array " + ++ arr ++ "in the definition of stream " ++ v ++ " is not of that " + ++ "form.\n" + ] show (BadType v v') = - "Error : the monitor variable " ++ v ++ ", called in the stream " ++ v' ++ - " either does not exist, or don't have the right type (there is no implicit conversion)\n" + unlines + [ "Error : the monitor variable " ++ v ++ ", called in the stream " + ++ v' ++ ", either" + , "does not exist, or don't have the right type (there is no implicit " + ++ "conversion).\n" + ] show (NonNegativeWeightedClosedPath vs w) = - "Error : the following path is closed in the dependency graph of this " - ++ "specification and have weight " ++ show w ++ " which is positive (append decrease the weight, " - ++ "while drop increase it). This is forbidden to avoid streams which could " - ++ "take 0 or several different values. Try adding some initial elements (e.g., [0,0,0] ++ ...) " - ++ "to the offending streams. \n" - ++ "Path : " ++ show (reverse vs) ++ "\n" + unlines + [ "Error : the following path is closed in the dependency graph of the " + ++ "specification and has" + , "weight " ++ show w ++ " which is positive (append decreases the weight, " + ++ "while drop increases it)." + , "This is forbidden to avoid streams which could take 0 or several different" + ++ " values." + , "Try adding some initial elements (e.g., [0,0,0] ++ ...) " + ++ "to the offending streams." + , "Path : " ++ show (reverse vs) ++ "\n" + ] show (DependsOnClosePast vs v w len) = - "Error : the following path is of weight " ++ show w ++ " ending in " - ++ "the external variable " ++ v ++ " while the first variable of that path " - ++ "has a prophecy array of length " ++ show len ++ ", which is strictly greater " - ++ "than the weight. This is forbidden. \n" - ++ "Path : " ++ show (reverse vs) ++ "\n" + unlines + [ "Error : the following path is of weight " ++ show w ++ " ending in " + ++ "the external variable " ++ v + , "while the first variable of that path has a prophecy array of length " + ++ show len ++ "," + , "which is strictly greater than the weight. This is forbidden." + , "Path : " ++ show (reverse vs) ++ "\n" + ] show (DependsOnFuture vs v w) = - "Error : the following path is of weight " ++ show w ++ " which is strictly positive. " - ++ "This means that the first variable depends on the future of the external variable " - ++ v ++ " which is quoted in the last variable of the path. This is obviously impossible. \n" - ++ "Path : " ++ show (reverse vs) ++ "\n" + unlines + [ "Error : the following path is of weight " ++ show w + ++ " which is strictly positive." + , "This means that the first variable depends on the future of the " + ++ "external variable " ++ v + , "which is quoted in the last variable of the path. This is " + ++ "obviously impossible." + , "Path : " ++ show (reverse vs) ++ "\n" + ] (&&>) :: Maybe a -> Maybe a -> Maybe a m &&> m' = @@ -76,15 +135,16 @@ infixr 2 ||> infixr 1 &&> --- | Check a /Copilot/ specification. +-- | Check a /Copilot/ specification. -- If it is not compilable, then returns an error describing the issue. -- Else, returns @Nothing@ check :: StreamableMaps Spec -> Maybe Error -check streams = +check streams = syntaxCheck streams &&> defCheck streams --- Represents all the kind of specs that are authorized after a given operator -data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet deriving Eq +-- Represents all the kind of specs that are authorized after a given operator. +data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet | PArrSet + deriving Eq -- Check that the AST of the copilot specification match the BNF -- Could have been verified by the type checker if the type of Spec had been cut @@ -94,33 +154,35 @@ syntaxCheck streams = foldStreamableMaps (checkSyntaxSpec AllSpecSet) streams Nothing where - checkSyntaxSpec :: Streamable a => SpecSet -> Var -> Spec a -> Maybe Error -> Maybe Error + checkSyntaxSpec :: Streamable a + => SpecSet -> Var -> Spec a -> Maybe Error -> Maybe Error checkSyntaxSpec set v s e = e &&> case s of - PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph Var _ -> Nothing Const _ -> Nothing - F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v &&> - (checkSyntaxSpec FunSpecSet v s0 Nothing) - F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v &&> - (checkSyntaxSpec FunSpecSet v s0 Nothing) &&> - checkSyntaxSpec FunSpecSet v s1 Nothing - F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v &&> - (checkSyntaxSpec FunSpecSet v s0 Nothing) &&> - (checkSyntaxSpec FunSpecSet v s1 Nothing) &&> - checkSyntaxSpec FunSpecSet v s2 Nothing - Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v &&> - checkSyntaxSpec AllSpecSet v s0 Nothing - Drop i s0 -> (0 <= i) ||> BadDrop i v &&> - (checkSyntaxSpec DropSpecSet v s0 Nothing) + PVar _ v' ph -> ph > 0 ||> BadSamplingPhase v v' ph + PArr _ (arr,s0) ph -> checkIndex v arr s0 + &&> ph > 0 ||> BadSamplingArrPhase v arr ph + &&> checkSyntaxSpec PArrSet v s0 Nothing + F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v + &&> checkSyntaxSpec FunSpecSet v s0 Nothing + F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v + &&> checkSyntaxSpec FunSpecSet v s0 Nothing + &&> checkSyntaxSpec FunSpecSet v s1 Nothing + F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v + &&> checkSyntaxSpec FunSpecSet v s0 Nothing + &&> checkSyntaxSpec FunSpecSet v s1 Nothing + &&> checkSyntaxSpec FunSpecSet v s2 Nothing + Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v + &&> checkSyntaxSpec AllSpecSet v s0 Nothing + Drop i s0 -> (0 <= i) ||> BadDrop i v + &&> checkSyntaxSpec DropSpecSet v s0 Nothing + checkIndex _ _ (Var _) = Nothing + checkIndex _ _ (Const _) = Nothing + checkIndex v arr idx = Just $ BadPArrSpec v arr (show idx) --- checks that streams are well defined (ie can be compiled) --- Currently very inefficient (for simplicity's sake), --- could probably be optimized if need be --- by keeping weights of paths in a matrix and doing some linear algebra --- (fast exponentiation could give some nice results) --- could also reuse the dependency graph (see below) +-- | Checks that streams are well defined (i.e., can be compiled). defCheck :: StreamableMaps Spec -> Maybe Error defCheck streams = let checkPathsFromSpec :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error @@ -136,9 +198,22 @@ case s of PVar t v _ -> case () of () | n > 0 -> Just $ DependsOnFuture vs v n - () | n > negate (prophecyArrayLength s0) -> Just $ DependsOnClosePast vs v n (prophecyArrayLength s0) - () | t /= getAtomType s -> Just $ BadType v (head vs) + | n > negate (prophecyArrayLength s0) -> + Just $ DependsOnClosePast vs v n + (prophecyArrayLength s0) + | t /= getAtomType s -> Just $ BadType v (head vs) _ -> Nothing + PArr t (arr, idx) _ + | n > 0 -> Just $ DependsOnFuture vs arr n + | n > negate (prophecyArrayLength idx) -> + Just $ DependsOnClosePast vs arr n + (prophecyArrayLength idx) + | t /= getAtomType s -> Just $ BadType arr (head vs) + | otherwise -> + case idx of + Const _ -> checkPath n vs idx + Var _ -> checkPath n vs idx + _ -> Just $ BadPArrSpec v0 arr (show idx) Var v -> if elem v vs then if n >= 0 @@ -152,37 +227,41 @@ Const _ -> Nothing F _ _ s1 -> checkPath n vs s1 F2 _ _ s1 s2 -> checkPath n vs s1 &&> checkPath n vs s2 - F3 _ _ s1 s2 s3 -> checkPath n vs s1 &&> checkPath n vs s2 &&> checkPath n vs s3 + F3 _ _ s1 s2 s3 -> checkPath n vs s1 &&> checkPath n vs s2 + &&> checkPath n vs s3 Append l s' -> checkPath (n - length l) vs s' Drop i s' -> checkPath (n + i) vs s' - in - foldStreamableMaps checkPathsFromSpec streams Nothing + in foldStreamableMaps checkPathsFromSpec streams Nothing -getAtomType :: Streamable a => Spec a -> A.Type -getAtomType s = - let unitElem = unit - _ = (Const unitElem) `asTypeOf` s -- to help the typechecker - in atomType unitElem +type Exs = (A.Type, Var, ExtVars) -getExternalVars :: StreamableMaps Spec -> [(A.Type, Var, Phase)] +data ExtVars = ExtV Phase + | ExtA Phase String + deriving Eq + +getExternalVars :: StreamableMaps Spec -> [Exs] getExternalVars streams = nub $ foldStreamableMaps decl streams [] where - decl :: Streamable a => Var -> Spec a -> [(A.Type, Var, Phase)] -> [(A.Type, Var, Phase)] + decl :: Streamable a + => Var -> Spec a -> [Exs] -> [Exs] decl _ s ls = case s of - PVar t v ph -> (t, v, ph) : ls + PVar t v ph -> (t, v, ExtV ph) : ls + PArr t (arr, s0) ph -> (t, arr, ExtA ph (show s0)) : ls F _ _ s0 -> decl undefined s0 ls F2 _ _ s0 s1 -> decl undefined s0 $ decl undefined s1 ls - F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1 $ decl undefined s2 ls + F3 _ _ s0 s1 s2 -> decl undefined s0 $ decl undefined s1 + $ decl undefined s2 ls Drop _ s' -> decl undefined s' ls Append _ s' -> decl undefined s' ls _ -> ls + ---- Dependency graphs (for next version of nNWCP, and for scheduling) {- type Weight = Int -data Node = +data Node = InternalVar Var [(Weight, Node)] | ExternalVar Var Phase deriving Show -- for debug diff --git a/Language/Copilot/AtomToC.hs b/Language/Copilot/AtomToC.hs --- a/Language/Copilot/AtomToC.hs +++ b/Language/Copilot/AtomToC.hs @@ -3,8 +3,10 @@ -- | Defines a main() and print statements to easily execute generated Copilot specs. module Language.Copilot.AtomToC(getPrePostCode) where +import Language.Copilot.Compiler (tmpSampleStr) import Language.Copilot.AdHocC import Language.Copilot.Core +import Language.Copilot.Analyser (ExtVars(..)) import qualified Language.Atom as A @@ -13,15 +15,26 @@ -- allExts represents all the variables to monitor (used for declaring them) -- inputExts represents the monitored variables which are to be feed to the standard input of the C program. -- only used for the testing with random streams and values. -getPrePostCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, Phase)] -> Vars -> Period -> (String, String) -getPrePostCode cName streams allExts inputExts p = - (preCode $ extDecls allExts, postCode cName streams allExts inputExts p) +getPrePostCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] + -> [(String,Int)] -> Vars -> Period -> (String, String) +getPrePostCode cName streams allExts arrDecs inputExts p = + (preCode $ extDecls allExts arrDecs, postCode cName streams allExts inputExts p) -- Make the declarations for external vars -extDecls :: [(A.Type, Var, Phase)] -> [String] -extDecls allExtVars = - let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') allExtVars in - map (\ (t, v, _) -> varDecl t [v]) uniqueExtVars +extDecls :: [(A.Type, Var, ExtVars)] -> [(String,Int)] -> [String] +extDecls allExtVars arrDecs = + let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') allExtVars + getDec (t, v, ExtV _) = varDecl t [v] + getDec (t, arr, ExtA _ _) = + case getIdx arr of + Nothing -> error $ "Please use the setArrs option to provide a list of " ++ + "pairs (a,idx) where a is the name of an external array and idx " ++ + "is its static size to declare. There is no size for array " ++ + arr ++ "." + Just idx -> arrDecl t [(arr, idx)] + getIdx arr = lookup arr arrDecs + in + map getDec uniqueExtVars preCode :: [String] -> String preCode extDeclarations = unlines $ @@ -37,7 +50,7 @@ vPre :: Name -> String vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "." -postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, Phase)] -> Vars -> Period -> String +postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, ExtVars)] -> Vars -> Period -> String postCode cName streams allExts inputExts p = unlines $ (if isEmptySM inputExts @@ -102,22 +115,29 @@ decl v l ls = let string = "string_" ++ v in (indent ++ "char " ++ string ++ " [50] = \"\";") : - (indent ++ "fgets (" ++ string ++ ", sizeof(" ++ string ++ "), stdin);") : - (indent ++ "sscanf (" ++ string ++ ", \"" ++ typeId (head l) ++ "\", &" ++ v ++ ");") : + (indent ++ "fgets (" ++ string ++ ", sizeof(" ++ string + ++ "), stdin);") : + (indent ++ "sscanf (" ++ string ++ ", \"" + ++ typeId (head l) ++ "\", &" ++ v ++ ");") : (indent ++ "clean (" ++ string ++ ", stdin);") : ls -sampleExtVars :: [(A.Type, Var, Phase)] -> Name -> [String] +sampleExtVars :: [(A.Type, Var, ExtVars)] -> Name -> [String] sampleExtVars allExts cName = - map sample allExts - where - sample :: (A.Type, Var, Phase) -> String - sample (_, v, ph) = - " " ++ vPre cName ++ "tmpSampleVal__" ++ v ++ "_" ++ show ph ++ " = " ++ v ++ ";" + map (\ext -> let (v,e) = sample ext in + " " ++ vPre cName ++ tmpSampleStr ++ e + ++ " = " ++ v ++ ";") + allExts + where + sample :: (A.Type, Var, ExtVars) -> (Var, String) + sample (_, v, ExtV ph) = (v, tmpVarName v ph) + sample (_, v, ExtA ph idx) = (v ++ "[0]", tmpArrName v ph idx) outputVars :: Name -> StreamableMaps Spec -> [String] outputVars cName streams = foldStreamableMaps decl streams [] where - decl :: forall a. Streamable a => Var -> Spec a -> [String] -> [String] + decl :: forall a. Streamable a + => Var -> Spec a -> [String] -> [String] decl v _ ls = - (" " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ " ") [vPre cName ++ "outputVal__" ++ v]) : ls + (" " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ " ") + [vPre cName ++ "outputVal__" ++ v]) : ls diff --git a/Language/Copilot/Compiler.hs b/Language/Copilot/Compiler.hs --- a/Language/Copilot/Compiler.hs +++ b/Language/Copilot/Compiler.hs @@ -3,36 +3,34 @@ -- Note : for now, the initial state is computed during the first tick -- | Transform the copilot specification in an atom one, and then compile that one. -module Language.Copilot.Compiler(copilotToAtom) where +module Language.Copilot.Compiler(copilotToAtom, tmpSampleStr) where import Language.Copilot.Core -import Data.Word import Data.Maybe import Data.Map as M import Data.List -import Control.Monad (when) +import Control.Monad (when) import qualified Language.Atom as A -import Language.Copilot.Analyser (getAtomType) -getValue :: PhasedValue a -> A.V a -getValue (Ph _ val) = val - -- | Compiles an /Copilot/ specification to an /Atom/ one. --- -- The period is given as a Maybe : if it is Nothing, an optimal period will be chosen. -copilotToAtom :: StreamableMaps Spec -> Sends -> Maybe Period -> Maybe [(Var, String)] -> (Period, A.Atom ()) +copilotToAtom :: StreamableMaps Spec -> Sends -> Maybe Period + -> [(Var, String)] -> (Period, A.Atom ()) copilotToAtom streams sends p triggers = (p', A.period p' $ do - -- Three streamableMaps : - -- prophecy arrays (Int, A.A a), outputs (A.V a), temporary samples (Phase, A.V a) + prophArrs <- mapStreamableMapsM initProphArr streams outputs <- mapStreamableMapsM initOutput streams - tmpSamples <- foldStreamableMaps initTmpSamples streams (return emptySM) + updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty) outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty) + tmpSamples <- foldStreamableMaps (\_ -> initExtSamples streams prophArrs outputIndexes) + streams + (return emptyTmpSamples) + -- One atom rule for each stream foldStreamableMaps (makeRule streams outputs prophArrs tmpSamples updateIndexes outputIndexes) @@ -44,8 +42,10 @@ foldSendableMaps (makeSend outputs) sends (return ()) - -- Sampling of the external variables - sampleVars tmpSamples) + -- Sampling of the external variables. Remove redundancies. + sequence_ $ snd . unzip $ nubBy (\x y -> fst x == fst y) $ + foldStreamableMaps (\_ -> sampleExts tmpSamples) streams [] + ) where optP = getOptimalPeriod streams p' = @@ -75,35 +75,74 @@ _ -> [] initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a) -initOutput v s = streamToUnitValue ("outputVal__" ++ normalizeVar v) s +initOutput v _ = do + atomConstructor ("outputVal__" ++ normalizeVar v) (unit::a) -initTmpSamples :: forall a. Streamable a => Var -> Spec a -> A.Atom TmpSamples -> A.Atom TmpSamples -initTmpSamples _ s tmpSamples = +tmpSampleStr :: String +tmpSampleStr = "tmpSampleVal__" + +initExtSamples :: forall a. Streamable a + => StreamableMaps Spec -> ProphArrs -> Indexes -> Spec a + -> A.Atom TmpSamples -> A.Atom TmpSamples +initExtSamples streams prophArrs outputIndexes s tmpSamples = do case s of Const _ -> tmpSamples - Var _ -> tmpSamples - Drop _ s' -> initTmpSamples undefined s' tmpSamples - Append _ s' -> initTmpSamples undefined s' tmpSamples - F _ _ s0 -> initTmpSamples undefined s0 tmpSamples - F2 _ _ s0 s1 -> initTmpSamples undefined s0 $ - initTmpSamples undefined s1 tmpSamples - F3 _ _ s0 s1 s2 -> initTmpSamples undefined s0 $ - initTmpSamples undefined s1 $ - initTmpSamples undefined s2 tmpSamples + Var _ -> tmpSamples + Drop _ s0 -> initExtSamples' s0 tmpSamples + Append _ s0 -> initExtSamples' s0 tmpSamples + F _ _ s0 -> initExtSamples' s0 tmpSamples + F2 _ _ s0 s1 -> initExtSamples' s0 $ + initExtSamples' s1 tmpSamples + F3 _ _ s0 s1 s2 -> initExtSamples' s0 $ initExtSamples' s1 $ + initExtSamples' s2 tmpSamples PVar _ v ph -> - do + do checkVar v ts <- tmpSamples - let v' = normalizeVar v ++ "_" ++ show ph - maybeElem = (getMaybeElem v' ts)::(Maybe (PhasedValue a)) - name = "tmpSampleVal__" ++ normalizeVar v' + let v' = tmpVarName v ph + vts = tmpVars ts + maybeElem = getMaybeElem v' vts::Maybe (PhasedValueVar a) + name = tmpSampleStr ++ normalizeVar v' case maybeElem of Nothing -> - do - val <- streamToUnitValue name s - let m' = M.insert v' (Ph ph val) (getSubMap ts) - return $ updateSubMap (\_ -> m') ts - Just _ -> return ts -- to avoid duplicates. - -- Beware : crashes if "tmpSamples" instead of "return ts" + do val <- atomConstructor name (unit::a) + let m' = M.insert v' (PhV ph val) (getSubMap vts) + return $ ts {tmpVars = updateSubMap (\_ -> m') vts} + Just _ -> return ts + PArr _ (arr, idx) ph -> + do checkVar arr + ts <- tmpSamples + let arr' = tmpArrName arr ph (show idx) + arrts = tmpArrs ts + idxts = tmpIdxs ts + maybeElem = getMaybeElem arr' arrts::Maybe (PhasedValueArr a) + name = tmpSampleStr ++ normalizeVar arr' + case maybeElem of + Nothing -> -- if the array isn't in the map, neither is the index + do val <- atomConstructor name (unit::a) + let i = case idx of + Const e -> PhIdx $ A.Const e + Var _ -> +-- let B initLen maybeArr = getElem v prophArrs +-- let B initLen maybeArr = +-- case getMaybeElem v prophArrs of +-- Nothing -> +-- error "Error in function initExtSamples." +-- Just x -> x + PhIdx $ nextSt streams prophArrs + undefined outputIndexes idx 0 + _ -> error "Unexpected Spec in initExtSamples." + let m' = M.insert arr' (PhA ph val) (getSubMap arrts) + let m'' = M.insert arr' i (getSubMap idxts) + return $ ts { tmpArrs = updateSubMap (\_ -> m') arrts + , tmpIdxs = updateSubMap (\_ -> m'') idxts + } + Just _ -> return ts + where checkVar v = when (normalizeVar v /= v) + (error $ "Copilot: external variable " ++ v ++ " is not " + ++ "a valid C99 variable.") + initExtSamples' :: Streamable b + => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples + initExtSamples' = initExtSamples streams prophArrs outputIndexes makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes makeUpdateIndex v (B n arr) indexes = @@ -130,7 +169,7 @@ Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom () makeRule streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do r - let B n maybeArr = (getElem v prophArrs)::(BoundedArray a) + let B n maybeArr = getElem v prophArrs::BoundedArray a case maybeArr of Nothing -> -- Fusing together the update and the output if the prophecy array doesn't exist @@ -149,47 +188,92 @@ ((getElem v outputs)::(A.V a)) A.<== arr A.!. (A.VRef outputIndex) outputIndex A.<== (A.VRef outputIndex + A.Const 1) `A.mod_` A.Const (n + 1) - A.phase 1 $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do + -- Spread these out evenly accross the remaining phases, staring no + -- earlier than phase 1. + A.phase ((maxSampleDep v streams) + 1) + $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do updateIndex A.<== (A.VRef updateIndex + A.Const 1) `A.mod_` A.Const (n + 1) --- A.phase 2 $ A.atom ("incrOutputIndex__" ++ normalizeVar v) $ do - - where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0 + +-- | Find the maximum phase as which an array sampling depends on this stream. +-- | Returns zero by default. +maxSampleDep :: Var -> StreamableMaps Spec -> Int +maxSampleDep v streams = + foldStreamableMaps (\_ -> streamDep) streams 0 + where + streamDep :: Streamable b => Spec b -> Int -> Int + streamDep s i = + case s of + Var _ -> i + Const _ -> i + PVar _ _ _ -> i + PArr _ (_, Var v') ph | v == v' -> max ph i + | otherwise -> i + PArr _ _ _ -> i + F _ _ s0 -> streamDep s0 i + F2 _ _ s0 s1 -> streamDep s0 $ streamDep s1 i + F3 _ _ s0 s1 s2 -> streamDep s0 $ streamDep s1 $ streamDep s2 i + Append _ s0 -> streamDep s0 i + Drop _ s0 -> streamDep s0 i makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom () -makeSend outputs name (Send (v, ph, port)) r = - r >> - do +makeSend outputs name (Send (v, ph, port)) r = do + r A.exactPhase ph $ A.atom ("__send_" ++ name) $ send ((A.value (getElem v outputs))::(A.E a)) port -sampleVars :: TmpSamples -> A.Atom () -sampleVars tmpSamples = - sequence_ $ foldStreamableMaps sample tmpSamples [] - where - sample :: Streamable a => Var -> PhasedValue a -> [A.Atom ()] -> [A.Atom ()] - sample v' (Ph ph val) xs = - (A.exactPhase ph $ - A.atom ("sample__" ++ normalizeVar v') $ - val A.<== (A.value $ externalAtomConstructor v) - ) : xs - where - -- TODO : fix this mess - v0 = reverse (tail (dropWhile (\c -> c /= '_') (reverse v'))) - (v1, n_final) = foldl (\ (s, n) c -> - if c == '_' - then (s, n + 1) - else (s ++ underscoreNumber2Symbol n ++ [c],0) - ) ("", 0) v0 - v = v1 ++ underscoreNumber2Symbol n_final - underscoreNumber2Symbol 0 = "" - underscoreNumber2Symbol 1 = "_" - underscoreNumber2Symbol 2 = "." - underscoreNumber2Symbol 3 = "[" - underscoreNumber2Symbol 4 = "]" - underscoreNumber2Symbol _ = undefined +-- What we really should be doing is just folding over the TmpSamples, since +-- that data should contain all the info we need to construct external variable +-- and external array samples. However, there is the issue that for array +-- samples, the type of the index may differ from the type of the array, and +-- having the spec available provides typing coercion. We could fold over the +-- TmpSamples, passing streams in, and extract the appropriate Spec a. +sampleExts :: forall a. Streamable a + => TmpSamples -> Spec a -> [(Var, A.Atom ())] -> [(Var, A.Atom ())] +sampleExts ts s a = do + case s of + Var _ -> a + Const _ -> a + PVar _ v ph -> + let v' = tmpVarName v ph + PhV _ var = getElem v' (tmpVars ts)::PhasedValueVar a in + (v', A.exactPhase ph $ + A.atom ("sample__" ++ v') $ + var A.<== (A.value $ externalAtomConstructor v) + ) : a + PArr _ (arr, idx) ph -> + let arr' = tmpArrName arr ph (show idx) + PhIdx i = getIdx arr' idx (tmpIdxs ts) +-- PhA _ arrV = getElem arr' (tmpArrs ts)::PhasedValueArr a in + PhA _ arrV = case getMaybeElem arr' (tmpArrs ts)::Maybe (PhasedValueArr a) of + Nothing -> error "Error in fucntion sampleExts." + Just x -> x + in + (arr', A.exactPhase ph $ + A.atom ("sample__" ++ arr') $ + arrV A.<== A.array' arr (atomType (unit::a)) A.!. i + ) : a + F _ _ s0 -> sampleExts ts s0 a + F2 _ _ s0 s1 -> sampleExts ts s0 $ sampleExts ts s1 a + F3 _ _ s0 s1 s2 -> sampleExts ts s0 $ sampleExts ts s1 $ + sampleExts ts s2 a + Append _ s0 -> sampleExts ts s0 a + Drop _ s0 -> sampleExts ts s0 a + +-- lookup the idx for external array accesses in the map. +getIdx :: forall a. (Streamable a, A.IntegralE a) + => Var -> Spec a -> StreamableMaps PhasedValueIdx -> PhasedValueIdx a +getIdx arr s ts = + case s of + Var _ -> case getMaybeElem arr ts of + Nothing -> error "Error in function getIdx." + Just x -> x + Const e -> PhIdx $ A.Const e + _ -> error $ "Expecing either a variable or constant for the index " + ++ "in the external array access for array " ++ arr ++ "." + getOptimalPeriod :: StreamableMaps Spec -> Period getOptimalPeriod streams = foldStreamableMaps getMaximumSamplingPhase streams 2 @@ -198,6 +282,7 @@ getMaximumSamplingPhase _ spec n = case spec of PVar _ _ p -> max (p + 1) n + PArr _ _ p -> max (p + 1) n F _ _ s -> getMaximumSamplingPhase "" s n F2 _ _ s0 s1 -> maximum [n, (getMaximumSamplingPhase "" s0 n), diff --git a/Language/Copilot/Core.hs b/Language/Copilot/Core.hs --- a/Language/Copilot/Core.hs +++ b/Language/Copilot/Core.hs @@ -13,20 +13,19 @@ Spec(..), Streams, Stream, Sends, Send(..), DistributedStreams, -- * General functions on 'Streams' and 'StreamableMaps' Streamable(..), Sendable(..), StreamableMaps(..), emptySM, - isEmptySM, getMaybeElem, getElem, streamToUnitValue, + isEmptySM, getMaybeElem, getElem, foldStreamableMaps, foldSendableMaps, mapStreamableMaps, mapStreamableMapsM, - filterStreamableMaps, normalizeVar, getVars, - Vars - -- Compiler - , nextSt, BoundedArray(..), Outputs, TmpSamples - , PhasedValue(..), ProphArrs, Indexes + filterStreamableMaps, normalizeVar, getVars, Vars, + -- compiler + BoundedArray(..), nextSt, Outputs, TmpSamples(..), emptyTmpSamples, + ProphArrs, Indexes, PhasedValueVar(..), PhasedValueArr(..), PhasedValueIdx(..), + tmpVarName, tmpArrName, getAtomType ) where import qualified Language.Atom as A import Data.Int import Data.Word -import Data.Maybe -import Data.List +import Data.List hiding (union) import qualified Data.Map as M import Text.Printf import Control.Monad.Writer @@ -47,18 +46,39 @@ -- | Specification of a stream, parameterized by the type of the values of the stream. -- The only requirement on @a@ is that it should be 'Streamable'. data Spec a where - PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a Var :: Streamable a => Var -> Spec a Const :: Streamable a => a -> Spec a + + PVar :: Streamable a => A.Type -> Var -> Phase -> Spec a + PArr :: (Streamable a, Streamable b, A.IntegralE b) + => A.Type -> (Var, Spec b) -> Phase -> Spec a + F :: (Streamable a, Streamable b) => (b -> a) -> (A.E b -> A.E a) -> Spec b -> Spec a F2 :: (Streamable a, Streamable b, Streamable c) => (b -> c -> a) -> (A.E b -> A.E c -> A.E a) -> Spec b -> Spec c -> Spec a F3 :: (Streamable a, Streamable b, Streamable c, Streamable d) => - (b -> c -> d -> a) -> (A.E b -> A.E c -> A.E d -> A.E a) -> Spec b -> Spec c -> Spec d -> Spec a + (b -> c -> d -> a) -> (A.E b -> A.E c -> A.E d -> A.E a) + -> Spec b -> Spec c -> Spec d -> Spec a + Append :: Streamable a => [a] -> Spec a -> Spec a Drop :: Streamable a => Int -> Spec a -> Spec a +-- These belong in Language.hs, but we don't want orphan instances. +instance (Streamable a, A.NumE a) => Num (Spec a) where + (+) = F2 (+) (+) -- A.NumE a => E a is an instance of Num + (*) = F2 (*) (*) + (-) = F2 (-) (-) + negate = F negate negate + abs = F abs abs + signum = F signum signum + fromInteger i = Const (fromInteger i) + +instance (Streamable a, A.NumE a, Fractional a) => Fractional (Spec a) where + (/) = F2 (/) (/) + recip = F recip recip + fromRational r = Const (fromRational r) + {-# RULES "Copilot.Core appendAppend" forall ls1 ls2 s. Append ls1 (Append ls2 s) = Append (ls1 ++ ls2) s "Copilot.Core dropDrop" forall i1 i2 s. Drop i1 (Drop i2 s) = Drop (i1 + i2) s @@ -70,6 +90,8 @@ instance Eq a => Eq (Spec a) where (==) (PVar t v ph) (PVar t' v' ph') = t == t' && v == v' && ph == ph' + (==) (PArr t (v, idx) ph) (PArr t' (v', idx') ph') = + t == t' && v == v' && show idx == show idx' && ph == ph' (==) (Var v) (Var v') = v == v' (==) (Const x) (Const x') = x == x' (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s' @@ -81,7 +103,6 @@ -- | Container for mutually recursive streams, whose specifications may be -- parameterized by different types ---type Streams = StreamableMaps Spec type Streams = Writer (StreamableMaps Spec) () -- | A named stream type Stream a = Streamable a => (Var, Spec a) @@ -135,13 +156,13 @@ -- for example the booleans are first converted to 0 or 1, and floats and doubles -- have the good precision. showAsC :: a -> String - - -- | To make customer C triggers. Only for Spec Bool (others through an error). - makeTrigger :: Maybe [(Var, String)] -> StreamableMaps Spec + + -- | To make customer C triggers. Only for Spec Bool (others throw an error). + -- XXX make them throw errors! + makeTrigger :: [(Var, String)] -> StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom () - class Streamable a => Sendable a where send :: A.E a -> Port -> A.Atom () @@ -160,10 +181,8 @@ A.cond (nextSt streams prophArrs tmpSamples outputIndexes s 0) A.call trig) else return () - where trigs = case triggers of - Nothing -> [] - Just t -> t - trig = case M.lookup v (M.fromList trigs) of + where + trig = case M.lookup v (M.fromList triggers) of Nothing -> "" Just fn -> fn @@ -176,7 +195,7 @@ typeId _ = "%d" atomType _ = A.Int8 showAsC x = printf "%d" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int16 where getSubMap = i16Map updateSubMap f sm = sm {i16Map = f $ i16Map sm} @@ -186,7 +205,7 @@ typeId _ = "%d" atomType _ = A.Int16 showAsC x = printf "%d" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int32 where getSubMap = i32Map updateSubMap f sm = sm {i32Map = f $ i32Map sm} @@ -196,7 +215,7 @@ typeId _ = "%d" atomType _ = A.Int32 showAsC x = printf "%d" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Int64 where getSubMap = i64Map updateSubMap f sm = sm {i64Map = f $ i64Map sm} @@ -206,7 +225,7 @@ typeId _ = "%lld" atomType _ = A.Int64 showAsC x = printf "%d" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word8 where getSubMap = w8Map updateSubMap f sm = sm {w8Map = f $ w8Map sm} @@ -216,7 +235,7 @@ typeId _ = "%u" atomType _ = A.Word8 showAsC x = printf "%u" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word16 where getSubMap = w16Map updateSubMap f sm = sm {w16Map = f $ w16Map sm} @@ -226,7 +245,7 @@ typeId _ = "%u" atomType _ = A.Word16 showAsC x = printf "%u" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word32 where getSubMap = w32Map updateSubMap f sm = sm {w32Map = f $ w32Map sm} @@ -236,7 +255,7 @@ typeId _ = "%u" atomType _ = A.Word32 showAsC x = printf "%u" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Word64 where getSubMap = w64Map updateSubMap f sm = sm {w64Map = f $ w64Map sm} @@ -246,7 +265,7 @@ typeId _ = "%llu" atomType _ = A.Word64 showAsC x = printf "%u" (toInteger x) - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Float where getSubMap = fMap updateSubMap f sm = sm {fMap = f $ fMap sm} @@ -257,7 +276,7 @@ typeIdPrec _ = "%.5f" atomType _ = A.Float showAsC x = printf "%.5f" x - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Streamable Double where getSubMap = dMap updateSubMap f sm = sm {dMap = f $ dMap sm} @@ -268,7 +287,7 @@ typeIdPrec _ = "%.10lf" atomType _ = A.Double showAsC x = printf "%.10f" x - makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + makeTrigger _ _ _ _ _ _ _ r = r >> return () instance Sendable Word8 where send e port = @@ -284,41 +303,45 @@ -- Launch an exception if the index is not in it {-# INLINE getElem #-} getElem :: Streamable a => Var -> StreamableMaps b -> b a -getElem v sm = fromJust $ getMaybeElem v sm +getElem v sm = case getMaybeElem v sm of + Nothing -> error "Error in application of getElem from Core.hs." + Just x -> x --- | Just produce an @Atom@ value named after its first argument, --- with an unspecified value. The second argument only coerces the type, it is discarded -{-# INLINE streamToUnitValue #-} -streamToUnitValue :: Streamable a => Var -> Spec a -> A.Atom (A.V a) -streamToUnitValue v _ = atomConstructor v unit +getAtomType :: Streamable a => Spec a -> A.Type +getAtomType s = + let unitElem = unit + _ = (Const unitElem) `asTypeOf` s -- to help the typechecker + in atomType unitElem -- | This function is used to iterate on all the values in all the maps stored -- by a @'StreamableMaps'@, accumulating a value over time {-# INLINE foldStreamableMaps #-} foldStreamableMaps :: forall b c. - (forall a. Streamable a => Var -> c a -> b -> b) -> + (Streamable a => Var -> c a -> b -> b) -> StreamableMaps c -> b -> b foldStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc = - let acc0 = M.foldWithKey f acc bm - acc1 = M.foldWithKey f acc0 i8m - acc2 = M.foldWithKey f acc1 i16m - acc3 = M.foldWithKey f acc2 i32m - acc4 = M.foldWithKey f acc3 i64m - acc5 = M.foldWithKey f acc4 w8m - acc6 = M.foldWithKey f acc5 w16m - acc7 = M.foldWithKey f acc6 w32m - acc8 = M.foldWithKey f acc7 w64m - acc9 = M.foldWithKey f acc8 fm - acc10 = M.foldWithKey f acc9 dm + let acc0 = M.foldrWithKey f acc bm + acc1 = M.foldrWithKey f acc0 i8m + acc2 = M.foldrWithKey f acc1 i16m + acc3 = M.foldrWithKey f acc2 i32m + acc4 = M.foldrWithKey f acc3 i64m + acc5 = M.foldrWithKey f acc4 w8m + acc6 = M.foldrWithKey f acc5 w16m + acc7 = M.foldrWithKey f acc6 w32m + acc8 = M.foldrWithKey f acc7 w64m + acc9 = M.foldrWithKey f acc8 fm + acc10 = M.foldrWithKey f acc9 dm in acc10 +-- XXX only sends Word8s right now -- | This function is used to iterate on all the values in all the maps stored -- by a @'StreamableMaps'@, accumulating a value over time {-# INLINE foldSendableMaps #-} foldSendableMaps :: forall b c. (forall a. Sendable a => Var -> c a -> b -> b) -> StreamableMaps c -> b -> b -foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc = +--foldSendableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) acc = +foldSendableMaps f (SM _ _ _ _ _ w8m _ _ _ _ _) acc = let acc1 = M.foldWithKey f acc w8m in acc1 @@ -343,7 +366,7 @@ {-# INLINE mapStreamableMapsM #-} mapStreamableMapsM :: forall s s' m. Monad m => - (forall a. Streamable a => Var -> s a -> m (s' a)) -> + (Streamable a => Var -> s a -> m (s' a)) -> StreamableMaps s -> m (StreamableMaps s') mapStreamableMapsM f sm = foldStreamableMaps ( @@ -353,12 +376,11 @@ return $ updateSubMap (\ m -> M.insert v s' m) sm' ) sm (return emptySM) --- | Only keeps in @sm@ the values whose key+type are in @l@. --- Also returns a bool saying whether all the elements in sm --- were in l. --- Works even if some elements in @l@ are not in @sm@. --- Not optimised at all -filterStreamableMaps :: forall c. StreamableMaps c -> [(A.Type, Var, Phase)] -> (StreamableMaps c, Bool) +-- | Only keeps in @sm@ the values whose key+type are in @l@. Also returns a +-- bool saying whether all the elements in sm were in l. Works even if some +-- elements in @l@ are not in @sm@. Not optimised at all. +filterStreamableMaps :: + forall c b. StreamableMaps c -> [(A.Type, Var, b)] -> (StreamableMaps c, Bool) filterStreamableMaps sm l = let (sm2, l2) = foldStreamableMaps filterElem sm (emptySM, []) in (sm2, (l' \\ nub l2) == []) @@ -443,10 +465,16 @@ M.null fm && M.null dm --- | Replace all accepted special characters by sequences of underscores +-- | Replace all accepted special characters by sequences of underscores. normalizeVar :: Var -> Var normalizeVar v = - foldl (\ acc c -> acc ++ case c of '.' -> "__" ; '[' -> "___" ; ']' -> "____" ; _ -> [c]) "" v + foldl (\ acc c -> acc ++ case c of + '.' -> "_" + '[' -> "_" + ']' -> "_" + ' ' -> "_" + _ -> [c]) + "" v -- | For each typed variable, this type holds all its successive values in an infinite list -- Beware : each element of one of those lists corresponds to a full @Atom@ period, @@ -465,6 +493,8 @@ showRaw :: Spec a -> Int -> String showRaw (PVar t v ph) _ = "PVar " ++ show t ++ " " ++ v ++ " " ++ show ph +showRaw (PArr t (v, idx) ph) _ = + "PArr " ++ show t ++ " (" ++ v ++ " ! (" ++ show idx ++ ")) " ++ show ph showRaw (Var v) _ = "Var " ++ v showRaw (Const e) _ = "Const " ++ show e showRaw (F _ _ s0) n = @@ -492,28 +522,57 @@ (concat $ replicate n " ") ++ ")" --- Compiler: the code below really belongs in Core.hs, but its called by + +-- Compiler: the code below really belongs in Compiler.hs, but its called by -- makeTrigger, which is a method of the class Streamable. +-- For the prophecy arrays type ArrIndex = Word64 - type ProphArrs = StreamableMaps BoundedArray type Outputs = StreamableMaps A.V -type TmpSamples = StreamableMaps PhasedValue type Indexes = M.Map Var (A.V ArrIndex) -data PhasedValue a = Ph Phase (A.V a) --- important invariant : the maybe is Nothing iff the int is 0 -data BoundedArray a = B ArrIndex (Maybe (A.A a)) -getValue :: PhasedValue a -> A.V a -getValue (Ph _ val) = val +-- External variables +data PhasedValueVar a = PhV Phase (A.V a) +--type TmpVarSamples = StreamableMaps PhasedValueVar +tmpVarName :: Var -> Phase -> Var +tmpVarName v ph = normalizeVar v ++ "_" ++ show ph + + +-- External arrays +data PhasedValueArr a = PhA Phase (A.V a) -- Array name. +data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. + +data TmpSamples = + TmpSamples { tmpVars :: StreamableMaps PhasedValueVar + , tmpArrs :: StreamableMaps PhasedValueArr + , tmpIdxs :: StreamableMaps PhasedValueIdx + } + +emptyTmpSamples :: TmpSamples +emptyTmpSamples = TmpSamples emptySM emptySM emptySM + +tmpArrName :: Var -> Phase -> String -> Var +tmpArrName v ph idx = (tmpVarName v ph) ++ "_" ++ normalizeVar idx + +data BoundedArray a = B ArrIndex (Maybe (A.A a)) + nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -> Spec a -> ArrIndex -> A.E a -nextSt streams prophArrs tmpSamples outputIndexes s index = +nextSt streams prophArrs tmpSamples outputIndexes s index = case s of - PVar _ v ph -> A.value . getValue - $ getElem (normalizeVar v ++ "_" ++ show ph) tmpSamples + PVar _ v ph -> + let PhV _ var = getElem (tmpVarName v ph) (tmpVars tmpSamples) in + A.value var + PArr _ (v, idx) ph -> + let PhA _ var = e tmp (tmpArrs tmpSamples) + tmp = tmpArrName v ph (show idx) + e a b = case getMaybeElem a b of + Nothing -> + error "Error in application of getElem in nextSt." + Just x -> x + in A.value var Var v -> let B initLen maybeArr = getElem v prophArrs in -- This check is extremely important -- It means that if x at time n depends on y at time n @@ -521,22 +580,31 @@ -- so it increases the size of code (sadly), -- but is the only thing preventing race conditions from occuring if index < initLen - -- if maybeArr == Nothing, then initLen == 0 and is <= index - then - let outputIndex = fromJust $ M.lookup v outputIndexes in - (fromJust maybeArr) A.!. - ((A.Const index + A.VRef outputIndex) `A.mod_` - (A.Const (initLen + 1))) - else next (getElem v streams) (index - initLen) + then getVar v initLen maybeArr + else let s0 = getElem v streams in + next s0 (index - initLen) Const e -> A.Const e F _ f s0 -> f $ next s0 index F2 _ f s0 s1 -> - f (next s0 index) (next s1 index) + f (next s0 index) + (next s1 index) F3 _ f s0 s1 s2 -> - f (next s0 index) (next s1 index) (next s2 index) - Append _ s' -> next s' index - Drop i s' -> next s' (fromInteger (toInteger i) + index) + f (next s0 index) + (next s1 index) + (next s2 index) + Append _ s0 -> next s0 index + Drop i s0 -> next s0 (fromInteger (toInteger i) + index) where next :: Streamable b => Spec b -> ArrIndex -> A.E b - next = nextSt streams prophArrs tmpSamples outputIndexes - + next = nextSt streams prophArrs tmpSamples outputIndexes + getVar :: Streamable a + => Var -> ArrIndex -> Maybe (A.A a) -> A.E a + getVar v initLen maybeArr = + let outputIndex = case M.lookup v outputIndexes of + Nothing -> error "Error in function getVar." + Just x -> x + arr = case maybeArr of + Nothing -> error "Error in function getVar (maybeArr)." + Just x -> x in + arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_` + (A.Const (initLen + 1))) diff --git a/Language/Copilot/Dispatch.hs b/Language/Copilot/Dispatch.hs --- a/Language/Copilot/Dispatch.hs +++ b/Language/Copilot/Dispatch.hs @@ -8,7 +8,8 @@ -- 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 +module Language.Copilot.Dispatch + (dispatch, BackEnd(..), AtomToC(..), Interpreted(..), Iterations, Verbose(..)) where import Language.Copilot.Core import Language.Copilot.Analyser @@ -34,13 +35,16 @@ , 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 :: Maybe [(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)@. + , 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." } @@ -69,19 +73,19 @@ dispatch streams sends inputExts backEnd iterations verbose = do hSetBuffering stdout LineBuffering - when isVerbose $ mapM_ putStrLn preludeText + 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 + let interpretedLines = showVars (interpretStreams streams trueInputExts) + iterations in case backEnd of Interpreter -> do - when (not allInputsPresents) $ error - "the interpreter don't have the values for some of the external variables" + when (not allInputsPresents) $ error errMsg mapM_ putStrLn interpretedLines Opts opts -> let isInterpreted = @@ -90,30 +94,35 @@ NotInterpreted -> False dirName = outputDir opts in do - putStrLn $ "Trying to create (if missing) " ++ dirName ++ " ..." + 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 - let copy ext = copyFile (cName opts ++ ext) (dirName ++ cName opts ++ ext) + -- 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 ++ " ..." + 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 - "The interpreter doesn't have the values for some of the external variables." - when isExecuted $ execute streams (dirName ++ cName opts) trueInputExts isInterpreted + 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 @@ -121,8 +130,8 @@ (trueInputExts, allInputsPresents) = filterStreamableMaps inputExts allExts -- Check that each trigger references an actual Copilot variable of type Bool. -checkTriggerVars :: StreamableMaps Spec -> Maybe [(Var, String)] -> IO () -checkTriggerVars streams triggers = +checkTriggerVars :: StreamableMaps Spec -> [(Var, String)] -> IO () +checkTriggerVars streams trigs = if null badDefs then if null badTypes then return () @@ -132,24 +141,22 @@ 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 bareTriggers \\ getVars streams + 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 bareTriggers) then (v, t):ls else ls + in if t /= A.Bool && v `elem` (map fst trigs) then (v, t):ls else ls badTypes = foldStreamableMaps listAtomTypes streams [] - bareTriggers = - case triggers of - Nothing -> [] - Just t -> t -copilotToC :: StreamableMaps Spec -> Sends -> [(A.Type, Var, Phase)] -> Vars - -> Name -> Maybe Period -> Maybe (String, String) -> Maybe [(Var, String)] -> Bool -> IO () -copilotToC streams sends allExts trueInputExts cFileName p prePostC triggers isVerbose = - let (p', program) = copilotToAtom streams sends p triggers +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 prePostC of - Nothing -> getPrePostCode cFileName streams allExts trueInputExts p' + 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), @@ -159,10 +166,28 @@ in do putStrLn $ "Compiling Copilot specs to C ..." (sched, _, _, _, _) <- A.compile cFileName atomConfig program - if isVerbose + 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 = @@ -245,18 +270,16 @@ (s', vs') preludeText :: [String] --- XXX TODO : fill the blanks in the text below preludeText = - [ "=================================================================" - , " CoPilot, a stream language for generating " - , " hard real-time C monitors." - , "=================================================================" - , "Built on the Atom, for generating deterministic time and space" - , "embedded C programs." + [ "" + , "=========================================================================" + , " CoPilot, a stream language for generating hard real-time C monitors. " + , "=========================================================================" + , "Copyright, Galois, Inc. 2010" , "BSD3 License" - , "" - , "" - , "Lee Pike, Robin Morisset, and Sebastian Niller" - , "Usage: " + , "Website: http://leepike.github.com/Copilot/" + , "Maintainer: Lee Pike (remove dashes)." + , "Usage: > help" + , "=========================================================================" , "" ] diff --git a/Language/Copilot/Examples/Examples.hs b/Language/Copilot/Examples/Examples.hs --- a/Language/Copilot/Examples/Examples.hs +++ b/Language/Copilot/Examples/Examples.hs @@ -4,8 +4,8 @@ import Data.Word import Prelude (($)) -import qualified Prelude as P import qualified Prelude as Prelude +import qualified Prelude as P -- for specifying options import Data.Map (fromList) @@ -13,14 +13,9 @@ import System.Random import Data.Int -import Language.Copilot.Core -import Language.Copilot.Language -import Language.Copilot.Interface +import Language.Copilot import Language.Copilot.Variables -import Language.Copilot.PrettyPrinter -import Language.Copilot.Libs.LTL - fib :: Streams fib = do "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib") @@ -43,7 +38,7 @@ t3 :: Streams t3 = do a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1 - b .= [True, False] ++ 2 + var a < 5 + extW32 "ext" 1 + b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1 t4 :: Streams t4 = do @@ -186,3 +181,29 @@ -- "loop1" .= [0] ++ varI32 "loop2" + 2 -- "loop2" .= [1] ++ varI32 "loop1" - 1 -- "other" .= drop 3 (varI32 "loop1") + +-- testing external array references +testArr :: Streams +testArr = do + -- a .= [True] ++ extArrB ("ff", varW16 b) 5 && extArrB ("ff", varW16 b) 1 + -- && extArrB ("ff", varW16 b) 2 + -- b .= [7] ++ varW16 b + const 3 + extArrW16 ("gg", varW16 f) 2 + -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4 + -- c .= [True] ++ var c + -- d .= varB c + e .= varW16 g -- + extArrW16 ("gg", varW16 b) 2 +-- f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 + g .= extArrW16 ("gg", varW16 e) 2 + -- h .= [0] ++ drop 1 (varW16 g) + + +-- t3 :: use an external variable called ext, typed Word32 +t99 :: Streams +t99 = do + a .= [0,1] ++ (var a) + extW32 "ext" 8 + extW32 "ext" 8 + extW32 "ext" 1 + b .= [True, False] ++ 2 + var a < 5 + extW32 "_ext" 1 + +-- test external idx before after and in the stream it references +-- test multiple defs +-- test defs in functions +-- test arrays at different indexes diff --git a/Language/Copilot/Examples/LTLExamples.hs b/Language/Copilot/Examples/LTLExamples.hs --- a/Language/Copilot/Examples/LTLExamples.hs +++ b/Language/Copilot/Examples/LTLExamples.hs @@ -4,42 +4,39 @@ import Prelude (replicate, Int) -import Language.Copilot.Core -import Language.Copilot.Language +import Language.Copilot import Language.Copilot.Variables -import Language.Copilot.Libs.LTL -import Language.Copilot.Libs.Indexes ---------------- -- LTL tests --- ---------------- -test, output :: Var -test = "test" +testing, output :: Var +testing = "test" output = "output" -- Can be tested with various values of n. Use the interpreter to see the outputs. tSoonest :: Int -> Streams -tSoonest n = do test .= (replicate (n+2) False) ++ const True - output .= soonest n (var test) +tSoonest n = do testing .= (replicate (n+2) False) ++ const True + output .= soonest n (var testing) tLatest :: Int -> Streams -tLatest n = do test .= (replicate (n-2) False) ++ const True - output .= latest n (var test) +tLatest n = do testing .= (replicate (n-2) False) ++ const True + output .= latest n (var testing) tAlways :: Int -> Streams -tAlways n = do test .= (replicate (n+3) True) ++ const False - output .= always n (varB test) +tAlways n = do testing .= (replicate (n+3) True) ++ const False + output .= always n (varB testing) tFuture :: Int -> Streams -tFuture n = do test .= (replicate (n+3) False) ++ varB a +tFuture n = do testing .= (replicate (n+3) False) ++ varB a a .= [False] ++ not (var a) - output .= eventually n (varB test) + output .= eventually n (varB testing) tUntil :: Int -> Streams diff --git a/Language/Copilot/Examples/PTLTLExamples.hs b/Language/Copilot/Examples/PTLTLExamples.hs --- a/Language/Copilot/Examples/PTLTLExamples.hs +++ b/Language/Copilot/Examples/PTLTLExamples.hs @@ -4,12 +4,8 @@ import Prelude () -import Language.Copilot.Core -import Language.Copilot.Language -import Language.Copilot.Interface +import Language.Copilot import Language.Copilot.Variables -import Language.Copilot.PrettyPrinter -import Language.Copilot.Libs.PTLTL -- Next examples are for testing of the ptLTL library diff --git a/Language/Copilot/Help.hs b/Language/Copilot/Help.hs --- a/Language/Copilot/Help.hs +++ b/Language/Copilot/Help.hs @@ -11,12 +11,14 @@ , "There are 4 essential Copilot commands. Each command may take a variety" , "of options. We describe the commands then list the possible options." , "" + , " interpret :: Streams -> Int -> Options -> IO ()" , " > interpret STREAMS RNDS [$ OPTS] baseOpts" , " Executes the interpreter for the Copilot specification STREAMS of type" , " 'Streams', where the specification is interpreted as a set of mutually-" , " recursive Haskell infinite lists. The output from the lists is given" , " for RNDS indexes. RNDS must be greater than 0." , "" + , " compile :: Streams -> String -> Options -> IO ()" , " > compile STREAMS FILENAME [$ OPTS] baseOpts" , " Compiles the Copilot specification STREAMS to constant-time & constant-" , " constant-space C program named FILENAME.c with header FILENAME.h" @@ -28,13 +30,15 @@ , " the interpreter over RNDS rounds. RNDS must be greater than 0. This" , " command is equivalent to executing the interpret command and the" , " compile command for a randomly-generated stream and comparing the" - , " results by-hand. Throws an error if the outputs differ." + , " results by-hand. Throws an error if the outputs differ. Testing" + , " external arrays is currently not supported." , "" , " > Prelude.putStr $ Prelude.show STREAMS -- or simply" , " > STREAMS -- in ghci" , " Pretty-prints the parsed Copilot specification of type 'Streams'." , "" - , " > verify PATH/FILE.c" + , " verify :: FilePath -> Int -> IO () (FilePath is a synonym for String)" + , " > verify PATH/FILE.c n" , " Calls cbmc, developed by Daniel Kroening \& Edmund Clarke" , " on a C file generated by Copilot." , " cbmc is a bounded model-checker that verifies C programs. While there" @@ -43,9 +47,12 @@ , " checks that there are no buffer overflows (both lower and upper), that" , " there are no pointer deferences of NULL, that there is no division by" , " zero, that floating point computations do not result in not-a-number" - , " (NaN), and that no uninitialized local variables are used. For more" - , " information on the properties checked, see" - , " ." + , " (NaN), and that no uninitialized local variables are used. The entry" + , " point of main() is assumed, and it is also assumed that main() can be" + , " unrolled at least n times, where n is an Int. This command is thus" + , " best used when generating a simulation program (i.e., the setPP flag" + , " is not used when compiling). For more information on the properties" + , " checked, see ." , "" , " > help " , " Displays this help message." @@ -127,6 +134,12 @@ , " setTriggers MUST be used in conjunction with the setPP option, as the" , " simulator does not know about custom trigger functions." , "" + , " setArrs :: [(String,Int)] -> Options -> Options (c)" + , " default: Nothing" + , " 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." + , "" , " setO :: Name -> Options -> Options (t)" , " default: \"copilotProgram\"" , " Sets the name of the executable (e.g., -o) generated by the C" @@ -141,7 +154,7 @@ , " Interprets t0 for 50 iterations." , "" , " > interpret t3 40" - , " $ setE setE (emptySM {w32Map = fromList " + , " $ setE (emptySM {w32Map = fromList " , " [ (\"ext0\", [0,1..])" , " , (\"ext1\", [3,3..])]})" , " $ setV Verbose baseOpts" diff --git a/Language/Copilot/Interface.hs b/Language/Copilot/Interface.hs --- a/Language/Copilot/Interface.hs +++ b/Language/Copilot/Interface.hs @@ -2,7 +2,7 @@ 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, + , setDir, setGCC, setTriggers, setArrs, module Language.Copilot.Dispatch ) where @@ -16,7 +16,6 @@ import Data.List ((\\)) import System.Random import System.Exit -import System.FilePath (takeBaseName) import System.Cmd import Data.Maybe import Control.Monad @@ -36,17 +35,21 @@ optCompiler :: String, -- ^ The C compiler to use, as a path to the executable. optOutputDir :: String, -- ^ Where to place the output C files (.c, .h, and binary). optPrePostCode :: Maybe (String, String), -- ^ Code to append above and below the C file. - optTriggers :: Maybe [(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)@. There - -- should be no more than one - -- function per trigger variable. - -- Triggers fire in the same phase (1) - -- that output vars are assigned. + optTriggers :: [(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)@. There + -- should be no more than one function + -- per trigger variable. Triggers fire + -- in the same phase (1) that output + -- vars are assigned. + optArrs :: [(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." } baseOpts :: Options @@ -64,7 +67,8 @@ optCompiler = "gcc", optOutputDir = "./", optPrePostCode = Nothing, - optTriggers = Nothing + optTriggers = [], + optArrs = [] } -- Functions for making it easier for configuring copilot in the frequent use cases @@ -80,8 +84,8 @@ compile streams fileName opts = interface $ setC "-Wall" $ setO fileName $ opts {optStreams = Just streams} -verify :: FilePath -> IO () -verify file = do +verify :: FilePath -> Int -> IO () +verify file n = do putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke " putStrLn ", with the following checks:" putStrLn " --bounds-check enable array bounds checks" @@ -90,7 +94,7 @@ 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 $ " assuming main() as the entry point:" putStrLn cmd code <- system cmd case code of @@ -99,24 +103,21 @@ 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 " + putStrLn "does not exist. See " putStrLn "for more information on cbmc." - where theMain = takeBaseName file - cmd = unwords ("cbmc" : args) + where cmd = unwords ("cbmc" : args) args = ["--div-by-zero-check", "--overflow-check", "--bounds-check" , "--nan-check", "--pointer-check" - , "--function " ++ theMain, file] + , "--unwind " ++ show n, file] - -- Small functions for easy modification of the Options record setS :: DistributedStreams -> Options -> Options setS (streams, sends) opts = opts {optStreams = Just streams, optSends = sends} --- | Sets the environment for simulation by giving a mapping of external variables to lists of values. E.g., +-- | Sets the environment for simulation by giving a mapping of external +-- variables to lists of values. E.g., -- -- @ setE (emptySM {w32Map = fromList [(\"ext\", [0,1..])]}) ... @ -- @@ -124,6 +125,9 @@ setE :: Vars -> Options -> Options setE vs opts = opts {optExts = Just vs} +setArrs :: [(String,Int)] -> Options -> Options +setArrs ls opts = opts {optArrs = ls} + -- | Sets the options for the compiler, e.g., -- -- @ setC \"-O2\" ... @ @@ -177,12 +181,12 @@ -- | Give C function triggers for Copilot Boolean streams. The tiggers fire if -- the stream becoms true. setTriggers :: [(Var, String)] -> Options -> Options -setTriggers triggers opts = +setTriggers trigs opts = if null repeats - then opts {optTriggers = Just triggers} + then opts {optTriggers = trigs} else error $ "Error: only one trigger per Copilot variable. Variables " ++ show (Set.fromList repeats) ++ " are given multiple triggers." - where vars = map fst triggers + where vars = map fst trigs repeats = vars \\ Set.toList (Set.fromList vars) -- | The "main" function @@ -236,7 +240,8 @@ outputDir = optOutputDir opts, compiler = optCompiler opts, prePostCode = optPrePostCode opts, - triggers = optTriggers opts + triggers = optTriggers opts, + arrDecs = optArrs opts } help :: IO () diff --git a/Language/Copilot/Interpreter.hs b/Language/Copilot/Interpreter.hs --- a/Language/Copilot/Interpreter.hs +++ b/Language/Copilot/Interpreter.hs @@ -1,12 +1,8 @@ --- | This interpreter is mostly used for checking the /Copilot/ implementation. --- But it can also be used for quick testing of a /Copilot/ design +-- | The Copilot interpreter. module Language.Copilot.Interpreter(interpretStreams) where import Language.Copilot.Core -import Data.List -import Prelude - -- | The main function of this module. -- It takes a /Copilot/ specification, the values of the monitored values, -- and returns the values of the streams. @@ -18,17 +14,18 @@ interpret :: Streamable a => Vars -> Vars -> Spec a -> [a] interpret inVs moVs s = - case s of - Const c -> repeat c - Var v -> getElem v inVs - PVar _ v _ -> getElem v moVs - Append ls s' -> ls ++ interpret inVs moVs s' - Drop i s' -> drop i $ interpret inVs moVs s' - F f _ s' -> map f (interpret inVs moVs s') - F2 f _ s0 s1 -> zipWith f - (interpret inVs moVs s0) - (interpret inVs moVs s1) - F3 f _ s0 s1 s2 -> zipWith3 f - (interpret inVs moVs s0) - (interpret inVs moVs s1) - (interpret inVs moVs s2) + case s of + Const c -> repeat c + Var v -> getElem v inVs + PVar _ v _ -> getElem v moVs + PArr _ (v,s') _ -> map (\i -> (getElem v moVs) !! fromIntegral i) + (interpret inVs moVs s') + Append ls s' -> ls ++ interpret inVs moVs s' + Drop i s' -> drop i $ interpret inVs moVs s' + F f _ s' -> map f (interpret inVs moVs s') + F2 f _ s0 s1 -> zipWith f (interpret inVs moVs s0) + (interpret inVs moVs s1) + F3 f _ s0 s1 s2 -> zipWith3 f + (interpret inVs moVs s0) + (interpret inVs moVs s1) + (interpret inVs moVs s2) diff --git a/Language/Copilot/Language.hs b/Language/Copilot/Language.hs --- a/Language/Copilot/Language.hs +++ b/Language/Copilot/Language.hs @@ -23,6 +23,9 @@ -- * The next functions provide easier access to typed external variables. extB, extI8, extI16, extI32, extI64, extW8, extW16, extW32, extW64, extF, extD, + -- * The next functions provide easier access to typed external arrays. + extArrB, extArrI8, extArrI16, extArrI32, extArrI64, + extArrW8, extArrW16, extArrW32, extArrW64, extArrF, extArrD, -- * Set of operators from which to choose during the generation of random streams opsF, opsF2, opsF3, -- * Constructs of the copilot language @@ -42,12 +45,10 @@ import qualified Language.Atom as A import Data.Int import Data.Word -import Data.Monoid -import Data.List(elem) import System.Random import qualified Data.Map as M -import Prelude ( Fractional((/)), Bool(..), Num(..), Float, Double - , Fractional(..), fromInteger, fail, zip, (>>=), Show(..), error, ($)) +import Prelude ( Bool(..), Num(..), Float, Double + , Fractional(..), fromInteger, zip, Show(..), Integer) import qualified Prelude as P import Control.Monad.Writer @@ -60,30 +61,20 @@ not :: Spec Bool -> Spec Bool not = F P.not A.not_ -instance (Streamable a, A.NumE a) => P.Num (Spec a) where - (+) = F2 (P.+) (P.+) -- A.NumE a => E a is an instance of Num - (*) = F2 (P.*) (P.*) - (-) = F2 (P.-) (P.-) - negate = F P.negate P.negate - abs = F P.abs P.abs - signum = F P.signum P.signum - fromInteger i = Const (P.fromInteger i) -instance (Streamable a, A.NumE a, P.Fractional a) => P.Fractional (Spec a) where - (/) = F2 (P./) (P./) - recip = F P.recip P.recip - fromRational r = Const (P.fromRational r) - -- | Beware : crash without any possible recovery if a division by 0 happens. -- Same risk with mod. Use div0 and mod0 if unsure. mod, div :: (Streamable a, A.IntegralE a) => Spec a -> Spec a -> Spec a mod = F2 P.mod A.mod_ div = F2 P.mod A.div_ --- | As mod and div, except that if the division would be by 0, it is instead by the first argument. +-- | As mod and div, except that if the division would be by 0, the first +-- argument is used as a default. mod0, div0 :: (Streamable a, A.IntegralE a) => a -> Spec a -> Spec a -> Spec a -mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d else x0 `P.div` x1) (\ e0 e1 -> A.mod0_ e0 e1 d) -div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d else x0 `P.mod` x1) (\ e0 e1 -> A.div0_ e0 e1 d) +mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d + else x0 `P.div` x1) (\ e0 e1 -> A.mod0_ e0 e1 d) +div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d + else x0 `P.mod` x1) (\ e0 e1 -> A.div0_ e0 e1 d) (<), (<=), (>=), (>) :: (Streamable a, A.OrdE a) => Spec a -> Spec a -> Spec Bool (<) = F2 (P.<) (A.<.) @@ -114,22 +105,27 @@ A.Retype P.. A.ue P.. (`A.mod_` (65536::(A.E Word64))) P.. A.Retype P.. A.ue) instance CastIntTo Word32 where cast = F (P.fromInteger P.. P.toInteger) ( - A.Retype P.. A.ue P.. (`A.mod_` ((2 P.^ 32)::(A.E Word64))) P.. A.Retype P.. A.ue) + A.Retype P.. A.ue P.. (`A.mod_` ((2 P.^ (32::Integer))::(A.E Word64))) P.. A.Retype P.. A.ue) instance CastIntTo Word64 where cast = F (P.fromInteger P.. P.toInteger) (A.Retype P.. A.ue) instance CastIntTo Int8 where cast = F (P.fromInteger P.. P.toInteger) ( - A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) + A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) + `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) instance CastIntTo Int16 where cast = F (P.fromInteger P.. P.toInteger) ( - A.Retype P.. A.ue P.. (\x -> ((x P.+ ((2 P.^15)::(A.E Word64))) `A.mod_` (2 P.^ 16)) P.- (2 P.^ 15)) P.. A.Retype P.. A.ue) + A.Retype P.. A.ue P.. (\x -> ((x P.+ ((2 P.^ (15::Integer))::(A.E Word64))) + `A.mod_` (2 P.^ (16::Integer))) P.- (2 P.^ (15::Integer))) + P.. A.Retype P.. A.ue) instance CastIntTo Int32 where cast = F (P.fromInteger P.. P.toInteger) ( - A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) + A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) + `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) instance CastIntTo Int64 where cast = F (P.fromInteger P.. P.toInteger) ( - A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) + A.Retype P.. A.ue P.. (\x -> ((x P.+ (128::(A.E Word64))) + `A.mod_` 256) P.- 128) P.. A.Retype P.. A.ue) -- | Beware : both sides are executed, even if the result of one is later discarded @@ -164,6 +160,8 @@ double = P.id -- Used for easily producing, and coercing PVars + +-- for variables extB :: Var -> Phase -> Spec Bool extB = PVar A.Bool extI8 :: Var -> Phase -> Spec Int8 @@ -186,6 +184,31 @@ extF = PVar A.Float extD :: Var -> Phase -> Spec Double extD = PVar A.Double + +-- for arrays +extArrB :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Bool +extArrB = \(v, idx) ph -> PArr A.Bool (v, idx) ph +extArrI8 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int8 +extArrI8 = \(v, idx) ph -> PArr A.Int8 (v, idx) ph +extArrI16 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int16 +extArrI16 = \(v, idx) ph -> PArr A.Int16 (v, idx) ph +extArrI32 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int32 +extArrI32 = \(v, idx) ph -> PArr A.Int32 (v, idx) ph +extArrI64 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Int64 +extArrI64 = \(v, idx) ph -> PArr A.Int64 (v, idx) ph +extArrW8 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word8 +extArrW8 = \(v, idx) ph -> PArr A.Word8 (v, idx) ph +extArrW16 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word16 +extArrW16 = \(v, idx) ph -> PArr A.Word16 (v, idx) ph +extArrW32 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word32 +extArrW32 = \(v, idx) ph -> PArr A.Word32 (v, idx) ph +extArrW64 :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Word64 +extArrW64 = \(v, idx) ph -> PArr A.Word64 (v, idx) ph +extArrF :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Float +extArrF = \(v, idx) ph -> PArr A.Float (v, idx) ph +extArrD :: (Streamable a, A.IntegralE a) => (Var, Spec a) -> Phase -> Spec Double +extArrD = \(v, idx) ph -> PArr A.Double (v, idx) ph + ---- Sets of operators for Tests.Random.hs ------------------------------------- diff --git a/Language/Copilot/Libs/ErrorChks.hs b/Language/Copilot/Libs/ErrorChks.hs --- a/Language/Copilot/Libs/ErrorChks.hs +++ b/Language/Copilot/Libs/ErrorChks.hs @@ -2,7 +2,7 @@ module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where -import Prelude (Num, Integral, Int, String, error, ($), show, maxBound, toInteger) +import Prelude (Integral, Int, String, error, ($), show, maxBound, toInteger) import qualified Prelude as P import Data.Int (Int16) diff --git a/Language/Copilot/Libs/Indexes.hs b/Language/Copilot/Libs/Indexes.hs --- a/Language/Copilot/Libs/Indexes.hs +++ b/Language/Copilot/Libs/Indexes.hs @@ -5,7 +5,7 @@ module Language.Copilot.Libs.Indexes(soonest, soonestFail, latest, latestFail) where -import Prelude (Integral, Bool(..), id, Int, String, error, fromIntegral, ($), show) +import Prelude (id, Int, String, fromIntegral, ($)) import qualified Prelude as P import Data.Int (Int16) diff --git a/Language/Copilot/Libs/LTL.hs b/Language/Copilot/Libs/LTL.hs --- a/Language/Copilot/Libs/LTL.hs +++ b/Language/Copilot/Libs/LTL.hs @@ -3,8 +3,7 @@ module Language.Copilot.Libs.LTL(always, next, eventually, until, release) where import Prelude (Int, ($)) -import qualified Prelude as P -import Data.List(foldl1) +import Data.List (foldl1) import Language.Copilot.Core import Language.Copilot.Language diff --git a/Language/Copilot/Libs/PTLTL.hs b/Language/Copilot/Libs/PTLTL.hs --- a/Language/Copilot/Libs/PTLTL.hs +++ b/Language/Copilot/Libs/PTLTL.hs @@ -1,7 +1,6 @@ --- | Provides past-time linear-temporal logic (ptLTL operators). - --- XXX won't make unique tmp stream names if you use the same operator twice in --- one stream definition. +-- | Provides past-time linear-temporal logic (ptLTL operators). Currently +-- won't make unique tmp stream names if you use the same operator twice in one +-- stream definition. module Language.Copilot.Libs.PTLTL(previous, alwaysBeen, eventuallyPrev, since) where diff --git a/Language/Copilot/Tests/Random.hs b/Language/Copilot/Tests/Random.hs --- a/Language/Copilot/Tests/Random.hs +++ b/Language/Copilot/Tests/Random.hs @@ -1,9 +1,11 @@ {-# LANGUAGE ScopedTypeVariables, FlexibleInstances, GADTs, RankNTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} +-- | Generate random specs for testing. We do not generate external array indexes. + module Language.Copilot.Tests.Random (randomStreams, Operator(..), Operators, fromOp) where -import Language.Copilot.Core +import Language.Copilot.Core import Language.Copilot.Analyser import qualified Language.Atom as A @@ -53,13 +55,17 @@ ---- Tools --------------------------------------------------------------------- data Operator a = - Operator (forall g . RandomGen g => (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> - g -> (Spec a, g)) + Operator (forall g . RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => + g' -> SpecSet -> (Spec a', g')) -> + g -> (Spec a, g)) type Operators = StreamableMaps Operator fromOp :: Operator a -> - (forall g. RandomGen g => (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> - g -> (Spec a, g)) + (forall g. RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => + g' -> SpecSet -> (Spec a', g')) -> + g -> (Spec a, g)) fromOp op = case op of Operator x -> x @@ -184,7 +190,8 @@ ---- Generation of random streams ---------------------------------------------- -randomStreams :: RandomGen g => Operators -> Operators -> Operators -> g -> (StreamableMaps Spec, Vars) +randomStreams :: RandomGen g => Operators -> Operators -> + Operators -> g -> (StreamableMaps Spec, Vars) randomStreams opsF opsF2 opsF3 g = let (vs, g0) = addRandomVNames weightsContinueVar weightsVarTypes g emptySM (exts, g1) = addRandomVNames weightsContinuePVar weightsPVarTypes g0 emptySM @@ -194,7 +201,8 @@ then (streams, vars) else randomStreams opsF opsF2 opsF3 g3 -addRandomVNames :: RandomGen g => [(Bool, Int)] -> [(A.Type, Int)] -> g -> Variables -> (Variables, g) +addRandomVNames :: RandomGen g => [(Bool, Int)] -> + [(A.Type, Int)] -> g -> Variables -> (Variables, g) addRandomVNames wContinue wTypes g vs = let (b, g0) = randomWeighted g wContinue (t, g1) = randomWeighted g0 wTypes @@ -229,9 +237,10 @@ Variables -> Variables -> Operators -> Operators -> Operators -> g -> SpecSet -> (Spec a, g) randomSpec vs exts opsF opsF2 opsF3 g set = let weights = case set of - AllSpecSet -> weightsAllSpecSet - FunSpecSet -> weightsFunSpecSet + AllSpecSet -> weightsAllSpecSet + FunSpecSet -> weightsFunSpecSet DropSpecSet -> weightsDropSpecSet + _ -> weightsAllSpecSet (n::Int, g0) = randomWeighted g weights in case n of 0 -> -- PVar @@ -263,7 +272,8 @@ (Drop i s', g2) _ -> error "Impossible" where - randomSpec' :: forall a' g'. (Streamable a', RandomGen g', Random a') => g' -> SpecSet -> (Spec a', g') + randomSpec' :: forall a' g'. (Streamable a', RandomGen g', Random a') + => g' -> SpecSet -> (Spec a', g') randomSpec' = randomSpec vs exts opsF opsF2 opsF3 getOpStream :: Operators -> g -> (Spec a, g) getOpStream ops g0 = diff --git a/README b/README --- a/README +++ b/README @@ -20,7 +20,7 @@ code. -******** +******************************************************************************* Please visit for more information about installing and using Copilot. @@ -30,4 +30,19 @@ > git checkout gh-pages and you should see index.html. -******** + + +******************************************************************************* +Release notes + +* Copilot-0.23 + + * All -Wall warnings removed (from importing Copilot.hs). + * Added support for sampling external array values. (See Examples.hs). + * Fixed a bug in calling CBMC to ensure it unrolls it's loop. Updated + documentation in Help.hs. + * Other minor stylistic changes and fixes. + +* Copilot-0.22: initial release + + diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,8 @@ +#! /usr/bin/env runhaskell + +> module Main (main) where +> +> import Distribution.Simple (defaultMain) +> +> main :: IO () +> main = defaultMain diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,12 +1,12 @@ name: copilot -version: 0.22 +version: 0.23 cabal-version: >= 1.2 license: BSD3 license-file: LICENSE -author: Lee Pike , Robin Morisset, Alwyn Goodloe, Sebastian Niller -synopsis: A stream DSL for writing embedded C. +author: Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller +synopsis: A stream DSL for writing embedded C monitors. build-type: Simple -maintainer: Lee Pike +maintainer: Lee Pike category: Language homepage: http://leepike.github.com/Copilot/ description: Can you write a list in Haskell? Then you can write embedded C code using @@ -32,7 +32,7 @@ library ghc-options: -Wall build-depends: base > 4 && < 5 - , atom >= 1.0.5 + , atom >= 1.0.7 , containers >= 0.2.0.1 , process >= 1.0.0.0 , random >= 1.0.0.0