Improve BitPack instances with undefined bits

[basile-henry]

Now that BitVectors contain a bitmask for which bits are defined, we should be able to improve some of the BitPack instances (mainly Vec).

For example, we could expect these two values to pack the same way:

Clash.Prelude> pack (Nothing :: Maybe Bit)
0.
Clash.Prelude> pack (0 :> undefined :> Nil :: Vec 2 Bit)
*** Exception: X: undefined
CallStack (from HasCallStack):
  errorX, called at <interactive>:5:12 in interactive:Ghci1

Which would allow us to do things like:

Clash.Prelude> bitCoerce (0 :> 1 :> Nil :: Vec 2 Bit) :: Maybe Bit
Nothing
Clash.Prelude> bitCoerce (0 :> undefined :> Nil :: Vec 2 Bit) :: Maybe Bit
*** Exception: X: undefined

Similarly we could get expressions like bv2v . v2bv to be closer to id even in the presence of undefined bits:

Clash.Prelude> head $ id (1 :> undefined :> Nil :: Vec 2 Bit)
1
Clash.Prelude> head $ (bv2v . v2bv) (1 :> undefined :> Nil :: Vec 2 Bit)
*** Exception: X: undefined
CallStack (from HasCallStack):
  errorX, called at src/Clash/Explicit/Prelude/Safe.hs:237:13 in clash-prelude-0.99-5tD8YyKlskCDMkI1EAcLIV:Clash.Explicit.Prelude.Safe
  undefined, called at <interactive>:15:28 in interactive:Ghci2

@christiaanb suggested to change the following:

clash-compiler/clash-prelude/src/Clash/Sized/Internal/BitVector.hs

Lines 323 to 324 in 1d02f8f

	pack# :: Bit -> BitVector 1
	pack# (Bit m b) = BV m b

To:

pack# :: Bit -> BitVector 1
pack# b = case maybeX b of
  Just (Bit m b) -> BV m b
  Nothing -> undefined#

One thing to note here, even if we manage to fix bv2v . v2bv == id, we wouldn't be able to recover the msg from a errorX msg through that expression. The errors would be represented as single bits, so all error messages would be "forgotten".

[martijnbastiaan]

The errors would be represented as single bits, so all error messages would be "forgotten".

I think this touches on a deeper issue; undefined bits are generally not going to survive a pack/unpack cycle. Consider the following definitions (never mind the probably wrong syntax :-)):

x1 = undefined# :> pack 8  :: BitVector 17
x2 = unpack x1             :: Either Int16 Int16
x3 = tail (pack x2)        :: BitVector 16

There's no way we can solve this correctly, even though Verilog and the hardware itself would conclude that x3 ~ 8, of course.

Considering that we'd be throwing away error messages and that undefinedness is couter-intuitive and fundamentally broken in Verilog (and my guess is all other HDLs too) anyway I think we'd be best of by introducing an unsafeUnpack. unsafeUnpack would simply do nothing in HDLs and hardware, but would - conceptually - insert random bits (or zeroes, or ones, or..). This is actually how some simulators do it right now, most notably Verilator.

[martijnbastiaan]

Actually, @leonschoorl kind of defeated by unsafeUnpack idea by proposing to pack/unpack an Either Int8 Int16, which would introduce undefined bits in x3 again. So I'm back at square one..

[jonfowler]

@martijnbastiaan, @cchalmers pointed out that the problem is actually:

> pack (undefined :: Int)
*** Exception: X: undefined
CallStack (from HasCallStack):
  errorX, called at src/Clash/Explicit/Prelude/Safe.hs:237:13 in clash-prelude-0.99-2D1T7X7iz93E7KJQ0JeVWa:Clash.Explicit.Prelude.Safe
  undefined, called at <interactive>:6:7 in interactive:Ghci1

Rather then:

> pack (undefined :: Int)
...._...._...._...._...._...._...._...._...._...._...._...._...._...._...._....

The solution to this is to test whether a value is errorX and pack this to undefined#. I.e. we could change the BitPack type class to:

class BitPack a where
  type BitSize a :: Nat

  pack :: a -> BitVector (BitSize a)
  pack a = case catchX a of
    Left _ -> undefined#
    Right _ -> packInternal a

  packInternal :: a -> BitVector (BitSize a)

  unpack :: BitVector (BitSize a) -> a

-- | catchX is the same a ifX but only evaluates to w.h.n.f
catchX :: a -> Either String a
catchX a = unsafeDupablePerformIO
  (catch (evaluate (evaluate a `seq` return (Right a)))  (\(XException msg) -> return (Left msg)))
{-# NOINLINE catchX #-}

-- | FYI isX could be written in terms of catchX
isX a = catchX (force a)

Where the current definitions for pack are used for packInternal. e.g.

instance BitPack Int where
  type BitSize Int = WORD_SIZE_IN_BITS
  packInternal   = fromIntegral
  unpack = checkUnpackUndef fromIntegral

[christiaanb]

It’ll be difficult to generate HDL for that definition. We currently do not even handle isX and friends: https://github.com/clash-lang/clash-compiler/blob/master/clash-lib/prims/common/Clash_XException.json

[jonfowler]

@christiaanb, how about:

catchX :: a -> a -> a
catchX a b = unsafeDupablePerformIO
  (catch (evaluate a)  (\(XException _) -> b))
{-# NOINLINE catchX #-}

With pack a = catchX (packInternal a) undefined#. The hdl for catchX can just be the same as const.

[jonfowler]

Obviously, this should be an Internal function as this would be pretty much the only reasonable use of this function in a circuit (and it's existence is only to make the Haskell simulation match normal simulation). I don't whether adding a primitive here could affect optimisations as well (although it seems unlikely)?

[christiaanb]

Fixed by #552