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

          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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 a. IO a -> CoreM a
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 a. a -> CoreM a
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
guts