copilot 1.0 → 1.0.1
raw patch · 16 files changed
+625/−289 lines, 16 filesdep ~base
Dependency ranges changed: base
Files
- Language/Copilot/Analyser.hs +117/−36
- Language/Copilot/AtomToC.hs +41/−45
- Language/Copilot/Compiler.hs +162/−67
- Language/Copilot/Core.hs +7/−6
- Language/Copilot/Dispatch.hs +27/−25
- Language/Copilot/Examples/Examples.hs +91/−21
- Language/Copilot/Examples/PTLTLExamples.hs +30/−24
- Language/Copilot/Examples/StatExamples.hs +0/−2
- Language/Copilot/Help.hs +28/−28
- Language/Copilot/Interface.hs +16/−11
- Language/Copilot/Interpreter.hs +2/−4
- Language/Copilot/Language.hs +1/−1
- Language/Copilot/Language/Sampling.hs +11/−11
- Language/Copilot/Libs/Statistics.hs +11/−4
- Language/Copilot/Libs/Vote.hs +76/−0
- copilot.cabal +5/−4
Language/Copilot/Analyser.hs view
@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -XRelaxedPolyRec #-}+{-# LANGUAGE RelaxedPolyRec #-} -- | This module provides a way to check that a /Copilot/ specification is -- compilable@@ -16,6 +16,7 @@ import Language.Copilot.Core import Data.List+import Data.Maybe(mapMaybe) type Weight = Int @@ -23,17 +24,11 @@ data Error = BadSyntax String Var -- ^ the BNF is not respected | BadDrop Int Var -- ^ A drop expression of less than 0 is used- -- | BadSamplingPhase Var Ext -- ^ if an external variable is sampled at phase- -- -- 0 then there is no time for the stream to be- -- -- updated- -- | BadSamplingArrPhase Var Ext -- ^ if an external variable is sampled at- -- -- phase 0 then there is no time for the- -- -- stream to be updated | BadPArrSpec Var Ext String -- ^ External array indexes can only take -- variables or constants as indexes.- | BadType Var Var -- ^ either a variable is not defined, or not with the- -- good type ; there is no implicit conversion of types in- -- /Copilot/+ | 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/@@ -50,6 +45,9 @@ | 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) =@@ -62,18 +60,6 @@ "of elements.\n" , show i ++ " is negative, and Drop only accepts positive arguments.\n" ]- -- show (BadSamplingPhase v v' ph) =- -- unlines- -- [ "Error : the external variable " ++ show v' ++ " is sampled at phase " ++ - -- show ph ++ " in the stream " ++ v ++ "." - -- , "Sampling can only occur from phase 1 onwards.\n"- -- ]- -- show (BadSamplingArrPhase v arr ph) =- -- unlines- -- [ "Error : the external array " ++ show arr ++ " is sampled at phase " ++ - -- show ph ++ " in the stream " ++ v ++ "."- -- , " Sampling can only occur from phase 1 onwards.\n"- -- ] show (BadPArrSpec v arr idx) = unlines [ "Error : the index into an external array can only take a "@@ -84,7 +70,7 @@ ] show (BadType v v') = unlines- [ "Error : the monitor variable " ++ v ++ ", called in the stream " + [ "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"@@ -127,6 +113,11 @@ ++ "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' =@@ -145,18 +136,18 @@ -- | Check a /Copilot/ specification. -- If it is not compilable, then returns an error describing the issue.--- Else, returns @Nothing@+-- Else, returns @Nothing@. check :: StreamableMaps Spec -> Maybe Error check streams =- syntaxCheck streams &&> defCheck 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 | PArrSet - deriving Eq+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.+-- 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 =@@ -169,10 +160,16 @@ case s of Var _ -> Nothing Const _ -> Nothing- PVar _ _ -> Nothing -- ph > 0 ||> BadSamplingPhase v v' ph+ PVar _ _ -> Nothing -- checkSampling s0 PArr _ (arr,s0) -> checkIndex v arr s0 --- &&> ph > 0 ||> BadSamplingArrPhase v arr ph - &&> checkSyntaxSpec PArrSet v s0 Nothing+-- 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 @@ -189,7 +186,20 @@ 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 =@@ -248,12 +258,16 @@ getExternalVars streams = nub $ foldStreamableMaps decl streams [] where- decl :: Streamable a - => Var -> Spec a -> [Exs] -> [Exs]+ 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 (show s0)) : 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 @@ -262,6 +276,73 @@ 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) {-
Language/Copilot/AtomToC.hs view
@@ -3,21 +3,28 @@ -- | Defines a main() and print statements to easily execute generated Copilot specs. module Language.Copilot.AtomToC(getPrePostCode) where -import Language.Copilot.Compiler (tmpSampleStr, tmpArrName, tmpVarName) 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 :: Name -> StreamableMaps Spec -> [Exs] - -> [(Ext,Int)] -> Vars -> Period -> (String, String)-getPrePostCode cName streams allExts arrDecs inputExts p =- (preCode $ extDecls allExts arrDecs, postCode cName streams allExts inputExts p)+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]@@ -43,19 +50,35 @@ [ includeBracket "stdio.h" , includeBracket "stdlib.h" , includeBracket "string.h"- , includeBracket "inttypes.h"+-- , includeBracket "inttypes.h" , "" , "unsigned long long rnd;" ] ++ extDeclarations- -postCode :: Name -> StreamableMaps Spec -> [Exs] -> Vars -> Period -> String-postCode cName streams allExts inputExts p = ++-- | 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)- +++ then []+ else cleanString)+ ++ -- make a loop to complete a period of computation. [ "int main(int argc, char *argv[]) {" , " if (argc != 2) {" , " " ++ printfNewline @@ -64,27 +87,14 @@ , " return 1;" , " }" , " rnd = atoi(argv[1]);"- ]- ++- inputExtVars inputExts " "- ++- sampleExtVars allExts cName- ++- [ " int i = 0;"- , " for(; i < rnd ; i++) {"- ]- ++- inputExtVars inputExts " "- ++- [ " int j = 0;"- , " for (; j < " ++ show p ++ " ; j++) {"- , " " ++ cName ++ "();"- , " }"+ , " int i;"+ , " for(i = 0; i < rnd ; i++) {" , " " ++ printf "period: %i " ["i"] ]- ++- outputVars cName streams - +++ ++ inputExtVars inputExts " "+ ++ [" " ++ tmpCFileName cName ++ "();"]+ ++ outputVars cName streams + ++ [ " " ++ printfNewline "" [] , " fflush(stdout);" , " }"@@ -118,20 +128,6 @@ (indent ++ "sscanf (" ++ string ++ ", \"" ++ typeId (head l) ++ "\", &" ++ v ++ ");") : (indent ++ "clean (" ++ string ++ ", stdin);") : ls--sampleExtVars :: [Exs] -> Name -> [String]-sampleExtVars allExts cName =- map (\ext -> let (v,e) = sample ext in- " " ++ vPre cName ++ tmpSampleStr ++ (normalizeVar e)- ++ " = " ++ v ++ ";") - allExts- where - sample :: Exs -> (Var, String)- sample (_, v, ExtRetV) = ( case v of - ExtV var -> var- Fun fname args -> funcShow cName fname args- , tmpVarName v)- sample (_, v, ExtRetA idx) = (show v ++ "[0]", tmpArrName v idx) outputVars :: Name -> StreamableMaps Spec -> [String] outputVars cName streams =
Language/Copilot/Compiler.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE ScopedTypeVariables, Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables, Rank2Types, GADTs #-} -- XXX Clean this up! @@ -12,7 +12,7 @@ import Data.Maybe import qualified Data.Map as M import Data.List-import Data.Word (Word64)+import Data.Word (Word32) import qualified Language.Atom as A @@ -29,8 +29,13 @@ (\_ -> 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 p' streams outputs prophArrs tmpSamples + foldStreamableMaps (makeRule nextStates outputs prophArrs updateIndexes outputIndexes) streams (return ()) @@ -46,12 +51,14 @@ -- where -- optP = getOptimalPeriod streams sends --- | For period of length n:--- Phase 0: state update.--- Phase 1: Compute output variables.--- Phase 2 - n-2: send values (if any).--- Phase 2 - n-2: Sample external vars (if any).--- Phase n-1: update indexes.++-- | 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 3: send values (if any).+-- Phase 4 up to n: update indexes. period :: Maybe Int -> Int period p = case p of@@ -61,10 +68,10 @@ else error $ "Copilot error: the period is too short, " ++ "it should be at least " ++ show minPeriod ++ " ticks." where minPeriod :: Int- minPeriod = 4+ minPeriod = 5 -- For the prophecy arrays-type ArrIndex = Word64+type ArrIndex = Word32 type ProphArrs = StreamableMaps BoundedArray type Outputs = StreamableMaps A.V type Indexes = M.Map Var (A.V ArrIndex)@@ -74,14 +81,98 @@ data BoundedArray a = B ArrIndex (Maybe (A.A a)) -nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes - -> Spec a -> ArrIndex -> A.E a-nextSt streams prophArrs tmpSamples outputIndexes s index = +-- nextSt :: Streamable a => StreamableMaps Spec -> ProphArrs -> TmpSamples -> Indexes +-- -> Spec a -> ArrIndex -> A.E a+-- nextSt streams prophArrs tmpSamples outputIndexes s index = +-- case s of+-- PVar _ v -> +-- let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in+-- A.value var+-- PArr _ (v, idx) -> +-- 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 -> A.Const e+-- F _ f s0 -> f $ next s0 index +-- F2 _ f s0 s1 -> +-- f (next s0 index) +-- (next s1 index)+-- F3 _ f s0 s1 s2 -> +-- f (next s0 index) +-- (next s1 index) +-- (next s2 index)+-- Append _ s0 -> next s0 index+-- Drop i s0 -> next s0 (fromInteger (toInteger i) + index)+-- where next :: Streamable b => Spec b -> ArrIndex -> A.E b+-- next = nextSt streams prophArrs tmpSamples outputIndexes++-- 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 +-- nextSt streams prophArrs tmpSamples outputIndexes s0 (index - initLen)+-- where getVar :: Streamable a => Var -> ArrIndex -> Maybe (A.A a) -> A.E a+-- getVar v initLen maybeArr =+-- let outputIndex = case M.lookup v outputIndexes of+-- Nothing -> error "Error in function getVar."+-- Just x -> x+-- arr = case maybeArr of+-- Nothing -> error "Error in function getVar (maybeArr)."+-- Just x -> x in +-- arr A.!. ((A.Const index + A.VRef outputIndex) `A.mod_` +-- (A.Const (initLen + 1)))+++-- | 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 -> + PVar _ v -> ExpLeaf $ let PhV var = getElem (tmpVarName v) (tmpVars tmpSamples) in A.value var- PArr _ (v, idx) -> + PArr _ (v, idx) -> ExpLeaf $ let PhA var = e tmp (tmpArrs tmpSamples) tmp = tmpArrName v (show idx) e a b = case getMaybeElem a b of@@ -89,34 +180,39 @@ error "Error in application of getElem in nextSt." Just x -> x in A.value var- Var v -> let B initLen maybeArr = getElem v prophArrs in- -- This check is extremely important- -- It means that if x at time n depends on y at time n- -- 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 - next s0 (index - initLen)- Const e -> A.Const e- F _ f s0 -> f $ next s0 index- F2 _ f s0 s1 ->- f (next s0 index) - (next s1 index)- F3 _ f s0 s1 s2 ->- f (next s0 index) - (next s1 index) - (next s2 index)+ 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 -> A.E b- next = nextSt streams prophArrs tmpSamples outputIndexes - getVar :: Streamable a - => Var -> ArrIndex -> Maybe (A.A a) -> A.E a- getVar v initLen maybeArr =- let outputIndex = case M.lookup v outputIndexes of+ 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@@ -125,7 +221,8 @@ 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 :: forall a. Streamable a + => Var -> Spec a -> A.Atom (BoundedArray a) initProphArr v s = let states = initState s name = "prophVal__" ++ normalizeVar v@@ -220,66 +317,64 @@ => 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+ 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+ do mindexes <- indexes index <- atomConstructor ("outputIndex__" ++ normalizeVar v) 0 return $ M.insert v index mindexes +-- where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0 makeRule :: forall a. Streamable a => - Period -> StreamableMaps Spec -> Outputs -> ProphArrs -> TmpSamples -> - Indexes -> Indexes -> Var -> Spec a -> A.Atom () -> A.Atom ()-makeRule p streams outputs prophArrs tmpSamples updateIndexes outputIndexes v s r = do+ 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 0 $ A.atom ("updateOutput__" ++ normalizeVar v) $ do- ((getElem v outputs)::(A.V a)) A.<== nextSt'+ A.exactPhase 2 $ 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 0 $ A.atom ("update__" ++ normalizeVar v) $ do- arr A.! (A.VRef updateIndex) A.<== nextSt'+ A.exactPhase 1 $ A.atom ("update__" ++ normalizeVar v) $ do+ arr A.! (A.VRef updateIndex) A.<== getElem v exps - A.exactPhase 1 $ A.atom ("output__" ++ normalizeVar v) $ do+ 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) - -- XXX For now, we put these all in the last phase. We want better- -- distribution though at some point.- A.phase (p - 1)+ A.phase 4 $ A.atom ("incrUpdateIndex__" ++ normalizeVar v) $ do updateIndex A.<== (A.VRef updateIndex + A.Const 1) `A.mod_` A.Const (n + 1)-- where nextSt' = nextSt streams prophArrs tmpSamples outputIndexes s 0 --- Do sends in phase 2. makeSend :: forall a. Streamable a => Outputs -> String -> Send a -> A.Atom () -> A.Atom () makeSend outputs name (Send v port portName) r = do r - A.exactPhase 2 $ A.atom ("__send_" ++ name) $+ A.exactPhase 3 $ A.atom ("__send_" ++ name) $ mkSend (A.value $ getElem (getMaybeVar v) outputs :: A.E a) port portName@@ -313,7 +408,7 @@ Nothing -> error $ "Copilot error: variable " ++ v' ++ " was not defined!." Just (PhV var') -> PhV var' in- (v', A.exactPhase minSampPh $ + (v', A.exactPhase 0 $ A.atom (sampleStr ++ normalizeVar v') $ var A.<== (A.value $ externalAtomConstructor $ getSampleFuncVar v) ) : a@@ -324,7 +419,7 @@ case getMaybeElem arr' (tmpArrs ts) :: Maybe (PhasedValueArr a) of Nothing -> error "Error in fucntion sampleExts." Just x -> x in- (arr', A.exactPhase minSampPh $ + (arr', A.exactPhase 0 $ A.atom (sampleStr ++ normalizeVar arr') $ arrV A.<== A.array' (getSampleFuncVar arr) (atomType (unit::a)) A.!. i@@ -335,8 +430,8 @@ sampleExts' s2 a Append _ s0 -> sampleExts' s0 a Drop _ s0 -> sampleExts' s0 a- where minSampPh :: Int- minSampPh = 2+ where -- minSampPh :: Int+ --minSampPh = 2 sampleExts' s' a' = sampleExts outputs ts cFileName s' a' getSampleFuncVar v = case v of ExtV extV -> extV@@ -364,7 +459,7 @@ makeTrigger :: Outputs -> Name -> Trigger -> A.Atom () -> A.Atom () makeTrigger outputs cFileName trigger@(Trigger s fnName args) r = do r - (A.exactPhase 2 $ A.atom (show trigger) $ + (A.exactPhase 3 $ A.atom (show trigger) $ do A.cond (getOutput outputs s) fnCall cFileName fnName args)
Language/Copilot/Core.hs view
@@ -49,7 +49,7 @@ Var :: Streamable a => Var -> Spec a Const :: Streamable a => a -> Spec a - PVar :: Streamable a => A.Type -> Ext -> 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 @@ -98,19 +98,20 @@ -- 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 String+ | ExtRetA ArgConstVar deriving Eq--instance Show Ext where- show (ExtV v) = v- show (Fun f args) = normalizeVar f ++ show args -- | For calling a function with Atom variables. funcShow :: Name -> String -> Args -> String
Language/Copilot/Dispatch.hs view
@@ -33,13 +33,14 @@ , interpreted :: Interpreted -- ^ Interpret the program or not , outputDir :: String -- ^ Where to put the executable , compiler :: String -- ^ Which compiler to use- , prePostCode :: Maybe (String, String) -- ^ Code to replace the default- -- initialization and main+ , 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."+ -- size allows them to be declared. , clock :: Maybe A.Clock -- Use the hardware clock to drive the timing -- of the program. }@@ -72,7 +73,7 @@ mapM_ putStrLn preludeText isValid <- case check (strms elems) of- Just x -> putStrLn (show x) >> return False+ Just x -> print x >> return False Nothing -> return True when isValid $ -- because haskell is lazy, will only get computed if later used@@ -81,7 +82,7 @@ in case backEnd of Interpreter -> do- when (not allInputsPresents) $ error errMsg+ unless allInputsPresents $ error errMsg mapM_ putStrLn interpretedLines Opts opts -> let isInterpreted =@@ -99,15 +100,15 @@ let delete ext = do f0 <- canonicalizePath (cName opts ++ ext) f1 <- canonicalizePath (dirName ++ cName opts ++ ext)- if f0 == f1 then return ()- else removeFile (cName opts ++ ext)+ 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 (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) @@ -127,12 +128,15 @@ let cFileName = cName opts (p', program) = copilotToAtom elems (getPeriod opts) cFileName (preCode, postCode) = - 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)+ 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@@ -143,11 +147,10 @@ in do putStrLn $ "Compiling Copilot specs to C ..." (sched, _, _, _, _) <- A.compile cFileName atomConfig program- if isVerbose- then putStrLn $ A.reportSchedule sched- else return ()+ 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@@ -157,8 +160,9 @@ programName = cName opts in do- let command = (compiler opts) ++ " " ++ dirName ++ cName opts ++ ".c" ++ " -o " - ++ dirName ++ programName ++ " " ++ gccOpts opts+ let command = compiler opts ++ " " ++ dirName ++ cName opts + ++ ".c" ++ " -o " ++ dirName ++ programName + ++ " " ++ gccOpts opts putStrLn "Calling the C compiler ..." putStrLn command _ <- system command@@ -172,10 +176,9 @@ when isInterpreted (do putStrLn "\n *** Checking the randomly-generated Copilot specification: ***\n"- putStrLn $ show streams)+ print streams) let inputVar v (val:vals) ioVars =- do- hPutStr hin (showAsC val ++ " \n")+ do hPutStr hin (showAsC val ++ " \n") hFlush hin vars <- ioVars return $ updateSubMap (\m -> M.insert v vals m) vars@@ -184,11 +187,10 @@ executePeriod _ [] _ = error "Impossible : empty ExecutePeriod" executePeriod inputExts (inLine:inLines) n = when (n > 0) $ - do- nextInputExts <- foldStreamableMaps inputVar inputExts (return emptySM)+ do nextInputExts <- foldStreamableMaps inputVar inputExts (return emptySM) line <- hGetLine hout let nextPeriod = - (when (not isSilent) $ putStrLn line) >> + (unless isSilent $ putStrLn line) >> executePeriod nextInputExts inLines (n - 1) -- Checking the compiler and interpreter. if isInterpreted
Language/Copilot/Examples/Examples.hs view
@@ -9,7 +9,7 @@ -- for specifying options import Data.Map (fromList) -import Data.Maybe (Maybe (..))+--import Data.Maybe (Maybe (..)) --import System.Random import Language.Copilot @@ -103,22 +103,7 @@ trigger w "z0_trigger" (a <> b <> true) trigger w "z1_trigger" (d <> constW16 3 <> w) --- If the temperature rises more than 2.3 degrees within 0.2 seconds, then the--- engine is immediately shut off. From the paper.-engine :: Streams-engine = do- -- external vars- let temp = extF "temp"- shutoff = extB "shutoff"- -- Copilot vars- temps = varF "temps"- overTemp = varB "overTemp"- err = varB "trigger" - temps .= [0, 0, 0] ++ temp- overTemp .= drop 2 temps > 2.3 + temps- err .= overTemp ==> shutoff- -- | Sending over ports. distrib :: Streams distrib = do@@ -132,6 +117,17 @@ send "portA" (port 2) a send "portB" (port 1) 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@@ -174,25 +170,28 @@ testCoercions :: Streams testCoercions = do let word = varW8 "word"+ int = varI16 "int" word .= [1] ++ word * (-2)- let int = varI16 "int" int .= 1 + cast word testCoercions2 :: Streams testCoercions2 = do let b = varB "b"+ i = varI16 "i"+ j = varI16 "j" b .= [True] ++ not b- let i = varI16 "i"- let j = varI16 "j" i .= cast j j .= 3 testCoercions3 :: Streams testCoercions3 = do let x = varB "x"- x .= [True] ++ not x- let y = varI32 "y"+ 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 @@ -285,6 +284,77 @@ 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
Language/Copilot/Examples/PTLTLExamples.hs view
@@ -6,8 +6,9 @@ import qualified Prelude as P import Data.Map (fromList) -import Language.Copilot+import Language.Copilot hiding (check) import Language.Copilot.Libs.PTLTL+import Language.Copilot.Libs.Vote -- Next examples are for testing of the ptLTL library @@ -91,36 +92,41 @@ t `ptltl` (alwaysBeen $ not a) e .= e1 ==> d --- "If the engine temperature exeeds 250 degrees, then the engine is shutoff--- within the next 10 periods, and in the period following the shutoff, the--- cooler is engaged and remains engaged."+-- "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 engineTemp = extW8 "engineTemp"- engineOff = extB "engineOff"- coolerOn = extB "coolerOn"+ let t0 = extW8 "temp_probe_0"+ t1 = extW8 "temp_probe_1"+ t2 = extW8 "temp_probe_2"+ cooler = extB "fan_status" -- Copilot vars- cnt = varW8 "cnt"- temp = varB "temp"- cooler = varB "cooler"- off = varB "off"- monitor = varB "monitor"+ 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 - temp `ptltl` (alwaysBeen (engineTemp > 250))- cnt .= [0] ++ mux (temp && cnt < 10) (cnt + 1) cnt- off .= cnt >= 10 ==> engineOff- cooler `ptltl` (coolerOn `since` engineOff)- monitor .= off && cooler -engineRun :: IO ()-engineRun = +engineRun :: Bool -> IO ()+engineRun b = if b then interpret engine 40 $ - setE (emptySM { bMap = fromList - [ ("engineOff", replicate 8 False P.++ repeat True)- , ("coolerOn", replicate 9 False P.++ repeat True)- ]- , w8Map = fromList [("engineTemp", [99,100..])]+ 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
Language/Copilot/Examples/StatExamples.hs view
@@ -3,8 +3,6 @@ import Prelude () import Language.Copilot.Core import Language.Copilot.Language-import Language.Copilot.Interface-import Language.Copilot.PrettyPrinter import Language.Copilot.Libs.Statistics t0 :: Streams
Language/Copilot/Help.hs view
@@ -50,9 +50,9 @@ , " (NaN), and that no uninitialized local variables are used. The entry" , " point of main() is assumed, and it is also assumed that main() can be" , " unrolled at least n times, where n is an Int. This command is thus"- , " best used when generating a simulation program (i.e., the setPP flag"- , " is not used when compiling). For more information on the properties" - , " checked, see <http://www.cprover.org/cprover-manual/properties.shtml>."+ , " best used when generating a simulation program (see the setSim option)." + , " For more information on the properties checked, see"+ , " <http://www.cprover.org/cprover-manual/properties.shtml>." , "" , " > help " , " Displays this help message."@@ -106,39 +106,39 @@ , " is returned if the number is too small. For any program, the number" , " of ticks must be at least 2." , ""- , " setPP :: (String, String) -> Options -> Options (c)"- , " default: Nothing. The default generates a main() function that calls"- , " Copilot code to run simulations."+ , " setR :: Int -> Options -> Options (t)"+ , " default: 0"+ , " Sets the seed for generating random Copilot specification during"+ , " testing." , ""- , " Sets C code to pretty-print before and after the generated Copilot"- , " code: the before code is the first element of the tuple and the after"- , " code is the second element. For writing ad-hoc C, please see"+ , " 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. ('PP' stands for 'pretty-print'.)" - , ""- , " NOTE: when the pre-/post-code is anything but Nothing, the C compiler"- , " is NOT called---we assume you're doing a custom build. We do NOT"- , " instrument your code with a 'main()' function simulator. Use this"- , " function to generate embedded programs."+ , " 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." , ""- , " setO :: Name -> Options -> Options (t)"- , " default: \"copilotProgram\""- , " Sets the name of the executable (e.g., -o) generated by the C"- , " compiler." , ""- , "" , "EXAMPLES:" , "The following examples reference Copilot specs defined in" , "Language.Copilot.Examples.Examples." , ""- , " > interpret t0 50 noOpts"+ , " > interpret t0 50 baseOpts" , " Interprets t0 for 50 iterations." , "" , " > interpret t3 40"@@ -149,24 +149,24 @@ , " Interpret t3 for 40 iterations, seeding the external variable \"ext\"" , " to [0,1,..], with 'Verbose' verbosity." , ""- , " > compile t1 \"t1\" noOpts"+ , " > 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"+ , " > 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"+ , " > test 1000 baseOpts" , " Compare the compiler and interpreter for a randomly-generated Copilot" , " spec for 1000 iterations." , ""- , " > Prelude.sequence_ [test 100 $ setR x | x <- [0..100]]"- , " Compare the compiler and interpreter on 100 randomly-generated Copilot"- , " specs, for 100 iterations each."+ , " > 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"+ , " > verify \"foo.c\" n baseOpts" , " Calls cbmc on foo.c (where foo.c is in the current directory) and" , " unrolls the program n times." ]
Language/Copilot/Interface.hs view
@@ -3,8 +3,8 @@ -- | 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, setPP, setN, setV, setR- , setDir, setGCC, setArrs, setClock, noOpts,+ , help , setE, setC, setO, setP, setI, setCode, setN, setV, setR+ , setDir, setGCC, setArrs, setClock, setSim, module Language.Copilot.Dispatch ) where @@ -39,7 +39,8 @@ optCName :: Name, -- ^ Name of the C file generated. optCompiler :: String, -- ^ The C compiler to use, as a path to the executable. optOutputDir :: String, -- ^ Where to place the output C files (.c, .h, and binary).- optPrePostCode :: Maybe (String, String), -- ^ Code to append above and below the C file.+ 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@@ -53,7 +54,7 @@ -- so we cannot declare them. Passing in -- pairs containing the name of the array -- and it's size allows them to be- -- declared."+ -- declared. optClock :: Maybe A.Clock -- ^ Use the hardware clock to drive the timing of the program? } @@ -71,7 +72,8 @@ optCName = "copilotProgram", optCompiler = "gcc", optOutputDir = "./",- optPrePostCode = Nothing,+ optPrePostCode = (Nothing, Nothing),+ optSimulate = False, optTriggers = M.empty, optArrs = [], optClock = Nothing@@ -79,12 +81,9 @@ -- Functions for making it easier for configuring copilot in the frequent use cases -noOpts :: Options -> Options-noOpts = id- test :: Int -> Options -> IO () test n opts = - interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ opts + interface $ setC "-Wall" $ setI $ setN n $ setV OnlyErrors $ setSim opts interpret :: Streams -> Int -> Options -> IO () interpret streams n opts = @@ -176,6 +175,7 @@ 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} @@ -194,9 +194,13 @@ -- | Sets the code to precede and follow the copilot specification -- If nothing, then code appropriate for communication with the interpreter is generated-setPP :: (String, String) -> Options -> Options-setPP pp opts = opts {optPrePostCode = Just pp}+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 =@@ -249,6 +253,7 @@ outputDir = optOutputDir opts, compiler = optCompiler opts, prePostCode = optPrePostCode opts,+ sim = optSimulate opts, -- triggers = optTriggers opts, arrDecs = optArrs opts, clock = optClock opts
Language/Copilot/Interpreter.hs view
@@ -10,10 +10,8 @@ -- 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+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 =
Language/Copilot/Language.hs view
@@ -67,7 +67,7 @@ -- Same risk with mod. Use div0 and mod0 if unsure. mod, div :: (Streamable a, A.IntegralE a) => Spec a -> Spec a -> Spec a mod = F2 P.mod A.mod_-div = F2 P.mod A.div_+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.
Language/Copilot/Language/Sampling.hs view
@@ -85,15 +85,15 @@ extF = PVar A.Float extD = PVar A.Double -- for arrays - extArrB = \fn idx -> PArr A.Bool (fn, idx)- extArrI8 = \fn idx -> PArr A.Int8 (fn, idx)- extArrI16 = \fn idx -> PArr A.Int16 (fn, idx)- extArrI32 = \fn idx -> PArr A.Int32 (fn, idx)- extArrI64 = \fn idx -> PArr A.Int64 (fn, idx)- extArrW8 = \fn idx -> PArr A.Word8 (fn, idx)- extArrW16 = \fn idx -> PArr A.Word16 (fn, idx)- extArrW32 = \fn idx -> PArr A.Word32 (fn, idx)- extArrW64 = \fn idx -> PArr A.Word64 (fn, idx)- extArrF = \fn idx -> PArr A.Float (fn, idx)- extArrD = \fn idx -> PArr A.Double (fn, idx)+ 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)
Language/Copilot/Libs/Statistics.hs view
@@ -2,9 +2,10 @@ -- the number of periods over which to compute the statistic (@n == 1@ computes -- it only over the current period). -module Language.Copilot.Libs.Statistics(max, min, sum, mean) where+module Language.Copilot.Libs.Statistics+ (max, min, sum, mean, meanNow) where -import Prelude (Int, ($), foldl1, fromIntegral)+import Prelude (Int, ($), foldl1, fromIntegral, foldl, error, length) --import qualified Prelude as P import qualified Language.Atom as A@@ -39,5 +40,11 @@ mean n s = nOneChk "mean" n $ (sum n s) / (fromIntegral n) --- majority :: (Streamable a, A.NumE a) => Int -> Spec a -> Spec a--- majority n s =+-- | 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)++
+ Language/Copilot/Libs/Vote.hs view
@@ -0,0 +1,76 @@+-- | 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)
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 1.0+version: 1.0.1 cabal-version: >= 1.2 license: BSD3 license-file: LICENSE@@ -32,11 +32,11 @@ extra-source-files: README library- ghc-options: -Wall + ghc-options: -Wall -- These build depends represent my current system. This will probably- -- build on packages outside these constaints.+ -- build on packages outside these constraints. build-depends: - base >= 4.2 && < 6+ base >= 4.0 && < 6 , atom >= 1.0.8 , containers >= 0.2.0.1 , process >= 1.0.0.0@@ -68,6 +68,7 @@ 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