SizeOf (in type of method with if-expression) remains after expanded (causing internal error)

Sorry I don't have a better understanding of the error to give this issue a better name.

Example code is here: https://github.com/rossc719g/bsc_examples/blob/main/internal_error_1/README.md

The code is not as small as I would like, but the example is lifted and boiled down from real code. The real code is significantly larger, but generates the same error message (with a few names changed).

I created a toy example, deleted all of the obviously extraneous code, and inlined a bunch of libraries that I use, so some of the code may look a tad silly. But I am not sure how to minimize it much further.

The error from the compiler is:

Internal Bluespec Compiler Error:
Please report this failure to the BSC developers, by opening a ticket
in the issue database: https://github.com/B-Lang-org/bsc/issues
The following internal error message should be included in your
correspondence along with any other relevant details:
Bluespec Compiler, version 2023.01 (build 52adafa)
chkADef mux_out :: ABSTRACT:  Prelude.Bit;
mux_out  = _if_ vMux_output_whas____d15 x__h1846 32'd0;
: (ADef {adef_objid = mux_out, adef_type = ATAbstract {ata_id = Prelude::Bit, ata_sizes = []}, adef_expr = APrim {ae_objid = Prelude::primIf, ae_type = ATBit {atb_size = 32}, aprim_prim = PrimIf, ae_args = [ASDef {ae_type = ATBit {atb_size = 1}, ae_objid = vMux_output_whas____d15[IdP_from_rhs]},ASDef {ae_type = ATBit {atb_size = 32}, ae_objid = x__h1846[IdP_keep]},ASInt {ae_objid = _, ae_type = ATBit {atb_size = 32}, ae_ival = 0}]}, adef_props = []}) ABSTRACT:  Prelude.Bit
 /= Bit 32

Happy to answer questions or run tests on my end if it does not repo for you.

This is small enough, thanks! I'll have a look at it.

I'm a bit unsure what Raw and Mux are doing for you. But I don't know if that's because it has been reduced too much. The comments mention Mux being used for better names -- if you're running into an issue there, it might be better to enhance BSC to give better names to things. Unfortunately, I don't use BH, so I don't know what's lacking there; for BSV, improvements were made over the years to improve output names. If BH is not up to the same level, I would love to have examples and work on improving them. Also, the BSV features are often implemented with underlying primitive functions, so you might be able to explicitly add these into your BH code as a workaround (until the BH parser implicitly supports it). A comment mentions _1 etc for Vectors, though, and I'd be surprised if that didn't work the same in BSV and BH. Anyway, if you wanted to provide an example, I'd be happy to look at it.

Similarly, I'm unsure what Raw is doing. Also, I don't know if you want comments on the code for it? For example, it looks like you may have added a Literal instance because BSC asked for it; BSC was only asking for it because you didn't provide an instance for DefaultValue, like this:

instance (Bits t tsz) => DefaultValue (Raw t) where
  defaultValue = Raw defaultValue

The DefaultValue class has a fall-through instance, so if no other instance is found then as a last resort it will try to use literal 0 to define it. You didn't provide an instance, so it resolve to the fall-through. FYI, this is the instance in the Prelude:

instance (Literal t) => DefaultValue t where
   defaultValue = fromInteger 0

Also, if you're going to define Raw as requiring Bits (which is what SizeOf does), then I don't think you need to define cook and uncook as members of a typeclass. Just define them like this:

cook :: (Bits t tsz) => Raw t -> t
cook (Raw x) = unpack x

uncook :: (Bits t tsz) => t -> Raw t
uncook x = Raw (pack x)

You would use a typeclass if you wanted to allow instances to be written for other types. But since you've defined Raw as being defined by Bits, there won't be other instances. Alternatively, you can keep the typeclass if you remove the Bits from Raw:

data Raw t sz = Raw (Bit sz)

Then the Cookable instance can specify what the raw size, regardless of the Bits size or even whether a Bits instance exists. You could even define it like this:

data Raw t = Raw t

and only pack the value in the places where packing is needed.

I guess it would depend on why you've defined this type. I don't think it would have any effect on generated code, so are you trying to add some safety into your design (by having BSC check that you're not mixing raw and unraw values, say)? Again, I'd be happy to help identify whether BSC needs a new feature to support what you're trying to do (or whether there's an existing better way to write this), if you wanted to explain more about what you're trying to do.

In any case, I'm able to reproduce the failure, and I'll have a look.

Here is a smaller example, which shows the ICE when compiled with bsc -verilog Test.bs:

package Test where

-- =========================

data Raw t = Raw (Bit (SizeOf t))
  deriving (Bits);

cook :: (Bits t tsz) => Raw t -> t
cook (Raw x) = unpack x

-- =========================

type T = Bit 4

interface Mux =
  mux :: T

{-# verilog mkTop #-}
mkTop :: Module Mux
mkTop = module
  output :: Reg (Raw T) <- mkDWire _
  interface Mux
    mux = cook output

-- =========================

The failure is reported after aConv (the ATS stage) when the sanity check (aCheck) is applied. The check fails because the method mux has a type that doesn't match the expression assigned to it. And this because the input to aConv still had SizeOf in the type of the method, even though uses of SizeOf should have been replaced with the actual size during elaboration (the expanded stage).

If we dump the output of the expanded stage, we see this:

-- imod interface
-- args
-- body
mux :: Prelude.Bit (Prelude.SizeOf (Prelude.Bit 4))
mux = PrimIf ?(Prelude.Bit (Prelude.SizeOf (Prelude.Bit 4))) __h95 _x__h101 _ ::  (Prelude.Bit 4)
...

We'll need to debug why SizeOf was not reduced away.

The mkDWire introduces an if-expression, which is key to triggering this bug. The following example makes the if-expression explicit and still has the error:

mkTop = module
  rg_c :: Reg Bool <- mkRegU
  output :: Reg (Raw T) <- mkRegU
  let x :: Raw T
      x = if rg_c then output else _

  interface Mux
    mux = cook x

Thanks! While you're digging, If you happen to stumble on a workaround I can use in the short term, I'd love to hear it it.

I'm intrigued that the mkDWire makes a difference. I had used a mkReg defaultValue in my debugging, and still had the error (or so I thought).

To answer some of your questions from above:

Re: `Raw` implementation.

You're absolutely right. I've removed the class and swapped the Literal instance for a DefaultValue instance both in my real code and in my examples. It is much cleaner, thanks!

Re: The reason `Raw` exists.

The goal of Raw (which does not really come up in the example I gave) comes up when there are large Vector types in the code. E.g., Vector 256 (Uint 4). All the implicit pack/unpacks that happen when reading/writing a register, or crossing module boundaries all add up quickly. Looking at the generated verilog, it feels like the compiler wants to break those large vectors apart, do some analysis on them, and then recombine them. It feels like some of the analysis it does might take exponential time. So, compile times go up a lot, and the generated verilog also becomes extremely verbose. With large complicated designs, it can be the difference between compiling cleanly, and running out of host memory (or user patience).

You can see a bit of this issue in my toy examples if you change T in MyMuxThing.bs to be a large vector. E.g., A Bit 1024 version produces 155 lines of Verilog pretty much instantly. But aVector 256 (Uint 4) produces 5015 lines, takes a noticeable amount of time, and generates warnings about function unfolding steps (unless I suppress them).

So, if I am using large vector types like this, and only need to inspect the contents of the vector in a small number of places, I can pass around a Raw (Vector bigNumber someType) instead, and then only cook it when I need to operate on its contents, and uncook any results generated before passing them around to other registers or modules.

I left the Raw in my examples because removing it made the error go away. (And now with your analysis, I see why!)

Re: The reason `Mux` exists.

This is all about verilog signal naming, and unfortunately, the examples I gave are not the best illustration. There are times when muxing a vector of inputs (like in the example I gave) is the correct thing, and the numbered inputs are just fine. But there are other times where I need to give each input of the mux a name beyond just _1, _2, _3.

I added an example called OptionsMux to illustrate. Hopefully it makes sense?

The reasoning here is that when the generated verilog is being synthesized, the names can be used to apply constraints to the registers/signals with certain names. If I just use vectors, then adding or removing one of the options would change all the names. Using a struct (interface actually) allows me to rely on the names long term.

P.S.

Since you mentioned naming.... I used to know a trick that I could use to add a name to an instantiated module, but I have since lost the memory of that trick. E.g., I could do something like this:

someReg :: UInt 4 <- addName "retimeMePlease" $ mkReg 0

And then addName function would just cause the word "retimeMePlease" to appear somewhere in the name of that register (I don't recall exactly where). And then in the physical design tools, I could tell it to retime (only) those registers to improve the timing of the resulting netlist.

Do you know the appropriate magic to implement a function like addName? I tried to find one, but got lost in prim* functions and such and gave up for now.

Thanks again!

A workaround is to not use SizeOf in the type of a data field:

data Raw t sz = Raw (Bit sz)

If you want to hide the size from users, you can name the data something else and make Raw be a type alias that inserts the bit size:

data RawT sz = Raw (Bit sz)
type Raw t = RawT t (SizeOf t)

The internal error goes away if normITAp (in ISyntax.hs) is updated to reduce SizeOf (Bit x) to x. For example:

normITAp (ITCon op _ _) (ITAp (ITCon c _ _) n) | op == idSizeOf && c == idBit = n

I will need to test if that breaks anything, though.

I notice that normITAp has an arm for SizeOf applied to something that isn't a variable:

normITAp f@(ITCon op _ _) a | op == idSizeOf && notVar a =
  -- trace ("normITAp: " ++ ppReadable (ITAp f a)) $
  ITAp f a

But this appears to be a no-op. It presumably exists just to insert a trace for situations when the SizeOf ought to be reduce-able. It could be worth turning this into an internal error and seeing if it ever occurs?

My suggestion for normITAp only worked because the example used Raw (Bit 4). If the type is not Bit (say Int 4), it still encounters the internal error, because normITAp doesn't have a rule for reducing SizeOf on that type.

In IExpand.evalAp', there is code to simplify type arguments:

-- simplify numeric types involving SizeOf
evalAp' e (T t : as) | not $ simpT t = do
    flags <- getFlags
    symt <- getSymTab
    case iConvT flags symt (iToCT t) of
      t'@(ITNum _) -> evalAp "simpNumT" e (T t' : as)
      _ -> errG (getIExprPosition e, EValueOf (ppString t))
  where simpT (ITNum _) = True
        simpT t = iGetKind t /= Just IKNum

This simplification only applies if the argument is numeric kind (#). But elaboration is introducing a type argument Bit (SizeOf T), as the type argument to primIf, because that's the type of the field in the datatype Raw. (The elaborator is converting if c then Raw e1 else Raw e2 to Raw (if c then e1 else e2).)

Potentially we can add an arm to evalAp' to reduce non-numeric types containing SizeOf:

evalAp' e (T t : as) | containsSizeOf t = do
    flags <- getFlags
    symt <- getSymTab
    case iConvT flags symt (iToCT t) of
      t' | t' /= t-> evalAp "simpNumT" e (T t' : as)
      _ -> -- XXX Is this a user error?
           internalError ("could not resolve SizeOf: " ++ ppString t)
  where containsSizeOf (ITAp (ITCon op _ _) _) | op == idSizeOf = True
        containsSizeOf (ITAp f a) = containsSizeOf f || containsSizeOf a
        containsSizeOf _ = False

This fixes the example and passes the test suite. However, I don't know the impact of traversing every non-numeric type argument (to find SizeOf) and then testing for equality (although we could live dangerously and not test).

The alternative is to perform the reduction at the place where the type argument is introduced. We would just need to be sure that we've covered all the possible places. The benefit of evalAp' is that it will cover all situations, regardless of where the type argument was introduced.

The example triggers an issue because SizeOf appears in the type of a field of a datatype. During elaboration, that type gets introduced when constructing and deconstructing the datatype. (And I think those can all be identified by looking for iConType in IExpand.hs.) I believe that most of these are benign, as they aren't introducing a type parameter. (But could the type become a type parameters if it interacts with something later?) The problem is in improveIf which performs the transform that I mentioned above, introducing a type parameter to primIf.

Instead of trying to reduce all type parameters encountered (in evalAp'), we could just reduce the parameter created in this optimization. For example, in improveIf, we would need this for constructors:

-- push if improvement inside matching constructors
improveIf f t cnd (IAps (ICon i1 c1@(ICCon {conTagInfo = cti1})) ts1 es1)
                  (IAps (ICon i2 c2@(ICCon {conTagInfo = cti2})) ts2 es2) | conNo cti1 == conNo cti2
                                                           -- need to check that constructor numbers match
                                                           -- because that test is otherwise buried in i1 == i2
                                                           = do
  when doTraceIf $ traceM ("improveIf ICCon triggered" ++ show i1 ++ show i2)
  flags <- getFlags
  symt <- getSymTab
  -- Get the type of the constructor as used here,
  -- by substituing in the types from the context
  let realConType0 = itInst (iConType c1) ts1
  -- Reduce any SizeOf operators in the type
  realConType = iConvT flags symt (iToCT realConType0)
  let (argTypes, _) = itGetArrows realConType
  when (length argTypes /= length es1 || length argTypes /= length es2) $
      internalError ("improveIf Con:" ++ ppReadable (argTypes, es1, es2))
  (es', bs) <- mapAndUnzipM (\(t, e1, e2) -> improveIf f t cnd e1 e2) (zip3 argTypes es1 es2)
  -- unambiguous improvement because the ICCon has propagated out
  return ((IAps (ICon i1 c1) ts1 es'), True)

I would guess that this is more efficient than trying all non-numeric type parameters in evalAp') (It also has the benefit of knowing that the reduction is only applied once, so if fails to reduce, there'll be no loop.)

We would need to do the same for struct fields (in the arm of improveIf that follows this one for unions). However, I don't know if there might be other situations that would introduce SizeOf in a type argument. The benefit of the evalAp' approach is that it would handle any situation.

FYI, here's a version that introduces the type argument in improveIf for structs:

struct Raw t = { f :: Bit (SizeOf t) }
  deriving (Bits);

cook :: (Bits t tsz) => Raw t -> t
cook r = unpack r.f

A third alternative is to give normITAp access to the symbol table, so that it can reduce SizeOf. (Should we be concerned that overlapping instances might be defined for Bits, and whether the instance resolution for SizeOf is resolving to the right one?)

Note that constructor fields containing type operators like TAdd etc don't cause an internal error (the type operators get reduced). This is because improveIf is constructing the type with itInst, which calls tSubst which calls normITAp, which reduces TAdd etc. (Looking at all the places where itInst is called in the evaluator, it does seem that the two places in improveIf are the only ones that could introduce a SizeOf.)

Here's an example of using TAdd:

data Raw sz = Raw (Bit (TAdd sz 1))
  deriving (Bits);

cook :: (Bits t tsz) => Raw tsz -> t
cook (Raw x) = unpack (truncate x)

Another possibility (and perhaps the cleanest) is that the evaluator shouldn't have to reconstruct types, they should be available -- for example, by replacing SizeOf in datatype fields with a type variable that is passed in as a type/dictionary argument to the constructor. Type-checking would insert this argument, and it would be available for use by the evaluator when transforming code (such as the if-expr optimization).

B-Lang-org / bsc