copilot-sbv (empty) → 0.1
raw patch · 14 files changed
+1381/−0 lines, 14 filesdep +basedep +containersdep +copilot-coresetup-changed
Dependencies added: base, containers, copilot-core, pretty, sbv
Files
- LICENSE +29/−0
- README.md +54/−0
- Setup.hs +2/−0
- copilot-sbv.cabal +45/−0
- src/Copilot/Compile/SBV.hs +54/−0
- src/Copilot/Compile/SBV/Code.hs +166/−0
- src/Copilot/Compile/SBV/Common.hs +48/−0
- src/Copilot/Compile/SBV/Copilot2SBV.hs +247/−0
- src/Copilot/Compile/SBV/Driver.hs +304/−0
- src/Copilot/Compile/SBV/Makefile.hs +45/−0
- src/Copilot/Compile/SBV/MetaTable.hs +189/−0
- src/Copilot/Compile/SBV/Params.hs +18/−0
- src/Copilot/Compile/SBV/Queue.hs +39/−0
- src/Copilot/Compile/SBV/Witness.hs +141/−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,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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-sbv.cabal view
@@ -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
+ src/Copilot/Compile/SBV.hs view
@@ -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."++--------------------------------------------------------------------------------
+ src/Copilot/Compile/SBV/Code.hs view
@@ -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
+ src/Copilot/Compile/SBV/Common.hs view
@@ -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
+ src/Copilot/Compile/SBV/Copilot2SBV.hs view
@@ -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
+ src/Copilot/Compile/SBV/Driver.hs view
@@ -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 <inttypes.h>")+ wr (text "#include <stdbool.h>")+ wr (text "#include <stdint.h>")+ wr (text "#include <stdio.h>")+ 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."
+ src/Copilot/Compile/SBV/Makefile.hs view
@@ -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})++--------------------------------------------------------------------------------+
+ src/Copilot/Compile/SBV/MetaTable.hs view
@@ -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
+ src/Copilot/Compile/SBV/Params.hs view
@@ -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
+ src/Copilot/Compile/SBV/Queue.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Compile/SBV/Witness.hs view
@@ -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++--------------------------------------------------------------------------------