---------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Analyze
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Main entry point to the SBV Plugin
-----------------------------------------------------------------------------

{-# 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)

-- | Entry point to the plugin
plugin :: Plugin
plugin :: Plugin
plugin = Plugin
defaultPlugin {installCoreToDos = install}
 where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
       install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
install []          [CoreToDo]
todos = [CoreToDo] -> CoreM [CoreToDo]
forall a. a -> CoreM a
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 a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return [CoreToDo]
todos
       install [CommandLineOption
"runLast"] [CoreToDo]
todos = [CoreToDo] -> CoreM [CoreToDo]
forall a. a -> CoreM a
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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 :: CoreProgram
mg_binds :: ModGuts -> CoreProgram
mg_binds} = do

          df   <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
          anns <- snd <$> getAnnotations deserializeWithData guts

          let 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))

          baseTCs       <- buildTCEnv  wsz
          baseEnv       <- buildFunEnv wsz
          baseDests     <- buildDests
          uninteresting <- uninterestingTypes
          specials      <- buildSpecials

          rUninterpreted <- liftIO $ newIORef []
          rUsedNames     <- liftIO $ newIORef []
          rUITypes       <- liftIO $ newIORef []

          let 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 (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
a Bind Id
b = Bind Id -> SrcSpan
bindLoc Bind Id
a SrcSpan -> SrcSpan -> Ordering
`leftmost_smallest` Bind Id -> SrcSpan
bindLoc Bind Id
b

          mapM_ (analyzeBind cfg) $ sortBy cmp mg_binds

          return guts