diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +2009 +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Language/Copilot.hs b/Language/Copilot.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot.hs @@ -0,0 +1,36 @@ +module Language.Copilot + ( module Language.Copilot.Core + , module Language.Copilot.Analyser + , module Language.Copilot.Interpreter + , module Language.Copilot.Help + , module Language.Copilot.AtomToC + , module Language.Copilot.Compiler + , module Language.Copilot.Language + -- , module Language.Copilot.Dispatch + , module Language.Copilot.Interface + , module Language.Copilot.Tests.Random + , module Language.Copilot.Libs.Indexes + , module Language.Copilot.Libs.LTL + , module Language.Copilot.Libs.PTLTL + -- , module Language.Copilot.Examples.Examples + -- , module Language.Copilot.Examples.LTLExamples + -- , module Language.Copilot.Examples.PTLTLExamples + ) where + +import Language.Copilot.Core +import Language.Copilot.Analyser +import Language.Copilot.Interpreter +import Language.Copilot.Help +import Language.Copilot.AtomToC +import Language.Copilot.Compiler +import Language.Copilot.Language (opsF, opsF2, opsF3) +import Language.Copilot.PrettyPrinter() +import Language.Copilot.Tests.Random +import Language.Copilot.Dispatch +import Language.Copilot.Interface +import Language.Copilot.Libs.Indexes +import Language.Copilot.Libs.LTL +import Language.Copilot.Libs.PTLTL +-- 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 new file mode 100644 --- /dev/null +++ b/Language/Copilot/AdHocC.hs @@ -0,0 +1,45 @@ +-- 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 + ) where + +import Data.List (intersperse) +import Language.Atom (Type(..)) +import Language.Atom.Code (cType) -- C99 + +-- | 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 + + +-- | Add an include of a library +includeBracket :: String -> String +includeBracket lib = "#include <" ++ lib ++ ">" + +-- | Add an include of a header file +includeQuote :: String -> String +includeQuote lib = "#include \"" ++ lib ++ "\"" + +printfPre :: String -> String +printfPre = ("printf(\"" ++) + +printfPost :: [String] -> String +printfPost vars = + let sep = if null vars then " " else ", " + in "\"" ++ sep ++ unwords (intersperse "," vars) ++ ");" + +newline :: String +newline = "\\n" + +-- | printf, with and without a newline (nl) character. +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 new file mode 100644 --- /dev/null +++ b/Language/Copilot/Analyser.hs @@ -0,0 +1,238 @@ +{-# OPTIONS_GHC -XRelaxedPolyRec #-} + +-- | 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 + {- + -- * Dependency Graphs (experimental) + Weight, Node(..), DependencyGraph, + mkDepGraph, showDG -} + ) where + +import Language.Copilot.Core + +import qualified Language.Atom as A + +import Data.List + +type Weight = Int + +-- | Used for representing an error in the specification, detected by @'check'@ +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 + +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 (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" + 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" + 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" + 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" + +(&&>) :: Maybe a -> Maybe a -> Maybe a +m &&> m' = + case m of + Just _ -> m + Nothing -> m' + +(||>) :: Bool -> a -> Maybe a +b ||> x = + if b + then Nothing + else Just x + +infixr 2 ||> +infixr 1 &&> + +-- | 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 = + syntaxCheck streams &&> defCheck streams + +-- Represents all the kind of specs that are authorized after a given operator +data SpecSet = AllSpecSet | FunSpecSet | DropSpecSet 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 +-- But then there would have been quite a lot construction/deconstruction to do everywhere. +-- Hence the compact type for Spec and this extra check. +syntaxCheck :: StreamableMaps Spec -> Maybe Error +syntaxCheck streams = + foldStreamableMaps (checkSyntaxSpec AllSpecSet) streams Nothing + where + 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) + +-- 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) +defCheck :: StreamableMaps Spec -> Maybe Error +defCheck streams = + let checkPathsFromSpec :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error + checkPathsFromSpec v0 s0 e = + e &&> checkPath 0 [v0] s0 + where + prophecyArrayLength s = + case s of + Append ls s' -> length ls + prophecyArrayLength s' + _ -> 0 + checkPath :: Streamable a => Int -> [Var] -> Spec a -> Maybe Error + checkPath n vs s = + 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) + _ -> Nothing + Var v -> + if elem v vs + then if n >= 0 + then Just $ NonNegativeWeightedClosedPath vs n + else Nothing + else + let spec = getMaybeElem v streams in + case spec of + Nothing -> Just $ BadType v (head vs) + Just s' -> checkPath n (v:vs) (s' `asTypeOf` s) + 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 + Append l s' -> checkPath (n - length l) vs s' + Drop i s' -> checkPath (n + i) vs s' + 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 + +getExternalVars :: StreamableMaps Spec -> [(A.Type, Var, Phase)] +getExternalVars streams = + nub $ foldStreamableMaps decl streams [] + where + decl :: Streamable a => Var -> Spec a -> [(A.Type, Var, Phase)] -> [(A.Type, Var, Phase)] + decl _ s ls = + case s of + PVar t v ph -> (t, v, ph) : 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 + 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 = + InternalVar Var [(Weight, Node)] + | ExternalVar Var Phase + deriving Show -- for debug + +instance Eq Node where + InternalVar v _ == InternalVar v' _ = v == v' + ExternalVar v ph == ExternalVar v' ph' = v == v' && ph == ph' + _ == _ = False + +type DependencyGraph = [Node] + +showDG :: DependencyGraph -> [String] +showDG dG = map show dG + +mkDepGraph :: StreamableMaps Spec -> DependencyGraph +mkDepGraph streams = + dGFixpoint + where + dGFixpoint :: DependencyGraph + dGFixpoint = foldStreamableMaps mkNode streams [] + mkNode :: Streamable a => Var -> Spec a -> DependencyGraph -> DependencyGraph + mkNode v s dG = + let edges = mkEdges 0 s + externalNodes = mkExternalNodes s in + (InternalVar v edges) : (nub $ externalNodes ++ dG) + -- TODO : the following functions can probably be fused together + mkExternalNodes :: Spec a -> [Node] + mkExternalNodes s = + case s of + PVar _ v ph -> [ExternalVar v ph] + Var _ -> [] + Const _ -> [] + F _ _ s0 -> mkExternalNodes s0 + F2 _ _ s0 s1 -> mkExternalNodes s0 ++ mkExternalNodes s1 + F3 _ _ s0 s1 s2 -> mkExternalNodes s0 ++ mkExternalNodes s1 ++ mkExternalNodes s2 + Append _ s0 -> mkExternalNodes s0 + Drop _ s0 -> mkExternalNodes s0 + mkEdges :: Weight -> Spec a -> [(Weight, Node)] + mkEdges w s = + case s of + PVar _ v ph -> [(w, getNode v $ Just ph)] + Var v -> [(w, getNode v Nothing)] + Const _ -> [] + F _ _ s0 -> mkEdges w s0 + F2 _ _ s0 s1 -> mkEdges w s0 ++ mkEdges w s1 + F3 _ _ s0 s1 s2 -> mkEdges w s0 ++ mkEdges w s1 ++ mkEdges w s2 + Append ls s0 -> mkEdges (w - length ls) s0 + Drop i s0 -> mkEdges (w + i) s0 + getNode :: Var -> Maybe Phase -> Node + getNode v mp = + case mp of + Nothing -> fromJust $ find ((==) (InternalVar v [])) dGFixpoint + Just ph -> fromJust $ find ((==) (ExternalVar v ph)) dGFixpoint -} diff --git a/Language/Copilot/AtomToC.hs b/Language/Copilot/AtomToC.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/AtomToC.hs @@ -0,0 +1,123 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Defines a main() and print statements to easily execute generated Copilot specs. +module Language.Copilot.AtomToC(getPrePostCode) where + +import Language.Copilot.AdHocC +import Language.Copilot.Core + +import qualified Language.Atom as A + +import Data.List + +-- 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) + +-- 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 + +preCode :: [String] -> String +preCode extDeclarations = unlines $ + [ includeBracket "stdio.h" + , includeBracket "stdlib.h" + , includeBracket "string.h" + , includeBracket "inttypes.h" + , "" + , "unsigned long long rnd;" + ] + ++ extDeclarations + +vPre :: Name -> String +vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "." + +postCode :: Name -> StreamableMaps Spec -> [(A.Type, Var, Phase)] -> Vars -> Period -> String +postCode cName streams allExts inputExts p = + unlines $ + (if isEmptySM inputExts + then [] + else cleanString) + ++ + [ "// #pragma GCC diagnostic ignored \"-Wformat\"" + , "int main(int argc, char *argv[]) {" + , " if (argc != 2) {" + , " " ++ printfNewline + "Please pass a single argument to the simulator containing the number of rounds to execute it." + [] + , " return 1;" + , " }" + , " rnd = atoi(argv[1]);" + ] + ++ + inputExtVars inputExts " " + ++ + sampleExtVars allExts cName + ++ + [ " int i = 0;" + , " for(; i < rnd ; i++) {" + ] + ++ + inputExtVars inputExts " " + ++ + [ " int j = 0;" + , " for (; j < " ++ show p ++ " ; j++) {" + , " " ++ cName ++ "();" + , " }" + , " " ++ printf "period: %i " ["i"] + ] + ++ + outputVars cName streams + ++ + [ " " ++ printfNewline "" [] + , " fflush(stdout);" + , " }" + , " return EXIT_SUCCESS;" + , "}" + ] + where + cleanString = + [ "void clean(const char *buffer, FILE *fp) {" + , " char *p = strchr(buffer,'\\n');" + , " if (p != NULL)" + , " *p = 0;" + , " else {" + , " int c;" + , " while ((c = fgetc(fp)) != '\\n' && c != EOF);" + , " }" + , "}" + , "" + ] + +inputExtVars :: Vars -> String -> [String] +inputExtVars exts indent = + foldStreamableMaps decl exts [] + where + decl :: Streamable a => Var -> [a] -> [String] -> [String] + 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 ++ "clean (" ++ string ++ ", stdin);") : ls + +sampleExtVars :: [(A.Type, Var, Phase)] -> 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 ++ ";" + +outputVars :: Name -> StreamableMaps Spec -> [String] +outputVars cName streams = + foldStreamableMaps decl streams [] + where + decl :: forall a. Streamable a => Var -> Spec a -> [String] -> [String] + decl v _ ls = + (" " ++ printf (v ++ ": " ++ typeIdPrec (unit::a) ++ " ") [vPre cName ++ "outputVal__" ++ v]) : ls diff --git a/Language/Copilot/Compiler.hs b/Language/Copilot/Compiler.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Compiler.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE ScopedTypeVariables, Rank2Types #-} + +-- 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 + +import Language.Copilot.Core + +import Data.Word +import Data.Maybe +import Data.Map as M +import Data.List +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 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) + + -- One atom rule for each stream + foldStreamableMaps (makeRule streams outputs prophArrs tmpSamples + updateIndexes outputIndexes) + streams (return ()) + + foldStreamableMaps (makeTrigger triggers streams prophArrs tmpSamples + outputIndexes) + streams (return ()) + + foldSendableMaps (makeSend outputs) sends (return ()) + + -- Sampling of the external variables + sampleVars tmpSamples) + where + optP = getOptimalPeriod streams + p' = + case p of + Nothing -> optP + Just i -> if i >= optP + then i + else error $ "Copilot error: the period is too short, " + ++ "it should be at least " ++ show optP ++ " ticks." + +initProphArr :: forall a. Streamable a => Var -> Spec a -> A.Atom (BoundedArray a) +initProphArr v s = + let states = initState s + name = "prophVal__" ++ normalizeVar v + n = genericLength states in + if n > 0 + then + do + array <- A.array name (states ++ [unit]) + -- unit is replaced by the good value during the first tick + return $ B n $ Just array + else return $ B n Nothing + where + initState s' = + case s' of + Append ls s'' -> ls ++ initState s'' + _ -> [] + +initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a) +initOutput v s = streamToUnitValue ("outputVal__" ++ normalizeVar v) s + +initTmpSamples :: forall a. Streamable a => Var -> Spec a -> A.Atom TmpSamples -> A.Atom TmpSamples +initTmpSamples _ s tmpSamples = + 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 + PVar _ v ph -> + do + ts <- tmpSamples + let v' = normalizeVar v ++ "_" ++ show ph + maybeElem = (getMaybeElem v' ts)::(Maybe (PhasedValue a)) + name = "tmpSampleVal__" ++ 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" + +makeUpdateIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes +makeUpdateIndex v (B n arr) indexes = + case arr of + Nothing -> indexes + Just _ -> + do + mindexes <- indexes + index <- atomConstructor ("updateIndex__" ++ normalizeVar v) n + return $ M.insert v index mindexes + +makeOutputIndex :: Var -> BoundedArray a -> A.Atom Indexes -> A.Atom Indexes +makeOutputIndex v (B _ arr) indexes = + case arr of + Nothing -> indexes + Just _ -> + do + mindexes <- indexes + index <- atomConstructor ("outputIndex__" ++ normalizeVar v) 0 + return $ M.insert v index mindexes + +makeRule :: forall a. Streamable a => + StreamableMaps Spec -> Outputs -> ProphArrs -> TmpSamples -> + 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) + case maybeArr of + Nothing -> + -- Fusing together the update and the output if the prophecy array doesn't exist + -- (ie if it would only have hold the output value) + A.exactPhase 0 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do + ((getElem v outputs)::(A.V a)) A.<== nextSt' + + Just arr -> do + let updateIndex = fromJust $ M.lookup v updateIndexes + outputIndex = fromJust $ M.lookup v outputIndexes + + A.exactPhase 0 $ A.atom ("update__" ++ normalizeVar v) $ do + arr A.! (A.VRef updateIndex) A.<== nextSt' + + A.exactPhase 1 $ A.atom ("output__" ++ normalizeVar v) $ do + ((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 + 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 + +makeSend :: forall a. Sendable a => Outputs -> Var -> Send a -> A.Atom () -> A.Atom () +makeSend outputs name (Send (v, ph, port)) r = + r >> + do + 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 + +getOptimalPeriod :: StreamableMaps Spec -> Period +getOptimalPeriod streams = + foldStreamableMaps getMaximumSamplingPhase streams 2 + where + getMaximumSamplingPhase :: Var -> Spec a -> Period -> Period + getMaximumSamplingPhase _ spec n = + case spec of + PVar _ _ p -> max (p + 1) n + F _ _ s -> getMaximumSamplingPhase "" s n + F2 _ _ s0 s1 -> maximum [n, + (getMaximumSamplingPhase "" s0 n), + (getMaximumSamplingPhase "" s1 n)] + F3 _ _ s0 s1 s2 -> maximum [n, + (getMaximumSamplingPhase "" s0 n), + (getMaximumSamplingPhase "" s1 n), + (getMaximumSamplingPhase "" s2 n)] + Drop _ s -> getMaximumSamplingPhase "" s n + Append _ s -> getMaximumSamplingPhase "" s n + _ -> n diff --git a/Language/Copilot/Core.hs b/Language/Copilot/Core.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Core.hs @@ -0,0 +1,542 @@ +{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, + FlexibleInstances #-} + +-- | Provides basic types and functions for other parts of /Copilot/. +-- +-- If you wish to add a new type, you need to make it an instance of @'Streamable'@, +-- to add it to @'foldStreamableMaps'@, @'mapStreamableMaps'@, and optionnaly +-- to add an ext[Type], a [type] and a var[Type] +-- functions in Language.hs to make it easier to use. +module Language.Copilot.Core ( + -- * Type hierarchy for the copilot language + Var, Name, Period, Phase, Port, + Spec(..), Streams, Stream, Sends, Send(..), DistributedStreams, + -- * General functions on 'Streams' and 'StreamableMaps' + Streamable(..), Sendable(..), StreamableMaps(..), emptySM, + isEmptySM, getMaybeElem, getElem, streamToUnitValue, + foldStreamableMaps, foldSendableMaps, mapStreamableMaps, mapStreamableMapsM, + filterStreamableMaps, normalizeVar, getVars, + Vars + -- Compiler + , nextSt, BoundedArray(..), Outputs, TmpSamples + , PhasedValue(..), ProphArrs, Indexes + ) where + +import qualified Language.Atom as A +import Data.Int +import Data.Word +import Data.Maybe +import Data.List +import qualified Data.Map as M +import Text.Printf +import Control.Monad.Writer + +---- Type hierarchy for the copilot language ----------------------------------- + +-- | Names of the streams or external variables +type Var = String +-- | C file name +type Name = String +-- | Atom period +type Period = Int +-- | Phase of an Atom phase +type Phase = Int +-- | Port over which to broadcast information +type Port = Int + +-- | 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 + 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 + Append :: Streamable a => [a] -> Spec a -> Spec a + Drop :: Streamable a => Int -> Spec a -> Spec a + +{-# 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 +"Copilot.Core dropConst" forall i x. Drop i (Const x) = Const x +"Copilot.Core FConst" forall fI fC x0. F fI fC (Const x0) = Const (fI x0) +"Copilot.Core F2Const" forall fI fC x0 x1. F2 fI fC (Const x0) (Const x1) = Const (fI x0 x1) +"Copilot.Core F3Const" forall fI fC x0 x1 x2. F3 fI fC (Const x0) (Const x1) (Const x2) = Const (fI x0 x1 x2) + #-} + +instance Eq a => Eq (Spec a) where + (==) (PVar t v ph) (PVar t' v' ph') = t == t' && v == v' && ph == ph' + (==) (Var v) (Var v') = v == v' + (==) (Const x) (Const x') = x == x' + (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s' + (==) s@(F2 _ _ _ _) s'@(F2 _ _ _ _) = show s == show s' + (==) s@(F3 _ _ _ _ _) s'@(F3 _ _ _ _ _) = show s == show s' + (==) (Append ls s) (Append ls' s') = ls == ls' && s == s' + (==) (Drop i s) (Drop i' s') = i == i' && s == s' + (==) _ _ = False + +-- | 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) +-- | An instruction to send data on a port at a given phase +data Send a = Sendable a => Send (Var, Phase, Port) +-- | Container for all the instructions sending data, parameterised by different types +type Sends = StreamableMaps Send +-- | Holds the complete specification of a distributed monitor +type DistributedStreams = (Streams, Sends) + +---- General functions on streams ---------------------------------------------- + +-- | A type is streamable iff a stream may emit values of that type +-- +-- There are very strong links between @'Streamable'@ and @'StreamableMaps'@ : +-- the types aggregated in @'StreamableMaps'@ are exactly the @'Streamable'@ types +-- and that invariant should be kept (see methods) +class (A.Expr a, A.Assign a, Show a) => Streamable a where + -- | Provides access to the Map in a StreamableMaps which store values + -- of the good type + getSubMap :: StreamableMaps b -> M.Map Var (b a) + + -- | Provides a way to modify (mostly used for insertions) the Map in a StreamableMaps + -- which store values of the good type + updateSubMap :: (M.Map Var (b a) -> M.Map Var (b a)) -> StreamableMaps b -> StreamableMaps b + + -- | A default value for the type @a@. Its value is not important. + unit :: a + + -- | A constructor to produce an @Atom@ value + atomConstructor :: Var -> a -> A.Atom (A.V a) + + -- | A constructor to get an @Atom@ value from an external variable + externalAtomConstructor :: Var -> A.V a + + -- | The argument only coerces the type, it is discarded. + -- Returns the format for outputting a value of this type with printf in C + -- + -- For example "%f" for a float + typeId :: a -> String + + -- | The same, only adds the wanted precision for floating points. + typeIdPrec :: a -> String + typeIdPrec x = typeId x + + -- | The argument only coerces the type, it is discarded. + -- Returns the corresponding /Atom/ type. + atomType :: a -> A.Type + + -- | Like Show, except that the formatting is exactly the same as the one of C + -- 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 + -> ProphArrs -> TmpSamples -> Indexes -> Var -> Spec a + -> A.Atom () -> A.Atom () + + +class Streamable a => Sendable a where + send :: A.E a -> Port -> A.Atom () + +instance Streamable Bool where + getSubMap = bMap + updateSubMap f sm = sm {bMap = f $ bMap sm} + unit = False + atomConstructor = A.bool + externalAtomConstructor = A.bool' + typeId _ = "%i" + atomType _ = A.Bool + showAsC x = printf "%u" (if x then 1::Int else 0) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> + if trig /= "" + then (A.exactPhase 0 $ A.atom ("trigger__" ++ normalizeVar v) $ do + 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 + Nothing -> "" + Just fn -> fn + +instance Streamable Int8 where + getSubMap = i8Map + updateSubMap f sm = sm {i8Map = f $ i8Map sm} + unit = 0 + atomConstructor = A.int8 + externalAtomConstructor = A.int8' + typeId _ = "%d" + atomType _ = A.Int8 + showAsC x = printf "%d" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Int16 where + getSubMap = i16Map + updateSubMap f sm = sm {i16Map = f $ i16Map sm} + unit = 0 + atomConstructor = A.int16 + externalAtomConstructor = A.int16' + typeId _ = "%d" + atomType _ = A.Int16 + showAsC x = printf "%d" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Int32 where + getSubMap = i32Map + updateSubMap f sm = sm {i32Map = f $ i32Map sm} + unit = 0 + atomConstructor = A.int32 + externalAtomConstructor = A.int32' + typeId _ = "%d" + atomType _ = A.Int32 + showAsC x = printf "%d" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Int64 where + getSubMap = i64Map + updateSubMap f sm = sm {i64Map = f $ i64Map sm} + unit = 0 + atomConstructor = A.int64 + externalAtomConstructor = A.int64' + typeId _ = "%lld" + atomType _ = A.Int64 + showAsC x = printf "%d" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Word8 where + getSubMap = w8Map + updateSubMap f sm = sm {w8Map = f $ w8Map sm} + unit = 0 + atomConstructor = A.word8 + externalAtomConstructor = A.word8' + typeId _ = "%u" + atomType _ = A.Word8 + showAsC x = printf "%u" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Word16 where + getSubMap = w16Map + updateSubMap f sm = sm {w16Map = f $ w16Map sm} + unit = 0 + atomConstructor = A.word16 + externalAtomConstructor = A.word16' + typeId _ = "%u" + atomType _ = A.Word16 + showAsC x = printf "%u" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Word32 where + getSubMap = w32Map + updateSubMap f sm = sm {w32Map = f $ w32Map sm} + unit = 0 + atomConstructor = A.word32 + externalAtomConstructor = A.word32' + typeId _ = "%u" + atomType _ = A.Word32 + showAsC x = printf "%u" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Word64 where + getSubMap = w64Map + updateSubMap f sm = sm {w64Map = f $ w64Map sm} + unit = 0 + atomConstructor = A.word64 + externalAtomConstructor = A.word64' + typeId _ = "%llu" + atomType _ = A.Word64 + showAsC x = printf "%u" (toInteger x) + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Float where + getSubMap = fMap + updateSubMap f sm = sm {fMap = f $ fMap sm} + unit = 0 + atomConstructor = A.float + externalAtomConstructor = A.float' + typeId _ = "%f" + typeIdPrec _ = "%.5f" + atomType _ = A.Float + showAsC x = printf "%.5f" x + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () +instance Streamable Double where + getSubMap = dMap + updateSubMap f sm = sm {dMap = f $ dMap sm} + unit = 0 + atomConstructor = A.double + externalAtomConstructor = A.double' + typeId _ = "%lf" + typeIdPrec _ = "%.10lf" + atomType _ = A.Double + showAsC x = printf "%.10f" x + makeTrigger triggers streams prophArrs tmpSamples outputIndexes v s r = r >> return () + +instance Sendable Word8 where + send e port = + A.action (\ [ueString] -> "sendW8_port" ++ show port + ++ "(" ++ ueString ++ ")") [A.ue e] + +-- | Lookup into the map of the right type in @'StreamableMaps'@ +{-# INLINE getMaybeElem #-} +getMaybeElem :: Streamable a => Var -> StreamableMaps b -> Maybe (b a) +getMaybeElem v sm = M.lookup v $ getSubMap sm + +-- | Lookup into the map of the right type in @'StreamableMaps'@ +-- 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 + +-- | 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 + +-- | 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) -> + 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 + in acc10 + +-- | 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 = + let acc1 = M.foldWithKey f acc w8m + in acc1 + +{-# INLINE mapStreamableMaps #-} +mapStreamableMaps :: forall s s'. + (forall a. Streamable a => Var -> s a -> s' a) -> + StreamableMaps s -> StreamableMaps s' +mapStreamableMaps f (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) = + SM { + bMap = M.mapWithKey f bm, + i8Map = M.mapWithKey f i8m, + i16Map = M.mapWithKey f i16m, + i32Map = M.mapWithKey f i32m, + i64Map = M.mapWithKey f i64m, + w8Map = M.mapWithKey f w8m, + w16Map = M.mapWithKey f w16m, + w32Map = M.mapWithKey f w32m, + w64Map = M.mapWithKey f w64m, + fMap = M.mapWithKey f fm, + dMap = M.mapWithKey f dm + } + +{-# INLINE mapStreamableMapsM #-} +mapStreamableMapsM :: forall s s' m. Monad m => + (forall a. Streamable a => Var -> s a -> m (s' a)) -> + StreamableMaps s -> m (StreamableMaps s') +mapStreamableMapsM f sm = + foldStreamableMaps ( + \ v s sm'M -> do + sm' <- sm'M + s' <- f v s + 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) +filterStreamableMaps sm l = + let (sm2, l2) = foldStreamableMaps filterElem sm (emptySM, []) in + (sm2, (l' \\ nub l2) == []) + where + filterElem :: forall a. Streamable a => Var -> c a -> + (StreamableMaps c, [(A.Type, Var)]) -> + (StreamableMaps c, [(A.Type, Var)]) + filterElem v s (sm', l2) = + let x = (atomType (unit::a), v) in + if x `elem` l' + then (updateSubMap (\m -> M.insert v s m) sm', x:l2) + else (sm', l2) + l' = nub $ map (\(x,y,_) -> (x,y)) l + +-- | This is a generalization of @'Streams'@ +-- which is used for storing Maps over values parameterized by different types. +-- +-- It is extensively used in the internals of Copilot, in conjunction with +-- @'foldStreamableMaps'@ and @'mapStreamableMaps'@ +data StreamableMaps a = + SM { + bMap :: M.Map Var (a Bool), + i8Map :: M.Map Var (a Int8), + i16Map :: M.Map Var (a Int16), + i32Map :: M.Map Var (a Int32), + i64Map :: M.Map Var (a Int64), + w8Map :: M.Map Var (a Word8), + w16Map :: M.Map Var (a Word16), + w32Map :: M.Map Var (a Word32), + w64Map :: M.Map Var (a Word64), + fMap :: M.Map Var (a Float), + dMap :: M.Map Var (a Double) + } + +instance Monoid (StreamableMaps Spec) where + mempty = emptySM + mappend x@(SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) + y@(SM bm' i8m' i16m' i32m' i64m' w8m' w16m' w32m' w64m' fm' dm') = overlap + where overlap = let multDefs = (getVars x `intersect` getVars y) + in if null multDefs then union + else error $ "Copilot error: The variables " + ++ show multDefs ++ " have multiple definitions." + union = SM (M.union bm bm') (M.union i8m i8m') (M.union i16m i16m') + (M.union i32m i32m') (M.union i64m i64m') (M.union w8m w8m') + (M.union w16m w16m') (M.union w32m w32m') (M.union w64m w64m') + (M.union fm fm') (M.union dm dm') + + +-- | Get the Copilot variables. +getVars :: StreamableMaps Spec -> [Var] +getVars streams = foldStreamableMaps (\k _ ks -> k:ks) streams [] + +-- | An empty streamableMaps. +emptySM :: StreamableMaps a +emptySM = SM + { + bMap = M.empty, + i8Map = M.empty, + i16Map = M.empty, + i32Map = M.empty, + i64Map = M.empty, + w8Map = M.empty, + w16Map = M.empty, + w32Map = M.empty, + w64Map = M.empty, + fMap = M.empty, + dMap = M.empty + } + +-- | Verifies if its argument is equal to emptySM +isEmptySM :: StreamableMaps a -> Bool +isEmptySM (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) = + M.null bm && + M.null i8m && + M.null i16m && + M.null i32m && + M.null i64m && + M.null w8m && + M.null w16m && + M.null w32m && + M.null w64m && + M.null fm && + M.null dm + +-- | Replace all accepted special characters by sequences of underscores +normalizeVar :: Var -> Var +normalizeVar 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, +-- not to a single clock tick. +type Vars = StreamableMaps [] + +-- Pretty printer: can't put in PrettyPrinter since that causes circular deps. + +instance Show a => Show (Spec a) where + show s = showIndented s 0 + +showIndented :: Spec a -> Int -> String +showIndented s n = + let tabs = concat $ replicate n " " in + tabs ++ showRaw s n + +showRaw :: Spec a -> Int -> String +showRaw (PVar t v ph) _ = "PVar " ++ show t ++ " " ++ v ++ " " ++ show ph +showRaw (Var v) _ = "Var " ++ v +showRaw (Const e) _ = "Const " ++ show e +showRaw (F _ _ s0) n = + "F op? (\n" ++ + showIndented s0 (n + 1) ++ "\n" ++ + (concat $ replicate n " ") ++ ")" +showRaw (F2 _ _ s0 s1) n = + "F2 op? (\n" ++ + showIndented s0 (n + 1) ++ "\n" ++ + showIndented s1 (n + 1) ++ "\n" ++ + (concat $ replicate n " ") ++ ")" +showRaw (F3 _ _ s0 s1 s2) n = + "F3 op? (\n" ++ + showIndented s0 (n + 1) ++ "\n" ++ + showIndented s1 (n + 1) ++ "\n" ++ + showIndented s2 (n + 1) ++ "\n" ++ + (concat $ replicate n " ") ++ ")" +showRaw (Append ls s0) n = + "Append " ++ show ls ++ " (\n" ++ + showIndented s0 (n + 1) ++ "\n" ++ + (concat $ replicate n " ") ++ ")" +showRaw (Drop i s0) n = + "Drop " ++ show i ++ " (\n" ++ + showIndented s0 (n + 1) ++ "\n" ++ + (concat $ replicate n " ") ++ ")" + + +-- Compiler: the code below really belongs in Core.hs, but its called by +-- makeTrigger, which is a method of the class Streamable. + +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 + +nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes + -> Spec a -> ArrIndex -> A.E a +nextSt streams prophArrs tmpSamples outputIndexes s index = + case s of + PVar _ v ph -> A.value . getValue + $ getElem (normalizeVar v ++ "_" ++ show ph) tmpSamples + 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 + -- then x is obtained not by y, but by inlining the definition of y + -- 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) + Const e -> A.Const e + F _ f s0 -> f $ next s0 index + F2 _ f s0 s1 -> + 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) + where + next :: Streamable b => Spec b -> ArrIndex -> A.E b + next = nextSt streams prophArrs tmpSamples outputIndexes + diff --git a/Language/Copilot/Dispatch.hs b/Language/Copilot/Dispatch.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Dispatch.hs @@ -0,0 +1,262 @@ +{-# 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 :: 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)@. + + } + +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 + when isVerbose $ 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 + "the interpreter don't have the values for some of the external variables" + mapM_ putStrLn interpretedLines + Opts opts -> + let isInterpreted = + case (interpreted opts) of + Interpreted -> True + NotInterpreted -> False + dirName = outputDir opts + in do + putStrLn $ "Trying to create (if missing) " ++ dirName ++ " ..." + 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) + 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 + "The interpreter doesn't have the values for some of the external variables." + when isExecuted $ execute streams (dirName ++ cName opts) trueInputExts isInterpreted + interpretedLines iterations isSilent + where + 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 -> Maybe [(Var, String)] -> IO () +checkTriggerVars streams triggers = + 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 bareTriggers \\ 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 + 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 + (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] +-- 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." + , "BSD3 License" + , "" + , "" + , "Lee Pike, Robin Morisset, and Sebastian Niller" + , "Usage: " + , "" + ] diff --git a/Language/Copilot/Examples/Examples.hs b/Language/Copilot/Examples/Examples.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Examples/Examples.hs @@ -0,0 +1,188 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Language.Copilot.Examples.Examples where + +import Data.Word +import Prelude (($)) +import qualified Prelude as P +import qualified Prelude as Prelude + +-- for specifying options +import Data.Map (fromList) +import Data.Maybe (Maybe (..)) +import System.Random +import Data.Int + +import Language.Copilot.Core +import Language.Copilot.Language +import Language.Copilot.Interface +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") + "t" .= even (var "fib") + where even :: Spec Word64 -> Spec Bool + even w' = w' `mod` const 2 == const 0 + +t1 :: Streams +t1 = do + x .= [0, 1, 2] ++ var x - (drop 1 $ varI32 x) + y .= [True, False] ++ var y ^ var z + z .= varI32 "x" <= drop 1 (var x) + +t2 :: Streams +t2 = do + a .= [True] ++ not (var a) + b .= mux (var a) 2 (int8 3) + +-- t3 :: use an external variable called ext, typed Word32 +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 + +t4 :: Streams +t4 = do + a .= [True,False] ++ not (var a) + b .= drop 1 (varB a) + +t5 :: Streams +t5 = do + x .= drop 3 (varB y) + y .= [True, True] ++ not (var z) + z .= [False, False] ++ not (var z) + w .= varB x || var y + +yy :: Streams +yy = do a .= constW64 4 + +zz :: Streams +zz = do --a .= [0..4] ++ drop 4 (varW32 a) + 1 + a .= (varW32 a) + 1 + b .= drop 3 (varW32 a) + +xx :: Streams +xx = do + a .= extW32 "ext" 5 + b .= [3] ++ (varW32 a) + c .= [0, 1, 3, 4] ++ drop 1 (varW32 b) + +-- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the +-- engine is immediately shut off. From the paper. +engine :: Streams +engine = do + "temps" .= [0, 0, 0] ++ extF "temp" 1 + "overTempRise" .= drop 2 (varF "temps") > const 2.3 + var "temps" + "trigger" .= (var "overTempRise") ==> (extB "shutoff" 2) + +-- To compile: > let (streams, ss) = dist in interface $ compileOpts streams ss "dist" +-- s at phase 2 on port 1. Not stable. +dist :: DistributedStreams +dist = + ( a .= [0,1] ++ (var a) + constW8 1 + , sendW8 a (2, 1) + ..| emptySM + ) + +-- greatest common divisor. +gcd :: Word16 -> Word16 -> Streams +gcd n0 n1 = do + a .= alg n0 a b + b .= alg n1 b a + "ans" .= varW16 a == var b + where alg x0 x1 x2 = [x0] ++ mux (varW16 x1 > var x2) (var x1 - var x2) (var x1) + +-- greatest common divisor of two external vars. Compare to +-- Language.Atom.Example Try +-- +-- interpret gcd' 40 $ setE (emptySM {w16Map = +-- fromList [("n", [9,9..]), ("m", [7,7..])]}) baseOpts +-- +-- Note we have to start streams a and b with a dummy value 0 before they can +-- sample the external variables. +gcd' :: Streams +gcd' = do + a .= alg "n" (sub a b) + b .= alg "m" (sub b a) + "ans" .= varW16 a == varW16 b && not (var "init") + "init" .= [True] ++ const False + where sub hi lo = mux (varW16 hi > var lo) (var hi - var lo) (var hi) + alg ext ex = [0] ++ mux (var "init") (extW16 ext 1) ex + +testCoercions :: Streams +testCoercions = do + "short" .= ((cast (varW64 "fib"))::(Spec Word8)) + "long" .= ((cast (varW8 "short"))::(Spec Word32)) + +testCoercionsInt :: Streams +testCoercionsInt = do + "counter" .= [0] ++ varW8 "counter" + 1 + "int" .= ((cast (varW8 "counter"))::(Spec Int8)) + +testRules :: Streams +testRules = do + "v1" .= (not (Const True)) || Var "v2" + "v2" .= [True, False] ++ [True] ++ Var "v3" < extI8 "v4" 5 + "v3" .= 0 + drop 3 (int8 6) + "v4" .= always 5 (Var "v1") + +i8 :: Streams +i8 = do + v .= [0, 1] ++ (varI8 v) + 1 + +trap :: Streams +trap = do + "target" .= [0] ++ varW32 "target" + 1 + "x" .= [0,0] ++ var "y" + varW32 "target" + "y" .= [0,0] ++ var "x" + varW32 "target" + + +-- vicious :: Streams +-- vicious = do +-- "varExt" .= extW32 "ext" 5 +-- "vicious" .= [0,1,2,3] ++ drop 4 (varW32 "varExt") + drop 1 (var "varExt") + var "varExt" + +-- testVicious :: Streams +-- testVicious = do +-- "counter" .= [0] ++ varW32 "counter" + 1 +-- "testVicious" .= [0,0,0,0,0,0,0,0,0,0] ++ drop 8 (varW32 "counter") + +-- -- The issue is when a variable v with a prophecy array of length n deps on +-- -- an external variable pv with a weight w, and that w > - n + 1 Here, w = 0 and +-- -- n = 2, so 0 > -1 holds. That means that it is impossible to fill the last +-- -- case of the prophecy array, because it is not yet known what the external +-- -- variable will be worth. It could be easily forbidden in the analyser. +-- -- However theoretically, nothing seems to prevent us form compiling it, we +-- -- would only need a way to say that in these case the middle of the prophecy +-- -- array should be updated and not the . (it would be safe because if another +-- -- variable was to dep on the of it it would dep on the external +-- -- variable with a weight > 0, which is always forbidden). It is probably +-- -- easier for now to just forbid it. But it could become an issue. +-- isBugged :: Streams +-- isBugged = do +-- "v" .= extW16 "ext" 5 +-- "v2" .= [0,1,3] ++ drop 1 (varW16 "v") + + +-- -- The next two examples are currently refused, because they include a +-- -- non-negative weighted closed path. But they could be compiled. More +-- -- generally I think that this restriction could be partially lifted to +-- -- forbiding non-negative circuits. However, this would demand longer +-- -- prophecyArrays than we have for now. (and probably a slightly different +-- -- algorithm) So even if we partially lift this restriction, a warning should +-- -- stay, because it breaks the current easy-to-evaluate bound on the memory +-- -- requirement of a Copilot monitor. +-- shouldBeRight :: Streams +-- shouldBeRight = do +-- "v1" .= [0] ++ varI32 "v1" + 1 +-- "v2" .= drop 2 (varI32 "v1") + +-- shouldBeRight2 :: Streams +-- shouldBeRight2 = do +-- "loop1" .= [0] ++ varI32 "loop2" + 2 +-- "loop2" .= [1] ++ varI32 "loop1" - 1 +-- "other" .= drop 3 (varI32 "loop1") diff --git a/Language/Copilot/Examples/LTLExamples.hs b/Language/Copilot/Examples/LTLExamples.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Examples/LTLExamples.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Language.Copilot.Examples.LTLExamples () where + +import Prelude (replicate, Int) + +import Language.Copilot.Core +import Language.Copilot.Language +import Language.Copilot.Variables +import Language.Copilot.Libs.LTL +import Language.Copilot.Libs.Indexes + +---------------- +-- LTL tests --- +---------------- + +test, output :: Var +test = "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) + + +tLatest :: Int -> Streams +tLatest n = do test .= (replicate (n-2) False) ++ const True + output .= latest n (var test) + + +tAlways :: Int -> Streams +tAlways n = do test .= (replicate (n+3) True) ++ const False + output .= always n (varB test) + + +tFuture :: Int -> Streams +tFuture n = do test .= (replicate (n+3) False) ++ varB a + a .= [False] ++ not (var a) + output .= eventually n (varB test) + + +tUntil :: Int -> Streams +tUntil n = do "t1" .= (replicate (n+2) False) ++ varB c + c .= [True] ++ not (var c) + "t0" .= const True + output .= until n (varB "t0") (varB "t1") + + +tRelease0 :: Int -> Streams +tRelease0 n = do output .= release n (const False) (const True) + + +tRelease1 :: Int -> Streams +tRelease1 n = do "t1" .= (replicate (n+2) True) ++ varB c + c .= [False] ++ not (var c) + "t0" .= const True + output .= release n (varB "t0") (varB "t1") + diff --git a/Language/Copilot/Examples/PTLTLExamples.hs b/Language/Copilot/Examples/PTLTLExamples.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Examples/PTLTLExamples.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Language.Copilot.Examples.PTLTLExamples where + +import Prelude () + +import Language.Copilot.Core +import Language.Copilot.Language +import Language.Copilot.Interface +import Language.Copilot.Variables +import Language.Copilot.PrettyPrinter +import Language.Copilot.Libs.PTLTL + +-- Next examples are for testing of the ptLTL library + +-- test of previous +tstdatprv :: Streams +tstdatprv = a .= [True, False] ++ varB a + +tprv :: Streams +tprv = do + tstdatprv + c `previous` (varB a) + +-- test of alwaysBeen +tstdatAB :: Streams +tstdatAB = d .= [True, True, True, True, True, True, True, False] ++ varB d + +tAB :: Streams +tAB = do + tstdatAB + f `alwaysBeen` (var d) + +-- test of eventuallyPrev +tstdatEP :: Streams +tstdatEP = g .= [False, False, False, False, False, True, False] ++ varB g + +tEP :: Streams +tEP = do + tstdatEP + h `eventuallyPrev` (varB g) + +-- test of since +tstdat1Sin :: Streams +tstdat1Sin = "q1" .= [True, True, True, True, True, True, False ] ++ varB "q1" + +tstdat2Sin :: Streams +tstdat2Sin = "q2" .= [False, False, True, False, False, False, False ] ++ varB "q2" + +tSin :: Streams +tSin = do + tstdat1Sin + tstdat2Sin + "z1" `since` (varB "q1", varB "q2") + +-- with external variables +-- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20 +tSinExt :: Streams +tSinExt = do + "z1" `since` (extB "e1" 2, extB "q2" 3) diff --git a/Language/Copilot/Examples/StatExamples.hs b/Language/Copilot/Examples/StatExamples.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Examples/StatExamples.hs @@ -0,0 +1,21 @@ +module Language.Copilot.Examples.StatExamples where + +import Prelude () +import Language.Copilot.Core +import Language.Copilot.Language +import Language.Copilot.Interface +import Language.Copilot.Variables +import Language.Copilot.PrettyPrinter +import Language.Copilot.Libs.Statistics + +t0 :: Streams +t0 = do + a .= [0..5] ++ (varW16 a) + 6 + "min" .= min 3 (varW16 a) + "max" .= max 3 (varW16 a) + "sum" .= sum 3 (varW16 a) + +tMean :: Streams +tMean = do + a .= [0..5] ++ (varD a) + 6 + "out" .= mean 4 (varD a) diff --git a/Language/Copilot/Help.hs b/Language/Copilot/Help.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Help.hs @@ -0,0 +1,178 @@ +-- | Help to display. +module Language.Copilot.Help (helpStr) + +where + +helpStr :: String +helpStr = + unlines + [ "" + , "USAGE:" + , "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 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 FILENAME [$ OPTS] baseOpts" + , " Compiles the Copilot specification STREAMS to constant-time & constant-" + , " constant-space C program named FILENAME.c with header FILENAME.h" + , " and executable FILENAME." + , "" + , " > test RNDS [$ OPTS] baseOpts" + , " Generates a random set of streams & inputs for external variables, and" + , " tests the equivalence between the output of the compiled C program and" + , " 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." + , "" + , " > Prelude.putStr $ Prelude.show STREAMS -- or simply" + , " > STREAMS -- in ghci" + , " Pretty-prints the parsed Copilot specification of type 'Streams'." + , "" + , " > verify PATH/FILE.c" + , " 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" + , " should be no incorrect C programs generated by the Copilot compiler," + , " cbmc provides independent evidence of this claim. Specifically, it" + , " 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" + , " ." + , "" + , " > help " + , " Displays this help message." + , "" + , "" + , "OPTIONS:" + , "In the following, we designate the interpreter by (i), the compiler by (c)," + , "and the test function by (t). Options are marked by which tool they are" + , "relevant to; e.g., (i, t) means that an option is relevant to the" + , "interpreter and test functions." + , "" + , "For each option, there is a default, that is included in baseOpts. For" + , "each option, we describe the default." + , "" + , " setE :: Vars -> Options -> Options (i)" + , " default: Nothing (no assignments)" + , " Set the environment for program variables. E.g., for the spec" + , "" + , " t :: Streams" + , " t = \"a\" .= [0,1] ++ extW32 \"ext0\" 7 + extW32 \"ext1\" 8 " + , " .| end" + , "" + , " setE (emptySM {w32Map = fromList " + , " [ (\"ext0\", [0,1..])" + , " , (\"ext1\", [3,3..])]})" + , " assigns external variable \"ext0\" the values 0,1,2... and " + , " external variable \"ext1\" the values 3,3,3... over Word32 in the" + , " sequential rounds. " + , "" + , " setV :: Verbose -> Options -> Options (i, c, t)" + , " default: DefaultVerbose" + , " Set the verbosity level. One of OnlyErrors | DefaultVerbose | Verbose." + , "" + , " setGCC :: String -> Options -> Options (c, t)" + , " default: \"gcc\"" + , " Sets the compiler to use, given as a path (String) to the executable." + , "" + , " setDir :: String -> Options -> Options (c, t)" + , " default: \"./\"" + , " The location for the generated .c, .h, and binary files. The" + , " path can be either absolute or relative, but MUST containing the" + , " trailing '/'." + , "" + , " setC :: String -> Options -> Options (c, t)" + , " default: Nothing" + , " Set the additional options to pass to the compiler. E.g.," + , " setC \"-O2\"." + , "" + , " setP :: Period -> Options -> Options (c, t)" + , " default: automatically computed minimal period." + , " Manually set the number of ticks per period for execution. An error" + , " is returned if the number is too small. For any program, the number" + , " of ticks must be at least 2." + , "" + , " setPP :: (String, String) -> Options -> Options (c)" + , " default: Nothing. The default generates a main() function that calls" + , " Copilot code to run simulations." + , "" + , " Sets C code to pretty-print before and after the generated Copilot" + , " code: the before code is the first element of the tuple and the after" + , " code is the second element. For writing ad-hoc C, please see" + , " Language.Copilot.AdHocC (and please add to it and send patches!)." + , " For exmple, pre-code might include 'includes'. Post-code might include" + , " a custom main() function. ('PP' stands for 'pretty-print'.)" + , "" + , " NOTE: when the pre-/post-code is anything but Nothing, the C compiler" + , " is NOT called---we assume you're doing a custom build. We do NOT" + , " instrument your code with a 'main()' function simulator. Use this" + , " function to generate embedded programs." + , "" + , " setTriggers :: [(Var, String)] -> Options -> Options (c)" + , " Provide a list of pairs '(v, n)', where 'v' is a Copilot variable" + , " (a String) denoting a stream of Booleans, and 'n' is the name of a C" + , " function to call if that stream ever takes the value True. The" + , " declaration of the C function must be 'void n(void)'. 'n()' is called" + , " in phase 0, the same phase that the state is updated (that is, the" + , " trigger fires at the soonest phase possible." + , "" + , " setTriggers MUST be used in conjunction with the setPP option, as the" + , " simulator does not know about custom trigger functions." + , "" + , " setO :: Name -> Options -> Options (t)" + , " default: \"copilotProgram\"" + , " Sets the name of the executable (e.g., -o) generated by the C" + , " compiler." + , "" + , "" + , "EXAMPLES:" + , "The following examples reference Copilot specs defined in" + , "Language.Copilot.Examples.Examples." + , "" + , " > interpret t0 50 baseOpts" + , " Interprets t0 for 50 iterations." + , "" + , " > interpret t3 40" + , " $ setE setE (emptySM {w32Map = fromList " + , " [ (\"ext0\", [0,1..])" + , " , (\"ext1\", [3,3..])]})" + , " $ setV Verbose baseOpts" + , " Interpret t3 for 40 iterations, seeding the external variable \"ext\"" + , " to [0,1,..], with 'Verbose' verbosity." + , "" + , " > compile t1 \"t1\" baseOpts" + , " Compile Copilot spec t1 to t1.c, t1.h, and executable t1 in the default" + , " directory, /tmp/copilot/ . This is compiled with a simulation main()" + , "" + , " > compile t2 \"t2\" $ setC \"-O2\" $ setP 100 baseOpts" + , " Compile Copilot spec t2 to t2.c, t2.h, and executable t2 in the default" + , " directory, /tmp/copilot/ , with optimization level -02 and period 100." + , " This is compiled with a simulation main()." + , "" + , " > compile t2 \"t2\" $ setTriggers [(\"b0\",\"foo0\"), (\"b1\",\"foo1\")]" + , " $ setPP (pre, post) baseOpts" + , " Compile Copilot spec t2 to t2.c, with triggers void 'foo0(void)' and" + , " 'void foo1(void)' for Boolean Copilot streams \"b0\" and \"b1\"," + , " respectively. 'pre' and 'post' are constants that (at least) provide" + , " headers for foo0 and foo1 (in 'pre') and definitions for foo0 and foo1" + , " in 'post'." + , "" + , " > test 1000 baseOpts" + , " Compare the compiler and interpreter for a randomly-generated Copilot" + , " spec for 1000 iterations." + , "" + , " > Prelude.sequence_ [test 100 $ setR x baseOpts | x <- [0..100]]" + , " Compare the compiler and interpreter on 100 randomly-generated Copilot" + , " specs, for 100 iterations each." + , "" + , " > verify \"foo.c\"" + , " Calls cbmc on foo.c (where foo.c is in the current directory)." + ] diff --git a/Language/Copilot/Interface.hs b/Language/Copilot/Interface.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Interface.hs @@ -0,0 +1,243 @@ +-- | Used by the end-user to easily give its arguments to dispatch. +module Language.Copilot.Interface ( + Options(), baseOpts, test, interpret, compile, verify, interface + , help , setS, setE, setC, setO, setP, setI, setPP, setN, setV, setR + , setDir, setGCC, setTriggers, + module Language.Copilot.Dispatch + ) where + +import Language.Copilot.Core +import Language.Copilot.Language (opsF, opsF2, opsF3) +import Language.Copilot.Tests.Random +import Language.Copilot.Dispatch +import Language.Copilot.Help + +import Data.Set as Set (fromList, toList) +import Data.List ((\\)) +import System.Random +import System.Exit +import System.FilePath (takeBaseName) +import System.Cmd +import Data.Maybe +import Control.Monad +import Control.Monad.Writer (execWriter) + +data Options = Options { + optStreams :: Maybe Streams, -- ^ If there's no Streams, then generate random streams. + optSends :: Sends, -- ^ For distributed monitors. + optExts :: Maybe Vars, -- ^ Assign values to external variables. + optCompile :: Maybe String, -- ^ Set gcc options. + optPeriod :: Maybe Period, -- ^ Set the period. If none is given, then the smallest feasible period is computed. + optInterpret :: Bool, -- ^ Interpreting? + optIterations :: Int, -- ^ How many iterations are we simulating for? + optVerbose :: Verbose, -- ^ Verbosity level: OnlyErrors | DefaultVerbose | Verbose. + optRandomSeed :: Maybe Int, -- ^ Random seed for generating Copilot specs. + optCName :: Name, -- ^ Name of the C file generated. + 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. + } + +baseOpts :: Options +baseOpts = Options { + optStreams = Nothing, + optSends = emptySM, + optExts = Nothing, + optCompile = Nothing, + optPeriod = Nothing, + optInterpret = False, + optIterations = 0, + optVerbose = DefaultVerbose, + optRandomSeed = Nothing, + optCName = "copilotProgram", + optCompiler = "gcc", + optOutputDir = "./", + optPrePostCode = Nothing, + optTriggers = Nothing + } + +-- Functions for making it easier for configuring copilot in the frequent use cases + +test :: Int -> Options -> IO () +test n opts = + interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ opts + +interpret :: Streams -> Int -> Options -> IO () +interpret streams n opts = interface $ setI $ setN n $ opts {optStreams = Just streams} + +compile :: Streams -> Name -> Options -> IO () +compile streams fileName opts = + interface $ setC "-Wall" $ setO fileName $ opts {optStreams = Just streams} + +verify :: FilePath -> IO () +verify file = do + putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke " + putStrLn ", with the following checks:" + putStrLn " --bounds-check enable array bounds checks" + putStrLn " --div-by-zero-check enable division by zero checks" + putStrLn " --pointer-check enable pointer checks" + putStrLn " --overflow-check enable arithmetic over- and underflow checks" + putStrLn " --nan-check check floating-point for NaN" + putStrLn "" + putStrLn $ " assuming " ++ theMain ++ " as the entry point:" + putStrLn cmd + code <- system cmd + case code of + ExitSuccess -> return () + _ -> do putStrLn $ "cbmc could not be called on file " ++ file ++ "." + putStrLn "Perhaps cbmc is not installed on your system, is" + putStrLn "not in your path, cbmc cannot be called from the" + putStrLn $ "command line on your system, or " ++ file + putStrLn $ "does not exist, or the dispatch function in" ++ file + putStrLn $ "is not called " ++ theMain ++ "." + putStrLn "See " + putStrLn "for more information on cbmc." + where theMain = takeBaseName file + cmd = unwords ("cbmc" : args) + args = ["--div-by-zero-check", "--overflow-check", "--bounds-check" + , "--nan-check", "--pointer-check" + , "--function " ++ theMain, file] + + + +-- 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., +-- +-- @ setE (emptySM {w32Map = fromList [(\"ext\", [0,1..])]}) ... @ +-- +-- sets the external variable names "ext" to take the natural numbers, up to the limit of Word32. +setE :: Vars -> Options -> Options +setE vs opts = opts {optExts = Just vs} + +-- | Sets the options for the compiler, e.g., +-- +-- @ setC \"-O2\" ... @ +-- +-- Sets gcc options. +setC :: String -> Options -> Options +setC gccOptions opts = opts {optCompile = Just gccOptions} + +-- | Manually set the period for the program. Otherwise, the minimum required period is computed automatically. E.g., +-- +-- @ setP 100 ... @ +-- sets the period to be 100. The period must be at least 1. +setP :: Period -> Options -> Options +setP p opts = opts {optPeriod = Just p} + +setI :: Options -> Options +setI opts = opts {optInterpret = True} + +-- | Sets the number of iterations of the program to simulation: +-- +-- @ setN 50 @ +-- simulations the program for 50 steps. +setN :: Int -> Options -> Options +setN n opts = opts {optIterations = n} + +-- | Set the verbosity level. +setV :: Verbose -> Options -> Options +setV v opts = opts {optVerbose = v} + +setR :: Int -> Options -> Options +setR seed opts = opts {optRandomSeed = Just seed} + +setO :: Name -> Options -> Options +setO fileName opts = opts {optCName = fileName} + +-- | Sets the compiler to use, given as a path to the executable. The default +-- is \"gcc\". +setGCC :: String -> Options -> Options +setGCC compilerStr opts = opts {optCompiler = compilerStr} + +-- | Sets the directory into which the output of compiled programs should be +-- placed. If the directory does not exist, it will be created. +setDir :: String -> Options -> Options +setDir dir opts = opts {optOutputDir = dir} + +-- | Sets the code to precede and follow the copilot specification +-- If nothing, then code appropriate for communication with the interpreter is generated +setPP :: (String, String) -> Options -> Options +setPP pp opts = opts {optPrePostCode = Just pp} + +-- | Give C function triggers for Copilot Boolean streams. The tiggers fire if +-- the stream becoms true. +setTriggers :: [(Var, String)] -> Options -> Options +setTriggers triggers opts = + if null repeats + then opts {optTriggers = Just triggers} + else error $ "Error: only one trigger per Copilot variable. Variables " + ++ show (Set.fromList repeats) ++ " are given multiple triggers." + where vars = map fst triggers + repeats = vars \\ Set.toList (Set.fromList vars) + +-- | The "main" function +interface :: Options -> IO () +interface opts = + do + seed <- createSeed opts + let (streams, vars) = getStreamsVars opts seed + sends = optSends opts + backEnd = getBackend opts seed + iterations = optIterations opts + verbose = optVerbose opts + when (verbose == Verbose) $ + putStrLn $ "Random seed :" ++ show seed + -- dispatch is doing all the heavy plumbing between + -- analyser, compiler, interpreter, gcc and the generated program + dispatch streams sends vars backEnd iterations verbose + +createSeed :: Options -> IO Int +createSeed opts = + case optRandomSeed opts of + Nothing -> + do + g <- newStdGen + return . fst . random $ g + Just i -> return i + +getStreamsVars :: Options -> Int -> (StreamableMaps Spec, Vars) +getStreamsVars opts seed = + case optStreams opts of + Nothing -> randomStreams opsF opsF2 opsF3 (mkStdGen seed) + Just s -> + case optExts opts of + Nothing -> (s', emptySM) + Just vs -> (s', vs) + where s' = execWriter s + +getBackend :: Options -> Int -> BackEnd +getBackend opts seed = + case optCompile opts of + Nothing -> + if not $ optInterpret opts + then error "neither interpreted nor compiled: nothing to be done" + else Interpreter + Just gccOptions -> + Opts $ AtomToC { + cName = optCName opts ++ if isJust $ optRandomSeed opts then show seed else "", + gccOpts = gccOptions, + getPeriod = optPeriod opts, + interpreted = if optInterpret opts then Interpreted else NotInterpreted, + outputDir = optOutputDir opts, + compiler = optCompiler opts, + prePostCode = optPrePostCode opts, + triggers = optTriggers opts + } + +help :: IO () +help = putStrLn helpStr diff --git a/Language/Copilot/Interpreter.hs b/Language/Copilot/Interpreter.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Interpreter.hs @@ -0,0 +1,34 @@ +-- | This interpreter is mostly used for checking the /Copilot/ implementation. +-- But it can also be used for quick testing of a /Copilot/ design +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. +interpretStreams :: StreamableMaps Spec -> Vars -> Vars +interpretStreams streams moVs = + inVs + where + inVs = mapStreamableMaps (\ _ -> interpret inVs moVs) streams + +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) diff --git a/Language/Copilot/Language.hs b/Language/Copilot/Language.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Language.hs @@ -0,0 +1,509 @@ +{-# LANGUAGE NoImplicitPrelude, Rank2Types, ScopedTypeVariables, FlexibleContexts #-} + +-- | Describes the language /Copilot/. +-- +-- If you wish to add a new operator, the only modification needed is adding it in this module. +-- But if you want it to be used in the random generated streams, add it to either @'opsF'@, @'opsF2'@ or @'opsF3'@ +module Language.Copilot.Language ( + -- * Operators and functions + mod, div, mod0, div0, + (<), (<=), (==), (/=), (>=), (>), + not, (||), (&&), (^), (==>), + -- * Boolean constants + Bool(..), + -- * Arithmetic operators (derived) + Num(..), + -- * Division + Fractional((/)), + mux, + CastIntTo(..), + -- * The next functions are used only to coerce the type of their argument + bool, int8, int16, int32, int64, + word8, word16, word32, word64, float, double, + -- * The next functions provide easier access to typed external variables. + extB, extI8, extI16, extI32, extI64, + extW8, extW16, extW32, extW64, extF, extD, + -- * Set of operators from which to choose during the generation of random streams + opsF, opsF2, opsF3, + -- * Constructs of the copilot language + var, const, drop, (++), (.=), (..|), + -- * The next functions are typed variable declarations to help the type-checker. + varB, varI8, varI16, varI32, varI64, + varW8, varW16, varW32, varW64, varF, varD, + -- * The next functions help typing the send operations + -- Warning: there is no typechecking of that yet + -- sendB, sendI8, sendI16, sendI32, sendI64, + sendW8, -- , sendW16, sendW32, sendW64, sendF, sendD + -- * Typed constant declarations. + constB, constI8, constI16, constI32, constI64, + constW8, constW16, constW32, constW64, constF, constD + ) where + +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 qualified Prelude as P +import Control.Monad.Writer + +import Language.Copilot.Core +import Language.Copilot.Analyser +import Language.Copilot.Tests.Random + +---- Operators and functions --------------------------------------------------- + +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. +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) + +(<), (<=), (>=), (>) :: (Streamable a, A.OrdE a) => Spec a -> Spec a -> Spec Bool +(<) = F2 (P.<) (A.<.) +(<=) = F2 (P.<=) (A.<=.) +(>=) = F2 (P.>=) (A.>=.) +(>) = F2 (P.>) (A.>.) + +(==), (/=) :: (Streamable a, A.EqE a) => Spec a -> Spec a -> Spec Bool +(==) = F2 (P.==) (A.==.) +(/=) = F2 (P./=) (A./=.) + +(||), (&&), (^), (==>) :: Spec Bool -> Spec Bool -> Spec Bool +(||) = F2 (P.||) (A.||.) +(&&) = F2 (P.&&) (A.&&.) +(^) = F2 + (\ x y -> (x P.&& P.not y) P.|| (y P.&& P.not x)) + (\ x y -> (x A.&&. A.not_ y) A.||. (y A.&&. A.not_ x)) +(==>) = F2 (\ x y -> y P.|| P.not x) A.imply + +class (Streamable a, P.Integral a) => CastIntTo a where + cast :: (Streamable b, A.IntegralE b) => Spec b -> Spec a + +instance CastIntTo Word8 where + cast = F (P.fromInteger P.. P.toInteger) ( + A.Retype P.. A.ue P.. (`A.mod_` (256::(A.E Word64))) P.. A.Retype P.. A.ue) +instance CastIntTo Word16 where + cast = F (P.fromInteger P.. P.toInteger) ( + 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) +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) +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) +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) +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) + + +-- | Beware : both sides are executed, even if the result of one is later discarded +mux :: (Streamable a) => Spec Bool -> Spec a -> Spec a -> Spec a +mux = F3 (\ b x y -> if b then x else y) A.mux + +infix 5 ==, /=, <, <=, >=, > +infixr 4 ||, &&, ^, ==> + +-- Used for helping ghc in infering the type of the streams +bool :: Spec Bool -> Spec Bool +int8 :: Spec Int8 -> Spec Int8 +int16 :: Spec Int16 -> Spec Int16 +int32 :: Spec Int32 -> Spec Int32 +int64 :: Spec Int64 -> Spec Int64 +word8 :: Spec Word8 -> Spec Word8 +word16 :: Spec Word16 -> Spec Word16 +word32 :: Spec Word32 -> Spec Word32 +word64 :: Spec Word64 -> Spec Word64 +float :: Spec Float -> Spec Float +double :: Spec Double -> Spec Double +bool = P.id +int8 = P.id +int16 = P.id +int32 = P.id +int64 = P.id +word8 = P.id +word16 = P.id +word32 = P.id +word64 = P.id +float = P.id +double = P.id + +-- Used for easily producing, and coercing PVars +extB :: Var -> Phase -> Spec Bool +extB = PVar A.Bool +extI8 :: Var -> Phase -> Spec Int8 +extI8 = PVar A.Int8 +extI16 :: Var -> Phase -> Spec Int16 +extI16 = PVar A.Int16 +extI32 :: Var -> Phase -> Spec Int32 +extI32 = PVar A.Int32 +extI64 :: Var -> Phase -> Spec Int64 +extI64 = PVar A.Int64 +extW8 :: Var -> Phase -> Spec Word8 +extW8 = PVar A.Word8 +extW16 :: Var -> Phase -> Spec Word16 +extW16 = PVar A.Word16 +extW32 :: Var -> Phase -> Spec Word32 +extW32 = PVar A.Word32 +extW64 :: Var -> Phase -> Spec Word64 +extW64 = PVar A.Word64 +extF :: Var -> Phase -> Spec Float +extF = PVar A.Float +extD :: Var -> Phase -> Spec Double +extD = PVar A.Double + +---- Sets of operators for Tests.Random.hs ------------------------------------- + +---- Helper functions + +mkOp :: (Random arg1, Streamable arg1) => + (Spec arg1 -> Spec r) -> Operator r +mkOp op = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet in + (op s0, g0) + ) + +mkOp2 :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) => + (Spec arg1 -> Spec arg2 -> Spec r) -> Operator r +mkOp2 op = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet in + (op s0 s1, g1) + ) + +mkOp3 :: (Random arg1, Random arg2, Random arg3, + Streamable arg1, Streamable arg2, Streamable arg3) => + (Spec arg1 -> Spec arg2 -> Spec arg3 -> Spec r) -> Operator r +mkOp3 op = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet + (s2, g2) = rand g1 FunSpecSet in + (op s0 s1 s2, g2) + ) + +mkOp2Coerce :: (Random arg1, Random arg2, Streamable arg1, Streamable arg2) => + (Spec arg1 -> Spec arg2 -> Spec r) -> arg1 -> arg2 -> Operator r +mkOp2Coerce op c0 c1 = + Operator (\ rand g -> + let (s0, g0) = rand g FunSpecSet + (s1, g1) = rand g0 FunSpecSet in + (op (s0 `P.asTypeOf` (Const c0)) (s1 `P.asTypeOf` (Const c1)), g1) + ) + +mkOp2Ord :: forall r. (forall arg. + (Random arg, A.OrdE arg, Streamable arg) => + (Spec arg -> Spec arg -> Spec r)) + -> Operator r +mkOp2Ord op = + let opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: + RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g) + opI8 = fromOp P.$ mkOp2Coerce op (unit::Int8) (unit::Int8) + opI16 = fromOp P.$ mkOp2Coerce op (unit::Int16) (unit::Int16) + opI32 = fromOp P.$ mkOp2Coerce op (unit::Int32) (unit::Int32) + opI64 = fromOp P.$ mkOp2Coerce op (unit::Int64) (unit::Int64) + opW8 = fromOp P.$ mkOp2Coerce op (unit::Word8) (unit::Word8) + opW16 = fromOp P.$ mkOp2Coerce op (unit::Word16) (unit::Word16) + opW32 = fromOp P.$ mkOp2Coerce op (unit::Word32) (unit::Word32) + opW64 = fromOp P.$ mkOp2Coerce op (unit::Word64) (unit::Word64) + opF = fromOp P.$ mkOp2Coerce op (unit::Float) (unit::Float) + opD = fromOp P.$ mkOp2Coerce op (unit::Double) (unit::Double) in + Operator (\ rand g -> + let (t, g0) = randomR (A.Int8, A.Double) g in + case t of + A.Int8 -> opI8 rand g0 + A.Int16 -> opI16 rand g0 + A.Int32 -> opI32 rand g0 + A.Int64 -> opI64 rand g0 + A.Word8 -> opW8 rand g0 + A.Word16 -> opW16 rand g0 + A.Word32 -> opW32 rand g0 + A.Word64 -> opW64 rand g0 + A.Float -> opF rand g0 + A.Double -> opD rand g0 + _ -> P.error "Impossible" + ) + +mkOp2Eq :: forall r. (forall arg. + (Random arg, A.EqE arg, Streamable arg) => + (Spec arg -> Spec arg -> Spec r)) + -> Operator r +mkOp2Eq op = + let opB, opI8, opI16, opI32, opI64, opW8, opW16, opW32, opW64, opF, opD :: + RandomGen g => + (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec r, g) + opB = fromOp P.$ mkOp2Coerce op (unit::Bool) (unit::Bool) + opI8 = fromOp P.$ mkOp2Coerce op (unit::Int8) (unit::Int8) + opI16 = fromOp P.$ mkOp2Coerce op (unit::Int16) (unit::Int16) + opI32 = fromOp P.$ mkOp2Coerce op (unit::Int32) (unit::Int32) + opI64 = fromOp P.$ mkOp2Coerce op (unit::Int64) (unit::Int64) + opW8 = fromOp P.$ mkOp2Coerce op (unit::Word8) (unit::Word8) + opW16 = fromOp P.$ mkOp2Coerce op (unit::Word16) (unit::Word16) + opW32 = fromOp P.$ mkOp2Coerce op (unit::Word32) (unit::Word32) + opW64 = fromOp P.$ mkOp2Coerce op (unit::Word64) (unit::Word64) + opF = fromOp P.$ mkOp2Coerce op (unit::Float) (unit::Float) + opD = fromOp P.$ mkOp2Coerce op (unit::Double) (unit::Double) in + Operator (\ rand g -> + let (t, g0) = random g in + case t of + A.Bool -> opB rand g0 + A.Int8 -> opI8 rand g0 + A.Int16 -> opI16 rand g0 + A.Int32 -> opI32 rand g0 + A.Int64 -> opI64 rand g0 + A.Word8 -> opW8 rand g0 + A.Word16 -> opW16 rand g0 + A.Word32 -> opW32 rand g0 + A.Word64 -> opW64 rand g0 + A.Float -> opF rand g0 + A.Double -> opD rand g0 + ) + +---- Definition of each operator + +not_ :: Operator Bool +not_ = mkOp not + +(+$), (-$), (*$) :: (Streamable a, A.NumE a, Random a) => Operator a +(+$) = mkOp2 (P.+) +(-$) = mkOp2 (P.-) +(*$) = mkOp2 (P.*) + +(/$) :: (Streamable a, A.NumE a, Fractional a, Random a) => Operator a +(/$) = mkOp2 (P./) + +(<$), (<=$), (>=$), (>$) :: Operator Bool +(<$) = mkOp2Ord (<) +(<=$) = mkOp2Ord (<=) +(>=$) = mkOp2Ord (>=) +(>$) = mkOp2Ord (>) + +(==$), (/=$) :: Operator Bool +(==$) = mkOp2Eq (==) +(/=$) = mkOp2Eq (/=) + +(||$), (&&$), (^$), (==>$) :: Operator Bool +(||$) = mkOp2 (||) +(&&$) = mkOp2 (&&) +(^$) = mkOp2 (^) +(==>$) = mkOp2 (==>) + +mux_ :: (Streamable a, Random a) => Operator a +mux_ = mkOp3 mux + +-- Packing of the operators in StreamableMaps + +createMapFromElems :: [val] -> M.Map Var val +createMapFromElems vals = + let ks = [[x] | x <- ['a'..]] + l = zip ks vals in + M.fromAscList l + +-- | opsF, opsF2 and opsF3 are feeded to Tests.Random.randomStreams. +-- They allows the random generated streams to include lots of operators. +-- If you add a new operator to Copilot, it would be nice to add it to one of those, +-- that way it could be used in the random streams used for testing. +-- opsF holds all the operators of arity 1, opsF2 of arity 2 and opsF3 of arity3 +-- They are StreamableMaps, because operators are sorted based on their return type. +opsF, opsF2, opsF3 :: Operators +opsF = emptySM {bMap = createMapFromElems [not_]} + +opsF2 = emptySM { + bMap = createMapFromElems [(<$), (<=$), (>=$), (>$), (==$), (/=$), (||$), (&&$), (^$), (==>$)], + i8Map = createMapFromElems [(+$), (-$), (*$)], + i16Map = createMapFromElems [(+$), (-$), (*$)], + i32Map = createMapFromElems [(+$), (-$), (*$)], + i64Map = createMapFromElems [(+$), (-$), (*$)], + w8Map = createMapFromElems [(+$), (-$), (*$)], + w16Map = createMapFromElems [(+$), (-$), (*$)], + w32Map = createMapFromElems [(+$), (-$), (*$)], + w64Map = createMapFromElems [(+$), (-$), (*$)], + fMap = createMapFromElems [(+$), (-$), (*$), (/$)], + dMap = createMapFromElems [(+$), (-$), (*$), (/$)] + } + +opsF3 = emptySM { + bMap = createMapFromElems [mux_], + i8Map = createMapFromElems [mux_], + i16Map = createMapFromElems [mux_], + i32Map = createMapFromElems [mux_], + i64Map = createMapFromElems [mux_], + w8Map = createMapFromElems [mux_], + w16Map = createMapFromElems [mux_], + w32Map = createMapFromElems [mux_], + w64Map = createMapFromElems [mux_], + fMap = createMapFromElems [mux_], + dMap = createMapFromElems [mux_] + } + +---- Constructs of the language ------------------------------------------------ + +-- | Stream variable reference +var :: Streamable a => Var -> Spec a +var v = Var v + +-- If a generic 'var' declaration is insufficient for the type-checker to determine the type, a monomorphic var operator can be used +varB :: Var -> Spec Bool +varB = Var +varI8 :: Var -> Spec Int8 +varI8 = Var +varI16 :: Var -> Spec Int16 +varI16 = Var +varI32 :: Var -> Spec Int32 +varI32 = Var +varI64 :: Var -> Spec Int64 +varI64 = Var +varW8 :: Var -> Spec Word8 +varW8 = Var +varW16 :: Var -> Spec Word16 +varW16 = Var +varW32 :: Var -> Spec Word32 +varW32 = Var +varW64 :: Var -> Spec Word64 +varW64 = Var +varF :: Var -> Spec Float +varF = Var +varD :: Var -> Spec Double +varD = Var + +{- +sendB :: Var -> (Phase, Port) -> Send Bool +sendB v (ph, port) = Send (v, ph, port) +sendI8 :: Var -> (Phase, Port) -> Send Int8 +sendI8 v (ph, port) = Send (v, ph, port) +sendI16 :: Var -> (Phase, Port) -> Send Int16 +sendI16 v (ph, port) = Send (v, ph, port) +sendI32 :: Var -> (Phase, Port) -> Send Int32 +sendI32 v (ph, port) = Send (v, ph, port) +sendI64 :: Var -> (Phase, Port) -> Send Int64 +sendI64 v (ph, port) = Send (v, ph, port) -} +sendW8 :: Var -> (Phase, Port) -> Send Word8 +sendW8 v (ph, port) = Send (v, ph, port) +{- sendW16 :: Var -> (Phase, Port) -> Send Word16 +sendW16 v (ph, port) = Send (v, ph, port) +sendW32 :: Var -> (Phase, Port) -> Send Word32 +sendW32 v (ph, port) = Send (v, ph, port) +sendW64 :: Var -> (Phase, Port) -> Send Word64 +sendW64 v (ph, port) = Send (v, ph, port) +sendF :: Var -> (Phase, Port) -> Send Float +sendF v (ph, port) = Send (v, ph, port) +sendD :: Var -> (Phase, Port) -> Send Double +sendD v (ph, port) = Send (v, ph, port) -} + +-- | A constant stream +const :: Streamable a => a -> Spec a +const x = Const x + +constB :: Bool -> Spec Bool +constB = Const +constI8 :: Int8 -> Spec Int8 +constI8 = Const +constI16 :: Int16 -> Spec Int16 +constI16 = Const +constI32 :: Int32 -> Spec Int32 +constI32 = Const +constI64 :: Int64 -> Spec Int64 +constI64 = Const +constW8 :: Word8 -> Spec Word8 +constW8 = Const +constW16 :: Word16 -> Spec Word16 +constW16 = Const +constW32 :: Word32 -> Spec Word32 +constW32 = Const +constW64 :: Word64 -> Spec Word64 +constW64 = Const +constF :: Float -> Spec Float +constF = Const +constD :: Double -> Spec Double +constD = Const + + +-- | Drop @i@ elements from a stream. +drop :: Streamable a => Int -> Spec a -> Spec a +drop i s = Drop i s + +-- | Just a trivial wrapper over the @'Append'@ constructor +(++) :: Streamable a => [a] -> Spec a -> Spec a +ls ++ s = Append ls s + +-- | Define a stream variable. +(.=) :: Streamable a => Var -> Spec a -> Streams +v .= s = tell (updateSubMap (M.insert v s) emptySM) + +-- | Allows to build a @'Sends'@ from specification +(..|) :: Sendable a => Send a -> Sends -> Sends +sendStmt@(Send (v, ph, port)) ..| sends = + updateSubMap (M.insert name sendStmt) sends + where name = v P.++ "_" P.++ show ph P.++ "_" P.++ show port + +infixr 3 ++ +infixr 2 .= +infixr 1 ..| + +---- Optimisation rules -------------------------------------------------------- + +{-# RULES +"Copilot.Language Plus0R" forall s. (P.+) s (Const 0) = s +"Copilot.Language Plus0L" forall s. (P.+) (Const 0) s = s +"Copilot.Language Minus0R" forall s. (P.-) s (Const 0) = s +"Copilot.Language Minus0L" forall s. (P.-) (Const 0) s = s +"Copilot.Language Times1R" forall s. (P.*) s (Const 1) = s +"Copilot.Language Times1L" forall s. (P.*) (Const 1) s = s +"Copilot.Language Times0R" forall s. (P.*) s (Const 0) = Const 0 +"Copilot.Language Times0L" forall s. (P.*) (Const 0) s = Const 0 +"Copilot.Language FracBy0" forall s. (P./) s (Const 0.0) = P.error "division by zero !" +"Copilot.Language FracBy1" forall s. (P./) s (Const 1.0) = s +"Copilot.Language Frac0" forall s. (P./) (Const 0.0) s = (Const 0.0) +"Copilot.Language OrFR" forall s. (||) s (Const False) = s +"Copilot.Language OrFL" forall s. (||) (Const False) s = s +"Copilot.Language OrTR" forall s. (||) s (Const True) = Const True +"Copilot.Language OrTL" forall s. (||) (Const True) s = Const True +"Copilot.Language AndFR" forall s. (&&) s (Const False) = Const False +"Copilot.Language AndFL" forall s. (&&) (Const False) s = Const False +"Copilot.Language AndTR" forall s. (&&) s (Const True) = s +"Copilot.Language AndTL" forall s. (&&) (Const True) s = s +"Copilot.Language ImpliesFL" forall s. (==>) (Const False) s = Const True +"Copilot.Language NotF" not (Const False) = Const True +"Copilot.Language NotT" not (Const True) = Const False +"Copilot.Language MuxF" forall s0 s1. mux (Const False) s0 s1 = s1 +"Copilot.Language MuxT" forall s0 s1. mux (Const True) s0 s1 = s0 +"Copilot.Language ImpliesDef" forall s0 s1. (||) s1 (not s0) = s0 ==> s1 + #-} diff --git a/Language/Copilot/Libs/ErrorChks.hs b/Language/Copilot/Libs/ErrorChks.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Libs/ErrorChks.hs @@ -0,0 +1,30 @@ +-- | Basic error checking for other libraries. + +module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where + +import Prelude (Num, Integral, Int, String, error, ($), show, maxBound, toInteger) +import qualified Prelude as P +import Data.Int (Int16) + +import Language.Copilot.Core + +chk :: String -> Int -> Spec a -> Int -> Spec a +chk name n s m = + if n P.< m + then error $ "Value " P.++ show n P.++ " in operator " P.++ name + P.++ " must be greater than or equal to " P.++ show m P.++ "." + else s + +nPosChk :: String -> Int -> Spec a -> Spec a +nPosChk name n s = chk name n s 0 + +nOneChk :: String -> Int -> Spec a -> Spec a +nOneChk name n s = chk name n s 1 + +int16Chk :: String -> Int -> Spec a -> Spec a +int16Chk name n s = + if (toInteger n) P.> max + then error $ "Offset " P.++ show n P.++ " in operator " P.++ name + P.++ " is larger than the Int16 maxBound, " P.++ show max P.++ "." + else s + where max = toInteger (maxBound::Int16) diff --git a/Language/Copilot/Libs/Indexes.hs b/Language/Copilot/Libs/Indexes.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Libs/Indexes.hs @@ -0,0 +1,52 @@ +-- | Queries into how long until properties hold or fail. We use Int16 to +-- return the value, so your queries must not require looking more than 32,767 +-- periods :) . Thus, in the following, the parameter @n@ must be @0 <= n <= +-- 32,767@. -1 indicates the test failed. + +module Language.Copilot.Libs.Indexes(soonest, soonestFail, latest, latestFail) where + +import Prelude (Integral, Bool(..), id, Int, String, error, fromIntegral, ($), show) +import qualified Prelude as P +import Data.Int (Int16) + +import Language.Copilot.Libs.ErrorChks +import Language.Copilot.Core +import Language.Copilot.Language + +soonestHlp :: String -> (Spec Bool -> Spec Bool) -> Int -> Spec Bool -> Spec Int16 +soonestHlp name f n s = int16Chk name n $ nPosChk name n (buildStr 0) + where buildStr m = + if m P.> n then const (-1) + else mux (f $ drop m s) (const $ fI m) (buildStr (m P.+ 1)) + fI = fromIntegral + +latestHlp :: String -> (Spec Bool -> Spec Bool) -> Int -> Spec Bool -> Spec Int16 +latestHlp name f n s = int16Chk name n $ nPosChk name n (buildStr n) + where buildStr m = + if m P.< 0 then const (-1) + else mux (f $ drop m s) (const $ fI m) (buildStr (m P.- 1)) + fI = fromIntegral + +-- | Returns the smallest @m <= n@ such that @drop m s@ is true, and @-1@ if no +-- such @m@ exists. +soonest :: Int -> Spec Bool -> Spec Int16 +soonest = soonestHlp "soonest" id + +-- | Returns the smallest @m <= n@ such that @drop m s@ is false, and @-1@ if no +-- such @m@ exists. +soonestFail :: Int -> Spec Bool -> Spec Int16 +soonestFail = soonestHlp "soonestFail" not + +-- | Returns the largest @m <= n@ such that @drop m s@ is true, and @-1@ if no +-- such @m@ exists. +latest :: Int -> Spec Bool -> Spec Int16 +latest = latestHlp "latest" id + +-- | Returns the largest @m <= n@ such that @drop m s@ is false, and @-1@ if no +-- such @m@ exists. +latestFail :: Int -> Spec Bool -> Spec Int16 +latestFail = latestHlp "latest" not + + + + diff --git a/Language/Copilot/Libs/LTL.hs b/Language/Copilot/Libs/LTL.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Libs/LTL.hs @@ -0,0 +1,57 @@ +-- | Bounded Linear Temporal Logic (LTL) operators. + +module Language.Copilot.Libs.LTL(always, next, eventually, until, release) where + +import Prelude (Int, ($)) +import qualified Prelude as P +import Data.List(foldl1) + +import Language.Copilot.Core +import Language.Copilot.Language +import Language.Copilot.Libs.Indexes +import Language.Copilot.Libs.ErrorChks + +-- | Property @s@ holds for the next @n@ periods. If @n == 0@, then @s@ holds +-- in the current period. We require @n >= 0@. +-- E.g., if @p = always 2 s@, then we have the following relationship between the streams generated: +-- @ +-- s => T T T T F F F F ... +-- p => T T F F F F F F ... +-- @ +always :: Int -> Spec Bool -> Spec Bool +always n s = nPosChk "always" n $ foldl1 (&&) [drop x s | x <- [0..n]] + +-- | Property @s@ holds at the next period. +next :: Spec Bool -> Spec Bool +next s = drop 1 s + +-- | Property @s@ holds at some period in the next @n@ periods. If @n == 0@, +-- then @s@ holds in the current period. We require @n >= 0@. +-- E.g., if @p = eventually 2 s@, then we have the following relationship between the streams generated: +-- @ +-- s => F F F F T F T F ... +-- p => F F T T T T T T ... +-- @ +eventually :: Int -> Spec Bool -> Spec Bool +eventually n s = nPosChk "eventually" n $ foldl1 (||) [drop x s | x <- [0..n]] + +-- | @until n s0 s1@ means that @eventually n s1@, and up until at least the +-- period before @s1@ holds, @s0@ continuously holds. +until :: Int -> Spec Bool -> Spec Bool -> Spec Bool +until n s0 s1 = + nPosChk "until" n $ ( (whenS0 < const 0) -- s0 didn't fail within n periods. + || (soonest n s1 <= whenS0)) -- s0 failed at some point before n. + && eventually n s1 -- guarantees that soonest n s1 >= 0 + where whenS0 = soonestFail n s0 + +-- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and +-- including the period at which @s0@ becomes true. +release :: Int -> Spec Bool -> Spec Bool -> Spec Bool +release n s0 s1 = + nPosChk "release" n $ (whenS1 < const 0) -- s1 never fails + || ( (whenS0 >= const 0) -- s0 becomes true at some point + && (whenS0 < whenS1)) -- and when s0 becomes true, + -- is strictly sooner than + -- whne s1 fails. + where whenS1 = soonestFail n s1 + whenS0 = soonest n s0 diff --git a/Language/Copilot/Libs/PTLTL.hs b/Language/Copilot/Libs/PTLTL.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Libs/PTLTL.hs @@ -0,0 +1,39 @@ +-- | 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. + +module Language.Copilot.Libs.PTLTL(previous, alwaysBeen, eventuallyPrev, since) where + +import Prelude () +import qualified Prelude as P + +import Language.Copilot.Core +import Language.Copilot.Language + +-- | Did @s@ hold in the previous period? +previous :: Var -> Spec Bool -> Streams +previous v s = do + v .= [False] ++ s + +-- | Has @s@ always held? +alwaysBeen :: Var -> Spec Bool -> Streams +alwaysBeen v s = do + tmp .= [True] ++ (var tmp) && s + v .= s && varB tmp + where tmp = "alwaysBeenTmp_" P.++ v + +-- | Did @s@ hold at some time in the past (including the current state)? +eventuallyPrev :: Var -> Spec Bool -> Streams +eventuallyPrev v s = do + tmp .= [False] ++ (var tmp) || s + v .= s || varB tmp + where tmp = "eventuallyPrevTmp_" P.++ v + +-- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold? +since :: Var -> (Spec Bool, Spec Bool) -> Streams +since v (s1, s2) = do + tmp .= [False] ++ (s2 || (s1 && varB v)) + v .= varB tmp && s1 + where tmp = "sinceTmp_" P.++ v + diff --git a/Language/Copilot/Libs/Statistics.hs b/Language/Copilot/Libs/Statistics.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Libs/Statistics.hs @@ -0,0 +1,43 @@ +-- | Basic bounded statistics. In the following, a bound @n@ is given stating +-- the number of periods over which to compute the statistic (@n == 1@ computes +-- it only over the current period). + +module Language.Copilot.Libs.Statistics(max, min, sum, mean) where + +import Prelude (Int, ($), foldl1, fromIntegral) +import qualified Prelude as P + +import qualified Language.Atom as A + +import Language.Copilot.Libs.ErrorChks (nOneChk) +import Language.Copilot.Core +import Language.Copilot.Language + +foldDrops :: (Streamable a) => Int -> (Spec a -> Spec a -> Spec a) -> Spec a -> Spec a +foldDrops n f s = foldl1 f [drop x s | x <- [0..(n-1)]] + +-- | Summation. +sum :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a +sum n s = + nOneChk "sum" n $ foldDrops n (+) s + +-- | Maximum value. +max :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a +max n s = + nOneChk "max" n $ foldDrops n largest s + where largest = \ x y -> mux (x <= y) y x + +-- | Minimum value. +min :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a +min n s = + nOneChk "max" n $ foldDrops n smallest s + where smallest = \ x y -> mux (x <= y) x y + +-- | Mean value. @n@ must not overflow +-- for word size @a@ for streams over which computation is peformed. +mean :: (Streamable a, Fractional a, A.NumE a) => Int -> Spec a -> Spec a +mean n s = + nOneChk "mean" n $ (sum n s) / (const $ fromIntegral n) + +-- majority :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a +-- majority n s = diff --git a/Language/Copilot/PrettyPrinter.hs b/Language/Copilot/PrettyPrinter.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/PrettyPrinter.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances, TypeSynonymInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | Only exports instances for Show which allows the printing of streams +module Language.Copilot.PrettyPrinter () where + +import Data.Int +import Data.Word +import Data.Map as M +import Control.Monad.Writer (execWriter) + +import Language.Copilot.Core + +instance (Show (a Bool), Show (a Int8), Show (a Int16), Show (a Int32), Show (a Int64), + Show (a Word8), Show (a Word16), Show (a Word32), Show (a Word64), + Show (a Float), Show (a Double)) => Show (StreamableMaps a) where + show (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) = + let acc0 = M.foldWithKey showVal "" bm + acc1 = M.foldWithKey showVal acc0 i8m + acc2 = M.foldWithKey showVal acc1 i16m + acc3 = M.foldWithKey showVal acc2 i32m + acc4 = M.foldWithKey showVal acc3 i64m + acc5 = M.foldWithKey showVal acc4 w8m + acc6 = M.foldWithKey showVal acc5 w16m + acc7 = M.foldWithKey showVal acc6 w32m + acc8 = M.foldWithKey showVal acc7 w64m + acc9 = M.foldWithKey showVal acc8 fm + acc10 = M.foldWithKey showVal acc9 dm + in acc10 + where + showVal :: (Streamable a, Show (b a)) => Var -> b a -> String -> String + showVal v val string = v ++ " .= " ++ show val ++ "\n" ++ string + +instance Show Streams where + show s = show (execWriter s) + +-- instance Show (StreamableMaps Spec) where +-- show (SM bm i8m i16m i32m i64m w8m w16m w32m w64m fm dm) = +-- show bm diff --git a/Language/Copilot/Tests/Random.hs b/Language/Copilot/Tests/Random.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Tests/Random.hs @@ -0,0 +1,303 @@ +{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, GADTs, RankNTypes #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Language.Copilot.Tests.Random (randomStreams, Operator(..), Operators, fromOp) where + +import Language.Copilot.Core +import Language.Copilot.Analyser + +import qualified Language.Atom as A + +import qualified Data.Map as M +import Prelude +import System.Random +import Data.Int +import Data.Word +import Data.Maybe + +---- Parameters of the random generation --------------------------------------- + +maxDrop, maxSamplePhase :: Int +maxDrop = 4 -- The maximum value for i in Drop i _ +maxSamplePhase = 8 -- The maximum value for ph in PVar _ _ ph + +-- These determines the number of streams and of monitored variables. +-- Bools are drawn each time with the following weights, until a False is drawn +weightsContinueVar, weightsContinuePVar :: [(Bool, Int)] +weightsContinueVar = [(True, 3), (False, 1)] +weightsContinuePVar = [(True, 1), (False, 1)] + +-- These determines the frequency of each atom type for the streams and the monitored variables +weightsVarTypes, weightsPVarTypes :: [(A.Type, Int)] +weightsVarTypes = + [(A.Bool, 5), (A.Word64, 3), (A.Int64, 3), (A.Float, 0), (A.Double, 4), + (A.Int8, 1), (A.Int16, 1), (A.Int32, 1), (A.Word8, 1), (A.Word16, 1), (A.Word32, 1)] +weightsPVarTypes = + [(A.Bool, 5), (A.Word64, 3), (A.Int64, 3), (A.Float, 0), (A.Double, 4), + (A.Int8, 1), (A.Int16, 1), (A.Int32, 1), (A.Word8, 1), (A.Word16, 1), (A.Word32, 1)] + +-- These determines the frequency of each constructor in the random streams +-- 0 -> PVar +-- 1 -> Var +-- 2 -> Const +-- 3 -> F +-- 4 -> F2 +-- 5 -> F3 +-- 6 -> Append +-- 7 -> Drop +weightsAllSpecSet, weightsFunSpecSet, weightsDropSpecSet :: [(Int, Int)] +weightsAllSpecSet = [(0, 2),(1,2),(2,6),(3,1),(4,3),(5,1),(6,4),(7,1)] +weightsFunSpecSet = [(0, 2),(1,2),(2,6),(3,1),(4,3),(5,1),(7,1)] +weightsDropSpecSet = [(1,2),(2,6),(7,1)] + +---- 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)) +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)) +fromOp op = + case op of + Operator x -> x + +foldRandomableMaps :: forall b c. + (forall a. (Streamable a, Random a) => Var -> c a -> b -> b) -> + StreamableMaps c -> b -> b +foldRandomableMaps 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 + in acc10 + +randomWeighted :: (RandomGen g, Random a) => g -> [(a, Int)] -> (a, g) +randomWeighted g l = + let l' = concatMap (\ (x, n) -> replicate n x) l + len = length l' + (i, g') = randomR (0, len - 1) g in + (l' !! i, g') + +data VName a = VName a +type Variables = StreamableMaps VName + +---- Instances of Random ------------------------------------------------------- + +instance Random Int8 where + random g = + let ((i::Int), g') = random g in + (fromInteger $ toInteger i, g') + randomR (lo, hi) g = + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + +instance Random Int16 where + random g = + let ((i::Int), g') = random g in + (fromInteger $ toInteger i, g') + randomR (lo, hi) g = + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + +instance Random Int32 where + random g = + let ((i::Int), g') = random g in + (fromInteger $ toInteger i, g') + randomR (lo, hi) g = + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + +instance Random Int64 where + random g = + let ((i0::Int32), g0) = random g + ((i1::Int32), g1) = random g0 in + (fromInteger (toInteger i0) + fromInteger (toInteger i1) * 2 ^ (32::Int), g1) + randomR (lo, hi) g = -- TODO : generate on the whole range, and not only on a part of it + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + +instance Random Word8 where + random g = + let ((i::Int), g') = random g in + (fromInteger $ toInteger i, g') + randomR (lo, hi) g = + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + +instance Random Word16 where + random g = + let ((i::Int), g') = random g in + (fromInteger $ toInteger i, g') + randomR (lo, hi) g = + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + + +instance Random Word32 where + random g = + let ((i0::Word16), g0) = random g + ((i1::Word16), g1) = random g0 in + (fromInteger (toInteger i0) + fromInteger (toInteger i1) * 2 ^ (16::Int), g1) + randomR (lo, hi) g = -- TODO : generate on the whole range, and not only on a part of it + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + + +instance Random Word64 where + random g = + let ((i0::Word32), g0) = random g + ((i1::Word32), g1) = random g0 in + (fromInteger (toInteger i0) + fromInteger (toInteger i1) * 2 ^ (32::Int), g1) + randomR (lo, hi) g = -- TODO : generate on the whole range, and not only on a part of it + let ((i::Int), g') = randomR (fromInteger $ toInteger lo, fromInteger $ toInteger hi) g in + (fromInteger $ toInteger i, g') + +instance Random a => Random [a] where + random g = + let (x, g0) = random g + (b, g1) = random g0 + (l, g2) = + if b + then random g1 + else ([], g1) in + (x:l, g2) + -- Totally useless as lists are not ordered (could be, however) + randomR (_, _) g = random g + +instance Random A.Type where + random g = + let (n, g') = randomR (0::Int, 10) g in + (toEnum n, g') + randomR (t, t') g = + let (n, g') = randomR (fromEnum t, fromEnum t') g in + (toEnum n, g') + +---- Generation of random streams ---------------------------------------------- + +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 + (streams, g2) = foldRandomableMaps (addRandomSpec opsF opsF2 opsF3 vs exts) vs (emptySM, g1) + (vars, g3) = foldRandomableMaps addRandomExternal exts (emptySM, g2) in + if isNothing $ check streams + then (streams, vars) + else randomStreams opsF opsF2 opsF3 g3 + +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 + (v_int::Word64, g2) = random g1 + v = "v" ++ show v_int + vs' = + case t of + A.Bool -> updateSubMap (\ m -> M.insert v (VName (unit::Bool)) m) vs + A.Int8 -> updateSubMap (\ m -> M.insert v (VName (unit::Int8)) m) vs + A.Int16 -> updateSubMap (\ m -> M.insert v (VName (unit::Int16)) m) vs + A.Int32 -> updateSubMap (\ m -> M.insert v (VName (unit::Int32)) m) vs + A.Int64 -> updateSubMap (\ m -> M.insert v (VName (unit::Int64)) m) vs + A.Word8 -> updateSubMap (\ m -> M.insert v (VName (unit::Word8)) m) vs + A.Word16 -> updateSubMap (\ m -> M.insert v (VName (unit::Word16)) m) vs + A.Word32 -> updateSubMap (\ m -> M.insert v (VName (unit::Word32)) m) vs + A.Word64 -> updateSubMap (\ m -> M.insert v (VName (unit::Word64)) m) vs + A.Float -> updateSubMap (\ m -> M.insert v (VName (unit::Float)) m) vs + A.Double -> updateSubMap (\ m -> M.insert v (VName (unit::Double)) m) vs + in + if b + then addRandomVNames wContinue wTypes g2 vs' + else (vs', g2) + +addRandomSpec :: forall a g. (Streamable a, Random a, RandomGen g) => + Operators -> Operators -> Operators -> Variables -> Variables -> + Var -> VName a -> (StreamableMaps Spec, g) -> (StreamableMaps Spec, g) +addRandomSpec opsF opsF2 opsF3 vs exts v _ (streams, g) = + let (spec::(Spec a), g') = randomSpec vs exts opsF opsF2 opsF3 g AllSpecSet in + (updateSubMap (\m -> M.insert v spec m) streams, g') + +randomSpec :: forall a g. (Streamable a, RandomGen g, Random a) => + 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 + DropSpecSet -> weightsDropSpecSet + (n::Int, g0) = randomWeighted g weights in + case n of + 0 -> -- PVar + case getVar g0 exts of + (Just v, g1) -> + let (ph, g2) = randomR (1, maxSamplePhase) g1 in + (PVar (atomType (unit::a)) v ph, g2) + (Nothing, g1) -> randomSpec' g1 set + 1 -> -- Var + case getVar g0 vs of + (Just v, g1) -> (Var v, g1) + (Nothing, g1) -> randomSpec' g1 set + 2 -> -- Const + let (e, g1) = random g0 in + (Const e, g1) + 3 -> -- F + getOpStream opsF g0 + 4 -> -- F2 + getOpStream opsF g0 + 5 -> -- F3 + getOpStream opsF g0 + 6 -> -- Append + let (ls, g1) = random g0 + (s', g2) = randomSpec' g1 set in + (Append ls s', g2) + 7 -> -- Drop + let (i, g1) = randomR (1::Int, maxDrop) g0 + (s', g2) = randomSpec' g1 DropSpecSet in + (Drop i s', g2) + _ -> error "Impossible" + where + 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 = + let m = getSubMap ops + ks = M.keys m + len = length ks + in + if len > 0 + then + let (i, g1) = randomR (0::Int, len - 1) g0 + k = ks !! i in + case fromJust $ M.lookup k m of + Operator op -> op randomSpec' g1 + else randomSpec' g0 set + getVar :: g -> Variables -> (Maybe Var, g) + getVar g0 variables = + let m :: M.Map Var (VName a) + m = getSubMap variables + ks = M.keys m + len = length ks + in + if len > 0 + then + let (i, g1) = randomR (0::Int, len - 1) g0 in + (Just (ks !! i), g1) + else (Nothing, g0) + +addRandomExternal :: forall a g. (Streamable a, Random a, RandomGen g) => + Var -> VName a -> (Vars, g) -> (Vars, g) +addRandomExternal v _ (vars, g) = + let (vals::[a], g') = randomExternalValues g in + (updateSubMap (\m -> M.insert v vals m) vars, g') + +randomExternalValues :: (Streamable a, Random a, RandomGen g) => g -> ([a], g) +randomExternalValues g = + let (oldG, newG) = split g in + (randoms oldG, newG) diff --git a/Language/Copilot/Variables.hs b/Language/Copilot/Variables.hs new file mode 100644 --- /dev/null +++ b/Language/Copilot/Variables.hs @@ -0,0 +1,32 @@ +-- | Variable names + +module Language.Copilot.Variables where + +a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p,q,r,s,t,u,v,w,x,y,z :: String + +a = "a" +b = "b" +c = "c" +d = "d" +e = "e" +f = "f" +g = "g" +h = "h" +i = "i" +j = "j" +k = "k" +l = "l" +m = "m" +n = "n" +o = "o" +p = "p" +q = "q" +r = "r" +s = "s" +t = "t" +u = "u" +v = "v" +w = "w" +x = "x" +y = "y" +z = "z" diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,33 @@ +Copilot: A (Haskell DSL) stream language for generating hard real-time C code. + +Can you write a list in Haskell? Then you can write embedded C code using +Copilot. Here's a Copilot program that computes the Fibonacci sequence (over +Word 64s) and tests for even numbers: + + +fib :: Streams +fib = do + "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib") + "t" .= even (var "fib") + where even :: Spec Word64 -> Spec Bool + even w = w `mod` const 2 == const 0 + +Copilot contains an interpreter, a compiler, and uses a model-checker to check +the correctness of your program. The compiler generates constant time and +constant space C code via Tom Hawkin's Atom (thanks Tom!). Copilot was +originally developed to write embedded monitors for more complex embedded +systems, but it can be used to develop a variety of functional-style embedded +code. + + +******** +Please visit for more information about +installing and using Copilot. + +Also available as index.html in the gh-pages branch of the Copilot repo. In +your local repo, + + > git checkout gh-pages + +and you should see index.html. +******** diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot.cabal b/copilot.cabal new file mode 100644 --- /dev/null +++ b/copilot.cabal @@ -0,0 +1,66 @@ +name: copilot +version: 0.21 +cabal-version: >= 1.2 +license: BSD3 +license-file: LICENSE +author: Lee Pike , Robin Morisset, Alwyn Goodloe, Sebastian Niller +synopsis: A lazy-list language for generating constant-time and constant-space C programs. Uses Atom as a backend. +build-type: Simple +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 + Copilot. Here's a Copilot program that computes the Fibonacci sequence (over + Word 64s) and tests for even numbers: + . + > fib :: Streams + > fib = do + > "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib") + > "t" .= even (var "fib") + > where even :: Spec Word64 -> Spec Bool + > even w = w `mod` const 2 == const 0 + . + Copilot contains an interpreter, a compiler, and uses a model-checker to check + the correctness of your program. The compiler generates constant time and + constant space C code via Tom Hawkin's Atom (thanks Tom!). Copilot was + originally developed to write embedded monitors for more complex embedded + systems, but it can be used to develop a variety of functional-style embedded + code. + +extra-source-files: README + +library + ghc-options: -Wall + build-depends: base > 4 && < 5 + , atom >= 1.0.5 + , containers >= 0.2.0.1 + , process >= 1.0.0.0 + , random >= 1.0.0.0 + , directory + , mtl >= 1.0.0.0 + , filepath >= 1.0.0.0 + + extensions: + exposed-modules: Language.Copilot + Language.Copilot.AdHocC + Language.Copilot.Core + Language.Copilot.Language + Language.Copilot.AtomToC + Language.Copilot.Compiler + Language.Copilot.Interpreter + Language.Copilot.Help + Language.Copilot.Analyser + Language.Copilot.PrettyPrinter + Language.Copilot.Tests.Random + Language.Copilot.Dispatch + Language.Copilot.Interface + Language.Copilot.Variables + Language.Copilot.Libs.ErrorChks + Language.Copilot.Libs.PTLTL + Language.Copilot.Libs.LTL + Language.Copilot.Libs.Indexes + Language.Copilot.Libs.Statistics + Language.Copilot.Examples.Examples + Language.Copilot.Examples.LTLExamples + Language.Copilot.Examples.PTLTLExamples + Language.Copilot.Examples.StatExamples