{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Plugin.Plugin(plugin) where
import GHC.Plugins
import System.Exit
import Data.Maybe (fromJust)
import Data.List (sortBy)
import Data.Bits (bitSizeMaybe)
import Data.IORef
import qualified Data.Map as M
import Data.SBV.Plugin.Common
import Data.SBV.Plugin.Env
import Data.SBV.Plugin.Analyze (analyzeBind)
plugin :: Plugin
plugin :: Plugin
plugin = Plugin
defaultPlugin {installCoreToDos :: CorePlugin
installCoreToDos = CorePlugin
install}
where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
install :: CorePlugin
install [] [CoreToDo]
todos = [CoreToDo] -> CoreM [CoreToDo]
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreToDo
sbvPass CoreToDo -> [CoreToDo] -> [CoreToDo]
forall a. a -> [a] -> [a]
: [CoreToDo]
todos)
install [CommandLineOption
"skip"] [CoreToDo]
todos = [CoreToDo] -> CoreM [CoreToDo]
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreToDo]
todos
install [CommandLineOption
"runLast"] [CoreToDo]
todos = [CoreToDo] -> CoreM [CoreToDo]
forall (m :: * -> *) a. Monad m => a -> m a
return ([CoreToDo]
todos [CoreToDo] -> [CoreToDo] -> [CoreToDo]
forall a. [a] -> [a] -> [a]
++ [CoreToDo
sbvPass])
install [CommandLineOption]
opts [CoreToDo]
_ = do IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption
"[SBV] Unexpected command line options: " CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ [CommandLineOption] -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show [CommandLineOption]
opts
IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn CommandLineOption
""
IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn CommandLineOption
"Options:"
IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn CommandLineOption
" skip (does not run the plugin)"
IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO ()
putStrLn CommandLineOption
" runLast (run the SBVPlugin last in the pipeline)"
IO [CoreToDo] -> CoreM [CoreToDo]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [CoreToDo]
forall a. IO a
exitFailure
sbvPass :: CoreToDo
sbvPass = CommandLineOption -> CorePluginPass -> CoreToDo
CoreDoPluginPass CommandLineOption
"SBV based analysis" CorePluginPass
pass
pass :: ModGuts -> CoreM ModGuts
pass :: CorePluginPass
pass guts :: ModGuts
guts@ModGuts{CoreProgram
mg_binds :: ModGuts -> CoreProgram
mg_binds :: CoreProgram
mg_binds} = do
DynFlags
df <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
NameEnv [SBVAnnotation]
anns <- (ModuleEnv [SBVAnnotation], NameEnv [SBVAnnotation])
-> NameEnv [SBVAnnotation]
forall a b. (a, b) -> b
snd ((ModuleEnv [SBVAnnotation], NameEnv [SBVAnnotation])
-> NameEnv [SBVAnnotation])
-> CoreM (ModuleEnv [SBVAnnotation], NameEnv [SBVAnnotation])
-> CoreM (NameEnv [SBVAnnotation])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Word8] -> SBVAnnotation)
-> ModGuts
-> CoreM (ModuleEnv [SBVAnnotation], NameEnv [SBVAnnotation])
forall a.
Typeable a =>
([Word8] -> a) -> ModGuts -> CoreM (ModuleEnv [a], NameEnv [a])
getAnnotations [Word8] -> SBVAnnotation
forall a. Data a => [Word8] -> a
deserializeWithData ModGuts
guts
let wsz :: Int
wsz = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Int -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe (Int
0::Int))
Map TCKey Kind
baseTCs <- Int -> CoreM (Map TCKey Kind)
buildTCEnv Int
wsz
Map (Id, SKind) Val
baseEnv <- Int -> CoreM (Map (Id, SKind) Val)
buildFunEnv Int
wsz
Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
baseDests <- CoreM
(Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)])))
buildDests
[Type]
uninteresting <- CoreM [Type]
uninterestingTypes
Specials
specials <- CoreM Specials
buildSpecials
IORef [((Id, Type), (Bool, CommandLineOption, Val))]
rUninterpreted <- IO (IORef [((Id, Type), (Bool, CommandLineOption, Val))])
-> CoreM (IORef [((Id, Type), (Bool, CommandLineOption, Val))])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef [((Id, Type), (Bool, CommandLineOption, Val))])
-> CoreM (IORef [((Id, Type), (Bool, CommandLineOption, Val))]))
-> IO (IORef [((Id, Type), (Bool, CommandLineOption, Val))])
-> CoreM (IORef [((Id, Type), (Bool, CommandLineOption, Val))])
forall a b. (a -> b) -> a -> b
$ [((Id, Type), (Bool, CommandLineOption, Val))]
-> IO (IORef [((Id, Type), (Bool, CommandLineOption, Val))])
forall a. a -> IO (IORef a)
newIORef []
IORef [CommandLineOption]
rUsedNames <- IO (IORef [CommandLineOption]) -> CoreM (IORef [CommandLineOption])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef [CommandLineOption])
-> CoreM (IORef [CommandLineOption]))
-> IO (IORef [CommandLineOption])
-> CoreM (IORef [CommandLineOption])
forall a b. (a -> b) -> a -> b
$ [CommandLineOption] -> IO (IORef [CommandLineOption])
forall a. a -> IO (IORef a)
newIORef []
IORef [(Type, Kind)]
rUITypes <- IO (IORef [(Type, Kind)]) -> CoreM (IORef [(Type, Kind)])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef [(Type, Kind)]) -> CoreM (IORef [(Type, Kind)]))
-> IO (IORef [(Type, Kind)]) -> CoreM (IORef [(Type, Kind)])
forall a b. (a -> b) -> a -> b
$ [(Type, Kind)] -> IO (IORef [(Type, Kind)])
forall a. a -> IO (IORef a)
newIORef []
let cfg :: Config
cfg = Config { isGHCi :: Bool
isGHCi = DynFlags -> GhcMode
ghcMode DynFlags
df GhcMode -> GhcMode -> Bool
forall a. Eq a => a -> a -> Bool
== GhcMode
CompManager
, opts :: [SBVAnnotation]
opts = []
, sbvAnnotation :: Id -> [SBVAnnotation]
sbvAnnotation = NameEnv [SBVAnnotation]
-> [SBVAnnotation] -> Name -> [SBVAnnotation]
forall key elt.
Uniquable key =>
UniqFM key elt -> elt -> key -> elt
lookupWithDefaultUFM NameEnv [SBVAnnotation]
anns [] (Name -> [SBVAnnotation]) -> (Id -> Name) -> Id -> [SBVAnnotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Name
varName
, cfgEnv :: Env
cfgEnv = Env { curLoc :: [SrcSpan]
curLoc = []
, flags :: DynFlags
flags = DynFlags
df
, machWordSize :: Int
machWordSize = Int
wsz
, mbListSize :: Maybe Int
mbListSize = Maybe Int
forall a. Maybe a
Nothing
, uninteresting :: [Type]
uninteresting = [Type]
uninteresting
, rUninterpreted :: IORef [((Id, Type), (Bool, CommandLineOption, Val))]
rUninterpreted = IORef [((Id, Type), (Bool, CommandLineOption, Val))]
rUninterpreted
, rUsedNames :: IORef [CommandLineOption]
rUsedNames = IORef [CommandLineOption]
rUsedNames
, rUITypes :: IORef [(Type, Kind)]
rUITypes = IORef [(Type, Kind)]
rUITypes
, specials :: Specials
specials = Specials
specials
, tcMap :: Map TCKey Kind
tcMap = Map TCKey Kind
baseTCs
, envMap :: Map (Id, SKind) Val
envMap = Map (Id, SKind) Val
baseEnv
, destMap :: Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
destMap = Map Id (Val -> [(Id, SKind)] -> (SVal, [((Id, SKind), Val)]))
baseDests
, bailOut :: forall a. CommandLineOption -> [CommandLineOption] -> Eval a
bailOut = \CommandLineOption
s [CommandLineOption]
ss -> CommandLineOption -> Eval a
forall a. HasCallStack => CommandLineOption -> a
error (CommandLineOption -> Eval a) -> CommandLineOption -> Eval a
forall a b. (a -> b) -> a -> b
$ [CommandLineOption] -> CommandLineOption
unlines (CommandLineOption
sCommandLineOption -> [CommandLineOption] -> [CommandLineOption]
forall a. a -> [a] -> [a]
:[CommandLineOption]
ss)
, coreMap :: Map Id (SrcSpan, CoreExpr)
coreMap = [(Id, (SrcSpan, CoreExpr))] -> Map Id (SrcSpan, CoreExpr)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Id
b, (Id -> SrcSpan
varSpan Id
b, CoreExpr
e)) | (Id
b, CoreExpr
e) <- CoreProgram -> [(Id, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds CoreProgram
mg_binds]
}
}
let bindLoc :: Bind Id -> SrcSpan
bindLoc (NonRec Id
b CoreExpr
_) = Id -> SrcSpan
varSpan Id
b
bindLoc (Rec []) = SrcSpan
noSrcSpan
bindLoc (Rec ((Id
b, CoreExpr
_):[(Id, CoreExpr)]
_)) = Id -> SrcSpan
varSpan Id
b
cmp :: Bind Id -> Bind Id -> Ordering
cmp Bind Id
a Bind Id
b = Bind Id -> SrcSpan
bindLoc Bind Id
a SrcSpan -> SrcSpan -> Ordering
`leftmost_smallest` Bind Id -> SrcSpan
bindLoc Bind Id
b
(Bind Id -> CoreM ()) -> CoreProgram -> CoreM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Config -> Bind Id -> CoreM ()
analyzeBind Config
cfg) (CoreProgram -> CoreM ()) -> CoreProgram -> CoreM ()
forall a b. (a -> b) -> a -> b
$ (Bind Id -> Bind Id -> Ordering) -> CoreProgram -> CoreProgram
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy Bind Id -> Bind Id -> Ordering
cmp CoreProgram
mg_binds
CorePluginPass
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
guts