Merge pull request #2153 from clash-lang/prim_eval_fixes

Prim eval fixes

Author: christiaanb

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. <[email protected]>
 
@@ -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 (removedArg, undefined, undefinedX)
 import           Clash.Unique
 import           Clash.Util                              (curLoc)
 
@@ -165,8 +165,17 @@ stepApp x y m tcm =
                         (m1,j) = newLetBinding tcm m0 a1
                     in  ghcPrimStep tcm (forcePrims m) p [] [Suspend (Var i), Suspend (Var j)] m1
 
-              (e':es) ->
-                Just . setTerm e' $ stackPush (PrimApply p (rights args) [] es) m
+              (e':es)
+                | primName p `elem` (undefinedXPrims ++ undefinedPrims)
+                -- The above primitives are (bottoming) values, whose arguments
+                -- are never used anywhere in the rest of the compiler. So
+                -- instead of pushing a PrimApply frame on the stack to evaluate
+                -- those arguments, we instead just unwind the stack with the
+                -- primitive value and leave its arguments in an unevaluated
+                -- state (Suspend).
+                -> ghcUnwind (PrimVal p (rights args) (map Suspend (e':es))) m tcm
+                | otherwise
+                -> Just . setTerm e' $ stackPush (PrimApply p (rights args) [] es) m
 
               _ -> error "internal error"
 
@@ -195,8 +204,9 @@ stepTyApp x ty m tcm =
       let tys = fst $ splitFunForallTy (primType p)
        in case compare (length args) (length tys) of
             EQ -> case lefts args of
-                    [] | primName p `elem` [ "Clash.Normalize.Primitives.removedArg"
-                                           , "Clash.Normalize.Primitives.undefined" ] ->
+                    [] | primName p `elem` fmap primName [ NP.removedArg
+                                                         , NP.undefined
+                                                         , NP.undefinedX ] ->
                             ghcUnwind (PrimVal p (rights args) []) m tcm
 
                        | otherwise ->
@@ -312,6 +322,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
@@ -328,6 +340,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
 
@@ -402,6 +416,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. <[email protected]>
 -}
@@ -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,10 +168,18 @@ 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
 
 ghcPrimUnwind tcm p tys vs v [e] m0
+  -- Note [Lazy primitives]
+  -- ~~~~~~~~~~~~~~~~~~~~~~
+  --
   -- Primitives are usually considered undefined when one of their arguments is
   -- (unless they're unused). _Some_ primitives can still yield a result even
   -- though one of their arguments is undefined. It turns out that all primitives
@@ -174,6 +190,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
@@ -1585,6 +1602,11 @@ ghcPrimStep tcm isSubj pInfo tys args mach = case primName pInfo of
     | [Lit (NaturalLiteral n), _] <- args
     -> reduce (Literal (NaturalLiteral n))
 
+  "GHC.TypeNats.someNatVal"
+    | [Lit (NaturalLiteral n)] <- args
+    -> let resTy = getResultTy tcm ty tys
+        in reduce (mkSomeNat tcm n resTy)
+
   "GHC.Int.I8#"
     | isSubj
     , [Lit (IntLiteral i)] <- args
@@ -1790,6 +1812,29 @@ 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
+    -- The second argument to `xToBV` is always going to be suspended.
+    -- See Note [Lazy primitives]
+    , [ _, (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
@@ -4213,6 +4258,31 @@ mkDoubleCLit tcm lit resTy =
   (Just doubleTc) = lookupUniqMap doubleTcNm tcm
   [doubleDc] = tyConDataCons doubleTc
 
+mkSomeNat :: TyConMap -> Integer -> Type -> Term
+mkSomeNat tcm lit resTy =
+  mkApps (Data someNatDc)
+         [ Right (LitTy (NumTy lit))
+         , Left (Literal (NaturalLiteral lit))
+         , Left proxy
+         ]
+ where
+  -- Get the SomeNat data constructor
+  TyConApp someNatTcNm [] = tyView resTy
+  (Just someNatTc) = lookupUniqMap someNatTcNm tcm
+  [someNatDc] = tyConDataCons someNatTc
+
+  -- Get the Proxy data constructor
+  (_:_:Right (tyView -> TyConApp proxyTcNm [natTy,_]):_,_) =
+    splitFunForallTy (dcType someNatDc)
+  (Just proxyTc) = lookupUniqMap proxyTcNm tcm
+  [proxyDc] = tyConDataCons proxyTc
+
+  -- Build the Proxy argument
+  proxy = mkApps (Data proxyDc)
+                 [ Right natTy
+                 , Right (LitTy (NumTy lit))
+                 ]
+
 -- From an argument list to function of type
 --   forall n. KnownNat n => ...
 -- extract (nTy,nInt)

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. <[email protected]>
@@ -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. <[email protected]>
 
@@ -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