copilot-bluespec (empty) → 3.19
raw patch · 16 files changed
+2468/−0 lines, 16 filesdep +HUnitdep +QuickCheckdep +basesetup-changed
Dependencies added: HUnit, QuickCheck, base, copilot-bluespec, copilot-core, directory, filepath, language-bluespec, pretty, process, random, test-framework, test-framework-hunit, test-framework-quickcheck2, unix
Files
- CHANGELOG +3/−0
- LICENSE +29/−0
- README.md +38/−0
- Setup.hs +2/−0
- copilot-bluespec.cabal +96/−0
- shared/Copilot/Compile/Bluespec/External.hs +57/−0
- src/Copilot/Compile/Bluespec.hs +12/−0
- src/Copilot/Compile/Bluespec/CodeGen.hs +259/−0
- src/Copilot/Compile/Bluespec/Compile.hs +294/−0
- src/Copilot/Compile/Bluespec/Error.hs +20/−0
- src/Copilot/Compile/Bluespec/Expr.hs +465/−0
- src/Copilot/Compile/Bluespec/Name.hs +95/−0
- src/Copilot/Compile/Bluespec/Settings.hs +14/−0
- src/Copilot/Compile/Bluespec/Type.hs +95/−0
- tests/Main.hs +18/−0
- tests/Test/Copilot/Compile/Bluespec.hs +971/−0
+ CHANGELOG view
@@ -0,0 +1,3 @@+2024-03-08+ * Version bump (3.19). (#5)+ * Create new library for Bluespec backend.
+ 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,38 @@+[](https://github.com/Copilot-Language/copilot-bluespec/actions?query=workflow%3Acopilot-bluespec)++# Copilot: a stream DSL+Copilot-Bluespec implements a Bluespec backend for Copilot, producing code that+is suitable for FPGAs.++Copilot is a runtime verification framework written in Haskell. It allows the+user to write programs in a simple but powerful way using a stream-based+approach.++Programs can be interpreted for testing, or translated Bluespec code to be+incorporated in a project, or as a standalone application. The Bluespec backend+ensures us that the output is constant in memory and time, making it suitable+for systems with hard realtime requirements.++## Installation+Copilot-Bluespec can be found on+[Hackage](https://hackage.haskell.org/package/copilot-bluespec). It is+typically only installed as part of the complete Copilot distribution. For+installation instructions, please refer to the [Copilot+website](https://copilot-language.github.io).++The generated Bluespec code requires `bsc` (the Bluespec compiler) in order to+be compiled. `bsc` can be downloaded+[here](https://github.com/B-Lang-org/bsc/releases).++## Further information+For further information, install instructions and documentation, please visit+the Copilot website:+[https://copilot-language.github.io](https://copilot-language.github.io)++There is also an implementation-focused design document+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-bluespec/DESIGN.md).+++## License+Copilot is distributed under the BSD-3-Clause license, which can be found+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-bluespec/LICENSE).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-bluespec.cabal view
@@ -0,0 +1,96 @@+cabal-version : >= 1.10+name : copilot-bluespec+version : 3.19+synopsis : A compiler for Copilot targeting FPGAs.+description :+ This package is a back-end from Copilot to FPGAs in Bluespec.+ .+ Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in+ Haskell. Copilot contains an interpreter, multiple back-end compilers, and+ other verification tools.+ .+ A tutorial, examples, and other information are available at+ <https://copilot-language.github.io>.++license : BSD3+license-file : LICENSE+maintainer : Ryan Scott <rscott@galois.com>+homepage : https://copilot-language.github.io+bug-reports : https://github.com/Copilot-Language/copilot-bluespec/issues+stability : Experimental+category : Language, Embedded+build-type : Simple+extra-source-files : README.md+ , CHANGELOG++author : Frank Dedden+ , Alwyn Goodloe+ , Ivan Perez+ , Ryan Scott++x-curation: uncurated++source-repository head+ type: git+ location: https://github.com/Copilot-Language/copilot-bluespec.git++library+ default-language : Haskell2010+ hs-source-dirs : src, shared++ ghc-options : -Wall+ build-depends : base >= 4.9 && < 5+ , directory >= 1.3 && < 1.4+ , filepath >= 1.4 && < 1.5+ , pretty >= 1.1.2 && < 1.2++ , copilot-core >= 3.19 && < 3.20+ , language-bluespec >= 0.1 && < 0.2++ exposed-modules : Copilot.Compile.Bluespec++ other-modules : Copilot.Compile.Bluespec.CodeGen+ , Copilot.Compile.Bluespec.Compile+ , Copilot.Compile.Bluespec.Error+ , Copilot.Compile.Bluespec.Expr+ , Copilot.Compile.Bluespec.External+ , Copilot.Compile.Bluespec.Name+ , Copilot.Compile.Bluespec.Settings+ , Copilot.Compile.Bluespec.Type++test-suite unit-tests+ type:+ exitcode-stdio-1.0++ main-is:+ Main.hs++ other-modules:+ Test.Copilot.Compile.Bluespec++ Copilot.Compile.Bluespec.External++ build-depends:+ base+ , directory+ , HUnit+ , QuickCheck+ , pretty+ , process+ , random+ , test-framework+ , test-framework-hunit+ , test-framework-quickcheck2+ , unix++ , copilot-core+ , copilot-bluespec++ hs-source-dirs:+ tests, shared++ default-language:+ Haskell2010++ ghc-options:+ -Wall
@@ -0,0 +1,57 @@+{-# LANGUAGE ExistentialQuantification #-}++-- | Represent information about externs needed in the generation of Bluespec+-- code for stream declarations and triggers.+module Copilot.Compile.Bluespec.External+ ( External(..)+ , gatherExts+ ) where++-- External imports+import Data.List (unionBy)++-- Internal imports: Copilot+import Copilot.Core ( Expr (..), Stream (..), Trigger (..), Type, UExpr (..) )++-- | Representation of external variables.+data External = forall a. External+ { extName :: String+ , extType :: Type a+ }++-- | Collect all external variables from the streams and triggers.+--+-- Although Copilot specifications can contain also properties and theorems,+-- the C99 backend currently only generates code for streams and triggers.+gatherExts :: [Stream] -> [Trigger] -> [External]+gatherExts streams triggers = streamsExts `extUnion` triggersExts+ where+ streamsExts = foldr (extUnion . streamExts) mempty streams+ triggersExts = foldr (extUnion . triggerExts) mempty triggers++ streamExts :: Stream -> [External]+ streamExts (Stream _ _ expr _) = exprExts expr++ triggerExts :: Trigger -> [External]+ triggerExts (Trigger _ guard args) = guardExts `extUnion` argExts+ where+ guardExts = exprExts guard+ argExts = concatMap uExprExts args++ uExprExts :: UExpr -> [External]+ uExprExts (UExpr _ expr) = exprExts expr++ exprExts :: Expr a -> [External]+ exprExts (Local _ _ _ e1 e2) = exprExts e1 `extUnion` exprExts e2+ exprExts (ExternVar ty name _) = [External name ty]+ exprExts (Op1 _ e) = exprExts e+ exprExts (Op2 _ e1 e2) = exprExts e1 `extUnion` exprExts e2+ exprExts (Op3 _ e1 e2 e3) = exprExts e1 `extUnion` exprExts e2+ `extUnion` exprExts e3+ exprExts (Label _ _ e) = exprExts e+ exprExts _ = []++ -- | Union over lists of External, we solely base the equality on the+ -- extName's.+ extUnion :: [External] -> [External] -> [External]+ extUnion = unionBy (\a b -> extName a == extName b)
+ src/Copilot/Compile/Bluespec.hs view
@@ -0,0 +1,12 @@+-- | Compile Copilot specifications to Bluespec code.+module Copilot.Compile.Bluespec+ ( compile+ , compileWith+ , BluespecSettings(..)+ , mkDefaultBluespecSettings+ ) where++-- Internal imports+import Copilot.Compile.Bluespec.Compile ( compile, compileWith )+import Copilot.Compile.Bluespec.Settings ( BluespecSettings (..),+ mkDefaultBluespecSettings )
+ src/Copilot/Compile/Bluespec/CodeGen.hs view
@@ -0,0 +1,259 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | High-level translation of Copilot Core into Bluespec.+module Copilot.Compile.Bluespec.CodeGen+ ( -- * Type declarations+ mkStructDecln++ -- * Ring buffers+ , mkBuffDecln+ , mkIndexDecln+ , mkAccessDecln++ -- * Stream generators+ , mkGenFun++ -- * Monitor processing+ , mkStepRule+ , mkTriggerRule++ -- * Module interface specifications+ , mkSpecIfcFields+ ) where++-- External imports+import Data.String (IsString (..))+import qualified Language.Bluespec.Classic.AST as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS++-- Internal imports: Copilot+import Copilot.Core++-- Internal imports+import Copilot.Compile.Bluespec.Expr+import Copilot.Compile.Bluespec.External+import Copilot.Compile.Bluespec.Name+import Copilot.Compile.Bluespec.Type++-- | Write a generator function for a stream.+mkGenFun :: String -> Expr a -> Type a -> BS.CDefl+mkGenFun name expr ty =+ -- name :: ty+ -- name = expr+ BS.CLValueSign+ (BS.CDef nameId (BS.CQType [] (transType ty)) [def])+ []+ where+ nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name+ def = BS.CClause [] [] (transExpr expr)++-- | Bind a buffer variable and initialise it with the stream buffer.+mkBuffDecln :: forall a. Id -> Type a -> [a] -> [BS.CStmt]+mkBuffDecln sId ty xs =+ initVals ++ [BS.CSletrec [initBufSig]]+ where+ -- sId_0 :: Reg <ty> <- mkReg xs_0+ -- ...+ -- sId_(n-1) :: Reg <ty> <- mkReg xs_(n-1)+ initVals = zipWith mkInitVal xs [0..]+ -- sId :: Vector n (Reg <ty>)+ -- sId = update (... (update newVector 0 sId_0) ...) (n-1) sId_(n-1)+ initBufSig = BS.CLValueSign+ (BS.CDef nameId (BS.CQType [] vecTy) [initBufDef])+ []+ initBufDef = BS.CClause+ []+ []+ (genVector+ (\idx _ -> BS.CVar $ BS.mkId BS.NoPos $+ fromString $ streamElemName sId idx)+ xs)++ nameId = BS.mkId BS.NoPos $ fromString $ streamName sId+ bsTy = tReg `BS.TAp` transType ty+ vecTy = tVector `BS.TAp` BS.cTNum numElems BS.NoPos `BS.TAp` bsTy+ numElems = toInteger $ length xs++ mkInitVal :: a -> Int -> BS.CStmt+ mkInitVal x elemNum =+ BS.CSBindT+ (BS.CPVar elemId)+ Nothing+ []+ (BS.CQType [] bsTy)+ (BS.CApply (BS.CVar (BS.mkId BS.NoPos "mkReg")) [constTy ty x])+ where+ elemName = streamElemName sId elemNum+ elemId = BS.mkId BS.NoPos $ fromString elemName++-- | Make an index variable and initialise it to 0.+mkIndexDecln :: Id -> BS.CStmt+mkIndexDecln sId =+ -- sId_idx :: Reg (Bit 64) <- mkReg 0+ BS.CSBindT+ (BS.CPVar nameId)+ Nothing+ []+ (BS.CQType [] bsTy)+ (BS.CApply (BS.CVar (BS.mkId BS.NoPos "mkReg"))+ [cLit $ BS.LInt $ BS.ilDec 0])+ where+ nameId = BS.mkId BS.NoPos $ fromString $ indexName sId+ bsTy = tReg `BS.TAp` BS.tBitN 64 BS.NoPos++-- | Define an accessor function for the ring buffer associated with a stream+mkAccessDecln :: Id -> Type a -> [a] -> BS.CDefl+mkAccessDecln sId ty xs =+ -- sId_get :: Bits 64 -> ty+ -- sId_get x = (select sId ((sId_idx + x) % buffLength))._read+ BS.CLValueSign (BS.CDef nameId (BS.CQType [] funTy) [def]) []+ where+ def = BS.CClause [BS.CPVar argId] [] expr+ argTy = BS.tBit `BS.TAp` BS.cTNum 64 BS.NoPos+ retTy = transType ty+ funTy = BS.tArrow `BS.TAp` argTy `BS.TAp` retTy+ name = streamAccessorName sId+ nameId = BS.mkId BS.NoPos $ fromString name+ buffLength = cLit $ BS.LInt $ BS.ilDec $ toInteger $ length xs+ argId = BS.mkId BS.NoPos "x"+ index = BS.CApply (BS.CVar (BS.idPercentAt BS.NoPos))+ [ BS.CApply (BS.CVar BS.idPlus)+ [ BS.CVar (BS.mkId BS.NoPos (fromString (indexName sId)))+ , BS.CVar argId+ ]+ , buffLength+ ]+ indexExpr = cIndexVector+ (BS.CVar (BS.mkId BS.NoPos (fromString (streamName sId))))+ index+ expr = BS.CSelect indexExpr (BS.id_read BS.NoPos)++-- | Define fields for a module interface containing a specification's trigger+-- functions and external variables.+mkSpecIfcFields :: [Trigger] -> [External] -> [BS.CField]+mkSpecIfcFields triggers exts =+ map mkTriggerField triggers ++ map mkExtField exts+ where+ -- trigger :: args_1 -> ... -> args_n -> Action+ mkTriggerField :: Trigger -> BS.CField+ mkTriggerField (Trigger name _ args) =+ mkField name $+ foldr+ (\(UExpr arg _) res -> BS.tArrow `BS.TAp` transType arg `BS.TAp` res)+ BS.tAction+ args++ -- ext :: Reg ty+ mkExtField :: External -> BS.CField+ mkExtField (External name ty) =+ mkField name $ tReg `BS.TAp` transType ty++-- | Define a rule for a trigger function.+mkTriggerRule :: Trigger -> BS.CRule+mkTriggerRule (Trigger name _ args) =+ BS.CRule+ []+ (Just $ cLit $ BS.LString name)+ [ BS.CQFilter $+ BS.CVar $ BS.mkId BS.NoPos $+ fromString $ guardName name+ ]+ (BS.CApply nameExpr args')+ where+ ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName+ nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name+ nameExpr = BS.CSelect (BS.CVar ifcArgId) nameId++ args' = take (length args) (map argCall (argNames name))+ argCall = BS.CVar . BS.mkId BS.NoPos . fromString++-- | Writes the @step@ rule that updates all streams.+mkStepRule :: [Stream] -> Maybe BS.CRule+mkStepRule streams+ | null allUpdates+ = -- If there is nothing to update, don't bother creating a step rule.+ -- Doing so wouldn't harm anything, but bsc will generate a warning+ -- when compiling such an empty rule.+ Nothing+ | otherwise+ = Just $+ BS.CRule+ []+ (Just $ cLit $ BS.LString "step")+ [BS.CQFilter $ BS.CCon BS.idTrue []]+ (BS.Caction BS.NoPos allUpdates)+ where+ allUpdates = bufferUpdates ++ indexUpdates+ (bufferUpdates, indexUpdates) = unzip $ map mkUpdateGlobals streams++ -- Write code to update global stream buffers and index.+ mkUpdateGlobals :: Stream -> (BS.CStmt, BS.CStmt)+ mkUpdateGlobals (Stream sId buff _ _) =+ (bufferUpdate, indexUpdate)+ where+ bufferUpdate =+ BS.CSExpr Nothing $+ BS.Cwrite+ BS.NoPos+ (cIndexVector (BS.CVar buffId) (BS.CVar indexId))+ (BS.CVar genId)++ indexUpdate =+ BS.CSExpr Nothing $+ BS.Cwrite+ BS.NoPos+ (BS.CVar indexId)+ (BS.CApply (BS.CVar (BS.idPercentAt BS.NoPos))+ [incIndex, buffLength])+ where+ buffLength = cLit $ BS.LInt $ BS.ilDec $ toInteger $ length buff+ incIndex = BS.CApply (BS.CVar BS.idPlus)+ [ BS.CVar indexId+ , cLit $ BS.LInt $ BS.ilDec 1+ ]++ buffId = BS.mkId BS.NoPos $ fromString $ streamName sId+ genId = BS.mkId BS.NoPos $ fromString $ generatorName sId+ indexId = BS.mkId BS.NoPos $ fromString $ indexName sId++-- | Write a struct declaration based on its definition.+mkStructDecln :: Struct a => a -> BS.CDefn+mkStructDecln x =+ BS.Cstruct+ True+ BS.SStruct+ (BS.IdK structId)+ [] -- No type variables+ structFields+ -- Derive a Bits instance so that we can put this struct in a Reg+ [BS.CTypeclass BS.idBits]+ where+ structId = BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName x+ structFields = map mkStructField $ toValues x++ mkStructField :: Value a -> BS.CField+ mkStructField (Value ty field) =+ mkField (fieldName field) (transType ty)++-- | Write a field of a struct or interface, along with its type.+mkField :: String -> BS.CType -> BS.CField+mkField name ty =+ BS.CField+ { BS.cf_name = BS.mkId BS.NoPos $ fromString $ lowercaseName name+ , BS.cf_pragmas = Nothing+ , BS.cf_type = BS.CQType [] ty+ , BS.cf_default = []+ , BS.cf_orig_type = Nothing+ }++-- | The @Reg@ Bluespec interface type.+tReg :: BS.CType+tReg = BS.TCon $+ BS.TyCon+ { BS.tcon_name = BS.idReg+ , BS.tcon_kind = Just (BS.Kfun BS.KStar BS.KStar)+ , BS.tcon_sort = BS.TIstruct (BS.SInterface [])+ [BS.id_write BS.NoPos, BS.id_read BS.NoPos]+ }
+ src/Copilot/Compile/Bluespec/Compile.hs view
@@ -0,0 +1,294 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}++-- | Compile Copilot specifications to Bluespec code.+module Copilot.Compile.Bluespec.Compile+ ( compile+ , compileWith+ ) where++-- External imports+import Data.List (nub, union)+import Data.Maybe (catMaybes, maybeToList)+import Data.String (IsString (..))+import Data.Typeable (Typeable)+import qualified Language.Bluespec.Classic.AST as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS+import Text.PrettyPrint.HughesPJClass (Pretty (..), render)+import System.Directory (createDirectoryIfMissing)+import System.Exit (exitFailure)+import System.FilePath ((</>))+import System.IO (hPutStrLn, stderr)++-- Internal imports: Copilot+import Copilot.Core++-- Internal imports+import Copilot.Compile.Bluespec.CodeGen+import Copilot.Compile.Bluespec.External+import Copilot.Compile.Bluespec.Name+import Copilot.Compile.Bluespec.Settings++-- | Compile a specification to a Bluespec file.+--+-- The first argument is the settings for the Bluespec code generated.+--+-- The second argument is used as a module name and the prefix for the .bs files+-- that are generated.+compileWith :: BluespecSettings -> String -> Spec -> IO ()+compileWith bsSettings prefix spec+ | null (specTriggers spec)+ = do hPutStrLn stderr $+ "Copilot error: attempt at compiling empty specification.\n"+ ++ "You must define at least one trigger to generate Bluespec monitors."+ exitFailure++ | otherwise+ = do let typesBsFile = render $ pPrint $ compileTypesBS bsSettings prefix spec+ ifcBsFile = render $ pPrint $ compileIfcBS bsSettings prefix spec+ bsFile = render $ pPrint $ compileBS bsSettings prefix spec++ let dir = bluespecSettingsOutputDirectory bsSettings+ createDirectoryIfMissing True dir+ writeFile (dir </> specTypesPkgName prefix ++ ".bs") typesBsFile+ writeFile (dir </> specIfcPkgName prefix ++ ".bs") ifcBsFile+ writeFile (dir </> prefix ++ ".bs") bsFile++-- | Compile a specification to a Bluespec.+--+-- The first argument is used as a prefix for the generated .bs files.+compile :: String -> Spec -> IO ()+compile = compileWith mkDefaultBluespecSettings++-- | Generate a @<prefix>.bs@ file from a 'Spec'. This is the main payload of+-- the Bluespec backend.+--+-- The generated Bluespec file will import a handful of files from the standard+-- library, as well as the following generated files:+--+-- * @<prefix>Ifc.bs@, which defines the interface containing the trigger+-- functions and external variables.+--+-- * @<prefix>Types.bs@, which defines any structs used in the 'Spec'.+--+-- It will also generate a @mk<prefix> :: Module <prefix>Ifc -> Module Empty@+-- function, which defines the module structure for this 'Spec'. The+-- @mk<prefix>@ function has the following structure:+--+-- * First, bind the argument of type @Module <prefix>Ifc@ so that trigger+-- functions can be invoked and external variables can be used.+--+-- * Next, declare stream buffers and indices.+--+-- * Next, declare generator functions for streams, accessor functions for+-- streams, and guard functions for triggers.+--+-- * Next, declare rules for each trigger function.+--+-- * Finally, declare a single rule that updates the stream buffers and+-- indices.+compileBS :: BluespecSettings -> String -> Spec -> BS.CPackage+compileBS _bsSettings prefix spec =+ BS.CPackage+ (BS.mkId BS.NoPos (fromString prefix))+ (Right [])+ (stdLibImports ++ genImports)+ []+ [moduleDef]+ []+ where+ -- import <prefix>Types+ -- import <prefix>Ifc+ genImports :: [BS.CImport]+ genImports =+ [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString+ $ specTypesPkgName prefix+ , BS.CImpId False $ BS.mkId BS.NoPos $ fromString+ $ specIfcPkgName prefix+ ]++ moduleDef :: BS.CDefn+ moduleDef = BS.CValueSign $+ BS.CDef+ (BS.mkId BS.NoPos $ fromString $ "mk" ++ prefix)+ -- :: Module <prefix>Ifc -> Module Empty+ (BS.CQType+ []+ (BS.tArrow+ `BS.TAp` (BS.tModule `BS.TAp` ifcTy)+ `BS.TAp` (BS.tModule `BS.TAp` emptyTy)))+ [ BS.CClause [BS.CPVar ifcModId] [] $+ BS.Cmodule BS.NoPos $+ BS.CMStmt+ (BS.CSBind (BS.CPVar ifcArgId) Nothing [] (BS.CVar ifcModId))+ : map BS.CMStmt mkGlobals +++ [ BS.CMStmt $ BS.CSletrec genFuns+ , BS.CMrules $ BS.Crules [] rules+ ]+ ]++ ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName+ ifcModId = BS.mkId BS.NoPos "ifcMod"++ rules :: [BS.CRule]+ rules = map mkTriggerRule triggers ++ maybeToList (mkStepRule streams)++ streams = specStreams spec+ triggers = specTriggers spec+ exts = gatherExts streams triggers++ ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix+ ifcFields = mkSpecIfcFields triggers exts+ ifcTy = BS.TCon (BS.TyCon+ { BS.tcon_name = ifcId+ , BS.tcon_kind = Just BS.KStar+ , BS.tcon_sort = BS.TIstruct+ (BS.SInterface [])+ (map BS.cf_name ifcFields)+ })++ emptyTy = BS.TCon (BS.TyCon+ { BS.tcon_name = BS.idEmpty+ , BS.tcon_kind = Just BS.KStar+ , BS.tcon_sort = BS.TIstruct (BS.SInterface []) []+ })++ -- Make buffer and index declarations for streams.+ mkGlobals :: [BS.CStmt]+ mkGlobals = concatMap buffDecln streams ++ map indexDecln streams+ where+ buffDecln (Stream sId buff _ ty) = mkBuffDecln sId ty buff+ indexDecln (Stream sId _ _ _ ) = mkIndexDecln sId++ -- Make generator functions, including trigger arguments.+ genFuns :: [BS.CDefl]+ genFuns = map accessDecln streams+ ++ map streamGen streams+ ++ concatMap triggerGen triggers+ where+ accessDecln :: Stream -> BS.CDefl+ accessDecln (Stream sId buff _ ty) = mkAccessDecln sId ty buff++ streamGen :: Stream -> BS.CDefl+ streamGen (Stream sId _ expr ty) = mkGenFun (generatorName sId) expr ty++ triggerGen :: Trigger -> [BS.CDefl]+ triggerGen (Trigger name guard args) = guardDef : argDefs+ where+ guardDef = mkGenFun (guardName name) guard Bool+ argDefs = map argGen (zip (argNames name) args)++ argGen :: (String, UExpr) -> BS.CDefl+ argGen (argName, UExpr ty expr) = mkGenFun argName expr ty++-- | Generate a @<prefix>Ifc.bs@ file from a 'Spec'. This contains the+-- definition of the @<prefix>Ifc@ interface, which declares the types of all+-- trigger functions and external variables. This is put in a separate file so+-- that larger applications can use it separately.+compileIfcBS :: BluespecSettings -> String -> Spec -> BS.CPackage+compileIfcBS _bsSettings prefix spec =+ BS.CPackage+ ifcPkgId+ (Right [])+ (stdLibImports ++ genImports)+ []+ [ifcDef]+ []+ where+ -- import <prefix>Types+ genImports :: [BS.CImport]+ genImports =+ [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString+ $ specTypesPkgName prefix+ ]++ ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix+ ifcPkgId = BS.mkId BS.NoPos $ fromString $ specIfcPkgName prefix+ ifcFields = mkSpecIfcFields triggers exts++ streams = specStreams spec+ triggers = specTriggers spec+ exts = gatherExts streams triggers++ ifcDef :: BS.CDefn+ ifcDef = BS.Cstruct+ True+ (BS.SInterface [])+ (BS.IdK ifcId)+ [] -- No type variables+ ifcFields+ [] -- No derived instances++-- | Generate a @<prefix>Types.bs@ file from a 'Spec'. This declares the types+-- of any structs used by the Copilot specification. This is put in a separate+-- file so that larger applications can more easily substitute their own struct+-- definitions if desired.+compileTypesBS :: BluespecSettings -> String -> Spec -> BS.CPackage+compileTypesBS _bsSettings prefix spec =+ BS.CPackage+ typesId+ (Right [])+ stdLibImports+ []+ structDefs+ []+ where+ typesId = BS.mkId BS.NoPos $ fromString $ specTypesPkgName prefix++ structDefs = mkTypeDeclns exprs++ exprs = gatherExprs streams triggers+ streams = specStreams spec+ triggers = specTriggers spec++ -- Generate type declarations.+ mkTypeDeclns :: [UExpr] -> [BS.CDefn]+ mkTypeDeclns es = catMaybes $ map mkTypeDecln uTypes+ where+ uTypes = nub $ concatMap (\(UExpr _ e) -> exprTypes e) es++ mkTypeDecln (UType ty) = case ty of+ Struct x -> Just $ mkStructDecln x+ _ -> Nothing++-- | Imports from the Bluespec standard library.+stdLibImports :: [BS.CImport]+stdLibImports =+ [ BS.CImpId False $ BS.mkId BS.NoPos "FloatingPoint"+ , BS.CImpId False $ BS.mkId BS.NoPos "Vector"+ ]++-- ** Obtain information from Copilot Core Exprs and Types.++-- | List all types of an expression, returns items uniquely.+exprTypes :: Typeable a => Expr a -> [UType]+exprTypes e = case e of+ Const ty _ -> typeTypes ty+ Local ty1 ty2 _ e1 e2 -> typeTypes ty1 `union` typeTypes ty2+ `union` exprTypes e1 `union` exprTypes e2+ Var ty _ -> typeTypes ty+ Drop ty _ _ -> typeTypes ty+ ExternVar ty _ _ -> typeTypes ty+ Op1 _ e1 -> exprTypes e1+ Op2 _ e1 e2 -> exprTypes e1 `union` exprTypes e2+ Op3 _ e1 e2 e3 -> exprTypes e1 `union` exprTypes e2+ `union` exprTypes e3+ Label ty _ _ -> typeTypes ty++-- | List all types of a type, returns items uniquely.+typeTypes :: Typeable a => Type a -> [UType]+typeTypes ty = case ty of+ Array ty' -> typeTypes ty' `union` [UType ty]+ Struct x -> concatMap (\(Value ty' _) -> typeTypes ty') (toValues x)+ `union` [UType ty]+ _ -> [UType ty]++-- | Collect all expression of a list of streams and triggers and wrap them+-- into an UEXpr.+gatherExprs :: [Stream] -> [Trigger] -> [UExpr]+gatherExprs streams triggers = map streamUExpr streams+ ++ concatMap triggerUExpr triggers+ where+ streamUExpr (Stream _ _ expr ty) = UExpr ty expr+ triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args
+ src/Copilot/Compile/Bluespec/Error.hs view
@@ -0,0 +1,20 @@+{-# LANGUAGE Safe #-}++-- |+-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.+--+-- Custom functions to report error messages to users.+module Copilot.Compile.Bluespec.Error+ ( impossible )+ where++-- | Report an error due to a bug in Copilot.+impossible :: String -- ^ Name of the function in which the error was detected.+ -> String -- ^ Name of the package in which the function is located.+ -> a+impossible function package =+ error $ "Impossible error in function "+ ++ function ++ ", in package " ++ package+ ++ ". Please file an issue at "+ ++ "https://github.com/Copilot-Language/copilot/issues"+ ++ " or email the maintainers at <ivan.perezdominguez@nasa.gov>"
+ src/Copilot/Compile/Bluespec/Expr.hs view
@@ -0,0 +1,465 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}++-- | Translate Copilot Core expressions and operators to Bluespec.+module Copilot.Compile.Bluespec.Expr+ ( transExpr+ , cIndexVector+ , cLit+ , constTy+ , genVector+ ) where++-- External imports+import Data.Foldable (foldl')+import Data.String (IsString (..))+import qualified Language.Bluespec.Classic.AST as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS++-- Internal imports: Copilot+import Copilot.Core++-- Internal imports+import Copilot.Compile.Bluespec.Error (impossible)+import Copilot.Compile.Bluespec.Name+import Copilot.Compile.Bluespec.Type++-- | Translates a Copilot Core expression into a Bluespec expression.+transExpr :: Expr a -> BS.CExpr+transExpr (Const ty x) = constTy ty x++transExpr (Local ty1 _ name e1 e2) =+ let nameId = BS.mkId BS.NoPos $ fromString name+ e1' = transExpr e1+ ty1' = transType ty1+ e2' = transExpr e2 in+ BS.Cletrec+ [ BS.CLValueSign+ (BS.CDef nameId (BS.CQType [] ty1') [BS.CClause [] [] e1'])+ []+ ]+ e2'++transExpr (Var _ n) = BS.CVar $ BS.mkId BS.NoPos $ fromString n++transExpr (Drop _ amount sid) =+ let accessVar = streamAccessorName sid+ index = BS.LInt $ BS.ilDec $ fromIntegral amount in+ BS.CApply (BS.CVar $ BS.mkId BS.NoPos $ fromString accessVar)+ [BS.CLit $ BS.CLiteral BS.NoPos index]++transExpr (ExternVar _ name _) =+ let ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName in+ BS.CSelect+ (BS.CSelect+ (BS.CVar ifcArgId)+ (BS.mkId BS.NoPos $ fromString $ lowercaseName name))+ (BS.id_read BS.NoPos)++transExpr (Label _ _ e) = transExpr e -- ignore label++transExpr (Op1 op e) = transOp1 op (transExpr e)++transExpr (Op2 op e1 e2) = transOp2 op (transExpr e1) (transExpr e2)++transExpr (Op3 op e1 e2 e3) =+ transOp3 op (transExpr e1) (transExpr e2) (transExpr e3)++-- | Translates a Copilot unary operator and its argument into a Bluespec+-- function.+transOp1 :: Op1 a b -> BS.CExpr -> BS.CExpr+transOp1 op e =+ case op of+ Not -> app BS.idNot+ Abs _ty -> app $ BS.mkId BS.NoPos "abs"+ Sign _ty -> app $ BS.mkId BS.NoPos "signum"+ -- Bluespec's Arith class does not have a `recip` method corresponding to+ -- Haskell's `recip` in the `Fractional` class, so we implement it+ -- ourselves.+ Recip ty -> BS.CApply+ (BS.CVar (BS.idSlashAt BS.NoPos))+ [constNumTy ty 1, e]+ BwNot _ty -> app $ BS.idInvertAt BS.NoPos+ Sqrt _ty -> BS.CSelect+ (BS.CApply+ (BS.CVar (BS.mkId BS.NoPos "sqrtFP"))+ [e, fpRM])+ BS.idPrimFst++ Cast fromTy toTy -> transCast fromTy toTy e+ GetField (Struct _) _ f -> BS.CSelect e $ BS.mkId BS.NoPos $+ fromString $ lowercaseName $ accessorName f+ GetField _ _ _ -> impossible "transOp1" "copilot-bluespec"++ -- Unsupported operations (see+ -- https://github.com/B-Lang-org/bsc/discussions/534)+ Exp _ty -> unsupportedFPOp "exp"+ Log _ty -> unsupportedFPOp "log"+ Acos _ty -> unsupportedFPOp "acos"+ Asin _ty -> unsupportedFPOp "asin"+ Atan _ty -> unsupportedFPOp "atan"+ Cos _ty -> unsupportedFPOp "cos"+ Sin _ty -> unsupportedFPOp "sin"+ Tan _ty -> unsupportedFPOp "tan"+ Acosh _ty -> unsupportedFPOp "acosh"+ Asinh _ty -> unsupportedFPOp "asinh"+ Atanh _ty -> unsupportedFPOp "atanh"+ Cosh _ty -> unsupportedFPOp "cosh"+ Sinh _ty -> unsupportedFPOp "sinh"+ Tanh _ty -> unsupportedFPOp "tanh"+ Ceiling _ty -> unsupportedFPOp "ceiling"+ Floor _ty -> unsupportedFPOp "floor"+ where+ app i = BS.CApply (BS.CVar i) [e]++-- | Translates a Copilot binary operator and its arguments into a Bluespec+-- function.+transOp2 :: Op2 a b c -> BS.CExpr -> BS.CExpr -> BS.CExpr+transOp2 op e1 e2 =+ case op of+ And -> app BS.idAnd+ Or -> app $ BS.idOrAt BS.NoPos+ Add _ty -> app BS.idPlus+ Sub _ty -> app BS.idMinus+ Mul _ty -> app $ BS.idStarAt BS.NoPos+ Mod _ty -> app $ BS.idPercentAt BS.NoPos+ Div _ty -> app $ BS.idSlashAt BS.NoPos+ Fdiv _ty -> app $ BS.idSlashAt BS.NoPos+ Eq _ -> app BS.idEqual+ Ne _ -> app BS.idNotEqual+ Le _ -> app $ BS.idLtEqAt BS.NoPos+ Ge _ -> app $ BS.idGtEqAt BS.NoPos+ Lt _ -> app $ BS.idLtAt BS.NoPos+ Gt _ -> app $ BS.idGtAt BS.NoPos+ BwAnd _ -> app $ BS.idBitAndAt BS.NoPos+ BwOr _ -> app $ BS.idBitOrAt BS.NoPos+ BwXor _ -> app $ BS.idCaretAt BS.NoPos+ BwShiftL _ _ -> app $ BS.idLshAt BS.NoPos+ BwShiftR _ _ -> app $ BS.idRshAt BS.NoPos+ Index _ -> cIndexVector e1 e2++ -- Unsupported operations (see+ -- https://github.com/B-Lang-org/bsc/discussions/534)+ Pow _ty -> unsupportedFPOp "(**)"+ Logb _ty -> unsupportedFPOp "logb"+ Atan2 _ty -> unsupportedFPOp "atan2"+ where+ app i = BS.CApply (BS.CVar i) [e1, e2]++-- | Translates a Copilot ternary operator and its arguments into a Bluespec+-- function.+transOp3 :: Op3 a b c d -> BS.CExpr -> BS.CExpr -> BS.CExpr -> BS.CExpr+transOp3 op e1 e2 e3 =+ case op of+ Mux _ -> BS.Cif BS.NoPos e1 e2 e3++-- | Bluespec does not have a general-purpose casting operation, so we must+-- handle casts on a case-by-case basis.+transCast :: Type a -> Type b -> BS.CExpr -> BS.CExpr+transCast fromTy toTy =+ case (fromTy, toTy) of+ -----+ -- "safe" casts that cannot lose information+ -----++ (Bool, Bool) -> id+ (Bool, Word8) -> upcastBool+ (Bool, Word16) -> upcastBool+ (Bool, Word32) -> upcastBool+ (Bool, Word64) -> upcastBool+ (Bool, Int8) -> upcastBool+ (Bool, Int16) -> upcastBool+ (Bool, Int32) -> upcastBool+ (Bool, Int64) -> upcastBool++ (Int8, Int8) -> id+ (Int8, Int16) -> upcast+ (Int8, Int32) -> upcast+ (Int8, Int64) -> upcast+ (Int16, Int16) -> id+ (Int16, Int32) -> upcast+ (Int16, Int64) -> upcast+ (Int32, Int32) -> id+ (Int32, Int64) -> upcast+ (Int64, Int64) -> id++ (Word8, Int16) -> unpackPackUpcast Word16+ (Word8, Int32) -> unpackPackUpcast Word32+ (Word8, Int64) -> unpackPackUpcast Word64+ (Word8, Word8) -> id+ (Word8, Word16) -> upcast+ (Word8, Word32) -> upcast+ (Word8, Word64) -> upcast+ (Word16, Int32) -> unpackPackUpcast Word32+ (Word16, Int64) -> unpackPackUpcast Word64+ (Word16, Word16) -> id+ (Word16, Word32) -> upcast+ (Word16, Word64) -> upcast+ (Word32, Int64) -> unpackPackUpcast Word64+ (Word32, Word32) -> id+ (Word32, Word64) -> upcast+ (Word64, Word64) -> id++ -----+ -- "unsafe" casts, which may lose information+ -----++ -- unsigned truncations+ (Word64, Word32) -> downcast+ (Word64, Word16) -> downcast+ (Word64, Word8) -> downcast+ (Word32, Word16) -> downcast+ (Word32, Word8) -> downcast+ (Word16, Word8) -> downcast++ -- signed truncations+ (Int64, Int32) -> downcast+ (Int64, Int16) -> downcast+ (Int64, Int8) -> downcast+ (Int32, Int16) -> downcast+ (Int32, Int8) -> downcast+ (Int16, Int8) -> downcast++ -- signed integer to float+ (Int64, Float) -> castIntegralToFloatingPoint+ (Int32, Float) -> castIntegralToFloatingPoint+ (Int16, Float) -> castIntegralToFloatingPoint+ (Int8, Float) -> castIntegralToFloatingPoint++ -- unsigned integer to float+ (Word64, Float) -> castIntegralToFloatingPoint+ (Word32, Float) -> castIntegralToFloatingPoint+ (Word16, Float) -> castIntegralToFloatingPoint+ (Word8, Float) -> castIntegralToFloatingPoint++ -- signed integer to double+ (Int64, Double) -> castIntegralToFloatingPoint+ (Int32, Double) -> castIntegralToFloatingPoint+ (Int16, Double) -> castIntegralToFloatingPoint+ (Int8, Double) -> castIntegralToFloatingPoint++ -- unsigned integer to double+ (Word64, Double) -> castIntegralToFloatingPoint+ (Word32, Double) -> castIntegralToFloatingPoint+ (Word16, Double) -> castIntegralToFloatingPoint+ (Word8, Double) -> castIntegralToFloatingPoint++ -- unsigned to signed conversion+ (Word64, Int64) -> unpackPack+ (Word32, Int32) -> unpackPack+ (Word16, Int16) -> unpackPack+ (Word8, Int8) -> unpackPack++ -- signed to unsigned conversion+ (Int64, Word64) -> unpackPack+ (Int32, Word32) -> unpackPack+ (Int16, Word16) -> unpackPack+ (Int8, Word8) -> unpackPack++ _ -> impossible "transCast" "copilot-bluespec"+ where+ -- unpackPack :: (Bits fromTy n, Bits toTy n) => fromTy -> toTy+ -- unpackPack e = (unpack (pack e)) :: toTy+ --+ -- The most basic cast. Used when fromTy and toTy are both integral types+ -- with the same number of bits.+ unpackPack :: BS.CExpr -> BS.CExpr+ unpackPack e = withTypeAnnotation toTy $+ BS.CApply+ (BS.CVar BS.idUnpack)+ [BS.CApply (BS.CVar BS.idPack) [e]]++ -- upcastBool :: (Add k 1 n, Bits toTy n) => Bool -> toTy+ -- upcastBool b = (unpack (extend (pack b))) :: toTy+ --+ -- Cast a Bool to a `Bits 1` value, extend it to `Bits n`, and then+ -- convert it back to an integral type.+ upcastBool :: BS.CExpr -> BS.CExpr+ upcastBool e = withTypeAnnotation toTy $+ BS.CApply+ (BS.CVar BS.idUnpack)+ [BS.CApply extendExpr [BS.CApply (BS.CVar BS.idPack) [e]]]++ -- upcast :: (BitExtend m n x) => x m -> x n+ -- upcast e = (extend e) :: ty+ --+ -- Convert a narrower integral type to a wider integral type (e.g.,+ -- `UInt 8` to `UInt 64` or `Int 8` to `Int 64`). Note that the `extend`+ -- operation is smart enough to choose between sign-extension and+ -- zero-extension depending on whether `x m` (i.e., fromTy) is a signed+ -- or unsigned type, respectively.+ upcast :: BS.CExpr -> BS.CExpr+ upcast e = withTypeAnnotation toTy $ BS.CApply extendExpr [e]++ -- downcast :: (BitExtend m n x) => x n -> x m+ -- downcast e = (truncate e) :: ty+ --+ -- Convert a wider integral type to a narrow integral type (e.g.,+ -- `UInt 64` to `UInt 8` or `Int 64` to `Int 8`) by truncating the most+ -- significant bits.+ downcast :: BS.CExpr -> BS.CExpr+ downcast e = withTypeAnnotation toTy $ BS.CApply truncateExpr [e]++ -- Apply upcast followed by unpackPack. This requires supplying the type to+ -- upcast to for type disambiguation purposes.+ unpackPackUpcast :: Type a -> BS.CExpr -> BS.CExpr+ unpackPackUpcast upcastTy e = unpackPack $+ withTypeAnnotation upcastTy $ BS.CApply extendExpr [e]++ -- castIntegralToFloatingPoint :: (FixedFloatCVT fromTy toTy) => fromTy toTy+ -- castIntegralToFloatingPoint e =+ -- ((vFixedToFloat e (0 :: UInt 64) Rnd_Nearest_Even).fst) :: tfl+ --+ -- While FloatingPoint does have a Bits instance, we don't want to convert+ -- an integral type to a FloatingPoint type using the Bits class, as the+ -- bit representation of an integral value differs quite a bit from the bit+ -- representation of a FloatingPoint value. Instead, we use the+ -- special-purpose FixedFloatCVT class for this task.+ castIntegralToFloatingPoint :: BS.CExpr -> BS.CExpr+ castIntegralToFloatingPoint e =+ withTypeAnnotation toTy $+ BS.CSelect+ (BS.CApply+ (BS.CVar (BS.mkId BS.NoPos "vFixedToFloat"))+ [ e+ , constNumTy Word64 0+ , fpRM+ ])+ BS.idPrimFst++ extendExpr = BS.CVar $ BS.mkId BS.NoPos "extend"+ truncateExpr = BS.CVar $ BS.mkId BS.NoPos "truncate"++-- | Transform a Copilot Core literal, based on its value and type, into a+-- Bluespec expression.+constTy :: Type a -> a -> BS.CExpr+constTy ty =+ case ty of+ -- The treatment of scalar types is relatively straightforward. Note that+ -- Bool is an enum, so we must construct it using a CCon rather than with+ -- a CLit.+ Bool -> \v -> BS.CCon (if v then BS.idTrue else BS.idFalse) []+ Int8 -> constInt ty . toInteger+ Int16 -> constInt ty . toInteger+ Int32 -> constInt ty . toInteger+ Int64 -> constInt ty . toInteger+ Word8 -> constInt ty . toInteger+ Word16 -> constInt ty . toInteger+ Word32 -> constInt ty . toInteger+ Word64 -> constInt ty . toInteger+ Float -> constFP ty . realToFrac+ Double -> constFP ty++ -- Translating a Copilot array literal to a Bluespec Vector is somewhat+ -- involved. Given a Copilot array {x_0, ..., x_(n-1)}, the+ -- corresponding Bluespec Vector will look something like:+ --+ -- let arr = update (... (update newVector 0 x_0)) (n-1) x_(n-1)+ --+ -- We use the `update` function instead of the := syntax (e.g.,+ -- { array_temp[0] := x; array_temp[1] := y; ...}) so that we can construct+ -- a Vector in a pure context.+ Array ty' -> constVector ty' . arrayElems++ -- Converting a Copilot struct { field_0 = x_0, ..., field_(n-1) = x_(n-1) }+ -- to a Bluespec struct is quite straightforward, given Bluespec's struct+ -- initialization syntax.+ Struct s -> \v ->+ BS.CStruct+ (Just True)+ (BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName s)+ (map (\(Value ty'' field@(Field val)) ->+ ( BS.mkId BS.NoPos $ fromString+ $ lowercaseName+ $ fieldName field+ , constTy ty'' val+ ))+ (toValues v))++-- | Transform a list of Copilot Core expressions of a given 'Type' into a+-- Bluespec @Vector@ expression.+constVector :: Type a -> [a] -> BS.CExpr+constVector ty = genVector (\_ -> constTy ty)++-- | Transform a list of Copilot Core expressions into a Bluespec @Vector@+-- expression. When invoking @genVector f es@, where @es@ has length @n@, the+-- resulting @Vector@ will consist of+-- @[f 0 (es !! 0), f 1 (es !! 1), ..., f (n-1) (es !! (n-1))]@.+genVector :: (Int -> a -> BS.CExpr) -> [a] -> BS.CExpr+genVector f vec =+ snd $+ foldl'+ (\(!i, !v) x ->+ ( i+1+ , BS.CApply+ (BS.CVar (BS.mkId BS.NoPos "update"))+ [ v+ , cLit (BS.LInt (BS.ilDec (toInteger i)))+ , f i x+ ]+ ))+ (0, BS.CVar (BS.mkId BS.NoPos "newVector"))+ vec++-- | Translate a literal number of type @ty@ into a Bluespec expression.+--+-- PRE: The type of PRE is numeric (integer or floating-point), that+-- is, not boolean, struct or array.+constNumTy :: Type a -> Integer -> BS.CExpr+constNumTy ty =+ case ty of+ Float -> constFP ty . fromInteger+ Double -> constFP ty . fromInteger+ _ -> constInt ty++-- | Translate a Copilot integer literal into a Bluespec expression.+constInt :: Type a -> Integer -> BS.CExpr+constInt ty i+ -- Bluespec intentionally does not support negative literal syntax (e.g.,+ -- -42), so we must create negative integer literals using the `negate`+ -- function.+ | i >= 0 = withTypeAnnotation ty $ cLit $ BS.LInt $ BS.ilDec i+ | otherwise = withTypeAnnotation ty $+ BS.CApply+ (BS.CVar $ BS.idNegateAt BS.NoPos)+ [cLit $ BS.LInt $ BS.ilDec $ negate i]++-- | Translate a Copilot floating-point literal into a Bluespec expression.+constFP :: Type ty -> Double -> BS.CExpr+constFP ty d+ -- Bluespec intentionally does not support negative literal syntax (e.g.,+ -- -42.5), so we must create negative floating-point literals using the+ -- `negate` function.+ | d >= 0 = withTypeAnnotation ty $ cLit $ BS.LReal d+ | otherwise = withTypeAnnotation ty $+ BS.CApply+ (BS.CVar $ BS.idNegateAt BS.NoPos)+ [cLit $ BS.LReal $ negate d]++-- | Create a Bluespec expression consisting of a literal.+cLit :: BS.Literal -> BS.CExpr+cLit = BS.CLit . BS.CLiteral BS.NoPos++-- | Create a Bluespec expression that indexes into a @Vector@.+cIndexVector :: BS.CExpr -> BS.CExpr -> BS.CExpr+cIndexVector vec idx =+ BS.CApply (BS.CVar (BS.mkId BS.NoPos "select")) [vec, idx]++-- | Explicitly annotate an expression with a type signature. This is necessary+-- to prevent expressions from having ambiguous types in certain situations.+withTypeAnnotation :: Type a -> BS.CExpr -> BS.CExpr+withTypeAnnotation ty e = e `BS.CHasType` BS.CQType [] (transType ty)++-- | Throw an error if attempting to use a floating-point operation that+-- Bluespec does not currently support.+unsupportedFPOp :: String -> a+unsupportedFPOp op =+ error $ "Bluespec's FloatingPoint type does not support the " ++ op +++ " operation."++-- | We assume round-near-even throughout, but this variable can be changed if+-- needed. This matches the behavior of @fpRM@ in @copilot-theorem@'s+-- @Copilot.Theorem.What4.Translate@ module.+fpRM :: BS.CExpr+fpRM = BS.CCon (BS.mkId BS.NoPos "Rnd_Nearest_Even") []
+ src/Copilot/Compile/Bluespec/Name.hs view
@@ -0,0 +1,95 @@+-- | Naming of variables and functions in Bluespec.+module Copilot.Compile.Bluespec.Name+ ( argNames+ , generatorName+ , guardName+ , ifcArgName+ , indexName+ , lowercaseName+ , specIfcName+ , specIfcPkgName+ , specTypesPkgName+ , streamAccessorName+ , streamElemName+ , streamName+ , uppercaseName+ ) where++-- External imports+import Data.Char (isLower, isUpper)++-- External imports: Copilot+import Copilot.Core (Id)++-- | Turn a specification name into the name of its module interface.+specIfcName :: String -> String+specIfcName prefix = uppercaseName (specIfcPkgName prefix)++-- | Turn a specification name into the name of the package that declares its+-- module interface. Note that 'specIfcPkgName' is not necessarily the same name+-- as 'specIfcName', as the former does not need to begin with an uppercase+-- letter, but the latter does.+specIfcPkgName :: String -> String+specIfcPkgName prefix = prefix ++ "Ifc"++-- | Turn a specification name into the name of the package that declares its+-- struct types.+specTypesPkgName :: String -> String+specTypesPkgName prefix = prefix ++ "Types"++-- | Turn a stream id into a stream element name.+streamElemName :: Id -> Int -> String+streamElemName sId n = streamName sId ++ "_" ++ show n++-- | The name of the variable of type @<prefix>Ifc@. This is used to select+-- trigger functions and external variables.+ifcArgName :: String+ifcArgName = "ifc"++-- | Create a Bluespec name that must start with an uppercase letter (e.g., a+-- struct or interface name). If the supplied name already begins with an+-- uppercase letter, this function returns the name unchanged. Otherwise, this+-- function prepends a @BS_@ prefix (short for \"Bluespec\") at the front.+uppercaseName :: String -> String+uppercaseName [] = []+uppercaseName n@(c:_)+ | isUpper c = n+ | otherwise = "BS_" ++ n++-- | Create a Bluespec name that must start with a lowercase letter (e.g., a+-- function or method name). If the supplied name already begins with a+-- lowercase letter, this function returns the name unchanged. Otherwise, this+-- function prepends a @bs_@ prefix (short for \"Bluespec\") at the front.+lowercaseName :: String -> String+lowercaseName [] = []+lowercaseName n@(c:_)+ | isLower c = n+ | otherwise = "bs_" ++ n++-- | Turn a stream id into a suitable Bluespec variable name.+streamName :: Id -> String+streamName sId = "s" ++ show sId++-- | Turn a stream id into the global varname for indices.+indexName :: Id -> String+indexName sId = streamName sId ++ "_idx"++-- | Turn a stream id into the name of its accessor function+streamAccessorName :: Id -> String+streamAccessorName sId = streamName sId ++ "_get"++-- | Turn stream id into name of its generator function.+generatorName :: Id -> String+generatorName sId = streamName sId ++ "_gen"++-- | Turn the name of a trigger into a guard generator.+guardName :: String -> String+guardName name = lowercaseName name ++ "_guard"++-- | Turn a trigger name into a an trigger argument name.+argName :: String -> Int -> String+argName name n = lowercaseName name ++ "_arg" ++ show n++-- | Enumerate all argument names based on trigger name.+argNames :: String -> [String]+argNames base = map (argName base) [0..]
+ src/Copilot/Compile/Bluespec/Settings.hs view
@@ -0,0 +1,14 @@+-- | Settings used by the code generator to customize the code.+module Copilot.Compile.Bluespec.Settings+ ( BluespecSettings(..)+ , mkDefaultBluespecSettings+ ) where++-- | Settings used to customize the code generated.+newtype BluespecSettings = BluespecSettings+ { bluespecSettingsOutputDirectory :: FilePath+ }++-- | Default Bluespec settings. Output to the current directory.+mkDefaultBluespecSettings :: BluespecSettings+mkDefaultBluespecSettings = BluespecSettings "."
+ src/Copilot/Compile/Bluespec/Type.hs view
@@ -0,0 +1,95 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}++-- | Translate Copilot Core expressions and operators to Bluespec.+module Copilot.Compile.Bluespec.Type+ ( transType+ , tVector+ ) where++-- External imports+import Data.String (IsString (..))+import qualified Language.Bluespec.Classic.AST as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS+import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS++-- Internal imports: Copilot+import Copilot.Core++-- Internal imports+import Copilot.Compile.Bluespec.Name++-- | Translate a Copilot type to a Bluespec type.+transType :: Type a -> BS.CType+transType ty = case ty of+ Bool -> BS.tBool+ Int8 -> BS.tInt `BS.TAp` BS.cTNum 8 BS.NoPos+ Int16 -> BS.tInt `BS.TAp` BS.cTNum 16 BS.NoPos+ Int32 -> BS.tInt `BS.TAp` BS.cTNum 32 BS.NoPos+ Int64 -> BS.tInt `BS.TAp` BS.cTNum 64 BS.NoPos+ Word8 -> BS.tUInt `BS.TAp` BS.cTNum 8 BS.NoPos+ Word16 -> BS.tUInt `BS.TAp` BS.cTNum 16 BS.NoPos+ Word32 -> BS.tUInt `BS.TAp` BS.cTNum 32 BS.NoPos+ Word64 -> BS.tUInt `BS.TAp` BS.cTNum 64 BS.NoPos++ Float -> BS.TCon $+ BS.TyCon+ { BS.tcon_name = BS.mkId BS.NoPos "Float"+ , BS.tcon_kind = Just BS.KStar+ , BS.tcon_sort = BS.TItype 0 $ tFloatingPoint `BS.TAp`+ BS.cTNum 8 BS.NoPos `BS.TAp`+ BS.cTNum 23 BS.NoPos+ }+ Double -> BS.TCon $+ BS.TyCon+ { BS.tcon_name = BS.mkId BS.NoPos "Double"+ , BS.tcon_kind = Just BS.KStar+ , BS.tcon_sort = BS.TItype 0 $ tFloatingPoint `BS.TAp`+ BS.cTNum 11 BS.NoPos `BS.TAp`+ BS.cTNum 52 BS.NoPos+ }+ Array ty' -> tVector `BS.TAp` BS.cTNum len BS.NoPos `BS.TAp` transType ty'+ where+ len = toInteger $ typeLength ty+ Struct s -> BS.TCon $+ BS.TyCon+ { BS.tcon_name = BS.mkId BS.NoPos $+ fromString $+ uppercaseName $+ typeName s+ , BS.tcon_kind = Just BS.KStar+ , BS.tcon_sort =+ BS.TIstruct BS.SStruct $+ map (\(Value _tu field) ->+ BS.mkId BS.NoPos $+ fromString $+ lowercaseName $+ fieldName field)+ (toValues s)+ }++-- | The @Vector@ Bluespec data type.+tVector :: BS.CType+tVector = BS.TCon $+ BS.TyCon+ { BS.tcon_name = BS.idVector+ , BS.tcon_kind = Just (BS.Kfun BS.KNum (BS.Kfun BS.KStar BS.KStar))+ , BS.tcon_sort =+ BS.TIdata+ { BS.tidata_cons = [BS.mkId BS.NoPos "V"]+ , BS.tidata_enum = False+ }+ }++-- | The @FloatingPoint@ Bluespec struct type.+tFloatingPoint :: BS.CType+tFloatingPoint = BS.TCon $+ BS.TyCon+ { BS.tcon_name = BS.mkId BS.NoPos "FloatingPoint"+ , BS.tcon_kind = Just (BS.Kfun BS.KNum (BS.Kfun BS.KNum BS.KStar))+ , BS.tcon_sort =+ BS.TIstruct BS.SStruct [ BS.mkId BS.NoPos "sign"+ , BS.mkId BS.NoPos "exp"+ , BS.mkId BS.NoPos "sfd"+ ]+ }
+ tests/Main.hs view
@@ -0,0 +1,18 @@+-- | Test copilot-bluespec.+module Main where++-- External imports+import Test.Framework (Test, defaultMain)++-- Internal library modules being tested+import qualified Test.Copilot.Compile.Bluespec++-- | Run all unit tests on copilot-bluespec.+main :: IO ()+main = defaultMain tests++-- | All unit tests in copilot-bluespec.+tests :: [Test.Framework.Test]+tests =+ [ Test.Copilot.Compile.Bluespec.tests+ ]
+ tests/Test/Copilot/Compile/Bluespec.hs view
@@ -0,0 +1,971 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+-- | Test copilot-bluespec:Copilot.Compile.Bluespec.+module Test.Copilot.Compile.Bluespec+ ( tests )+ where++-- External imports+import Control.Arrow ((&&&))+import Control.Exception (IOException, catch)+import Control.Monad (when)+import Data.Bits (Bits, complement)+import Data.Foldable (foldl')+import Data.List (intercalate)+import Data.Type.Equality (testEquality)+import Data.Typeable (Proxy (..), (:~:) (Refl))+import GHC.TypeLits (KnownNat, natVal)+import System.Directory (doesFileExist,+ getTemporaryDirectory,+ removeDirectoryRecursive,+ setCurrentDirectory)+import System.IO (hPutStrLn, stderr)+import System.Posix.Temp (mkdtemp)+import System.Process (callProcess, readProcess)+import System.Random (Random)+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.QuickCheck (Arbitrary, Gen, Property,+ arbitrary, choose, elements,+ forAll, forAllBlind, frequency,+ getPositive, ioProperty, oneof,+ vectorOf, withMaxSuccess, (.&&.))+import Test.QuickCheck.Gen (chooseAny, chooseBoundedIntegral)++-- External imports: Copilot+import Copilot.Core hiding (Property)++-- External imports: Modules being tested+import Copilot.Compile.Bluespec (bluespecSettingsOutputDirectory,+ compile, compileWith,+ mkDefaultBluespecSettings)+import Copilot.Compile.Bluespec.External (External (extName), gatherExts)++-- * Constants++-- | All unit tests for copilot-bluespec:Copilot.Compile.Bluespec.+tests :: Test.Framework.Test+tests =+ testGroup "Copilot.Compile.Bluespec"+ [ testProperty "Compile specification" testCompile+ , testProperty "Compile specification in custom dir" testCompileCustomDir+ , testProperty "Run specification" testRun+ , testProperty "Run and compare results" testRunCompare+ ]++-- * Individual tests++-- | Test compiling a spec.+testCompile :: Property+testCompile = ioProperty $ do+ tmpDir <- getTemporaryDirectory+ setCurrentDirectory tmpDir++ testDir <- mkdtemp "CopilotTest"+ setCurrentDirectory testDir++ compile "CopilotTest" spec+ r <- compileBluespec "CopilotTest" []++ setCurrentDirectory tmpDir+ removeDirectoryRecursive testDir++ return r++ where++ spec = Spec streams observers triggers properties++ streams = []+ observers = []+ triggers = [ Trigger function guard args ]+ properties = []++ function = "func"++ guard = Const Bool True++ args = []++-- | Test compiling a spec in a custom directory.+testCompileCustomDir :: Property+testCompileCustomDir = ioProperty $ do+ tmpDir <- getTemporaryDirectory+ setCurrentDirectory tmpDir++ testDir <- mkdtemp "CopilotTest"++ compileWith (mkDefaultBluespecSettings+ { bluespecSettingsOutputDirectory = testDir })+ "CopilotTest"+ spec++ setCurrentDirectory testDir+ r <- compileBluespec "CopilotTest" []++ setCurrentDirectory tmpDir+ removeDirectoryRecursive testDir++ return r++ where++ spec = Spec streams observers triggers properties++ streams = []+ observers = []+ triggers = [ Trigger function guard args ]+ properties = []++ function = "nop"++ guard = Const Bool True++ args = []++-- | Test compiling a spec and running the resulting program.+--+-- The actual behavior is ignored.+testRun :: Property+testRun = ioProperty $ do+ tmpDir <- getTemporaryDirectory+ setCurrentDirectory tmpDir++ testDir <- mkdtemp "CopilotTest"+ setCurrentDirectory testDir++ let bluespecProgram = unlines+ [ "package Top where"+ , ""+ , "import CopilotTest"+ , "import CopilotTestIfc"+ , "import CopilotTestTypes"+ , ""+ , "copilotTestIfc :: Module CopilotTestIfc"+ , "copilotTestIfc ="+ , " module"+ , " interface"+ , " nop :: Action"+ , " nop = return ()"+ , ""+ , "mkTop :: Module Empty"+ , "mkTop = mkCopilotTest copilotTestIfc"+ ]++ writeFile "Top.bs" bluespecProgram++ compile "CopilotTest" spec+ r <- compileBluespec "Top" ["-g", "mkTop"]++ -- Compile a main program+ r2 <- compileExecutable "mkTop"+ callProcess "./mkTop" ["-m", "2"]++ setCurrentDirectory tmpDir+ removeDirectoryRecursive testDir++ return $ r && r2++ where++ spec = Spec streams observers triggers properties++ streams = []+ observers = []+ triggers = [ Trigger function guard args ]+ properties = []++ function = "nop"++ guard = Const Bool True++ args = []++-- | Test running compiled spec and comparing the results to the+-- expectation.+testRunCompare :: Property+testRunCompare =+ -- It takes a pretty long time to run these tests, so we set the maximum+ -- number of successful tests to 5 instead of the default (100) for the sake+ -- of making the test suite complete in a more reasonable amount of time.+ withMaxSuccess 5 $+ testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int8 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int16 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int32 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int64 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word8 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word16 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word32 Bool))+ .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word64 Bool))+ .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Float Bool))+ .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Double Bool))+ .&&. testRunCompare1 (arbitraryOpStruct :: Gen (TestCase1 MyStruct Int8))+ .&&. testRunCompare2 (arbitraryArrayNum :: Gen (TestCase2 (Array 2 Int8) Word32 Int8))+ .&&. testRunCompare2 (arbitraryArrayNum :: Gen (TestCase2 (Array 2 Int16) Word32 Int16))++-- * Random generators++-- ** Random function generators++-- | Generator of functions that produce booleans.+arbitraryOpBool :: Typed a => Gen (Fun a Bool, [a] -> [Bool])+arbitraryOpBool =+ frequency+ [ (5, arbitraryOp1Any)+ , (5, funCompose1 <$> arbitraryOp1Bool <*> arbitraryOpBool)+ , (2, funCompose2 <$> arbitraryOp2Bool <*> arbitraryOpBool <*> arbitraryOpBool)+ , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBool <*> arbitraryOpBool)+ ]++-- | Generator of functions that take Bits and produce booleans.+arbitraryOpBoolBits :: (Typed a, Bits a) => Gen (Fun a Bool, [a] -> [Bool])+arbitraryOpBoolBits =+ frequency+ [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBits <*> arbitraryOpBits)+ ]++-- | Generator of functions that take Nums and produce booleans.+arbitaryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a)+ => Gen (Fun a Bool, [a] -> [Bool])+arbitaryOpBoolOrdEqNum =+ frequency+ [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum <*> arbitraryOpNum)+ , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpNum <*> arbitraryOpNum)+ ]++-- | Generator of functions that take Floating point numbers and produce+-- booleans.+arbitraryOpBoolEqNumFloat :: (Typed t, Eq t, Num t, Floating t)+ => Gen (Fun t Bool, [t] -> [Bool])+arbitraryOpBoolEqNumFloat =+ frequency+ [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum <*> arbitraryOpFloat)+ , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpFloat <*> arbitraryOpNum)+ ]++-- | Generator of functions that take and produce Bits.+arbitraryOpBits :: (Bits t, Typed t)+ => Gen (Fun t t, [t] -> [t])+arbitraryOpBits = elements+ [ (Op1 (BwNot typeOf), fmap complement)+ ]++-- | Generator of functions that take and produce Nums.+arbitraryOpNum :: (Typed t, Num t) => Gen (Fun t t, [t] -> [t])+arbitraryOpNum = elements+ [ (Op1 (Abs typeOf), fmap abs)+ , (Op1 (Sign typeOf), fmap signum)+ ]++-- | Generator of functions that take an arrays and indicates and produce+-- elements from the array.+arbitraryArrayIx :: forall t n . (Typed t, KnownNat n, Num t)+ => Gen ( Fun2 (Array n t) Word32 t+ , [Array n t] -> [Word32] -> [t]+ )+arbitraryArrayIx = return+ (Op2 (Index typeOf), zipWith (\x y -> arrayElems x !! fromIntegral y))++-- | Generator of functions that take structs produce fields of the struct.+arbitraryStructField :: Gen ( Fun MyStruct Int8+ , [MyStruct] -> [Int8]+ )+arbitraryStructField = elements+ [ (Op1 (GetField typeOf typeOf myStruct1), fmap (unField . myStruct1))+ , (Op1 (GetField typeOf typeOf myStruct2), fmap (unField . myStruct2))+ ]++-- | Generator of functions on Floating point numbers.+arbitraryOpFloat :: (Floating t, Typed t) => Gen (Fun t t, [t] -> [t])+arbitraryOpFloat = elements+ [ (Op1 (Sqrt typeOf), fmap sqrt)+ , (Op1 (Recip typeOf), fmap recip)+ ]++-- | Generator of functions on that produce elements of any type.+arbitraryOp1Any :: forall a b+ . (Arbitrary b, Typed a, Typed b)+ => Gen (Fun a b, [a] -> [b])+arbitraryOp1Any = oneof $+ [ (\v -> (\_ -> Const typeOf v, fmap (const v))) <$> arbitrary ]+ +++ rest+ where+ rest | Just Refl <- testEquality t1 t2+ = [return (id, id)]+ | otherwise+ = []++ t1 :: Type a+ t1 = typeOf++ t2 :: Type b+ t2 = typeOf++-- | Generator of functions on Booleans.+arbitraryOp1Bool :: Gen (Fun Bool Bool, [Bool] -> [Bool])+arbitraryOp1Bool = elements+ [ (Op1 Not, fmap not)+ ]++-- | Generator of binary functions on Booleans.+arbitraryOp2Bool :: Gen (Fun2 Bool Bool Bool, [Bool] -> [Bool] -> [Bool])+arbitraryOp2Bool = elements+ [ (Op2 And, zipWith (&&))+ , (Op2 Or, zipWith (||))+ ]++-- | Generator of binary functions that take two Eq elements of the same type+-- and return a Bool.+arbitraryOp2Eq :: (Typed t, Eq t)+ => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool])+arbitraryOp2Eq = elements+ [ (Op2 (Eq typeOf), zipWith (==))+ , (Op2 (Ne typeOf), zipWith (/=))+ ]++-- | Generator of binary functions that take two Ord elements of the same type+-- and return a Bool.+arbitraryOp2Ord :: (Typed t, Ord t)+ => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool])+arbitraryOp2Ord = elements+ [ (Op2 (Le typeOf), zipWith (<=))+ , (Op2 (Lt typeOf), zipWith (<))+ , (Op2 (Ge typeOf), zipWith (>=))+ , (Op2 (Gt typeOf), zipWith (>))+ ]++-- ** Random data generators++-- | Random array generator.+arbitraryArray :: forall n t . (KnownNat n, Random t) => Gen (Array n t)+arbitraryArray = array <$> vectorOf len chooseAny+ where+ len :: Int+ len = fromIntegral $ natVal (Proxy :: Proxy n)++-- | Random struct generator.+arbitraryStruct :: Gen MyStruct+arbitraryStruct = do+ fld1 <- Field <$> gen+ fld2 <- Field <$> gen+ return $ MyStruct fld1 fld2+ where+ gen :: Gen Int8+ gen = chooseBoundedIntegral (minBound, maxBound)++-- ** Random test case generators++-- | Generator for test cases on integral numbers that produce booleans.+arbitraryOpIntegralBool :: (Typed t, Bounded t, Integral t, Bits t)+ => Gen (TestCase1 t Bool)+arbitraryOpIntegralBool = frequency+ [ (5, mkTestCase1+ arbitraryOpBool+ (chooseBoundedIntegral (minBound, maxBound)))++ , (2, mkTestCase1+ arbitraryOpBoolBits+ (chooseBoundedIntegral (minBound, maxBound)))++ -- we need to use +1 because certain operations overflow the number+ , (2, mkTestCase1+ arbitaryOpBoolOrdEqNum+ (chooseBoundedIntegral (minBound + 1, maxBound)))+ ]++-- | Generator for test cases on floating-point numbers that produce booleans.+arbitraryOpFloatingBool :: (Random t, Typed t, Floating t, Eq t)+ => Gen (TestCase1 t Bool)+arbitraryOpFloatingBool = oneof+ [ mkTestCase1 arbitraryOpBoolEqNumFloat chooseAny+ ]++-- | Generator for test cases on Arrays selection producing values of the+-- array.+arbitraryArrayNum :: forall n a+ . (KnownNat n, Num a, Random a, Typed a)+ => Gen (TestCase2 (Array n a) Word32 a)+arbitraryArrayNum = oneof+ [ mkTestCase2 arbitraryArrayIx arbitraryArray gen+ ]+ where+ gen :: Gen Word32+ gen = choose (0, len - 1)++ len :: Word32+ len = fromIntegral $ natVal (Proxy :: Proxy n)++-- | Generator for test cases on structs that produce fields of the struct.+arbitraryOpStruct :: Gen (TestCase1 MyStruct Int8)+arbitraryOpStruct = oneof+ [ mkTestCase1+ arbitraryStructField+ arbitraryStruct+ ]++-- * Semantics++-- ** Functions++-- | Unary Copilot function.+type Fun a b = Expr a -> Expr b++-- | Binary Copilot function.+type Fun2 a b c = Expr a -> Expr b -> Expr c++-- | Compose functions, paired with the Haskell functions that define their+-- idealized meaning.+funCompose1 :: (Fun b c, [b] -> [c])+ -> (Fun a b, [a] -> [b])+ -> (Fun a c, [a] -> [c])+funCompose1 (f1, g1) (f2, g2) = (f1 . f2, g1 . g2)++-- | Compose a binary function, with two functions, one for each argument.+funCompose2 :: (Fun2 b c d, [b] -> [c] -> [d])+ -> (Fun a b, [a] -> [b])+ -> (Fun a c, [a] -> [c])+ -> (Fun a d, [a] -> [d])+funCompose2 (f1, g1) (f2, g2) (f3, g3) =+ (uncurry f1 . (f2 &&& f3), uncurry g1 . (g2 &&& g3))++-- ** Test cases++-- | Test case specification for specs with one input variable and one output.+data TestCase1 a b = TestCase1+ { wrapTC1Expr :: Spec+ -- ^ Specification containing a trigger an extern of type 'a' and a trigger+ -- with an argument of type 'b'.++ , wrapTC1Fun :: [a] -> [b]+ -- ^ Function expected to function in the same way as the Spec being+ -- tested.++ , wrapTC1CopInp :: (Type a, String, Gen a)+ -- ^ Input specification.+ --+ -- - The first element contains the type of the input in Bluespec.+ --+ -- - The second contains the variable name in Bluespec.+ --+ -- - The latter contains a randomized generator for values of the given+ -- type.++ , wrapTC1CopOut :: Type b+ -- ^ The type of the output in Bluespec.+ }++-- | Test case specification for specs with two input variables and one output.+data TestCase2 a b c = TestCase2+ { wrapTC2Expr :: Spec+ -- ^ Specification containing a trigger an extern of type 'a' and a trigger+ -- with an argument of type 'b'.++ , wrapTC2Fun :: [a] -> [b] -> [c]+ -- ^ Function expected to function in the same way as the Spec being+ -- tested.++ , wrapTC2CopInp1 :: (Type a, String, Gen a)+ -- ^ Input specification for the first input.+ --+ -- - The first element contains the type of the input in Bluespec.+ --+ -- - The second contains the variable name in Bluespec.+ --+ -- - The latter contains a randomized generator for values of the given+ -- type.++ , wrapTC2CopInp2 :: (Type b, String, Gen b)+ -- ^ Input specification for the second input.+ --+ -- - The first element contains the type of the input in Bluespec.+ --+ -- - The second contains the variable name in Bluespec.+ --+ -- - The latter contains a randomized generator for values of the given+ -- type.++ , wrapTC2CopOut :: Type c+ -- ^ The type of the output in Bluespec.+ }++-- | Generate test cases for expressions that behave like unary functions.+mkTestCase1 :: (Typed a, Typed b)+ => Gen (Fun a b, [a] -> [b])+ -> Gen a+ -> Gen (TestCase1 a b)+mkTestCase1 genO gen = do+ (copilotF, semF) <- genO++ let spec = alwaysTriggerArg1 (UExpr t2 appliedOp)+ appliedOp = copilotF (ExternVar t1 varName Nothing)++ return $+ TestCase1+ { wrapTC1Expr = spec+ , wrapTC1Fun = semF+ , wrapTC1CopInp = ( t1, varName, gen )+ , wrapTC1CopOut = t2+ }++ where++ t1 = typeOf+ t2 = typeOf++ varName = "input"++-- | Generate test cases for expressions that behave like binary functions.+mkTestCase2 :: (Typed a, Typed b, Typed c)+ => Gen (Fun2 a b c, [a] -> [b] -> [c])+ -> Gen a+ -> Gen b+ -> Gen (TestCase2 a b c)+mkTestCase2 genO genA genB = do+ (copilotF, semF) <- genO++ let spec = alwaysTriggerArg1 (UExpr t3 appliedOp)+ appliedOp = copilotF (ExternVar t1 varName1 Nothing)+ (ExternVar t2 varName2 Nothing)++ return $+ TestCase2+ { wrapTC2Expr = spec+ , wrapTC2Fun = semF+ , wrapTC2CopInp1 = ( t1, varName1, genA )+ , wrapTC2CopInp2 = ( t2, varName2, genB )+ , wrapTC2CopOut = t3+ }++ where++ t1 = typeOf+ t2 = typeOf+ t3 = typeOf++ varName1 = "input1"+ varName2 = "input2"++-- | Test running a compiled Bluespec program and comparing the results.+testRunCompare1 :: (Show a, Typed a, ReadableFromBluespec b, Eq b, Typed b)+ => Gen (TestCase1 a b) -> Property+testRunCompare1 ops =+ forAllBlind ops $ \testCase ->+ let (TestCase1+ { wrapTC1Expr = copilotSpec+ , wrapTC1Fun = haskellFun+ , wrapTC1CopInp = inputVar+ , wrapTC1CopOut = outputType+ }) = testCase+ (bluespecTypeInput, bluespecInputName, gen) = inputVar++ in forAll (getPositive <$> arbitrary) $ \len ->++ forAll (vectorOf len gen) $ \nums -> do++ let inputs = filterOutUnusedExts+ copilotSpec+ [ (typeBluespec bluespecTypeInput,+ fmap (bluespecShow bluespecTypeInput) nums,+ bluespecInputName)+ ]+ outputs = haskellFun nums++ testRunCompareArg+ inputs len outputs copilotSpec (typeBluespec outputType)++-- | Test running a compiled Bluespec program and comparing the results.+testRunCompare2 :: (Show a1, Typed a1, Show a2, Typed a2,+ ReadableFromBluespec b, Eq b, Typed b)+ => Gen (TestCase2 a1 a2 b) -> Property+testRunCompare2 ops =+ forAllBlind ops $ \testCase ->+ let (TestCase2+ { wrapTC2Expr = copilotSpec+ , wrapTC2Fun = haskellFun+ , wrapTC2CopInp1 = inputVar1+ , wrapTC2CopInp2 = inputVar2+ , wrapTC2CopOut = outputType+ }) =+ testCase++ (bluespecTypeInput1, bluespecInputName1, gen1) = inputVar1+ (bluespecTypeInput2, bluespecInputName2, gen2) = inputVar2++ in forAll (getPositive <$> arbitrary) $ \len ->+ forAll (vectorOf len gen1) $ \nums1 ->+ forAll (vectorOf len gen2) $ \nums2 -> do+ let inputs = filterOutUnusedExts+ copilotSpec+ [ (typeBluespec bluespecTypeInput1,+ fmap (bluespecShow bluespecTypeInput1) nums1,+ bluespecInputName1)+ , (typeBluespec bluespecTypeInput2,+ fmap (bluespecShow bluespecTypeInput2) nums2,+ bluespecInputName2)+ ]+ outputs = haskellFun nums1 nums2++ testRunCompareArg+ inputs len outputs copilotSpec (typeBluespec outputType)++-- | Test running a compiled Bluespec program and comparing the results, when+-- the program produces one output as an argument to a trigger that always+-- fires.+--+-- PRE: all lists (second argument) of inputs have the length given as second+-- argument.+--+-- PRE: the monitoring code this is linked against uses the function+-- @printBack@ with exactly one argument to pass the results.+testRunCompareArg :: (ReadableFromBluespec b, Eq b)+ => [(String, [String], String)]+ -> Int+ -> [b]+ -> Spec+ -> String+ -> Property+testRunCompareArg inputs numInputs nums spec outputType =+ ioProperty $ do+ tmpDir <- getTemporaryDirectory+ setCurrentDirectory tmpDir++ -- Operate in temporary directory+ testDir <- mkdtemp "CopilotTest"+ setCurrentDirectory testDir++ -- Produce wrapper program+ let bluespecProgram =+ testRunCompareArgBluespecProgram inputs outputType+ writeFile "Top.bs" bluespecProgram++ -- Produce copilot monitoring code+ compile "CopilotTest" spec+ r <- compileBluespec "Top" ["-g", "mkTop"]++ -- Compile main program+ r2 <- compileExecutable "mkTop"++ -- Print result so far (for debugging purposes only)+ {-+ print r2+ print testDir+ -}++ -- Run program and compare result+ out <- readProcess "./mkTop" ["-m", show (numInputs + 2)] ""+ let outNums = readFromBluespec <$> lines out+ comparison = outNums == nums++ -- Only clean up if the test succeeded; otherwise, we want to inspect it.+ when comparison $ do+ -- Remove temporary directory+ setCurrentDirectory tmpDir+ removeDirectoryRecursive testDir++ return $ r && r2 && comparison++-- | Return a wrapper Bluespec program that runs for a number of clock cycles,+-- updating external stream registers on every cycle, running the monitors, and+-- publishing the results of any outputs.+testRunCompareArgBluespecProgram+ :: [(String, [String], String)]+ -> String+ -> String+testRunCompareArgBluespecProgram inputs outputType = unlines $+ [ "package Top where"+ , ""+ , "import FloatingPoint"+ , "import Vector"+ , ""+ , "import CopilotTest"+ , "import CopilotTestIfc"+ , "import CopilotTestTypes"+ , ""+ ]+ ++ inputVecDecls +++ [ ""+ , "copilotTestIfc :: Module CopilotTestIfc"+ , "copilotTestIfc ="+ , " module"+ ]+ ++ inputRegs +++ [ " i :: Reg (Bit 64) <- mkReg 0"+ , " ready :: Reg Bool <- mkReg False"+ , " interface"+ , " printBack :: " ++ outputType ++ " -> Action"+ , " printBack num = $display (fshow num)"+ , " when ready"+ , ""+ ]+ ++ inputMethods +++ [ ""+ , " rules"+ , " \"inputs\": when True ==> do"+ ]+ ++ inputUpdates +++ [ " i := i + 1"+ , " ready := True"+ , ""+ , "mkTop :: Module Empty"+ , "mkTop = mkCopilotTest copilotTestIfc"+ ]+ where+ inputVecDecls :: [String]+ inputVecDecls =+ concatMap+ (\(bluespecType, _varName, _regName, inputVecName, inputVals) ->+ [ inputVecName ++ " :: Vector " ++ show (length inputVals) +++ " (" ++ bluespecType ++ ")"+ , inputVecName ++ " = " ++ genVector inputVals+ ])+ vars++ inputRegs :: [String]+ inputRegs =+ map+ (\(bluespecType, _varName, regName, _inputVecName, _inputVals) ->+ " " ++ regName ++ " :: Reg (" ++ bluespecType ++ ") <- mkRegU")+ vars++ inputMethods :: [String]+ inputMethods =+ concatMap+ (\(bluespecType, varName, regName, _inputVecName, _inputVals) ->+ [ " " ++ varName ++ " :: Reg (" ++ bluespecType ++ ")"+ , " " ++ varName ++ " = " ++ regName+ ])+ vars++ inputUpdates :: [String]+ inputUpdates =+ map+ (\(_bluespecType, _varName, regName, inputVecName, _inputVals) ->+ " " ++ regName ++ " := select " ++ inputVecName ++ " i")+ vars++ vars = map oneInput inputs+ oneInput (bluespecTypeInput, inputVals, bluespecInputName) =+ (bluespecTypeInput, inputVarName, inputRegVarName, inputVecVarName,+ inputVals)+ where+ inputVarName = bluespecInputName+ inputRegVarName = bluespecInputName ++ "Impl"+ inputVecVarName = bluespecInputName ++ "Inputs"++-- * Auxiliary functions++-- ** Specs handling++-- | Build a 'Spec' that triggers at every step, passing the given expression+-- as argument, and execution a function 'printBack'.+alwaysTriggerArg1 :: UExpr -> Spec+alwaysTriggerArg1 = triggerArg1 (Const Bool True)++ where++ -- | Build a 'Spec' that triggers based on a given boolean stream, passing+ -- the given expression as argument, and execution a function 'printBack'.+ triggerArg1 :: Expr Bool -> UExpr -> Spec+ triggerArg1 guard expr = Spec streams observers triggers properties++ where++ streams = []+ observers = []+ properties = []++ triggers = [ Trigger function guard args ]+ function = "printBack"+ args = [ expr ]++-- | Filter out any elements in the input list (of type @[(a, b, String)]@)+-- whose first element (the name of an external stream) does not correspond to+-- the name of an external stream in the supplied 'Spec'. For example, a Copilot+-- source program may declare external streams, but if none of them are used in+-- the 'Spec', then the 'Spec' value itself will not contain any external stream+-- definitions. As a result, we want to ensure that the input list also does not+-- contain any external streams.+filterOutUnusedExts :: Spec -> [(a, b, String)] -> [(a, b, String)]+filterOutUnusedExts spec = filter (\(_, _, name) -> name `elem` extNames)+ where+ extNames = map extName $ gatherExts (specStreams spec) (specTriggers spec)++-- ** Compilation of Bluespec programs++-- | Compile a Bluespec file given its basename.+compileBluespec :: String -> [String] -> IO Bool+compileBluespec baseName extraArgs = do+ result <- catch (do callProcess "bsc" $ extraArgs +++ [ "-sim", "-quiet", "-u",+ -- We suppress the G0023 warning,+ -- which arises due to the `nop`+ -- triggers defined above. See the+ -- DESIGN.md document for more+ -- details on what these warning+ -- codes mean.+ "-suppress-warnings", "G0023:S0080",+ baseName ++ ".bs" ]+ return True+ )+ (\e -> do+ hPutStrLn stderr $+ "copilot-bluespec: error: compileBluespec: "+ ++ "cannot compile " ++ baseName ++ ".bs with bsc"+ hPutStrLn stderr $+ "copilot-bluespec: exception: " ++ show (e :: IOException)+ return False+ )+ if result+ then doesFileExist $ baseName ++ ".bo"+ else return False++-- | Compile a Bluespec file into an executable given its basename.+compileExecutable :: String -> IO Bool+compileExecutable topExe = do+ result <- catch (do callProcess "bsc" $ [ "-sim", "-quiet" ]+ ++ [ "-e", topExe ]+ ++ [ "-o", topExe ]+ return True+ )+ (\e -> do+ hPutStrLn stderr $+ "copilot-bluespec: error: compileExecutable: "+ ++ "cannot compile " ++ topExe ++ " with bsc"+ hPutStrLn stderr $+ "copilot-bluespec: exception: "+ ++ show (e :: IOException)+ return False+ )+ if result+ then doesFileExist topExe+ else return False++-- ** Interfacing between Haskell and Bluespec++-- | Bluespec type used to store values of a given type.+typeBluespec :: Typed a => Type a -> String+typeBluespec Bool = "Bool"+typeBluespec Int8 = "Int 8"+typeBluespec Int16 = "Int 16"+typeBluespec Int32 = "Int 32"+typeBluespec Int64 = "Int 64"+typeBluespec Word8 = "UInt 8"+typeBluespec Word16 = "UInt 16"+typeBluespec Word32 = "UInt 32"+typeBluespec Word64 = "UInt 64"+typeBluespec Float = "Float"+typeBluespec Double = "Double"+typeBluespec t@(Array tE) =+ "Vector " ++ show (typeLength t) ++ "(" ++ typeBluespec tE ++ ")"+typeBluespec (Struct s) = typeName s++-- | Show a value of a given type in Bluespec.+bluespecShow :: Type a -> a -> String+bluespecShow Bool x = show x+bluespecShow Int8 x = bluespecShowIntegral x+bluespecShow Int16 x = bluespecShowIntegral x+bluespecShow Int32 x = bluespecShowIntegral x+bluespecShow Int64 x = bluespecShowIntegral x+bluespecShow Word8 x = bluespecShowIntegral x+bluespecShow Word16 x = bluespecShowIntegral x+bluespecShow Word32 x = bluespecShowIntegral x+bluespecShow Word64 x = bluespecShowIntegral x+bluespecShow Float x = bluespecShowRealFrac x+bluespecShow Double x = bluespecShowRealFrac x+bluespecShow (Array tE) x = genVector $ map (bluespecShow tE) $ arrayElems x+bluespecShow (Struct s) x =+ typeName s+ ++ "{ "+ ++ intercalate ";"+ (map+ (\(Value fldTy fld@(Field val)) ->+ fieldName fld ++ " = " ++ bluespecShow fldTy val)+ (toValues x))+ ++ "}"++-- | Show a value of a integral type (e.g., 'Int8' or 'Word8').+bluespecShowIntegral :: (Integral a, Num a, Ord a, Show a) => a -> String+bluespecShowIntegral x+ | x >= 0 = show x+ -- Bluespec Haskell doesn't have negative integer literals, so something like+ -- "-42" won't parse. Instead, we must rely on Bluespec's `negate` function.+ --+ -- We must be careful to negate an Integer literal rather than than a+ -- fixed-precision literal. For instance, suppose we wanted to display+ -- (-128 :: Int8). We wouldn't want to do this by displaying `negate 128`,+ -- since 128 isn't a valid Int8 value—the maximum Int8 value is 127!+ -- Instead, we want to display `fromInteger (negate 128)`, where 128 is an+ -- Integer. This way, `negate` can turn `128` to `-128` without issues.+ | otherwise = "fromInteger (negate " ++ show (abs (toInteger x)) ++ ")"++-- | Show a value of a fractional type (e.g., 'Float' or 'Double').+bluespecShowRealFrac :: (Num a, Ord a, Show a) => a -> String+bluespecShowRealFrac x+ | x >= 0 = show x+ | otherwise = "negate " ++ show x++-- | Given a list of elements as arguments, show a @Vector@ expression. For+-- example, @'genVector' [\"27\", \"42\"]@ will return+-- @\"updateVector (updateVector newVector 0 27) 1 42)\"@.+genVector :: [String] -> String+genVector vals =+ snd $+ foldl'+ (\(!i, !v) x ->+ (i+1, "update (" ++ v ++ ") " ++ show i ++ " (" ++ x ++ ")"))+ (0 :: Int, "newVector")+ vals++-- | Read a value of a given type in Bluespec.+class ReadableFromBluespec a where+ readFromBluespec :: String -> a++instance ReadableFromBluespec Bool where+ readFromBluespec = read++instance ReadableFromBluespec Int8 where+ readFromBluespec = read++instance ReadableFromBluespec Int16 where+ readFromBluespec = read++instance ReadableFromBluespec Int32 where+ readFromBluespec = read++instance ReadableFromBluespec Int64 where+ readFromBluespec = read++instance ReadableFromBluespec Word8 where+ readFromBluespec = read++instance ReadableFromBluespec Word16 where+ readFromBluespec = read++instance ReadableFromBluespec Word32 where+ readFromBluespec = read++instance ReadableFromBluespec Word64 where+ readFromBluespec = read++-- ** A simple struct definition for unit testing purposes++data MyStruct = MyStruct+ { myStruct1 :: Field "myStruct1" Int8+ , myStruct2 :: Field "myStruct2" Int8+ }++instance Struct MyStruct where+ typeName _ = "MyStruct"+ toValues ms = [ Value Int8 (myStruct1 ms)+ , Value Int8 (myStruct2 ms)+ ]++instance Typed MyStruct where+ typeOf = Struct (MyStruct (Field 0) (Field 0))++-- | Unwrap a 'Field' to obtain the underlying value.+unField :: Field s t -> t+unField (Field val) = val