Render overflowed Index literals as errors

Author: leonschoorl

changelog/2024-10-01T14_41_36+02_00_fix_index_literal_rendering

@@ -1 +1,2 @@
 FIXED: Clash hanging when rendering `Index n` literals, for large values of `n` [#2813](https://github.com/clash-lang/clash-compiler/issues/2813)
+FIXED: Render overflowed Index literals as errors

clash-lib/src/Clash/Backend/VHDL.hs

@@ -1769,7 +1769,7 @@ expr_ _ (BlackBoxE pNm _ _ _ _ bbCtx _)
   , [Literal _ (NumLit n), Literal _ i] <- extractLiterals bbCtx
   , Just k <- clogBase 2 n
   , let k' = max 1 k
-  = exprLit (Just (Unsigned k',k')) i
+  = exprLit (Just (Index n,k')) i
 
 expr_ _ (BlackBoxE pNm _ _ _ _ bbCtx _)
   | pNm == "Clash.Sized.Internal.Index.maxBound#"
@@ -1867,6 +1867,9 @@ exprLit (Just (hty,sz)) (NumLit i) = case hty of
     | i < 0                    -> "unsigned" <> parens ("std_logic_vector" <> parens ("to_signed" <> parens(integer i <> "," <> int n)))
     | i < 2^(31 :: Integer) -> "to_unsigned" <> parens (integer i <> "," <> int n)
     | otherwise -> "unsigned'" <> parens lit
+  Index n
+   | 0 <= i && i < n -> exprLit (Just (Unsigned sz, sz)) (NumLit i)  -- reuse Unsigned implementation above
+   | otherwise       -> hdlTypeErrValue hty
   Signed n
     | i < 2^(31 :: Integer) && i > (-2^(31 :: Integer)) -> "to_signed" <> parens (integer i <> "," <> int n)
     | otherwise -> "signed'" <> parens lit

clash-lib/src/Clash/Backend/Verilog.hs

@@ -1218,14 +1218,16 @@ rtreeChain _                               = Nothing
 exprLitV :: Maybe (HWType,Size) -> Literal -> VerilogM Doc
 exprLitV = exprLit undefValue
 
-exprLit :: Lens' s (Maybe (Maybe Int)) -> Maybe (HWType,Size) -> Literal -> Ap (State s) Doc
+exprLit :: Backend s => Lens' s (Maybe (Maybe Int)) -> Maybe (HWType,Size) -> Literal -> Ap (State s) Doc
 exprLit _ Nothing (NumLit i) = integer i
 
 exprLit k (Just (hty,sz)) (NumLit i0) = case hty of
   Unsigned _
    | i < 0     -> string "-" <> int sz <> string "'d" <> integer (abs i)
    | otherwise -> int sz <> string "'d" <> integer i
-  Index _ -> int (typeSize hty) <> string "'d" <> integer i
+  Index n
+   | 0 <= i0 && i0 < n -> int (typeSize hty) <> string "'d" <> integer i0
+   | otherwise         -> hdlTypeErrValue hty
   Signed _
    | i < 0     -> string "-" <> int sz <> string "'sd" <> integer (abs i)
    | otherwise -> int sz <> string "'sd" <> integer i

tests/shouldfail/Verification/SymbiYosys.hs

@@ -13,10 +13,13 @@ import           Clash.Verification  (RenderAs (YosysFormal), assert, checkI,
 topEntity :: Clock System -> Reset System -> Enable System -> Signal System (Bool, Bool, Bool)
 topEntity = exposeClockResetEnable go
 
-go :: HiddenClockResetEnable dom => Signal dom (Bool, Bool, Bool)
+go :: forall dom. HiddenClockResetEnable dom => Signal dom (Bool, Bool, Bool)
 go =
   let -- oops, 'b' is never lit
-      c   = register (0 :: Index 15) (countSucc <$> c)
+      cI :: Signal dom (Index 15)
+      cI  = register (0 :: Index 15) (countSucc <$> cI)
+      c :: Signal dom (Unsigned 4)
+      c   = fmap bitCoerce cI
       r   = (< 10) <$> c
       g   = ((>= 10) .&&. (< 15)) <$> c
       b   = (>= 15) <$> c