Add checked versions of 'resize', 'truncateB', and 'fromIntegral'

Depending on the type 'resize', 'truncateB', and 'fromIntegral' either
yield an XException or silently perform wrap-around if its argument does
not fit in the resulting type's bounds. The added functions check the
bound condition and fail with an error call if the condition is
violated. They do not affect HDL generation.

Useful in cases where runtime behavior should ensure that and out of
bound or wrap around should not occur and users want their code to fail
hard if this invariant is ever violated.

changelog/2020-08-27T16_45_36+02_00_added_checked_functions

@@ -0,0 +1,11 @@
+ADDED: Checked versions of 'resize', 'truncateB', and 'fromIntegral'
+
+Depending on the type 'resize', 'truncateB', and 'fromIntegral' either
+yield an XException or silently perform wrap-around if its argument does
+not fit in the resulting type's bounds. The added functions check the
+bound condition and fail with an error call if the condition is
+violated. They do not affect HDL generation.
+
+Useful in cases where runtime behavior should ensure that and out of
+bound or wrap around should not occur and users want their code to fail
+hard if this invariant is ever violated.

clash-prelude/clash-prelude.cabal

@@ -382,6 +382,7 @@ test-suite unittests
       ghc-typelits-knownnat,
 
       base,
+      deepseq,
       hint          >= 0.7      && < 0.10,
       quickcheck-classes-base >= 0.6 && < 1.0,
       tasty         >= 1.2      && < 1.4,
@@ -399,6 +400,7 @@ test-suite unittests
                  Clash.Tests.Signed
                  Clash.Tests.SizedNum
                  Clash.Tests.NFDataX
+                 Clash.Tests.Resize
                  Clash.Tests.TopEntityGeneration
                  Clash.Tests.Unsigned
 

clash-prelude/src/Clash/Class/Resize.hs

@@ -1,17 +1,27 @@
 {-|
 Copyright  :  (C) 2013-2016, University of Twente
+                  2020,      Myrtle Software Ltd
 License    :  BSD2 (see the file LICENSE)
-Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
+Maintainer :  QBayLogic B.V. <devops@qbaylogic.com>
 -}
 
 {-# LANGUAGE Safe #-}
 
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 
-module Clash.Class.Resize where
+module Clash.Class.Resize
+ ( Resize(..)
+
+ -- * Resize helpers
+ , checkedResize
+ , checkedFromIntegral
+ , checkedTruncateB
+ ) where
 
 import Data.Kind (Type)
+import Data.Proxy (Proxy(Proxy))
+import GHC.Stack (HasCallStack)
 import GHC.TypeLits (Nat, KnownNat, type (+))
 
 -- | Coerce a value to be represented by a different number of bits
@@ -37,3 +47,65 @@ class Resize (f :: Nat -> Type) where
   signExtend = resize
   -- | Remove bits from the MSB
   truncateB :: KnownNat a => f (a + b) -> f a
+
+-- | Helper function of 'fromIntegralChecked' and 'resizeChecked'
+checkIntegral ::
+  forall a b.
+  HasCallStack =>
+  (Integral a, Integral b, Bounded b) =>
+  Proxy b ->
+  a -> ()
+checkIntegral Proxy a =
+  if toInteger a > toInteger (maxBound @b)
+  || toInteger a < toInteger (minBound @b) then
+    error $ "Given integral " <> show (toInteger a) <> " is out of bounds for" <>
+            " target type. Bounds of target type are: [" <>
+            show (toInteger (minBound @b)) <> ".." <>
+            show (toInteger (maxBound @b)) <> "]."
+  else
+    ()
+
+-- | Like 'fromIntegral', but errors if /a/ is out of bounds for /b/. Useful when
+-- you "know" /a/ can't be out of bounds, but would like to have your assumptions
+-- checked.
+--
+-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted
+-- into the generated HDL
+checkedFromIntegral::
+  forall a b.
+  HasCallStack =>
+  (Integral a, Integral b, Bounded b) =>
+  a -> b
+checkedFromIntegral a =
+  checkIntegral (Proxy @b) a `seq` fromIntegral a
+
+-- | Like 'resize', but errors if /f a/ is out of bounds for /f b/. Useful when
+-- you "know" /f a/ can't be out of bounds, but would like to have your
+-- assumptions checked.
+--
+-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted
+-- into the generated HDL
+checkedResize ::
+  forall a b f.
+  ( HasCallStack
+  , Resize f
+  , KnownNat a, Integral (f a)
+  , KnownNat b, Integral (f b), Bounded (f b) ) =>
+  f a -> f b
+checkedResize a =
+  checkIntegral (Proxy @(f b)) a `seq` resize a
+
+-- | Like 'truncateB', but errors if /f (a + b)/ is out of bounds for /f a/. Useful
+-- when you "know" /f (a + b)/ can't be out of bounds, but would like to have your
+-- assumptions checked.
+--
+-- __N.B.__: Check only affects simulation. I.e., no checks will be inserted
+-- into the generated HDL
+checkedTruncateB ::
+  forall a b f.
+  ( HasCallStack
+  , Resize f
+  , KnownNat b, Integral (f (a + b))
+  , KnownNat a, Integral (f a), Bounded (f a) ) =>
+  f (a + b) -> f a
+checkedTruncateB = checkedResize

clash-prelude/tests/Clash/Tests/Resize.hs

@@ -0,0 +1,53 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Clash.Tests.Resize (tests) where
+
+import Control.DeepSeq (NFData)
+import Control.Exception (SomeException, try, evaluate)
+import Clash.XException (XException)
+import Data.Either (isLeft)
+import Data.Proxy (Proxy(Proxy))
+import GHC.TypeNats (KnownNat, type (<=))
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.QuickCheck
+
+import qualified Clash.Class.Resize as Resize
+import Clash.Sized.Index
+
+-- | Anything that's in bounds should not cause an error
+indexProp ::
+  forall a b.
+  ((a <= b), KnownNat a, KnownNat b) =>
+  Proxy b -> Index a -> Bool
+indexProp Proxy a =
+  Resize.resize a == Resize.checkedResize @a @b a
+
+-- | Anything that's out of bounds should cause an error
+indexFailProp ::
+  forall a b.
+  ((b <= a), KnownNat a, KnownNat b) =>
+  Proxy b -> Index a -> Property
+indexFailProp Proxy a =
+  let checked = Resize.checkedResize @a @b a in
+  if toInteger a > toInteger (maxBound @(Index b)) then
+    expectExceptionNoX checked
+  else
+    discard
+
+-- | Succeed if evaluating leads to a non-XException Exception
+expectExceptionNoX :: (Show a, NFData a) => a -> Property
+expectExceptionNoX a0 = ioProperty $ do
+  a1 <- try @SomeException (try @XException (evaluate a0))
+  pure $
+    counterexample
+      ("Expected non-XException Exception, got: " <> show a1)
+      (isLeft a1)
+
+tests :: TestTree
+tests = testGroup "Resize"
+  [ testGroup "checkedResize"
+    [ testProperty "indexProp @17 @19" (indexProp @17 @19 Proxy)
+    , testProperty "indexProp @19 @19" (indexProp @19 @19 Proxy)
+    , testProperty "indexFailProp @37 @7" (indexFailProp @37 @7 Proxy)
+    ]
+  ]

clash-prelude/tests/unittests.hs

@@ -9,6 +9,7 @@ import qualified Clash.Tests.DerivingDataRepr
 import qualified Clash.Tests.Signal
 import qualified Clash.Tests.Signed
 import qualified Clash.Tests.NFDataX
+import qualified Clash.Tests.Resize
 import qualified Clash.Tests.TopEntityGeneration
 import qualified Clash.Tests.Unsigned
 
@@ -23,6 +24,7 @@ tests = testGroup "Unittests"
   , Clash.Tests.NFDataX.tests
   , Clash.Tests.TopEntityGeneration.tests
   , Clash.Tests.Unsigned.tests
+  , Clash.Tests.Resize.tests
   ]
 
 main :: IO ()