Skip to content

Commit e6f8124

Browse files
christiaanbchristiaanb
committed
Do X to undefined# in the evaluator
Fixes #2154
1 parent 53ebf63 commit e6f8124

File tree

18 files changed

+198
-79
lines changed

18 files changed

+198
-79
lines changed

‎changelog/2022-03-30T13_55_22+02_00_fix2154‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
{-|
2-
Copyright : (C) 2017, Google Inc.,
3-
2021, QBayLogic B.V.
2+
Copyright : (C) 2017-2022, Google Inc.,
3+
2021 , QBayLogic B.V.
44
License : BSD2 (see the file LICENSE)
55
Maintainer : QBayLogic B.V. <[email protected]>
66
@@ -49,7 +49,7 @@ import Clash.Core.Util
4949
import Clash.Core.Var
5050
import Clash.Core.VarEnv
5151
import Clash.Debug
52-
import qualified Clash.Normalize.Primitives as NP (undefined)
52+
import qualified Clash.Normalize.Primitives as NP (removedArg, undefined, undefinedX)
5353
import Clash.Unique
5454
import Clash.Util (curLoc)
5555

@@ -166,7 +166,7 @@ stepApp x y m tcm =
166166
in ghcPrimStep tcm (forcePrims m) p [] [Suspend (Var i), Suspend (Var j)] m1
167167

168168
(e':es)
169-
| primName p `elem` undefinedPrims
169+
| primName p `elem` (undefinedXPrims ++ undefinedPrims)
170170
-- The above primitives are (bottoming) values, whose arguments
171171
-- are never used anywhere in the rest of the compiler. So
172172
-- instead of pushing a PrimApply frame on the stack to evaluate
@@ -204,8 +204,9 @@ stepTyApp x ty m tcm =
204204
let tys = fst $ splitFunForallTy (primType p)
205205
in case compare (length args) (length tys) of
206206
EQ -> case lefts args of
207-
[] | primName p `elem` [ "Clash.Normalize.Primitives.removedArg"
208-
, "Clash.Normalize.Primitives.undefined" ] ->
207+
[] | primName p `elem` fmap primName [ NP.removedArg
208+
, NP.undefined
209+
, NP.undefinedX ] ->
209210
ghcUnwind (PrimVal p (rights args) []) m tcm
210211

211212
| otherwise ->
@@ -321,6 +322,8 @@ apply _tcm (Lambda x' e) x m =
321322
subst = extendIdSubst subst0 x' (Var x)
322323
subst0 = mkSubst $ extendInScopeSet (mScopeNames m) x
323324
apply tcm pVal@(PrimVal (PrimInfo{primType}) tys vs) x m
325+
| isUndefinedXPrimVal pVal
326+
= setTerm (TyApp (Prim NP.undefinedX) ty) m
324327
| isUndefinedPrimVal pVal
325328
= setTerm (TyApp (Prim NP.undefined) ty) m
326329
where
@@ -337,6 +340,8 @@ instantiate _tcm (TyLambda x e) ty m =
337340
subst0 = mkSubst iss0
338341
iss0 = mkInScopeSet (freeVarsOf e `unionUniqSet` freeVarsOf ty)
339342
instantiate tcm pVal@(PrimVal (PrimInfo{primType}) tys []) ty m
343+
| isUndefinedXPrimVal pVal
344+
= setTerm (TyApp (Prim NP.undefinedX) (piResultTys tcm primType (tys ++ [ty]))) m
340345
| isUndefinedPrimVal pVal
341346
= setTerm (TyApp (Prim NP.undefined) (piResultTys tcm primType (tys ++ [ty]))) m
342347

@@ -411,6 +416,8 @@ scrutinise (DC dc xs) _altTy alts m
411416
= setTerm altE m
412417

413418
scrutinise v@(PrimVal p _ vs) altTy alts m
419+
| isUndefinedXPrimVal v
420+
= setTerm (TyApp (Prim NP.undefinedX) altTy) m
414421
| isUndefinedPrimVal v
415422
= setTerm (TyApp (Prim NP.undefined) altTy) m
416423

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

Lines changed: 44 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
{-|
22
Copyright : (C) 2013-2016, University of Twente,
33
2016-2017, Myrtle Software Ltd,
4-
2017 , QBayLogic, Google Inc.,
5-
2021-2022, QBayLogic B.V.
4+
2017-2022, Google Inc.,
5+
2017-2022, QBayLogic B.V.
66
License : BSD2 (see the file LICENSE)
77
Maintainer : QBayLogic B.V. <[email protected]>
88
-}
@@ -20,6 +20,7 @@ module Clash.GHC.Evaluator.Primitive
2020
( ghcPrimStep
2121
, ghcPrimUnwind
2222
, isUndefinedPrimVal
23+
, isUndefinedXPrimVal
2324
) where
2425

2526
import Control.Concurrent.Supply (Supply,freshId)
@@ -88,15 +89,16 @@ import Clash.Core.Name
8889
import Clash.Core.Pretty (showPpr)
8990
import Clash.Core.Term
9091
(IsMultiPrim (..), Pat (..), PrimInfo (..), Term (..), WorkInfo (..), mkApps,
91-
PrimUnfolding(..))
92+
PrimUnfolding(..), collectArgs)
9293
import Clash.Core.Type
9394
(Type (..), ConstTy (..), LitTy (..), TypeView (..), mkFunTy, mkTyConApp,
9495
splitFunForallTy, tyView)
9596
import Clash.Core.TyCon
9697
(TyConMap, TyConName, tyConDataCons)
9798
import Clash.Core.TysPrim
9899
import Clash.Core.Util
99-
(mkRTree,mkVec,tyNatSize,dataConInstArgTys,primCo, mkSelectorCase,undefinedPrims)
100+
(mkRTree,mkVec,tyNatSize,dataConInstArgTys,primCo, mkSelectorCase,undefinedPrims,
101+
undefinedXPrims)
100102
import Clash.Core.Var (mkLocalId, mkTyVar)
101103
import Clash.Debug
102104
import Clash.GHC.GHC2Core (modNameM)
@@ -124,6 +126,11 @@ isUndefinedPrimVal (PrimVal (PrimInfo{primName}) _ _) =
124126
primName `elem` undefinedPrims
125127
isUndefinedPrimVal _ = False
126128

129+
isUndefinedXPrimVal :: Value -> Bool
130+
isUndefinedXPrimVal (PrimVal (PrimInfo{primName}) _ _) =
131+
primName `elem` undefinedXPrims
132+
isUndefinedXPrimVal _ = False
133+
127134
-- | Evaluation of primitive operations.
128135
ghcPrimUnwind :: PrimUnwind
129136
ghcPrimUnwind tcm p tys vs v [] m
@@ -132,6 +139,7 @@ ghcPrimUnwind tcm p tys vs v [] m
132139
, Text.pack (show 'NP.removedArg)
133140
, "GHC.Prim.MutableByteArray#"
134141
, Text.pack (show 'NP.undefined)
142+
, Text.pack (show 'NP.undefinedX)
135143
]
136144
-- The above primitives are actually values, and not operations.
137145
= ghcUnwind (PrimVal p tys (vs ++ [v])) m tcm
@@ -160,10 +168,18 @@ ghcPrimUnwind tcm p tys vs v [] m
160168
tmArgs = map (Left . valToTerm) (vs ++ [v])
161169
in Just $ flip setTerm m $ TyApp (Prim NP.undefined) $
162170
applyTypeToArgs (Prim p) tcm (primType p) (tyArgs ++ tmArgs)
171+
| isUndefinedXPrimVal v
172+
= let tyArgs = map Right tys
173+
tmArgs = map (Left . valToTerm) (vs ++ [v])
174+
in Just $ flip setTerm m $ TyApp (Prim NP.undefinedX) $
175+
applyTypeToArgs (Prim p) tcm (primType p) (tyArgs ++ tmArgs)
163176
| otherwise
164177
= ghcPrimStep tcm (forcePrims m) p tys (vs ++ [v]) m
165178

166179
ghcPrimUnwind tcm p tys vs v [e] m0
180+
-- Note [Lazy primitives]
181+
-- ~~~~~~~~~~~~~~~~~~~~~~
182+
--
167183
-- Primitives are usually considered undefined when one of their arguments is
168184
-- (unless they're unused). _Some_ primitives can still yield a result even
169185
-- 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
174190
, "Clash.Sized.Vector.replace_int"
175191
, "GHC.Classes.&&"
176192
, "GHC.Classes.||"
193+
, "Clash.Class.BitPack.Internal.xToBV"
177194
]
178195
= if isUndefinedPrimVal v then
179196
let tyArgs = map Right tys
@@ -1795,6 +1812,29 @@ ghcPrimStep tcm isSubj pInfo tys args mach = case primName pInfo of
17951812
val = unpack (toBV i :: BitVector 64)
17961813
in reduce (mkDoubleCLit tcm val resTy)
17971814

1815+
"Clash.Class.BitPack.Internal.xToBV"
1816+
| isSubj
1817+
, Just (nTy, kn) <- extractKnownNat tcm tys
1818+
-- The second argument to `xToBV` is always going to be suspended.
1819+
-- See Note [Lazy primitives]
1820+
, [ _, (Suspend arg) ] <- args
1821+
, eval <- Evaluator ghcStep ghcUnwind ghcPrimStep ghcPrimUnwind
1822+
, mach1@Machine{mStack=[],mTerm=argWHNF} <-
1823+
whnf eval tcm True (setTerm arg (stackClear mach))
1824+
, let undefBitVector =
1825+
Just $ mach1
1826+
{ mStack = mStack mach
1827+
, mTerm = mkBitVectorLit ty nTy kn (bit (fromInteger kn)-1) 0
1828+
}
1829+
-> case isX argWHNF of
1830+
Left _ -> undefBitVector
1831+
_ -> case collectArgs argWHNF of
1832+
(Prim p,_) | primName p `elem` undefinedXPrims -> undefBitVector
1833+
_ -> Just $ mach1
1834+
{ mStack = mStack mach
1835+
, mTerm = argWHNF
1836+
}
1837+
17981838
-- expIndex#
17991839
-- :: KnownNat m
18001840
-- => Index m

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

Lines changed: 31 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
{-|
22
Copyright : (C) 2013-2016, University of Twente,
33
2016-2017, Myrtle Software Ltd,
4-
2017-2818, Google Inc.
4+
2017-2022, Google Inc.
55
2021, QBayLogic B.V.,
66
License : BSD2 (see the file LICENSE)
77
Maintainer : QBayLogic B.V. <[email protected]>
@@ -159,8 +159,9 @@ import qualified Clash.Core.Name as C
159159
import qualified Clash.Core.Term as C
160160
import qualified Clash.Core.TyCon as C
161161
import qualified Clash.Core.Type as C
162-
import qualified Clash.Core.Util as C (undefinedTy)
162+
import qualified Clash.Core.Util as C (undefinedTy, undefinedXPrims)
163163
import qualified Clash.Core.Var as C
164+
import Clash.Normalize.Primitives as C
164165
import Clash.Primitives.Types
165166
import qualified Clash.Unique as C
166167
import Clash.Util
@@ -381,9 +382,6 @@ coreToTerm primMap unlocs = term
381382
go "GHC.Stack.withFrozenCallStack" args
382383
| length args == 3
383384
= term (App (args!!2) (args!!1))
384-
go "Clash.Class.BitPack.Internal.packXWith" args
385-
| [_nTy,_aTy,_kn,f] <- args
386-
= term f
387385
go "Clash.Sized.BitVector.Internal.checkUnpackUndef" args
388386
| [_nTy,_aTy,_kn,_typ,f] <- args
389387
= term f
@@ -461,9 +459,34 @@ coreToTerm primMap unlocs = term
461459
x' <- coreToIdSP sp x
462460
return (x',b')
463461

464-
term' (Case _ _ ty []) =
465-
C.TyApp (C.Prim (C.PrimInfo (pack "EmptyCase") C.undefinedTy C.WorkNever C.SingleResult C.NoUnfolding))
466-
<$> coreToType ty
462+
term' (Case s _ ty []) = do
463+
s' <- term' s
464+
ty' <- coreToType ty
465+
case C.collectArgs s' of
466+
(C.Prim p, _) | C.primName p `elem` C.undefinedXPrims ->
467+
-- GHC translates things like:
468+
--
469+
-- xToBV (Index.pack# (errorX @TY "QQ"))
470+
--
471+
-- to
472+
--
473+
-- xToBV (case (errorX @TY "QQ") of {})
474+
--
475+
--
476+
-- Here we then translate
477+
--
478+
-- case (errorX @TY "QQ") of {}
479+
--
480+
-- to
481+
--
482+
-- undefinedX @TY
483+
--
484+
-- So that the evaluator rule for 'xToBV' can recognize things that
485+
-- would normally throw XException
486+
return (C.TyApp (C.Prim C.undefinedX) ty')
487+
_ ->
488+
return (C.TyApp (C.Prim C.undefined) ty')
489+
467490
term' (Case e b ty alts) = do
468491
let usesBndr = any ( not . isEmptyVarSet . exprSomeFreeVars (== b))
469492
$ rhssOfAlts alts
@@ -550,7 +573,6 @@ coreToTerm primMap unlocs = term
550573
| f == "GHC.Magic.noinline" -> return (idTerm xType)
551574
| f == "GHC.Magic.lazy" -> return (idTerm xType)
552575
| f == "GHC.Magic.runRW#" -> return (runRWTerm xType)
553-
| f == "Clash.Class.BitPack.Internal.packXWith" -> return (packXWithTerm xType)
554576
| f == "Clash.Sized.Internal.BitVector.checkUnpackUndef" -> return (checkUnpackUndefTerm xType)
555577
| f == "Clash.Magic.prefixName"
556578
-> return (nameModTerm C.PrefixName xType)
@@ -1343,32 +1365,6 @@ runRWTerm (C.ForAllTy rTV (C.ForAllTy oTV funTy)) =
13431365

13441366
runRWTerm ty = error $ $(curLoc) ++ show ty
13451367

1346-
-- | Given type type:
1347-
--
1348-
-- @forall (n :: Nat) (a :: Type) .Knownnat n => (a -> BitVector n) -> a -> BitVector n@
1349-
--
1350-
-- Generate the term:
1351-
--
1352-
-- @/\(n:Nat)./\(a:TYPE r).\(kn:KnownNat n).\(f:a -> BitVector n).f@
1353-
packXWithTerm
1354-
:: C.Type
1355-
-> C.Term
1356-
packXWithTerm (C.ForAllTy nTV (C.ForAllTy aTV funTy)) =
1357-
C.TyLam nTV (
1358-
C.TyLam aTV (
1359-
C.Lam knId (
1360-
C.Lam fId (
1361-
C.Var fId))))
1362-
where
1363-
C.FunTy knTy rTy = C.tyView funTy
1364-
C.FunTy fTy _ = C.tyView rTy
1365-
knName = C.mkUnsafeSystemName "kn" 0
1366-
fName = C.mkUnsafeSystemName "f" 1
1367-
knId = C.mkLocalId knTy knName
1368-
fId = C.mkLocalId fTy fName
1369-
1370-
packXWithTerm ty = error $ $(curLoc) ++ show ty
1371-
13721368
-- | Given type type:
13731369
--
13741370
-- @forall (n :: Nat) (a :: Type) .Knownnat n => Typeable a => (BitVector n -> a) -> BitVector n -> a@

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
{-|
2-
Copyright : (C) 2020-2021, QBayLogic B.V.
2+
Copyright : (C) 2020-2021, QBayLogic B.V.,
3+
2022 , Google Inc.
34
License : BSD2 (see the file LICENSE)
45
Maintainer : QBayLogic B.V. <[email protected]>
56
@@ -49,7 +50,7 @@ import Clash.Core.Type
4950
import Clash.Core.TysPrim (integerPrimTy)
5051
import Clash.Core.Var
5152
import Clash.Driver.Types (Binding(..), IsPrim(..))
52-
import qualified Clash.Normalize.Primitives as NP (undefined)
53+
import qualified Clash.Normalize.Primitives as NP (undefined, undefinedX)
5354
import Clash.Unique (lookupUniqMap')
5455

5556
-- | Evaluate a term to WHNF.
@@ -290,7 +291,9 @@ caseCon subject ty alts = do
290291
forcedSubject <- keepLifted (forceEval subject)
291292

292293
-- If the subject is undefined, the whole expression is undefined.
293-
case isUndefined forcedSubject of
294+
case isUndefinedX forcedSubject of
295+
True -> eval (TyApp (Prim NP.undefinedX) ty)
296+
False -> case isUndefined forcedSubject of
294297
True -> eval (TyApp (Prim NP.undefined) ty)
295298
False ->
296299
case stripValue forcedSubject of

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,3 +26,9 @@
2626
64 -> Double'
2727
template: ~ARG[0]
2828
workInfo: Never
29+
- BlackBox:
30+
name: Clash.Class.BitPack.Internal.xToBV
31+
kind: Expression
32+
type: 'xToBV :: KnownNat n => BitVector n -> BitVector n'
33+
template: ~ARG[1]
34+
workInfo: Never

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
- BlackBox:
2-
name: EmptyCase
3-
kind: Expression
4-
template: ~ERRORO
5-
workInfo: Constant
61
- Primitive:
72
name: _CO_
83
primType: Constructor

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,12 @@
1111
a . a'
1212
template: ~ERRORO
1313
workInfo: Constant
14+
- BlackBox:
15+
name: Clash.Normalize.Primitives.undefinedX
16+
kind: Expression
17+
type: 'undefinedX :: forall a . a'
18+
template: ~ERRORO
19+
workInfo: Constant
1420
- BlackBox:
1521
name: c$multiPrimSelect
1622
kind: Expression

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

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
{-|
2-
Copyright : (C) 2020-2021, QBayLogic B.V.
2+
Copyright : (C) 2020-2021, QBayLogic B.V.,
3+
2022 , Google Inc.
34
License : BSD2 (see the file LICENSE)
45
Maintainer : QBayLogic B.V. <[email protected]>
56
@@ -24,6 +25,7 @@ module Clash.Core.PartialEval.NormalForm
2425
, stripValue
2526
, collectValueTicks
2627
, isUndefined
28+
, isUndefinedX
2729
, Normal(..)
2830
, LocalEnv(..)
2931
, GlobalEnv(..)
@@ -40,7 +42,7 @@ import Clash.Core.Literal
4042
import Clash.Core.Term (Bind, Term(..), PrimInfo(primName), TickInfo, Pat)
4143
import Clash.Core.TyCon (TyConMap)
4244
import Clash.Core.Type (Type, TyVar)
43-
import Clash.Core.Util (undefinedPrims)
45+
import Clash.Core.Util (undefinedPrims, undefinedXPrims)
4446
import Clash.Core.Var (Id)
4547
import Clash.Core.VarEnv (VarEnv, InScopeSet)
4648
import Clash.Driver.Types (Binding(..))
@@ -127,6 +129,13 @@ isUndefined = \case
127129

128130
_ -> False
129131

132+
isUndefinedX :: Value -> Bool
133+
isUndefinedX = \case
134+
VNeutral (NePrim pr _) ->
135+
primName pr `elem` undefinedXPrims
136+
137+
_ -> False
138+
130139
-- | A term which is in beta-normal eta-long form (NF). This has no redexes,
131140
-- and all partially applied functions in sub-terms are eta-expanded.
132141
--

0 commit comments

Comments
 (0)