copilot-sbv 0.1 → 0.2

raw patch · 9 files changed

+624/−222 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• copilot-sbv.cabal +1/−1
• src/Copilot/Compile/SBV.hs +10/−3
• src/Copilot/Compile/SBV/Code.hs +118/−42
• src/Copilot/Compile/SBV/Common.hs +14/−4
• src/Copilot/Compile/SBV/Copilot2SBV.hs +94/−51
• src/Copilot/Compile/SBV/Driver.hs +94/−40
• src/Copilot/Compile/SBV/Makefile.hs +2/−1
• src/Copilot/Compile/SBV/MetaTable.hs +87/−79
• src/Copilot/Compile/SBV/Witness.hs +204/−1

@@ -1,6 +1,6 @@ cabal-version             : >= 1.10 name                      : copilot-sbv-version                   : 0.1+version                   : 0.2 synopsis                  : A compiler for CoPilot targeting SBV. description               : Blah blah blah... license                   : BSD3

@@ -4,6 +4,7 @@  module Copilot.Compile.SBV   ( compile+  , sbvDirName   , module Copilot.Compile.SBV.Params   ) where @@ -14,7 +15,8 @@  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.Code +  (updateStates, updateObservers, fireTriggers, getExtArrs) import Copilot.Compile.SBV.MetaTable (allocMetaTable) import Copilot.Compile.SBV.Params @@ -22,10 +24,13 @@  -- Note: we put everything in a directory named by the dirName. +sbvDirName :: String+sbvDirName = "copilot-sbv"+ compile :: Params -> C.Spec -> IO () compile params spec = do   let meta    = allocMetaTable spec-      dirName = withPrefix (prefix params) "copilot"+      dirName = withPrefix (prefix params) sbvDirName       sbvName = withPrefix (prefix params) "internal"   putStrLn "Compiling SBV-generated functions .." @@ -34,7 +39,9 @@     sbvName     (  updateStates    meta spec     ++ updateObservers meta spec-    ++ fireTriggers    meta spec )+    ++ fireTriggers    meta spec +    ++ getExtArrs      meta +    )    putStrLn ""   putStrLn $ "Generating Copilot driver " ++ driverName params ++ " .."

@@ -9,6 +9,7 @@   ( updateStates   , updateObservers   , fireTriggers+  , getExtArrs   ) where  import Copilot.Compile.SBV.Copilot2SBV@@ -20,9 +21,10 @@ import Copilot.Core.Type.Equality ((=~=), coerce, cong)  import qualified Data.SBV as S-import qualified Data.SBV.Internals as S+--import qualified Data.SBV.Internals as S  import qualified Data.Map as M+import Control.Monad (foldM) import Prelude hiding (id)  --------------------------------------------------------------------------------@@ -43,15 +45,16 @@   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+                                                      } +    = 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+  updateStreamState1 :: C.Type a -> S.SBV a -> C.Stream -> S.SBVCodeGen ()+  updateStreamState1 t1 e1 C.Stream { C.streamExprType = t2 }+    = do     W.SymWordInst <- return (W.symWordInst t2)     W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t2)     Just p <- return (t1 =~= t2)@@ -112,55 +115,128 @@  -------------------------------------------------------------------------------- --- 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).+-- Generate an SBV function that calculates the Copilot expression to get the+-- next index to sample an external array.+getExtArrs :: MetaTable -> [SBVFunc]+getExtArrs meta@(MetaTable { externArrInfoMap = arrs })+  = map mkIdx (M.toList arrs)+  +  where+  mkIdx :: (C.Name, C.ExtArray) -> SBVFunc+  mkIdx (name, C.ExtArray { C.externArrayIdx     = idx+                          , C.externArrayIdxType = t   })+    = +    mkSBVFunc (mkExtArrFn name) mkSBVExpr+    where+    mkSBVExpr :: S.SBVCodeGen ()+    mkSBVExpr = do+      inputs <- mkInputs meta (c2Args idx)+      W.SymWordInst <- return (W.symWordInst t)+      W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)+      S.cgReturn (c2sExpr inputs idx) -mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen [Input]-mkInputs meta args =-  mapM argToInput args+-------------------------------------------------------------------------------- +-- mkInputs takes the datatype containing the entire spec (meta) as well as all+-- possible arguments to the SBV function generating the expression.  From those+-- arguments, it then generates in the SBVCodeGen monad---the actual Inputs---+-- the queues to hold streams as well as external variables.++-- XXX MUST be put in the monad in the same order as the function call+-- (argToCall from MetaTable.hs).++mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen Inputs+mkInputs meta args = +  foldM argToInput (Inputs [] [] [] []) args +   where-  argToInput :: Arg -> S.SBVCodeGen Input-  argToInput (Extern name) = -    let extInfos = externInfoMap meta in+  argToInput :: Inputs -> Arg -> S.SBVCodeGen Inputs++-----------------------------------------+ +  -- External variables+  argToInput acc (Extern name) = +    let extInfos = externVarInfoMap 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.ExtVar -> S.SBVCodeGen Inputs+    mkExtInput (C.ExtVar _ C.UType { C.uTypeType = t }) = do+      ext <- mkExtInput_ t (mkExtTmpVar name)+      return acc { extVars = (name, (ExtInput { extInput = ext +                                              , extType  = t })+                             ) : extVars acc } -    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) =+-- External arrays+  argToInput acc (ExternArr name) = +    let extInfos = externArrInfoMap meta in+    let Just extInfo = M.lookup name extInfos in+    mkExtInput extInfo++    where +    mkExtInput :: C.ExtArray -> S.SBVCodeGen Inputs+    mkExtInput C.ExtArray { C.externArrayElemType = t }+      = do+      v <- mkExtInput_ t (mkExtTmpVar name)+      return acc { extArrs = (name, ExtInput +                                      { extInput  = v+                                      , extType   = t }+                             ) : extArrs acc }++-----------------------------------------++-- External functions+  argToInput acc (ExternFun name tag) =+    let extInfos = externFunInfoMap meta in+    let Just extInfo = M.lookup name extInfos in+    mkExtInput extInfo++    where+    mkExtInput :: C.ExtFun -> S.SBVCodeGen Inputs+    mkExtInput C.ExtFun { C.externFunType = t }+      = do+      v <- mkExtInput_ t (mkExtTmpFun name tag)+      return acc { extFuns = (name, ExtInput +                                      { extInput = v+                                      , extType  = t }+                             ) : extFuns acc }++-----------------------------------------++-- Stream queues+  argToInput acc (Queue id) =     let strmInfos = streamInfoMap meta in     let Just strmInfo = M.lookup id strmInfos in-    mkArrInput strmInfo+    mkQueInput strmInfo      where-    mkArrInput :: StreamInfo -> S.SBVCodeGen Input-    mkArrInput StreamInfo { streamInfoQueue = que-                          , streamInfoType  = t } = do-      arr <- mkArrInput_ t que+    mkQueInput :: C.Stream -> S.SBVCodeGen Inputs+    mkQueInput C.Stream { C.streamBuffer = que+                        , C.streamExprType  = t } = do+      arr <- mkQueInput_ 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+      return acc { extQues = (id, QueInput (QueueIn { queue   = arr+                                                    , quePtr  = ptr+                                                    , arrType = t })+                             ) : extQues acc+                 }+                   +    mkQueInput_ :: C.Type a -> [a] -> S.SBVCodeGen [S.SBV a]+    mkQueInput_ t que = do       W.SymWordInst        <- return (W.symWordInst t)       W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)       arr <- S.cgInputArr (length que) (mkQueueVar id)       return arr++-----------------------------------------++mkExtInput_ :: C.Type a -> String -> S.SBVCodeGen (S.SBV a)+mkExtInput_ t name = do+  W.SymWordInst        <- return (W.symWordInst t)+  W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)+  ext <- S.cgInput name+  return ext

@@ -2,19 +2,23 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +-- Builds names of functions and variables used.+ module Copilot.Compile.SBV.Common   ( mkTmpStVar   , mkUpdateStFn   , mkQueueVar   , mkQueuePtrVar   , mkExtTmpVar+  , mkExtTmpFun+  , mkExtArrFn   , mkObserverFn   , mkTriggerGuardFn   , mkTriggerArgFn   , mkTriggerArgIdx   ) where -import Copilot.Core (Id)+import Copilot.Core (Id, Tag) import Prelude hiding (id)  mkVar :: String -> Id -> String@@ -35,14 +39,20 @@ mkExtTmpVar :: String -> String mkExtTmpVar = ("ext_" ++) +mkExtTmpFun :: String -> Tag -> String+mkExtTmpFun name tag = "ext_" ++ name ++ "_" ++ show tag++mkExtArrFn :: String -> String+mkExtArrFn = (++) "mk_ext_arr_"+ mkObserverFn :: String -> String-mkObserverFn = ("observer_" ++)+mkObserverFn = ("mk_observer_" ++)  mkTriggerGuardFn :: String -> String-mkTriggerGuardFn = ("trigger_guard_" ++)+mkTriggerGuardFn = ("mk_trigger_guard_" ++)  mkTriggerArgFn :: Int -> String -> String-mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i+mkTriggerArgFn i nm = "mk_trigger_" ++ nm ++ "_arg_" ++ show i  mkTriggerArgIdx :: [a] -> [(Int, a)] mkTriggerArgIdx args = zip [0,1 ..] args

@@ -6,9 +6,12 @@  module Copilot.Compile.SBV.Copilot2SBV   ( c2sExpr-  , Input(..)+  , Inputs(..)+  , Ext+--  , ExtArr+  , ExtQue   , ExtInput(..)-  , ArrInput(..)+  , QueInput(..)   , QueueIn(..)   )  where@@ -18,37 +21,45 @@ import qualified Data.Map as M  import qualified Data.SBV as S-import qualified Data.SBV.Internals 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.Error (impossible) import Copilot.Core.Type.Equality ((=~=), coerce, cong) - -------------------------------------------------------------------------------- -data Input = -    ExtIn C.Name ExtInput-  | ArrIn C.Id ArrInput+type Ext = (C.Name, ExtInput)+type ExtQue = (C.Id, QueInput) +-- These are all the inputs to the to the SBV expression we're building.+data Inputs = Inputs+  { extVars  :: [Ext] -- external variables+  , extArrs  :: [Ext] -- external arrays+  , extFuns  :: [Ext] -- external functions+  , extQues  :: [ExtQue] }++-- External input -- variables, arrays, and functions data ExtInput = forall a. ExtInput    { extInput :: S.SBV a   , extType  :: C.Type a } -data ArrInput = forall a. ArrInput +-- Stream queues+data QueInput = forall a. QueInput    { arrInput :: QueueIn a }  data QueueIn a = QueueIn-  { queue  :: [S.SBV a]-  , quePtr :: S.SBV Q.QueueSize +  { queue    :: [S.SBV a]+  , quePtr   :: S.SBV Q.QueueSize    , arrType  :: C.Type a }  -------------------------------------------------------------------------------- -c2sExpr :: [Input] -> C.Expr a -> S.SBV a+c2sExpr :: Inputs -> C.Expr a -> S.SBV a c2sExpr inputs e = c2sExpr_ e M.empty inputs  --------------------------------------------------------------------------------@@ -61,7 +72,19 @@  -------------------------------------------------------------------------------- -c2sExpr_ :: C.Expr a -> Env -> [Input] -> S.SBV a+lookupInput :: Eq a => a -> [(a,b)] -> b+lookupInput id prs =+  case lookup id prs of+    Nothing   -> impossible "lookupInput" "copilot-sbv"+    Just val  -> val++--------------------------------------------------------------------------------++-- Translate a Copilot expression into an SBV expression.  The environment+-- passed in is for tracking let expression bindings (in the Copilot language),+-- and the list of inputs are all the external things needed as input to the SBV+-- function.+c2sExpr_ :: C.Expr a -> Env -> Inputs -> S.SBV a c2sExpr_ e0 env inputs = case e0 of    C.Const t x ->@@ -69,21 +92,13 @@    ---------------------------------------------------- -  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-+  C.Drop t i id -> drop1 t que     where-    drop1 :: C.Type a -> ArrInput -> S.SBV a-    drop1 t1 ArrInput { arrInput = QueueIn { queue   = que +    que :: QueInput+    que = lookupInput id (extQues inputs)++    drop1 :: C.Type a -> QueInput -> S.SBV a+    drop1 t1 QueInput { arrInput = QueueIn { queue   = que'                                            , quePtr  = qPtr                                            , arrType = t2 } } =       let Just p = t2 =~= t1 in@@ -91,7 +106,7 @@         W.SymWordInst ->            case W.hasSignAndSizeInst t2 of             W.HasSignAndSizeInst ->-              coerce (cong p) (Q.lookahead i que qPtr)+              coerce (cong p) (Q.lookahead i que' qPtr)    ---------------------------------------------------- @@ -115,39 +130,46 @@    ---------------------------------------------------- -  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+  C.ExternVar t name _ -> +    getSBV t ext      where +    ext :: ExtInput+    ext = lookupInput name (extVars inputs) +     getSBV :: C.Type a -> ExtInput -> S.SBV a-    getSBV t1 ExtInput { extInput = ext+    getSBV t1 ExtInput { extInput = ext'                        , extType  = t2 } =       let Just p = t2 =~= t1 in-      coerce (cong p) ext+      coerce (cong p) ext'    ---------------------------------------------------- -  -- externFun t name _ = C2AExpr $ \ _ meta ->-  --   let Just extFunInfo = M.lookup name (externFunInfoMap meta) in-  --   externFun1 t extFunInfo+  C.ExternArray _ t name _ _ _ _ -> +    getSBV t getExtArr -  --   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)+    where +    getExtArr :: ExtInput+    getExtArr = lookupInput name (extArrs inputs)++    getSBV t1 ExtInput { extInput  = v+                       , extType = t2 }+      = let Just p = t2 =~= t1 in+        coerce (cong p) v++  ----------------------------------------------------++  C.ExternFun t name _ _ _ ->+    getSBV t getExtFun++    where+    getExtFun :: ExtInput+    getExtFun = lookupInput name (extFuns inputs)++    getSBV t1 ExtInput { extType  = t2+                       , extInput = v }+      = let Just p = t2 =~= t1 in+        coerce (cong p) v     ---------------------------------------------------- @@ -189,6 +211,9 @@   BwNot t -> case W.bitsInst    t of                         W.BitsInst            -> (S.complement) +  Cast t0 t1 -> case W.castInst t0 t1 of +                  W.CastInst -> W.sbvCast+   Recip _ -> noFloatOpsErr "recip"   Exp   _ -> noFloatOpsErr "exp"   Sqrt  _ -> noFloatOpsErr "sqrt"@@ -235,6 +260,20 @@   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)+  BwShiftL tvec tidx -> +    case W.bitsInst tvec of +      W.BitsInst -> +        \vec idx -> case W.symWordInst tidx of+                      W.SymWordInst -> case S.unliteral idx of+                                         Nothing -> badUsage "Using the SBV backend, shiftL only supports constant shift indicies"+                                         Just x  -> S.shiftL vec (fromIntegral x)+  BwShiftR tvec tidx -> +    case W.bitsInst tvec of +      W.BitsInst -> +        \vec idx -> case W.symWordInst tidx of+                      W.SymWordInst -> case S.unliteral idx of+                                         Nothing -> badUsage "Using the SBV backend, shiftR only supports constant shift indicies"+                                         Just x  -> S.shiftR vec (fromIntegral x)    Fdiv  _ -> noFloatOpsErr "fdiv"   Pow   _ -> noFloatOpsErr "pow"@@ -245,3 +284,7 @@   Mux t ->     case W.mergeableInst t of        W.MergeableInst -> \b c1 c2 -> S.ite b c1 c2+++--------------------------------------------------------------------------------+

@@ -24,6 +24,7 @@ import Copilot.Compile.SBV.Params  import qualified Copilot.Core as C+--import Copilot.Core.Type.Equality ((=~=), coerce, cong) import qualified Copilot.Core.Type.Show as C (showWithType, ShowType(..)) import Copilot.Compile.Header.C99 (c99HeaderName) @@ -44,6 +45,7 @@ mkArgs :: [Doc] -> Doc mkArgs args = hsep (punctuate comma args) +-- | Call a C function. mkFuncCall :: String -> [Doc] -> Doc mkFuncCall f args = text f <> lparen <> mkArgs args <> rparen @@ -88,22 +90,24 @@     mkFunc (withPrefix (prefix params) "step")            (   mkFuncCall sampleExtsF    [] <> semi             $$ mkFuncCall updateStatesF  [] <> semi+            $$ mkFuncCall updateBuffersF [] <> semi+            $$ mkFuncCall updatePtrsF    [] <> 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 ]+    , updatePtrs meta +    , updateObservers params meta+    , fireTriggers meta+    ]  -------------------------------------------------------------------------------- --- Declare gloabl variables.+-- Declare global variables.  data Decl = Decl { retT    :: Doc                  , declVar :: Doc@@ -115,15 +119,15 @@   where   getVars :: MetaTable -> [Decl]    getVars MetaTable { streamInfoMap = streams -                    , externInfoMap = externs } = +                    , externVarInfoMap = 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 }) = +  getTmpStVars :: (C.Id, C.Stream) -> Decl+  getTmpStVars (id, C.Stream { C.streamExprType  = t+                               , C.streamBuffer = que }) =      Decl (retType t) (text $ mkTmpStVar id) getFirst     where      -- ASSUME queue is nonempty!@@ -131,9 +135,9 @@     headErr [] = C.impossible "headErr" "copilot-sbv"     headErr xs = head xs   -  getQueueVars :: (C.Id, StreamInfo) -> Decl-  getQueueVars (id, StreamInfo { streamInfoType = t-                               , streamInfoQueue = que }) =+  getQueueVars :: (C.Id, C.Stream) -> Decl+  getQueueVars (id, C.Stream { C.streamExprType = t+                             , C.streamBuffer = que }) =     Decl (retType t)           (text (mkQueueVar id) <> lbrack <> int (length que) <> rbrack)          getInits@@ -151,8 +155,8 @@     queSize :: C.Type QueueSize     queSize = C.typeOf  -  getExtVars :: (C.Name, C.UType) -> Decl-  getExtVars (var, C.UType { C.uTypeType = t }) = +  getExtVars :: (C.Name, C.ExtVar) -> Decl+  getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) =      Decl (retType t) (text $ mkExtTmpVar var) (int 0)    varDecl :: Decl -> Doc@@ -175,44 +179,89 @@     C.Observer       { C.observerName     = name       , C.observerExprType = t } =-    retType t <+> text (withPrefix prfx name) <> text ";"+    retType t <+> text (withPrefix prfx name) <> semi  --------------------------------------------------------------------------------  sampleExts :: MetaTable -> Doc-sampleExts MetaTable { externInfoMap = extMap } =-  mkFunc sampleExtsF $ vcat $ map sampleExt ((fst . unzip . M.toList) extMap)+sampleExts MetaTable { externVarInfoMap = extVMap+                     , externArrInfoMap = extAMap+                     , externFunInfoMap = extFMap } +  =+  -- Arrays and functions have to come after vars.  This is because we may use+  -- the assignment of extVars in the definition of extArrs.  We could write it+  -- differently, but it's easier.  The Analyzer.hs copilot-core prevents arrays+  -- or functions from being used in arrays or functions.+  mkFunc sampleExtsF $ vcat (extVars ++ extArrs ++ extFuns)    where-  sampleExt :: C.Name -> Doc-  sampleExt name = text (mkExtTmpVar name) <+> equals <+> text name <> semi+  extVars = map sampleVExt ((fst . unzip . M.toList) extVMap)+  extArrs = map sampleAExt (M.toList extAMap)+  extFuns = map sampleFExt (M.toList extFMap)  -------------------------------------------------------------------------------- +-- Variables+sampleVExt :: C.Name -> Doc+sampleVExt name = +  text (mkExtTmpVar name) <+> equals <+> text name <> semi++--------------------------------------------------------------------------------+-- Arrays++-- Currenty, Analyze.hs in copilot-language forbids recurssion in+-- external arrays or functions (i.e., an external array can't use another+-- external array to compute it's index), so a lot of what is below isn't+-- currently necessary.+sampleAExt :: (C.Name, C.ExtArray) -> Doc+sampleAExt (name, C.ExtArray { C.externArrayIdx = idx })+  = +  text (mkExtTmpVar name) <+> equals <+> arrIdx name idx+ +  where +  arrIdx :: C.Name -> C.Expr a -> Doc+  arrIdx name' e = +    text name' <> lbrack <> idxFCall e <> rbrack <> semi++  -- Ok, because the analyzer disallows arrays or function calls in index+  -- expressions, and we assign all variables before arrays.+  idxFCall :: C.Expr a -> Doc+  idxFCall e = +    mkFuncCall (mkExtArrFn name) (map text $ collectArgs e)++--------------------------------------------------------------------------------++-- External functions+sampleFExt :: (C.Name, C.ExtFun) -> Doc+sampleFExt (name, C.ExtFun { C.externFunArgs = args })+  = +  text (mkExtTmpVar name) <+> equals <+> text name <> lparen+    <+> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args))+    <> rparen <> semi++     where+     mkArgCall = undefined--  (i, ( C.UType { C.uTypeType = t}++--------------------------------------------------------------------------------+ 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)+                     (map text $ collectArgs e)+      <>  semi  --------------------------------------------------------------------------------  updateObservers :: Params -> MetaTable -> Doc-updateObservers params MetaTable { observerInfoMap = observers } =-+updateObservers params MetaTable { observerInfoMap = observers } +  =   mkFunc observersF $ vcat $ map updateObsv (M.toList observers)-   where   updateObsv :: (C.Name, ObserverInfo) -> Doc   updateObsv (name, ObserverInfo { observerArgs = args }) =@@ -222,20 +271,23 @@ --------------------------------------------------------------------------------  fireTriggers :: MetaTable -> Doc-fireTriggers MetaTable { triggerInfoMap = triggers } =-+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+                              , triggerArgArgs = argArgs }) +    = +    let f = mkFuncCall name (map mkArg (mkTriggerArgIdx argArgs)) <> semi in+    text "if" <+> lparen <> guardF <> rparen $+$ nest 2 f+     where     guardF :: Doc     guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs)+     mkArg :: (Int, [String]) -> Doc     mkArg (i, args) =       mkFuncCall (mkTriggerArgFn i name) (map text args)@@ -243,11 +295,12 @@ --------------------------------------------------------------------------------  updateBuffers :: MetaTable -> Doc-updateBuffers MetaTable { streamInfoMap = strMap } =+updateBuffers MetaTable { streamInfoMap = strMap } +  =   mkFunc updateBuffersF $ vcat $ map updateBuf (M.toList strMap)    where-  updateBuf :: (C.Id, StreamInfo) -> Doc+  updateBuf :: (C.Id, C.Stream) -> Doc   updateBuf (id, _) =     updateFunc (mkQueueVar id) (mkQueuePtrVar id) (mkTmpStVar id) @@ -263,8 +316,8 @@   mkFunc updatePtrsF $ vcat $ map varAndUpdate (M.toList strMap)    where -  varAndUpdate :: (C.Id, StreamInfo) -> Doc-  varAndUpdate (id, StreamInfo { streamInfoQueue = que }) =+  varAndUpdate :: (C.Id, C.Stream) -> Doc+  varAndUpdate (id, C.Stream { C.streamBuffer = que }) =     updateFunc (fromIntegral $ length que) (mkQueuePtrVar id)    -- idx = (idx + 1) % queueSize;@@ -276,7 +329,8 @@  -------------------------------------------------------------------------------- -sampleExtsF, triggersF, observersF, updatePtrsF, updateBuffersF, updateStatesF :: String+sampleExtsF, triggersF, observersF, updatePtrsF :: String+updateBuffersF, updateStatesF :: String updatePtrsF    = "updatePtrs" updateBuffersF = "updateBuffers" updateStatesF  = "updateStates"

@@ -28,7 +28,8 @@   wr (text "# Makefile rules for the Copilot driver.")   wr (text "")   wr $ text "driver" <> colon -        <+> text (driverName params) <+> text fileName <> text ".h"+        <+> text (driverName params) <+> text fileName <> text ".h" +        <+> text "internal.a"   wr $ text "\t"           <> (hsep [ text "$" <> braces (text "CC")                   , text "$" <> braces (text "CCFLAGS")

@@ -5,10 +5,11 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-}  module Copilot.Compile.SBV.MetaTable-  ( StreamInfo (..)-  , StreamInfoMap-  , ExternInfoMap-  , ExternFunInfo (..)+  ( --StreamInfo (..)+    StreamInfoMap+  , ExternVarInfoMap+  , ExternArrInfoMap+--  , ExternFunInfo (..)   , ExternFunInfoMap   , TriggerInfo (..)   , TriggerInfoMap@@ -16,39 +17,26 @@   , ObserverInfoMap   , MetaTable (..)   , allocMetaTable-  , argToCall+  , collectArgs   , 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 Data.Maybe (fromJust) 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+type StreamInfoMap = Map C.Id C.Stream+type ExternVarInfoMap = Map C.Name C.ExtVar+type ExternArrInfoMap = Map C.Name C.ExtArray+type ExternFunInfoMap = Map C.Name C.ExtFun  -------------------------------------------------------------------------------- @@ -69,7 +57,8 @@  data MetaTable = MetaTable   { streamInfoMap     :: StreamInfoMap-  , externInfoMap     :: ExternInfoMap+  , externVarInfoMap  :: ExternVarInfoMap+  , externArrInfoMap  :: ExternArrInfoMap   , externFunInfoMap  :: ExternFunInfoMap   , triggerInfoMap    :: TriggerInfoMap   , observerInfoMap   :: ObserverInfoMap }@@ -79,50 +68,56 @@ 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)+    streamInfoMap_    = M.fromList $ map allocStream     (C.specStreams spec)+    externVarInfoMap_ = M.fromList $ map allocExternVars (C.externVars spec)+    externArrInfoMap_ = M.fromList $ map allocExternArrs (C.externArrays spec)+    externFunInfoMap_ = M.fromList $ map allocExternFuns (C.externFuns 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_+    MetaTable { streamInfoMap    = streamInfoMap_+              , externVarInfoMap = externVarInfoMap_+              , externArrInfoMap = externArrInfoMap_+              , externFunInfoMap = externFunInfoMap_+              , triggerInfoMap   = triggerInfoMap_+              , observerInfoMap  = observerInfoMap_+              }+      +-------------------------------------------------------------------------------- +allocStream :: C.Stream -> (C.Id, C.Stream)+allocStream strm = +  (C.streamId strm, strm)+ -------------------------------------------------------------------------------- -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)+allocExternVars :: C.ExtVar -> (C.Name, C.ExtVar)+allocExternVars var =+  (C.externVarName var, var)  -------------------------------------------------------------------------------- -allocExtern :: C.ExtVar -> (C.Name, C.UType)-allocExtern (C.ExtVar name t) =-  (name, t)+allocExternArrs :: C.ExtArray -> (C.Name, C.ExtArray)+allocExternArrs arr =+  (C.externArrayName arr, arr)  -------------------------------------------------------------------------------- +allocExternFuns :: C.ExtFun -> (C.Name, C.ExtFun)+allocExternFuns fun =+  (C.externFunName fun, fun)++--------------------------------------------------------------------------------+ allocTrigger :: C.Trigger -> (C.Name, TriggerInfo) allocTrigger C.Trigger { C.triggerName  = name                        , C.triggerGuard = guard-                       , C.triggerArgs  = args } = +                       , C.triggerArgs  = args } +  =   let mkArgArgs :: C.UExpr -> [String]-      mkArgArgs C.UExpr { C.uExprExpr = e } = -        nub (concatMap argToCall (c2Args e)) in+      mkArgArgs C.UExpr { C.uExprExpr = e } = collectArgs e in   let triggerInfo = -        TriggerInfo { guardArgs      = nub (concatMap argToCall (c2Args guard))+        TriggerInfo { guardArgs      = collectArgs guard                      , triggerArgArgs = map mkArgArgs args } in   (name, triggerInfo) @@ -130,31 +125,38 @@  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)+                         , C.observerExpr = e } +  = +  let observerInfo = ObserverInfo { observerArgs = collectArgs 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+         | ExternFun C.Name C.Tag          | ExternArr C.Name          | Queue     C.Id   deriving Eq +-- | Normal argument calls. argToCall :: Arg -> [String]-argToCall (Extern name) = [mkExtTmpVar name]-argToCall (Queue id ) = [ mkQueueVar id -                        , mkQueuePtrVar id ]+argToCall (Extern name)        = [mkExtTmpVar name]+argToCall (ExternArr name)     = [mkExtTmpVar name]+argToCall (ExternFun name tag) = [mkExtTmpFun name tag]+argToCall (Queue id)           = [ mkQueueVar id +                                 , mkQueuePtrVar id ] +--------------------------------------------------------------------------------++collectArgs :: C.Expr a -> [String]+collectArgs e = concatMap argToCall (nub $ c2Args e)++-- extCollectArgs :: C.Expr a -> [String]+-- extCollectArgs e = nub (concatMap extArgToCall (c2Args e))++--------------------------------------------------------------------------------+ -- Gathers the names of the arguments to the SBV updateState function so that we -- can construct the prototypes. @@ -163,27 +165,33 @@ -- are pushed into the SBVCodeGen.  However, there should really be an API for -- getting the prototypes. +c2Args :: C.Expr a -> [Arg]+c2Args e = nub $ c2Args_ e+ c2Args_ :: C.Expr a -> [Arg] c2Args_ e0 = case e0 of-  C.Const _ _ -> [] +  C.Const _ _            -> []  -  C.Drop _ _ id -> [ Queue id ]+  C.Drop _ _ id          -> [ Queue id ]  -  C.Local _ _ _ e1 e2 -> c2Args_ e1 ++ c2Args_ e2+  C.Local _ _ _ e1 e2    -> c2Args_ e1 ++ c2Args_ e2 -  C.Var _ _ -> []+  C.Var _ _              -> [] -  C.ExternVar   _ name -> [Extern name]+  C.ExternVar   _ name _ -> [Extern name] -  C.ExternFun   _ name args _ -> -    ExternFun name : concatMap (\C.UExpr { C.uExprExpr = expr } -                                             -> c2Args expr) -                                        args+  C.ExternFun   _ name args _ tag -> +    (ExternFun name (fromJust tag)) : +      concatMap (\C.UExpr { C.uExprExpr = expr } +                     -> c2Args expr) +                args -  C.ExternArray _ _ name idx _ -> ExternArr name : c2Args_ idx+  C.ExternArray _ _ name _ _ _ _  -> [ExternArr name]  -  C.Op1 _ e -> c2Args_ e+  C.Op1 _ e        -> c2Args_ e -  C.Op2 _ e1 e2 -> c2Args_ e1 ++ c2Args_ e2+  C.Op2 _ e1 e2    -> c2Args_ e1 ++ c2Args_ e2    C.Op3 _ e1 e2 e3 -> c2Args_ e1 ++ c2Args_ e2 ++ c2Args_ e3++--------------------------------------------------------------------------------

@@ -2,12 +2,14 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- -{-# LANGUAGE FlexibleContexts, GADTs #-}+{-# LANGUAGE FlexibleContexts, GADTs, MultiParamTypeClasses #-}  module Copilot.Compile.SBV.Witness   ( SymWordInst(..)       , symWordInst+  , NumInst(..)           , numInst   , HasSignAndSizeInst(..), hasSignAndSizeInst   , EqInst(..)            , eqInst +  , CastInst(..)          , castInst   , sbvCast   , BVDivisibleInst(..)   , divInst   , OrdInst(..)           , ordInst    , MergeableInst(..)     , mergeableInst @@ -18,6 +20,8 @@ import qualified Data.SBV.Internals as S import qualified Copilot.Core as C +import Data.Word (Word8, Word16, Word32, Word64)+import Data.Int (Int8, Int16, Int32, Int64) import Data.Bits  --------------------------------------------------------------------------------@@ -42,6 +46,21 @@  -------------------------------------------------------------------------------- +data NumInst a = Num a => NumInst++numInst :: C.Type a -> NumInst a+numInst t =+  case t of+    C.Bool   -> badInst+    C.Int8   -> NumInst ; C.Int16  -> NumInst+    C.Int32  -> NumInst ; C.Int64  -> NumInst+    C.Word8  -> NumInst ; C.Word16 -> NumInst+    C.Word32 -> NumInst ; C.Word64 -> NumInst+    C.Float  -> badInst+    C.Double -> badInst++--------------------------------------------------------------------------------+ data HasSignAndSizeInst a = S.HasSignAndSize a => HasSignAndSizeInst  hasSignAndSizeInst :: C.Type a -> HasSignAndSizeInst a@@ -139,3 +158,187 @@     C.Double -> badInst  --------------------------------------------------------------------------------++data CastInst a b = SBVCast a b => CastInst++castInst :: C.Type a -> C.Type b -> CastInst a b+castInst t0 t1 = +  case t0 of+    C.Bool   -> case t1 of+                  C.Bool    -> CastInst+                  C.Word8   -> CastInst+                  C.Word16  -> CastInst+                  C.Word32  -> CastInst+                  C.Word64  -> CastInst+                  C.Int8    -> CastInst+                  C.Int16   -> CastInst+                  C.Int32   -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst++    C.Word8  -> case t1 of+                  C.Word8   -> CastInst+                  C.Word16  -> CastInst+                  C.Word32  -> CastInst+                  C.Word64  -> CastInst+                  C.Int16   -> CastInst+                  C.Int32   -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Word16 -> case t1 of+                  C.Word16  -> CastInst+                  C.Word32  -> CastInst+                  C.Word64  -> CastInst+                  C.Int32   -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Word32 -> case t1 of+                  C.Word32  -> CastInst+                  C.Word64  -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Word64 -> case t1 of+                  C.Word64  -> CastInst+                  _         -> badInst++    C.Int8   -> case t1 of+                  C.Int8    -> CastInst+                  C.Int16   -> CastInst+                  C.Int32   -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Int16  -> case t1 of+                  C.Int16   -> CastInst+                  C.Int32   -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Int32  -> case t1 of+                  C.Int32   -> CastInst+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Int64  -> case t1 of+                  C.Int64   -> CastInst+                  _         -> badInst+    C.Float  -> badInst+    C.Double -> badInst++--------------------------------------------------------------------------------+-- | A class for casting SBV values.  We return errors for casts allowed by+-- Copilot.++class SBVCast a b where+  sbvCast :: S.SBV a -> S.SBV b++--------------------------------------------------------------------------------++castBool :: (Num a, S.SymWord a) => S.SBV Bool -> S.SBV a+castBool x = case S.unliteral x of+               Just bool -> if bool then 1 else 0+               Nothing   -> S.ite x 1 0++castErr :: a+castErr = C.badUsage $ "the SBV backend does not currently support casts to signed word types"++--------------------------------------------------------------------------------++instance SBVCast Bool Bool where+  sbvCast = id+instance SBVCast Bool Word8 where+  sbvCast = castBool+instance SBVCast Bool Word16 where+  sbvCast = castBool+instance SBVCast Bool Word32 where+  sbvCast = castBool+instance SBVCast Bool Word64 where+  sbvCast = castBool++instance SBVCast Bool Int8 where+  sbvCast = castErr +instance SBVCast Bool Int16 where+  sbvCast = castErr +instance SBVCast Bool Int32 where+  sbvCast = castErr +instance SBVCast Bool Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Word8 Word8 where+  sbvCast = id+instance SBVCast Word8 Word16 where+  sbvCast = S.extend+instance SBVCast Word8 Word32 where+  sbvCast = S.extend . S.extend+instance SBVCast Word8 Word64 where+  sbvCast = S.extend . S.extend . S.extend++instance SBVCast Word8 Int16 where+  sbvCast = castErr +instance SBVCast Word8 Int32 where+  sbvCast = castErr +instance SBVCast Word8 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Word16 Word16 where+  sbvCast = id+instance SBVCast Word16 Word32 where+  sbvCast = S.extend+instance SBVCast Word16 Word64 where+  sbvCast = S.extend . S.extend++instance SBVCast Word16 Int32 where+  sbvCast = castErr +instance SBVCast Word16 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Word32 Word32 where+  sbvCast = id+instance SBVCast Word32 Word64 where+  sbvCast = S.extend++instance SBVCast Word32 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Word64 Word64 where+  sbvCast = id++--------------------------------------------------------------------------------++instance SBVCast Int8 Int8 where+  sbvCast = castErr +instance SBVCast Int8 Int16 where+  sbvCast = castErr +instance SBVCast Int8 Int32 where+  sbvCast = castErr +instance SBVCast Int8 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Int16 Int16 where+  sbvCast = castErr +instance SBVCast Int16 Int32 where+  sbvCast = castErr +instance SBVCast Int16 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Int32 Int32 where+  sbvCast = castErr +instance SBVCast Int32 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------++instance SBVCast Int64 Int64 where+  sbvCast = castErr ++--------------------------------------------------------------------------------+