{-
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 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
     [Char] -> IO [Char]
resolveSolverPath (Text -> [Char]
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 :: 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