content: {-
  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 path = do
    Env.findExecutable =<< Env.expandEnvironmentPath Map.empty path
  
  findSolverPath :: ConfigOption (BaseStringType Unicode) -> Config -> IO FilePath
  findSolverPath o cfg =
    do v <- getOpt =<< getOptionSetting o 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 path args mcwd action = do
    let onError (_,_,_,ph) = do
          -- Interrupt process; suppress any exceptions that occur.
          catchJust filterAsync (terminateProcess ph) (\(ex :: SomeException) ->
            hPutStrLn stderr $ displayException ex)
  
    bracket (startProcess path args mcwd)
            (void . cleanupProcess)
            (\hs -> onException (action hs) (onError hs))
  
  
  -- | Close the connected process pipes and wait for the process to exit
  cleanupProcess :: (Handle, Handle, Handle, ProcessHandle) -> IO ExitCode
  cleanupProcess (h_in, h_out, h_err, ph) =
   do catchJust filterAsync
           (hClose h_in >> hClose h_out >> hClose h_err)
           (\(_ :: SomeException) -> return ())
      waitForProcess 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 path args mcwd =
    do let create_proc
              = (proc path args)
                { std_in  = CreatePipe
                , std_out = CreatePipe
                , std_err = CreatePipe
                , create_group = False
                , cwd = mcwd
                , delegate_ctlc = True
                }
       createProcess create_proc >>= \case
         (Just in_h, Just out_h, Just err_h, ph) -> return (in_h, out_h, err_h, ph)
         _ -> panic "startProcess" $
                 [ "Failed to exec: " ++ show path
                 , "With the following arguments:"
                 ] ++ 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 e
    | Just (_ :: AsyncException) <- fromException e = Nothing
    | otherwise = Just e
  