copilot-c99 (empty) → 0.1
raw patch · 18 files changed
+1584/−0 lines, 18 filesdep +QuickCheckdep +atomdep +basesetup-changed
Dependencies added: QuickCheck, atom, base, bytestring, bytestring-csv, containers, copilot-core, directory, pretty, process, random, text
Files
- LICENSE +29/−0
- README.md +56/−0
- Setup.hs +2/−0
- copilot-c99.cabal +87/−0
- src/Copilot/Compile/C99.hs +49/−0
- src/Copilot/Compile/C99/C2A.hs +259/−0
- src/Copilot/Compile/C99/Common.hs +32/−0
- src/Copilot/Compile/C99/MetaTable.hs +163/−0
- src/Copilot/Compile/C99/Params.hs +20/−0
- src/Copilot/Compile/C99/Phases.hs +254/−0
- src/Copilot/Compile/C99/PrePostCode.hs +57/−0
- src/Copilot/Compile/C99/Queue.hs +56/−0
- src/Copilot/Compile/C99/Test/CheckSpec.hs +76/−0
- src/Copilot/Compile/C99/Test/Driver.hs +156/−0
- src/Copilot/Compile/C99/Test/Iteration.hs +48/−0
- src/Copilot/Compile/C99/Test/ReadCSV.hs +48/−0
- src/Copilot/Compile/C99/Witness.hs +142/−0
- test/CopilotC99Test.hs +50/−0
+ LICENSE view
@@ -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.
+ README.md view
@@ -0,0 +1,56 @@+Overview+========+This package is a Copilot back-end that targets Atom+<http://hackage.haskell.org/package/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.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-c99.cabal view
@@ -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
+ src/Copilot/Compile/C99.hs view
@@ -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
+ src/Copilot/Compile/C99/C2A.hs view
@@ -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
+ src/Copilot/Compile/C99/Common.hs view
@@ -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"
+ src/Copilot/Compile/C99/MetaTable.hs view
@@ -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
+ src/Copilot/Compile/C99/Params.hs view
@@ -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
+ src/Copilot/Compile/C99/Phases.hs view
@@ -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
+ src/Copilot/Compile/C99/PrePostCode.hs view
@@ -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" ++ "();"
+ src/Copilot/Compile/C99/Queue.hs view
@@ -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) }
+ src/Copilot/Compile/C99/Test/CheckSpec.hs view
@@ -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 ()
+ src/Copilot/Compile/C99/Test/Driver.hs view
@@ -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 <stdint.h>"+ , text "#include <inttypes.h>"+ , text "#include <stdio.h>"+ , 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
+ src/Copilot/Compile/C99/Test/Iteration.hs view
@@ -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 }
+ src/Copilot/Compile/C99/Test/ReadCSV.hs view
@@ -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
+ src/Copilot/Compile/C99/Witness.hs view
@@ -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++--------------------------------------------------------------------------------
+ test/CopilotC99Test.hs view
@@ -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 ()+