    {-
    Module           : What4.Utils.Process
    Copyright        : (c) Galois, Inc 2014-2020
    License          : BSD3
    Maintainer       : Rob Dockins <rdockins@galois.com>

    Common utilities for running solvers and getting back results.
    -}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    module What4.Utils.Process
      ( withProcessHandles
      , resolveSolverPath
      , findSolverPath
      , filterAsync
      , startProcess
      , cleanupProcess
      ) where

    import           Control.Exception
    import           Control.Monad (void)
    import qualified Data.Map as Map
    import qualified Data.Text as T
    import           System.IO
    import           System.Exit (ExitCode)
    import           System.Process hiding (cleanupProcess)

    import           What4.BaseTypes
    import           What4.Config
    import qualified What4.Utils.Environment as Env
    import           What4.Panic

    -- | Utility function that runs a solver specified by the given
    -- config setting within a context.  Errors can then be attributed
    -- to the solver.
    resolveSolverPath :: FilePath
                   -> IO FilePath
    resolveSolverPath :: [Char] -> IO [Char]
    resolveSolverPath [Char]
    path = do
      [Char] -> IO [Char]
    forall (m :: Type -> Type).
    (MonadIO m, MonadFail m) =>
    [Char] -> m [Char]
    Env.findExecutable ([Char] -> IO [Char]) -> IO [Char] -> IO [Char]
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Map [Char] [Char] -> [Char] -> IO [Char]
    Env.expandEnvironmentPath Map [Char] [Char]
    forall k a. Map k a
    Map.empty [Char]
    path

    findSolverPath :: ConfigOption (BaseStringType Unicode) -> Config -> IO FilePath
    findSolverPath :: ConfigOption (BaseStringType Unicode) -> Config -> IO [Char]
    findSolverPath ConfigOption (BaseStringType Unicode)
    o Config
    cfg =
      do v <- OptionSetting (BaseStringType Unicode) -> IO Text
    forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
    getOpt (OptionSetting (BaseStringType Unicode) -> IO Text)
    -> IO (OptionSetting (BaseStringType Unicode)) -> IO Text
    forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConfigOption (BaseStringType Unicode)
    -> Config -> IO (OptionSetting (BaseStringType Unicode))
    forall (tp :: BaseType).
    ConfigOption tp -> Config -> IO (OptionSetting tp)
    getOptionSetting ConfigOption (BaseStringType Unicode)
    o Config
    cfg
         resolveSolverPath (T.unpack v)

    -- | This runs a given external binary, providing the process handle and handles to
    -- input and output to the action.  It takes care to terminate the process if any
    -- exception is thrown by the action.
    withProcessHandles :: FilePath -- ^ Path to process
                       -> [String] -- ^ Arguments to process
                       -> Maybe FilePath -- ^ Working directory if any.
                       -> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
                          -- ^ Action to run with process; should wait for process to terminate
                          -- before returning.
                       -> IO a
    withProcessHandles :: forall a.
    [Char]
    -> [[Char]]
    -> Maybe [Char]
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
    -> IO a
    withProcessHandles [Char]
    path [[Char]]
    args Maybe [Char]
    mcwd (Handle, Handle, Handle, ProcessHandle) -> IO a
    action = do
      let onError :: (a, b, c, ProcessHandle) -> IO ()
    onError (a
    _,b
    _,c
    _,ProcessHandle
    ph) = do
            -- Interrupt process; suppress any exceptions that occur.
            (SomeException -> Maybe SomeException)
    -> IO () -> (SomeException -> IO ()) -> IO ()
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    catchJust SomeException -> Maybe SomeException
    filterAsync (ProcessHandle -> IO ()
    terminateProcess ProcessHandle
    ph) (\(SomeException
    ex :: SomeException) ->
              Handle -> [Char] -> IO ()
    hPutStrLn Handle
    stderr ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ SomeException -> [Char]
    forall e. Exception e => e -> [Char]
    displayException SomeException
    ex)

      IO (Handle, Handle, Handle, ProcessHandle)
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO ())
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
    -> IO a
    forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
    bracket ([Char]
    -> [[Char]]
    -> Maybe [Char]
    -> IO (Handle, Handle, Handle, ProcessHandle)
    startProcess [Char]
    path [[Char]]
    args Maybe [Char]
    mcwd)
              (IO ExitCode -> IO ()
    forall (f :: Type -> Type) a. Functor f => f a -> f ()
    void (IO ExitCode -> IO ())
    -> ((Handle, Handle, Handle, ProcessHandle) -> IO ExitCode)
    -> (Handle, Handle, Handle, ProcessHandle)
    -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
    cleanupProcess)
              (\(Handle, Handle, Handle, ProcessHandle)
    hs -> IO a -> IO () -> IO a
    forall a b. IO a -> IO b -> IO a
    onException ((Handle, Handle, Handle, ProcessHandle) -> IO a
    action (Handle, Handle, Handle, ProcessHandle)
    hs) ((Handle, Handle, Handle, ProcessHandle) -> IO ()
    forall {a} {b} {c}. (a, b, c, ProcessHandle) -> IO ()
    onError (Handle, Handle, Handle, ProcessHandle)
    hs))

    -- | Close the connected process pipes and wait for the process to exit
    cleanupProcess :: (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
    cleanupProcess :: (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
    cleanupProcess (Handle
    h_in, Handle
    h_out, Handle
    h_err, ProcessHandle
    ph) =
     do (SomeException -> Maybe SomeException)
    -> IO () -> (SomeException -> IO ()) -> IO ()
    forall e b a.
    Exception e =>
    (e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
    catchJust SomeException -> Maybe SomeException
    filterAsync
             (Handle -> IO ()
    hClose Handle
    h_in IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Handle -> IO ()
    hClose Handle
    h_out IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
    >> Handle -> IO ()
    hClose Handle
    h_err)
             (\(SomeException
    _ :: SomeException) -> () -> IO ()
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ())
        ProcessHandle -> IO ExitCode
    waitForProcess ProcessHandle
    ph

    -- | Start a process connected to this one via pipes.
    startProcess ::
      FilePath {-^ Path to executable -} ->
      [String] {-^ Command-line arguments -} ->
      Maybe FilePath {-^ Optional working directory -} ->
      IO (Handle, Handle, Handle, ProcessHandle)
      {-^ process stdin, process stdout, process stderr, process handle -}
    startProcess :: [Char]
    -> [[Char]]
    -> Maybe [Char]
    -> IO (Handle, Handle, Handle, ProcessHandle)
    startProcess [Char]
    path [[Char]]
    args Maybe [Char]
    mcwd =
      do let create_proc :: CreateProcess
    create_proc
                = ([Char] -> [[Char]] -> CreateProcess
    proc [Char]
    path [[Char]]
    args)
                  { std_in  = CreatePipe
                  , std_out = CreatePipe
                  , std_err = CreatePipe
                  , create_group = False
                  , cwd = mcwd
                  , delegate_ctlc = True
                  }
         CreateProcess
    -> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    createProcess CreateProcess
    create_proc IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    -> ((Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
        -> IO (Handle, Handle, Handle, ProcessHandle))
    -> IO (Handle, Handle, Handle, ProcessHandle)
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
           (Just Handle
    in_h, Just Handle
    out_h, Just Handle
    err_h, ProcessHandle
    ph) -> (Handle, Handle, Handle, ProcessHandle)
    -> IO (Handle, Handle, Handle, ProcessHandle)
    forall a. a -> IO a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return (Handle
    in_h, Handle
    out_h, Handle
    err_h, ProcessHandle
    ph)
           (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
    _ -> [Char] -> [[Char]] -> IO (Handle, Handle, Handle, ProcessHandle)
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "startProcess" ([[Char]] -> IO (Handle, Handle, Handle, ProcessHandle))
    -> [[Char]] -> IO (Handle, Handle, Handle, ProcessHandle)
    forall a b. (a -> b) -> a -> b
    $
                   [ [Char]
    "Failed to exec: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [Char]
    forall a. Show a => a -> [Char]
    show [Char]
    path
                   , [Char]
    "With the following arguments:"
                   ] [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]]
    args

    -- | Filtering function for use with `catchJust` or `tryJust`
    --   that filters out async exceptions so they are rethrown
    --   instead of captured
    filterAsync :: SomeException -> Maybe SomeException
    filterAsync :: SomeException -> Maybe SomeException
    filterAsync SomeException
    e
      | Just (AsyncException
    _ :: AsyncException) <- SomeException -> Maybe AsyncException
    forall e. Exception e => SomeException -> Maybe e
    fromException SomeException
    e = Maybe SomeException
    forall a. Maybe a
    Nothing
      | Bool
    otherwise = SomeException -> Maybe SomeException
    forall a. a -> Maybe a
    Just SomeException
    e