{-
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 :: FilePath -> IO FilePath
resolveSolverPath FilePath
path = do
  FilePath -> IO FilePath
forall (m :: Type -> Type).
(MonadIO m, MonadFail m) =>
FilePath -> m FilePath
Env.findExecutable (FilePath -> IO FilePath) -> IO FilePath -> IO FilePath
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map FilePath FilePath -> FilePath -> IO FilePath
Env.expandEnvironmentPath Map FilePath FilePath
forall k a. Map k a
Map.empty FilePath
path

findSolverPath :: ConfigOption (BaseStringType Unicode) -> Config -> IO FilePath
findSolverPath :: ConfigOption (BaseStringType Unicode) -> Config -> IO FilePath
findSolverPath ConfigOption (BaseStringType Unicode)
o Config
cfg =
  do Text
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
     FilePath -> IO FilePath
resolveSolverPath (Text -> FilePath
T.unpack Text
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 :: FilePath
-> [FilePath]
-> Maybe FilePath
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles FilePath
path [FilePath]
args Maybe FilePath
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 -> FilePath -> IO ()
hPutStrLn Handle
stderr (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ SomeException -> FilePath
forall e. Exception e => e -> FilePath
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 (FilePath
-> [FilePath]
-> Maybe FilePath
-> IO (Handle, Handle, Handle, ProcessHandle)
startProcess FilePath
path [FilePath]
args Maybe FilePath
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 (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hClose Handle
h_out IO () -> IO () -> IO ()
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hClose Handle
h_err)
         (\(SomeException
_ :: SomeException) -> () -> IO ()
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 :: FilePath
-> [FilePath]
-> Maybe FilePath
-> IO (Handle, Handle, Handle, ProcessHandle)
startProcess FilePath
path [FilePath]
args Maybe FilePath
mcwd =
  do let create_proc :: CreateProcess
create_proc
            = (FilePath -> [FilePath] -> CreateProcess
proc FilePath
path [FilePath]
args)
              { std_in :: StdStream
std_in  = StdStream
CreatePipe
              , std_out :: StdStream
std_out = StdStream
CreatePipe
              , std_err :: StdStream
std_err = StdStream
CreatePipe
              , create_group :: Bool
create_group = Bool
False
              , cwd :: Maybe FilePath
cwd = Maybe FilePath
mcwd
              }
     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 (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 (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)
_ -> FilePath
-> [FilePath] -> IO (Handle, Handle, Handle, ProcessHandle)
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"startProcess" ([FilePath] -> IO (Handle, Handle, Handle, ProcessHandle))
-> [FilePath] -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$
               [ FilePath
"Failed to exec: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
path
               , FilePath
"With the following arguments:"
               ] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
args

-- | Filtering function for use with `catchJust` or `tryJust`
--   that filters out asynch 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