Bit Vector of Unknown Size Error in Generated Bluespec Code

[sukhmankkahlon]

I created a Copilot (Haskell) specification that, when compiled into bluespec, produces code that BSC cannot compile correctly.

Specifically, I created the following haskell file, which compares the first element of an array of 1 with a constant value of 4 to just a single constant value of 4.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
module Main (main) where
import GHC.Generics (Generic)

import Copilot.Compile.Bluespec
import Language.Copilot
import Prelude hiding ((++), (==), (!))

-- Testing Equivalence

-- array == vector in bluespec
-- have to wrap it in a constant because we want one value
arr :: Stream (Array 1 Int16)
arr = constant (array [4::Int16])

single :: Stream Int16
single = constant (4::Int16)

--extract the first element of your array 
arrfirst :: Stream Int16
arrfirst = arr ! 0

isequal :: Stream Bool
isequal = single == arrfirst

spec :: Spec
spec = do
    trigger "single" (true) [arg single]
    trigger "vector" (true) [arg arr]
    trigger "isequal" (true) [arg isequal]

main :: IO ()
main = do
  spec' <- reify spec
  compile "TestOne" spec'

Compiling this into bluespec completes without errors but, when I compile the resulting bluespec, I get issues from the generated bluespec code stating:

"Error: "TestOne.bs", line 31, column 19: (T0035)
Bit vector of unknown size introduced near this location.
Please remove unnecessary extensions, truncations and concatenations and/or
provide more type information to resolve this ambiguity."

Below is my top bluespec module, which should just display the (numeric) values of single and arr, and the Boolean value of isequal at any point in time:

--Top Level Module TopOne.bs
package TopOne where

import TestOne
import TestOneIfc
import TestOneTypes


testOneIfc :: Prelude.Module TestOneIfc
testOneIfc = 
  module
    interface
      single x =
        $display "single %0d" x

      vector x =
        $display "vector %0d" x

      isequal x =
        $display "equal %0d" x

mkTopOne :: Prelude.Module Prelude.Empty
mkTopOne = mkTestOne testOneIfc

TestOne.bs Generated Bluespec File

package TestOne where {
import FloatingPoint;
                    
import Vector;
             
import TestOneTypes;
                   
import TestOneIfc;
                 
import BluespecFP;
                 
mkTestOne :: Prelude.Module TestOneIfc ->
             Prelude.Module Prelude.Empty;
mkTestOne ifcMod = 
    module {
      ifc <- ifcMod;
      let { single_0_guard :: Prelude.Bool;
            single_0_guard =  Prelude.True;
            single_0_arg0 :: Prelude.Int 16;
            single_0_arg0 =  4::(Prelude.Int 16);
            vector_1_guard :: Prelude.Bool;
            vector_1_guard =  Prelude.True;
            vector_1_arg0 :: Vector.Vector 1 (Prelude.Int 16);
            vector_1_arg0 =  update newVector 0 (4::(Prelude.Int 16));
            isequal_2_guard :: Prelude.Bool;
            isequal_2_guard =  Prelude.True;
            isequal_2_arg0 :: Prelude.Bool;
            isequal_2_arg0 = 
                (Prelude.==)
                  (4::(Prelude.Int 16))
                  (select
                     (update newVector 0 (4::(Prelude.Int 16)))
                     (0::(Prelude.UInt 32))); };
      rules {
        
        "single_0":  when single_0_guard   ==> ifc.single single_0_arg0;
        
        "vector_1":  when vector_1_guard   ==> ifc.vector vector_1_arg0;
        
        "isequal_2":  when isequal_2_guard   ==> ifc.isequal isequal_2_arg0
      }
    };
}

TestOneIfc.bs Generated Bluespec File

package TestOneIfc where {
import FloatingPoint;
                    
import Vector;
             
import TestOneTypes;
                   
interface TestOneIfc = {
    single :: Prelude.Int 16 -> Prelude.Action;
    vector :: Vector.Vector 1 (Prelude.Int 16) -> Prelude.Action;
    isequal :: Prelude.Bool -> Prelude.Action
}
}

[RyanGlScott]

The relevant code that it is complaining about is:

isequal_2_arg0 :: Prelude.Bool;
isequal_2_arg0 =
    (Prelude.==)
      (4::(Prelude.Int 16))
      (select
         (update newVector 0 (4::(Prelude.Int 16)))
         (0::(Prelude.UInt 32))); };

This calls select on a Vector n (Int 16) value, but there isn't enough type information to figure out what n should be. Normally, calls to newVector/update (which work over Vectors of any length) are accompanied by a type signature that clarifies the length, but isequal is a degenerate case where this does not happen.

Two possible ways of fixing this that come to mind:

1. Instead of of building a Vector value using newVector/update, build a Vector value using nil/cons, i.e.,

   isequal_2_arg0 :: Prelude.Bool;
   isequal_2_arg0 =
       (Prelude.==)
         (4::(Prelude.Int 16))
         (select
            (cons (4::(Prelude.Int 16)) nil)
            (0::(Prelude.UInt 32))); };

2. Add an explicit type signature to the call to newVector, i.e.,

   isequal_2_arg0 :: Prelude.Bool;
   isequal_2_arg0 =
       (Prelude.==)
         (4::(Prelude.Int 16))
         (select
            (update (newVector :: Vector 1 (Int 16)) 0 (4::(Prelude.Int 16)))
            (0::(Prelude.UInt 32))); };

The Bluespec Reference Guide notes that cons can lead to large compile times, so my preference would be towards option (2).

[RyanGlScott]

Here is a proof-of-concept patch which implements option (2):

diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs
index 6d9fde04..4cab3f10 100644
--- a/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs
+++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs
@@ -70,6 +70,7 @@ mkBuffDecln sId ty xs =
                    (genVector
                      (\idx _ -> BS.CVar $ BS.mkId BS.NoPos $
                                 fromString $ streamElemName sId idx)
+                     ty
                      xs)

     nameId   = BS.mkId BS.NoPos $ fromString $ streamName sId
diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
index c4978aef..6c3d95d9 100644
--- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
+++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}

 -- | Translate Copilot Core expressions and operators to Bluespec.
 module Copilot.Compile.Bluespec.Expr
@@ -568,14 +569,14 @@ constTy ty =
 -- | Transform a list of Copilot Core expressions of a given 'Type' into a
 -- Bluespec @Vector@ expression.
 constVector :: Type a -> [a] -> BS.CExpr
-constVector ty = genVector (\_ -> constTy ty)
+constVector ty = genVector (\_ -> constTy ty) ty

 -- | Transform a list of Copilot Core expressions into a Bluespec @Vector@
--- expression. When invoking @genVector f es@, where @es@ has length @n@, the
--- resulting @Vector@ will consist of
+-- expression. When invoking @genVector f ty es@, where @es@ has length @n@ and
+-- each element is of type @ty@, the resulting @Vector@ will consist of
 -- @[f 0 (es !! 0), f 1 (es !! 1), ..., f (n-1) (es !! (n-1))]@.
-genVector :: (Int -> a -> BS.CExpr) -> [a] -> BS.CExpr
-genVector f vec =
+genVector :: (Int -> a -> BS.CExpr) -> Type a -> [a] -> BS.CExpr
+genVector f ty vec =
   snd $
   foldl'
     (\(!i, !v) x ->
@@ -585,8 +586,15 @@ genVector f vec =
           (cLit (BS.LInt (BS.ilDec (toInteger i))))
           (f i x)
       ))
-    (0, BS.CVar (BS.mkId BS.NoPos "newVector"))
+    ( 0
+    , withBsTypeAnnotation
+        (tVector `BS.TAp` BS.cTNum vecLength BS.NoPos `BS.TAp` transType ty)
+        (BS.CVar (BS.mkId BS.NoPos "newVector"))
+    )
     vec
+  where
+    vecLength :: Integer
+    vecLength = toInteger (length vec)

 -- | Translate a literal number of type @ty@ into a Bluespec expression.
 --
@@ -656,7 +664,12 @@ fpFunId ty funPrefix =
 -- | Explicitly annotate an expression with a type signature. This is necessary
 -- 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)
+withTypeAnnotation ty = withBsTypeAnnotation (transType ty)
+
+-- | Like 'withTypeAnnotation', except that this takes a raw Bluespec 'BS.Type'
+-- instead of a Copilot 'Type'.
+withBsTypeAnnotation :: BS.Type -> BS.CExpr -> BS.CExpr
+withBsTypeAnnotation ty e = e `BS.CHasType` BS.CQType [] ty

 -- | True if the type given is a floating point number.
 typeIsFloating :: Type a -> Bool

[RyanGlScott]

I see that this was closed, but I think there is still an unresolved bug in copilot-bluespec that needs to be addressed. I think this warrants an actual issue on the Copilot issue tracker, however. @ivanperez-keera, should I open this issue?