`Couldn't instantiate blackbox for Clash.Sized.Vector.replicate.` unless manually marked for inlining #1454

gergoerdi · 2020-07-15T15:03:58Z

This was quite challenging to minimize into a standalone program, but here it is. It requires splitting into two modules to demonstrate the problem.

`BCD.hs`

{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
module BCD where

import Clash.Prelude hiding (shift, add)

bitwise :: (BitPack a) => (BitVector (BitSize a) -> BitVector (BitSize a)) -> (a -> a)
bitwise f = unpack . f . pack

type BCDSize n = CLog 10 (2 ^ n)
type ShiftAdd n = (Vec (BCDSize n) (Unsigned 4), Unsigned n)

initBCD :: (KnownNat n) => Unsigned n -> ShiftAdd n
initBCD = shift . (,) (repeat 0)

stepBCD :: (KnownNat n) => ShiftAdd n -> ShiftAdd n
stepBCD = shift . add

shift :: (KnownNat n) => ShiftAdd n -> ShiftAdd n
shift = bitwise (`shiftL` 1)

add :: ShiftAdd n -> ShiftAdd n
add (digits, buf) = (map add3 digits, buf)
  where
    add3 d = if d >= 5 then d + 3 else d

toBCD :: forall n. (KnownNat n, 1 <= n) => Unsigned n -> Vec (BCDSize n) (Unsigned 4)
toBCD = leToPlus @1 @n $ fst . last . iterate (SNat @n) stepBCD . initBCD

`Top.hs`

module Top where

import Clash.Prelude hiding (shift, add)
import Clash.Annotations.TH
import BCD

topEntity
    :: "CLK_25MHZ" ::: Clock System
    -> "RESET"     ::: Reset System
    -> "INPUT"     ::: Signal System (Unsigned 8)
    -> "OUTPUT"    ::: Signal System (Vec 3 (Unsigned 4))
topEntity clk rst = withClockResetEnable clk rst enableGen board
  where
    board inp = toBCD <$> inp

makeTopEntity 'topEntity

As is, this when compiling to Verilog, with the following error message:

Clash.Netlist.BlackBox(188): Couldn't instantiate blackbox for Clash.Sized.Vector.replicate. Verification procedure reported:

Argument 0 should be literal, as blackbox used ~LIT[0], but was:
DataCon (Unsigned 64) (DC (Void Nothing,-1)) [Identifier "result" Nothing]
The source location of the error is not exact, only indicative, as it is acquired
after optimizations. The actual location of the error can be in a function that is
inlined. To prevent inlining of those functions, annotate them with a NOINLINE pragma.
   |
12 | topEntity clk rst = withClockResetEnable clk rst enableGen board
   | ^^^^^^^^^

What I have found is that I can work around this problem by manually adding an INLINE pragma to initBCD and toBCD. This set seems to be minimal, as in adding INLINE to just any one of them doesn't fix the problem.

The text was updated successfully, but these errors were encountered:

christiaanb · 2020-07-16T10:59:58Z

Something has gone horribly wrong at the GHC side. I'm seeing this in -ddump-simpl:

Test.$sinitBCD_g
  = replicate
      @ (CLog 10 (2 ^ 8))
      @ (Unsigned 4)
      (Clash.Promoted.Nat.SNat
         @ (CLog 10 (2 ^ 8))
         (case BCD.initBCD2 of {
            GHC.Natural.NatS# a1_ap0t ->
              Test.$s$w$cnatSing2
              `cast` (GHC.TypeLits.KnownNat.N:SNatKn[0]
                          <"GHC.TypeLits.Extra.CLog">_P ; (Sym (GHC.TypeNats.N:SNat[0]
                                                                    <CLog
                                                                       10
                                                                       (2
                                                                        ^ 8)>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <CLog
                                                                                                                       10
                                                                                                                       (2
                                                                                                                        ^ 8)>_N)
                      :: GHC.TypeLits.KnownNat.SNatKn "GHC.TypeLits.Extra.CLog"
                         ~R# KnownNat (CLog 10 (2 ^ 8)));
            GHC.Natural.NatJ# dt_apaH ->
              case {__pkg_ccall integer-gmp-1.0.2.0 ByteArray#
                                 -> ByteArray#
                                 -> Int#
                                 -> State# RealWorld
                                 -> (# State# RealWorld, Int# #)}_apaT
                     dt_apaH
                     dt_apaH
                     (GHC.Prim.uncheckedIShiftRL#
                        (GHC.Prim.sizeofByteArray# dt_apaH) 3#)
                     GHC.Prim.realWorld#
              of
              { (# ds2_apaW, ds3_apaX #) ->
              Test.$s$w$cnatSing2
              `cast` (GHC.TypeLits.KnownNat.N:SNatKn[0]
                          <"GHC.TypeLits.Extra.CLog">_P ; (Sym (GHC.TypeNats.N:SNat[0]
                                                                    <CLog
                                                                       10
                                                                       (2
                                                                        ^ 8)>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <CLog
                                                                                                                       10
                                                                                                                       (2
                                                                                                                        ^ 8)>_N)
                      :: GHC.TypeLits.KnownNat.SNatKn "GHC.TypeLits.Extra.CLog"
                         ~R# KnownNat (CLog 10 (2 ^ 8)))
              }
          }))
      (Clash.Sized.Internal.Unsigned.fromInteger#
         @ 4
         (BCD.add1
          `cast` (Sym (GHC.TypeNats.N:SNat[0]
                           <4>_P) ; Sym (GHC.TypeNats.N:KnownNat[0]) <4>_N
                  :: GHC.Natural.Natural ~R# KnownNat 4))
         0)

The important bit there is Test.$s$w$cnatSing2 which is supposed to be a Natural with the value CLog 10 (2 ^ 8)

However, when I look it up I see:

Test.$s$w$cnatSing2
  = case GHC.Integer.Logarithms.integerLogBase#
           Test.$s$w$cnatSing2_x1 Test.$s$w$cnatSing2_y1
    of z1_aqy6
    { __DEFAULT ->
    case GHC.Integer.Logarithms.integerLogBase#
           Test.$s$w$cnatSing2_x1
           (integer-gmp-1.0.2.0:GHC.Integer.Type.minusInteger
              Test.$s$w$cnatSing2_y1
              GHC.TypeLits.Extra.$fKnownNat2"GHC.TypeLits.Extra.CLog"xy2)
    of z2_aqy8
    { __DEFAULT ->
    case integer-gmp-1.0.2.0:GHC.Integer.Type.eqInteger#
           Test.$s$w$cnatSing2_y1
           GHC.TypeLits.Extra.$fKnownNat2"GHC.TypeLits.Extra.CLog"xy2
    of {
      __DEFAULT ->
        case GHC.Prim.==# z1_aqy6 z2_aqy8 of {
          __DEFAULT ->
            (GHC.Natural.NatS# (GHC.Prim.int2Word# z1_aqy6))
            `cast` (Sym (GHC.TypeLits.KnownNat.N:SNatKn[0]
                             <"GHC.TypeLits.Extra.CLog">_P)
                    :: GHC.Natural.Natural
                       ~R# GHC.TypeLits.KnownNat.SNatKn "GHC.TypeLits.Extra.CLog");
          1# ->
            (GHC.Natural.NatS# (GHC.Prim.int2Word# (GHC.Prim.+# z1_aqy6 1#)))
            `cast` (Sym (GHC.TypeLits.KnownNat.N:SNatKn[0]
                             <"GHC.TypeLits.Extra.CLog">_P)
                    :: GHC.Natural.Natural
                       ~R# GHC.TypeLits.KnownNat.SNatKn "GHC.TypeLits.Extra.CLog")
        };
      1# ->
        GHC.TypeLits.Extra.$fKnownNat2"GHC.TypeLits.Extra.CLog"xy1
        `cast` (Sym (GHC.TypeLits.KnownNat.N:SNatKn[0]
                         <"GHC.TypeLits.Extra.CLog">_P)
                :: GHC.Natural.Natural
                   ~R# GHC.TypeLits.KnownNat.SNatKn "GHC.TypeLits.Extra.CLog")
    }
    }
    }

again, the important part of that is:

case GHC.Integer.Logarithms.integerLogBase#
           Test.$s$w$cnatSing2_x1 Test.$s$w$cnatSing2_y1
    of z1_aqy6

where

Test.$s$w$cnatSing2_x1 = 10

but

Test.$s$w$cnatSing2_y1
  = GHC.Natural.naturalToInteger GHC.Natural.lcmNatural1

So Test.$s$w$cnatSing2 will not have the value CLog 10 (2 ^ 8), but CLog 10 GHC.Natural.lcmNatural1 !!! where the value of GHC.Natural.lcmNatural1 is 0.

christiaanb · 2020-07-16T11:06:20Z

When I add {-# OPTIONS_GHC -fno-specialize #-} to Test.hs, thus preventing cross-module specializations, it compiles. HORRIBLE!

christiaanb · 2020-07-16T11:46:18Z

My guess is that ghc-typelits-knownnat / ghc-typelits-extra is violating some invariant, and GHC has decided that the KnownNat (CLog 10 0) dictionary and KnownNat (CLog 2 (2 ^ 8)) dictionary are the same.

It might because we only tag the evidence with the (string representation of the) name of the operation ("CLog" in the above case):
https://github.com/clash-lang/ghc-typelits-knownnat/blob/88c8a28f1dc60322cb6f96122478387f8c425ed0/src/GHC/TypeLits/KnownNat.hs#L172

I'll see what happens if I tag the evidence with all the parameters.

For some bizarre reason, which I cannot reproduce, the set of optimizations that Clash picks results in a weird specialization of the `natSing2` implementation for `GHC.TypeNats.^`, which is specialized to the `y` in `x ^ y` being a negative number. This then causes the: > shiftL x y = if y <= 0 then shiftLNatural x y else shiftRNatural x (negate y) to pick the else branch, which in turn causes fast power-of-two calculation in `natSing2` to do `1 shiftR y` instead of the intended `1 shiftL y`. Anyhow... I don't know what's going on... This patch ensures we call `shiftLNatural` directly, since we know the exponent never a negative number; and GHC won't be able to specialize. Fixes clash-lang/clash-compiler#1454

christiaanb · 2020-07-25T11:38:09Z

@gergoerdi This will be fixed by clash-lang/ghc-typelits-knownnat#36

For some bizarre reason, which I cannot reproduce, the set of optimizations that Clash picks results in a weird specialization of the `natSing2` implementation for `GHC.TypeNats.^`, which is specialized to the `y` in `x ^ y` being a negative number. This then causes the: > shiftL x y = if y <= 0 then shiftLNatural x y else shiftRNatural x (negate y) to pick the else branch, which in turn causes fast power-of-two calculation in `natSing2` to do `1 shiftR y` instead of the intended `1 shiftL y`. Anyhow... I don't know what's going on... This patch ensures we call `shiftLNatural` directly, since we know the exponent never a negative number; and GHC won't be able to specialize. Fixes clash-lang/clash-compiler#1454

gergoerdi added a commit to gergoerdi/retroclash-lib that referenced this issue Jul 15, 2020

Workaround for clash-lang/clash-compiler#1454

9655288

christiaanb added the bug label Jul 16, 2020

christiaanb mentioned this issue Jul 25, 2020

Use shiftL(Natural/Integer) instead of Bits.shiftL clash-lang/ghc-typelits-knownnat#36

Merged

christiaanb closed this as completed in clash-lang/ghc-typelits-knownnat#36 Jul 25, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`Couldn't instantiate blackbox for Clash.Sized.Vector.replicate.` unless manually marked for inlining #1454

`Couldn't instantiate blackbox for Clash.Sized.Vector.replicate.` unless manually marked for inlining #1454

gergoerdi commented Jul 15, 2020

christiaanb commented Jul 16, 2020

christiaanb commented Jul 16, 2020

christiaanb commented Jul 16, 2020 •

edited

christiaanb commented Jul 25, 2020

Couldn't instantiate blackbox for Clash.Sized.Vector.replicate. unless manually marked for inlining #1454

Couldn't instantiate blackbox for Clash.Sized.Vector.replicate. unless manually marked for inlining #1454

Comments

gergoerdi commented Jul 15, 2020

BCD.hs

Top.hs

christiaanb commented Jul 16, 2020

christiaanb commented Jul 16, 2020

christiaanb commented Jul 16, 2020 • edited

christiaanb commented Jul 25, 2020

`Couldn't instantiate blackbox for Clash.Sized.Vector.replicate.` unless manually marked for inlining #1454

`Couldn't instantiate blackbox for Clash.Sized.Vector.replicate.` unless manually marked for inlining #1454

`BCD.hs`

`Top.hs`

christiaanb commented Jul 16, 2020 •

edited