copilot-bluespec 3.19 → 3.20
raw patch · 6 files changed
+573/−50 lines, 6 filesdep +ieee754dep ~copilot-corePVP ok
version bump matches the API change (PVP)
Dependencies added: ieee754
Dependency ranges changed: copilot-core
API changes (from Hackage documentation)
Files
- CHANGELOG +6/−0
- README.md +23/−4
- copilot-bluespec.cabal +4/−3
- src/Copilot/Compile/Bluespec/Expr.hs +195/−5
- tests/Main.hs +2/−2
- tests/Test/Copilot/Compile/Bluespec.hs +343/−36
CHANGELOG view
@@ -1,3 +1,9 @@+2024-07-11+ * Version bump (3.20). (#11)+ * Support translating Copilot struct updates to Bluespec (#10).+ * Fix a bug in the translation of the signum function. (#14)+ * Fix a bug in the translation of floating-point comparisons. (#15)+ 2024-03-08 * Version bump (3.19). (#5) * Create new library for Bluespec backend.
README.md view
@@ -15,14 +15,33 @@ ## 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).+[Hackage](https://hackage.haskell.org/package/copilot-bluespec). It is intended+to be installed alongside a Copilot distribution by running the following+commands: +```+$ cabal update+$ cabal install copilot+$ cabal install copilot-bluespec+```++For more detailed instructions on how to install Copilot, 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).++We also provide a [Dockerfile](Dockerfile) which automates the process of+installing Copilot, Copilot-Bluespec, and `bsc`. The Dockerfile can be built and+run using the following commands:++```+$ docker build -t <tag> .+$ docker run -it <tag>+```++Where `<tag>` is a unique name for the Docker image. ## Further information For further information, install instructions and documentation, please visit
copilot-bluespec.cabal view
@@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-bluespec-version : 3.19+version : 3.20 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec.@@ -44,7 +44,7 @@ , filepath >= 1.4 && < 1.5 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 3.19 && < 3.20+ , copilot-core >= 3.20 && < 3.21 , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec@@ -58,7 +58,7 @@ , Copilot.Compile.Bluespec.Settings , Copilot.Compile.Bluespec.Type -test-suite unit-tests+test-suite tests type: exitcode-stdio-1.0 @@ -75,6 +75,7 @@ , directory , HUnit , QuickCheck+ , ieee754 , pretty , process , random
src/Copilot/Compile/Bluespec/Expr.hs view
@@ -73,7 +73,7 @@ case op of Not -> app BS.idNot Abs _ty -> app $ BS.mkId BS.NoPos "abs"- Sign _ty -> app $ BS.mkId BS.NoPos "signum"+ Sign ty -> transSign ty e -- Bluespec's Arith class does not have a `recip` method corresponding to -- Haskell's `recip` in the `Fractional` class, so we implement it -- ourselves.@@ -128,16 +128,21 @@ 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+ Le ty -> transLe ty e1 e2+ Ge ty -> transGe ty e1 e2+ Lt ty -> transLt ty e1 e2+ Gt ty -> transGt ty e1 e2 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+ UpdateField (Struct _) _ f ->+ let field :: BS.FString+ field = fromString $ lowercaseName $ accessorName f in+ BS.CStructUpd e1 [(BS.mkId BS.NoPos field, e2)]+ UpdateField _ _ _ -> impossible "transOp2" "copilot-bluespec" -- Unsupported operations (see -- https://github.com/B-Lang-org/bsc/discussions/534)@@ -154,6 +159,185 @@ case op of Mux _ -> BS.Cif BS.NoPos e1 e2 e3 +-- | Translate @'Sign' e@ in Copilot Core into a Bluespec expression.+--+-- @signum e@ is translated as:+--+-- @+-- if e > 0 then 1 else (if e < 0 then negate 1 else e)+-- @+--+-- That is:+--+-- 1. If @e@ is positive, return @1@.+--+-- 2. If @e@ is negative, return @-1@.+--+-- 3. Otherwise, return @e@. This handles the case where @e@ is @0@ when the+-- type is an integral type. If the type is a floating-point type, it also+-- handles the cases where @e@ is @-0@ or @NaN@.+--+-- This implementation is modeled after how GHC implements 'signum'+-- <https://gitlab.haskell.org/ghc/ghc/-/blob/aed98ddaf72cc38fb570d8415cac5de9d8888818/libraries/base/GHC/Float.hs#L523-L525 here>.+transSign :: Type a -> BS.CExpr -> BS.CExpr+transSign ty e = positiveCase $ negativeCase e+ where+ -- If @e@ is positive, return @1@, otherwise fall back to the argument.+ --+ -- Produces the following code, where @<arg>@ is the argument to this+ -- function:+ -- @+ -- if e > 0 then 1 else <arg>+ -- @+ positiveCase :: BS.CExpr -- ^ Value returned if @e@ is not positive.+ -> BS.CExpr+ positiveCase =+ BS.Cif BS.NoPos (transGt ty e (constNumTy ty 0)) (constNumTy ty 1)++ -- If @e@ is negative, return @1@, otherwise fall back to the argument.+ --+ -- Produces the following code, where @<arg>@ is the argument to this+ -- function:+ -- @+ -- if e < 0 then negate 1 else <arg>+ -- @+ negativeCase :: BS.CExpr -- ^ Value returned if @e@ is not negative.+ -> BS.CExpr+ negativeCase =+ BS.Cif BS.NoPos (transLt ty e (constNumTy ty 0)) (constNumTy ty (-1))++-- | Translate a Copilot @x < y@ expression into Bluespec. We will generate+-- different code depending on whether the arguments have a floating-point type+-- or not.+transLt :: Type a+ -- ^ The type of the arguments.+ -> BS.CExpr -> BS.CExpr -> BS.CExpr+transLt ty e1 e2+ | typeIsFloating ty+ = transLtOrGtFP (BS.mkId BS.NoPos "LT") e1 e2+ | otherwise+ = BS.CApply (BS.CVar (BS.idLtAt BS.NoPos)) [e1, e2]++-- | Translate a Copilot @x > y@ expression into Bluespec. We will generate+-- different code depending on whether the arguments have a floating-point type+-- or not.+transGt :: Type a+ -- ^ The type of the arguments.+ -> BS.CExpr -> BS.CExpr -> BS.CExpr+transGt ty e1 e2+ | typeIsFloating ty+ = transLtOrGtFP (BS.mkId BS.NoPos "GT") e1 e2+ | otherwise+ = BS.CApply (BS.CVar (BS.idGtAt BS.NoPos)) [e1, e2]++-- | Translate a Copilot @x <= y@ expression into Bluespec. We will generate+-- different code depending on whether the arguments have a floating-point type+-- or not.+transLe :: Type a+ -- ^ The type of the arguments.+ -> BS.CExpr -> BS.CExpr -> BS.CExpr+transLe ty e1 e2+ | typeIsFloating ty+ = transLeOrGeFP (BS.mkId BS.NoPos "LT") e1 e2+ | otherwise+ = BS.CApply (BS.CVar (BS.idLtEqAt BS.NoPos)) [e1, e2]++-- | Translate a Copilot @x >= y@ expression into Bluespec. We will generate+-- different code depending on whether the arguments have a floating-point type+-- or not.+transGe :: Type a+ -- ^ The type of the arguments.+ -> BS.CExpr -> BS.CExpr -> BS.CExpr+transGe ty e1 e2+ | typeIsFloating ty+ = transLeOrGeFP (BS.mkId BS.NoPos "GT") e1 e2+ | otherwise+ = BS.CApply (BS.CVar (BS.idGtEqAt BS.NoPos)) [e1, e2]++-- | Translate a Copilot floating-point comparison involving @<@ or @>@ into a+-- Bluespec expression. Specifically, @x < y@ is translated to:+--+-- @+-- compareFP x y == LT+-- @+--+-- @x > y@ is translated similarly, except that @GT@ is used instead of @LT@.+--+-- See the comments on 'compareFPExpr' for why we translate floating-point+-- comparison operators this way.+transLtOrGtFP :: BS.Id+ -- ^ A @Disorder@ label, which we check against the result of+ -- calling @compareFP@. This should be either @LT@ or @GT@.+ -> BS.CExpr -> BS.CExpr -> BS.CExpr+transLtOrGtFP disorderLabel e1 e2 =+ BS.CApply+ (BS.CVar BS.idEqual)+ [compareFPExpr e1 e2, BS.CCon disorderLabel []]++-- | Translate a Copilot floating-point comparison involving @<=@ or @>=@ into+-- a Bluespec expression. Specifically, @x <= y@ is translated to:+--+-- @+-- let _c = compareFP x y+-- in (_c == LT) || (_c == EQ)+-- @+--+-- @x >= y@ is translated similarly, except that @GT@ is used instead of @LT@.+--+-- See the comments on 'compareFPExpr' for why we translate floating-point+-- comparison operators this way.+transLeOrGeFP :: BS.Id+ -- ^ A @Disorder@ label, which we check against the result of+ -- calling @compareFP@. This should be either @LT@ or @GT@.+ -> BS.CExpr -> BS.CExpr -> BS.CExpr+transLeOrGeFP disorderLabel e1 e2 =+ BS.Cletrec+ [BS.CLValue c [BS.CClause [] [] (compareFPExpr e1 e2)] []]+ (BS.CApply+ (BS.CVar (BS.idOrAt BS.NoPos))+ [ BS.CApply+ (BS.CVar BS.idEqual)+ [BS.CVar c, BS.CCon disorderLabel []]+ , BS.CApply+ (BS.CVar BS.idEqual)+ [BS.CVar c, BS.CCon (BS.mkId BS.NoPos "EQ") []]+ ])+ where+ c = BS.mkId BS.NoPos "_c"++-- | Generate an expression of the form @compareFP x y@. This is used to power+-- the translations of the Copilot @<@, @<=@, @>@, and @>=@ floating-point+-- operators to Bluespec.+--+-- Translating these operators using @compareFP@ is a somewhat curious design+-- choice, given that Bluespec already defines its own versions of these+-- operators. Unfortunately, we cannot directly use the Bluespec versions of+-- these operators, as they are defined in such a way that they will call+-- @error@ when one of the arguments is a NaN value. This would pose two+-- problems:+--+-- 1. This would differ from the semantics of Copilot, where @x < y@ will return+-- @False@ (instead of erroring) when one of the arguments is NaN. (Similarly+-- for the other floating-point comparison operators.)+--+-- 2. Moreover, if you have a Bluespec program that calls @x < y@, where the+-- value of @x@ or @y@ is derived from a register, then @bsc@ will always+-- fail to compile the code. This is because Bluespec must generate hardware+-- for all possible code paths in @<@, and because one of the code paths+-- calls @error@, this will cause compilation to result in an error. (See+-- https://github.com/B-Lang-org/bsc/discussions/711#discussioncomment-10003586+-- for a more detailed explanation.)+--+-- As such, we avoid using Bluespec's comparison operators and instead translate+-- Copilot's comparison operators to expressions derived from @compareFP@.+-- Unlike Bluespec's other comparison operators, calling @compareFP@ will never+-- result in an error.+compareFPExpr :: BS.CExpr -> BS.CExpr -> BS.CExpr+compareFPExpr e1 e2 =+ BS.CApply+ (BS.CVar (BS.mkId BS.NoPos "compareFP"))+ [e1, e2]+ -- | 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@@ -450,6 +634,12 @@ -- 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)++-- | True if the type given is a floating point number.+typeIsFloating :: Type a -> Bool+typeIsFloating Float = True+typeIsFloating Double = True+typeIsFloating _ = False -- | Throw an error if attempting to use a floating-point operation that -- Bluespec does not currently support.
tests/Main.hs view
@@ -7,11 +7,11 @@ -- Internal library modules being tested import qualified Test.Copilot.Compile.Bluespec --- | Run all unit tests on copilot-bluespec.+-- | Run all @copilot-bluespec@ tests. main :: IO () main = defaultMain tests --- | All unit tests in copilot-bluespec.+-- | All @copilot-bluespec@ tests. tests :: [Test.Framework.Test] tests = [ Test.Copilot.Compile.Bluespec.tests
tests/Test/Copilot/Compile/Bluespec.hs view
@@ -11,12 +11,18 @@ import Control.Arrow ((&&&)) import Control.Exception (IOException, catch) import Control.Monad (when)+import Data.AEq (AEq (..)) 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.Float (castDoubleToWord64,+ castFloatToWord32,+ castWord32ToFloat,+ castWord64ToDouble) import GHC.TypeLits (KnownNat, natVal)+import Numeric.IEEE (infinity, nan) import System.Directory (doesFileExist, getTemporaryDirectory, removeDirectoryRecursive,@@ -30,9 +36,11 @@ import Test.QuickCheck (Arbitrary, Gen, Property, arbitrary, choose, elements, forAll, forAllBlind, frequency,- getPositive, ioProperty, oneof,- vectorOf, withMaxSuccess, (.&&.))+ getPositive, ioProperty, once,+ oneof, vectorOf, withMaxSuccess,+ (.&&.)) import Test.QuickCheck.Gen (chooseAny, chooseBoundedIntegral)+import Text.ParserCombinators.ReadPrec (minPrec) -- External imports: Copilot import Copilot.Core hiding (Property)@@ -45,21 +53,27 @@ -- * Constants --- | All unit tests for copilot-bluespec:Copilot.Compile.Bluespec.+-- | All 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+ [ testGroup "Unit tests"+ [ testProperty "Compile specification" testCompile+ , testProperty "Compile specification in custom dir" testCompileCustomDir+ , testProperty "Run specification" testRun+ , testProperty "Run and compare results" testRunCompare+ ]+ , testGroup "Regression tests"+ [ test14+ , test15+ ] ] -- * Individual tests -- | Test compiling a spec. testCompile :: Property-testCompile = ioProperty $ do+testCompile = once $ ioProperty $ do tmpDir <- getTemporaryDirectory setCurrentDirectory tmpDir @@ -91,7 +105,7 @@ -- | Test compiling a spec in a custom directory. testCompileCustomDir :: Property-testCompileCustomDir = ioProperty $ do+testCompileCustomDir = once $ ioProperty $ do tmpDir <- getTemporaryDirectory setCurrentDirectory tmpDir @@ -129,7 +143,7 @@ -- -- The actual behavior is ignored. testRun :: Property-testRun = ioProperty $ do+testRun = once $ ioProperty $ do tmpDir <- getTemporaryDirectory setCurrentDirectory tmpDir @@ -202,9 +216,122 @@ .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Float Bool)) .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Double Bool)) .&&. testRunCompare1 (arbitraryOpStruct :: Gen (TestCase1 MyStruct Int8))+ .&&. testRunCompare2 (arbitraryOp2Struct :: Gen (TestCase2 MyStruct Int8 MyStruct)) .&&. testRunCompare2 (arbitraryArrayNum :: Gen (TestCase2 (Array 2 Int8) Word32 Int8)) .&&. testRunCompare2 (arbitraryArrayNum :: Gen (TestCase2 (Array 2 Int16) Word32 Int16)) +-- * Regression tests++-- | Regression tests for+-- https://github.com/Copilot-Language/copilot-bluespec/issues/14 which ensure+-- that @copilot-bluespec@ generates code for the @signum@ function that adheres+-- to Copilot's @signum@ semantics.+test14 :: Test.Framework.Test+test14 =+ testGroup "#14"+ [ testProperty "`signum @Int8` generates correct Bluespec code" $+ mkRegressionTest1 (Sign Int8) (fmap signum)+ [-2, -1, 0, 1, 2]+ , testProperty "`signum @Double` generates correct Bluespec code" $+ mkRegressionTest1 (Sign Double) (fmap signum)+ [-nan, -infinity, -2, -1, -0.0, 0, 1, 2, infinity, nan]+ ]++-- | Regression tests for+-- https://github.com/Copilot-Language/copilot-bluespec/issues/15 which ensure+-- that @copilot-bluespec@ generates valid code for comparison operators (('<'),+-- ('<='), ('>'), and ('>=')) that are capable of handling NaN values.+test15 :: Test.Framework.Test+test15 =+ testGroup "#15"+ [ testProperty "Generates valid (<) code for NaNs" $+ mkRegressionTest2 (Lt Double) (zipWith (<)) vals+ , testProperty "Generates valid (<=) code for NaNs" $+ mkRegressionTest2 (Le Double) (zipWith (<=)) vals+ , testProperty "Generates valid (>) code for NaNs" $+ mkRegressionTest2 (Gt Double) (zipWith (>)) vals+ , testProperty "Generates valid (>=) code for NaNs" $+ mkRegressionTest2 (Ge Double) (zipWith (>=)) vals+ ]+ where+ vals :: [(Double, Double)]+ vals = [(0, nan), (nan, 0)]++-- | Test the behavior of a unary operation (an @'Op1' a b@ value) against its+-- expected behavior (as a Haskell function of type @[a] -> [b]@) using the+-- supplied inputs (of type @[a]@). This function is intended to be used to+-- construct regression tests.+mkRegressionTest1 :: (Typed a, Typed b,+ DisplayableInBluespec b, ReadableFromBluespec b, AEq b)+ => Op1 a b+ -> ([a] -> [b])+ -> [a]+ -> Property+mkRegressionTest1 op haskellFun vals =+ let spec = alwaysTriggerArg1 (UExpr t2 appliedOp)+ appliedOp = Op1 op (ExternVar t1 varName Nothing)++ len = length vals+ inputs = filterOutUnusedExts+ spec+ [ (typeBluespec t1,+ fmap (bluespecShow t1) vals,+ varName)+ ]+ outputs = haskellFun vals in++ once $+ testRunCompareArg+ inputs len outputs spec (typeBluespec t2)++ where++ t1 = typeOf+ t2 = typeOf++ varName = "input"++-- | Test the behavior of a binary operation (an @'Op2' a b c@ value) against+-- its expected behavior (as a Haskell function of type @[a] -> [b] -> [c]@)+-- using the supplied inputs (of type @[(a, b)]@). This function is intended to+-- be used to construct regression tests.+mkRegressionTest2 :: (Typed a, Typed b, Typed c,+ DisplayableInBluespec c, ReadableFromBluespec c, AEq c)+ => Op2 a b c+ -> ([a] -> [b] -> [c])+ -> [(a, b)]+ -> Property+mkRegressionTest2 op haskellFun vals =+ let spec = alwaysTriggerArg1 (UExpr t3 appliedOp)+ appliedOp = Op2 op (ExternVar t1 varName1 Nothing)+ (ExternVar t2 varName2 Nothing)++ len = length vals+ (vals1, vals2) = unzip vals+ inputs = filterOutUnusedExts+ spec+ [ (typeBluespec t1,+ fmap (bluespecShow t1) vals1,+ varName1)+ , (typeBluespec t2,+ fmap (bluespecShow t2) vals2,+ varName2)+ ]+ outputs = haskellFun vals1 vals2 in++ once $+ testRunCompareArg+ inputs len outputs spec (typeBluespec t3)++ where++ t1 = typeOf+ t2 = typeOf+ t3 = typeOf++ varName1 = "input1"+ varName2 = "input2"+ -- * Random generators -- ** Random function generators@@ -277,6 +404,20 @@ , (Op1 (GetField typeOf typeOf myStruct2), fmap (unField . myStruct2)) ] +-- | Generator of functions that take and produce structs, where the returned+-- structs have one field value updated.+arbitraryStructUpdate :: Gen ( Fun2 MyStruct Int8 MyStruct+ , [MyStruct] -> [Int8] -> [MyStruct]+ )+arbitraryStructUpdate = elements+ [ ( Op2 (UpdateField typeOf typeOf myStruct1)+ , zipWith (\s i -> s { myStruct1 = Field i })+ )+ , ( Op2 (UpdateField typeOf typeOf myStruct2)+ , zipWith (\s i -> s { myStruct2 = Field i })+ )+ ]+ -- | Generator of functions on Floating point numbers. arbitraryOpFloat :: (Floating t, Typed t) => Gen (Fun t t, [t] -> [t]) arbitraryOpFloat = elements@@ -406,6 +547,19 @@ arbitraryStruct ] +-- | Generator for test cases that take and produce structs, where the returned+-- structs have one field value updated.+arbitraryOp2Struct :: Gen (TestCase2 MyStruct Int8 MyStruct)+arbitraryOp2Struct = oneof+ [ mkTestCase2+ arbitraryStructUpdate+ arbitraryStruct+ gen+ ]+ where+ gen :: Gen Int8+ gen = chooseBoundedIntegral (minBound, maxBound)+ -- * Semantics -- ** Functions@@ -549,7 +703,9 @@ varName2 = "input2" -- | Test running a compiled Bluespec program and comparing the results.-testRunCompare1 :: (Show a, Typed a, ReadableFromBluespec b, Eq b, Typed b)+testRunCompare1 :: (Show a, Typed a,+ DisplayableInBluespec b, ReadableFromBluespec b,+ AEq b, Typed b) => Gen (TestCase1 a b) -> Property testRunCompare1 ops = forAllBlind ops $ \testCase ->@@ -563,22 +719,23 @@ in forAll (getPositive <$> arbitrary) $ \len -> - forAll (vectorOf len gen) $ \nums -> do+ forAll (vectorOf len gen) $ \vals -> do let inputs = filterOutUnusedExts copilotSpec [ (typeBluespec bluespecTypeInput,- fmap (bluespecShow bluespecTypeInput) nums,+ fmap (bluespecShow bluespecTypeInput) vals, bluespecInputName) ]- outputs = haskellFun nums+ outputs = haskellFun vals 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)+ DisplayableInBluespec b, ReadableFromBluespec b,+ AEq b, Typed b) => Gen (TestCase2 a1 a2 b) -> Property testRunCompare2 ops = forAllBlind ops $ \testCase ->@@ -595,18 +752,18 @@ (bluespecTypeInput2, bluespecInputName2, gen2) = inputVar2 in forAll (getPositive <$> arbitrary) $ \len ->- forAll (vectorOf len gen1) $ \nums1 ->- forAll (vectorOf len gen2) $ \nums2 -> do+ forAll (vectorOf len gen1) $ \vals1 ->+ forAll (vectorOf len gen2) $ \vals2 -> do let inputs = filterOutUnusedExts copilotSpec [ (typeBluespec bluespecTypeInput1,- fmap (bluespecShow bluespecTypeInput1) nums1,+ fmap (bluespecShow bluespecTypeInput1) vals1, bluespecInputName1) , (typeBluespec bluespecTypeInput2,- fmap (bluespecShow bluespecTypeInput2) nums2,+ fmap (bluespecShow bluespecTypeInput2) vals2, bluespecInputName2) ]- outputs = haskellFun nums1 nums2+ outputs = haskellFun vals1 vals2 testRunCompareArg inputs len outputs copilotSpec (typeBluespec outputType)@@ -620,14 +777,15 @@ -- -- 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)+testRunCompareArg :: forall b+ . (DisplayableInBluespec b, ReadableFromBluespec b, AEq b) => [(String, [String], String)] -> Int -> [b] -> Spec -> String -> Property-testRunCompareArg inputs numInputs nums spec outputType =+testRunCompareArg inputs numInputs vals spec outputType = ioProperty $ do tmpDir <- getTemporaryDirectory setCurrentDirectory tmpDir@@ -638,7 +796,7 @@ -- Produce wrapper program let bluespecProgram =- testRunCompareArgBluespecProgram inputs outputType+ testRunCompareArgBluespecProgram (Proxy :: Proxy b) inputs outputType writeFile "Top.bs" bluespecProgram -- Produce copilot monitoring code@@ -654,10 +812,14 @@ print testDir -} - -- Run program and compare result+ -- Run the program and compare the results. Note that we use (===) (using+ -- the `AEq` class from the `ieee754` package) rather than (==) (using the+ -- `Eq` class), as the former allows us to use exact equality comparisons+ -- for floating-point types. This lets us ensure that we are handling NaN+ -- and -0.0 values correctly. out <- readProcess "./mkTop" ["-m", show (numInputs + 2)] "" let outNums = readFromBluespec <$> lines out- comparison = outNums == nums+ comparison = outNums === vals -- Only clean up if the test succeeded; otherwise, we want to inspect it. when comparison $ do@@ -671,10 +833,12 @@ -- updating external stream registers on every cycle, running the monitors, and -- publishing the results of any outputs. testRunCompareArgBluespecProgram- :: [(String, [String], String)]+ :: DisplayableInBluespec b+ => Proxy b+ -> [(String, [String], String)] -> String -> String-testRunCompareArgBluespecProgram inputs outputType = unlines $+testRunCompareArgBluespecProgram proxy inputs outputType = unlines $ [ "package Top where" , "" , "import FloatingPoint"@@ -696,8 +860,8 @@ , " ready :: Reg Bool <- mkReg False" , " interface" , " printBack :: " ++ outputType ++ " -> Action"- , " printBack num = $display (fshow num)"- , " when ready"+ , " printBack output = $display " ++ printBackDisplayArgs+ , " when ready" , "" ] ++ inputMethods ++@@ -713,6 +877,9 @@ , "mkTop = mkCopilotTest copilotTestIfc" ] where+ printBackDisplayArgs :: String+ printBackDisplayArgs = unwords (displayInBluespec proxy "output")+ inputVecDecls :: [String] inputVecDecls = concatMap@@ -873,8 +1040,8 @@ 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 Float x = bluespecShowRealFloat 32 castFloatToWord32 x+bluespecShow Double x = bluespecShowRealFloat 64 castDoubleToWord64 x bluespecShow (Array tE) x = genVector $ map (bluespecShow tE) $ arrayElems x bluespecShow (Struct s) x = typeName s@@ -901,12 +1068,42 @@ -- 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+-- | Show a value of a floating-point type (e.g., 'Float' or 'Double'). We make+-- sure to convert NaN and infinity values to the corresponding Bluespec+-- @FloatingPoint@ functions that construct these values.+bluespecShowRealFloat ::+ (Num float, Ord float, RealFloat float, Show float, Show word)+ => Int+ -> (float -> word)+ -> float+ -> String+bluespecShowRealFloat floatSizeInBits castFloatToWord float+ -- We want to ensure that NaN values are correctly translated to Bluespec,+ -- bit by bit. We have two mechanisms to do so. On the Haskell side, we have+ -- `ieee754`'s `nanWithPayload` function, and on the Bluespec side, we have+ -- `FloatingPoint`'s `nanQuiet` function. Unfortunately, their arguments are+ -- of different types, and it isn't quite clear how to express one function+ -- in terms of the other.+ --+ -- To avoid this problem, we take a more indirect approach: we first cast+ -- the Haskell floating-point value to a word and then `unpack` the word to+ -- a floating-point value on the Bluespec side. It's somewhat verbose, but+ -- it gets the job done reliably.+ | isNaN float+ = "unpack (" ++ show (castFloatToWord float) +++ " :: Bit " ++ show floatSizeInBits ++ ")" + | isInfinite float+ = "infinity " ++ show floatIsNeg++ | floatIsNeg+ = "negate " ++ show (abs float)++ | otherwise+ = show float+ where+ floatIsNeg = (float < 0) || isNegativeZero float+ -- | 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)\"@.@@ -919,6 +1116,69 @@ (0 :: Int, "newVector") vals +-- | Display a value of a given type in Bluespec using @$display@.+class DisplayableInBluespec a where+ displayInBluespec ::+ proxy a -- ^ The type of the value.+ -> String -- ^ The name of the Bluespec variable.+ -> [String] -- ^ All arguments that are passed to @$display@.++-- | Most Bluespec types can be displayed using @fshow@.+fshowDisplay :: proxy a -> String -> [String]+fshowDisplay _ output = ["(fshow " ++ output ++ ")"]++-- | We display floating-point numbers by converting them to an integer and+-- printing them in hexadecimal (using the @%x@ modifier). This somewhat unusual+-- choice is motivated by the fact that this output is easier to parse than the+-- @fshow@ output.+hexFloatDisplay :: proxy a -> String -> [String]+hexFloatDisplay _ output = ["\"%x\"", output]++instance DisplayableInBluespec Bool where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Int8 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Int16 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Int32 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Int64 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Word8 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Word16 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Word32 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Word64 where+ displayInBluespec = fshowDisplay++instance DisplayableInBluespec Float where+ displayInBluespec = hexFloatDisplay++instance DisplayableInBluespec Double where+ displayInBluespec = hexFloatDisplay++-- | @copilot-bluespec@–generated structs currently do not have @FShow@+-- instances. (Perhaps they should: see+-- https://github.com/Copilot-Language/copilot-bluespec/issues/12)+-- In lieu of this, we manually define the same code that would be used in a+-- derived @FShow@ instance.+instance DisplayableInBluespec MyStruct where+ displayInBluespec _ output =+ [ "\"MyStruct { myStruct1 = %d ; myStruct2 = %d }\""+ , output ++ ".myStruct1"+ , output ++ ".myStruct2"+ ]+ -- | Read a value of a given type in Bluespec. class ReadableFromBluespec a where readFromBluespec :: String -> a@@ -950,12 +1210,59 @@ instance ReadableFromBluespec Word64 where readFromBluespec = read +-- We print out floating-point values in hexadecimal (see `hexFloatDisplay`+-- above), so we parse them accordingly here.++instance ReadableFromBluespec Float where+ readFromBluespec s = castWord32ToFloat $ read $ "0x" ++ s++instance ReadableFromBluespec Double where+ readFromBluespec s = castWord64ToDouble $ read $ "0x" ++ s++instance ReadableFromBluespec MyStruct where+ readFromBluespec str =+ case readsEither (readsStruct minPrec) str of+ Left err -> error err+ Right ms -> ms++-- | Attempt to read a value of type @a@. If successful, return 'Right' with+-- the read value. Otherwise, return @'Left' err@, where @err@ is an error+-- message describing what went wrong.+readsEither :: ReadS a -> String -> Either String a+readsEither readIt s =+ case [ x | (x,"") <- readIt s ] of+ [x] -> Right x+ [] -> Left $ "readsEither: no parse: " ++ s+ _ -> Left $ "readsEither: ambiguous parse: " ++ s+ -- ** A simple struct definition for unit testing purposes data MyStruct = MyStruct { myStruct1 :: Field "myStruct1" Int8 , myStruct2 :: Field "myStruct2" Int8 }++-- | Like a derived @Eq@ instance, except that this looks through 'Field's.+instance Eq MyStruct where+ MyStruct (Field f1a) (Field f2a) == MyStruct (Field f1b) (Field f2b) =+ f1a == f1b && f2a == f2b+instance AEq MyStruct++-- | Like a derived @Read@ instance, except that this adds 'Field' wrappers as+-- needed.+readsStruct :: Int -> ReadS MyStruct+readsStruct p = readParen (p > 10) $ \s -> do+ ("MyStruct", s1) <- lex s+ ("{", s2) <- lex s1+ ("myStruct1", s3) <- lex s2+ ("=", s4) <- lex s3+ (f1, s5) <- readsPrec 0 s4+ (";", s6) <- lex s5+ ("myStruct2", s7) <- lex s6+ ("=", s8) <- lex s7+ (f2, s9) <- readsPrec 0 s8+ ("}", s10) <- lex s9+ pure (MyStruct (Field f1) (Field f2), s10) instance Struct MyStruct where typeName _ = "MyStruct"