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,54 @@ +Overview +======== +[copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) Another back-end +that translates to [SBV](http://hackage.haskell.org/package/sbv), using its code +generator to generate hard real-time C code as well. The ad + +Copilot 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-sbv + +However, we strongly recommend you install Copilot, which installs copilot-sbv +and other packages automatically. Execute + + cabal install copilot + +Dependencies +============= +copilot-sbv depends on the [SBV](http://hackage.haskell.org/package/sbv) library +to generate hard real-time C code. + +Resources +========= +[copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) 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-sbv.cabal b/copilot-sbv.cabal new file mode 100644 --- /dev/null +++ b/copilot-sbv.cabal @@ -0,0 +1,45 @@ +cabal-version : >= 1.10 +name : copilot-sbv +version : 0.1 +synopsis : A compiler for CoPilot targeting SBV. +description : Blah blah blah... +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-sbv.git + +library + default-language : Haskell2010 + hs-source-dirs : src + ghc-options : -Wall -fwarn-tabs + ghc-prof-options : -auto-all -caf-all + + build-depends : sbv >= 0.9.21 + , base >= 4.3 && < 5 + , containers >= 0.4 + , copilot-core + , pretty >= 1 + + exposed-modules : Copilot.Compile.SBV + , Copilot.Compile.SBV.Code + , Copilot.Compile.SBV.Common + , Copilot.Compile.SBV.Copilot2SBV + , Copilot.Compile.SBV.MetaTable + , Copilot.Compile.SBV.Params + , Copilot.Compile.SBV.Queue + , Copilot.Compile.SBV.Witness + , Copilot.Compile.SBV.Driver + , Copilot.Compile.SBV.Makefile diff --git a/src/Copilot/Compile/SBV.hs b/src/Copilot/Compile/SBV.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV.hs @@ -0,0 +1,54 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.SBV + ( compile + , module Copilot.Compile.SBV.Params + ) where + +import qualified Copilot.Core as C +import Copilot.Compile.Header.C99 (c99HeaderName, genC99Header) + +import qualified Data.SBV as S + +import Copilot.Compile.SBV.Driver (driver, driverName) +import Copilot.Compile.SBV.Makefile (makefile, makefileName) +import Copilot.Compile.SBV.Code (updateStates, updateObservers, fireTriggers) +import Copilot.Compile.SBV.MetaTable (allocMetaTable) +import Copilot.Compile.SBV.Params + +-------------------------------------------------------------------------------- + +-- Note: we put everything in a directory named by the dirName. + +compile :: Params -> C.Spec -> IO () +compile params spec = do + let meta = allocMetaTable spec + dirName = withPrefix (prefix params) "copilot" + sbvName = withPrefix (prefix params) "internal" + putStrLn "Compiling SBV-generated functions .." + + S.compileToCLib + (Just dirName) + sbvName + ( updateStates meta spec + ++ updateObservers meta spec + ++ fireTriggers meta spec ) + + putStrLn "" + putStrLn $ "Generating Copilot driver " ++ driverName params ++ " .." + driver params meta spec dirName sbvName + + putStrLn "" + putStrLn $ "Generating Copilot header " ++ c99HeaderName (prefix params) ++ " .." + genC99Header (prefix params) dirName spec + + putStrLn "" + putStrLn $ "Generating Copilot driver Makefile rules .." + ++ makefileName params ++ " .." + makefile params dirName sbvName + + putStrLn "Done." + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Compile/SBV/Code.hs b/src/Copilot/Compile/SBV/Code.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Code.hs @@ -0,0 +1,166 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ExistentialQuantification #-} + +module Copilot.Compile.SBV.Code + ( updateStates + , updateObservers + , fireTriggers + ) where + +import Copilot.Compile.SBV.Copilot2SBV +import Copilot.Compile.SBV.MetaTable +import qualified Copilot.Compile.SBV.Witness as W +import Copilot.Compile.SBV.Common + +import qualified Copilot.Core as C +import Copilot.Core.Type.Equality ((=~=), coerce, cong) + +import qualified Data.SBV as S +import qualified Data.SBV.Internals as S + +import qualified Data.Map as M +import Prelude hiding (id) + +-------------------------------------------------------------------------------- + +type SBVFunc = (String, S.SBVCodeGen ()) + +mkSBVFunc :: String -> S.SBVCodeGen () -> (String, S.SBVCodeGen ()) +mkSBVFunc str codeGen = (str, codeGen) + +-------------------------------------------------------------------------------- + +updateStates :: MetaTable -> C.Spec -> [SBVFunc] +updateStates meta (C.Spec streams _ _) = + map updateStreamState streams + + where + updateStreamState :: C.Stream -> SBVFunc + updateStreamState C.Stream { C.streamId = id + , C.streamExpr = e + , C.streamExprType = t1 + } = + mkSBVFunc (mkUpdateStFn id) $ do + inputs <- mkInputs meta (c2Args e) + let e' = c2sExpr inputs e + let Just strmInfo = M.lookup id (streamInfoMap meta) + updateStreamState1 t1 e' strmInfo + + updateStreamState1 :: C.Type a -> S.SBV a -> StreamInfo -> S.SBVCodeGen () + updateStreamState1 t1 e1 (StreamInfo _ t2) = do + W.SymWordInst <- return (W.symWordInst t2) + W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t2) + Just p <- return (t1 =~= t2) + S.cgReturn $ coerce (cong p) e1 + +-------------------------------------------------------------------------------- + +updateObservers :: MetaTable -> C.Spec -> [SBVFunc] +updateObservers meta (C.Spec _ observers _) = + map updateObs observers + + where + updateObs :: C.Observer -> SBVFunc + updateObs C.Observer { C.observerName = name + , C.observerExpr = e + , C.observerExprType = t } = + mkSBVFunc (mkObserverFn name) mkSBVExp + + where + mkSBVExp = + do + inputs <- mkInputs meta (c2Args e) + let e' = c2sExpr inputs e + W.SymWordInst <- return (W.symWordInst t) + W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) + S.cgReturn e' + +-------------------------------------------------------------------------------- + +fireTriggers :: MetaTable -> C.Spec -> [SBVFunc] +fireTriggers meta (C.Spec _ _ triggers) = + concatMap fireTrig triggers + + where + fireTrig :: C.Trigger -> [SBVFunc] + fireTrig C.Trigger { C.triggerName = name + , C.triggerGuard = guard + , C.triggerArgs = args } = + mkSBVFunc (mkTriggerGuardFn name) mkSBVExp + : map (mkTriggerArg name) (mkTriggerArgIdx args) + where + mkSBVExp = do + inputs <- mkInputs meta (c2Args guard) + let e = c2sExpr inputs guard + S.cgReturn e + + mkTriggerArg :: String -> (Int, C.UExpr) -> SBVFunc + mkTriggerArg name (i, C.UExpr { C.uExprExpr = e + , C.uExprType = t } ) = + mkSBVFunc (mkTriggerArgFn i name) mkExpr + where + mkExpr = do + inputs <- mkInputs meta (c2Args e) + let e' = c2sExpr inputs e + W.SymWordInst <- return (W.symWordInst t) + W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) + S.cgReturn e' + +-------------------------------------------------------------------------------- + +-- We first need to analyze the expression, running down it to get all the drop +-- ids and externals mentioned in it. The we use those inputs to process the +-- expression. XXX MUST be put in the monad in the same order as the function +-- call (argToCall from MetaTable.hs). + +mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen [Input] +mkInputs meta args = + mapM argToInput args + + where + argToInput :: Arg -> S.SBVCodeGen Input + argToInput (Extern name) = + let extInfos = externInfoMap meta in + let Just extInfo = M.lookup name extInfos in + mkExtInput extInfo + + where + mkExtInput :: C.UType -> S.SBVCodeGen Input + mkExtInput C.UType { C.uTypeType = t } = do + ext <- mkExtInput_ t + return $ ExtIn name (ExtInput { extInput = ext + , extType = t }) + + mkExtInput_ :: C.Type a -> S.SBVCodeGen (S.SBV a) + mkExtInput_ t = do + W.SymWordInst <- return (W.symWordInst t) + W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) + ext <- S.cgInput (mkExtTmpVar name) + return ext + + argToInput (Queue id) = + let strmInfos = streamInfoMap meta in + let Just strmInfo = M.lookup id strmInfos in + mkArrInput strmInfo + + where + mkArrInput :: StreamInfo -> S.SBVCodeGen Input + mkArrInput StreamInfo { streamInfoQueue = que + , streamInfoType = t } = do + arr <- mkArrInput_ t que + ptr <- S.cgInput (mkQueuePtrVar id) + + return $ ArrIn id (ArrInput (QueueIn { queue = arr + , quePtr = ptr + , arrType = t })) + + mkArrInput_ :: C.Type a -> [a] -> S.SBVCodeGen [S.SBV a] + mkArrInput_ t que = do + W.SymWordInst <- return (W.symWordInst t) + W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) + arr <- S.cgInputArr (length que) (mkQueueVar id) + return arr diff --git a/src/Copilot/Compile/SBV/Common.hs b/src/Copilot/Compile/SBV/Common.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Common.hs @@ -0,0 +1,48 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.SBV.Common + ( mkTmpStVar + , mkUpdateStFn + , mkQueueVar + , mkQueuePtrVar + , mkExtTmpVar + , mkObserverFn + , mkTriggerGuardFn + , mkTriggerArgFn + , mkTriggerArgIdx + ) where + +import Copilot.Core (Id) +import Prelude hiding (id) + +mkVar :: String -> Id -> String +mkVar str id = str ++ show id + +mkTmpStVar :: Id -> String +mkTmpStVar = mkVar "tmp_" + +mkUpdateStFn :: Id -> String +mkUpdateStFn = mkVar "update_state_" + +mkQueueVar :: Id -> String +mkQueueVar = mkVar "queue_" + +mkQueuePtrVar :: Id -> String +mkQueuePtrVar = mkVar "ptr_" + +mkExtTmpVar :: String -> String +mkExtTmpVar = ("ext_" ++) + +mkObserverFn :: String -> String +mkObserverFn = ("observer_" ++) + +mkTriggerGuardFn :: String -> String +mkTriggerGuardFn = ("trigger_guard_" ++) + +mkTriggerArgFn :: Int -> String -> String +mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i + +mkTriggerArgIdx :: [a] -> [(Int, a)] +mkTriggerArgIdx args = zip [0,1 ..] args diff --git a/src/Copilot/Compile/SBV/Copilot2SBV.hs b/src/Copilot/Compile/SBV/Copilot2SBV.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Copilot2SBV.hs @@ -0,0 +1,247 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +module Copilot.Compile.SBV.Copilot2SBV + ( c2sExpr + , Input(..) + , ExtInput(..) + , ArrInput(..) + , QueueIn(..) + ) +where + +import Prelude hiding (id) +import Data.Map (Map) +import qualified Data.Map as M + +import qualified Data.SBV as S +import qualified Data.SBV.Internals as S + +import qualified Copilot.Compile.SBV.Queue as Q +import qualified Copilot.Compile.SBV.Witness as W + +import Copilot.Core (Op1 (..), Op2 (..), Op3 (..), badUsage) +import qualified Copilot.Core as C +import Copilot.Core.Type.Equality ((=~=), coerce, cong) + + +-------------------------------------------------------------------------------- + +data Input = + ExtIn C.Name ExtInput + | ArrIn C.Id ArrInput + +data ExtInput = forall a. ExtInput + { extInput :: S.SBV a + , extType :: C.Type a } + +data ArrInput = forall a. ArrInput + { arrInput :: QueueIn a } + +data QueueIn a = QueueIn + { queue :: [S.SBV a] + , quePtr :: S.SBV Q.QueueSize + , arrType :: C.Type a } + +-------------------------------------------------------------------------------- + +c2sExpr :: [Input] -> C.Expr a -> S.SBV a +c2sExpr inputs e = c2sExpr_ e M.empty inputs + +-------------------------------------------------------------------------------- + +data Local = forall a . Local + { localSBVExpr :: S.SBV a + , localType :: C.Type a } + +type Env = Map C.Name Local + +-------------------------------------------------------------------------------- + +c2sExpr_ :: C.Expr a -> Env -> [Input] -> S.SBV a +c2sExpr_ e0 env inputs = case e0 of + + C.Const t x -> + case W.symWordInst t of W.SymWordInst -> S.literal x + + ---------------------------------------------------- + + C.Drop t i id -> + let que :: ArrInput + Just que = foldl + ( \acc x -> case x of + ArrIn id' q -> if id' == id then Just q + else acc + ExtIn _ _ -> acc ) + Nothing + inputs + in + drop1 t que + + where + drop1 :: C.Type a -> ArrInput -> S.SBV a + drop1 t1 ArrInput { arrInput = QueueIn { queue = que + , quePtr = qPtr + , arrType = t2 } } = + let Just p = t2 =~= t1 in + case W.symWordInst t2 of + W.SymWordInst -> + case W.hasSignAndSizeInst t2 of + W.HasSignAndSizeInst -> + coerce (cong p) (Q.lookahead i que qPtr) + + ---------------------------------------------------- + + C.Local t1 _ name e1 e2 -> + let e1' = c2sExpr_ e1 env inputs in + let env' = M.insert name (Local e1' t1) env in + c2sExpr_ e2 env' inputs + + ---------------------------------------------------- + + C.Var t1 name -> + let Just local = M.lookup name env + in + case local of + Local + { localSBVExpr = e + , localType = t2 + } -> + let Just p = t2 =~= t1 + in coerce (cong p) e + + ---------------------------------------------------- + + C.ExternVar t name -> + let ext :: ExtInput + Just ext = foldl + ( \acc x -> case x of + ArrIn _ _ -> acc + ExtIn nm e -> if nm == name then Just e + else acc ) + Nothing + inputs + in getSBV t ext + + where + getSBV :: C.Type a -> ExtInput -> S.SBV a + getSBV t1 ExtInput { extInput = ext + , extType = t2 } = + let Just p = t2 =~= t1 in + coerce (cong p) ext + + ---------------------------------------------------- + + -- externFun t name _ = C2AExpr $ \ _ meta -> + -- let Just extFunInfo = M.lookup name (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.Op1 op e -> + let res1 = c2sExpr_ e env inputs in + c2sOp1 op res1 + + ---------------------------------------------------- + + C.Op2 op e1 e2 -> + let res1 = c2sExpr_ e1 env inputs in + let res2 = c2sExpr_ e2 env inputs in + c2sOp2 op res1 res2 + + ---------------------------------------------------- + + C.Op3 op e1 e2 e3 -> + let res1 = c2sExpr_ e1 env inputs in + let res2 = c2sExpr_ e2 env inputs in + let res3 = c2sExpr_ e3 env inputs in + c2sOp3 op res1 res2 res3 + +-------------------------------------------------------------------------------- + +noFloatOpsErr :: String -> a +noFloatOpsErr op = + badUsage ("Floating/Double operators not supported for the SBV backend: " + ++ "operator " ++ op ++ " not supported.") + +-------------------------------------------------------------------------------- + +c2sOp1 :: C.Op1 a b -> S.SBV a -> S.SBV b +c2sOp1 op = case op of + Not -> \x -> S.ite (x S..== S.false) S.true S.false + Abs t -> case W.symWordInst t of + W.SymWordInst -> abs + Sign t -> case W.symWordInst t of + W.SymWordInst -> signum + BwNot t -> case W.bitsInst t of + W.BitsInst -> (S.complement) + + Recip _ -> noFloatOpsErr "recip" + Exp _ -> noFloatOpsErr "exp" + Sqrt _ -> noFloatOpsErr "sqrt" + Log _ -> noFloatOpsErr "log" + Sin _ -> noFloatOpsErr "sin" + Tan _ -> noFloatOpsErr "tan" + Cos _ -> noFloatOpsErr "cos" + Asin _ -> noFloatOpsErr "asin" + Atan _ -> noFloatOpsErr "atan" + Acos _ -> noFloatOpsErr "acos" + Sinh _ -> noFloatOpsErr "sinh" + Tanh _ -> noFloatOpsErr "tanh" + Cosh _ -> noFloatOpsErr "cosh" + Asinh _ -> noFloatOpsErr "asinh" + Atanh _ -> noFloatOpsErr "atanh" + Acosh _ -> noFloatOpsErr "acosh" + +-------------------------------------------------------------------------------- + +c2sOp2 :: C.Op2 a b c -> S.SBV a -> S.SBV b -> S.SBV c +c2sOp2 op = case op of + And -> \x y -> S.ite (x S..== S.false) + S.false + (S.ite (y S..== S.false) S.false S.true) + Or -> \x y -> S.ite (x S..== S.false) + (S.ite (y S..== S.false) S.false S.true) + S.true + Add t -> case W.symWordInst t of W.SymWordInst -> (+) + Sub t -> case W.symWordInst t of W.SymWordInst -> (-) + Mul t -> case W.symWordInst t of W.SymWordInst -> (*) + + Eq t -> case W.eqInst t of W.EqInst -> (S..==) + Ne t -> case W.eqInst t of W.EqInst -> (S../=) + Le t -> case W.ordInst t of W.OrdInst -> (S..<=) + Ge t -> case W.ordInst t of W.OrdInst -> (S..>=) + Lt t -> case W.ordInst t of W.OrdInst -> (S..<) + Gt t -> case W.ordInst t of W.OrdInst -> (S..>) + + Div t -> case W.divInst t of W.BVDivisibleInst -> + \x y -> fst (S.bvQuotRem x y) + Mod t -> case W.divInst t of W.BVDivisibleInst -> + \x y -> snd (S.bvQuotRem x y) + + BwAnd t -> case W.bitsInst t of W.BitsInst -> (S..&.) + BwOr t -> case W.bitsInst t of W.BitsInst -> (S..|.) + BwXor t -> case W.bitsInst t of W.BitsInst -> (S.xor) + + Fdiv _ -> noFloatOpsErr "fdiv" + Pow _ -> noFloatOpsErr "pow" + Logb _ -> noFloatOpsErr "logb" + +c2sOp3 :: C.Op3 a b c d -> S.SBV a -> S.SBV b -> S.SBV c -> S.SBV d +c2sOp3 op = case op of + Mux t -> + case W.mergeableInst t of + W.MergeableInst -> \b c1 c2 -> S.ite b c1 c2 diff --git a/src/Copilot/Compile/SBV/Driver.hs b/src/Copilot/Compile/SBV/Driver.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Driver.hs @@ -0,0 +1,304 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification, GADTs #-} + +-- | Generates the code around the SBV functions to hold the state-updates, +-- external variables, etc. + +module Copilot.Compile.SBV.Driver + ( driver + , driverName + ) where + +import Prelude hiding (id) +import qualified Data.Map as M +import Data.List (intersperse) +import qualified System.IO as I +import Text.PrettyPrint.HughesPJ + +import Copilot.Compile.SBV.MetaTable +import Copilot.Compile.SBV.Queue (QueueSize) +import Copilot.Compile.SBV.Common +import Copilot.Compile.SBV.Params + +import qualified Copilot.Core as C +import qualified Copilot.Core.Type.Show as C (showWithType, ShowType(..)) +import Copilot.Compile.Header.C99 (c99HeaderName) + +-------------------------------------------------------------------------------- + +driverName :: Params -> String +driverName params = withPrefix (prefix params) "driver" ++ ".c" + +-------------------------------------------------------------------------------- + +-- | Define a C function. +mkFunc :: String -> Doc -> Doc +mkFunc fnName doc = + text "void" <+> text fnName + <> lparen <> text "void" <> rparen <+> lbrace + $$ nest 2 doc $$ nest 0 rbrace + +mkArgs :: [Doc] -> Doc +mkArgs args = hsep (punctuate comma args) + +mkFuncCall :: String -> [Doc] -> Doc +mkFuncCall f args = text f <> lparen <> mkArgs args <> rparen + +-------------------------------------------------------------------------------- + +driver :: Params -> MetaTable -> C.Spec -> String -> String -> IO () +driver params meta (C.Spec streams observers _) dir fileName = do + let filePath = dir ++ '/' : driverName params + h <- I.openFile filePath I.WriteMode + let wr doc = I.hPutStrLn h (mkStyle doc) + + wr ( text "/*" + <+> text "Driver for SBV program generated from Copilot." + <+> text "*/") + wr (text "/*" <+> text "Edit as you see fit" <+> text "*/") + wr (text "") + + wr (text "#include ") + wr (text "#include ") + wr (text "#include ") + wr (text "#include ") + wr (text "#include" <+> doubleQuotes (text fileName <> text ".h")) + wr (text "#include" <+> doubleQuotes (text $ c99HeaderName (prefix params))) + wr (text "") + + wr (declObservers (prefix params) observers) + wr (text "") + + wr (varDecls meta) + wr (text "") + + wr copilot + wr (text "") + wr driverFn + + where + mkStyle :: Doc -> String + mkStyle = renderStyle (style {lineLength = 80}) + + driverFn :: Doc + driverFn = + mkFunc (withPrefix (prefix params) "step") + ( mkFuncCall sampleExtsF [] <> semi + $$ mkFuncCall updateStatesF [] <> semi + $$ mkFuncCall observersF [] <> semi + $$ mkFuncCall triggersF [] <> semi + $$ mkFuncCall updateBuffersF [] <> semi + $$ mkFuncCall updatePtrsF [] <> semi) + + copilot = vcat $ intersperse (text "") + [ sampleExts meta + , updateStates streams + , fireTriggers meta + , updateObservers params meta + , updateBuffers meta + , updatePtrs meta ] + +-------------------------------------------------------------------------------- + +-- Declare gloabl variables. + +data Decl = Decl { retT :: Doc + , declVar :: Doc + , initVal :: Doc } + +varDecls :: MetaTable -> Doc +varDecls meta = vcat $ map varDecl (getVars meta) + + where + getVars :: MetaTable -> [Decl] + getVars MetaTable { streamInfoMap = streams + , externInfoMap = externs } = + map getTmpStVars (M.toList streams) + ++ map getQueueVars (M.toList streams) + ++ map getQueuePtrVars (map fst $ M.toList streams) + ++ map getExtVars (M.toList externs) + + getTmpStVars :: (C.Id, StreamInfo) -> Decl + getTmpStVars (id, StreamInfo { streamInfoType = t + , streamInfoQueue = que }) = + Decl (retType t) (text $ mkTmpStVar id) getFirst + where + -- ASSUME queue is nonempty! + getFirst = text (cShow $ C.showWithType C.Haskell t (headErr que)) + headErr [] = C.impossible "headErr" "copilot-sbv" + headErr xs = head xs + + getQueueVars :: (C.Id, StreamInfo) -> Decl + getQueueVars (id, StreamInfo { streamInfoType = t + , streamInfoQueue = que }) = + Decl (retType t) + (text (mkQueueVar id) <> lbrack <> int (length que) <> rbrack) + getInits + where + getInits = lbrace <+> vals <+> rbrace + where + vals = hcat $ punctuate (comma <> text " ") + (map (text . cShow . C.showWithType C.Haskell t) + que) + + getQueuePtrVars :: C.Id -> Decl + getQueuePtrVars id = + Decl (retType queSize) (text $ mkQueuePtrVar id) (int 0) + where + queSize :: C.Type QueueSize + queSize = C.typeOf + + getExtVars :: (C.Name, C.UType) -> Decl + getExtVars (var, C.UType { C.uTypeType = t }) = + Decl (retType t) (text $ mkExtTmpVar var) (int 0) + + varDecl :: Decl -> Doc + varDecl Decl { retT = t, declVar = v, initVal = i } = + t <+> v <+> equals <+> i <> semi + + cShow :: String -> String + cShow "True" = show (1::Int) + cShow "False" = show (0::Int) + cShow x = x + +-------------------------------------------------------------------------------- + +declObservers :: Maybe String -> [C.Observer] -> Doc +declObservers prfx = vcat . map declObserver + + where + declObserver :: C.Observer -> Doc + declObserver + C.Observer + { C.observerName = name + , C.observerExprType = t } = + retType t <+> text (withPrefix prfx name) <> text ";" + +-------------------------------------------------------------------------------- + +sampleExts :: MetaTable -> Doc +sampleExts MetaTable { externInfoMap = extMap } = + mkFunc sampleExtsF $ vcat $ map sampleExt ((fst . unzip . M.toList) extMap) + + where + sampleExt :: C.Name -> Doc + sampleExt name = text (mkExtTmpVar name) <+> equals <+> text name <> semi + +-------------------------------------------------------------------------------- + +updateStates :: [C.Stream] -> Doc +updateStates streams = + mkFunc updateStatesF $ vcat $ map updateSt streams + + where + -- tmp_X = updateState(arg0, arg1, ... ); + updateSt :: C.Stream -> Doc + updateSt C.Stream { C.streamId = id + , C.streamExpr = e } = + text (mkTmpStVar id) <+> equals + <+> mkFuncCall (mkUpdateStFn id) + (map text getArgs) + <> semi + where + getArgs :: [String] + getArgs = concatMap argToCall (c2Args e) + +-------------------------------------------------------------------------------- + +updateObservers :: Params -> MetaTable -> Doc +updateObservers params MetaTable { observerInfoMap = observers } = + + mkFunc observersF $ vcat $ map updateObsv (M.toList observers) + + where + updateObsv :: (C.Name, ObserverInfo) -> Doc + updateObsv (name, ObserverInfo { observerArgs = args }) = + text (withPrefix (prefix params) name) <+> text "=" <+> + mkFuncCall (mkObserverFn name) (map text args) <> semi + +-------------------------------------------------------------------------------- + +fireTriggers :: MetaTable -> Doc +fireTriggers MetaTable { triggerInfoMap = triggers } = + + mkFunc triggersF $ vcat $ map fireTrig (M.toList triggers) + + where + -- if (guard) trigger(args); + fireTrig :: (C.Name, TriggerInfo) -> Doc + fireTrig (name, TriggerInfo { guardArgs = gArgs + , triggerArgArgs = argArgs }) = + text "if" <+> lparen <> guardF <> rparen <+> + mkFuncCall name (map mkArg (mkTriggerArgIdx argArgs)) <> semi + where + guardF :: Doc + guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs) + mkArg :: (Int, [String]) -> Doc + mkArg (i, args) = + mkFuncCall (mkTriggerArgFn i name) (map text args) + +-------------------------------------------------------------------------------- + +updateBuffers :: MetaTable -> Doc +updateBuffers MetaTable { streamInfoMap = strMap } = + mkFunc updateBuffersF $ vcat $ map updateBuf (M.toList strMap) + + where + updateBuf :: (C.Id, StreamInfo) -> Doc + updateBuf (id, _) = + updateFunc (mkQueueVar id) (mkQueuePtrVar id) (mkTmpStVar id) + + -- queue_strX[ptr] = newVal; + updateFunc :: String -> String -> String -> Doc + updateFunc que ptr tmp = + text que <> lbrack <> text ptr <> rbrack <+> equals <+> text tmp <> semi + +-------------------------------------------------------------------------------- + +updatePtrs :: MetaTable -> Doc +updatePtrs MetaTable { streamInfoMap = strMap } = + mkFunc updatePtrsF $ vcat $ map varAndUpdate (M.toList strMap) + + where + varAndUpdate :: (C.Id, StreamInfo) -> Doc + varAndUpdate (id, StreamInfo { streamInfoQueue = que }) = + updateFunc (fromIntegral $ length que) (mkQueuePtrVar id) + + -- idx = (idx + 1) % queueSize; + updateFunc :: QueueSize -> String -> Doc + updateFunc sz ptr = + text ptr <+> equals + <+> lparen <> text ptr <+> text "+" <+> int 1 <> rparen + <+> text "%" <+> int (fromIntegral sz) <> semi + +-------------------------------------------------------------------------------- + +sampleExtsF, triggersF, observersF, updatePtrsF, updateBuffersF, updateStatesF :: String +updatePtrsF = "updatePtrs" +updateBuffersF = "updateBuffers" +updateStatesF = "updateStates" +triggersF = "fireTriggers" +observersF = "updateObservers" +sampleExtsF = "sampleExts" + +-------------------------------------------------------------------------------- + +retType :: C.Type a -> Doc +retType t = text $ + case t of + C.Bool -> "SBool" + + C.Int8 -> "SInt8" + C.Int16 -> "SInt16" + C.Int32 -> "SInt32" + C.Int64 -> "SInt64" + + C.Word8 -> "SWord8" + C.Word16 -> "SWord16" + C.Word32 -> "SWord32" + C.Word64 -> "SWord64" + + _ -> C.badUsage "You've tried to compile a Copilot program to SBV with a type SBV does not support. SBV does not support floats or doubles. To compile programs using these types, use the copilot-c99 (Atom) backend. See README.md for more information." diff --git a/src/Copilot/Compile/SBV/Makefile.hs b/src/Copilot/Compile/SBV/Makefile.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Makefile.hs @@ -0,0 +1,45 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.SBV.Makefile + ( makefile + , makefileName + ) where + +import Copilot.Compile.SBV.Driver (driverName) +import Copilot.Compile.SBV.Params +import Text.PrettyPrint.HughesPJ +import qualified System.IO as I + +-------------------------------------------------------------------------------- + +makefileName :: Params -> String +makefileName params = withPrefix (prefix params) "copilot" ++ ".mk" + +-------------------------------------------------------------------------------- + +makefile :: Params -> String -> String -> IO () +makefile params dir sbvName = do + let filePath = dir ++ '/' : (makefileName params) + fileName = "copilot" + h <- I.openFile filePath I.WriteMode + let wr doc = I.hPutStrLn h (mkStyle doc) + wr (text "# Makefile rules for the Copilot driver.") + wr (text "") + wr $ text "driver" <> colon + <+> text (driverName params) <+> text fileName <> text ".h" + wr $ text "\t" + <> (hsep [ text "$" <> braces (text "CC") + , text "$" <> braces (text "CCFLAGS") + , text "$<" + , text "-o" + , text "$@" + , text sbvName <> text ".a"]) + + where + mkStyle :: Doc -> String + mkStyle = renderStyle (style {lineLength = 80}) + +-------------------------------------------------------------------------------- + diff --git a/src/Copilot/Compile/SBV/MetaTable.hs b/src/Copilot/Compile/SBV/MetaTable.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/MetaTable.hs @@ -0,0 +1,189 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification, GADTs #-} + +module Copilot.Compile.SBV.MetaTable + ( StreamInfo (..) + , StreamInfoMap + , ExternInfoMap + , ExternFunInfo (..) + , ExternFunInfoMap + , TriggerInfo (..) + , TriggerInfoMap + , ObserverInfo (..) + , ObserverInfoMap + , MetaTable (..) + , allocMetaTable + , argToCall + , Arg(..) + , c2Args + ) where + +import Copilot.Compile.SBV.Common +import qualified Copilot.Core as C +--import qualified Copilot.Core.External as C (ExternVar (..), externVars) + +import Data.Map (Map) +import Data.List (nub) +import qualified Data.Map as M +import Prelude hiding (id) + +-------------------------------------------------------------------------------- + +data StreamInfo = forall a . StreamInfo + { streamInfoQueue :: [a] + , streamInfoType :: C.Type a } + +type StreamInfoMap = Map C.Id StreamInfo + +-------------------------------------------------------------------------------- + +type ExternInfoMap = Map C.Name C.UType + +-------------------------------------------------------------------------------- + +data ExternFunInfo = forall a . ExternFunInfo + { externFunInfoArgs :: [(C.UType, C.UExpr)] + , externFunInfoType :: C.Type a } + +type ExternFunInfoMap = Map C.Name ExternFunInfo + +-------------------------------------------------------------------------------- + +data TriggerInfo = TriggerInfo + { guardArgs :: [String] + , triggerArgArgs :: [[String]] } + +type TriggerInfoMap = Map C.Name TriggerInfo + +-------------------------------------------------------------------------------- + +data ObserverInfo = ObserverInfo + { observerArgs :: [String] } + +type ObserverInfoMap = Map C.Name ObserverInfo + +-------------------------------------------------------------------------------- + +data MetaTable = MetaTable + { streamInfoMap :: StreamInfoMap + , externInfoMap :: ExternInfoMap + , externFunInfoMap :: ExternFunInfoMap + , triggerInfoMap :: TriggerInfoMap + , observerInfoMap :: ObserverInfoMap } + +-------------------------------------------------------------------------------- + +allocMetaTable :: C.Spec -> MetaTable +allocMetaTable spec = + let + streamInfoMap_ = M.fromList $ map allocStream (C.specStreams spec) + externInfoMap_ = M.fromList $ map allocExtern (C.externVars spec) + triggerInfoMap_ = M.fromList $ map allocTrigger (C.specTriggers spec) + observerInfoMap_ = M.fromList $ map allocObserver (C.specObservers spec) + in + MetaTable + streamInfoMap_ + externInfoMap_ + (error "undefined in MetaTable.hs in copilot-sbv.") + triggerInfoMap_ + observerInfoMap_ + +-------------------------------------------------------------------------------- + +allocStream :: C.Stream -> (C.Id, StreamInfo) +allocStream C.Stream + { C.streamId = id + , C.streamBuffer = buf + , C.streamExprType = t + } = + let + strmInfo = + StreamInfo + { streamInfoQueue = buf + , streamInfoType = t } in + (id, strmInfo) + +-------------------------------------------------------------------------------- + +allocExtern :: C.ExtVar -> (C.Name, C.UType) +allocExtern (C.ExtVar name t) = + (name, t) + +-------------------------------------------------------------------------------- + +allocTrigger :: C.Trigger -> (C.Name, TriggerInfo) +allocTrigger C.Trigger { C.triggerName = name + , C.triggerGuard = guard + , C.triggerArgs = args } = + let mkArgArgs :: C.UExpr -> [String] + mkArgArgs C.UExpr { C.uExprExpr = e } = + nub (concatMap argToCall (c2Args e)) in + let triggerInfo = + TriggerInfo { guardArgs = nub (concatMap argToCall (c2Args guard)) + , triggerArgArgs = map mkArgArgs args } in + (name, triggerInfo) + +-------------------------------------------------------------------------------- + +allocObserver :: C.Observer -> (C.Name, ObserverInfo) +allocObserver C.Observer { C.observerName = name + , C.observerExpr = e } = + let + observerInfo = + ObserverInfo { observerArgs = nub (concatMap argToCall (c2Args e)) } + in + (name, observerInfo) + +-------------------------------------------------------------------------------- +-- Getting SBV function args from the expressions. + +c2Args :: C.Expr a -> [Arg] +c2Args e = nub $ c2Args_ e + +-- Kinds of arguments to SBV functions +data Arg = Extern C.Name + | ExternFun C.Name + | ExternArr C.Name + | Queue C.Id + deriving Eq + +argToCall :: Arg -> [String] +argToCall (Extern name) = [mkExtTmpVar name] +argToCall (Queue id ) = [ mkQueueVar id + , mkQueuePtrVar id ] + +-- Gathers the names of the arguments to the SBV updateState function so that we +-- can construct the prototypes. + +-- XXX It depends on gathering the the arguments in the same order that SBV uses +-- them. SBV makes the arguments in the order that the cgInput and cgInputArr +-- are pushed into the SBVCodeGen. However, there should really be an API for +-- getting the prototypes. + +c2Args_ :: C.Expr a -> [Arg] +c2Args_ e0 = case e0 of + C.Const _ _ -> [] + + C.Drop _ _ id -> [ Queue id ] + + C.Local _ _ _ e1 e2 -> c2Args_ e1 ++ c2Args_ e2 + + C.Var _ _ -> [] + + C.ExternVar _ name -> [Extern name] + + C.ExternFun _ name args _ -> + ExternFun name : concatMap (\C.UExpr { C.uExprExpr = expr } + -> c2Args expr) + args + + C.ExternArray _ _ name idx _ -> ExternArr name : c2Args_ idx + + C.Op1 _ e -> c2Args_ e + + C.Op2 _ e1 e2 -> c2Args_ e1 ++ c2Args_ e2 + + C.Op3 _ e1 e2 e3 -> c2Args_ e1 ++ c2Args_ e2 ++ c2Args_ e3 diff --git a/src/Copilot/Compile/SBV/Params.hs b/src/Copilot/Compile/SBV/Params.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Params.hs @@ -0,0 +1,18 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +module Copilot.Compile.SBV.Params (Params (..), defaultParams, withPrefix) where + +data Params = Params + { prefix :: Maybe String + } + +defaultParams :: Params +defaultParams = Params + { prefix = Nothing + } + +withPrefix :: Maybe String -> String -> String +withPrefix (Just cs) ds = cs ++ "_" ++ ds +withPrefix _ ds = ds diff --git a/src/Copilot/Compile/SBV/Queue.hs b/src/Copilot/Compile/SBV/Queue.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Queue.hs @@ -0,0 +1,39 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +-- | Implements queues holding stream values. + +module Copilot.Compile.SBV.Queue + ( Queue(..) + , lookahead + , QueueSize + ) where + +import Prelude hiding (id, rem) +import qualified Data.SBV as S +import qualified Data.SBV.Internals as S + +import Copilot.Core.Expr (DropIdx) +import Copilot.Core.Error (impossible) + +-------------------------------------------------------------------------------- + +type QueueSize = DropIdx + +data Queue a = Queue + { queue :: [a] } + +-------------------------------------------------------------------------------- + +lookahead :: (S.HasSignAndSize a, S.SymWord a) + => DropIdx -> [S.SBV a] -> S.SBV QueueSize -> S.SBV a +lookahead i buf ptr = + let sz = fromIntegral $ length buf in + let (_, rem) = (ptr + fromIntegral i) `S.bvQuotRem` sz in + let defaultVal = if null buf + then impossible "lookahead" "copilot-sbv" + else head buf in + S.select buf defaultVal rem + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Compile/SBV/Witness.hs b/src/Copilot/Compile/SBV/Witness.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Compile/SBV/Witness.hs @@ -0,0 +1,141 @@ +-------------------------------------------------------------------------------- +-- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +-------------------------------------------------------------------------------- + +{-# LANGUAGE FlexibleContexts, GADTs #-} + +module Copilot.Compile.SBV.Witness + ( SymWordInst(..) , symWordInst + , HasSignAndSizeInst(..), hasSignAndSizeInst + , EqInst(..) , eqInst + , BVDivisibleInst(..) , divInst + , OrdInst(..) , ordInst + , MergeableInst(..) , mergeableInst + , BitsInst(..) , bitsInst + ) where + +import qualified Data.SBV as S +import qualified Data.SBV.Internals as S +import qualified Copilot.Core as C + +import Data.Bits + +-------------------------------------------------------------------------------- + +badInst :: a +badInst = C.impossible "witnesses" "copilot-sbv" + +-------------------------------------------------------------------------------- + +data SymWordInst a = S.SymWord a => SymWordInst + +symWordInst :: C.Type a -> SymWordInst a +symWordInst t = + case t of + C.Bool -> SymWordInst + C.Int8 -> SymWordInst ; C.Int16 -> SymWordInst + C.Int32 -> SymWordInst ; C.Int64 -> SymWordInst + C.Word8 -> SymWordInst ; C.Word16 -> SymWordInst + C.Word32 -> SymWordInst ; C.Word64 -> SymWordInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data HasSignAndSizeInst a = S.HasSignAndSize a => HasSignAndSizeInst + +hasSignAndSizeInst :: C.Type a -> HasSignAndSizeInst a +hasSignAndSizeInst t = + case t of + C.Bool -> HasSignAndSizeInst + C.Int8 -> HasSignAndSizeInst + C.Int16 -> HasSignAndSizeInst + C.Int32 -> HasSignAndSizeInst + C.Int64 -> HasSignAndSizeInst + C.Word8 -> HasSignAndSizeInst + C.Word16 -> HasSignAndSizeInst + C.Word32 -> HasSignAndSizeInst + C.Word64 -> HasSignAndSizeInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data EqInst a = S.EqSymbolic (S.SBV a) => EqInst + +eqInst :: C.Type a -> EqInst a +eqInst t = + case t of + C.Bool -> EqInst + C.Int8 -> EqInst ; C.Int16 -> EqInst + C.Int32 -> EqInst ; C.Int64 -> EqInst + C.Word8 -> EqInst ; C.Word16 -> EqInst + C.Word32 -> EqInst ; C.Word64 -> EqInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data BVDivisibleInst a = S.BVDivisible (S.SBV a) => BVDivisibleInst + +divInst :: C.Type a -> BVDivisibleInst a +divInst t = + case t of + C.Bool -> badInst + C.Int8 -> badInst + C.Int16 -> badInst + C.Int32 -> badInst + C.Int64 -> badInst + C.Word8 -> BVDivisibleInst + C.Word16 -> BVDivisibleInst + C.Word32 -> BVDivisibleInst + C.Word64 -> BVDivisibleInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data OrdInst a = S.OrdSymbolic (S.SBV a) => OrdInst + +ordInst :: C.Type a -> OrdInst a +ordInst t = + case t of + C.Bool -> OrdInst + C.Int8 -> OrdInst ; C.Int16 -> OrdInst + C.Int32 -> OrdInst ; C.Int64 -> OrdInst + C.Word8 -> OrdInst ; C.Word16 -> OrdInst + C.Word32 -> OrdInst ; C.Word64 -> OrdInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data MergeableInst a = S.Mergeable (S.SBV a) => MergeableInst + +mergeableInst :: C.Type a -> MergeableInst a +mergeableInst t = + case t of + C.Bool -> MergeableInst + C.Int8 -> MergeableInst ; C.Int16 -> MergeableInst + C.Int32 -> MergeableInst ; C.Int64 -> MergeableInst + C.Word8 -> MergeableInst ; C.Word16 -> MergeableInst + C.Word32 -> MergeableInst ; C.Word64 -> MergeableInst + C.Float -> badInst + C.Double -> badInst + +-------------------------------------------------------------------------------- + +data BitsInst a = (Bits a, S.Bits (S.SBV a)) => BitsInst + +bitsInst :: C.Type a -> BitsInst a +bitsInst t = + case t of + C.Bool -> badInst + C.Int8 -> BitsInst ; C.Int16 -> BitsInst + C.Int32 -> BitsInst ; C.Int64 -> BitsInst + C.Word8 -> BitsInst ; C.Word16 -> BitsInst + C.Word32 -> BitsInst ; C.Word64 -> BitsInst + C.Float -> badInst + C.Double -> badInst + +--------------------------------------------------------------------------------