refineFromInScope panic with -O2 on GHC 9.2.5/9.4.3 (but not on 9.2.4/9.4.2)
The saw-script repository panics when built with GHC 9.2.5, but not with GHC 9.2.4. Here is a somewhat minimal reproducer with no external dependencies:
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module SAWScript.HeapsterBuiltins (heapster_add_block_hints) where
import qualified Control.Exception as X
import Control.Applicative
import Control.Monad
import Control.Monad.Catch (MonadThrow(..), MonadCatch(..), catches, Handler(..))
import Control.Monad.IO.Class
import qualified Control.Monad.Fail as Fail
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.Reader (ReaderT)
import Data.Coerce (Coercible, coerce)
import Data.IORef
import Data.Kind (Type)
import Data.Monoid
import GHC.Exts (build)
failOnNothing :: Fail.MonadFail m => String -> Maybe a -> m a
failOnNothing err_str Nothing = Fail.fail err_str
failOnNothing _ (Just a) = return a
lookupLLVMSymbolModAndCFG :: HeapsterEnv -> String -> IO (Maybe (AnyCFG LLVM))
lookupLLVMSymbolModAndCFG _ _ = pure Nothing
heapster_add_block_hints :: HeapsterEnv -> String -> [Int] ->
(forall ext blocks ret.
CFG ext blocks ret ->
TopLevel Hint) ->
TopLevel ()
heapster_add_block_hints henv nm blks hintF =
do env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv
AnyCFG cfg <-
failOnNothing ("Could not find symbol definition: " ++ nm) =<<
io (lookupLLVMSymbolModAndCFG henv nm)
let blocks = fmapFC blockInputs $ cfgBlockMap cfg
block_idxs = fmapFC (blockIDIndex . blockID) $ cfgBlockMap cfg
blkIDs <- case blks of
[] -> pure $ toListFC (Some . BlockID) block_idxs
_ -> forM blks $ \blk ->
failOnNothing ("Block ID " ++ show blk ++
" not found in function " ++ nm)
(fmapF BlockID <$> intIndex blk (size blocks))
env' <- foldM (\env' _ ->
permEnvAddHint env' <$>
hintF cfg)
env blkIDs
liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
-----
data Some (f:: k -> Type) = forall x . Some (f x)
class FunctorF m where
fmapF :: (forall x . f x -> g x) -> m f -> m g
mapSome :: (forall tp . f tp -> g tp) -> Some f -> Some g
mapSome f (Some x) = Some $! f x
instance FunctorF Some where fmapF = mapSome
type SingleCtx x = EmptyCtx ::> x
data Ctx k
= EmptyCtx
| Ctx k ::> k
type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where
x <+> EmptyCtx = x
x <+> (y ::> e) = (x <+> y) ::> e
data Height = Zero | Succ Height
data BalancedTree h (f :: k -> Type) (p :: Ctx k) where
BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)
BalPair :: !(BalancedTree h f x)
-> !(BalancedTree h f y)
-> BalancedTree ('Succ h) f (x <+> y)
data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
Empty :: BinomialTree h f EmptyCtx
PlusOne :: !Int
-> !(BinomialTree ('Succ h) f x)
-> !(BalancedTree h f y)
-> BinomialTree h f (x <+> y)
PlusZero :: !Int
-> !(BinomialTree ('Succ h) f x)
-> BinomialTree h f x
tsize :: BinomialTree h f a -> Int
tsize Empty = 0
tsize (PlusOne s _ _) = 2*s+1
tsize (PlusZero s _) = 2*s
fmap_bin :: (forall tp . f tp -> g tp)
-> BinomialTree h f c
-> BinomialTree h g c
fmap_bin _ Empty = Empty
fmap_bin f (PlusOne s t x) = PlusOne s (fmap_bin f t) (fmap_bal f x)
fmap_bin f (PlusZero s t) = PlusZero s (fmap_bin f t)
{-# INLINABLE fmap_bin #-}
fmap_bal :: (forall tp . f tp -> g tp)
-> BalancedTree h f c
-> BalancedTree h g c
fmap_bal = go
where go :: (forall tp . f tp -> g tp)
-> BalancedTree h f c
-> BalancedTree h g c
go f (BalLeaf x) = BalLeaf (f x)
go f (BalPair x y) = BalPair (go f x) (go f y)
{-# INLINABLE fmap_bal #-}
traverse_bin :: Applicative m
=> (forall tp . f tp -> m (g tp))
-> BinomialTree h f c
-> m (BinomialTree h g c)
traverse_bin _ Empty = pure Empty
traverse_bin f (PlusOne s t x) = PlusOne s <$> traverse_bin f t <*> traverse_bal f x
traverse_bin f (PlusZero s t) = PlusZero s <$> traverse_bin f t
{-# INLINABLE traverse_bin #-}
traverse_bal :: Applicative m
=> (forall tp . f tp -> m (g tp))
-> BalancedTree h f c
-> m (BalancedTree h g c)
traverse_bal = go
where go :: Applicative m
=> (forall tp . f tp -> m (g tp))
-> BalancedTree h f c
-> m (BalancedTree h g c)
go f (BalLeaf x) = BalLeaf <$> f x
go f (BalPair x y) = BalPair <$> go f x <*> go f y
{-# INLINABLE traverse_bal #-}
data Assignment (f :: k -> Type) (ctx :: Ctx k)
= Assignment (BinomialTree 'Zero f ctx)
newtype Index (ctx :: Ctx k) (tp :: k) = Index { indexVal :: Int }
newtype Size (ctx :: Ctx k) = Size Int
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i))
| otherwise = Nothing
size :: Assignment f ctx -> Size ctx
size (Assignment t) = Size (tsize t)
sizeInt :: Size ctx -> Int
sizeInt (Size n) = n
class FunctorFC (t :: (k -> Type) -> l -> Type) where
fmapFC :: forall f g. (forall x. f x -> g x) ->
(forall x. t f x -> t g x)
(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
(#.) _f = coerce
class FoldableFC (t :: (k -> Type) -> l -> Type) where
foldMapFC :: forall f m. Monoid m => (forall x. f x -> m) -> (forall x. t f x -> m)
foldMapFC f = foldrFC (mappend . f) mempty
foldrFC :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)
foldrFC f z t = appEndo (foldMapFC (Endo #. f) t) z
toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])
toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t)
foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m)
foldMapFCDefault = \f -> getConst . traverseFC (Const . f)
{-# INLINE foldMapFCDefault #-}
class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> Type) -> l -> Type) where
traverseFC :: forall f g m. Applicative m
=> (forall x. f x -> m (g x))
-> (forall x. t f x -> m (t g x))
instance FunctorFC Assignment where
fmapFC = \f (Assignment x) -> Assignment (fmap_bin f x)
{-# INLINE fmapFC #-}
instance FoldableFC Assignment where
foldMapFC = foldMapFCDefault
{-# INLINE foldMapFC #-}
instance TraversableFC Assignment where
traverseFC = \f (Assignment x) -> Assignment <$> traverse_bin f x
{-# INLINE traverseFC #-}
data CrucibleType
data TypeRepr (tp::CrucibleType) where
type CtxRepr = Assignment TypeRepr
data CFG (ext :: Type)
(blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType)
= CFG { cfgBlockMap :: !(BlockMap ext blocks ret)
}
type BlockMap ext blocks ret = Assignment (Block ext blocks ret) blocks
data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ctx
= Block { blockID :: !(BlockID blocks ctx)
, blockInputs :: !(CtxRepr ctx)
}
newtype BlockID (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType)
= BlockID { blockIDIndex :: Index blocks tp }
data LLVM
data AnyCFG ext where
AnyCFG :: CFG ext blocks ret
-> AnyCFG ext
newtype StateContT s r m a
= StateContT { runStateContT :: (a -> s -> m r)
-> s
-> m r
}
fmapStateContT :: (a -> b) -> StateContT s r m a -> StateContT s r m b
fmapStateContT = \f m -> StateContT $ \c -> runStateContT m (\v s -> (c $! f v) s)
{-# INLINE fmapStateContT #-}
applyStateContT :: StateContT s r m (a -> b) -> StateContT s r m a -> StateContT s r m b
applyStateContT = \mf mv ->
StateContT $ \c ->
runStateContT mf (\f -> runStateContT mv (\v s -> (c $! f v) s))
{-# INLINE applyStateContT #-}
returnStateContT :: a -> StateContT s r m a
returnStateContT = \v -> seq v $ StateContT $ \c -> c v
{-# INLINE returnStateContT #-}
bindStateContT :: StateContT s r m a -> (a -> StateContT s r m b) -> StateContT s r m b
bindStateContT = \m n -> StateContT $ \c -> runStateContT m (\a -> runStateContT (n a) c)
{-# INLINE bindStateContT #-}
instance Functor (StateContT s r m) where
fmap = fmapStateContT
instance Applicative (StateContT s r m) where
pure = returnStateContT
(<*>) = applyStateContT
instance Monad (StateContT s r m) where
(>>=) = bindStateContT
instance MonadFail m => MonadFail (StateContT s r m) where
fail = \msg -> StateContT $ \_ _ -> fail msg
instance MonadTrans (StateContT s r) where
lift = \m -> StateContT $ \c s -> m >>= \v -> seq v (c v s)
instance MonadIO m => MonadIO (StateContT s r m) where
liftIO = lift . liftIO
instance MonadThrow m => MonadThrow (StateContT s r m) where
throwM e = StateContT (\_k _s -> throwM e)
instance MonadCatch m => MonadCatch (StateContT s r m) where
catch m hdl =
StateContT $ \k s ->
catch
(runStateContT m k s)
(\e -> runStateContT (hdl e) k s)
data TopLevelRO
data TopLevelRW
data Value
newtype TopLevel a =
TopLevel_ (ReaderT TopLevelRO (StateContT TopLevelRW (Value, TopLevelRW) IO) a)
deriving (Applicative, Functor, Monad, MonadFail, MonadThrow, MonadCatch)
instance MonadIO TopLevel where
liftIO = io
io :: IO a -> TopLevel a
io f = TopLevel_ (liftIO f) `catches` [Handler handleIO]
where
rethrow :: X.Exception ex => ex -> TopLevel a
rethrow ex = throwM (X.SomeException ex)
handleIO :: X.IOException -> TopLevel a
handleIO = rethrow
data HeapsterEnv = HeapsterEnv {
heapsterEnvPermEnvRef :: IORef PermEnv
}
data Hint where
data PermEnv = PermEnv {
permEnvHints :: [Hint]
}
permEnvAddHint :: PermEnv -> Hint -> PermEnv
permEnvAddHint env hint = env { permEnvHints = hint : permEnvHints env }
type family CtxToRList (ctx :: Ctx k) :: RList k where
CtxToRList EmptyCtx = RNil
CtxToRList (ctx' ::> x) = CtxToRList ctx' :> x
data RList a
= RNil
| (RList a) :> aThis will panic when built with -O2 using GHC 9.2.5 or 9.4.3:
$ ghc-9.2.5 Bug.hs -O2 -fforce-recomp
[1 of 1] Compiling SAWScript.HeapsterBuiltins ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 9.2.5:
refineFromInScope
InScope {wild_00 eta_B0 eta_B1 eta_B2 eta_B3 eta_X3 eta_X4 eta_Xb
eta_Xc eta_Xd a_Xk eta_Xl eta_Xm wild_Xo v_Xp exit_Xr a_Xs eta_Xt
a_a128 henv_a129 nm_a12a blks_a12b hintF_a12c a_a1tQ
$cp1MonadCatch_a345 $cliftIO_a35g $c>>_a36S $cfoldrFC_a3a4
$ctoListFC_a3ap $cfmapF_a3ba $krep_a5fW $krep_a5fY $krep_a5fZ
$krep_a5g0 $krep_a5g1 $krep_a5g2 $krep_a5g3 $krep_a5g4 $krep_a5g5
$krep_a5g6 $krep_a5g7 $krep_a5g8 $krep_a5g9 $krep_a5ga $krep_a5gb
$krep_a5gc $krep_a5gd $krep_a5ge $krep_a5gf $krep_a5gg $krep_a5gh
$krep_a5gi $krep_a5gj $krep_a5gk $krep_a5gl $krep_a5gm $krep_a5go
$krep_a5gq $krep_a5gr $krep_a5gs $krep_a5gt $krep_a5gu $krep_a5gv
$krep_a5gy $krep_a5gz $krep_a5gA $krep_a5gB $krep_a5gC $krep_a5gD
$krep_a5gE $krep_a5gF $krep_a5gG $krep_a5gH $krep_a5gI $krep_a5gJ
$krep_a5gK $krep_a5gL $krep_a5gM $krep_a5gN $krep_a5gP $krep_a5gQ
$krep_a5gR $krep_a5gS $krep_a5gT $krep_a5gU $krep_a5gW $krep_a5gX
$krep_a5gY $krep_a5gZ $krep_a5h1 $krep_a5h2 $krep_a5h3 $krep_a5h4
$krep_a5h5 $krep_a5h6 $krep_a5h7 $krep_a5h8 $krep_a5h9 $krep_a5ha
$krep_a5hc $krep_a5hd $krep_a5he $krep_a5hf $krep_a5hg $krep_a5hh
$krep_a5hi $krep_a5hl $krep_a5hm $krep_a5hn $krep_a5ho $krep_a5hr
$krep_a5hs $krep_a5ht $krep_a5hu $krep_a5hv $krep_a5hx $krep_a5hy
$krep_a5hz $krep_a5hA $krep_a5hB $krep_a5hC $krep_a5hD $krep_a5hE
$krep_a5hF $krep_a5hG $krep_a5hH $krep_a5hI r1_a5BO e1_a5E3
eta1_a5E4 permEnvHints heapsterEnvPermEnvRef runStateContT
blockIDIndex blockID blockInputs cfgBlockMap indexVal
heapster_add_block_hints fmap_bin fmap_bal traverse_bin
traverse_bal $tc'Some $tcSome $tcFunctorF $fFunctorFkSome
$tc'EmptyCtx $tc'::> $tcCtx $tc'Zero $tc'Succ $tcHeight $tc'BalLeaf
$tcBalancedTree $tc'Empty $tc'PlusZero $tcBinomialTree
$tc'Assignment $tcAssignment $tc'Index $tcIndex $tc'Size $tcSize
$tcFunctorFC $fFunctorFCkCtxAssignment $tcFoldableFC $dmfoldMapFC
$dmfoldrFC $dmtoListFC $fFoldableFCkCtxAssignment $tcTraversableFC
$fTraversableFCkCtxAssignment $tcCrucibleType $tcTypeRepr
$tc'BlockID $tcBlockID $tc'Block $tcBlock $tc'CFG $tcCFG $tcLLVM
$tc'AnyCFG $tcAnyCFG $tc'StateContT $tcStateContT
$fMonadCatchStateContT $fMonadThrowStateContT $fMonadIOStateContT
$fMonadTransStateContT $fMonadFailStateContT $fMonadStateContT
$fApplicativeStateContT $fFunctorStateContT $tcTopLevelRO
$tcTopLevelRW $tcValue $tc'TopLevel_ $tcTopLevel $fMonadIOTopLevel
$tcHint $tc'PermEnv $tcPermEnv $tc'HeapsterEnv $tcHeapsterEnv
$tc'RNil $tc':> $tcRList $fApplicativeTopLevel $fFunctorTopLevel
$fMonadTopLevel $fMonadFailTopLevel $fMonadThrowTopLevel
$fMonadCatchTopLevel $trModule $clift_s5zq indexVal_s5zu
blockIDIndex_s5zv runStateContT_s5zw $ccatch_s5zx go_s5zy
$fTraversableFCkCtxAssignment_s5zH
$fTraversableFCkCtxAssignment_s5zI $fFunctorStateContT_s5A1
$c<$_s5A2 $fApplicativeStateContT_s5At $fApplicativeStateContT_s5Au
$fMonadStateContT_s5BE $creturn_s5BG $c>>_s5C9 $trModule_s5El
$trModule_s5Em $trModule_s5En $trModule_s5Eo $tcSome_s5EI
$tcSome_s5EJ $krep_s5EK $tc'Some_s5EM $tc'Some_s5EN
$tcFunctorF_s5EO $tcFunctorF_s5EP $tcCtx_s5EQ $tcCtx_s5ER
$krep_s5ES $tc'EmptyCtx_s5ET $tc'EmptyCtx_s5EU $tc'::>_s5EW
$tc'::>_s5EX $krep_s5EY $krep_s5EZ $krep_s5F0 $tcHeight_s5F1
$tcHeight_s5F2 $tc'Zero_s5F3 $tc'Zero_s5F4 $tc'Succ_s5F5
$tc'Succ_s5F6 $tcBalancedTree_s5F8 $tcBalancedTree_s5F9 $krep_s5Fa
$krep_s5Fb $krep_s5Fc $krep_s5Fd $tc'BalLeaf_s5Fe $tc'BalLeaf_s5Ff
$tcBinomialTree_s5Fg $tcBinomialTree_s5Fh $krep_s5Fi $krep_s5Fj
$krep_s5Fk $krep_s5Fl $krep_s5Fm $krep_s5Fn $krep_s5Fo $krep_s5Fp
$tc'Empty_s5Fq $tc'Empty_s5Fr $krep_s5Fu $krep_s5Fv
$tc'PlusZero_s5Fw $tc'PlusZero_s5Fx $krep_s5FA $krep_s5FB
$tcAssignment_s5FC $tcAssignment_s5FD $krep_s5FG
$tc'Assignment_s5FH $tc'Assignment_s5FI $tcIndex_s5FJ $tcIndex_s5FK
$krep_s5FM $tc'Index_s5FO $tc'Index_s5FP $tcSize_s5FQ $tcSize_s5FR
$tc'Size_s5FU $tc'Size_s5FV $tcFunctorFC_s5FW $tcFunctorFC_s5FX
$tcFoldableFC_s5FY $tcFoldableFC_s5FZ $tcTraversableFC_s5G0
$tcTraversableFC_s5G1 $tcCrucibleType_s5G2 $tcCrucibleType_s5G3
$krep_s5G4 $krep_s5G6 $krep_s5G7 $krep_s5G8 $tcTypeRepr_s5G9
$tcTypeRepr_s5Ga $krep_s5Gb $krep_s5Gc $krep_s5Gd $tcBlockID_s5Ge
$tcBlockID_s5Gf $tc'BlockID_s5Gi $tc'BlockID_s5Gj $krep_s5Gl
$tcBlock_s5Gm $tcBlock_s5Gn $krep_s5Gr $krep_s5Gt $krep_s5Gu
$tc'Block_s5GA $tc'Block_s5GB $tcCFG_s5GC $tcCFG_s5GD $tc'CFG_s5GH
$tc'CFG_s5GI $tcLLVM_s5GJ $tcLLVM_s5GK $tcAnyCFG_s5GL
$tcAnyCFG_s5GM $tc'AnyCFG_s5GO $tc'AnyCFG_s5GP $tcStateContT_s5GQ
$tcStateContT_s5GR $krep_s5GT $krep_s5GU $krep_s5GV $krep_s5GW
$tc'StateContT_s5GX $tc'StateContT_s5GY $tcTopLevelRO_s5GZ
$tcTopLevelRO_s5H0 $tcTopLevelRW_s5H1 $tcTopLevelRW_s5H2
$tcValue_s5H3 $tcValue_s5H4 $krep_s5H5 $krep_s5H6 $krep_s5H7
$krep_s5H8 $krep_s5H9 $krep_s5Ha $krep_s5Hc $krep_s5Hd
$tcTopLevel_s5He $tcTopLevel_s5Hf $tc'TopLevel__s5Hh
$tc'TopLevel__s5Hi $tcHint_s5Hj $tcHint_s5Hk $krep_s5Hl
$tcPermEnv_s5Hm $tcPermEnv_s5Hn $tc'PermEnv_s5Ho $tc'PermEnv_s5Hp
$krep_s5Hq $tcHeapsterEnv_s5Hr $tcHeapsterEnv_s5Hs
$tc'HeapsterEnv_s5Ht $tc'HeapsterEnv_s5Hu $tcRList_s5Hv
$tcRList_s5Hw $tc'RNil_s5Hy $tc'RNil_s5Hz $tc':>_s5HA $tc':>_s5HB
$fFoldableFCkCtxAssignment_s5Po $c*>_s5Pp $cliftA2_s5Pq $c<*_s5Ps
$creturn_s5Pu $cthrowM_s5Pv $ccatch_s5Pw ipv_s5PP ipv_s5PQ ipv_s5PR
$s$fMonadFailStateContT_s5Ro $scatches_s5RP $sfoldlM_s5Se
$s$fMonadFailReaderT_$cfail_s5Sz $s$fMonadReaderT_$c>>=_s5SB
$s$fApplicativeReaderT_$c<*_s5SD $s$fApplicativeReaderT_$c*>_s5SF
$s$fApplicativeReaderT_$cliftA2_s5SH
$s$fApplicativeReaderT_$c<*>_s5SJ $s$fFunctorReaderT_$c<$_s5SN
$s$fFunctorReaderT_$cfmap_s5SP go_s5T6 lvl_s5T7 lvl_s5T8 lvl_s5Tb
lvl_s5Tc lvl_s5Tf eta_s5Tj m1_s5Tn lvl_s5Tp lvl_s5Tq lvl_s5Tx
lvl_s5Ty lvl_s5TB karg_s5U0 io_s5Up lvl_s5Us go1_s5Uz eta_s5UI
$wgo_s5Vj lvl_s5Xj lvl_s5Xk lvl_s5Xl lvl_s5Xm sc_s5Xw sc_s5Xx
sc_s5Xy sg_s5Xz $sgo1_s5XA $sgo1_s5ZU}
eta_B4
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Opt/Simplify/Env.hs:706:30 in ghc:GHC.Core.Opt.Simplify.Env
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabugOn the other hand, this does not panic when built with 9.2.4 or 9.4.2:
$ ghc-9.2.4 Bug.hs -O2 -fforce-recomp
[1 of 1] Compiling SAWScript.HeapsterBuiltins ( Bug.hs, Bug.o )
$ ghc-9.4.2 Bug.hs -O2 -fforce-recomp
[1 of 1] Compiling SAWScript.HeapsterBuiltins ( Bug.hs, Bug.o )