Do X to undefined# in the evaluator

Fixes #2154

changelog/2022-03-30T13_55_22+02_00_fix2154

@@ -0,0 +1 @@
+FIXED: Simulation/Synthesis mismatch for X-exception to undefined bitvector conversion [#2154](https://github.com/clash-lang/clash-compiler/issues/2154)

clash-ghc/src-ghc/Clash/GHC/Evaluator.hs

@@ -1,6 +1,6 @@
 {-|
-  Copyright   :  (C) 2017, Google Inc.,
-                     2021, QBayLogic B.V.
+  Copyright   :  (C) 2017-2022, Google Inc.,
+                     2021     , QBayLogic B.V.
   License     :  BSD2 (see the file LICENSE)
   Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
 
@@ -49,7 +49,7 @@ import           Clash.Core.Util
 import           Clash.Core.Var
 import           Clash.Core.VarEnv
 import           Clash.Debug
-import qualified Clash.Normalize.Primitives as NP (undefined)
+import qualified Clash.Normalize.Primitives as NP (undefined, undefinedX)
 import           Clash.Unique
 import           Clash.Util                              (curLoc)
 
@@ -166,7 +166,7 @@ stepApp x y m tcm =
                     in  ghcPrimStep tcm (forcePrims m) p [] [Suspend (Var i), Suspend (Var j)] m1
 
               (e':es)
-                | primName p `elem` undefinedPrims
+                | primName p `elem` (undefinedXPrims ++ undefinedPrims)
                 -> ghcUnwind (PrimVal p (rights args) (map Suspend (e':es))) m tcm
                 | otherwise
                 -> Just . setTerm e' $ stackPush (PrimApply p (rights args) [] es) m
@@ -199,7 +199,8 @@ stepTyApp x ty m tcm =
        in case compare (length args) (length tys) of
             EQ -> case lefts args of
                     [] | primName p `elem` [ "Clash.Normalize.Primitives.removedArg"
-                                           , "Clash.Normalize.Primitives.undefined" ] ->
+                                           , "Clash.Normalize.Primitives.undefined"
+                                           , "Clash.Normalize.Primitives.undefinedX" ] ->
                             ghcUnwind (PrimVal p (rights args) []) m tcm
 
                        | otherwise ->
@@ -315,6 +316,8 @@ apply _tcm (Lambda x' e) x m =
   subst  = extendIdSubst subst0 x' (Var x)
   subst0 = mkSubst $ extendInScopeSet (mScopeNames m) x
 apply tcm pVal@(PrimVal (PrimInfo{primType}) tys vs) x m
+  | isUndefinedXPrimVal pVal
+  = setTerm (TyApp (Prim NP.undefinedX) ty) m
   | isUndefinedPrimVal pVal
   = setTerm (TyApp (Prim NP.undefined) ty) m
  where
@@ -331,6 +334,8 @@ instantiate _tcm (TyLambda x e) ty m =
   subst0 = mkSubst iss0
   iss0   = mkInScopeSet (freeVarsOf e `unionUniqSet` freeVarsOf ty)
 instantiate tcm pVal@(PrimVal (PrimInfo{primType}) tys []) ty m
+  | isUndefinedXPrimVal pVal
+  = setTerm (TyApp (Prim NP.undefinedX) (piResultTys tcm primType (tys ++ [ty]))) m
   | isUndefinedPrimVal pVal
   = setTerm (TyApp (Prim NP.undefined) (piResultTys tcm primType (tys ++ [ty]))) m
 
@@ -405,6 +410,8 @@ scrutinise (DC dc xs) _altTy alts m
   = setTerm altE m
 
 scrutinise v@(PrimVal p _ vs) altTy alts m
+  | isUndefinedXPrimVal v
+  = setTerm (TyApp (Prim NP.undefinedX) altTy) m
   | isUndefinedPrimVal v
   = setTerm (TyApp (Prim NP.undefined) altTy) m
 

clash-ghc/src-ghc/Clash/GHC/Evaluator/Primitive.hs

@@ -1,8 +1,8 @@
 {-|
   Copyright   :  (C) 2013-2016, University of Twente,
                      2016-2017, Myrtle Software Ltd,
-                     2017     , QBayLogic, Google Inc.,
-                     2021-2022, QBayLogic B.V.
+                     2017-2022, Google Inc.,
+                     2017-2022, QBayLogic B.V.
   License     :  BSD2 (see the file LICENSE)
   Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
 -}
@@ -20,6 +20,7 @@ module Clash.GHC.Evaluator.Primitive
   ( ghcPrimStep
   , ghcPrimUnwind
   , isUndefinedPrimVal
+  , isUndefinedXPrimVal
   ) where
 
 import           Control.Concurrent.Supply  (Supply,freshId)
@@ -88,15 +89,16 @@ import           Clash.Core.Name
 import           Clash.Core.Pretty   (showPpr)
 import           Clash.Core.Term
   (IsMultiPrim (..), Pat (..), PrimInfo (..), Term (..), WorkInfo (..), mkApps,
-   PrimUnfolding(..))
+   PrimUnfolding(..), collectArgs)
 import           Clash.Core.Type
   (Type (..), ConstTy (..), LitTy (..), TypeView (..), mkFunTy, mkTyConApp,
    splitFunForallTy, tyView)
 import           Clash.Core.TyCon
   (TyConMap, TyConName, tyConDataCons)
 import           Clash.Core.TysPrim
 import           Clash.Core.Util
-  (mkRTree,mkVec,tyNatSize,dataConInstArgTys,primCo, mkSelectorCase,undefinedPrims)
+  (mkRTree,mkVec,tyNatSize,dataConInstArgTys,primCo, mkSelectorCase,undefinedPrims,
+   undefinedXPrims)
 import           Clash.Core.Var      (mkLocalId, mkTyVar)
 import           Clash.Debug
 import           Clash.GHC.GHC2Core  (modNameM)
@@ -124,6 +126,11 @@ isUndefinedPrimVal (PrimVal (PrimInfo{primName}) _ _) =
   primName `elem` undefinedPrims
 isUndefinedPrimVal _ = False
 
+isUndefinedXPrimVal :: Value -> Bool
+isUndefinedXPrimVal (PrimVal (PrimInfo{primName}) _ _) =
+  primName `elem` undefinedXPrims
+isUndefinedXPrimVal _ = False
+
 -- | Evaluation of primitive operations.
 ghcPrimUnwind :: PrimUnwind
 ghcPrimUnwind tcm p tys vs v [] m
@@ -132,6 +139,7 @@ ghcPrimUnwind tcm p tys vs v [] m
                        , Text.pack (show 'NP.removedArg)
                        , "GHC.Prim.MutableByteArray#"
                        , Text.pack (show 'NP.undefined)
+                       , Text.pack (show 'NP.undefinedX)
                        ]
               -- The above primitives are actually values, and not operations.
   = ghcUnwind (PrimVal p tys (vs ++ [v])) m tcm
@@ -160,6 +168,11 @@ ghcPrimUnwind tcm p tys vs v [] m
         tmArgs = map (Left . valToTerm) (vs ++ [v])
     in  Just $ flip setTerm m $ TyApp (Prim NP.undefined) $
           applyTypeToArgs (Prim p) tcm (primType p) (tyArgs ++ tmArgs)
+  | isUndefinedXPrimVal v
+  = let tyArgs = map Right tys
+        tmArgs = map (Left . valToTerm) (vs ++ [v])
+    in  Just $ flip setTerm m $ TyApp (Prim NP.undefinedX) $
+          applyTypeToArgs (Prim p) tcm (primType p) (tyArgs ++ tmArgs)
   | otherwise
   = ghcPrimStep tcm (forcePrims m) p tys (vs ++ [v]) m
 
@@ -174,6 +187,7 @@ ghcPrimUnwind tcm p tys vs v [e] m0
                        , "Clash.Sized.Vector.replace_int"
                        , "GHC.Classes.&&"
                        , "GHC.Classes.||"
+                       , "Clash.Class.BitPack.Internal.xToBV"
                        ]
   = if isUndefinedPrimVal v then
       let tyArgs = map Right tys
@@ -1795,6 +1809,27 @@ ghcPrimStep tcm isSubj pInfo tys args mach = case primName pInfo of
            val = unpack (toBV i :: BitVector 64)
         in reduce (mkDoubleCLit tcm val resTy)
 
+  "Clash.Class.BitPack.Internal.xToBV"
+    | isSubj
+    , Just (nTy, kn) <- extractKnownNat tcm tys
+    , [ _, (Suspend arg) ] <- args
+    , eval <- Evaluator ghcStep ghcUnwind ghcPrimStep ghcPrimUnwind
+    , mach1@Machine{mStack=[],mTerm=argWHNF} <-
+        whnf eval tcm True (setTerm arg (stackClear mach))
+    , let undefBitVector =
+            Just $ mach1
+                 { mStack = mStack mach
+                 , mTerm  = mkBitVectorLit ty nTy kn (bit (fromInteger kn)-1) 0
+                 }
+    -> case isX argWHNF of
+         Left _ -> undefBitVector
+         _ -> case collectArgs argWHNF of
+           (Prim p,_) | primName p `elem` undefinedXPrims -> undefBitVector
+           _ -> Just $ mach1
+                     { mStack = mStack mach
+                     , mTerm  = argWHNF
+                     }
+
   -- expIndex#
   --   :: KnownNat m
   --   => Index m

clash-ghc/src-ghc/Clash/GHC/GHC2Core.hs

@@ -1,7 +1,7 @@
 {-|
   Copyright   :  (C) 2013-2016, University of Twente,
                      2016-2017, Myrtle Software Ltd,
-                     2017-2818, Google Inc.
+                     2017-2022, Google Inc.
                      2021,      QBayLogic B.V.,
   License     :  BSD2 (see the file LICENSE)
   Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>
@@ -159,8 +159,9 @@ import qualified Clash.Core.Name             as C
 import qualified Clash.Core.Term             as C
 import qualified Clash.Core.TyCon            as C
 import qualified Clash.Core.Type             as C
-import qualified Clash.Core.Util             as C (undefinedTy)
+import qualified Clash.Core.Util             as C (undefinedTy, undefinedXPrims)
 import qualified Clash.Core.Var              as C
+import           Clash.Normalize.Primitives  as C
 import           Clash.Primitives.Types
 import qualified Clash.Unique                as C
 import           Clash.Util
@@ -381,9 +382,6 @@ coreToTerm primMap unlocs = term
         go "GHC.Stack.withFrozenCallStack"     args
           | length args == 3
           = term (App (args!!2) (args!!1))
-        go "Clash.Class.BitPack.Internal.packXWith" args
-          | [_nTy,_aTy,_kn,f] <- args
-          = term f
         go "Clash.Sized.BitVector.Internal.checkUnpackUndef" args
           | [_nTy,_aTy,_kn,_typ,f] <- args
           = term f
@@ -461,9 +459,34 @@ coreToTerm primMap unlocs = term
         x' <- coreToIdSP sp x
         return (x',b')
 
-    term' (Case _ _ ty [])  =
-      C.TyApp (C.Prim (C.PrimInfo (pack "EmptyCase") C.undefinedTy C.WorkNever C.SingleResult C.NoUnfolding))
-        <$> coreToType ty
+    term' (Case s _ ty [])  = do
+      s'  <- term' s
+      ty' <- coreToType ty
+      case C.collectArgs s' of
+        (C.Prim p, _) | C.primName p `elem` C.undefinedXPrims ->
+          -- GHC translates things like:
+          --
+          --   xToBV (Index.pack# (errorX @TY "QQ"))
+          --
+          -- to
+          --
+          --   xToBV (case (errorX @TY "QQ") of {})
+          --
+          --
+          -- Here we then translate
+          --
+          --   case (errorX @TY "QQ") of {}
+          --
+          -- to
+          --
+          --   undefinedX @TY
+          --
+          -- So that the evaluator rule for 'xToBV' can recognize things that
+          -- would normally throw XException
+          return (C.TyApp (C.Prim C.undefinedX) ty')
+        _ ->
+          return (C.TyApp (C.Prim C.undefined) ty')
+
     term' (Case e b ty alts) = do
      let usesBndr = any ( not . isEmptyVarSet . exprSomeFreeVars (== b))
                   $ rhssOfAlts alts
@@ -550,7 +573,6 @@ coreToTerm primMap unlocs = term
               | f == "GHC.Magic.noinline"               -> return (idTerm xType)
               | f == "GHC.Magic.lazy"                   -> return (idTerm xType)
               | f == "GHC.Magic.runRW#"                 -> return (runRWTerm xType)
-              | f == "Clash.Class.BitPack.Internal.packXWith"    -> return (packXWithTerm xType)
               | f == "Clash.Sized.Internal.BitVector.checkUnpackUndef" -> return (checkUnpackUndefTerm xType)
               | f == "Clash.Magic.prefixName"
               -> return (nameModTerm C.PrefixName xType)
@@ -1343,32 +1365,6 @@ runRWTerm (C.ForAllTy rTV (C.ForAllTy oTV funTy)) =
 
 runRWTerm ty = error $ $(curLoc) ++ show ty
 
--- | Given type type:
---
--- @forall (n :: Nat) (a :: Type) .Knownnat n => (a -> BitVector n) -> a -> BitVector n@
---
--- Generate the term:
---
--- @/\(n:Nat)./\(a:TYPE r).\(kn:KnownNat n).\(f:a -> BitVector n).f@
-packXWithTerm
-  :: C.Type
-  -> C.Term
-packXWithTerm (C.ForAllTy nTV (C.ForAllTy aTV funTy)) =
-  C.TyLam nTV (
-  C.TyLam aTV (
-  C.Lam knId (
-  C.Lam fId (
-  C.Var fId))))
-  where
-    C.FunTy knTy rTy = C.tyView funTy
-    C.FunTy fTy _    = C.tyView rTy
-    knName           = C.mkUnsafeSystemName "kn" 0
-    fName            = C.mkUnsafeSystemName "f" 1
-    knId             = C.mkLocalId knTy knName
-    fId              = C.mkLocalId fTy fName
-
-packXWithTerm ty = error $ $(curLoc) ++ show ty
-
 -- | Given type type:
 --
 -- @forall (n :: Nat) (a :: Type) .Knownnat n => Typeable a => (BitVector n -> a) -> BitVector n -> a@

clash-ghc/src-ghc/Clash/GHC/PartialEval/Eval.hs

@@ -1,5 +1,6 @@
 {-|
-Copyright   : (C) 2020-2021, QBayLogic B.V.
+Copyright   : (C) 2020-2021, QBayLogic B.V.,
+                  2022     , Google Inc.
 License     : BSD2 (see the file LICENSE)
 Maintainer  : QBayLogic B.V. <devops@qbaylogic.com>
 
@@ -49,7 +50,7 @@ import           Clash.Core.Type
 import           Clash.Core.TysPrim (integerPrimTy)
 import           Clash.Core.Var
 import           Clash.Driver.Types (Binding(..), IsPrim(..))
-import qualified Clash.Normalize.Primitives as NP (undefined)
+import qualified Clash.Normalize.Primitives as NP (undefined, undefinedX)
 import           Clash.Unique (lookupUniqMap')
 
 -- | Evaluate a term to WHNF.
@@ -290,7 +291,9 @@ caseCon subject ty alts = do
   forcedSubject <- keepLifted (forceEval subject)
 
   -- If the subject is undefined, the whole expression is undefined.
-  case isUndefined forcedSubject of
+  case isUndefinedX forcedSubject of
+   True -> eval (TyApp (Prim NP.undefinedX) ty)
+   False -> case isUndefined forcedSubject of
     True -> eval (TyApp (Prim NP.undefined) ty)
     False ->
       case stripValue forcedSubject of

clash-lib/prims/common/Clash_Class_BitPack.primitives.yaml

@@ -26,3 +26,9 @@
       64 -> Double'
     template: ~ARG[0]
     workInfo: Never
+- BlackBox:
+    name: Clash.Class.BitPack.Internal.xToBV
+    kind: Expression
+    type: 'xToBV :: KnownNat n => BitVector n -> BitVector n'
+    template: ~ARG[1]
+    workInfo: Never

clash-lib/prims/common/Clash_GHC_GHC2Core.primitives.yaml

@@ -1,8 +1,3 @@
-- BlackBox:
-    name: EmptyCase
-    kind: Expression
-    template: ~ERRORO
-    workInfo: Constant
 - Primitive:
     name: _CO_
     primType: Constructor

clash-lib/prims/common/Clash_Normalize_Primitives.primitives.yaml

@@ -11,6 +11,12 @@
       a . a'
     template: ~ERRORO
     workInfo: Constant
+- BlackBox:
+    name: Clash.Normalize.Primitives.undefinedX
+    kind: Expression
+    type: 'undefinedX :: forall a . a'
+    template: ~ERRORO
+    workInfo: Constant
 - BlackBox:
     name: c$multiPrimSelect
     kind: Expression

clash-lib/src/Clash/Core/PartialEval/NormalForm.hs

@@ -1,5 +1,6 @@
 {-|
-Copyright   : (C) 2020-2021, QBayLogic B.V.
+Copyright   : (C) 2020-2021, QBayLogic B.V.,
+                  2022     , Google Inc.
 License     : BSD2 (see the file LICENSE)
 Maintainer  : QBayLogic B.V. <devops@qbaylogic.com>
 
@@ -24,6 +25,7 @@ module Clash.Core.PartialEval.NormalForm
   , stripValue
   , collectValueTicks
   , isUndefined
+  , isUndefinedX
   , Normal(..)
   , LocalEnv(..)
   , GlobalEnv(..)
@@ -40,7 +42,7 @@ import Clash.Core.Literal
 import Clash.Core.Term (Bind, Term(..), PrimInfo(primName), TickInfo, Pat)
 import Clash.Core.TyCon (TyConMap)
 import Clash.Core.Type (Type, TyVar)
-import Clash.Core.Util (undefinedPrims)
+import Clash.Core.Util (undefinedPrims, undefinedXPrims)
 import Clash.Core.Var (Id)
 import Clash.Core.VarEnv (VarEnv, InScopeSet)
 import Clash.Driver.Types (Binding(..))
@@ -127,6 +129,13 @@ isUndefined = \case
 
   _ -> False
 
+isUndefinedX :: Value -> Bool
+isUndefinedX = \case
+  VNeutral (NePrim pr _) ->
+    primName pr `elem` undefinedXPrims
+
+  _ -> False
+
 -- | A term which is in beta-normal eta-long form (NF). This has no redexes,
 -- and all partially applied functions in sub-terms are eta-expanded.
 --