diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +2009 +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,56 @@ +Overview +======== +This package is a Copilot back-end that targets Atom +. Atom is a Haskell DSL that generates +real-time C code. + +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. + +Examples +========= +Please see the files under the Examples directory in the +[Copilot](http://hackage.haskell.org/package/copilot) 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-c99 + +However, we strongly recommend you install Copilot, which installs copilot-c99 +and other packages automatically. Execute + + cabal install copilot + +Dependencies +============= +copilot-c99 depends on the +[Atom](http://hackage.haskell.org/package/copilot-cbmc) to generate hard +real-time C code. + +Resources +========= +[copilot-c99](http://hackage.haskell.org/package/copilot-c99) is available on +Hackage. + +**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! + +Copyright, License +================== +Copilot is distributed with the BSD3 license. The license file contains the +[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage. + +Thanks +====== +We are grateful for NASA Contract NNL08AD13T to [Galois, +Inc](http://corp.galois.com/) and the [National Institute of +Aerospace](http://www.nianet.org/), which partially supported this work. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot-c99.cabal b/copilot-c99.cabal new file mode 100644 --- /dev/null +++ b/copilot-c99.cabal @@ -0,0 +1,87 @@ +cabal-version : >= 1.10 +name : copilot-c99 +version : 0.1 +synopsis : A compiler for Copilot targeting C99. +description : This is a back-end from Copilot to the Atom DSL. Please see README.mk for more details. +license : BSD3 +license-file : LICENSE +maintainer : leepike@galois.com +stability : Experimental +category : Language, Embedded +build-type : Simple +extra-source-files : README.md + +author : Lee Pike + , Robin Morisset + , Alwyn Goodloe + , Sebastian Niller + , Nis Nordby Wegmann + +source-repository head + type: git + location: git://github.com/niswegmann/copilot-c99.git + +library + default-language : Haskell2010 + hs-source-dirs : src + ghc-options : -Wall -fwarn-tabs + ghc-prof-options : -auto-all -caf-all + + build-depends : atom >= 1.0.9 + , base >= 4.3 && < 5 + , bytestring + , bytestring-csv + , containers >= 0.4 + , copilot-core + , directory >= 1.1 + , process >= 1.0 + , pretty >= 1.0 + , random >= 1.0 + , text >= 0.6 + , QuickCheck >= 2.4 + + exposed-modules : Copilot.Compile.C99.Test.CheckSpec + , Copilot.Compile.C99.Test.Driver + , Copilot.Compile.C99.Test.Iteration + , Copilot.Compile.C99.Test.ReadCSV + , Copilot.Compile.C99 + , Copilot.Compile.C99.C2A + , Copilot.Compile.C99.Common + , Copilot.Compile.C99.MetaTable + , Copilot.Compile.C99.Params + , Copilot.Compile.C99.Phases + , Copilot.Compile.C99.PrePostCode + , Copilot.Compile.C99.Queue + , Copilot.Compile.C99.Witness + +executable copilot-c99-qc + default-language : Haskell2010 + hs-source-dirs : test, src + ghc-options : -Wall -fwarn-tabs + main-is : CopilotC99Test.hs + + build-depends : atom >= 1.0.9 + , base >= 4.3 + , bytestring + , bytestring-csv + , containers >= 0.4 + , copilot-core + , directory >= 1.1 + , process >= 1.0 + , pretty >= 1.0 + , random >= 1.0 + , text >= 0.6 + , QuickCheck >= 2.4 + + other-modules : Copilot.Compile.C99 + , Copilot.Compile.C99.C2A + , Copilot.Compile.C99.MetaTable + , Copilot.Compile.C99.Params + , Copilot.Compile.C99.Phases + , Copilot.Compile.C99.PrePostCode + , Copilot.Compile.C99.Queue + , Copilot.Compile.C99.Witness + , Copilot.Compile.C99.Test.CheckSpec + , Copilot.Compile.C99.Test.Driver + , Copilot.Compile.C99.Test.Iteration + , Copilot.Compile.C99.Test.ReadCSV diff --git a/src/Copilot/Compile/C99.hs b/src/Copilot/Compile/C99.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99.hs @@ -0,0 +1,49 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | + +module Copilot.Compile.C99 + ( compile + , module Copilot.Compile.C99.Params + ) where + +import Copilot.Compile.Header.C99 (genC99Header) +import Copilot.Compile.C99.MetaTable (allocMetaTable) +import Copilot.Compile.C99.Params +import Copilot.Compile.C99.Phases (schedulePhases) +import Copilot.Compile.C99.PrePostCode (preCode, postCode) +import qualified Copilot.Core as Core +import Language.Atom (Atom) +import qualified Language.Atom as Atom +import Control.Monad (when) + +-------------------------------------------------------------------------------- + +compile :: Params -> Core.Spec -> IO () +compile params spec0 = + do + (schedule, _, _, _, _) <- Atom.compile programName atomDefaults atomProgram + when (verbose params) $ putStrLn (Atom.reportSchedule schedule) + genC99Header (prefix params) "." spec + + where + + spec :: Core.Spec + spec = Core.makeTags spec0 + + programName :: String + programName = withPrefix (prefix params) "copilot" + + atomDefaults :: Atom.Config + atomDefaults = + Atom.defaults + { Atom.cCode = \ _ _ _ -> + (preCode params spec, postCode params spec) } + + atomProgram :: Atom () + atomProgram = + do + meta <- allocMetaTable spec + schedulePhases params meta spec diff --git a/src/Copilot/Compile/C99/C2A.hs b/src/Copilot/Compile/C99/C2A.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/C2A.hs @@ -0,0 +1,259 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification, GADTs #-} + +module Copilot.Compile.C99.C2A + ( c2aExpr + , c2aType + ) where + +import qualified Copilot.Compile.C99.Queue as Q +import qualified Copilot.Compile.C99.Witness as W +import Copilot.Compile.C99.MetaTable +import Copilot.Core (Op1 (..), Op2 (..), Op3 (..)) +import qualified Copilot.Core as C +import Copilot.Core.Type.Equality ((=~=), coerce, cong) +import Data.Map (Map) +import qualified Data.Map as M +import qualified Language.Atom as A +import qualified Prelude as P +import Prelude hiding (id) + +-------------------------------------------------------------------------------- + +c2aExpr :: MetaTable -> C.Expr a -> A.E a +c2aExpr meta e = c2aExpr_ e M.empty meta + +-------------------------------------------------------------------------------- + +c2aType :: C.Type a -> A.Type +c2aType t = + case t of + C.Bool -> A.Bool + C.Int8 -> A.Int8 ; C.Int16 -> A.Int16 + C.Int32 -> A.Int32 ; C.Int64 -> A.Int64 + C.Word8 -> A.Word8 ; C.Word16 -> A.Word16 + C.Word32 -> A.Word32 ; C.Word64 -> A.Word64 + C.Float -> A.Float ; C.Double -> A.Double + +-------------------------------------------------------------------------------- + +data Local = forall a . Local + { localAtomExpr :: A.E a + , localType :: C.Type a } + +type Env = Map C.Name Local + +-------------------------------------------------------------------------------- + +c2aExpr_ :: C.Expr a -> Env -> MetaTable -> A.E a +c2aExpr_ e0 env meta = case e0 of + + ---------------------------------------------------- + + C.Const _ x -> + + A.Const x + + ---------------------------------------------------- + + C.Drop t i id -> + + let + Just strmInfo = M.lookup id (streamInfoMap meta) + in + drop1 t strmInfo + + where + + drop1 :: C.Type a -> StreamInfo -> A.E a + drop1 t1 + StreamInfo + { streamInfoQueue = que + , streamInfoType = t2 + } = + let + Just p = t2 =~= t1 + in + case W.exprInst t2 of + W.ExprInst -> + coerce (cong p) (Q.lookahead (fromIntegral i) que) + + ---------------------------------------------------- + + C.Local t1 _ name e1 e2 -> + + let + e1' = c2aExpr_ e1 env meta + env' = M.insert name (Local e1' t1) env + in + c2aExpr_ e2 env' meta + + ---------------------------------------------------- + + C.Var t1 name -> + + let + Just local = M.lookup name env + in + case local of + Local + { localAtomExpr = e + , localType = t2 + } -> + let + Just p = t2 =~= t1 + in + case W.exprInst t2 of + W.ExprInst -> + coerce (cong p) e + + ---------------------------------------------------- + + C.ExternVar t name -> + + let + Just externInfo = M.lookup name (externInfoMap meta) + in + externVar1 t externInfo + + where + + externVar1 :: C.Type a -> ExternInfo -> A.E a + externVar1 t1 + ExternInfo + { externInfoVar = v + , externInfoType = t2 + } = + let + Just p = t2 =~= t1 + in + coerce (cong p) (A.value v) + + ---------------------------------------------------- + + C.ExternFun t name _ (Just tag) -> + + let + Just extFunInfo = M.lookup (name, tag) (externFunInfoMap meta) + in + externFun1 t extFunInfo + + where + + externFun1 t1 + ExternFunInfo + { externFunInfoVar = var + , externFunInfoType = t2 + } = + let + Just p = t2 =~= t1 + in + case W.exprInst t2 of + W.ExprInst -> + coerce (cong p) (A.value var) + + ---------------------------------------------------- + + C.ExternArray _ t name _ (Just tag) -> + + let + Just extArrayInfo = M.lookup (name, tag) (externArrayInfoMap meta) + in + externArray1 t extArrayInfo + + where + + externArray1 t1 + ExternArrayInfo + { externArrayInfoVar = var + , externArrayInfoElemType = t2 + } = + let + Just p = t2 =~= t1 + in + case W.exprInst t2 of + W.ExprInst -> + coerce (cong p) (A.value var) + + ---------------------------------------------------- + + C.Op1 op e -> + + c2aOp1 op (c2aExpr_ e env meta) + + ---------------------------------------------------- + + C.Op2 op e1 e2 -> + + c2aOp2 op (c2aExpr_ e1 env meta) (c2aExpr_ e2 env meta) + + ---------------------------------------------------- + + C.Op3 op e1 e2 e3 -> + + c2aOp3 op (c2aExpr_ e1 env meta) (c2aExpr_ e2 env meta) + (c2aExpr_ e3 env meta) + + ---------------------------------------------------- + +c2aOp1 :: C.Op1 a b -> A.E a -> A.E b +c2aOp1 op = case op of + Not -> A.not_ + Abs t -> case W.numEInst t of W.NumEInst -> abs + Sign t -> case W.numEInst t of W.NumEInst -> signum + Recip t -> case W.numEInst t of W.NumEInst -> recip + Exp t -> case W.floatingEInst t of W.FloatingEInst -> exp + Sqrt t -> case W.floatingEInst t of W.FloatingEInst -> sqrt + Log t -> case W.floatingEInst t of W.FloatingEInst -> log + Sin t -> case W.floatingEInst t of W.FloatingEInst -> sin + Tan t -> case W.floatingEInst t of W.FloatingEInst -> tan + Cos t -> case W.floatingEInst t of W.FloatingEInst -> cos + Asin t -> case W.floatingEInst t of W.FloatingEInst -> asin + Atan t -> case W.floatingEInst t of W.FloatingEInst -> atan + Acos t -> case W.floatingEInst t of W.FloatingEInst -> acos + Sinh t -> case W.floatingEInst t of W.FloatingEInst -> sinh + Tanh t -> case W.floatingEInst t of W.FloatingEInst -> tanh + Cosh t -> case W.floatingEInst t of W.FloatingEInst -> cosh + Asinh t -> case W.floatingEInst t of W.FloatingEInst -> asinh + Atanh t -> case W.floatingEInst t of W.FloatingEInst -> atanh + Acosh t -> case W.floatingEInst t of W.FloatingEInst -> acosh + BwNot t -> case W.bitsEInst t of W.BitsEInst -> (A.complement) + Cast C.Bool C.Bool -> P.id + Cast C.Bool t -> case W.numEInst t of + W.NumEInst -> \e -> A.mux e (A.Const 1) (A.Const 0) + Cast t0 t1 -> case W.numEInst t0 of + W.NumEInst -> + case W.numEInst t1 of W.NumEInst -> A.Cast + +c2aOp2 :: C.Op2 a b c -> A.E a -> A.E b -> A.E c +c2aOp2 op = case op of + And -> (A.&&.) + Or -> (A.||.) + Add t -> case W.numEInst t of W.NumEInst -> (+) + Sub t -> case W.numEInst t of W.NumEInst -> (-) + Mul t -> case W.numEInst t of W.NumEInst -> (*) + Div t -> case W.integralEInst t of W.IntegralEInst -> A.div_ + Mod t -> case W.integralEInst t of W.IntegralEInst -> A.mod_ + Fdiv t -> case W.numEInst t of W.NumEInst -> (/) + Pow t -> case W.floatingEInst t of W.FloatingEInst -> (**) + Logb t -> case W.floatingEInst t of W.FloatingEInst -> logBase + Eq t -> case W.eqEInst t of W.EqEInst -> (A.==.) + Ne t -> case W.eqEInst t of W.EqEInst -> (A./=.) + Le t -> case W.ordEInst t of W.OrdEInst -> (A.<=.) + Ge t -> case W.ordEInst t of W.OrdEInst -> (A.>=.) + Lt t -> case W.ordEInst t of W.OrdEInst -> (A.<.) + Gt t -> case W.ordEInst t of W.OrdEInst -> (A.>.) + BwAnd t -> case W.bitsEInst t of W.BitsEInst -> (A..&.) + BwOr t -> case W.bitsEInst t of W.BitsEInst -> (A..|.) + BwXor t -> case W.bitsEInst t of W.BitsEInst -> (A.xor) + BwShiftL t t' -> case ( W.bitsEInst t, W.integralEInst t' ) + of ( W.BitsEInst, W.IntegralEInst ) -> (A..<<.) + BwShiftR t t' -> case ( W.bitsEInst t, W.integralEInst t' ) + of ( W.BitsEInst, W.IntegralEInst ) -> (A..>>.) + +c2aOp3 :: C.Op3 a b c d -> A.E a -> A.E b -> A.E c -> A.E d +c2aOp3 op = case op of + Mux t -> case W.exprInst t of W.ExprInst -> A.mux diff --git a/src/Copilot/Compile/C99/Common.hs b/src/Copilot/Compile/C99/Common.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Common.hs @@ -0,0 +1,32 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs #-} + +module Copilot.Compile.C99.Common + ( mkTmpExtFunVarName + , typeSpec + ) where + +import qualified Copilot.Core as C + +-------------------------------------------------------------------------------- + +mkTmpExtFunVarName :: C.Name -> C.Tag -> String +mkTmpExtFunVarName name tag = "tmp_ext_fun_" ++ name ++ "_" ++ "_" ++ show tag + +-------------------------------------------------------------------------------- + +typeSpec :: C.Type a -> String +typeSpec C.Bool = "bool" +typeSpec C.Int8 = "int8_t" +typeSpec C.Int16 = "int16_t" +typeSpec C.Int32 = "int32_t" +typeSpec C.Int64 = "int64_t" +typeSpec C.Word8 = "uint8_t" +typeSpec C.Word16 = "uint16_t" +typeSpec C.Word32 = "uint32_t" +typeSpec C.Word64 = "uint64_t" +typeSpec C.Float = "float" +typeSpec C.Double = "double" diff --git a/src/Copilot/Compile/C99/MetaTable.hs b/src/Copilot/Compile/C99/MetaTable.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/MetaTable.hs @@ -0,0 +1,163 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification #-} + +module Copilot.Compile.C99.MetaTable + ( StreamInfo (..) + , ExternInfo (..) + , ExternArrayInfo (..) + , ExternFunInfo (..) + , StreamInfoMap + , ExternInfoMap + , ExternFunInfoMap + , MetaTable (..) + , allocMetaTable + ) where + +import Control.Monad (liftM) +import qualified Copilot.Compile.C99.Queue as Q +import qualified Copilot.Compile.C99.Witness as W +import qualified Copilot.Core as C +import Copilot.Core.External +import Data.Map (Map) +import qualified Data.Map as M +import Language.Atom (Atom) +import qualified Language.Atom as A +import Prelude hiding (id) + +-------------------------------------------------------------------------------- + +data StreamInfo = forall a . StreamInfo + { streamInfoQueue :: Q.Queue a + , streamInfoTempVar :: A.V a + , streamInfoType :: C.Type a } + +type StreamInfoMap = Map C.Id StreamInfo + +-------------------------------------------------------------------------------- + +data ExternInfo = forall a . ExternInfo + { externInfoVar :: A.V a + , externInfoType :: C.Type a } + +type ExternInfoMap = Map C.Name ExternInfo + +-------------------------------------------------------------------------------- + +data ExternArrayInfo = forall a b . Integral a => ExternArrayInfo + { externArrayInfoVar :: A.V b + , externArrayInfoIdxExpr :: C.Expr a + , externArrayInfoIdxType :: C.Type a + , externArrayInfoElemType :: C.Type b } + +type ExternArrayInfoMap = Map (C.Name, C.Tag) ExternArrayInfo + +-------------------------------------------------------------------------------- + +data ExternFunInfo = forall a . ExternFunInfo + { externFunInfoArgs :: [C.UExpr] + , externFunInfoVar :: A.V a + , externFunInfoType :: C.Type a } + +type ExternFunInfoMap = Map (C.Name, C.Tag) ExternFunInfo + +-------------------------------------------------------------------------------- + +data MetaTable = MetaTable + { streamInfoMap :: StreamInfoMap + , externInfoMap :: ExternInfoMap + , externArrayInfoMap :: ExternArrayInfoMap + , externFunInfoMap :: ExternFunInfoMap } + +-------------------------------------------------------------------------------- + +allocMetaTable :: C.Spec -> A.Atom MetaTable +allocMetaTable spec = + do + streamInfoMap_ <- + liftM M.fromList $ mapM allocStream (C.specStreams spec) + + externInfoMap_ <- + liftM M.fromList $ mapM allocExternVar (externVars spec) + + externArrayInfoMap_ <- + liftM M.fromList $ mapM allocExternArray (externArrays spec) + + externFunInfoMap_ <- + liftM M.fromList $ mapM allocExternFun (externFuns spec) + + return $ + MetaTable + streamInfoMap_ + externInfoMap_ + externArrayInfoMap_ + externFunInfoMap_ + +-------------------------------------------------------------------------------- + +allocStream :: C.Stream -> Atom (C.Id, StreamInfo) +allocStream + C.Stream + { C.streamId = id + , C.streamBuffer = buf + , C.streamExprType = t + } = + do + W.ExprInst <- return (W.exprInst t) + que <- Q.queue (mkQueueName id) buf + tmp <- A.var (mkTempVarName id) (C.uninitialized t) + let + strmInfo = + StreamInfo + { streamInfoQueue = que + , streamInfoTempVar = tmp + , streamInfoType = t } + return (id, strmInfo) + +-------------------------------------------------------------------------------- + +allocExternVar :: ExtVar -> Atom (C.Name, ExternInfo) +allocExternVar (ExtVar name ut) = + case ut of + C.UType t -> + do + W.ExprInst <- return (W.exprInst t) + v <- A.var (mkExternName name) (C.uninitialized t) + return (name, ExternInfo v t) + +-------------------------------------------------------------------------------- + +allocExternArray :: ExtArray -> Atom ((C.Name, C.Tag), ExternArrayInfo) +allocExternArray (ExtArray name elemType idxExpr idxType (Just tag)) = + do + W.ExprInst <- return (W.exprInst elemType) + v <- A.var (mkExternArrayName name tag) (C.uninitialized elemType) + return ((name, tag), ExternArrayInfo v idxExpr idxType elemType) + +-------------------------------------------------------------------------------- + +allocExternFun :: ExtFun -> Atom ((C.Name, C.Tag), ExternFunInfo) +allocExternFun (ExtFun name t args (Just tag)) = + do + W.ExprInst <- return (W.exprInst t) + v <- A.var (mkExternFunName name tag) (C.uninitialized t) + return ((name, tag), ExternFunInfo args v t) + +-------------------------------------------------------------------------------- + +mkExternName :: C.Name -> A.Name +mkExternName name = "ext_" ++ name + +mkExternArrayName :: C.Name -> C.Tag -> A.Name +mkExternArrayName name tag = "ext_array_" ++ show tag ++ "_" ++ name + +mkExternFunName :: C.Name -> C.Tag -> A.Name +mkExternFunName name tag = "ext_fun_" ++ show tag ++ "_" ++ name + +mkQueueName :: C.Id -> A.Name +mkQueueName id = "str" ++ show id + +mkTempVarName :: C.Id -> A.Name +mkTempVarName id = "tmp" ++ show id diff --git a/src/Copilot/Compile/C99/Params.hs b/src/Copilot/Compile/C99/Params.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Params.hs @@ -0,0 +1,20 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.C99.Params (Params (..), defaultParams, withPrefix) where + +data Params = Params + { prefix :: Maybe String -- An string to prefix the output with + , verbose :: Bool + } + +defaultParams :: Params +defaultParams = Params + { prefix = Nothing + , verbose = True + } + +withPrefix :: Maybe String -> String -> String +withPrefix (Just cs) ds = cs ++ "_" ++ ds +withPrefix _ ds = ds diff --git a/src/Copilot/Compile/C99/Phases.hs b/src/Copilot/Compile/C99/Phases.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Phases.hs @@ -0,0 +1,254 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, Rank2Types #-} + +module Copilot.Compile.C99.Phases + ( schedulePhases + , numberOfPhases + ) where + +import Copilot.Compile.C99.C2A (c2aExpr, c2aType) +import Copilot.Compile.C99.Common (mkTmpExtFunVarName) +import Copilot.Compile.C99.MetaTable + (MetaTable (..), StreamInfo (..), ExternInfo (..), ExternArrayInfo (..) + ,ExternFunInfo (..)) +import Copilot.Compile.C99.Params +import qualified Copilot.Compile.C99.Queue as Q +import qualified Copilot.Compile.C99.Witness as W +import qualified Copilot.Core as Core +import Copilot.Core.Type.Equality ((=~=), Equal (..)) +import Data.List (intersperse) +import qualified Data.Map as M +import Language.Atom (Atom, (<==), atom, cond, exactPhase) +import qualified Language.Atom as A +import Prelude hiding (id) + +-------------------------------------------------------------------------------- + +data Phase + = SampleExternVars + | SampleExternArrays + | SampleExternFuns + | UpdateStates + | FireTriggers + | UpdateBuffers + | UpdateObservers + deriving (Bounded, Eq, Enum, Ord, Show) + +numberOfPhases :: Int +numberOfPhases = succ (fromEnum (maxBound :: Phase)) + +-------------------------------------------------------------------------------- + +schedulePhases :: Params -> MetaTable -> Core.Spec -> Atom () +schedulePhases params meta spec = + A.period numberOfPhases $ + sampleExternVars params meta spec >> + sampleExternArrays params meta spec >> + sampleExternFuns params meta spec >> + updateStates params meta spec >> + fireTriggers params meta spec >> + updateObservers params meta spec >> + updateBuffers params meta spec + +-------------------------------------------------------------------------------- + +sampleExternVars :: Params -> MetaTable -> Core.Spec -> Atom () +sampleExternVars _ meta _ = + (mapM_ sampleExternVar . M.toList . externInfoMap) meta + + where + + sampleExternVar :: (Core.Name, ExternInfo) -> Atom () + sampleExternVar (name, ExternInfo v t) = + exactPhase (fromEnum SampleExternVars) $ + atom ("sample_var_" ++ name) $ + do + W.AssignInst <- return $ W.assignInst t + v <== A.value (A.var' name (c2aType t)) + +-------------------------------------------------------------------------------- + +sampleExternArrays :: Params -> MetaTable -> Core.Spec -> Atom () +sampleExternArrays _ meta _ = + (mapM_ sampleExternArray . M.toList . externArrayInfoMap) meta + + where + + sampleExternArray :: ((Core.Name, Core.Tag), ExternArrayInfo) -> Atom () + sampleExternArray ((name, tag), ExternArrayInfo var idxExpr idxType elemType) = + exactPhase (fromEnum SampleExternArrays) $ + atom ("sample_array_" ++ name ++ "_" ++ show tag) $ + do + W.IntegralEInst <- return $ W.integralEInst idxType + W.AssignInst <- return $ W.assignInst elemType + W.ExprInst <- return $ W.exprInst elemType + let e = c2aExpr meta idxExpr + arr = A.array' name (c2aType elemType) + var <== A.value (arr A.! e) + +-------------------------------------------------------------------------------- + +sampleExternFuns :: Params -> MetaTable -> Core.Spec -> Atom () +sampleExternFuns _ meta _ = + (mapM_ sampleExternFun . M.toList . externFunInfoMap) meta + + where + + c2aUExpr :: Core.UExpr -> A.UE + c2aUExpr (Core.UExpr t e) = + case W.exprInst t of + W.ExprInst -> A.ue (c2aExpr meta e) + + sampleExternFun :: ((Core.Name, Core.Tag), ExternFunInfo) -> Atom () + sampleExternFun ((name, tag), ExternFunInfo args var t) = + exactPhase (fromEnum SampleExternFuns) $ + atom ("sample_fun_" ++ name ++ "_" ++ show tag) $ + do + let args' = map c2aUExpr args + A.action fnCall args' + W.AssignInst <- return $ W.assignInst t + var <== A.value (A.var' (mkTmpExtFunVarName name tag) (c2aType t)) + + where + + fnCall :: [String] -> String + fnCall xs = mkTmpExtFunVarName name tag ++ " = " ++ name ++ "(" + ++ concat (intersperse "," xs) ++ ")" + +-------------------------------------------------------------------------------- + +updateStates :: Params -> MetaTable -> Core.Spec -> Atom () +updateStates _ meta + Core.Spec + { Core.specStreams = streams + } = mapM_ updateStreamState streams + + where + + updateStreamState :: Core.Stream -> Atom () + updateStreamState + Core.Stream + { Core.streamId = id + , Core.streamExpr = e + , Core.streamExprType = t1 + , Core.streamGuard = g + } = + do + let e' = c2aExpr meta e + Just strmInfo = M.lookup id (streamInfoMap meta) + g' = cond (c2aExpr meta g) + updateStreamState1 t1 id e' g' strmInfo + + updateStreamState1 + :: Core.Type a -> Core.Id -> A.E a -> Atom () -> StreamInfo -> Atom () + updateStreamState1 t1 id e1 g1 + StreamInfo + { streamInfoTempVar = tmp + , streamInfoType = t2 + } = + exactPhase (fromEnum UpdateStates) $ + atom ("update_state_s" ++ show id) $ + do + g1 + W.AssignInst <- return (W.assignInst t2) + Just Refl <- return (t1 =~= t2) + tmp <== e1 -- coerce (cong p) e1 + +-------------------------------------------------------------------------------- + +fireTriggers :: Params -> MetaTable -> Core.Spec -> Atom () +fireTriggers params meta + Core.Spec + { Core.specTriggers = triggers + } = + mapM_ fireTrigger triggers + + where + + fireTrigger :: Core.Trigger -> Atom () + fireTrigger + Core.Trigger + { Core.triggerName = name + , Core.triggerGuard = e0 + , Core.triggerArgs = args + } = + exactPhase (fromEnum FireTriggers) $ + atom ("fire_trigger_" ++ name) $ + do + let args' = map triggerArg2UE (reverse args) + e0' = c2aExpr meta e0 + cond e0' + A.action fnCall args' + + where + + triggerArg2UE :: Core.UExpr -> A.UE + triggerArg2UE (Core.UExpr t e) = + case W.exprInst t of + W.ExprInst -> A.ue (c2aExpr meta e) + + fnCall :: [String] -> String + fnCall xs = withPrefix (prefix params) name ++ + "(" ++ concat (intersperse "," xs) ++ ")" + +-------------------------------------------------------------------------------- + +updateObservers :: Params -> MetaTable -> Core.Spec -> Atom () +updateObservers params meta + Core.Spec + { Core.specObservers = observers + } = + mapM_ updateObserver observers + + where + + updateObserver :: Core.Observer -> Atom () + updateObserver + Core.Observer + { Core.observerName = name + , Core.observerExpr = e + , Core.observerExprType = t + } = + exactPhase (fromEnum UpdateObservers) $ + atom ("update_observer_" ++ name) $ + do + let e' = c2aExpr meta e + W.AssignInst <- return (W.assignInst t) + (A.var' (withPrefix (prefix params) name) . c2aType) t <== e' + +-------------------------------------------------------------------------------- + +updateBuffers :: Params -> MetaTable -> Core.Spec -> Atom () +updateBuffers _ meta + Core.Spec + { Core.specStreams = streams + } = + mapM_ updateBuffer streams + + where + + updateBuffer :: Core.Stream -> Atom () + updateBuffer + Core.Stream + { Core.streamId = id + } = + let + Just strmInfo = M.lookup id (streamInfoMap meta) + in + updateBuffer1 id strmInfo + + updateBuffer1 :: Core.Id -> StreamInfo -> Atom () + updateBuffer1 id + StreamInfo + { streamInfoQueue = que + , streamInfoTempVar = tmp + , streamInfoType = t + } = + exactPhase (fromEnum UpdateBuffers) $ + atom ("update_buffer_s" ++ show id) $ + do + W.AssignInst <- return (W.assignInst t) + Q.dropFirstElemAndSnoc (A.value tmp) que diff --git a/src/Copilot/Compile/C99/PrePostCode.hs b/src/Copilot/Compile/C99/PrePostCode.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/PrePostCode.hs @@ -0,0 +1,57 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs #-} + +module Copilot.Compile.C99.PrePostCode + ( preCode , postCode + ) where + +import Copilot.Core +import Copilot.Compile.C99.Common (typeSpec, mkTmpExtFunVarName) +import Copilot.Compile.C99.Params +import Copilot.Compile.C99.Phases (numberOfPhases) +import Copilot.Compile.Header.C99 (c99HeaderName) + +-------------------------------------------------------------------------------- + +preCode :: Params -> Spec -> String +preCode params spec = unlines $ + [ "#include \"" ++ c99HeaderName (prefix params) ++ "\"" ] ++ + ( map (observerDecl params) . specObservers ) spec ++ + ( map (tmpExtFunVar params) . externFuns ) spec + +-------------------------------------------------------------------------------- + +observerDecl :: Params -> Observer -> String +observerDecl params (Observer cs _ t) = typeSpec t ++ " " ++ name ++ ";" + + where + + name = withPrefix (prefix params) cs + +-------------------------------------------------------------------------------- + +tmpExtFunVar :: Params -> ExtFun -> String +tmpExtFunVar _ ExtFun + { externFunName = name + , externFunType = t +-- , externFunArgs = args + , externFunTag = Just tag } = + "static " ++ typeSpec t ++ " " ++ mkTmpExtFunVarName name tag ++ ";" + +-------------------------------------------------------------------------------- + +postCode :: Params -> Spec -> String +postCode params _ = + unlines + [ "void " ++ withPrefix (prefix params) "step" ++ "()" + , "{" + , " " ++ concat (replicate numberOfPhases step) + , "}" + ] + + where + + step = withPrefix (prefix params) "copilot" ++ "();" diff --git a/src/Copilot/Compile/C99/Queue.hs b/src/Copilot/Compile/C99/Queue.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Queue.hs @@ -0,0 +1,56 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.C99.Queue + ( Queue + , dropFirstElemAndSnoc + , lookahead + , size + , queue + ) where + +import Data.Word (Word16) +import Language.Atom + +type QueueIndexType = Word16 + +data Queue a = Queue + { queueRingBuffer :: A a + , queuePointer :: V QueueIndexType + , size :: QueueIndexType + } + +dropFirstElemAndSnoc :: Assign a => E a -> Queue a -> Atom () +dropFirstElemAndSnoc x + Queue + { queueRingBuffer = buf + , queuePointer = p + , size = sz + } = + do + (buf ! value p) <== x + p <== mux (value p + 1 >=. fromIntegral sz) 0 (value p + 1) + +lookahead :: Expr a => Int -> Queue a -> E a +lookahead i + Queue + { queueRingBuffer = buf + , queuePointer = p + , size = sz + } = + let + k = (value p + fromIntegral i) `mod_` fromIntegral sz + in + buf !. k + +queue :: Expr a => String -> [a] -> Atom (Queue a) +queue name xs = + do + buf <- array ("queue_buffer_" ++ name) xs + p <- var ("queue_pointer_" ++ name) 0 + return + Queue + { queueRingBuffer = buf + , queuePointer = p + , size = fromIntegral (length xs) } diff --git a/src/Copilot/Compile/C99/Test/CheckSpec.hs b/src/Copilot/Compile/C99/Test/CheckSpec.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Test/CheckSpec.hs @@ -0,0 +1,76 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.C99.Test.CheckSpec (checkSpec) where + +import Copilot.Core (Spec) +import Copilot.Core.Interpret.Eval (eval, ExtEnv(..)) +import Copilot.Compile.C99 (compile) +import Copilot.Compile.C99.Params (Params (..), defaultParams) +import Copilot.Compile.C99.Test.Driver (driver) +import Copilot.Compile.C99.Test.Iteration (Iteration(..), execTraceToIterations) +import Copilot.Compile.C99.Test.ReadCSV (iterationsFromCSV) +import Copilot.Core.Type.Show (ShowType(..)) + +import Data.ByteString (ByteString) +import qualified Data.ByteString.Char8 as B +import qualified Data.Map as M +import qualified Data.Text.IO as TIO +import System.Directory (removeFile) +import System.Process (system, readProcess) +import Control.Monad (when, unless) +import Text.PrettyPrint (text, (<+>), ($$), render, vcat, hang) + +-------------------------------------------------------------------------------- + +checkSpec :: Int -> Spec -> IO Bool +checkSpec numIterations spec = do + genCFiles numIterations spec + compileCFiles + csv <- execute numIterations + let is1 = iterationsFromCSV csv + let is2 = interp numIterations spec + -- print is1 + -- print "..." + -- print is2 + let eq = is1 == is2 + unless eq (putStrLn $ showCompare is1 is2) + -- Keep things around if there's a failure + when eq cleanUp + return eq + +showCompare :: [Iteration] -> [Iteration] -> String +showCompare s1 s2 = + render $ text "From C:" <+> text "---" <+> text "From Interpreter:" $$ + (vcat $ map (\(a,b) -> hang a 10 b) zipped) + where + zipped = zip (toDoc s1) (toDoc s2) + toDoc = map (text . show) + +genCFiles :: Int -> Spec -> IO () +genCFiles numIterations spec = do + compile (defaultParams { prefix = Nothing, verbose = False }) spec + TIO.writeFile "driver.c" (driver M.empty numIterations spec) + return () + +compileCFiles :: IO () +compileCFiles = do + _ <- system $ "gcc copilot.c driver.c -o _test" + return () + +execute :: Int -> IO ByteString +execute _ = do + fmap B.pack (readProcess "./_test" [] "") + +interp :: Int -> Spec -> [Iteration] +interp numIterations = + execTraceToIterations . eval C numIterations (ExtEnv [] [] []) + +cleanUp :: IO () +cleanUp = do + removeFile "copilot.c" + removeFile "copilot.h" + removeFile "driver.c" + removeFile "_test" + return () diff --git a/src/Copilot/Compile/C99/Test/Driver.hs b/src/Copilot/Compile/C99/Test/Driver.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Test/Driver.hs @@ -0,0 +1,156 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs #-} + +module Copilot.Compile.C99.Test.Driver + ( driver + ) where + +import Copilot.Core + (Spec (..), Trigger (..), UExpr (..), Type (..), UType (..)) +import Data.List (intersperse) +import Data.Map (Map) +import Data.Text (Text) +import Data.Text (pack) +import Text.PrettyPrint + (Doc, ($$), (<>), (<+>), nest, text, empty, render, vcat, hcat) + +type ExternalEnv = Map String (UType, [Int]) + +driver :: ExternalEnv -> Int -> Spec -> Text +driver _ numIterations Spec { specTriggers = trigs } = + pack $ render $ + ppHeader $$ + ppMain numIterations $$ + ppTriggers trigs + +ppHeader :: Doc +ppHeader = + vcat $ + [ text "#include " + , text "#include " + , text "#include " + , text "#include \"copilot.h\"" + ] + +ppMain :: Int -> Doc +ppMain numIterations = + vcat $ + [ text "int main(int argc, char const *argv[]) {" + , text " int i, k;" + , text " k = " <> text (show $ numIterations + 1) <> text ";" + , text " for (i = 1; i < k; i++) {" + , text " " <> it + , text " if (i < k-1) printf(\"#\\n\");" + , text " }" + , text " return 0;" + , text "}" + ] + + where + + it :: Doc + it = text "step();" + +ppTriggers :: [Trigger] -> Doc +ppTriggers = foldr ($$) empty . map ppTrigger + +ppTrigger :: Trigger -> Doc +ppTrigger + Trigger + { triggerName = name + , triggerArgs = args } = + hcat $ + [ text "void" <+> + text name <+> + text "(" <> + ppPars args <> + text ")" + , text "{" + , nest 2 $ + ppPrintf name args <> + text ";" + , text "}" + ] + +ppPrintf :: String -> [UExpr] -> Doc +ppPrintf name args = + text "printf(\"" <> + text name <> + text "," <> + ppFormats args <> + text "\"\\n\"," <+> + ppArgs args <> + text ")" + +ppFormats :: [UExpr] -> Doc +ppFormats + = vcat + . intersperse (text ",") + . map (text "%\"" <>) + . map ppFormat + +ppPars :: [UExpr] -> Doc +ppPars + = vcat + . intersperse (text ", ") + . map ppPar + . zip [0..] + + where + + ppPar :: (Int, UExpr) -> Doc + ppPar (k, par) = case par of + UExpr + { uExprType = t } -> + ppUType (UType t) <+> text ("t" ++ show k) + +ppArgs :: [UExpr] -> Doc +ppArgs args + = vcat + $ intersperse (text ", ") + $ map ppArg + $ [0..length args-1] + + where + + ppArg :: Int -> Doc + ppArg k = text ("t" ++ show k) + +ppUType :: UType -> Doc +ppUType UType { uTypeType = t } = text $ typeSpec' t + + where + + typeSpec' Bool = "bool" + typeSpec' Int8 = "int8_t" + typeSpec' Int16 = "int16_t" + typeSpec' Int32 = "int32_t" + typeSpec' Int64 = "int64_t" + typeSpec' Word8 = "uint8_t" + typeSpec' Word16 = "uint16_t" + typeSpec' Word32 = "uint32_t" + typeSpec' Word64 = "uint64_t" + typeSpec' Float = "float" + typeSpec' Double = "double" + +ppFormat :: UExpr -> Doc +ppFormat + UExpr { uExprType = t } = + text $ case t of + Bool -> "PRIu8" + Int8 -> "PRIi8" + Int16 -> "PRIi16" + Int32 -> "PRIi32" + Int64 -> "PRIi64" + Word8 -> "PRIu8" + Word16 -> "PRIu16" + Word32 -> "PRIu32" + Word64 -> "PRIu64" + Float -> "\"f\"" + Double -> "\"lf\"" + +--ppExterns :: +--ppExterns = undefined diff --git a/src/Copilot/Compile/C99/Test/Iteration.hs b/src/Copilot/Compile/C99/Test/Iteration.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Test/Iteration.hs @@ -0,0 +1,48 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.C99.Test.Iteration + ( Iteration (..) + , execTraceToIterations + ) where + +import Copilot.Core.Interpret.Eval (ExecTrace (..), Output) +import Data.List (unfoldr) +import Data.Map (Map) +import qualified Data.Map as M +import Data.Maybe (isJust, fromJust) + +-- An iteration represents the output of all triggers within a single +-- iteration. +newtype Iteration = + Iteration + { iterationOutputs :: (Map String [Output]) } + deriving Eq + +instance Show Iteration where + show Iteration { iterationOutputs = io } = show $ M.toList io + +execTraceToIterations :: ExecTrace -> [Iteration] +execTraceToIterations = unfoldr step + + where + + step :: ExecTrace -> Maybe (Iteration, ExecTrace) + step trace@ExecTrace { interpTriggers = trigs } + | nullary = Nothing + | otherwise = Just (iteration, tails) + + where + iteration :: Iteration + iteration = Iteration $ + fmap fromJust + $ M.filter isJust + $ fmap head + $ trigs + + nullary :: Bool + nullary = any null (M.elems trigs) + + tails :: ExecTrace + tails = trace { interpTriggers = fmap tail trigs } diff --git a/src/Copilot/Compile/C99/Test/ReadCSV.hs b/src/Copilot/Compile/C99/Test/ReadCSV.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Test/ReadCSV.hs @@ -0,0 +1,48 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.C99.Test.ReadCSV (iterationsFromCSV) where + +import Copilot.Core.Interpret.Eval (Output) +import Copilot.Core.Error (impossible) +import Copilot.Compile.C99.Test.Iteration (Iteration (..)) + +import Prelude as P +import Data.ByteString (ByteString) +import qualified Data.ByteString.Char8 as B +import qualified Data.Map as M +import Text.CSV.ByteString + +parseError :: a +parseError = impossible "CSV parsing" "copilot-c99" + +iterationsFromCSV :: ByteString -> [Iteration] +iterationsFromCSV = iterationsFromCSV' . handleMaybe . parseCSV + +handleMaybe :: Maybe a -> a +handleMaybe (Just x) = x +handleMaybe Nothing = parseError + +iterationsFromCSV' :: CSV -> [Iteration] +iterationsFromCSV' = map Iteration . go M.empty + + where + go m [] = [m] + go m (x:xs) + | nextIteration x = m : go M.empty xs + | otherwise = + let + m' = M.insert (triggerName x) (triggerOutputs x) m + in + go m' xs + +nextIteration :: Record -> Bool +nextIteration [x] = B.unpack x == "#" +nextIteration _ = False + +triggerName :: Record -> String +triggerName = B.unpack . head + +triggerOutputs :: Record -> [Output] +triggerOutputs = fmap B.unpack . tail diff --git a/src/Copilot/Compile/C99/Witness.hs b/src/Copilot/Compile/C99/Witness.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/C99/Witness.hs @@ -0,0 +1,142 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs #-} + +module Copilot.Compile.C99.Witness + ( ExprInst (..) , exprInst + , AssignInst (..) , assignInst + , EqEInst (..) , eqEInst + , OrdEInst (..) , ordEInst + , NumEInst (..) , numEInst + , IntegralEInst (..) , integralEInst + , FloatingEInst (..) , floatingEInst + , BitsEInst (..) , bitsEInst + ) where + +import qualified Language.Atom as A +import qualified Copilot.Core as C +import Data.Bits + +-------------------------------------------------------------------------------- + +badInst :: a +badInst = C.impossible "witnesses" "copilot-c99" + +-------------------------------------------------------------------------------- + +data ExprInst a = A.Expr a => ExprInst + +exprInst :: C.Type a -> ExprInst a +exprInst t = + case t of + C.Bool -> ExprInst + C.Int8 -> ExprInst ; C.Int16 -> ExprInst + C.Int32 -> ExprInst ; C.Int64 -> ExprInst + C.Word8 -> ExprInst ; C.Word16 -> ExprInst + C.Word32 -> ExprInst ; C.Word64 -> ExprInst + C.Float -> ExprInst ; C.Double -> ExprInst + +-------------------------------------------------------------------------------- + +data AssignInst a = A.Assign a => AssignInst + +assignInst :: C.Type a -> AssignInst a +assignInst t = + case t of + C.Bool -> AssignInst + C.Int8 -> AssignInst ; C.Int16 -> AssignInst + C.Int32 -> AssignInst ; C.Int64 -> AssignInst + C.Word8 -> AssignInst ; C.Word16 -> AssignInst + C.Word32 -> AssignInst ; C.Word64 -> AssignInst + C.Float -> AssignInst ; C.Double -> AssignInst + +-------------------------------------------------------------------------------- + +data EqEInst a = A.EqE a => EqEInst + +eqEInst :: Eq a => C.Type a -> EqEInst a +eqEInst t = + case t of + C.Bool -> EqEInst + C.Int8 -> EqEInst ; C.Int16 -> EqEInst + C.Int32 -> EqEInst ; C.Int64 -> EqEInst + C.Word8 -> EqEInst ; C.Word16 -> EqEInst + C.Word32 -> EqEInst ; C.Word64 -> EqEInst + C.Float -> EqEInst ; C.Double -> EqEInst + +-------------------------------------------------------------------------------- + +data OrdEInst a = A.OrdE a => OrdEInst + +ordEInst :: Ord a => C.Type a -> OrdEInst a +ordEInst t = + case t of + C.Bool -> badInst + C.Int8 -> OrdEInst ; C.Int16 -> OrdEInst + C.Int32 -> OrdEInst ; C.Int64 -> OrdEInst + C.Word8 -> OrdEInst ; C.Word16 -> OrdEInst + C.Word32 -> OrdEInst ; C.Word64 -> OrdEInst + C.Float -> OrdEInst ; C.Double -> OrdEInst + +-------------------------------------------------------------------------------- + +data NumEInst a = A.NumE a => NumEInst + +numEInst :: Num a => C.Type a -> NumEInst a +numEInst t = + case t of + C.Bool -> badInst + C.Int8 -> NumEInst ; C.Int16 -> NumEInst + C.Int32 -> NumEInst ; C.Int64 -> NumEInst + C.Word8 -> NumEInst ; C.Word16 -> NumEInst + C.Word32 -> NumEInst ; C.Word64 -> NumEInst + C.Float -> NumEInst ; C.Double -> NumEInst + +-------------------------------------------------------------------------------- + +data IntegralEInst a = A.IntegralE a => IntegralEInst + +integralEInst :: Integral a => C.Type a -> IntegralEInst a +integralEInst t = + case t of + C.Bool -> badInst + C.Int8 -> IntegralEInst ; C.Int16 -> IntegralEInst + C.Int32 -> IntegralEInst ; C.Int64 -> IntegralEInst + C.Word8 -> IntegralEInst ; C.Word16 -> IntegralEInst + C.Word32 -> IntegralEInst ; C.Word64 -> IntegralEInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data FloatingEInst a = A.FloatingE a => FloatingEInst + +floatingEInst :: Floating a => C.Type a -> FloatingEInst a +floatingEInst t = + case t of + C.Float -> FloatingEInst + C.Double -> FloatingEInst + _ -> badInst + +-------------------------------------------------------------------------------- + +data BitsEInst a = ( A.Expr a, A.OrdE a, A.EqE a, A.IntegralE a, Bits a ) => BitsEInst + +bitsEInst :: Bits a => C.Type a -> BitsEInst a +bitsEInst t = + case t of + C.Bool -> badInst + C.Int8 -> BitsEInst + C.Int16 -> BitsEInst + C.Int32 -> BitsEInst + C.Int64 -> BitsEInst + C.Word8 -> BitsEInst + C.Word16 -> BitsEInst + C.Word32 -> BitsEInst + C.Word64 -> BitsEInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- diff --git a/test/CopilotC99Test.hs b/test/CopilotC99Test.hs new file mode 100644 --- /dev/null +++ b/test/CopilotC99Test.hs @@ -0,0 +1,50 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification #-} + +module Main (main) where + +import Copilot.Core.PrettyPrint (prettyPrint) +import Copilot.Core.Random (randomSpec) +import Copilot.Core.Random.Weights (Weights (..), simpleWeights) +import Copilot.Compile.C99.Test.CheckSpec (checkSpec) +import Prelude +import System.Random + +myWeights :: Weights +myWeights = + simpleWeights + { maxExprDepth = 2 + , maxBuffSize = 2 + , maxTriggers = 1 + , maxTrigArgs = 1 + , maxObservers = 0 + , numStreams = 3 + , floatFreq = 0 + , doubleFreq = 0 + , divModFreq = False + } + +testRandomSpec :: IO Bool +testRandomSpec = do + g <- newStdGen + let spec = randomSpec myWeights g + putStrLn "------------------------------------------" + putStrLn "Specification to test:" + putStrLn $ prettyPrint spec + checkSpec 10 spec + +main :: IO () +main = do + putStrLn "Enter the number of random specifications to test:" + i <- readLn :: IO Int + go i + where go 0 = putStrLn "No failures found." + go i = do b <- testRandomSpec + if b then do putStrLn "" + go (i-1) + else do putStrLn "Inconsistency found!" + return () +