copilot-sbv 0.3 → 0.4
raw patch · 8 files changed
+183/−118 lines, 8 files
Files
- copilot-sbv.cabal +1/−1
- src/Copilot/Compile/SBV.hs +11/−2
- src/Copilot/Compile/SBV/Code.hs +51/−28
- src/Copilot/Compile/SBV/Common.hs +21/−11
- src/Copilot/Compile/SBV/Copilot2SBV.hs +5/−6
- src/Copilot/Compile/SBV/Driver.hs +61/−31
- src/Copilot/Compile/SBV/Makefile.hs +5/−3
- src/Copilot/Compile/SBV/MetaTable.hs +28/−36
copilot-sbv.cabal view
@@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-sbv-version : 0.3+version : 0.4 synopsis : A compiler for CoPilot targeting SBV. description : Blah blah blah... license : BSD3
src/Copilot/Compile/SBV.hs view
@@ -4,6 +4,7 @@ module Copilot.Compile.SBV ( compile+ , compileWithSBV , sbvDirName , module Copilot.Compile.SBV.Params ) where@@ -16,7 +17,7 @@ import Copilot.Compile.SBV.Driver (driver, driverName) import Copilot.Compile.SBV.Makefile (makefile, makefileName) import Copilot.Compile.SBV.Code - (updateStates, updateObservers, fireTriggers, getExtArrs)+ (updateStates, updateObservers, fireTriggers, getExtArrs, getExtFuns) import Copilot.Compile.SBV.MetaTable (allocMetaTable) import Copilot.Compile.SBV.Params @@ -30,7 +31,11 @@ sbvDirName = "copilot-sbv-codegen" compile :: Params -> C.Spec -> IO ()-compile params spec = do+compile p s = compileWithSBV p [] s++-- | sbvs are optional additional SBVCodeGens to generate.+compileWithSBV :: Params -> [(String, S.SBVCodeGen ())] -> C.Spec -> IO ()+compileWithSBV params sbvs spec0 = do let meta = allocMetaTable spec dirName = withPrefix (prefix params) sbvDirName sbvName = withPrefix (prefix params) "internal"@@ -43,6 +48,8 @@ ++ updateObservers meta spec ++ fireTriggers meta spec ++ getExtArrs meta + ++ getExtFuns meta + ++ sbvs ) putStrLn ""@@ -64,6 +71,8 @@ putStrLn "" putStrLn "Done."++ where spec = C.makeTags spec0 --------------------------------------------------------------------------------
src/Copilot/Compile/SBV/Code.hs view
@@ -10,6 +10,7 @@ , updateObservers , fireTriggers , getExtArrs+ , getExtFuns ) where import Copilot.Compile.SBV.Copilot2SBV@@ -21,7 +22,6 @@ 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 Control.Monad (foldM)@@ -94,25 +94,29 @@ , C.triggerGuard = guard , C.triggerArgs = args } = mkSBVFunc (mkTriggerGuardFn name) mkSBVExp- : map (mkTriggerArg name) (mkTriggerArgIdx args)+ : map go (mkArgIdx args) where+ go (i,e) = mkArgCall meta (mkTriggerArgFn i name) e 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'+-------------------------------------------------------------------------------- +mkArgCall :: MetaTable -> String -> C.UExpr -> SBVFunc+mkArgCall meta fnCallName C.UExpr { C.uExprExpr = e+ , C.uExprType = t } + =+ mkSBVFunc fnCallName 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'+ -------------------------------------------------------------------------------- -- Generate an SBV function that calculates the Copilot expression to get the@@ -122,9 +126,10 @@ = map mkIdx (M.toList arrs) where- mkIdx :: (C.Name, C.ExtArray) -> SBVFunc- mkIdx (name, C.ExtArray { C.externArrayIdx = idx- , C.externArrayIdxType = t })+ mkIdx :: (Int, C.ExtArray) -> SBVFunc+ mkIdx (_, C.ExtArray { C.externArrayName = name+ , C.externArrayIdx = idx+ , C.externArrayIdxType = t }) = mkSBVFunc (mkExtArrFn name) mkSBVExpr where@@ -137,6 +142,24 @@ -------------------------------------------------------------------------------- +-- Generate an SBV function that calculates the Copilot expression to get the+-- next index to sample an external array.+getExtFuns :: MetaTable -> [SBVFunc]+getExtFuns meta@(MetaTable { externFunInfoMap = exts })+ = concatMap mkExtF (M.toList exts)+ + where+ mkExtF :: (Int, C.ExtFun) -> [SBVFunc]+ mkExtF (_, C.ExtFun { C.externFunName = name+ , C.externFunTag = tag+ , C.externFunArgs = args })+ = + map go (mkArgIdx args)+ where+ go (i,e) = mkArgCall meta (mkExtFunArgFn i name tag) e++--------------------------------------------------------------------------------+ -- 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---@@ -152,7 +175,7 @@ where argToInput :: Inputs -> Arg -> S.SBVCodeGen Inputs ------------------------------------------+ ----------------------------------------- -- External variables argToInput acc (Extern name) = @@ -168,45 +191,45 @@ , extType = t }) ) : extVars acc } ------------------------------------------+ ----------------------------------------- --- External arrays- argToInput acc (ExternArr name) = + -- External arrays+ argToInput acc (ExternArr name tag) = let extInfos = externArrInfoMap meta in- let Just extInfo = M.lookup name extInfos in+ let Just extInfo = M.lookup tag extInfos in mkExtInput extInfo where mkExtInput :: C.ExtArray -> S.SBVCodeGen Inputs mkExtInput C.ExtArray { C.externArrayElemType = t } = do- v <- mkExtInput_ t (mkExtTmpVar name)+ v <- mkExtInput_ t (mkExtTmpTag name (Just tag)) return acc { extArrs = (name, ExtInput { extInput = v , extType = t } ) : extArrs acc } ------------------------------------------+ ----------------------------------------- --- External functions+ -- External functions argToInput acc (ExternFun name tag) = let extInfos = externFunInfoMap meta in- let Just extInfo = M.lookup name extInfos in+ let Just extInfo = M.lookup tag extInfos in mkExtInput extInfo where mkExtInput :: C.ExtFun -> S.SBVCodeGen Inputs mkExtInput C.ExtFun { C.externFunType = t } = do- v <- mkExtInput_ t (mkExtTmpFun name tag)+ v <- mkExtInput_ t (mkExtTmpTag name (Just tag)) return acc { extFuns = (name, ExtInput { extInput = v , extType = t } ) : extFuns acc } ------------------------------------------+ ----------------------------------------- --- Stream queues+ -- Stream queues argToInput acc (Queue id) = let strmInfos = streamInfoMap meta in let Just strmInfo = M.lookup id strmInfos in
src/Copilot/Compile/SBV/Common.hs view
@@ -10,15 +10,17 @@ , mkQueueVar , mkQueuePtrVar , mkExtTmpVar- , mkExtTmpFun+ , mkExtTmpTag , mkExtArrFn+ , mkExtFunArgFn , mkObserverFn , mkTriggerGuardFn , mkTriggerArgFn- , mkTriggerArgIdx+ , mkArgIdx+ , tagExtract ) where -import Copilot.Core (Id, Tag)+import Copilot.Core (Id, Tag, impossible) import Prelude hiding (id) mkVar :: String -> Id -> String@@ -39,20 +41,28 @@ mkExtTmpVar :: String -> String mkExtTmpVar = ("ext_" ++) -mkExtTmpFun :: String -> Tag -> String-mkExtTmpFun name tag = "ext_" ++ name ++ "_" ++ show tag+mkExtTmpTag :: String -> Maybe Tag -> String+mkExtTmpTag name tag = "ext_" ++ name ++ "_" ++ show (tagExtract tag) mkExtArrFn :: String -> String-mkExtArrFn = (++) "mk_ext_arr_"+mkExtArrFn = (++) "ext_arr_" +mkExtFunArgFn :: Int -> String -> Maybe Tag -> String+mkExtFunArgFn i nm tag = + "ext_" ++ nm ++ "_" ++ show (tagExtract tag) ++ "_arg" ++ show i+ mkObserverFn :: String -> String-mkObserverFn = ("mk_observer_" ++)+mkObserverFn = ("observer_" ++) mkTriggerGuardFn :: String -> String-mkTriggerGuardFn = ("mk_trigger_guard_" ++)+mkTriggerGuardFn = ("trigger_guard_" ++) mkTriggerArgFn :: Int -> String -> String-mkTriggerArgFn i nm = "mk_trigger_" ++ nm ++ "_arg_" ++ show i+mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i -mkTriggerArgIdx :: [a] -> [(Int, a)]-mkTriggerArgIdx args = zip [0,1 ..] args+mkArgIdx :: [a] -> [(Int, a)]+mkArgIdx args = zip [0,1 ..] args++tagExtract :: Maybe Tag -> Tag+tagExtract Nothing = impossible "tagExtract" "copilot-sbv"+tagExtract (Just tag) = tag
src/Copilot/Compile/SBV/Copilot2SBV.hs view
@@ -8,7 +8,6 @@ ( c2sExpr , Inputs(..) , Ext--- , ExtArr , ExtQue , ExtInput(..) , QueInput(..)@@ -59,11 +58,6 @@ -------------------------------------------------------------------------------- -c2sExpr :: Inputs -> 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 }@@ -77,6 +71,11 @@ case lookup id prs of Nothing -> impossible "lookupInput" "copilot-sbv" Just val -> val++--------------------------------------------------------------------------------++c2sExpr :: Inputs -> C.Expr a -> S.SBV a+c2sExpr inputs e = c2sExpr_ e M.empty inputs --------------------------------------------------------------------------------
src/Copilot/Compile/SBV/Driver.hs view
@@ -5,7 +5,9 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} -- | Generates the code around the SBV functions to hold the state-updates,--- external variables, etc.+-- external variables, etc. Note: this just creates calls to SBV-generated+-- functions, it does not create them! (Use the names from Common.hs to ensure+-- agreement on names.) module Copilot.Compile.SBV.Driver ( driver@@ -24,7 +26,6 @@ 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) @@ -71,9 +72,11 @@ wr (text "#include" <+> doubleQuotes (text $ c99HeaderName (prefix params))) wr (text "") + wr (text "/* Observers */") wr (declObservers (prefix params) observers) wr (text "") + wr (text "/* Variables */") wr (varDecls meta) wr (text "") @@ -89,20 +92,20 @@ driverFn = mkFunc (withPrefix (prefix params) "step") ( mkFuncCall sampleExtsF [] <> semi+ $$ mkFuncCall triggersF [] <> semi+ $$ mkFuncCall observersF [] <> semi $$ mkFuncCall updateStatesF [] <> semi $$ mkFuncCall updateBuffersF [] <> semi $$ mkFuncCall updatePtrsF [] <> semi- $$ mkFuncCall observersF [] <> semi- $$ mkFuncCall triggersF [] <> semi ) copilot = vcat $ intersperse (text "") [ sampleExts meta+ , fireTriggers meta+ , updateObservers params meta , updateStates streams , updateBuffers meta , updatePtrs meta - , updateObservers params meta- , fireTriggers meta ] --------------------------------------------------------------------------------@@ -118,12 +121,19 @@ where getVars :: MetaTable -> [Decl] - getVars MetaTable { streamInfoMap = streams - , externVarInfoMap = externs } = - map getTmpStVars (M.toList streams)- ++ map getQueueVars (M.toList streams)- ++ map getQueuePtrVars (map fst $ M.toList streams)+ getVars MetaTable { streamInfoMap = streams + , externVarInfoMap = externs + , externArrInfoMap = externArrs+ , externFunInfoMap = externFuns }+ = + map getTmpStVars strLst+ ++ map getQueueVars strLst+ ++ map getQueuePtrVars (map fst strLst) ++ map getExtVars (M.toList externs)+ ++ map getExtArrs (M.toList externArrs)+ ++ map getExtFuns (M.toList externFuns)+ where+ strLst = M.toList streams getTmpStVars :: (C.Id, C.Stream) -> Decl getTmpStVars (id, C.Stream { C.streamExprType = t@@ -159,6 +169,20 @@ getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) = Decl (retType t) (text $ mkExtTmpVar var) (int 0) + getExtArrs :: (Int, C.ExtArray) -> Decl + getExtArrs (_, C.ExtArray { C.externArrayName = name+ , C.externArrayElemType = t + , C.externArrayTag = tag })+ =+ Decl (retType t) (text $ mkExtTmpTag name tag) (int 0)++ getExtFuns :: (Int, C.ExtFun) -> Decl+ getExtFuns (_, C.ExtFun { C.externFunName = name+ , C.externFunType = t+ , C.externFunTag = tag })+ =+ Decl (retType t) (text $ mkExtTmpTag name tag) (int 0)+ varDecl :: Decl -> Doc varDecl Decl { retT = t, declVar = v, initVal = i } = t <+> v <+> equals <+> i <> semi@@ -189,9 +213,9 @@ , 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.+ -- the assignment of extVars in the definition of extArrs. The Analyzer.hs+ -- copilot-core prevents arrays or functions from being used in arrays or+ -- functions. mkFunc sampleExtsF $ vcat (extVars ++ extArrs ++ extFuns) where@@ -209,19 +233,19 @@ -------------------------------------------------------------------------------- -- 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 })+-- 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).+sampleAExt :: (Int, C.ExtArray) -> Doc+sampleAExt (_, C.ExtArray { C.externArrayName = name+ , C.externArrayIdx = idx + , C.externArrayTag = t }) = - text (mkExtTmpVar name) <+> equals <+> arrIdx name idx+ text (mkExtTmpTag name t) <+> equals <+> arrIdx name idx where arrIdx :: C.Name -> C.Expr a -> Doc- arrIdx name' e = - text name' <> lbrack <> idxFCall e <> rbrack <> semi+ 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.@@ -232,15 +256,19 @@ -------------------------------------------------------------------------------- -- External functions-sampleFExt :: (C.Name, C.ExtFun) -> Doc-sampleFExt (name, C.ExtFun { C.externFunArgs = args })+sampleFExt :: (Int, C.ExtFun) -> Doc+sampleFExt (_, C.ExtFun { C.externFunName = name+ , C.externFunArgs = args + , C.externFunTag = tag }) = - text (mkExtTmpVar name) <+> equals <+> text name <> lparen- <+> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args))+ text (mkExtTmpTag name tag) <+> equals <+> text name <> lparen+ <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) <> rparen <> semi where- mkArgCall = undefined-- (i, ( C.UType { C.uTypeType = t}+ mkArgCall :: (Int, C.UExpr) -> Doc + mkArgCall (i, C.UExpr { C.uExprExpr = e }) = + mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e) -------------------------------------------------------------------------------- @@ -281,16 +309,18 @@ fireTrig (name, TriggerInfo { guardArgs = gArgs , triggerArgArgs = argArgs }) = - let f = mkFuncCall name (map mkArg (mkTriggerArgIdx argArgs)) <> semi in text "if" <+> lparen <> guardF <> rparen $+$ nest 2 f where+ f = text name <> lparen + <> vcat (punctuate comma $ map mkArg (mkArgIdx argArgs)) + <> rparen <> semi + guardF :: Doc guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs) mkArg :: (Int, [String]) -> Doc- mkArg (i, args) =- mkFuncCall (mkTriggerArgFn i name) (map text args)+ mkArg (i, args) = mkFuncCall (mkTriggerArgFn i name) (map text args) --------------------------------------------------------------------------------
src/Copilot/Compile/SBV/Makefile.hs view
@@ -28,17 +28,19 @@ wr (text "# Makefile rules for the Copilot driver.") wr (text "") wr $ text "driver" <> colon - <+> text (driverName params) <+> text fileName <> text ".h" - <+> text "internal.a"+ <+> text (driverName params) <+> text (withPre fileName) <> text ".h" + <+> archive wr $ text "\t" <> (hsep [ text "$" <> braces (text "CC") , text "$" <> braces (text "CCFLAGS") , text "$<" , text "-o" , text "$@"- , text sbvName <> text ".a"])+ , archive]) where + archive = text sbvName <> text ".a"+ withPre nm = withPrefix (prefix params) nm mkStyle :: Doc -> String mkStyle = renderStyle (style {lineLength = 80})
src/Copilot/Compile/SBV/MetaTable.hs view
@@ -5,11 +5,9 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} module Copilot.Compile.SBV.MetaTable- ( --StreamInfo (..)- StreamInfoMap+ ( StreamInfoMap , ExternVarInfoMap , ExternArrInfoMap--- , ExternFunInfo (..) , ExternFunInfoMap , TriggerInfo (..) , TriggerInfoMap@@ -27,7 +25,6 @@ import Data.Map (Map) import Data.List (nub)-import Data.Maybe (fromJust) import qualified Data.Map as M import Prelude hiding (id) @@ -35,8 +32,8 @@ 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+type ExternArrInfoMap = Map C.Tag C.ExtArray+type ExternFunInfoMap = Map C.Tag C.ExtFun -------------------------------------------------------------------------------- @@ -67,45 +64,40 @@ allocMetaTable :: C.Spec -> MetaTable allocMetaTable spec =- let- 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 = streamInfoMap_- , externVarInfoMap = externVarInfoMap_- , externArrInfoMap = externArrInfoMap_- , externFunInfoMap = externFunInfoMap_- , triggerInfoMap = triggerInfoMap_- , observerInfoMap = observerInfoMap_- }+ MetaTable { streamInfoMap = streamInfoMap_+ , externVarInfoMap = externVarInfoMap_+ , externArrInfoMap = externArrInfoMap_+ , externFunInfoMap = externFunInfoMap_+ , triggerInfoMap = triggerInfoMap_+ , observerInfoMap = observerInfoMap_ }++ where+ 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) -------------------------------------------------------------------------------- allocStream :: C.Stream -> (C.Id, C.Stream)-allocStream strm = - (C.streamId strm, strm)+allocStream strm = (C.streamId strm, strm) -------------------------------------------------------------------------------- allocExternVars :: C.ExtVar -> (C.Name, C.ExtVar)-allocExternVars var =- (C.externVarName var, var)+allocExternVars var = (C.externVarName var, var) -------------------------------------------------------------------------------- -allocExternArrs :: C.ExtArray -> (C.Name, C.ExtArray)-allocExternArrs arr =- (C.externArrayName arr, arr)+allocExternArrs :: C.ExtArray -> (C.Tag, C.ExtArray)+allocExternArrs arr = (tagExtract $ C.externArrayTag arr, arr) -------------------------------------------------------------------------------- -allocExternFuns :: C.ExtFun -> (C.Name, C.ExtFun)-allocExternFuns fun =- (C.externFunName fun, fun)+allocExternFuns :: C.ExtFun -> (C.Tag, C.ExtFun)+allocExternFuns fun = (tagExtract $ C.externFunTag fun, fun) -------------------------------------------------------------------------------- @@ -135,15 +127,15 @@ -- Kinds of arguments to SBV functions data Arg = Extern C.Name | ExternFun C.Name C.Tag- | ExternArr C.Name+ | ExternArr C.Name C.Tag | Queue C.Id deriving Eq -- | Normal argument calls. argToCall :: Arg -> [String] argToCall (Extern name) = [mkExtTmpVar name]-argToCall (ExternArr name) = [mkExtTmpVar name]-argToCall (ExternFun name tag) = [mkExtTmpFun name tag]+argToCall (ExternArr name tag) = [mkExtTmpTag name (Just tag)]+argToCall (ExternFun name tag) = [mkExtTmpTag name (Just tag)] argToCall (Queue id) = [ mkQueueVar id , mkQueuePtrVar id ] @@ -181,12 +173,12 @@ C.ExternVar _ name _ -> [Extern name] C.ExternFun _ name args _ tag -> - (ExternFun name (fromJust tag)) : + (ExternFun name (tagExtract tag)) : concatMap (\C.UExpr { C.uExprExpr = expr } -> c2Args expr) args - C.ExternArray _ _ name _ _ _ _ -> [ExternArr name] + C.ExternArray _ _ name _ _ _ tag -> [ExternArr name (tagExtract tag)] C.Op1 _ e -> c2Args_ e