diff --git a/Language/Copilot.hs b/Language/Copilot.hs deleted file mode 100644 --- a/Language/Copilot.hs +++ /dev/null @@ -1,44 +0,0 @@ -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.Sampling - -- , module Language.Copilot.Casting - -- , 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.Libs.Clocks - -- , module Language.Copilot.AdHocC - -- , module Language.Copilot.Examples.Examples - -- , module Language.Copilot.Examples.LTLExamples - -- , module Language.Copilot.Examples.PTLTLExamples - ) where - -import Language.Copilot.Core (Streams, Spec, emptySM, StreamableMaps(..)) -- XXX for libs, probably need to export all the maps. Maybe put in a different file? -import Language.Copilot.Analyser -import Language.Copilot.Interpreter -import Language.Copilot.Help -import Language.Copilot.AtomToC -import Language.Copilot.Compiler -import Language.Copilot.Tests.Random -import Language.Copilot.Language --- import Language.Copilot.Language.Sampling --- import Language.Copilot.Language.Casting --- import Language.Copilot.PrettyPrinter() --- 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.Libs.Clocks --- import Language.Copilot.AdHocC --- import Language.Copilot.Examples.Examples --- import Language.Copilot.Examples.LTLExamples --- import Language.Copilot.Examples.PTLTLExamples diff --git a/Language/Copilot/AdHocC.hs b/Language/Copilot/AdHocC.hs deleted file mode 100644 --- a/Language/Copilot/AdHocC.hs +++ /dev/null @@ -1,73 +0,0 @@ --- generate C-Code with combinators, high-level, safe haskell. - --- | Helper functions for writing free-form C code. -module Language.Copilot.AdHocC ( - varDecl, arrDecl, varInit, arrayInit, funcDecl - , 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) ++ ";" - --- | Takes a type and a list of array names and their sizes declares them. -arrDecl :: Type -> [(String, Int)] -> String -arrDecl t arrs = - cType t ++ " " ++ unwords (intersperse "," mkArrs) ++ ";" - where mkArrs = map (\(a,size) -> a ++ "[" ++ show size ++ "]") arrs - --- | Takes a type and a variable and initializes it. It is YOUR responsibility --- to ensure that @val@ is of type @t@. -varInit :: Show a => Type -> String -> a -> String -varInit t var val = cType t ++ " " ++ var ++ " = " ++ show val ++ ";" - --- | Takes a type and an array and initializes it. It is YOUR responsibility to --- ensure that @vals@ is of type @t@. -arrayInit :: Show a => Type -> String -> [a] -> String -arrayInit t var vals = - cType t ++ " " ++ var ++ "[" ++ show (length vals) - ++ "] = " ++ bracesListShow ++ ";" - where - -- Show a list with braces {} rather than brackets []. - bracesListShow :: String - bracesListShow = - "{" ++ (foldl (++) "" $ intersperse "," $ map show vals) ++ "}" - --- | Declare function prototypes, given a return type, a function name, and a --- | list of argument types. Use 'Nothing' for a return type of @void@. -funcDecl :: Maybe Type -> String -> [Type] -> String -funcDecl t fn argTs = makeRet t ++ " " ++ fn ++ "(" ++ makeArgTs ++ ");" - where makeRet Nothing = "void" - makeRet (Just t') = cType t' - makeArgTs | null argTs = "void" - | otherwise = unwords (intersperse "," $ map cType argTs) - --- | Add an include of a library -includeBracket :: String -> String -includeBracket lib = "#include <" ++ lib ++ ">" - --- | 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 deleted file mode 100644 --- a/Language/Copilot/Analyser.hs +++ /dev/null @@ -1,403 +0,0 @@ -{-# LANGUAGE RelaxedPolyRec #-} - --- | 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 - {- - -- * Dependency Graphs (experimental) - Weight, Node(..), DependencyGraph, - mkDepGraph, showDG -} - ) where - -import Language.Copilot.Core - -import Data.List -import Data.Maybe(mapMaybe) - -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 - | BadPArrSpec Var Ext String -- ^ External array indexes can only take - -- variables or constants as indexes. - | BadType Var String -- ^ either a variable is not defined, or not with the - -- good type ; there is no implicit conversion of types - -- in /Copilot/. - | BadTypeExt Ext Var -- ^ either an external 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] Ext Weight Weight -- ^ Could be compiled, but - -- would need bigger - -- prophecyArrays - | DependsOnFuture [Var] Ext Weight -- ^ If an output depends of a future of - -- an input it will be hard to compile to - -- say the least - | NoInit Var -- ^ If we are sampling a function and it has an - -- argument that is a Copilot stream, the weight of - -- that stream must have at least one initial element. - -instance Show Error where - show (BadSyntax s v) = - unlines - ["Error syntax : " ++ s ++ " is not allowed in that position in stream " - ++ v ++ "."] - show (BadDrop i v) = - unlines - [ "Error : a Drop in stream " ++ v ++ " drops the number " ++ show i ++ - "of elements.\n" - , show i ++ " is negative, and Drop only accepts positive arguments.\n" - ] - show (BadPArrSpec v arr idx) = - unlines - [ "Error : the index into an external array can only take a " - ++ "variable or a constant. The index\n" - , idx ++ "\n\n in external array " - ++ show arr ++ "in the definition of stream " ++ v ++ " is not of that " - ++ "form.\n" - ] - show (BadType v v') = - unlines - [ "Error : the monitor variable " ++ v ++ ", called from " - ++ v' ++ ", either" - , "does not exist, or don't have the right type (there is no implicit " - ++ "conversion).\n" - ] - show (BadTypeExt v v') = - unlines - [ "Error : the external call " ++ show 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) = - unlines - [ "Error : the following path is closed in the dependency graph of the " - ++ "specification and has" - , "weight " ++ show w ++ " which is positive (append decreases the weight, " - ++ "while drop increases it)." - , "This is forbidden to avoid streams which could take 0 or several different" - ++ " values." - , "Try adding some initial elements (e.g., [0,0,0] ++ ...) " - ++ "to the offending streams." - , "Path : " ++ show (reverse vs) ++ "\n" - ] - show (DependsOnClosePast vs v w len) = - unlines - [ "Error : the following path is of weight " ++ show w ++ " ending in " - ++ "the external variable " ++ show v - , "while the first variable of that path has a prophecy array of length " - ++ show len ++ "," - , "which is strictly greater than the weight. This is forbidden." - , "Path : " ++ show (reverse vs) ++ "\n" - ] - show (DependsOnFuture vs v w) = - unlines - [ "Error : the following path is of weight " ++ show w - ++ " which is strictly positive." - , "This means that the first variable depends on the future of the " - ++ "external variable " ++ show v - , "which is quoted in the last variable of the path. This is " - ++ "obviously impossible." - , "Path : " ++ show (reverse vs) ++ "\n" - ] - show (NoInit v) = - "Error : the Copilot variable " ++ v ++ " appears either as an argument in an " - ++ "external function that is sampled or an index in an external array being sampled. " - ++ "In either case, the stream must have an initial value (that is not drawn from an " - ++ "external variable)." - -(&&>) :: 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 &&> checkInitsArgs 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 - Var _ -> Nothing - Const _ -> Nothing - PVar _ _ -> Nothing -- checkSampling s0 - PArr _ (arr,s0) -> checkIndex v arr s0 --- case chkInitElem streams (getElem v streams `asTypeOf` s0) of --- Left () -> Just $ NoInit (show arr) v --- Right () -> Nothing --- _ -> Just $ BadArrIdx (show arr) (show s0) --- ) &&> checkSampling arr --- &&> checkSyntaxSpec PArrSet v s0 Nothing - -- PVar _ _ -> Nothing - -- PArr _ (arr,s0) -> - F _ _ s0 -> set /= DropSpecSet ||> BadSyntax "F" v - &&> checkSyntaxSpec FunSpecSet v s0 Nothing - F2 _ _ s0 s1 -> set /= DropSpecSet ||> BadSyntax "F2" v - &&> checkSyntaxSpec FunSpecSet v s0 Nothing - &&> checkSyntaxSpec FunSpecSet v s1 Nothing - F3 _ _ s0 s1 s2 -> set /= DropSpecSet ||> BadSyntax "F3" v - &&> checkSyntaxSpec FunSpecSet v s0 Nothing - &&> checkSyntaxSpec FunSpecSet v s1 Nothing - &&> checkSyntaxSpec FunSpecSet v s2 Nothing - Append _ s0 -> set == AllSpecSet ||> BadSyntax "Append" v - &&> checkSyntaxSpec AllSpecSet v s0 Nothing - Drop i s0 -> (0 <= i) ||> BadDrop i v - &&> checkSyntaxSpec DropSpecSet v s0 Nothing - checkIndex _ _ (Var _) = Nothing - checkIndex _ _ (Const _) = Nothing - checkIndex v arr idx = Just $ BadPArrSpec v arr (show idx) - -- checkSampling s = - -- case s of - -- ExtV _ -> Nothing - -- fun@(Fun f args) -> - -- foldl (\n arg -> case arg of - -- C _ -> n &&> Nothing - -- -- already check elems defined in defCheck - -- V v -> n &&> (case chkInitElem streams (getElem v streams) of - -- Left () -> Just $ NoInit (show fun) v - -- Right () -> Nothing - -- ) - -- ) Nothing args - - --- | Checks that streams are well defined (i.e., can be compiled). -defCheck :: StreamableMaps Spec -> Maybe Error -defCheck streams = - let checkPathsFromSpec :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error - 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 $ BadTypeExt v (head vs) - _ -> Nothing - PArr t (arr, idx) - | n > 0 -> Just $ DependsOnFuture vs arr n - | n > negate (prophecyArrayLength idx) -> - Just $ DependsOnClosePast vs arr n - (prophecyArrayLength idx) - | t /= getAtomType s -> - Just $ BadTypeExt arr (head vs) - | otherwise -> - case idx of - Const _ -> checkPath n vs idx - Var _ -> checkPath n vs idx - _ -> - Just $ BadPArrSpec v0 arr (show idx) - Var v -> - if elem v vs - then if n >= 0 - 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 - -getExternalVars :: StreamableMaps Spec -> [Exs] -getExternalVars streams = - nub $ foldStreamableMaps decl streams [] - where - decl :: Streamable a => Var -> Spec a -> [Exs] -> [Exs] - decl _ s ls = - case s of - PVar t v -> (t, v, ExtRetV) : ls - PArr t (arr, s0) -> (t, arr - , ExtRetA (case s0 of - Var v -> V v - Const c -> C (show c) - _ -> error "Error in getExternalVars.") - ) : 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 - --- | Is there an initial element (for sampling functions)? -checkInitsArgs :: StreamableMaps Spec -> Maybe Error -checkInitsArgs streams = - let checkInits :: Streamable a => Var -> Spec a -> Maybe Error -> Maybe Error - checkInits v s err = - err &&> if checkPath 0 [v] s >= 0 then Just (NoInit v) - else Nothing - where checkPath :: Streamable a => Int -> [Var] -> Spec a -> Int - checkPath n vs s0 = - if (v `elem` samplingFuncs) || (v `elem` arrIndices) - then case s0 of - Var v0 -> if elem v0 vs then n - else checkPath n (v0:vs) - (getElem v0 streams `asTypeOf` s0) - Append ls s1 -> checkPath (n - length ls) vs s1 - Drop m s1 -> checkPath (m + n) vs s1 - _ -> n - -- Const _ -> n - -- PVar _ _ -> n - -- PArr _ _ -> n - -- F _ _ _ -> n - -- F2 _ _ _ _ -> n - -- F3 _ _ _ _ _ -> n - else (-1) - samplingFuncs = - concatMap (\x -> case x of - (_, Fun _ args, _) -> - mapMaybe (\arg -> - case arg of - C _ -> Nothing - V v0 -> Just v0 - ) args - (_, ExtV _, _) -> []) - (getExternalVars streams) - arrIndices = mapMaybe (\x -> case x of - (_,_,ExtRetV) -> Nothing - (_,_,ExtRetA idx) -> - case idx of - V v' -> Just v' - C _ -> Nothing) - (getExternalVars streams) - in foldStreamableMaps checkInits streams Nothing - --- chkInitElem :: Streamable a => StreamableMaps Spec -> Spec a -> Either () () --- chkInitElem streams spec = --- initElem spec 0 [] --- where --- -- getSpec :: Streamable a => Var -> Spec a --- -- getSpec v = let s = getMaybeElem v streams in --- -- case s of --- -- Nothing -> error $ "Error: No Copilot stream " --- -- ++ v ++ " exists." --- -- Just s0 -> s0 `asTypeOf` s --- initElem :: Streamable a => Spec a -> Int -> [Var] -> Either () () --- initElem s cnt vs = --- case s of --- Var v -> if elem v vs then initChk --- else initElem (getElem v streams) cnt (v:vs) --- Const _ -> initChk --- PVar t v -> initChk --- PArr t (arr, s0) -> initChk --- F _ _ _ -> initChk --- F2 _ _ _ _ -> initChk --- F3 _ _ _ _ _ -> initChk --- Append ls s0 -> initElem s0 (cnt - length ls) vs --- Drop n s0 -> initElem s0 (cnt + n) vs --- where initChk = if cnt < 0 then Right () else Left () - ----- 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 deleted file mode 100644 --- a/Language/Copilot/AtomToC.hs +++ /dev/null @@ -1,140 +0,0 @@ -{-# 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 Data.Maybe (fromMaybe) -import Data.List - --- allExts represents all the variabbles to monitor (used for declaring them) --- inputExts represents the monitored variables which are to be fed to the --- standard input of the C program. only used for the testing with random --- streams and values. -getPrePostCode :: Bool -> (Maybe String, Maybe String) -> Name - -> StreamableMaps Spec -> [Exs] -> [(Ext,Int)] -> Vars - -> Period -> (String, String) -getPrePostCode simulatation (pre, post) cName streams allExts - arrDecs inputExts p = - ( (if simulatation then preCode (extDecls allExts arrDecs) - else "") ++ fromMaybe "" pre - , fromMaybe "" post ++ periodLoop cName p - ++ if simulatation then (postCode cName streams inputExts) - else "" - ) - --- Make the declarations for external vars -extDecls :: [Exs] -> [(Ext,Int)] -> [String] -extDecls allExtVars arrDecs = - let uniqueExtVars = nubBy (\ (x, y, _) (x', y', _) -> x == x' && y == y') - allExtVars - getDec :: Exs -> String - getDec (t, (ExtV v), ExtRetV) = varDecl t [v] - getDec (_, (Fun _ _), ExtRetV) = "" - getDec (t, arr, ExtRetA _) = - case getIdx arr of - Nothing -> error $ "Please use the setArrs option to provide a list of " ++ - "pairs (a,idx) where a is the name of an external array and idx " ++ - "is its static size to declare. There is no size for array " ++ - show arr ++ "." - Just idx -> arrDecl t [(show arr, idx)] - getIdx arr = lookup arr arrDecs - in - map getDec uniqueExtVars - -preCode :: [String] -> String -preCode extDeclarations = unlines $ - [ includeBracket "stdio.h" - , includeBracket "stdlib.h" - , includeBracket "string.h" --- , includeBracket "inttypes.h" - , "" - , "unsigned long long rnd;" - ] - ++ extDeclarations - --- | Generate a temporary C file name. -tmpCFileName :: String -> String -tmpCFileName name = "__" ++ name - -periodLoop :: Name -> Period -> String -periodLoop cName p = unlines - [ "\n" - , "void " ++ tmpCFileName cName ++ "(void) {" - , " int i;" - , " for(i = 0; i < " ++ show p ++ "; i++) {" - , " " ++ cName ++ "();" - , " }" - , "}" - ] - -postCode :: Name -> StreamableMaps Spec -> Vars -> String -postCode cName streams inputExts = - unlines $ - [""] ++ - (if isEmptySM inputExts - then [] - else cleanString) - ++ -- make a loop to complete a period of computation. - [ "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]);" - , " int i;" - , " for(i = 0; i < rnd ; i++) {" - , " " ++ printf "period: %i " ["i"] - ] - ++ inputExtVars inputExts " " - ++ [" " ++ tmpCFileName cName ++ "();"] - ++ 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 - -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 ++ v]) : ls diff --git a/Language/Copilot/Compiler.hs b/Language/Copilot/Compiler.hs deleted file mode 100644 --- a/Language/Copilot/Compiler.hs +++ /dev/null @@ -1,407 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables, Rank2Types, GADTs #-} - --- XXX Clean this up! - --- | Transform the copilot specification in an atom one, and then compile that one. -module Language.Copilot.Compiler - (copilotToAtom, tmpSampleStr, tmpArrName, tmpVarName - ) where - -import Language.Copilot.Core - -import Data.Maybe -import qualified Data.Map as M -import Data.List -import Data.Word (Word32) - -import qualified Language.Atom as A - --- | 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 :: LangElems -> Maybe Period -> Name -> (Period, A.Atom ()) -copilotToAtom (LangElems streams triggers) p cFileName = - (p', A.period p' $ do - prophArrs <- mapStreamableMapsM initProphArr streams - outputs <- mapStreamableMapsM initOutput streams - updateIndexes <- foldStreamableMaps makeUpdateIndex prophArrs (return M.empty) - outputIndexes <- foldStreamableMaps makeOutputIndex prophArrs (return M.empty) - tmpSamples <- foldStreamableMaps - (\_ -> initExtSamples streams outputs prophArrs outputIndexes) - streams - (return emptyTmpSamples) - - let nextStates = makeStates $ - mapStreamableMaps - (nextSt streams prophArrs tmpSamples outputIndexes 0) - streams - - -- One atom rule for each stream - foldStreamableMaps (makeRule nextStates outputs prophArrs - updateIndexes outputIndexes) - streams (return ()) - - M.fold (makeTrigger outputs cFileName) (return ()) triggers - - -- Sampling of the external variables. Remove redundancies. - sequence_ $ snd . unzip $ nubBy (\x y -> fst x == fst y) $ - foldStreamableMaps (\_ -> sampleExts outputs tmpSamples cFileName) streams [] - ) - where p' = period p - --- | For period n >= 5: --- Phase 0: Sample external vars (if any). --- Phase 1: state update. --- Phase 2: Compute output variables. --- Phase 3: Fire triggers (if any). --- Phase 4 up to n: update indexes. -period :: Maybe Int -> Int -period p = - case p of - Nothing -> minPeriod - Just i -> if i >= minPeriod - then i - else error $ "Copilot error: the period is too short, " - ++ "it should be at least " ++ show minPeriod ++ " ticks." - where minPeriod :: Int - minPeriod = 5 - --- For the prophecy arrays -type ArrIndex = Word32 -type ProphArrs = StreamableMaps BoundedArray -type Outputs = StreamableMaps A.V -type Indexes = M.Map Var (A.V ArrIndex) - --- External variables -data PhasedValueVar a = PhV (A.V a) - -data BoundedArray a = B ArrIndex (Maybe (A.A a)) - --- | Takes the NextSts and walks over the tree building the Atom expression. -makeStates :: StreamableMaps NextSt -> StreamableMaps A.E -makeStates trees = - mapStreamableMaps (\_ -> makeState) trees - where - makeState :: (Streamable a) => NextSt a -> A.E a - makeState tree = - case tree of - ExpLeaf s -> s - F1Node f s0 -> f (makeState s0) - F2Node f s0 s1 -> f (makeState s0) (makeState s1) - F3Node f s0 s1 s2 -> f (makeState s0) (makeState s1) (makeState s2) - VarRefLeaf v -> makeState (getElem v trees) - --- | A tree datatype that holds Atom expressions from the 'nextSt' function --- | until we've got all variable references collected up. In particular, we --- | have told function applications. -data NextSt a where - -- Leaves - ExpLeaf :: A.E a -> NextSt a - VarRefLeaf :: Var -> NextSt a - -- Parent nodes - F1Node :: (Streamable a, Streamable b) - => (A.E b -> A.E a) -> NextSt b -> NextSt a - F2Node :: (Streamable a, Streamable b, Streamable c) - => (A.E b -> A.E c -> A.E a) -> NextSt b -> NextSt c -> NextSt a - F3Node :: (Streamable a, Streamable b, Streamable c, Streamable d) - => (A.E b -> A.E c -> A.E d -> A.E a) - -> NextSt b -> NextSt c -> NextSt d -> NextSt a - --- | Compute the next state value. -nextSt :: Streamable a - => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes -> ArrIndex - -> Var -> Spec a -> NextSt a -nextSt streams prophArrs tmpSamples outputIndexes index _ s = - case s of - PVar _ v -> ExpLeaf $ - let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in - A.value var - PArr _ (v, idx) -> ExpLeaf $ - let PhA var = e tmp (tmpArrs tmpSamples) - tmp = tmpArrName v (show idx) - e a b = case getMaybeElem a b of - Nothing -> - error "Error in application of getElem in nextSt." - Just x -> x - in A.value var - Var v -> nextStVar v streams prophArrs tmpSamples outputIndexes index - Const e -> ExpLeaf $ A.Const e - F _ f s0 -> F1Node f (next s0 index) - F2 _ f s0 s1 -> F2Node f (next s0 index) (next s1 index) - F3 _ f s0 s1 s2 -> F3Node f (next s0 index) (next s1 index) (next s2 index) - Append _ s0 -> next s0 index - Drop i s0 -> next s0 (fromInteger (toInteger i) + index) - where next :: Streamable b => Spec b -> ArrIndex -> NextSt b - next s' ind = - nextSt streams prophArrs tmpSamples outputIndexes ind undefined s' - --- | Get the next state when one stream references another Copilot stream variable. -nextStVar :: Streamable a => Var -> StreamableMaps Spec -> ProphArrs - -> TmpSamples -> Indexes -> ArrIndex -> NextSt a -nextStVar v streams prophArrs tmpSamples outputIndexes index = - 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 - then getVar v initLen maybeArr - else let s0 = getElem v streams in - -- XXX This should be generalized to handle arbitrary index values. - -- For now, as a test, we'll just use the cahced nextState value if - -- it's like computing that stream's nextState from scratch. - let newIndex = index - initLen in - if newIndex == 0 then VarRefLeaf v - else nextSt streams prophArrs tmpSamples outputIndexes - newIndex undefined s0 - where getVar :: Streamable a => Var -> ArrIndex -> Maybe (A.A a) -> NextSt a - getVar v' initLen maybeArr = ExpLeaf $ - let outputIndex = case M.lookup v' outputIndexes of - Nothing -> error "Error in function getVar." - Just x -> x - arr = case maybeArr of - Nothing -> error "Error in function getVar (maybeArr)." - Just x -> x in - arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_` - (A.Const (initLen + 1))) - -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'' - _ -> [] - - --- External arrays -data PhasedValueArr a = PhA (A.V a) -- Array name. -data PhasedValueIdx a = PhIdx (A.E a) -- variable that gives index. - -data TmpSamples = - TmpSamples { tmpVars :: StreamableMaps PhasedValueVar - , tmpArrs :: StreamableMaps PhasedValueArr - , tmpIdxs :: StreamableMaps PhasedValueIdx - } - -emptyTmpSamples :: TmpSamples -emptyTmpSamples = TmpSamples emptySM emptySM emptySM - -tmpVarName :: Ext -> Var -tmpVarName v = show v - -tmpArrName :: Ext -> String -> Var -tmpArrName v idx = (tmpVarName v) ++ "_" ++ normalizeVar idx - -initOutput :: forall a. Streamable a => Var -> Spec a -> A.Atom (A.V a) -initOutput v _ = do - atomConstructor (normalizeVar v) (unit::a) - -tmpSampleStr :: String -tmpSampleStr = "tmpSampleVal__" - -initExtSamples :: forall a. Streamable a - => StreamableMaps Spec -> Outputs -> ProphArrs -> Indexes -> Spec a - -> A.Atom TmpSamples -> A.Atom TmpSamples -initExtSamples streams outputs prophArrs outputIndexes s tmpSamples = do - case s of - Const _ -> tmpSamples - Var _ -> tmpSamples - Drop _ s0 -> initExtSamples' s0 tmpSamples - Append _ s0 -> initExtSamples' s0 tmpSamples - F _ _ s0 -> initExtSamples' s0 tmpSamples - F2 _ _ s0 s1 -> initExtSamples' s0 $ - initExtSamples' s1 tmpSamples - F3 _ _ s0 s1 s2 -> initExtSamples' s0 $ initExtSamples' s1 $ - initExtSamples' s2 tmpSamples - PVar _ v -> - do ts <- tmpSamples - let v' = tmpVarName v - vts = tmpVars ts - maybeElem = getMaybeElem v' vts::Maybe (PhasedValueVar a) - name = tmpSampleStr ++ normalizeVar v' - case maybeElem of - Nothing -> - do val <- atomConstructor name (unit::a) - let m' = M.insert v' (PhV val) (getSubMap vts) - return $ ts {tmpVars = updateSubMap (\_ -> m') vts} - Just _ -> return ts - PArr _ (arr, idx) -> - do ts <- tmpSamples - let arr' = tmpArrName arr (show idx) - arrts = tmpArrs ts - idxts = tmpIdxs ts - maybeElem = getMaybeElem arr' arrts::Maybe (PhasedValueArr a) - name = tmpSampleStr ++ normalizeVar arr' - case maybeElem of - Nothing -> -- if the array isn't in the map, neither is the index - do val <- atomConstructor name (unit::a) - let i = case idx of - Const e -> PhIdx $ A.Const e - Var v -> PhIdx $ A.value (getElem v outputs) - _ -> error "Unexpected Spec in initExtSamples." - let m' = M.insert arr' (PhA val) (getSubMap arrts) - let m'' = M.insert arr' i (getSubMap idxts) - return $ ts { tmpArrs = updateSubMap (\_ -> m') arrts - , tmpIdxs = updateSubMap (\_ -> m'') idxts - } - Just _ -> return ts - where initExtSamples' :: Streamable b - => Spec b -> A.Atom TmpSamples -> A.Atom TmpSamples - initExtSamples' = initExtSamples streams outputs prophArrs outputIndexes - --- | For each stream, make an index into its array of values telling you where --- the next value in the array to update is. -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 - --- | For each stream, make an index into its array of values telling you where --- its current output value is. -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 A.E -> Outputs -> ProphArrs - -> Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom () -makeRule exps outputs prophArrs updateIndexes outputIndexes v _ 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 1 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do - ((getElem v outputs)::(A.V a)) A.<== getElem v exps - - Just arr -> do - let updateIndex = fromJust $ M.lookup v updateIndexes - outputIndex = fromJust $ M.lookup v outputIndexes - - A.exactPhase 1 $ A.atom ("update__" ++ normalizeVar v) $ do - arr A.! (A.VRef updateIndex) A.<== getElem v exps - - A.exactPhase 2 $ 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 4 - $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do - updateIndex A.<== (A.VRef updateIndex + A.Const 1) - `A.mod_` A.Const (n + 1) - -sampleStr :: String -sampleStr = "sample__" - --- What we really should be doing is just folding over the TmpSamples, since --- that data should contain all the info we need to construct external variable --- and external array samples. However, there is the issue that for array --- samples, the type of the index may differ from the type of the array, and --- having the spec available provides typing coercion. We could fold over the --- TmpSamples, passing streams in, and extract the appropriate Spec a. -sampleExts :: forall a. Streamable a - => Outputs -> TmpSamples -> Name -> Spec a - -> [(Var, A.Atom ())] -> [(Var, A.Atom ())] -sampleExts outputs ts cFileName s a = do - case s of - Var _ -> a - Const _ -> a - PVar _ v -> - let v' = tmpVarName v - PhV var = case getMaybeElem v' (tmpVars ts) :: Maybe (PhasedValueVar a) of - Nothing -> error $ "Copilot error: variable " ++ v' - ++ " was not defined!." - Just (PhV var') -> PhV var' in - (v', A.exactPhase 0 $ - A.atom (sampleStr ++ normalizeVar v') $ - var A.<== (A.value $ externalAtomConstructor $ getSampleFuncVar v) - ) : a - PArr _ (arr, idx) -> - let arr' = tmpArrName arr (show idx) - PhIdx i = getIdx arr' idx (tmpIdxs ts) - PhA arrV = - case getMaybeElem arr' (tmpArrs ts) :: Maybe (PhasedValueArr a) of - Nothing -> error "Error in fucntion sampleExts." - Just x -> x in - (arr', A.exactPhase 0 $ - A.atom (sampleStr ++ normalizeVar arr') $ - arrV A.<== A.array' (getSampleFuncVar arr) - (atomType (unit::a)) A.!. i - ) : a - F _ _ s0 -> sampleExts' s0 a - F2 _ _ s0 s1 -> sampleExts' s0 $ sampleExts' s1 a - F3 _ _ s0 s1 s2 -> sampleExts' s0 $ sampleExts' s1 $ - sampleExts' s2 a - Append _ s0 -> sampleExts' s0 a - Drop _ s0 -> sampleExts' s0 a - where - sampleExts' :: Streamable b => Spec b -> [(Var, A.Atom ())] -> [(Var, A.Atom ())] - sampleExts' s' a' = sampleExts outputs ts cFileName s' a' - getSampleFuncVar v = - case v of - ExtV extV -> extV - -- XXX A bit of a hack. Atom should be changed to allow "out-of-Atom" - -- assignments. But this works for now. - Fun nm args -> funcShow cFileName nm args - - --- lookup the idx for external array accesses in the map. -getIdx :: forall a. (Streamable a, A.IntegralE a) - => Var -> Spec a -> StreamableMaps PhasedValueIdx -> PhasedValueIdx a -getIdx arr s ts = - case s of - Var _ -> case getMaybeElem arr ts of - Nothing -> error "Error in function getIdx." - Just x -> x - Const e -> PhIdx $ A.Const e - _ -> error $ "Expecing either a variable or constant for the index " - ++ "in the external array access for array " ++ arr ++ "." - --- TRIGGERS ----------------------------- - --- | To make customer C triggers. Only for Spec Bool (others throw an --- error). -makeTrigger :: Outputs -> Name -> Trigger -> A.Atom () -> A.Atom () -makeTrigger outputs cFileName trigger@(Trigger s fnName args) r = - do r - (A.exactPhase 3 $ A.atom (show trigger) $ - do A.cond (getOutput outputs s) - fnCall cFileName fnName args) - --- | Building an external function call in Atom. -fnCall :: Name -> String -> Args -> A.Atom () -fnCall cFileName fnName args = - A.action (\_ -> funcShow cFileName fnName args) [] - -getOutput :: Streamable a => Outputs -> Spec a -> A.E a -getOutput outputs s = - case s of - (Var v) -> A.value - (case getMaybeElem v outputs of - Nothing -> error $ "Copilot error in trigger specification: variable " - ++ v ++ " was not defined!." - Just v' -> v') - (Const c) -> A.Const c - _ -> error "Impossible error in getOutput in Compiler.hs." diff --git a/Language/Copilot/Core.hs b/Language/Copilot/Core.hs deleted file mode 100644 --- a/Language/Copilot/Core.hs +++ /dev/null @@ -1,591 +0,0 @@ -{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, FlexibleContexts, - FlexibleInstances, TypeSynonymInstances #-} - --- | 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 ( - Period, Var, Name, Port(..), Ext(..), - Exs, ExtRet(..), Args, ArgConstVar(..), - Spec(..), Streams, Stream, - Trigger(..), Triggers, LangElems(..), - Streamable(..), StreamableMaps(..), emptySM, - isEmptySM, getMaybeElem, getElem, - foldStreamableMaps, - mapStreamableMaps, mapStreamableMapsM, - filterStreamableMaps, normalizeVar, getVars, Vars, - getAtomType, getSpecs, getTriggers, vPre, funcShow, - notConstVarErr - ) where - -import qualified Language.Atom as A - -import Data.Int -import Data.Word -import Data.List hiding (union) -import qualified Data.Map as M -import Text.Printf -import Control.Monad.Writer (Writer, Monoid(..), execWriter) - ----- Type hierarchy for the copilot language ----------------------------------- - --- | Names of the streams or external variables -type Var = String --- | C file name -type Name = String --- | Atom period -- used as an option to control the duration of a Copilot "tick". -type Period = Int --- -- | Phase of an Atom phase --- type Phase = Int --- | Port over which to broadcast information -data Port = 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 - Var :: Streamable a => Var -> Spec a - Const :: Streamable a => a -> Spec a - - PVar :: Streamable a => A.Type -> Ext -> Spec a - PArr :: (Streamable a, Streamable b, A.IntegralE b) - => A.Type -> (Ext, Spec b) -> 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 - --- | Arguments to be passed to a C function. Either a Copilot variable or a --- constant. A little hacky that I store constants as strings so we don't have --- to pass around types. However, these data are just used to make external C --- calls, for which we have no type info anyway, so it's a bit of a moot point. -data ArgConstVar = V Var - | C String - deriving Eq - -instance Show ArgConstVar where - show args = case args of - V v -> normalizeVar v - C c -> "_const_" ++ c ++ "_" - -type Args = [ArgConstVar] - -data Trigger = - Trigger { trigVar :: Spec Bool - , trigName :: String - -- We carry around both the value and the vars of the arguments to be - -- passed to the trigger. The vars are used to put the arguments in - -- the correct order, since the values are stored in a map, destroying - -- their order. - , trigArgs :: Args} - -type Triggers = M.Map String Trigger - -instance Show Trigger where - show (Trigger s fnName args) = - "trigger_" ++ notConstVarErr s show ++ "_" ++ fnName ++ "_" ++ normalizeVar (show args) - - -- getMaybeVar :: Streamable a => Spec a -> Var - -- getMaybeVar (Var v) = v - -- getMaybeVar s = - -- error $ "Expected a Copilot variable but provided " ++ show s ++ " instead." - --- XXX change the constructors to SimpleVar and Function (or something like that) --- XXX in Ext, we throw away the type info for Args. This is because we're just --- making external calls, and we don't know anything about the types anyway (we --- just make strings). Remove from the datatype. - --- | Holds external variables or external functions to call. -data Ext = ExtV Var - | Fun String Args - -instance Show Ext where - show (ExtV v) = v - show (Fun f args) = normalizeVar f ++ show args - -type Exs = (A.Type, Ext, ExtRet) - -data ExtRet = ExtRetV - | ExtRetA ArgConstVar - deriving Eq - --- | For calling a function with Atom variables. -funcShow :: Name -> String -> Args -> String -funcShow cName fname args = - fname ++ "(" ++ (unwords $ intersperse "," - (map (\arg -> case arg of - v@(V _) -> vPre cName ++ show v - C c -> c - ) args)) ++ ")" - -instance Eq Ext where - (==) (ExtV v0) (ExtV v1) = v0 == v1 - (==) (Fun f0 l0) (Fun f1 l1) = f0 == f1 && l0 == l1 - (==) _ _ = False - --- These belong in Language.hs, but we don't want orphan instances. -instance (Streamable a, A.NumE a) => Num (Spec a) where - (+) = F2 (+) (+) -- A.NumE a => E a is an instance of Num - (*) = F2 (*) (*) - (-) = F2 (-) (-) - negate = F negate negate - abs = F abs abs - signum = F signum signum - fromInteger i = Const (fromInteger i) - -instance (Streamable a, A.NumE a, Fractional a) => Fractional (Spec a) where - (/) = F2 (/) (/) - recip = F recip recip - fromRational r = Const (fromRational r) - -{-# RULES -"Copilot.Core appendAppend" forall ls1 ls2 s. Append ls1 (Append ls2 s) = Append (ls1 ++ ls2) s -"Copilot.Core dropDrop" forall i1 i2 s. Drop i1 (Drop i2 s) = Drop (i1 + i2) s -"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) (PVar t' v') = t == t' && v == v' -- && ph == ph' - (==) (PArr t (v, idx)) (PArr t' (v', idx')) = - t == t' && v == v' && show idx == show idx' -- && ph == ph' - (==) (Var v) (Var v') = v == v' - (==) (Const x) (Const x') = x == x' - (==) s@(F _ _ _) s'@(F _ _ _) = show s == show s' - (==) 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 - --- | Copilot variable reference, taking the name of the generated C file. -vPre :: Name -> String -vPre cName = "copilotState" ++ cName ++ "." ++ cName ++ "." - --- -- | An instruction to send data on a port at a given phase. --- -- data Send a = Sendable a => Send (Var, Phase, Port) --- data Send a = --- Send { sendVar :: Spec a --- , sendPort :: Port --- , sendName :: String} - --- instance Streamable a => Show (Send a) where --- show (Send s (Port port) portName) = --- portName ++ "_port_" ++ show port ++ "_var_" ++ getMaybeVar s - --- | Holds all the different kinds of language elements that are pushed into the --- Writer monad. This currently includes the actual specs and trigger --- directives. (Use the functions in Language.hs to make sends and triggers.) -data LangElems = LangElems - { strms :: StreamableMaps Spec - , trigs :: Triggers} - --- | Container for mutually recursive streams, whose specifications may be --- parameterized by different types -type Streams = Writer LangElems () - -getSpecs :: Streams -> StreamableMaps Spec -getSpecs streams = - let (LangElems ss _) = execWriter streams - in ss - -getTriggers :: Streams -> Triggers -getTriggers streams = - let (LangElems _ triggers) = execWriter streams - in triggers - --- | A named stream -type Stream a = Streamable a => (Var, Spec a) - --- | If the 'Spec' isn't a 'Var' or 'Const', then throw an error; otherwise, --- apply the function. -notConstVarErr :: Streamable a => Spec a -> (ArgConstVar -> b) -> b -notConstVarErr s f = f $ - case s of - Var v -> V v - Const c -> C (showAsC c) - _ -> error $ "You provided specification \n" ++ " " ++ show s - ++ "\n where you needed to give a Copilot variable or constant." - - --- | 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 - -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) -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) -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) -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) -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) -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) -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) -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) -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) -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 -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 - --- | 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 = - case getMaybeElem v sm of - Nothing -> error $ "Error in application of getElem from Core.hs for variable " - ++ v ++ "." - Just x -> x - -getAtomType :: Streamable a => Spec a -> A.Type -getAtomType s = - let unitElem = unit - _ = (Const unitElem) `asTypeOf` s -- to help the typechecker - in atomType unitElem - --- | This function is used to iterate on all the values in all the maps stored --- by a @'StreamableMaps'@, accumulating a value over time -{-# INLINE foldStreamableMaps #-} -foldStreamableMaps :: forall b c. - (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.foldrWithKey f acc bm - acc1 = M.foldrWithKey f acc0 i8m - acc2 = M.foldrWithKey f acc1 i16m - acc3 = M.foldrWithKey f acc2 i32m - acc4 = M.foldrWithKey f acc3 i64m - acc5 = M.foldrWithKey f acc4 w8m - acc6 = M.foldrWithKey f acc5 w16m - acc7 = M.foldrWithKey f acc6 w32m - acc8 = M.foldrWithKey f acc7 w64m - acc9 = M.foldrWithKey f acc8 fm - acc10 = M.foldrWithKey f acc9 dm - in acc10 - -{-# 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 => - (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 b. StreamableMaps c -> [(A.Type, Var, b)] -> (StreamableMaps c, Bool) -filterStreamableMaps sm l = - let (sm2, l2) = foldStreamableMaps filterElem sm (emptySM, []) in - (sm2, (l' \\ nub l2) == []) - 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 y = overlap x y - -instance Monoid LangElems where - mempty = LangElems emptySM M.empty - mappend (LangElems x z) (LangElems x' z') = - LangElems (overlap x x') (M.union z z') -overlap :: StreamableMaps s -> StreamableMaps s -> StreamableMaps s -overlap 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') = - let multDefs = (getVars x `intersect` getVars y) - in if null multDefs then union - else error $ "Copilot error: The variables " - ++ show multDefs ++ " have multiple definitions." - where 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 s -> [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 = - map (\c -> if (c `elem` ".[]()") then '_' else c) - (filter (\c -> c /= ',' && 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) _ = "PVar " ++ show t ++ " " ++ show v -- ++ " " ++ show ph -showRaw (PArr t (v, idx)) _ = - "PArr " ++ show t ++ " (" ++ show v ++ " ! (" ++ show idx ++ "))" -- ++ show ph -showRaw (Var v) _ = "Var " ++ v -showRaw (Const e) _ = 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 " ") ++ ")" - - - diff --git a/Language/Copilot/Dispatch.hs b/Language/Copilot/Dispatch.hs deleted file mode 100644 --- a/Language/Copilot/Dispatch.hs +++ /dev/null @@ -1,246 +0,0 @@ -{-# 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 (check, getExternalVars) -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 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 - , sim :: Bool -- ^ Are we running a C simulator? - , prePostCode :: (Maybe String, Maybe String) -- ^ Code to replace the default - -- initialization and main - , arrDecs :: [(String, Int)] -- ^ When generating C programs to test, we - -- don't know how large external arrays are, so - -- we cannot declare them. Passing in pairs - -- containing the name of the array and it's - -- size allows them to be declared. - , clock :: Maybe A.Clock -- Use the hardware clock to drive the timing - -- of the program. - } - -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 :: LangElems -> Vars -> BackEnd -> Iterations -> Verbose -> IO () -dispatch elems inputExts backEnd iterations verbose = - do - hSetBuffering stdout LineBuffering - mapM_ putStrLn preludeText - isValid <- - case check (strms elems) of - Just x -> print x >> return False - Nothing -> return True - when isValid $ - -- because haskell is lazy, will only get computed if later used - let interpretedLines = showVars (interpretStreams (strms elems) trueInputExts) - iterations - in case backEnd of - Interpreter -> - do - unless allInputsPresents $ error errMsg - mapM_ putStrLn interpretedLines - Opts opts -> - let isInterpreted = - case (interpreted opts) of - Interpreted -> True - NotInterpreted -> False - dirName = outputDir opts - in do - putStrLn $ "Trying to create the directory " ++ dirName - ++ " (if missing) ..." - createDirectoryIfMissing False dirName - copilotToC elems allExts trueInputExts opts isVerbose - let copy ext = copyFile (cName opts ++ ext) - (dirName ++ cName opts ++ ext) - let delete ext = do - f0 <- canonicalizePath (cName opts ++ ext) - f1 <- canonicalizePath (dirName ++ cName opts ++ ext) - unless (f0 == f1) $ 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 (sim opts) (gccCall (Opts opts)) - when ((isInterpreted || isExecuted) && not allInputsPresents) $ - error errMsg - when isExecuted $ execute (strms elems) (dirName ++ cName opts) - trueInputExts isInterpreted - interpretedLines iterations isSilent - where - errMsg = "The interpreter does not have values for some of the external variables." - isVerbose = verbose == Verbose - isSilent = verbose == OnlyErrors - isExecuted = iterations /= 0 - allExts = getExternalVars (strms elems) - (trueInputExts :: StreamableMaps [] , allInputsPresents :: Bool) = - filterStreamableMaps inputExts (map (\(a,v,r) -> (a, show v, r)) allExts) - -copilotToC :: LangElems -> [Exs] -> Vars -> AtomToC -> Bool -> IO () -copilotToC elems allExts trueInputExts opts isVerbose = - let cFileName = cName opts - (p', program) = copilotToAtom elems (getPeriod opts) cFileName - (preCode, postCode) = - getPrePostCode (sim opts) (prePostCode opts) cFileName - (strms elems) allExts (map (\(x,y) -> (ExtV x,y)) - (arrDecs opts)) trueInputExts p' - -- case (prePostCode opts) of - -- Nothing -> - -- getPrePostCode cFileName (strms elems) allExts - -- (map (\(x,y) -> (ExtV x,y)) (arrDecs opts)) - -- trueInputExts p' - -- Just (pre, post) -> (pre, post) - atomConfig = A.defaults - { A.cCode = \_ _ _ -> (preCode, postCode) - , A.cRuleCoverage = False - , A.cAssert = False - , A.hardwareClock = clock opts - , A.cStateName = "copilotState" ++ cFileName - } - in do - putStrLn $ "Compiling Copilot specs to C ..." - (sched, _, _, _, _) <- A.compile cFileName atomConfig program - when isVerbose (putStrLn $ A.reportSchedule sched) - putStrLn $ "Generated " ++ cFileName ++ ".c and " ++ cFileName ++ ".h" - --- | Call Gcc to compile the code. -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" - print 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 = - (unless isSilent $ putStrLn line) >> - executePeriod nextInputExts inLines (n - 1) - -- Checking the compiler and interpreter. - if isInterpreted - then if inLine == line - then nextPeriod - else error $ unlines - [ "Failure: interpreter /= compiler" - , " program name: " ++ programName - , " interpreter: " ++ inLine - , " compiler: " ++ line - ] - else nextPeriod - - -- useful for initializing the sampling temporary variables - firstInputExts <- foldStreamableMaps inputVar trueInputExts (return emptySM) - executePeriod firstInputExts interpretedLines iterations - where - processConfig = - (shell $ programName ++ " " ++ show iterations) - {std_in = CreatePipe, std_out = CreatePipe, std_err = UseHandle stdout} - -showVars :: Vars -> Int-> [String] -showVars interpretedVars n = - showVarsLine interpretedVars 0 - where - showVarsLine inVs i = - if i == n - then [] - else - let (string, inVs') = foldStreamableMaps prettyShow inVs ("", emptySM) - endString = showVarsLine inVs' (i + 1) - beginString = "period: " ++ show i ++ " " ++ string - in - beginString:endString - prettyShow v l (s, vs) = - let s' = v ++ ": " ++ showAsC (head l) ++ " " ++ s - vs' = updateSubMap (\ m -> M.insert v (tail l) m) vs in - (s', vs') - -preludeText :: [String] -preludeText = - [ "" - , "=========================================================================" - , " CoPilot, a stream language for generating hard real-time C monitors. " - , "=========================================================================" - , "Copyright, Galois, Inc. 2010" - , "BSD3 License" - , "Website: http://leepike.github.com/Copilot/" - , "Maintainer: Lee Pike (remove dashes)." - , "Usage: > help" - , "=========================================================================" - , "" - ] diff --git a/Language/Copilot/Examples/Examples.hs b/Language/Copilot/Examples/Examples.hs deleted file mode 100644 --- a/Language/Copilot/Examples/Examples.hs +++ /dev/null @@ -1,372 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} - -module Language.Copilot.Examples.Examples where - -import Data.Word -import Prelude (($)) -import qualified Prelude as Prelude -import qualified Prelude as P - --- for specifying options -import Data.Map (fromList) ---import Data.Maybe (Maybe (..)) ---import System.Random - -import Language.Copilot --- import Language.Copilot.Variables - -fib :: Streams -fib = do - let f = varW64 "f" - t = varB "t" - f .= [0,1] ++ f + (drop 1 f) - t .= even f - where even :: Spec Word64 -> Spec Bool - even w' = w' `mod` 2 == 0 - -t1 :: Streams -t1 = do - let x = varI32 "x" - y = varB "y" - z = varB "z" - w = varB "w" - x .= [0, 1, 2] ++ x - (drop 1 x) - y .= [True, False] ++ y ^ z - z .= x <= drop 1 x - w .= 3 == 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 - let a = varW32 "a" - b = varB "b" - ext8 = extW32 "ext" - ext1 = extW32 "ext" - a .= [0,1] ++ a + ext8 + ext8 + ext1 - b .= [True, False] ++ 2 + a < 5 + ext1 - -t4 :: Streams -t4 = do - let a = varB "a" - b = varB "b" - a .= [True,False] ++ not a - b .= drop 1 a - -t5 :: Streams -t5 = do - let x = varW16 "x" - y = varB "y" - z = varB "z" - x .= [0] ++ x + 1 - y .= [True, True] ++ y - z .= [False] ++ not z - -- triggers - trigger y "y_trigger" void - trigger z "z0_trigger" x - trigger z "z1_trigger" (y <> constW16 3 <> x) - -yy :: Streams -yy = do - let a = varW32 "a" --- ans2 = varW32 "ans2" - a .= [3,5] ++ a + 1 --- ans2 .= a - -maj1 :: Streams -maj1 = do - let v0 = varW32 "v0" - ans2 = varW32 "ans2" - v0 .= [3,7] ++ v0 + 1 - ans2 .= v0 - - -zz :: Streams -zz = do - let a = varW32 "a" - b = varW32 "b" - --a .= [0..4] ++ drop 4 (varW32 a) + 1 - a .= a + 1 - b .= drop 3 a - -xx :: Streams -xx = do - let a = varW32 "a" - b = varW32 "b" - c = varW32 "c" - e = extW32 "ext" - d = varB "d" - f = extW32 (fun "fun1" void) - h = extArrW16 (fun "g" b) a - g = extW16 (fun "fun2" (true <> b <> constW16 3)) - w = varB "w" - a .= e + f - b .= [3] ++ a - c .= [0, 1, 3, 4] ++ drop 1 b - d .= h < g - -- triggers - trigger d "y_trigger" void - trigger w "z0_trigger" (a <> b <> true) - trigger w "z1_trigger" (d <> constW16 3 <> w) - - --- | Sending over ports. -distrib :: Streams -distrib = do - -- vars - let a = varW8 "a" - b = varB "b" - -- spec - a .= [0,1] ++ a + 1 - b .= mod a 2 == 0 - -- sends - trigger true "portA" a - trigger true "portB" b - -monitor :: Streams -monitor = do - -- external variables - let word = extW32 "rx" - arbiter = extB "arbiter" - -- Copilot variables - words = varW32 "words" - arbiters = varB "arbiters" - words .= [0] ++ mux arbiter word words - arbiters .= [False] ++ mux arbiter false arbiter - --- greatest common divisor. -gcd :: Word16 -> Word16 -> Streams -gcd n0 n1 = do - let a = varW16 "a" - b = varW16 "b" - a .= alg n0 a b - b .= alg n1 b a - - let ans = varB "ans" - ans .= a == b - where alg x0 x1 x2 = [x0] ++ mux (x1 > x2) (x1 - x2) 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 - -- externals - let n = extW16 "n" - m = extW16 "m" - -- copilot vars - a = varW16 "a" - b = varW16 "b" - init = varB "init" - ans = varB "ans" - - a .= alg n (sub a b) init - b .= alg m (sub b a) init - ans .= a == b && not init - init .= [True] ++ false - - where sub hi lo = mux (hi > lo) (hi - lo) hi - alg ext ex init = [0] ++ mux init ext ex - -testCoercions :: Streams -testCoercions = do - let word = varW8 "word" - int = varI16 "int" - word .= [1] ++ word * (-2) - int .= 1 + cast word - -testCoercions2 :: Streams -testCoercions2 = do - let b = varB "b" - i = varI16 "i" - j = varI16 "j" - b .= [True] ++ not b - i .= cast j - j .= 3 - -testCoercions3 :: Streams -testCoercions3 = do - let x = varB "x" - y = varI32 "y" - z = varI32 "z" - x .= [True, True] ++ not x - y .= cast x + cast x --- z .= drop 1 (cast x) - z .= cast (not true) - -i8 :: Streams -i8 = let v = varI8 "v" in v .= [0, 1] ++ v + 1 - -trap :: Streams -trap = do - let target = varW32 "target" - target .= [0] ++ target + 1 - - let x = varW32 "x" - let y = varW32 "y" - x .= [0,0] ++ y + target - y .= [0,0] ++ x + 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") - --- testing external array references -testArr :: Streams -testArr = do - -- a .= [True] ++ extArrB ("ff", varW16 b) 5 && extArrB ("ff", varW16 b) 1 - -- && extArrB ("ff", varW16 b) 2 - -- b .= [7] ++ varW16 b + 3 + extArrW16 ("gg", varW16 f) 2 - -- b .= [0] ++ extArrW16 ("gg", varW16 b) 4 - -- c .= [True] ++ var c - -- d .= varB c - let e = varW16 "e" - e .= [6,7,8] ++ 3 -- + extArrW16 ("gg", varW16 b) 2 --- f .= extArrW16 ("gg", varW16 e) 2 + extArrW16 ("gg", varW16 e) 2 - let g = varB "g" - let gg = extArrW16 "gg" e - g .= gg < 13 - -- h .= [0] ++ drop 1 (varW16 g) - - --- t3 :: use an external variable called ext, typed Word32 -t99 :: Streams -t99 = do - let ext = extW32 "ext" - a = varW32 "a" - a .= [0,1] ++ a + ext + ext + ext - - let b = varB "b" - b .= [True, False] ++ 2 + a < 5 + ext - -t11 :: Streams -t11 = do - let v = varB "v" - v .= [False, True, False] ++ v - -tdiv :: Streams -tdiv = do - let a = varW16 "a" - b = varW16 "b" - a .= [3] ++ a `div` 5 - b .= [3] ++ a `mod` 5 - -extT :: Streams -extT = do - let x = extW16 "x" - let y = varW16 "y" - y .= x - --- Examples: -interpretExtT :: Prelude.IO () -interpretExtT = - interpret extT 10 $ - setE (emptySM {w16Map = fromList [("x", [8,9..])]}) - baseOpts -compileExtT :: P.IO () -compileExtT = - compile extT "extT" $ setCode (P.Just "#include \"mylib.h\"", P.Nothing) baseOpts - --- Testing error checking for badly-formed external sampling. - --- Should fail. -extT2 :: Streams -extT2 = do - let y = varW16 "y" - x = extW16 (fun "f" y) - y .= x - --- Should pass. -extT3 :: Streams -extT3 = do - let y = varW16 "y" - x = extW16 (fun "f" y) - y .= [3] ++ x - --- Should fail. -extT4 :: Streams -extT4 = do - let y = varW16 "y" - x = extArrW16 "arr" y - z = extW16 "z" - w = varW16 "w" - y .= z - w .= x - --- Should fail. -extT5 :: Streams -extT5 = do - let y = varW16 "y" - x = extW16 (fun "f" y) - z = extW16 "z" - w = varW16 "w" - y .= z - w .= x - --- Should work. -extT6 :: Streams -extT6 = do - let y = varW16 "y" - x = extArrW16 "arr" y - z = extW16 "z" - w = varW16 "w" - y .= [7] ++ z - w .= x - - - --- test external idx before after and in the stream it references --- test multiple defs --- test defs in functions --- test arrays at different indexes diff --git a/Language/Copilot/Examples/LTLExamples.hs b/Language/Copilot/Examples/LTLExamples.hs deleted file mode 100644 --- a/Language/Copilot/Examples/LTLExamples.hs +++ /dev/null @@ -1,83 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} - -module Language.Copilot.Examples.LTLExamples where - -import Prelude (replicate, Int, replicate) -import qualified Prelude as P - -import Language.Copilot -import Language.Copilot.Libs.Indexes -import Language.Copilot.Libs.LTL - ----------------- --- LTL tests --- ----------------- - --- Can be tested with various values of val. Use the interpreter to see the --- outputs. - -testing, output :: Spec Bool -testing = varB "testing" -output = varB "output" - -tSoonest :: Int -> Streams -tSoonest val = do - testing .= replicate (val+2) False ++ true - let out = varI16 "out" - out .= soonest val testing - -tLatest :: Int -> Streams -tLatest val = do - testing .= replicate (val-2) False ++ true - let out = varI16 "out" - out .= latest val testing - -tAlways :: Int -> Int -> Streams -tAlways i1 i2 = do - testing .= (replicate i1 True P.++ [False]) ++ true - output `ltl` always i2 testing - -tNext :: Int -> Streams -tNext i1 = do - testing .= (replicate i1 False P.++ [True]) ++ false - output `ltl` next testing - -tFuture :: Int -> Int -> Streams -tFuture i1 i2 = do - testing .= (replicate i1 False P.++ [True]) ++ testing - output `ltl` eventually i2 testing - - -c, t0, t1 :: Spec Bool -t0 = varB "t0" -t1 = varB "t1" -c = varB "c" - -tUntil :: Int -> Int -> Int -> Streams -tUntil i1 i2 i3 = do - t1 .= replicate i1 False ++ true - t0 .= replicate i2 True ++ false - output `ltl` until i3 t0 t1 - -tRelease0 :: Int -> Streams -tRelease0 val = output `ltl` release val false true - -tRelease1 :: Int -> Int -> Streams -tRelease1 i1 i2 = do - t1 .= replicate i1 True ++ c - c .= [False] ++ not c - t0 .= true - output `ltl` release i2 t0 t1 - -testRules :: Streams -testRules = do - let v1 = varB "v1" - v2 = varB "v2" - v3 = varI16 "v3" - v4 = varB "v4" - ex = extI8 "ex" - v1 .= (not true) || v2 - v2 .= [True, False] ++ [True] ++ v3 < cast ex - v3 .= 0 + drop 3 6 - v4 `ltl` always 5 v1 - diff --git a/Language/Copilot/Examples/PTLTLExamples.hs b/Language/Copilot/Examples/PTLTLExamples.hs deleted file mode 100644 --- a/Language/Copilot/Examples/PTLTLExamples.hs +++ /dev/null @@ -1,132 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} - -module Language.Copilot.Examples.PTLTLExamples where - -import Prelude (($), repeat, replicate, IO()) -import qualified Prelude as P -import Data.Map (fromList) - -import Language.Copilot hiding (check) -import Language.Copilot.Libs.PTLTL -import Language.Copilot.Libs.Vote - --- Next examples are for testing of the ptLTL library - --- test of previous -tstdatprv :: Streams -tstdatprv = do - let a = varB "a" - a .= [True, False] ++ a - -tprv :: Streams -tprv = do - let c = varB "c" - a = varB "a" - tstdatprv - c `ptltl` previous a - --- test of alwaysBeen -tstdatAB :: Streams -tstdatAB = do - let d = varB "d" - d .= [True, True, True, True, True, True, True, False] ++ d - -tAB :: Streams -tAB = do - let f = varB "f" - d = varB "d" - tstdatAB - f `ptltl` alwaysBeen d - --- test of eventuallyPrev -tstdatEP :: Streams -tstdatEP = do - let g = varB "g" - g .= [False, False, False, False, False, True, False] ++ g - -tEP :: Streams -tEP = do - let h = varB "h" - g = varB "g" - tstdatEP - h `ptltl` eventuallyPrev g - -q1, q2, z :: Spec Bool -q1 = varB "q1" -q2 = varB "q2" -z = varB "z" - --- test of since -tstdat1Sin :: Streams -tstdat1Sin = q1 .= [False, False, False, False, True] ++ true --varB "q1" - -tstdat2Sin :: Streams -tstdat2Sin = q2 .= [False, False, True, False, False, False, False ] ++ q2 - -tSince :: Streams -tSince = do - tstdat1Sin - tstdat2Sin - z `ptltl` (q1 `since` q2) - --- with external variables --- interface $ setE (emptySM {bMap = fromList [("e1", [True,True ..]), ("e2", [False,False ..])]}) $ interpretOpts tSinExt 20 -tSinExt :: Streams -tSinExt = do - let e1 = extB "e1" - e2 = extB "e2" - z `ptltl` (e1 `since` e2) - -tSinExt2 :: Streams -tSinExt2 = do - let e1 = extB "e1" - e2 = extB "e2" - a = varB "a" - s = varB "s" - d = varB "d" - t = varB "t" - e = varB "e" - - a .= not e1 - s `ptltl` (e2 `since` d) - t `ptltl` (alwaysBeen $ not a) - e .= e1 ==> d - --- "If the majority of the engine temperature probes exeeds 250 degrees, then --- the cooler is engaged and remains engaged until the majority of the engine --- temperature drops to 250 or below. Otherwise, trigger an immediate shutdown --- of the engine." -engine :: Streams -engine = do - -- external vars - let t0 = extW8 "temp_probe_0" - t1 = extW8 "temp_probe_1" - t2 = extW8 "temp_probe_2" - cooler = extB "fan_status" - -- Copilot vars - maj = varW8 "maj" - check = varB "maj_check" - overHeat = varB "over_heat" - monitor = varB "monitor" - -- local vars - temps = [t0, t1, t2] - maj .= majority temps - check .= aMajority temps maj - overHeat `ptltl` ( (cooler || (maj <= 250 && check)) - `since` (maj > 250)) - monitor .= not overHeat - trigger monitor "shutoff_engine" void - - -engineRun :: Bool -> IO () -engineRun b = if b then - interpret engine 40 $ - setE (emptySM { bMap = fromList [("fan_status", replicate 3 False P.++ repeat False)] - , w8Map = fromList [ ("temp_probe_0", [240,240..]) - , ("temp_probe_1", [240,241..]) - , ("temp_probe_2", [240,241..]) - ] - }) - baseOpts - else compile engine "engine" $ setSim baseOpts - diff --git a/Language/Copilot/Examples/StatExamples.hs b/Language/Copilot/Examples/StatExamples.hs deleted file mode 100644 --- a/Language/Copilot/Examples/StatExamples.hs +++ /dev/null @@ -1,26 +0,0 @@ -module Language.Copilot.Examples.StatExamples where - -import Prelude () -import Language.Copilot.Core -import Language.Copilot.Language -import Language.Copilot.Libs.Statistics - -t0 :: Streams -t0 = do - let minV = varW16 "min" - maxV = varW16 "max" - sumV = varW16 "sum" - a = varW16 "a" - - a .= [0..5] ++ a + 6 - minV .= min 3 a - maxV .= max 3 a - sumV .= sum 3 a - -tMean :: Streams -tMean = do - let a = varD "a" - out = varD "out" - - a .= [0..5] ++ a + 6 - out .= mean 4 a diff --git a/Language/Copilot/Help.hs b/Language/Copilot/Help.hs deleted file mode 100644 --- a/Language/Copilot/Help.hs +++ /dev/null @@ -1,172 +0,0 @@ --- | 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 -> Int -> (Options -> Options) -> IO ()" - , " > interpret STREAMS RNDS (noOpts | [$ OPTS])" - , " Executes the interpreter for the Copilot specification STREAMS of type" - , " 'Streams', where the specification is interpreted as a set of mutually-" - , " recursive Haskell infinite lists. The output from the lists is given" - , " for RNDS indexes. RNDS must be greater than 0." - , "" - , " compile :: Streams -> String -> (Options -> Options) -> IO ()" - , " > compile STREAMS FILENAME (noOpts | [$ OPTS])" - , " 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 (noOpts | [$ OPTS])" - , " 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. Testing" - , " external arrays is currently not supported." - , "" - , " > Prelude.putStr $ Prelude.show STREAMS -- or simply" - , " > STREAMS -- in ghci" - , " Pretty-prints the parsed Copilot specification of type 'Streams'." - , "" - , " verify :: FilePath -> Int -> String -> IO () (FilePath is a synonym for String)" - , " > verify PATH/FILE.c n opts (opts are additional options for cbmc.)" - , " 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. The entry" - , " point of main() is assumed, and it is also assumed that main() can be" - , " unrolled at least n times, where n is an Int. This command is thus" - , " best used when generating a simulation program (see the setSim option)." - , " 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 described below." - , "" - , " 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." - , "" - , " setR :: Int -> Options -> Options (t)" - , " default: 0" - , " Sets the seed for generating random Copilot specification during" - , " testing." - , "" - , " setCode :: (Maybe String, Maybe String) -> Options -> Options (c)" - , " default: (Nothing, Nothing)." - , " To place arbitrary C code in the generated file. The first element of" - , " the pair is code to place above the generated code, and the second" - , " element is code to place below. 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." - , "" - , " setSim :: Options -> Options (c)" - , " default: False" - , " When used, generates a main() function in the generated C file that" - , " includes a driver to call the scheduler to simulate the function and" - , " print the reults to standard out. Additionally, we attempt to compile" - , " the code when setSim is used." - , "" - , " setArrs :: [(String,Int)] -> Options -> Options (c)" - , " default: Nothing" - , " When generating C programs to test, we don't know how large external" - , " arrays are, so we cannot declare them. Passing in pairs containing the" - , " name of the array and it's size allows them to be declared." - , "" - , "" - , "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 (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()." - , "" - , " > test 1000 baseOpts" - , " Compare the compiler and interpreter for a randomly-generated Copilot" - , " spec for 1000 iterations." - , "" - , " > Prelude.sequence_ [test 10 $ setR x baseOpts | x <- [0..100]]" - , " Compare the compiler and interpreter on 100 random seeds generating" - , " Copilot specs, for 10 iterations each." - , "" - , " > verify \"foo.c\" n baseOpts" - , " Calls cbmc on foo.c (where foo.c is in the current directory) and" - , " unrolls the program n times." - ] diff --git a/Language/Copilot/Interface.hs b/Language/Copilot/Interface.hs deleted file mode 100644 --- a/Language/Copilot/Interface.hs +++ /dev/null @@ -1,263 +0,0 @@ -{-# LANGUAGE FlexibleInstances #-} - --- | Used by the end-user to easily give its arguments to dispatch. -module Language.Copilot.Interface ( - Options(), baseOpts, test, interpret, compile, verify, interface - , help , setE, setC, setO, setP, setI, setCode, setN, setV, setR - , setDir, setGCC, setArrs, setClock, setSim, - module Language.Copilot.Dispatch - ) where - -import Language.Copilot.Core ---import Language.Copilot.Language (opsF, opsF2, opsF3) -import Language.Copilot.Language.RandomOps (opsF, opsF2, opsF3) -import Language.Copilot.Tests.Random -import Language.Copilot.Dispatch -import Language.Copilot.Help -import qualified Language.Atom as A (Clock) - -import System.Random -import System.Exit -import System.Cmd -import Data.Maybe -import qualified Data.Map as M (empty) -import Control.Monad (when) - -data Options = Options { - optStreams :: Maybe (StreamableMaps Spec), -- ^ If there's no Streams, - -- then generate random - -- streams. --- optSends :: StreamableMaps Send, -- ^ 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, Maybe String), -- ^ Code to append above and below the C file. - optSimulate :: Bool, -- ^ Do we want a simulation driver? - optTriggers :: Triggers, -- ^ A list of Copilot variable C function name - -- pairs. The C funciton is called if the - -- Copilot stream becomes True. The Stream - -- must be of Booleans and the C function must - -- be of type void @foo(void)@. There should - -- be no more than one function per trigger - -- variable. Triggers fire in the same phase - -- (1) that output vars are assigned. - optArrs :: [(String, Int)], -- ^ When generating C programs to test, we - -- don't know how large external arrays are, - -- so we cannot declare them. Passing in - -- pairs containing the name of the array - -- and it's size allows them to be - -- declared. - optClock :: Maybe A.Clock -- ^ Use the hardware clock to drive the timing of the program? - } - -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, Nothing), - optSimulate = False, - optTriggers = M.empty, - optArrs = [], - optClock = 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 $ setSim opts - -interpret :: Streams -> Int -> Options -> IO () -interpret streams n opts = - interface $ setI $ setN n $ opts {optStreams = Just (getSpecs streams)} - -compile :: Streams -> Name -> Options -> IO () -compile streams fileName opts = - interface $ setC "-Wall" $ setO fileName - $ setTriggers (getTriggers streams) - $ opts {optStreams = Just (getSpecs streams)} - -verify :: FilePath -> Int -> String -> IO () -verify file n opts = do - putStrLn "Calling cbmc, developed by Daniel Kroening \& Edmund Clarke." - putStrLn ", with the following checks:" - putStrLn " --bounds-check enable array bounds checks" - putStrLn " --div-by-zero-check enable division by zero checks" - putStrLn " --pointer-check enable pointer checks" - putStrLn " --overflow-check enable arithmetic over- and underflow checks" - putStrLn " --nan-check check floating-point for NaN" - putStrLn "" - putStrLn "Assuming main() as the entry point unless specified otherwise (--function f)" - putStrLn cmd - code <- system cmd - case code of - ExitSuccess -> return () - _ -> do putStrLn "" - putStrLn $ "An error was returned by cbmc. This may have be due to cbmc not finding the file " ++ file ++ ". Perhaps cbmc is not installed on your system, is not in your path, cbmc cannot be called from the command line on your system, or " ++ file ++ " does not exist. See for more information on cbmc." - where cmd = unwords ("cbmc" : args) - args = ["--div-by-zero-check", "--overflow-check", "--bounds-check" - , "--nan-check", "--pointer-check" - , "--unwind " ++ show n, opts, file] - - --- Small functions for easy modification of the Options record - --- -- | Set the directives for sending stream values on ports. --- setS :: StreamableMaps Send -> Options -> Options --- setS sends opts = opts {optSends = sends} - --- -- | Set the directives for sending stream values on ports. -setTriggers :: Triggers -> Options -> Options -setTriggers triggers opts = opts {optTriggers = triggers} - --- | 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} - --- | Set the external arrays. -setArrs :: [(String,Int)] -> Options -> Options -setArrs ls opts = opts {optArrs = ls} - --- | Sets the hardware clock. See --- http://github.com/tomahawkins/atom/blob/master/Language/Atom/Code.hs. -setClock :: A.Clock -> Options -> Options -setClock clk opts = opts {optClock = Just clk} - --- | 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} - --- | Set the random seed for generating random `Copilot` specs. -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 -setCode :: (Maybe String, Maybe String) -> Options -> Options -setCode pp opts = opts {optPrePostCode = pp} - --- | Include simulation driver code (in a main() loop)? -setSim :: Options -> Options -setSim opts = opts {optSimulate = True} - --- | The "main" function that dispatches. -interface :: Options -> IO () -interface opts = - do - seed <- createSeed opts - let (streams, vars) = getStreamsVars opts seed --- sends = optSends opts - triggers = optTriggers 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 (LangElems streams triggers) vars backEnd iterations verbose - -createSeed :: Options -> IO Int -createSeed opts = - case optRandomSeed opts of - Nothing -> - do - g <- newStdGen - return . fst . random $ g - Just i -> return i - --- | Were streams given? If not, just make random streams. -getStreamsVars :: Options -> Int -> (StreamableMaps Spec, Vars) -getStreamsVars opts seed = - case optStreams opts of - Nothing -> randomStreams opsF opsF2 opsF3 (mkStdGen seed) - Just s -> - case optExts opts of - Nothing -> (s, emptySM) - Just vs -> (s, vs) - -getBackend :: Options -> Int -> BackEnd -getBackend opts seed = - case optCompile opts of - Nothing -> - if not $ optInterpret opts - then error "neither interpreted nor compiled: nothing to be done" - else Interpreter - Just gccOptions -> - Opts $ AtomToC { - cName = optCName opts ++ if isJust $ optRandomSeed opts then show seed else "", - gccOpts = gccOptions, - getPeriod = optPeriod opts, - interpreted = if optInterpret opts then Interpreted else NotInterpreted, - outputDir = optOutputDir opts, - compiler = optCompiler opts, - prePostCode = optPrePostCode opts, - sim = optSimulate opts, --- triggers = optTriggers opts, - arrDecs = optArrs opts, - clock = optClock opts - } - -help :: IO () -help = putStrLn helpStr diff --git a/Language/Copilot/Interpreter.hs b/Language/Copilot/Interpreter.hs deleted file mode 100644 --- a/Language/Copilot/Interpreter.hs +++ /dev/null @@ -1,42 +0,0 @@ -{-# LANGUAGE Rank2Types #-} - --- | The Copilot interpreter. -module Language.Copilot.Interpreter - (interpretStreams) where - -import Language.Copilot.Core - --- | 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 :: forall a. 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 -> checkV v (\v' -> (getElem v' moVs)) - PArr _ (v,s') -> checkV v (\v' -> map (\i -> getElem v' moVs - !! fromIntegral i) - (interpret inVs moVs s')) - Append ls s' -> ls ++ interpret inVs moVs s' - Drop i s' -> drop i $ interpret inVs moVs s' - F f _ s' -> map f (interpret inVs moVs s') - F2 f _ s0 s1 -> zipWith f (interpret inVs moVs s0) - (interpret inVs moVs s1) - F3 f _ s0 s1 s2 -> zipWith3 f - (interpret inVs moVs s0) - (interpret inVs moVs s1) - (interpret inVs moVs s2) - where - checkV :: Ext -> (Var -> [a]) -> [a] - checkV v f = - case v of - ExtV v' -> f v' - -- XXX support this? - Fun _ _ -> error $ "Sampling functions is not currently supported" - ++ " in the Copilot interpreter." - diff --git a/Language/Copilot/Language.hs b/Language/Copilot/Language.hs deleted file mode 100644 --- a/Language/Copilot/Language.hs +++ /dev/null @@ -1,222 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude, FlexibleContexts #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | 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, - -- * Copilot variable declarations. - var, varB, varI8, varI16, varI32, varI64, - varW8, varW16, varW32, varW64, varF, varD, - -- * Copilot constant declarations. For the most part, these are - -- unnecessary, as constants are automatically lifted in into the * - -- Copilot types. They are useful though for specifying triggers and * - -- function samplings. - const, constI8, constI16, constI32, constI64, - constW8, constW16, constW32, constW64, constF, constD, - -- * Boolean stream constants - true, false, - module Language.Copilot.Language.Sampling, - -- * Constructs of the copilot language - drop, (++), (.=), -- (..|), - -- * Triggers - module Language.Copilot.Language.FunctionCalls, - -- * Safe casting - module Language.Copilot.Language.Casting, - notConstVarErr - ) where - -import qualified Language.Atom as A -import Data.Int -import Data.Word -import Prelude ( Bool(..), Num(..), Float, Double, ($), error - , Fractional(..), fromInteger, Show(..)) -import qualified Prelude as P -import Control.Monad.Writer (tell) -import qualified Data.Map as M - -import Language.Copilot.Core -import Language.Copilot.Language.Sampling -import Language.Copilot.Language.Casting -import Language.Copilot.Language.FunctionCalls ---import Language.Copilot.Language.RandomOps - ----- Operators and functions --------------------------------------------------- - -not :: Spec Bool -> Spec Bool -not = F P.not A.not_ - - --- | 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.div A.div_ - --- | As mod and div, except that if the division would be by 0, the first --- argument is used as a default. -mod0, div0 :: (Streamable a, A.IntegralE a) => a -> Spec a -> Spec a -> Spec a -mod0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.div` d - else x0 `P.div` x1) - (\ e0 e1 -> A.mod0_ e0 e1 d) -div0 d = F2 (\ x0 x1 -> if x1 P.== 0 then x0 `P.mod` d - else x0 `P.mod` x1) - (\ e0 e1 -> A.div0_ e0 e1 d) - - --- class (Streamable a, A.OrdE a) => SpecOrd a where --- (<) - -(<), (<=), (>=), (>) :: (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 - --- | 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 ||, &&, ^, ==> - - ----- Constructs of the language ------------------------------------------------ - - --- If a generic 'var' declaration is insufficient for the type-checker to --- determine the type, a monomorphic var operator can be used. - --- | Useful for writing libraries. -var :: Streamable a => Var -> Spec a -var = Var - -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 - --- | Define a stream variable. -(.=) :: Streamable a => Spec a -> Spec a -> Streams -v .= s = - case v of - (Var v') -> tell $ LangElems (updateSubMap (M.insert v' s) emptySM) - M.empty - _ -> error $ "Given spec " P.++ show v - P.++ " but expected a variable in a Copilot definition (.=)." - --- | Coerces a type that is 'Streamable' into a Copilot constant. -const :: Streamable a => a -> Spec a -const = 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 - -true, false :: Spec Bool -true = Const True -false = Const False - --- | 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 - - -infixr 3 ++ -infixr 2 .= - ----- 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 - #-} - --- "Copilot.Core CastLift" forall s i. drop i (cast s) = cast (drop i s) diff --git a/Language/Copilot/Language/Casting.hs b/Language/Copilot/Language/Casting.hs deleted file mode 100644 --- a/Language/Copilot/Language/Casting.hs +++ /dev/null @@ -1,99 +0,0 @@ --- | Safe casting of values. - -module Language.Copilot.Language.Casting ( cast ) where - -import qualified Language.Atom as A - -import Data.Int -import Data.Word - -import Language.Copilot.Core - --- | Cast 'a' into 'b'. We only allow "safe casts" to larger types. -class Streamable a => Castable a where - castFrom :: (Streamable b, A.IntegralE b) => Spec a -> Spec b - cast :: (Castable b, Streamable b) => Spec b -> Spec a - -castErr :: String -> A.Type -> String -castErr toT fromT = "Error: cannot cast type " ++ show fromT - ++ " into " ++ toT ++ ". Only casts guarnateed \n" - ++ "not to change sign and to larger types are allowed." - -instance Castable Bool where - castFrom = F (\b -> if b then 1 else 0) - (\b -> A.mux b 1 0) - cast x = error $ castErr "Bool" (getAtomType x) - -instance Castable Word8 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - t -> error $ castErr "Word8" t - -instance Castable Word16 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Word8 -> castFrom x - t -> error $ castErr "Word16" t - -instance Castable Word32 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - t -> error $ castErr "Word32" t - -instance Castable Word64 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - A.Word32 -> castFrom x - t -> error $ castErr "Word64" t - -instance Castable Int8 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - t -> error $ castErr "Int8" t - -instance Castable Int16 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Int8 -> castFrom x - A.Word8 -> castFrom x - t -> error $ castErr "Int16" t - -instance Castable Int32 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Int8 -> castFrom x - A.Int16 -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - t -> error $ castErr "Int32" t - -instance Castable Int64 where - castFrom = F (fromInteger . toInteger) - (A.Retype . A.ue) - cast x = case getAtomType x of - A.Bool -> castFrom x - A.Int8 -> castFrom x - A.Int16 -> castFrom x - A.Int32 -> castFrom x - A.Word8 -> castFrom x - A.Word16 -> castFrom x - A.Word32 -> castFrom x - t -> error $ castErr "Int64" t diff --git a/Language/Copilot/Language/FunctionCalls.hs b/Language/Copilot/Language/FunctionCalls.hs deleted file mode 100644 --- a/Language/Copilot/Language/FunctionCalls.hs +++ /dev/null @@ -1,46 +0,0 @@ -{-# LANGUAGE TypeSynonymInstances #-} - -module Language.Copilot.Language.FunctionCalls - ((<>), trigger, void, fun) where - -import Language.Copilot.Core - -import Control.Monad.Writer (tell) -import qualified Data.Map as M - --- | No C arguments -void :: Args -void = [] - -class ArgCl a where - (<>) :: Streamable b => Spec b -> a -> Args - trigger :: Spec Bool -> String -> a -> Streams - fun :: String -> a -> Ext - -instance ArgCl Args where - s <> args = argUpdate s args - trigger v fnName args = trigger' v fnName args - fun = Fun - -instance Streamable b => ArgCl (Spec b) where - s <> s' = (argUpdate s (argUpdate s' [])) - trigger v fnName arg = - let arg' = argUpdate arg [] in - trigger' v fnName arg' - fun f arg = - let arg' = argUpdate arg [] in - Fun f arg' - -infixr 1 <> - --- | XXX document -trigger' :: Spec Bool -> String -> Args -> Streams -trigger' v fnName args = - tell $ LangElems - emptySM - (M.insert (show trig) trig M.empty) - where trig = Trigger v fnName args - -argUpdate :: Streamable a => Spec a -> Args -> Args -argUpdate s args = notConstVarErr s (\v -> v:args) - diff --git a/Language/Copilot/Language/RandomOps.hs b/Language/Copilot/Language/RandomOps.hs deleted file mode 100644 --- a/Language/Copilot/Language/RandomOps.hs +++ /dev/null @@ -1,206 +0,0 @@ -{-# LANGUAGE Rank2Types, ScopedTypeVariables #-} - --- | Sets of operators for Tests.Random.hs - -module Language.Copilot.Language.RandomOps ( --- mkOp, mkOp2, mkOp3, mkOp2Coerce, mkOp2Ord, mkOp2Eq, - opsF, opsF2, opsF3, - module Language.Copilot.Tests.Random - ) where - -import qualified Language.Atom as A - -import Prelude (($), Float, Double, error, zip, asTypeOf) -import Data.Int -import Data.Word -import System.Random -import Data.Map as M - -import Language.Copilot.Core -import Language.Copilot.Language -import Language.Copilot.Analyser -import Language.Copilot.Tests.Random - -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 `asTypeOf` (Const c0)) (s1 `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 $ mkOp2Coerce op (unit::Int8) (unit::Int8) - opI16 = fromOp $ mkOp2Coerce op (unit::Int16) (unit::Int16) - opI32 = fromOp $ mkOp2Coerce op (unit::Int32) (unit::Int32) - opI64 = fromOp $ mkOp2Coerce op (unit::Int64) (unit::Int64) - opW8 = fromOp $ mkOp2Coerce op (unit::Word8) (unit::Word8) - opW16 = fromOp $ mkOp2Coerce op (unit::Word16) (unit::Word16) - opW32 = fromOp $ mkOp2Coerce op (unit::Word32) (unit::Word32) - opW64 = fromOp $ mkOp2Coerce op (unit::Word64) (unit::Word64) - opF = fromOp $ mkOp2Coerce op (unit::Float) (unit::Float) - opD = fromOp $ 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 - _ -> 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 $ mkOp2Coerce op (unit::Bool) (unit::Bool) - opI8 = fromOp $ mkOp2Coerce op (unit::Int8) (unit::Int8) - opI16 = fromOp $ mkOp2Coerce op (unit::Int16) (unit::Int16) - opI32 = fromOp $ mkOp2Coerce op (unit::Int32) (unit::Int32) - opI64 = fromOp $ mkOp2Coerce op (unit::Int64) (unit::Int64) - opW8 = fromOp $ mkOp2Coerce op (unit::Word8) (unit::Word8) - opW16 = fromOp $ mkOp2Coerce op (unit::Word16) (unit::Word16) - opW32 = fromOp $ mkOp2Coerce op (unit::Word32) (unit::Word32) - opW64 = fromOp $ mkOp2Coerce op (unit::Word64) (unit::Word64) - opF = fromOp $ mkOp2Coerce op (unit::Float) (unit::Float) - opD = fromOp $ 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 (+) -(-$) = mkOp2 (-) -(*$) = mkOp2 (*) - -(/$) :: (Streamable a, A.NumE a, Fractional a, Random a) => Operator a -(/$) = mkOp2 (/) - -(<$), (<=$), (>=$), (>$) :: 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 fed 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_] - } diff --git a/Language/Copilot/Language/Sampling.hs b/Language/Copilot/Language/Sampling.hs deleted file mode 100644 --- a/Language/Copilot/Language/Sampling.hs +++ /dev/null @@ -1,99 +0,0 @@ -{-# LANGUAGE TypeSynonymInstances #-} - --- | Functions for sampling external variables. - -module Language.Copilot.Language.Sampling ( - -- * The next functions provide easier access to typed external variables. - extB, extI8, extI16, extI32, extI64, - extW8, extW16, extW32, extW64, extF, extD, - -- * The next functions provide easier access to typed external arrays. - extArrB, extArrI8, extArrI16, extArrI32, extArrI64, - extArrW8, extArrW16, extArrW32, extArrW64, extArrF, extArrD, - ) where - - -import qualified Language.Atom as A -import Data.Int -import Data.Word - -import Language.Copilot.Core - -class ExtCl a where - extB :: a -> Spec Bool - extI8 :: a -> Spec Int8 - extI16 :: a -> Spec Int16 - extI32 :: a -> Spec Int32 - extI64 :: a -> Spec Int64 - extW8 :: a -> Spec Word8 - extW16 :: a -> Spec Word16 - extW32 :: a -> Spec Word32 - extW64 :: a -> Spec Word64 - extF :: a -> Spec Float - extD :: a -> Spec Double - - -- for arrays - extArrB :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Bool - extArrI8 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int8 - extArrI16 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int16 - extArrI32 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int32 - extArrI64 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Int64 - extArrW8 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word8 - extArrW16 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word16 - extArrW32 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word32 - extArrW64 :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Word64 - extArrF :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Float - extArrD :: (Streamable b, A.IntegralE b) => a -> Spec b -> Spec Double - --- | For global variables. -instance ExtCl String where - extB var = PVar A.Bool (ExtV var) - extI8 var = PVar A.Int8 (ExtV var) - extI16 var = PVar A.Int16 (ExtV var) - extI32 var = PVar A.Int32 (ExtV var) - extI64 var = PVar A.Int64 (ExtV var) - extW8 var = PVar A.Word8 (ExtV var) - extW16 var = PVar A.Word16 (ExtV var) - extW32 var = PVar A.Word32 (ExtV var) - extW64 var = PVar A.Word64 (ExtV var) - extF var = PVar A.Float (ExtV var) - extD var = PVar A.Double (ExtV var) - - -- for arrays - extArrB = \v idx -> PArr A.Bool (ExtV v, idx) - extArrI8 = \v idx -> PArr A.Int8 (ExtV v, idx) - extArrI16 = \v idx -> PArr A.Int16 (ExtV v, idx) - extArrI32 = \v idx -> PArr A.Int32 (ExtV v, idx) - extArrI64 = \v idx -> PArr A.Int64 (ExtV v, idx) - extArrW8 = \v idx -> PArr A.Word8 (ExtV v, idx) - extArrW16 = \v idx -> PArr A.Word16 (ExtV v, idx) - extArrW32 = \v idx -> PArr A.Word32 (ExtV v, idx) - extArrW64 = \v idx -> PArr A.Word64 (ExtV v, idx) - extArrF = \v idx -> PArr A.Float (ExtV v, idx) - extArrD = \v idx -> PArr A.Double (ExtV v, idx) - --- | For functions. -instance ExtCl Ext where - extB = PVar A.Bool - extI8 = PVar A.Int8 - extI16 = PVar A.Int16 - extI32 = PVar A.Int32 - extI64 = PVar A.Int64 - extW8 = PVar A.Word8 - extW16 = PVar A.Word16 - extW32 = PVar A.Word32 - extW64 = PVar A.Word64 - extF = PVar A.Float - extD = PVar A.Double - -- for arrays - extArrB = curry (PArr A.Bool) - extArrI8 = curry (PArr A.Int8) - extArrI16 = curry (PArr A.Int16) - extArrI32 = curry (PArr A.Int32) - extArrI64 = curry (PArr A.Int64) - extArrW8 = curry (PArr A.Word8) - extArrW16 = curry (PArr A.Word16) - extArrW32 = curry (PArr A.Word32) - extArrW64 = curry (PArr A.Word64) - extArrF = curry (PArr A.Float) - extArrD = curry (PArr A.Double) - diff --git a/Language/Copilot/Libs/ErrorChks.hs b/Language/Copilot/Libs/ErrorChks.hs deleted file mode 100644 --- a/Language/Copilot/Libs/ErrorChks.hs +++ /dev/null @@ -1,28 +0,0 @@ --- | Basic error checking for other libraries. - -module Language.Copilot.Libs.ErrorChks(nOneChk, nPosChk, int16Chk) where - -import Data.Int (Int16) - -import Language.Copilot.Core - -chk :: String -> Int -> Spec a -> Int -> Spec a -chk name n s m = - if n < m - then error $ "Value " ++ show n ++ " in operator " ++ name - ++ " must be greater than or equal to " ++ show m ++ "." - 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) > maxVal - then error $ "Offset " ++ show n ++ " in operator " ++ name - ++ " is larger than the Int16 maxBound, " ++ show maxVal ++ "." - else s - where maxVal = toInteger (maxBound::Int16) diff --git a/Language/Copilot/Libs/Indexes.hs b/Language/Copilot/Libs/Indexes.hs deleted file mode 100644 --- a/Language/Copilot/Libs/Indexes.hs +++ /dev/null @@ -1,48 +0,0 @@ --- | 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 (id, Int, String, fromIntegral, ($)) -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 (-1) - else mux (f $ drop m s) (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 (-1) - else mux (f $ drop m s) (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 deleted file mode 100644 --- a/Language/Copilot/Libs/LTL.hs +++ /dev/null @@ -1,125 +0,0 @@ --- XXX test until, release --- XXX move the engineLTL example --- XXX fix engine example in ppt slides - --- | Bounded Linear Temporal Logic (LTL) operators. For a bound @n@, a property --- @p@ holds if it holds on the next @n@ transitions (between periods). If @n --- == 0@, then the trace includes only the current period. For example, --- @ --- always 3 p --- @ --- holds if @p@ holds at least once every four periods (3 transitions). --- --- Interface: see Examples/LTLExamples.hs You can embed a LTL specification --- within a Copilot specification using the form: --- @ --- var `ltl` (operator spec) --- @ --- where 'var' is the variable you want to assign to the LTL specification --- you're writing. --- --- For some properties, stream dependencies may not allow their specification. --- In particular, you cannot determine the "future" value of an external --- variable. In general, the ptLTL library is probaby more useful. - -module Language.Copilot.Libs.LTL - ( ltl, eventually, next, always, until, release - ) - where - -import Prelude (Int, ($), String, error) -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 - -ltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams -ltl v f = f v - -tmpName :: Spec Bool -> String -> Spec Bool -tmpName v name = - case v of - Var v' -> varB (v' P.++ "_" P.++ name) - _ -> error $ "Copilot: " P.++ "error in tmpName in LTL.hs." - --- | Property @s@ holds for the next @n@ periods. We require @n >= 0@. If @n == --- 0@, then @s@ holds in the current period. E.g., if @p = always 2 s@, then we --- have the following relationship between the streams generated: --- @ --- 0 1 2 3 4 5 6 7 --- s => T T T F T T T T ... --- p => T F F F T T ... --- @ -always :: Int -> Spec Bool -> Spec Bool -> Streams -always n s v = do - v .= (nPosChk "always" n $ foldl1 (&&) [drop x s' | x <- [0..n]]) - s' .= s - where s' = tmpName v "always" - --- | Property @s@ holds at the next period. For example: --- @ --- 0 1 2 3 4 5 6 7 --- s => F F F T F F T F ... --- next s => F F T F F T F ... --- @ --- Note: s must have sufficient history to drop a value from it. -next :: Spec Bool -> Spec Bool -> Streams -next s v = do - v .= drop 1 s' - s' .= s - where s' = tmpName v "next" - --- | 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 T F F F T ... --- p => F T T T F T T T ... --- @ -eventually :: Int -> Spec Bool -> Spec Bool -> Streams -eventually n s v = do - v .= (nPosChk "eventually" n $ foldl1 (||) [drop x s' | x <- [0..n]]) - s' .= s - where s' = tmpName v "eventually" - --- | @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 -> Streams -until n s0 s1 v = do - v' .= (nPosChk "until" n $ - ( (whenS0 < 0) -- s0 didn't fail within n periods. - || (soonest n s1' <= whenS0))) -- s0 failed at some point before n. - v'' `ltl` eventually n s1' -- guarantees that soonest n s1 >= 0 - v .= v' && v'' - s0' .= s0 - s1' .= s1 - where - s0' = tmpName v "until_0" - s1' = tmpName v "until_1" - v'' = tmpName v "until_2" - v' = tmpName v "until3" - 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 -> Streams -release n s0 s1 v = do - v' .= (nPosChk "release" n $ ( (whenS0 >= 0) -- s0 becomes true at some point - && (whenS0 < whenS1))) -- and when s0 becomes true, - -- is strictly sooner than - -- when s1 fails. - v'' `ltl` always n s1' -- s1 never fails - v .= v' || v'' - s0' .= s0 - s1' .= s1 - where - s0' = tmpName v "release0" - s1' = tmpName v "release1" - v'' = tmpName v "release2" - v' = tmpName v "release3" - whenS1 = soonestFail n s1' - whenS0 = soonest n s0' diff --git a/Language/Copilot/Libs/PTLTL.hs b/Language/Copilot/Libs/PTLTL.hs deleted file mode 100644 --- a/Language/Copilot/Libs/PTLTL.hs +++ /dev/null @@ -1,65 +0,0 @@ --- | Provides past-time linear-temporal logic (ptLTL operators). --- --- Interface: see Examples/PTLTLExamples.hs, particularly function tSinExt2 in --- that file. You can embed a ptLTL specification within a Copilot --- specification using the form: --- @ --- var `ptltl` (operator spec) --- @ --- where 'var' is the variable you want to assign to the ptLTL specification --- you're writing. - -module Language.Copilot.Libs.PTLTL - ( ptltl, since, alwaysBeen, eventuallyPrev, previous ) - where - -import Prelude (String, ($), error) -import qualified Prelude as P - -import Language.Copilot.Core -import Language.Copilot.Language - -tmpName :: Spec Bool -> String -> Spec Bool -tmpName v name = - case v of - Var v' -> varB (v' P.++ "_" P.++ name) - _ -> error "Copilot error in tmpName in PTLTL.hs." - -ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams -ptltl v f = f v - --- | Did @s@ hold in the previous period? -previous :: Spec Bool -> Spec Bool -> Streams -previous s v = v .= [False] ++ s - --- | Has @s@ always held (up to and including the current state)? -alwaysBeen :: Spec Bool -> Spec Bool -> Streams -alwaysBeen s v = do - tmp .= [True] ++ v - v .= tmp && s' - s' .= s - where - tmp = tmpName v "ab_tmp" - s' = tmpName v "ab" - --- | Did @s@ hold at some time in the past (including the current state)? -eventuallyPrev :: Spec Bool -> Spec Bool -> Streams -eventuallyPrev s v = do - tmp .= [False] ++ tmp || s' - v .= s' || tmp - s' .= s - where - tmp = tmpName v "ep_tmp" - s' = tmpName v "ep" - --- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold? -since :: Spec Bool -> Spec Bool -> Spec Bool -> Streams -since s1 s2 v = do - tmp `ptltl` (eventuallyPrev $ [False] ++ s2) -- has s2 been true at some point? - v `ptltl` (alwaysBeen $ tmp ==> s1') - s1' .= s1 - s2' .= s2 - where - tmp = tmpName v "since_tmp" - s1' = tmpName v "since1" - s2' = tmpName v "since2" diff --git a/Language/Copilot/Libs/Statistics.hs b/Language/Copilot/Libs/Statistics.hs deleted file mode 100644 --- a/Language/Copilot/Libs/Statistics.hs +++ /dev/null @@ -1,50 +0,0 @@ --- | 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, meanNow) where - -import Prelude (Int, ($), foldl1, fromIntegral, foldl, error, length) ---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) / (fromIntegral n) - --- | Mean value over the current set of specs passed in. -meanNow :: (Streamable a, A.IntegralE a) => [Spec a] -> Spec a -meanNow [] = error - "Error in majority: list of arguments must be nonempty." -meanNow ls = - (foldl (+) 0 ls) `div` (fromIntegral $ length ls) - - diff --git a/Language/Copilot/Libs/Vote.hs b/Language/Copilot/Libs/Vote.hs deleted file mode 100644 --- a/Language/Copilot/Libs/Vote.hs +++ /dev/null @@ -1,76 +0,0 @@ --- | Voting algorithms over streams of data. - -module Language.Copilot.Libs.Vote - (majority, aMajority, ftAvg) where - -import Prelude - ( ($), fromIntegral, error, length, otherwise - , Bounded(..), maxBound, minBound, Int) -import Data.List (replicate, foldl') -import qualified Prelude as P -import Data.Word - -import Language.Copilot.Language -import Language.Copilot.Core -import qualified Language.Atom as A - --- | Boyer-Moore linear majority algorithm. Warning! Returns an arbitary --- element if no majority is returned. See 'aMajority' below. -majority :: (Streamable a, A.EqE a) => [Spec a] -> Spec a -majority [] = - error "Error in majority: list of arguments must be nonempty." -majority ls = majority' ls (const unit) 0 - -majority' :: (Streamable a, A.EqE a) - => [Spec a] -> Spec a -> Spec Word32 -> Spec a -majority' [] candidate _ = candidate -majority' (x:xs) candidate cnt = - majority' xs (mux (cnt == 0) x candidate) - (mux (cnt == 0 || x == candidate) (cnt + 1) (cnt - 1)) - -aMajority :: (Streamable a, A.EqE a) => [Spec a] -> Spec a -> Spec Bool -aMajority [] _ = - error "Error in aMajority: list of arguments must be nonempty." -aMajority ls candidate = - (foldl' (\cnt x -> mux (x == candidate) - (cnt + 1) - cnt :: Spec Word32 - ) 0 ls - ) * 2 - > (fromIntegral $ length ls) - --- | Fault-tolerant average. Throw away the bottom and top @n@ elements and --- take the average of the rest. Return an error if there are less than @2 * n --- + 1@ elements in the list. -ftAvg :: (Streamable a, A.IntegralE a, Bounded a) => [Spec a] -> Int -> Spec a -ftAvg ls n | length ls P.<= 2 P.* n = - error $ "Error in ftAvg: list of arguments must be at least " - P.++ P.show (2 * n + 1) P.++ "." - | otherwise = (ftAvg' ls (replicate n low) (replicate n high) 0) - `div` (fromIntegral $ length ls P.- (2 P.* n)) - where low = const maxBound - high = const minBound - --- | Return the total sum of values, minus the high and low values. -ftAvg' :: (Streamable a, A.IntegralE a, Bounded a) - => [Spec a] -> [Spec a] -> [Spec a] -> Spec a -> Spec a -ftAvg' [] lows highs sum = foldl' (-) sum (lows P.++ highs) -ftAvg' (x:xs) lows highs sum = - ftAvg' xs (insert (<) lows x) (insert (>) highs x) (sum + x) - --- | Insert an element into an ordered list. --- insert :: (Streamable a, A.OrdE a) --- => (Spec a -> Spec a -> Spec Bool) --- -> [Spec a] -> Spec a -> Int -> [Spec a] --- insert _ xs _ idx | idx P.== length xs = [] --- insert ord xs x idx | otherwise = --- let n = xs !! idx --- choice = mux (x `ord` n) x n in --- choice : insert ord xs choice (idx + 1) -insert :: (Streamable a, A.OrdE a) - => (Spec a -> Spec a -> Spec Bool) - -> [Spec a] -> Spec a -> [Spec a] -insert _ [] _ = [] -insert ord (n:ns) x = - let pred = x `ord` n in - mux pred x n : insert ord ns (mux pred n x) diff --git a/Language/Copilot/PrettyPrinter.hs b/Language/Copilot/PrettyPrinter.hs deleted file mode 100644 --- a/Language/Copilot/PrettyPrinter.hs +++ /dev/null @@ -1,37 +0,0 @@ -{-# 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 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.foldrWithKey showVal "" bm - acc1 = M.foldrWithKey showVal acc0 i8m - acc2 = M.foldrWithKey showVal acc1 i16m - acc3 = M.foldrWithKey showVal acc2 i32m - acc4 = M.foldrWithKey showVal acc3 i64m - acc5 = M.foldrWithKey showVal acc4 w8m - acc6 = M.foldrWithKey showVal acc5 w16m - acc7 = M.foldrWithKey showVal acc6 w32m - acc8 = M.foldrWithKey showVal acc7 w64m - acc9 = M.foldrWithKey showVal acc8 fm - acc10 = M.foldrWithKey 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 (getSpecs s) - - - diff --git a/Language/Copilot/Tests/Random.hs b/Language/Copilot/Tests/Random.hs deleted file mode 100644 --- a/Language/Copilot/Tests/Random.hs +++ /dev/null @@ -1,315 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, GADTs, RankNTypes #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | Generate random specs for testing. We do not generate external array indexes. - -module Language.Copilot.Tests.Random - (randomStreams, Operator(..), Operators, fromOp) where - -import Language.Copilot.Core -import Language.Copilot.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 :: 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.foldrWithKey f acc bm - acc1 = M.foldrWithKey f acc0 i8m - acc2 = M.foldrWithKey f acc1 i16m - acc3 = M.foldrWithKey f acc2 i32m - acc4 = M.foldrWithKey f acc3 i64m - acc5 = M.foldrWithKey f acc4 w8m - acc6 = M.foldrWithKey f acc5 w16m - acc7 = M.foldrWithKey f acc6 w32m - acc8 = M.foldrWithKey f acc7 w64m - acc9 = M.foldrWithKey f acc8 fm - acc10 = M.foldrWithKey f acc9 dm - in acc10 - -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 - _ -> weightsAllSpecSet - (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)) (ExtV v), g1) - (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/README b/README deleted file mode 100644 --- a/README +++ /dev/null @@ -1,235 +0,0 @@ -******************************************************************************* -Overview -******************************************************************************* - -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 - let f = varW64 "f" - let t = varB "t" - f .= [0,1] ++ f + (drop 1 f) - t .= even f - where even :: Spec Word64 -> Spec Bool - even w' = w' `mod` 2 == 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. - -The documentation for the language itself is mainly at - - Copilot/doc/Language-Copilot-Language.html - -and there are numerous examples in - - Copilot/Language/Copilot/Examples - -******************************************************************************* -Download -******************************************************************************* - -Please visit for more information about -installing and using Copilot. - -The page is 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. - - -******************************************************************************* -Release notes -******************************************************************************* - -* Copilot-1.0.2 - * Fixed a major compilation bug. - * Upgraded to GHC 7.0.2 (Haskell Platform). - -* Copilot-1.0.1 - * Removed send operators---use triggers instead (see the distributed voting - * example in VoteExamples.hs. - -* Copilot-1.0 - * Language frozen. - * Added sampling functions and returning arrays. - -* Copilot-0.29 - - * Refactor Language.hs into submodules. - * Removed the notion of phases from sampling. That is a compiler-level - concern. - -* Copilot-0.28 - - * Make triggers part of the Copilot language (see example t5 in Examples.hs). - -* Copilot-0.27 - - * Changed syntax and semantics of the 'send' function (Language.hs) for - sending Copilot values on ports. An example is in Example.hs (grep for - 'send'). - -* Copilot-0.26 - - * Variables are now specs, not strings. This gives stream expressions a type, - so no need for constant functions, monomorphic cast functions, or var - annotations in expressions. Examples updated to reflect the change. - -* Copilot-0.25 - - * Added true, false Specs (Spec Bool) - * Removed generic const -- unneeded, since Spec instantiates Num. - * Change casting to only allow casts that (1) are guaranteed not to change the - sign and (2) are to a larger type. - * Removed libs from Copilot.hs. You must import these explicitly. - * Fixed buts with LTL and ptLTL libraries and examples and added documentation. - -* Copilot-0.24 - - * Fixed a bug in external array analysis for computing the minimum period - size. - * Added the ability to specify a HW clock for Atom. - -* Copilot-0.23 - - * All -Wall warnings removed (from importing Copilot.hs). - * Added support for sampling external array values. (See Examples.hs). - * Fixed a bug in calling CBMC to ensure it unrolls it's loop. Updated - documentation in Help.hs. - * Other minor stylistic changes and fixes. - -* Copilot-0.22: initial release - - -******************************************************************************* -Modifying the Compiler -******************************************************************************* - -This document is intended as a help for whoever wants to hack the internals of -Copilot. It is up-to-date on August 2010, the 17th. - -I will first explain what each module does, then where to look to do some simple -modifications. - -*** Modules *** - -Core : -Defines all the important data-structures. -Especially interestings are : -- Spec, the AST of the streams specifications. - Notice that the operators on streams (F, F2, F3) actually holds functions - that helps interpreting/compiling them -- Streamable, a type class whose instances are all the possible types of output - for a stream -- StreamableMaps, a generic container for holding pairs of key/values, with - values of different types - -Compiler : -Does all the scheduling, and translates a Copilot specification, to an Atom -program. More information on its algorithm can be found in the paper "Copilot: A -Hard Real-Time Runtime Monitor". - -Interpreter : -Provides a small interpreter, mostly for checking the compiler against it. Its -design is very concise, because all the hard scheduling work is done by the -Haskell runtime. The streams are indeed translated to mutually recursives -infinite lists, and the lazyness of Haskell spare us from having to schedule -their computation. There is no specific code for each operator either, as -operators hold the function to be applied to their argument. - -Analyser : -There are several kinds of restrictions on the inputs accepted by Copilot. -Some of them are catched by the Haskell compiler (for example bad typing into -a stream specification), but others aren't : -- Bad typing across stream boundaries -- Specifications which doesn't obey the syntax of Copilot (it could have been - checked by Haskell too, but would have greatly complicated the Spec type) -- All kinds of properties on the dependency graph of the specification. -All these additional restrictions are checked by the Analyser. - -PrettyPrinter : -Just allows to print the structure of a specification - -Tests.Random : -Generates random streams and random input values, for easily checking the -compiler against the interpreter in an automated way. Currently a bit ugly, -would probably have benefited from using the QuickCheck library, rather than the -lower-level Random library. All the parameters of the random generation are near -the top of the file. - -Language : -Defines all the different operators of the language. These are defined through a -F, F2 or F3 constructor, a function on how to compile them, and a function on -how to interpret them. These are also packed in a Operators data structure for -use in the random streams generator. Also contains some monomorphic versions of -the polymorphic language constructs, to help the type inferer. - -AdHocC : -A small number of uninteresting functions to output C code. Used by AtomToC. - -AtomToC : -Adds to the atom-generated code a main function and some initialisation stuff. - -Main : -"Plumbing" module. Makes the analyser/interpreter/compiler, atom, gcc, and the -generated C program interact. Takes its arguments in a very heavy format (not -very convenient for fast testing). Warning : it is rather easy to desynchronyze -the generated C program and the interpreter with very small modifications -(leading to strange bugs). - -Interface : -Is a wrapper around Main. Writing its argument is usually much easier, thanks -to the provided combinators and the reasonable defaults. All it does is -translating those into the numerous and verbose arguments Main expects. - -Libs.* : -As Copilot is embedded in Haskell, it is very easy to write libraries of "macros" -that simplify the writing of some specifications. Thus these files, that holds -for example functions for easily writing LTL and PTLTL formulas. - -Examples.* : -Self-explanatory. - -*** Simple modifications *** - -Add an example : -In Examples.Examples, or if related to a library, in Examples.LibraryName - -Add some high-level combinator on streams : -In a library, in Lib.* -Should not call Atom, should only use other combinators and base operators. - -Add some operator in the base language : -Write in Language.hs, from F, F2 or F3 (see examples) Would be nice to also add -to the corresponding Operators set (opsF, opsF2 or opsF3), so that it could be -automatically checked. This last point obviously require that the interpreted -and compiled semantics are equivalents. - -Add some possible types for the streams : -Add a new instance of Stremable in Core.hs -Add a new record to StreamableMaps in Core.hs -Update foldStreamableMaps, mapStreamableMaps, mapStreamableMapsM, -and filterStreamableMaps in Core.hs -Update foldRandomableMaps in Tests/Random.hs - -Authorise a new type to be exchanged by monitors : -Add a new instance of Sendable in Core.hs -Update foldSendableMaps in Core.hs - -Add a new option to Copilot : -Add a new field to the Options record in Interface.hs -Add a new combinator for that field in Interface.hs -Update the baseOptions in Interface.hs -Implement it (probably in Main.hs). -Update interface in Interface.hs to convey it to the Main. - diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,88 @@ +Copilot: a stream DSL +==================================== +Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in +Haskell that compiles into embedded C. Copilot is similar in spirit to +languages like Lustre. Copilot contains an interpreter, multiple back-end +compilers, and other verification tools. + +Resources +========= +Copilot is comprised of a number of sub-projects which are automatically +installed when you install Copilot from Hackage, as described below: + +* [copilot-language](http://hackage.haskell.org/package/copilot-language) The + front-end of Copilot defining the user language. + +* [copilot-libraries](http://hackage.haskell.org/package/copilot-libraries) + User-supplied libraries for Copilot, including linear-temporal logic, + fault-tolerant voting, regular expressions, etc. + +* [copilot-core](http://hackage.haskell.org/package/copilot-core) The core + language, which efficiently represents Copilot expressions. The core is only + of interest to implementers wishing to add a new back-end to Copilot. + +* [copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) A tool to + generate a driver using CBMC, a third-party tool (see Dependencies below) that + proves that the code generated by different C back-ends is equivalent. + Currently, this includes the C99 back-end and the SBV back-end. + +* [copilot-c99](http://hackage.haskell.org/package/copilot-c99) A back-end that + translates to [Atom](http://hackage.haskell.org/package/copilot-cbmc) to + generate hard real-time C code. + +Optionally, you may which also to install + +* [copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) Another back-end + that translates to [SBV](http://hackage.haskell.org/package/sbv), using its + code generator to generate hard real-time C code as well. The ad + +* [copilot-discussion](https://github.com/niswegmann/copilot-discussion) + Contains a tutorial, todos, and other items regarding the Copilot system. + +**Sources** for each package are available on Github as well. Just go to +[Github](github.com) and search for the package of interest. Feel free to fork! + +Comments, bug reports, and patches are always welcome. Send them to leepike @ +gmail.com + +Examples +========= +Please see the files under the Examples directory for a number of examples +showing the syntax, use of libraries, and use of the interpreter and back-ends. +The examples is the best way to start. + +Installation +============ +The Copilot library is cabalized. Assuming you have cabal and the GHC compiler +installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the +easiest way to obtain these), it should merely be a matter of running + + cabal install copilot + +with an Internet connection. Please see the INSTALL file for installation +details. + +Once the installation is done, you can run the executable `XXX` which will +execute the regression test suite for sbv on your machine. + +Dependencies +============= +copilot-cbmc depends on the C model-checker, CBMC. +[CBMC](http://www.cprover.org/cbmc/) is a bounded model-checker for C code. We +use CBMC to prove that two back-ends generating C generate semantically +equivalent C, to help detect bugs in C back-ends. + +Copyright, License +================== +Copilot is distributed with the BSD3 license. The license file contains the +[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage. + +Thanks +====== +Copilot was developed, in part, with support from NASA's Aviation Safety +Program, Contract #NNL08AD13T. Copilot was developed jointly by Galois, +Inc. and the National Institute of Aerospace. + +The following people have contributed to Copilot: Lee Pike, Nis Wegmann, +Sebastian Niller, Robin Morisset, Alwyn Goodloe, and Levent Erkok. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,11 @@ +import Distribution.Simple +import System.Exit (exitWith, ExitCode(..)) + +main :: IO () +main = defaultMainWithHooks simpleUserHooks{ postInst = msg } + where + msg _ _ _ _ = do + putStrLn "Execute \"/.cabal/bin/copilot-regression\" to run some very simple tests to ensure your installation built correctly." + putStrLn "To QuickCheck the Atom backend, execute \"/.cabal/bin/copilot-c99-qc .\"" + exitWith ExitSuccess + diff --git a/Setup.lhs b/Setup.lhs deleted file mode 100644 --- a/Setup.lhs +++ /dev/null @@ -1,8 +0,0 @@ -#! /usr/bin/env runhaskell - -> module Main (main) where -> -> import Distribution.Simple (defaultMain) -> -> main :: IO () -> main = defaultMain diff --git a/Tests/Test.hs b/Tests/Test.hs new file mode 100644 --- /dev/null +++ b/Tests/Test.hs @@ -0,0 +1,127 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | A very small test suite to check for basic functionality. + +{-# LANGUAGE RebindableSyntax #-} + +module Main where + +import qualified Prelude as P +import Language.Copilot hiding (even, odd) +import Copilot.Compile.C99 + +import System.Directory (removeFile) +-------------------------------------------------------------------------------- + +-- +-- Some utility functions: +-- + +flipflop :: Stream Bool -> Stream Bool +flipflop x = y + where + y = [False] ++ if x then not y else y + +nats :: Stream Word64 +nats = [0] ++ nats + 1 + +even :: (P.Integral a, Typed a) => Stream a -> Stream Bool +even x = x `mod` 2 == 0 + +odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool +odd = not . even + +counter :: (Num a, Typed a) => Stream Bool -> Stream a +counter reset = y + where + zy = [0] ++ y + y = if reset then 0 else zy + 1 + +booleans :: Stream Bool +booleans = [True, True, False] ++ booleans + +fib :: Stream Word64 +fib = [1, 1] ++ fib + drop 1 fib + +bitWise :: Stream Word8 +bitWise = ( let a = [ 1, 1, 0 ] ++ a in a ) + .^. + ( let b = [ 0, 1, 1 ] ++ b in b ) + +sumExterns :: Stream Word64 +sumExterns = + let + ex1 = extern "e1" + ex2 = extern "e2" + in + ex1 + ex2 + +-------------------------------------------------------------------------------- + +-- +-- An example of a complete copilot specification. + + +-- A specification: +spec :: Spec +spec = + do + -- A trigger with four arguments: + trigger "e" booleans + [ arg fib, arg nats, arg sumExterns, arg bitWise ] + + -- A trigger with two arguments: + trigger "f" booleans + [ arg fib, arg sumExterns ] + + -- A trigger with a single argument: + trigger "g" (flipflop booleans) + [ arg (sumExterns + counter false + 25) ] + + -- A trigger with a single argument (should never fire): + trigger "h" (extern "e3" /= fib) + [ arg (0 :: Stream Int8) ] + + observer "i" (odd nats) + +--- Some infinite lists for simulating external variables: +e1, e2, e3 :: [Word64] +e1 = [0..] +e2 = 5 : 4 : e2 +e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3) + +main :: IO () +main = do + putStrLn "PrettyPrinter:" + putStrLn "" + prettyPrint spec + putStrLn "" + putStrLn "" + putStrLn "Interpreter:" + putStrLn "" + interpret 10 [var "e1" e1, var "e2" e2, var "e3" e3] spec + putStrLn "" + putStrLn "" + putStrLn "Atom compilation:" + reify spec >>= compile defaultParams + cleanUp + putStrLn "*********************************" + putStrLn " Ok, things seem to work. Enjoy!" + putStrLn "*********************************" + + -- Don't assume SBV is installed. + -- putStrLn "Check equivalence:" + -- putStrLn "" + -- putStrLn "" + -- reify spec >>= + -- C.genCBMC C.defaultParams {C.numIterations = 20} + +-------------------------------------------------------------------------------- + +cleanUp :: IO () +cleanUp = do + removeFile "copilot.c" + removeFile "copilot.h" + return () diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,79 +1,49 @@ name: copilot -version: 1.0.2 -cabal-version: >= 1.6 +version: 2.0 +cabal-version: >= 1.10 license: BSD3 license-file: LICENSE -author: Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller -synopsis: A stream DSL for writing embedded C monitors. +author: Nis Nordby Wegmann, Lee Pike, Robin Morisset, Sebastian Niller, Alwyn Goodloe +synopsis: A stream DSL for writing embedded C programs. build-type: Simple maintainer: Lee Pike category: Language, Embedded 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 - > let f = varW64 "fib" - > let t = varB "t" - > f .= [0,1] ++ f + (drop 1 f) - > t .= even f - > where even :: Spec Word64 -> Spec Bool - > even w' = w' `mod` 2 == 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. +stability: Experimental +description: Documentation is available at the website, and see the included examples. -extra-source-files: README +extra-source-files: README.md source-repository head type: git location: git://github.com/leepike/Copilot.git library - ghc-options: -Wall - -- These build depends represent my current system. This will probably - -- build on packages outside these constraints. - build-depends: - base >= 4.0 && < 6 - , atom >= 1.0.8 - , containers >= 0.2.0.1 - , process >= 1.0.0.0 - , random >= 1.0.0.0 - , directory >= 1.0.0.0 - , mtl >= 1.0.0.0 - , filepath >= 1.0.0.0 - - extensions: + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: + -Wall + -fwarn-tabs + -auto-all + -caf-all + -fno-warn-orphans + build-depends: + base >= 4.0 && <5 + , copilot-core + , copilot-language + , copilot-libraries + , copilot-cbmc exposed-modules: Language.Copilot - Language.Copilot.AdHocC - Language.Copilot.Core - Language.Copilot.Language - Language.Copilot.Language.Sampling - Language.Copilot.Language.FunctionCalls - Language.Copilot.Language.RandomOps - Language.Copilot.Language.Casting - 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.Libs.ErrorChks - Language.Copilot.Libs.PTLTL - Language.Copilot.Libs.LTL - Language.Copilot.Libs.Indexes - Language.Copilot.Libs.Statistics - Language.Copilot.Libs.Vote - Language.Copilot.Examples.Examples - Language.Copilot.Examples.LTLExamples - Language.Copilot.Examples.PTLTLExamples - Language.Copilot.Examples.StatExamples + +executable copilot-regression + default-language : Haskell2010 + hs-source-dirs : Tests, src + ghc-options : -Wall -fwarn-tabs + main-is : Test.hs + build-depends: + base >= 4.0 + , copilot-core + , copilot-language + , copilot-libraries + , copilot-c99 + , directory >= 1.1 diff --git a/src/Language/Copilot.hs b/src/Language/Copilot.hs new file mode 100644 --- /dev/null +++ b/src/Language/Copilot.hs @@ -0,0 +1,39 @@ +module Language.Copilot + ( + module Copilot.Language + , module Copilot.Language.Prelude + , module Copilot.Language.Reify + + -- Code generators + -- , module Copilot.Compile.C99 + -- , module Copilot.Compile.SBV + + -- Libraries + , module Copilot.Library.Clocks + , module Copilot.Library.LTL + , module Copilot.Library.PTLTL + , module Copilot.Library.Statistics + , module Copilot.Library.RegExp + , module Copilot.Library.Utils + , module Copilot.Library.Voting + , module Copilot.Library.Stacks + ) where + +import Copilot.Language +import Copilot.Language.Prelude +import Copilot.Language.Reify + +-- Code generators +-- import Copilot.Compile.C99 +-- import Copilot.Compile.SBV + +-- Libraries +import Copilot.Library.Clocks +import Copilot.Library.LTL +import Copilot.Library.PTLTL +import Copilot.Library.Statistics +import Copilot.Library.RegExp +import Copilot.Library.Utils +import Copilot.Library.Voting +import Copilot.Library.Stacks +