diff options
Diffstat (limited to 'source/Provers.hs')
| -rw-r--r-- | source/Provers.hs | 1940 |
1 files changed, 0 insertions, 1940 deletions
diff --git a/source/Provers.hs b/source/Provers.hs deleted file mode 100644 index 7a22e12..0000000 --- a/source/Provers.hs +++ /dev/null @@ -1,1940 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RecordWildCards #-} - -module Provers - ( Vampire - , vampire - , VampireTaskMode(..) - , VampireStatus(..) - , CanonicalAtpOutcome(..) - , CanonicalAtpRejection(..) - , VampireProtocolError(..) - , classifyVampireProtocol - , vampireStatusParser - , TimeLimit(..) - , MemoryLimit(..) - , defaultTimeLimit - , defaultMemoryLimit - , ProverAnswer - ( CounterSatisfiable - , ContradictoryAxioms - , Uncertain - , Error - ) - , pattern Yes - , ProverStream(..) - , ProverOutputStream(..) - , ProverProcessError(..) - , VerificationDialect(..) - , PreparedVerificationRequest - , preparedVerificationDialect - , preparedVerificationText - , preparedVerificationBytes - , preparedVerificationByteCount - , preparedVerificationRequestId - , PreparedTypedProverTask - , prepareTypedProverTask - , preparedTypedProverLogicalProblem - , preparedTypedProverRequest - , AcceptedVampireRun - , acceptedVampireRequestId - , provedVampireRun - , runPreparedTypedProver - , runPreparedTypedProverWithObserver - , EffectiveJobs - , effectiveJobs - , effectiveJobsValue - , JobsSelection(..) - , selectEffectiveJobs - , WorkPosition - , workPosition - , workPositionModuleOrdinal - , workPositionLocalRequestOrdinal - , VampireExecutor - , VampireExecutorFault - , VampireExecutorObservation(..) - , VampireRequestOwner - , VampireHandle - , VampireTerminal(..) - , renderVampireTerminalDiagnostic - , VampireCompletion(..) - , withVampireExecutor - , withVampireRequestOwner - , submitVampireRequest - , awaitVampireRequest - , awaitPreparedVampireRequest - , cancelVampireRequest - , runPreparedTypedProverWithExecutor - , vampireExecutorObservation - ) where - -import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem -import Checking.Backend.Tptp - -import Control.Concurrent.STM - ( STM - , TBQueue - , TMVar - , TVar - , atomically - , check - , modifyTVar' - , newEmptyTMVarIO - , newTBQueueIO - , newTVarIO - , orElse - , readTMVar - , readTBQueue - , readTVar - , readTVarIO - , throwSTM - , tryPutTMVar - , tryReadTMVar - , writeTBQueue - , writeTVar - ) -import Control.Exception - ( AsyncException - , IOException - , SomeException - , displayException - , fromException - ) -import Control.Exception qualified as Exception -import Control.Monad (replicateM, unless, when) -import Control.Monad.Logger -import Data.ByteString qualified as ByteString -import Data.IntMap.Strict qualified as IntMap -import Data.IORef - ( IORef - , atomicModifyIORef' - , newIORef - , readIORef - , writeIORef - ) -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Text.Encoding qualified as TextEncoding -import Data.Text.Encoding.Error qualified as TextEncodingError -import Data.Time -import Numeric.Natural (Natural) -import System.Exit (ExitCode(..)) -import System.Posix.Signals (sigKILL, signalProcessGroup) -import System.Posix.Types (ProcessGroupID) -import System.Process - ( CreateProcess(..) - , ProcessHandle - , StdStream(CreatePipe) - , getPid - , proc - , waitForProcess - , withCreateProcess - ) -import System.Timeout qualified as Timeout -import Text.Megaparsec -import Text.Megaparsec.Char qualified as Char -import TextBuilder -import UnliftIO.Async - ( async - , cancel - , concurrently - , waitCatch - , waitCatchSTM - ) - -data Vampire = Vampire - { vampireExecutable :: FilePath - , vampireTimeLimit :: TimeLimit - , vampireMemoryLimit :: MemoryLimit - } - deriving (Show, Eq) - -newtype TimeLimit = Seconds Word64 deriving (Show, Eq, Num) -newtype MemoryLimit = Megabytes Word64 deriving (Show, Eq) - -defaultTimeLimit :: TimeLimit -defaultTimeLimit = Seconds 10 - -defaultMemoryLimit :: MemoryLimit -defaultMemoryLimit = Megabytes 5000 - -vampire :: FilePath -> TimeLimit -> MemoryLimit -> Vampire -vampire = Vampire - -vampireArguments :: Vampire -> [String] -vampireArguments Vampire{..} = - [ "--input_syntax", "tptp" - , "--mode", "casc" - , "--time_limit", toSeconds vampireTimeLimit - , "--memory_limit", toMegabytes vampireMemoryLimit - , "--cores", "2" - ] - --- | A strictly positive invocation-local bound for module pipelines and --- top-level Vampire invocations. -newtype EffectiveJobs = EffectiveJobs Int - deriving (Show, Eq, Ord) - -effectiveJobs :: Int -> Maybe EffectiveJobs -effectiveJobs amount - | amount > 0 = Just (EffectiveJobs amount) - | otherwise = Nothing - -effectiveJobsValue :: EffectiveJobs -> Int -effectiveJobsValue (EffectiveJobs amount) = amount - --- | The effective worker policy selected for one invocation. Processor --- discovery is operational evidence only and enters no durable identity. -data JobsSelection = JobsSelection - { jobsSelectionDetectedProcessors :: !(Maybe Int) - , jobsSelectionEffectiveJobs :: !EffectiveJobs - , jobsSelectionWasOverridden :: !Bool - } - deriving (Show, Eq) - --- | Select the worker bound, with processor discovery injected for focused --- testing. Asynchronous cancellation is never mistaken for failed discovery. -selectEffectiveJobs - :: Maybe EffectiveJobs - -> IO Int - -> IO JobsSelection -selectEffectiveJobs override detectProcessors = - case override of - Just selected -> - pure - JobsSelection - { jobsSelectionDetectedProcessors = Nothing - , jobsSelectionEffectiveJobs = selected - , jobsSelectionWasOverridden = True - } - Nothing -> do - detectedResult <- Exception.try detectProcessors - case detectedResult of - Left detectionFailure - | Just asynchronous <- - (fromException detectionFailure - :: Maybe AsyncException) -> - Exception.throwIO asynchronous - | otherwise -> - fallback - Right detectedRaw -> - let detected = max 1 detectedRaw - -- Two portfolio workers plus one module pipeline - -- nominally consume about three logical CPUs. - automaticJobs = max 1 ((detected + 1) `div` 3) - in pure - JobsSelection - { jobsSelectionDetectedProcessors = - Just detected - , jobsSelectionEffectiveJobs = - EffectiveJobs automaticJobs - , jobsSelectionWasOverridden = False - } - where - fallback = - pure - JobsSelection - { jobsSelectionDetectedProcessors = Nothing - , jobsSelectionEffectiveJobs = EffectiveJobs 1 - , jobsSelectionWasOverridden = False - } - --- | Stable runtime diagnostic position. It is deliberately separate from --- request, validation, cache, and mathematical identities. -data WorkPosition = WorkPosition !Natural !Natural - deriving (Show, Eq, Ord) - -workPosition :: Natural -> Natural -> WorkPosition -workPosition = WorkPosition - -workPositionModuleOrdinal :: WorkPosition -> Natural -workPositionModuleOrdinal (WorkPosition moduleOrdinal _localOrdinal) = - moduleOrdinal - -workPositionLocalRequestOrdinal :: WorkPosition -> Natural -workPositionLocalRequestOrdinal (WorkPosition _moduleOrdinal localOrdinal) = - localOrdinal - -toSeconds :: TimeLimit -> String -toSeconds (Seconds secs) = show secs - -toMegabytes :: MemoryLimit -> String -toMegabytes (Megabytes mbs) = show mbs - -data VampireTaskMode - = DirectTask - | IndirectTask - deriving (Show, Eq) - -data VampireStatus - = StatusTheorem - | StatusCounterSatisfiable - | StatusContradictoryAxioms - | StatusTimeout - | StatusResourceOut - | StatusGaveUp - | StatusUnknown - | UnsupportedStatus Text - deriving (Show, Eq) - -data CanonicalAtpOutcome - = Proved - | Counterexample - | ContradictoryInput - | Indeterminate - deriving (Show, Eq, Ord) - --- | The closed non-accepting subset of canonical ATP outcomes. Protocol --- disagreement is represented separately from a semantic non-proof, while an --- accepting result is unrepresentable here. -data CanonicalAtpRejection - = RejectedCounterexample - | RejectedContradictoryInput - | RejectedIndeterminate - deriving (Show, Eq) - -data VampireProtocolError - = UnsuccessfulVampireExit ExitCode - | UnsupportedVampireStatuses (Set Text) - | MalformedVampireStatusLines (Set Text) - | MissingVampireOutcome - | ConflictingTerminalOutcomes (Set CanonicalAtpOutcome) - deriving (Show, Eq) - -data CompleteCapturedStreams = CompleteCapturedStreams - { completedStdout :: !Text - , completedStderr :: !Text - } - deriving (Show, Eq) - -data CompletedTranscript = CompletedTranscript - { completedExitCode :: !ExitCode - , completedStreams :: !CompleteCapturedStreams - } - deriving (Show, Eq) - -data PartialCapturedStreams = PartialCapturedStreams - { partialStdout :: !ByteString.ByteString - , partialStderr :: !ByteString.ByteString - } - deriving (Eq) - -instance Show PartialCapturedStreams where - showsPrec precedence PartialCapturedStreams{..} = - showParen (precedence > applicationPrecedence) - ( showString "PartialCapturedStreams " - . shows - ( ByteString.length partialStdout - , ByteString.length partialStderr - ) - ) - -data BoundedBytes = BoundedBytes - { boundedBytesOriginalCount :: !Int - , boundedBytesRetained :: !ByteString.ByteString - , boundedBytesTruncated :: !Bool - } - deriving (Eq) - -instance Show BoundedBytes where - showsPrec precedence BoundedBytes{..} = - showParen (precedence > applicationPrecedence) - ( showString "BoundedBytes " - . shows - ( boundedBytesOriginalCount - , ByteString.length boundedBytesRetained - , boundedBytesTruncated - ) - ) - -data BoundedCapturedStreams = BoundedCapturedStreams - { boundedStdout :: !BoundedBytes - , boundedStderr :: !BoundedBytes - } - deriving (Show, Eq) - -data BoundedDiagnostic = BoundedDiagnostic - { boundedDiagnosticSummary :: !Text - , boundedDiagnosticStdout :: !BoundedBytes - , boundedDiagnosticStderr :: !BoundedBytes - } - deriving (Show, Eq) - --- | Classify parsed Vampire statuses without depending on stream or line order. -classifyVampireProtocol - :: VampireTaskMode - -> ExitCode - -> [VampireStatus] - -> Either VampireProtocolError CanonicalAtpOutcome -classifyVampireProtocol mode exitCode statuses = - case exitCode of - ExitFailure _ -> - Left (UnsuccessfulVampireExit exitCode) - ExitSuccess - | not (Set.null unsupported) -> - Left (UnsupportedVampireStatuses unsupported) - | otherwise -> - classifyOutcomes - (Set.fromList - [ outcome - | status <- statuses - , Just outcome <- [vampireStatusOutcome mode status] - ]) - where - unsupported = - Set.fromList - [ status - | UnsupportedStatus status <- statuses - ] - -classifyOutcomes - :: Set CanonicalAtpOutcome - -> Either VampireProtocolError CanonicalAtpOutcome -classifyOutcomes outcomes = - case Set.toList terminalOutcomes of - [] -> - if Indeterminate `Set.member` outcomes - then Right Indeterminate - else Left MissingVampireOutcome - [outcome] -> - Right outcome - _ -> - Left (ConflictingTerminalOutcomes terminalOutcomes) - where - terminalOutcomes = Set.delete Indeterminate outcomes - -vampireStatusOutcome - :: VampireTaskMode - -> VampireStatus - -> Maybe CanonicalAtpOutcome -vampireStatusOutcome mode = \case - StatusTheorem -> - Just Proved - StatusCounterSatisfiable -> - Just Counterexample - StatusContradictoryAxioms -> - Just case mode of - DirectTask -> ContradictoryInput - IndirectTask -> Proved - StatusTimeout -> - Just Indeterminate - StatusResourceOut -> - Just Indeterminate - StatusGaveUp -> - Just Indeterminate - StatusUnknown -> - Just Indeterminate - UnsupportedStatus{} -> - Nothing - -data VerificationDialect - = VerificationFof - | VerificationTh0 - deriving (Show, Eq) - -data PreparedVerificationRequest = PreparedVerificationRequest - { preparedVerificationDialect :: !VerificationDialect - , preparedVerificationMode :: !VampireTaskMode - , preparedVerificationInput :: !ByteString.ByteString - , preparedVerificationIdentity :: !Authority.PreparedRequestId - } - deriving (Eq) - --- | Decode the one canonical serialized request only at a textual boundary. --- Prepared requests deliberately do not retain an equivalent 'Text' copy. -preparedVerificationText :: PreparedVerificationRequest -> Text -preparedVerificationText request = - let encoded = preparedVerificationInput request - withoutFinalNewline = - case ByteString.unsnoc encoded of - Just (body, 10) -> body - _ -> encoded - in TextEncoding.decodeUtf8 withoutFinalNewline - -preparedVerificationByteCount - :: PreparedVerificationRequest - -> Int -preparedVerificationByteCount = - ByteString.length . preparedVerificationInput - -preparedVerificationBytes - :: PreparedVerificationRequest - -> ByteString.ByteString -preparedVerificationBytes = - preparedVerificationInput - -preparedVerificationRequestId - :: PreparedVerificationRequest - -> Authority.PreparedRequestId -preparedVerificationRequestId = - preparedVerificationIdentity - -data PreparedTypedProverTask ref local origin global = - PreparedTypedProverTask - !(TypedProblem ref local origin global) - !PreparedVerificationRequest - !Text - -prepareTypedProverTask - :: (Ord local, Ord global) - => VampireTaskMode - -> TypedProblem ref local origin global - -> Either - (TypedTptpPreparationError local global) - (PreparedTypedProverTask ref local origin global) -prepareTypedProverTask mode problem = do - prepared <- - prepareTypedTptpProblem problem - let dialect = - case preparedTypedTptpRoute prepared of - RouteFof -> VerificationFof - RouteTh0 -> VerificationTh0 - bytes = - TextEncoding.encodeUtf8 - (preparedTypedTptpTextNewline prepared) - identity = - Authority.preparedRequestId - (case dialect of - VerificationFof -> Authority.PreparedRequestFof - VerificationTh0 -> Authority.PreparedRequestTh0) - (case mode of - DirectTask -> Authority.PreparedRequestDirect - IndirectTask -> Authority.PreparedRequestIndirect) - bytes - preparedRequest = - PreparedVerificationRequest - { preparedVerificationDialect = dialect - , preparedVerificationMode = mode - , preparedVerificationInput = bytes - , preparedVerificationIdentity = identity - } - pure - (PreparedTypedProverTask - problem - preparedRequest - (preparedTypedTptpConjectureText prepared)) - -preparedTypedProverLogicalProblem - :: PreparedTypedProverTask ref local origin global - -> TypedProblem ref local origin global -preparedTypedProverLogicalProblem - (PreparedTypedProverTask - problem - _request - _conjecture) = - problem - -preparedTypedProverRequest - :: PreparedTypedProverTask ref local origin global - -> PreparedVerificationRequest -preparedTypedProverRequest - (PreparedTypedProverTask - _problem - request - _conjecture) = - request - -data AcceptedVampireRun = AcceptedVampireRun - { acceptedVampireRequestId :: !Authority.PreparedRequestId } - deriving (Eq) - -data ProverAnswer - = ProvedAnswer AcceptedVampireRun - | CounterSatisfiable Text - | ContradictoryAxioms Text - | Uncertain Text - | Error Text Text - deriving (Eq) - -pattern Yes :: ProverAnswer -pattern Yes <- ProvedAnswer _ - -{-# COMPLETE Yes, CounterSatisfiable, ContradictoryAxioms, Uncertain, Error #-} - -instance Show ProverAnswer where - showsPrec _ (ProvedAnswer _) = - showString "Yes" - showsPrec precedence (CounterSatisfiable task) = - showParen (precedence > applicationPrecedence) - (showString "CounterSatisfiable " - . showsPrec (applicationPrecedence + 1) task) - showsPrec precedence (ContradictoryAxioms task) = - showParen (precedence > applicationPrecedence) - (showString "ContradictoryAxioms " - . showsPrec (applicationPrecedence + 1) task) - showsPrec precedence (Uncertain task) = - showParen (precedence > applicationPrecedence) - (showString "Uncertain " - . showsPrec (applicationPrecedence + 1) task) - showsPrec precedence (Error errorLabel message) = - showParen (precedence > applicationPrecedence) - (showString "Error " - . showsPrec (applicationPrecedence + 1) errorLabel - . showChar ' ' - . showsPrec (applicationPrecedence + 1) message) - -provedVampireRun :: ProverAnswer -> Maybe AcceptedVampireRun -provedVampireRun = \case - ProvedAnswer accepted -> - Just accepted - CounterSatisfiable{} -> - Nothing - ContradictoryAxioms{} -> - Nothing - Uncertain{} -> - Nothing - Error{} -> - Nothing - -applicationPrecedence :: Int -applicationPrecedence = 10 - -data ProverStream - = ProverStdin - | ProverStdout - | ProverStderr - deriving (Show, Eq) - -data ProverOutputStream - = ProverOutputStdout - | ProverOutputStderr - deriving (Show, Eq) - -data ProverProcessError - = ProverLaunchFailed !FilePath !Text - | ProverCommunicationFailed !FilePath !ProverStream !Text - | ProverOutputMalformedUtf8 !FilePath !ProverOutputStream !Text - | ProverTimedOut - !FilePath - !TimeLimit - !BoundedCapturedStreams - | ProverOutputLimitExceeded - !FilePath - !ProverOutputStream - !BoundedCapturedStreams - | ProverTerminatedBySignal - !FilePath - !Int - !BoundedCapturedStreams - | ProverLifecycleFailed !FilePath !Text - deriving (Show, Eq) - -data SupervisorAbort - = SupervisorCommunicationFailed !ProverStream !Text - | SupervisorOutputLimitExceeded !ProverOutputStream - | SupervisorLifecycleFailed !Text - deriving (Show) - -instance Exception.Exception SupervisorAbort - -data CaptureBuffer = CaptureBuffer - { captureByteCount :: !Int - , captureChunksReversed :: ![ByteString.ByteString] - } - -vampireOutputByteLimit :: Int -vampireOutputByteLimit = - 16 * 1024 * 1024 - -vampireWallGraceSeconds :: Integer -vampireWallGraceSeconds = - 2 - -captureChunkSize :: Int -captureChunkSize = - 32 * 1024 - -runPreparedTypedProver - :: (MonadIO io, MonadLogger io) - => Vampire - -> PreparedTypedProverTask ref local origin global - -> io (Either ProverProcessError ProverAnswer) -runPreparedTypedProver - vampireCommand = - runPreparedTypedProverWithObserver - (\_request -> pure ()) - vampireCommand - -runPreparedTypedProverWithObserver - :: (MonadIO io, MonadLogger io) - => (PreparedVerificationRequest -> IO ()) - -> Vampire - -> PreparedTypedProverTask ref local origin global - -> io (Either ProverProcessError ProverAnswer) -runPreparedTypedProverWithObserver - observer - vampireCommand - (PreparedTypedProverTask - _problem - preparedRequest - conjecture) = do - startTime <- liftIO getCurrentTime - terminal <- liftIO - (runPreparedVerificationTerminal - observer - vampireCommand - preparedRequest) - answer <- liftIO - (completionProverResult - preparedRequest - (VampireCompletion terminal)) - endTime <- liftIO getCurrentTime - let duration = - timeDifferenceToText - startTime - endTime - dialect = - case preparedVerificationDialect preparedRequest of - VerificationFof -> - "FOF" - VerificationTh0 -> - "TH0" - logInfoN - (duration - <> " " - <> conjecture - <> " [typed " - <> dialect - <> "]") - pure answer - --- | Invocation-local bounded owner of Vampire subprocesses. The finite queue --- carries only immutable prepared bytes plus runtime diagnostic position; --- checker builders and typed tasks never cross this boundary. -data VampireExecutor = VampireExecutor - { executorQueue :: !(TBQueue ExecutorJob) - , executorState :: !(TVar VampireExecutorState) - , executorNextHandle :: !(TVar Int) - , executorCommand :: !Vampire - , executorRequestObserver - :: !(WorkPosition -> PreparedVerificationRequest -> IO ()) - , executorRuntime :: !(TVar VampireExecutorRuntime) - } - -data ExecutorJob = ExecutorJob - { executorJobPosition :: !WorkPosition - , executorJobRequest :: !PreparedVerificationRequest - , executorJobCancelled :: !(TVar Bool) - , executorJobStarted :: !(TVar Bool) - , executorJobCompletion - :: !(TMVar VampireCompletion) - } - -data VampireExecutorState - = ExecutorRunning - | ExecutorClosing - | ExecutorFaulted !VampireExecutorFault - --- | A global executor fault is distinct from one request's declared process --- or protocol outcome. Its bounded message carries no process transcript. -newtype VampireExecutorFault = VampireExecutorFault Text - deriving (Show) - -instance Exception.Exception VampireExecutorFault - -data VampireRequestOwner = VampireRequestOwner - { requestOwnerExecutor :: !VampireExecutor - , requestOwnerState :: !(TVar VampireRequestOwnerState) - } - -data VampireRequestOwnerState - = RequestOwnerOpen !(IntMap VampireHandle) - | RequestOwnerClosed - --- | An opaque, owner-scoped completion handle. It deliberately retains no --- prepared request, command, transcript, builder, or parser state. -data VampireHandle = VampireHandle - { vampireHandleOrdinal :: !Int - , vampireHandleOwner :: !VampireRequestOwner - , vampireHandleCancelled :: !(TVar Bool) - , vampireHandleStarted :: !(TVar Bool) - , vampireHandleCompletion :: !(TMVar VampireCompletion) - } - -data VampireTerminal - = VampireAccepted !Authority.PreparedRequestId - | VampireRejected !CanonicalAtpRejection !BoundedDiagnostic - | VampireProtocolFailed !BoundedDiagnostic - | VampireProcessFailed !ProverProcessError - | VampireCancelled - deriving (Show, Eq) - -newtype VampireCompletion = VampireCompletion - { vampireCompletionTerminal :: VampireTerminal } - deriving (Show, Eq) - -renderVampireTerminalDiagnostic :: VampireTerminal -> Maybe Text -renderVampireTerminalDiagnostic = \case - VampireAccepted{} -> Nothing - VampireRejected _rejection diagnostic -> - Just (renderBoundedDiagnostic diagnostic) - VampireProtocolFailed diagnostic -> - Just (renderBoundedDiagnostic diagnostic) - VampireProcessFailed processFailure -> - Just (Text.pack (show processFailure)) - VampireCancelled -> Nothing - -data VampireExecutorRuntime = VampireExecutorRuntime - { runtimeSubmittedCount :: !Int - , runtimeRunCount :: !Int - , runtimeLiveCount :: !Int - , runtimeMaximumLiveCount :: !Int - , runtimeFirstStartNanoseconds :: !(Maybe Word64) - , runtimeFinalSubmissionNanoseconds :: !(Maybe Word64) - , runtimeFinalCompletionNanoseconds :: !(Maybe Word64) - , runtimeExecutionNanoseconds :: !Word64 - , runtimeLongestExecutionNanoseconds :: !Word64 - } - -data VampireExecutorObservation = VampireExecutorObservation - { vampireExecutorSubmittedCount :: !Int - , vampireExecutorRunCount :: !Int - , vampireExecutorMaximumLiveCount :: !Int - , vampireExecutorFirstStartNanoseconds :: !(Maybe Word64) - , vampireExecutorFinalSubmissionNanoseconds :: !(Maybe Word64) - , vampireExecutorFinalCompletionNanoseconds :: !(Maybe Word64) - , vampireExecutorExecutionNanoseconds :: !Word64 - , vampireExecutorLongestExecutionNanoseconds :: !Word64 - } - deriving (Show, Eq) - -data VampireExecutorClosed = VampireExecutorClosed - deriving (Show) - -instance Exception.Exception VampireExecutorClosed - -data VampireRequestOwnerClosed = VampireRequestOwnerClosed - deriving (Show) - -instance Exception.Exception VampireRequestOwnerClosed - -data RequestObserverFailure = RequestObserverFailure SomeException - -instance Show RequestObserverFailure where - show (RequestObserverFailure observerError) = - "request observer failed: " <> displayException observerError - -instance Exception.Exception RequestObserverFailure - -initialVampireExecutorRuntime :: VampireExecutorRuntime -initialVampireExecutorRuntime = - VampireExecutorRuntime - { runtimeSubmittedCount = 0 - , runtimeRunCount = 0 - , runtimeLiveCount = 0 - , runtimeMaximumLiveCount = 0 - , runtimeFirstStartNanoseconds = Nothing - , runtimeFinalSubmissionNanoseconds = Nothing - , runtimeFinalCompletionNanoseconds = Nothing - , runtimeExecutionNanoseconds = 0 - , runtimeLongestExecutionNanoseconds = 0 - } - --- | Bracket exactly the selected number of workers. Cancelling the bracket --- cancels each worker; a worker owning a subprocess in turn terminates and --- reaps that process group through the ordinary supervisor boundary. -withVampireExecutor - :: EffectiveJobs - -> Vampire - -> (WorkPosition -> PreparedVerificationRequest -> IO ()) - -> (VampireExecutor -> IO value) - -> IO value -withVampireExecutor selected command observer action = - Exception.bracket acquire release (action . fst) - where - workerCount = effectiveJobsValue selected - - acquire = do - queue <- newTBQueueIO - (fromIntegral workerCount * 2) - state <- newTVarIO ExecutorRunning - nextHandle <- newTVarIO 0 - runtime <- newTVarIO initialVampireExecutorRuntime - let executor = - VampireExecutor - { executorQueue = queue - , executorState = state - , executorNextHandle = nextHandle - , executorCommand = command - , executorRequestObserver = observer - , executorRuntime = runtime - } - workers <- replicateM workerCount - (async (superviseExecutorWorker executor)) - pure (executor, workers) - - release (executor, workers) = do - atomically do - state <- readTVar (executorState executor) - case state of - ExecutorRunning -> - writeTVar (executorState executor) ExecutorClosing - ExecutorClosing -> - pure () - ExecutorFaulted{} -> - pure () - traverse_ cancel workers - traverse_ waitCatch workers - --- | Bracket the complete set of handles submitted by one module pipeline. --- Normal early return, failure, and asynchronous cancellation all cancel and --- reap the remaining owned work before the scope is left. -withVampireRequestOwner - :: VampireExecutor - -> (VampireRequestOwner -> IO value) - -> IO value -withVampireRequestOwner executor = - Exception.bracket acquire release - where - acquire = - VampireRequestOwner executor - <$> newTVarIO (RequestOwnerOpen IntMap.empty) - - release owner = Exception.mask_ do - handles <- atomically do - state <- readTVar (requestOwnerState owner) - case state of - RequestOwnerClosed -> - pure [] - RequestOwnerOpen owned -> do - writeTVar (requestOwnerState owner) RequestOwnerClosed - pure (IntMap.elems owned) - traverse_ signalVampireCancellation handles - traverse_ awaitVampireCancellation handles - traverse_ deregisterVampireHandle handles - -runPreparedTypedProverWithExecutor - :: (MonadIO io, MonadLogger io) - => VampireRequestOwner - -> WorkPosition - -> PreparedTypedProverTask ref local origin global - -> io (Either ProverProcessError ProverAnswer) -runPreparedTypedProverWithExecutor - owner - position - (PreparedTypedProverTask - _problem - preparedRequest - conjecture) = do - startTime <- liftIO getCurrentTime - answer <- liftIO do - handle <- submitVampireRequest owner position preparedRequest - completion <- - awaitVampireRequest handle - `Exception.onException` cancelVampireRequest handle - completionProverResult preparedRequest completion - endTime <- liftIO getCurrentTime - let dialect = - case preparedVerificationDialect preparedRequest of - VerificationFof -> "FOF" - VerificationTh0 -> "TH0" - logInfoN - (timeDifferenceToText startTime endTime - <> " " - <> conjecture - <> " [typed " - <> dialect - <> "]") - pure answer - -vampireExecutorObservation - :: VampireExecutor - -> IO VampireExecutorObservation -vampireExecutorObservation executor = do - runtime <- readTVarIO (executorRuntime executor) - pure - VampireExecutorObservation - { vampireExecutorSubmittedCount = runtimeSubmittedCount runtime - , vampireExecutorRunCount = runtimeRunCount runtime - , vampireExecutorMaximumLiveCount = - runtimeMaximumLiveCount runtime - , vampireExecutorFirstStartNanoseconds = - runtimeFirstStartNanoseconds runtime - , vampireExecutorFinalSubmissionNanoseconds = - runtimeFinalSubmissionNanoseconds runtime - , vampireExecutorFinalCompletionNanoseconds = - runtimeFinalCompletionNanoseconds runtime - , vampireExecutorExecutionNanoseconds = - runtimeExecutionNanoseconds runtime - , vampireExecutorLongestExecutionNanoseconds = - runtimeLongestExecutionNanoseconds runtime - } - -submitVampireRequest - :: VampireRequestOwner - -> WorkPosition - -> PreparedVerificationRequest - -> IO VampireHandle -submitVampireRequest owner position request = do - -- Force the compact queue payload before masked ownership acquisition. - _ <- Exception.evaluate (preparedVerificationByteCount request) - _ <- Exception.evaluate (preparedVerificationRequestId request) - Exception.mask_ do - cancelled <- newTVarIO False - started <- newTVarIO False - completion <- newEmptyTMVarIO - let executor = requestOwnerExecutor owner - handle <- atomically do - executorStatus <- readTVar (executorState executor) - case executorStatus of - ExecutorClosing -> throwSTM VampireExecutorClosed - ExecutorFaulted fault -> throwSTM fault - ExecutorRunning -> pure () - ownerStatus <- readTVar (requestOwnerState owner) - owned <- case ownerStatus of - RequestOwnerClosed -> throwSTM VampireRequestOwnerClosed - RequestOwnerOpen current -> pure current - ordinal <- readTVar (executorNextHandle executor) - writeTVar (executorNextHandle executor) (ordinal + 1) - let acquired = - VampireHandle - { vampireHandleOrdinal = ordinal - , vampireHandleOwner = owner - , vampireHandleCancelled = cancelled - , vampireHandleStarted = started - , vampireHandleCompletion = completion - } - job = - ExecutorJob - { executorJobPosition = position - , executorJobRequest = request - , executorJobCancelled = cancelled - , executorJobStarted = started - , executorJobCompletion = completion - } - writeTBQueue (executorQueue executor) job - writeTVar - (requestOwnerState owner) - (RequestOwnerOpen (IntMap.insert ordinal acquired owned)) - modifyTVar' - (executorRuntime executor) - (\runtime -> - runtime - { runtimeSubmittedCount = - runtimeSubmittedCount runtime + 1 - }) - pure acquired - submitted <- getMonotonicTimeNSec - atomically - (modifyTVar' - (executorRuntime executor) - (\runtime -> - runtime - { runtimeFinalSubmissionNanoseconds = - Just - (maybe submitted - (max submitted) - (runtimeFinalSubmissionNanoseconds - runtime)) - })) - pure handle - -awaitVampireRequest :: VampireHandle -> IO VampireCompletion -awaitVampireRequest handle = Exception.mask \restore -> do - let executor = requestOwnerExecutor (vampireHandleOwner handle) - completion <- restore (atomically do - executorStatus <- readTVar (executorState executor) - case executorStatus of - ExecutorFaulted fault -> throwSTM fault - ExecutorRunning -> readTMVar (vampireHandleCompletion handle) - ExecutorClosing -> - (readTMVar (vampireHandleCompletion handle)) - `orElse` throwSTM VampireExecutorClosed) - deregisterVampireHandle handle - pure completion - --- | Await one already submitted request and recover the ordinary typed --- prover result. The supplied immutable request is checked against an --- accepting terminal before any caller may treat the result as evidence. -awaitPreparedVampireRequest - :: PreparedVerificationRequest - -> VampireHandle - -> IO (Either ProverProcessError ProverAnswer) -awaitPreparedVampireRequest request handle = - awaitVampireRequest handle >>= completionProverResult request - -cancelVampireRequest :: VampireHandle -> IO () -cancelVampireRequest handle = Exception.mask_ do - signalVampireCancellation handle - awaitVampireCancellation handle - deregisterVampireHandle handle - -signalVampireCancellation :: VampireHandle -> IO () -signalVampireCancellation handle = do - let executor = requestOwnerExecutor (vampireHandleOwner handle) - completion = VampireCompletion VampireCancelled - _ <- Exception.evaluate completion - published <- getMonotonicTimeNSec - atomically do - writeTVar (vampireHandleCancelled handle) True - started <- readTVar (vampireHandleStarted handle) - unless started - (void - (publishVampireTerminalSTM - executor - (vampireHandleCompletion handle) - published - completion)) - -awaitVampireCancellation :: VampireHandle -> IO () -awaitVampireCancellation handle = - -- A running worker acknowledges ordinary cancellation only after - -- terminating and reaping its owned process group. After a global fault, - -- the worker lifecycle flag is the acknowledgement because the terminal - -- cell deliberately remains subordinate to that fault. - atomically do - executorStatus <- readTVar - (executorState (requestOwnerExecutor (vampireHandleOwner handle))) - case executorStatus of - ExecutorFaulted{} -> do - stillRunning <- readTVar (vampireHandleStarted handle) - check (not stillRunning) - _ -> void (readTMVar (vampireHandleCompletion handle)) - -deregisterVampireHandle :: VampireHandle -> IO () -deregisterVampireHandle handle = atomically do - let owner = vampireHandleOwner handle - state <- readTVar (requestOwnerState owner) - case state of - RequestOwnerClosed -> pure () - RequestOwnerOpen owned -> - writeTVar - (requestOwnerState owner) - (RequestOwnerOpen - (IntMap.delete (vampireHandleOrdinal handle) owned)) - -superviseExecutorWorker :: VampireExecutor -> IO () -superviseExecutorWorker executor = do - result <- Exception.try (executorWorker executor) - case result of - Right () -> pure () - Left workerFailure -> do - state <- readTVarIO (executorState executor) - case state of - ExecutorRunning -> - recordExecutorFault executor workerFailure - ExecutorClosing -> - pure () - ExecutorFaulted{} -> - pure () - -recordExecutorFault :: VampireExecutor -> SomeException -> IO () -recordExecutorFault executor workerFailure = atomically do - state <- readTVar (executorState executor) - case state of - ExecutorRunning -> - writeTVar - (executorState executor) - (ExecutorFaulted - (VampireExecutorFault - (boundedText - (Text.pack (displayException workerFailure))))) - ExecutorClosing -> pure () - ExecutorFaulted{} -> pure () - -executorWorker :: VampireExecutor -> IO () -executorWorker executor = do - next <- atomically do - state <- readTVar (executorState executor) - case state of - ExecutorRunning -> Just <$> readTBQueue (executorQueue executor) - ExecutorClosing -> pure Nothing - ExecutorFaulted{} -> pure Nothing - case next of - Nothing -> pure () - Just job -> do - shouldRun <- atomically do - completed <- tryReadTMVar (executorJobCompletion job) - case completed of - Just _ -> pure False - Nothing -> do - writeTVar (executorJobStarted job) True - pure True - when shouldRun - (executeJob executor job - `Exception.finally` - atomically (writeTVar (executorJobStarted job) False)) - executorWorker executor - -data JobWait value - = JobFinished !(Either SomeException value) - | JobCancelled - | JobExecutorStopped - -executeJob :: VampireExecutor -> ExecutorJob -> IO () -executeJob executor job = - Exception.mask \restore -> do - running <- async - (restore - (timedExecutorRun executor job)) - waited <- restore - (atomically - (do - state <- readTVar (executorState executor) - case state of - ExecutorRunning -> - (JobFinished <$> waitCatchSTM running) - `orElse` - (do - cancelled <- readTVar - (executorJobCancelled job) - check cancelled - pure JobCancelled) - ExecutorClosing -> pure JobExecutorStopped - ExecutorFaulted{} -> pure JobExecutorStopped)) - `Exception.onException` - (cancel running >> void (waitCatch running)) - case waited of - JobFinished result -> case result of - Left workerFailure -> Exception.throwIO workerFailure - Right terminal -> - publishVampireTerminal - executor - (executorJobCompletion job) - terminal - JobCancelled -> do - cancel running - void (waitCatch running) - publishVampireTerminal - executor - (executorJobCompletion job) - VampireCancelled - JobExecutorStopped -> do - cancel running - void (waitCatch running) - -timedExecutorRun - :: VampireExecutor - -> ExecutorJob - -> IO VampireTerminal -timedExecutorRun executor job = Exception.mask \restore -> do - started <- getMonotonicTimeNSec - atomically - (modifyTVar' - (executorRuntime executor) - (\runtime -> - let live = runtimeLiveCount runtime + 1 - in runtime - { runtimeRunCount = runtimeRunCount runtime + 1 - , runtimeLiveCount = live - , runtimeMaximumLiveCount = - max live (runtimeMaximumLiveCount runtime) - , runtimeFirstStartNanoseconds = - runtimeFirstStartNanoseconds runtime <|> Just started - })) - terminal <- restore - (runPreparedVerificationTerminal - (executorRequestObserver executor (executorJobPosition job)) - (executorCommand executor) - (executorJobRequest job)) - `Exception.onException` finishExecutorRun executor started - finishExecutorRun executor started - pure terminal - -finishExecutorRun :: VampireExecutor -> Word64 -> IO () -finishExecutorRun executor started = do - finished <- getMonotonicTimeNSec - let elapsed = finished - started - atomically - (modifyTVar' - (executorRuntime executor) - (\runtime -> - runtime - { runtimeLiveCount = runtimeLiveCount runtime - 1 - , runtimeExecutionNanoseconds = - runtimeExecutionNanoseconds runtime + elapsed - , runtimeLongestExecutionNanoseconds = - max elapsed (runtimeLongestExecutionNanoseconds runtime) - })) - -publishVampireTerminal - :: VampireExecutor - -> TMVar VampireCompletion - -> VampireTerminal - -> IO () -publishVampireTerminal executor completionCell terminal = do - let completion = VampireCompletion terminal - _ <- Exception.evaluate completion - published <- getMonotonicTimeNSec - void - (atomically - (publishVampireTerminalSTM - executor completionCell published completion)) - -publishVampireTerminalSTM - :: VampireExecutor - -> TMVar VampireCompletion - -> Word64 - -> VampireCompletion - -> STM Bool -publishVampireTerminalSTM executor completionCell published completion = do - inserted <- tryPutTMVar completionCell completion - when inserted - (modifyTVar' - (executorRuntime executor) - (\runtime -> - runtime - { runtimeFinalCompletionNanoseconds = - Just - (maybe published - (max published) - (runtimeFinalCompletionNanoseconds runtime)) - })) - pure inserted - -runPreparedVerificationTerminal - :: (PreparedVerificationRequest -> IO ()) - -> Vampire - -> PreparedVerificationRequest - -> IO VampireTerminal -runPreparedVerificationTerminal observer command request = do - transcriptResult <- - runPreparedVampireProcessWithObserver observer command request - pure case transcriptResult of - Left processFailure -> - VampireProcessFailed processFailure - Right transcript -> - case classifyVampireCompleted - (preparedVerificationMode request) - transcript of - Left protocolFailure -> - VampireProtocolFailed - (boundedTranscriptDiagnostic - (Text.pack (show protocolFailure)) - transcript) - Right Proved -> - VampireAccepted (preparedVerificationRequestId request) - Right Counterexample -> - VampireRejected - RejectedCounterexample - (boundedTranscriptDiagnostic - "Vampire found a countermodel" - transcript) - Right ContradictoryInput -> - VampireRejected - RejectedContradictoryInput - (boundedTranscriptDiagnostic - "Vampire reported contradictory input" - transcript) - Right Indeterminate -> - VampireRejected - RejectedIndeterminate - (boundedTranscriptDiagnostic - "Vampire did not establish the obligation" - transcript) - -completionProverResult - :: PreparedVerificationRequest - -> VampireCompletion - -> IO (Either ProverProcessError ProverAnswer) -completionProverResult request completion = - case vampireCompletionTerminal completion of - VampireAccepted acceptedId - | acceptedId == preparedVerificationRequestId request -> - pure - (Right - (ProvedAnswer - (AcceptedVampireRun acceptedId))) - | otherwise -> - Exception.throwIO - (VampireExecutorFault - "accepted Vampire result has the wrong request id") - VampireRejected rejection _diagnostic -> - pure - (Right - (case rejection of - RejectedCounterexample -> - CounterSatisfiable task - RejectedContradictoryInput -> - ContradictoryAxioms task - RejectedIndeterminate -> - Uncertain task)) - VampireProtocolFailed diagnostic -> - pure - (Right - (Error - "typed obligation" - (renderBoundedDiagnostic diagnostic))) - VampireProcessFailed processFailure -> - pure (Left processFailure) - VampireCancelled -> - Exception.throwIO - (VampireExecutorFault - "active admission encountered a cancelled Vampire request") - where - task = preparedVerificationText request - -runPreparedVampireProcessWithObserver - :: (PreparedVerificationRequest -> IO ()) - -> Vampire - -> PreparedVerificationRequest - -> IO (Either ProverProcessError CompletedTranscript) -runPreparedVampireProcessWithObserver - observer - vampireCommand@Vampire{vampireExecutable = executable} - preparedRequest = do - callbackStarted <- newIORef False - processResult <- Exception.try - (withCreateProcess - (proc executable (vampireArguments vampireCommand)) - { std_in = CreatePipe - , std_out = CreatePipe - , std_err = CreatePipe - , create_group = True - } - \mIn mOut mErr processHandle -> - Exception.mask \restore -> do - writeIORef callbackStarted True - case (mIn, mOut, mErr) of - (Just inputHandle, Just outputHandle, Just errorHandle) -> do - maybePid <- getPid processHandle - processGroup <- case maybePid of - Just pid -> - pure (fromIntegral pid) - Nothing -> - impossible - "Vampire supervisor: missing process-group id" - restore - (do - runRequestObserver - observer - preparedRequest - superviseVampireProcess - executable - (vampireTimeLimit vampireCommand) - preparedRequest - inputHandle - outputHandle - errorHandle - processGroup - processHandle) - `Exception.onException` - forceTerminateProcessGroup - processGroup - processHandle - _ -> - impossible - "Vampire supervisor: expected CreatePipe handles") - :: IO - (Either - SomeException - (Either ProverProcessError CompletedTranscript)) - case processResult of - Right result -> - pure result - Left err - | Just (RequestObserverFailure observerFailure) <- - fromException err -> - Exception.throwIO observerFailure - | Just asynchronous <- - (fromException err :: Maybe AsyncException) -> - Exception.throwIO asynchronous - | Just ioFailure <- - (fromException err :: Maybe IOException) -> do - started <- readIORef callbackStarted - pure - (Left - (if started - then - ProverLifecycleFailed - executable - (boundedText - (exceptionText ioFailure)) - else - ProverLaunchFailed - executable - (boundedText - (exceptionText ioFailure)))) - | otherwise -> - Exception.throwIO err - -runRequestObserver - :: (PreparedVerificationRequest -> IO ()) - -> PreparedVerificationRequest - -> IO () -runRequestObserver observer request = - observer request `Exception.catch` \observerError -> - case fromException observerError :: Maybe AsyncException of - Just asynchronous -> - Exception.throwIO asynchronous - Nothing -> - Exception.throwIO - (RequestObserverFailure observerError) - -superviseVampireProcess - :: FilePath - -> TimeLimit - -> PreparedVerificationRequest - -> Handle - -> Handle - -> Handle - -> ProcessGroupID - -> ProcessHandle - -> IO (Either ProverProcessError CompletedTranscript) -superviseVampireProcess - executable - timeLimit - preparedRequest - inputHandle - outputHandle - errorHandle - processGroup - processHandle = do - stdoutCapture <- newIORef emptyCaptureBuffer - stderrCapture <- newIORef emptyCaptureBuffer - let terminateOwnedProcess = - forceTerminateProcessGroup - processGroup - processHandle - communicate = - communicateWithVampire - preparedRequest - inputHandle - outputHandle - errorHandle - stdoutCapture - stderrCapture - processHandle - supervised <- - Timeout.timeout - (wallTimeoutMicroseconds timeLimit) - (Exception.try communicate - :: IO (Either SupervisorAbort ExitCode)) - case supervised of - Nothing -> do - terminateOwnedProcess - partial <- - capturedStreams - stdoutCapture - stderrCapture - pure - (Left - (ProverTimedOut - executable - timeLimit - (boundedCapturedStreams partial))) - Just (Left abort) -> do - terminateOwnedProcess - partial <- - capturedStreams - stdoutCapture - stderrCapture - pure - (Left - (supervisorAbortError - executable - partial - abort)) - Just (Right exitCode) -> do - terminateRemainingProcessGroup processGroup - partial <- - capturedStreams - stdoutCapture - stderrCapture - case exitCode of - ExitFailure signalCode - | signalCode < 0 -> - pure - (Left - (ProverTerminatedBySignal - executable - (negate signalCode) - (boundedCapturedStreams partial))) - _ -> - pure do - stdout <- decodeOutput - executable - ProverOutputStdout - (partialStdout partial) - stderr <- decodeOutput - executable - ProverOutputStderr - (partialStderr partial) - Right - CompletedTranscript - { completedExitCode = exitCode - , completedStreams = - CompleteCapturedStreams - { completedStdout = stdout - , completedStderr = stderr - } - } - -communicateWithVampire - :: PreparedVerificationRequest - -> Handle - -> Handle - -> Handle - -> IORef CaptureBuffer - -> IORef CaptureBuffer - -> ProcessHandle - -> IO ExitCode -communicateWithVampire - preparedRequest - inputHandle - outputHandle - errorHandle - stdoutCapture - stderrCapture - processHandle = do - _ <- - concurrently - (concurrently - (captureCommunication ProverStdin - (ByteString.hPut - inputHandle - (preparedVerificationInput preparedRequest) - `Exception.finally` hClose inputHandle)) - (captureOutput - ProverOutputStdout - outputHandle - stdoutCapture)) - (captureOutput - ProverOutputStderr - errorHandle - stderrCapture) - captureLifecycle (waitForProcess processHandle) - -captureCommunication - :: ProverStream - -> IO a - -> IO a -captureCommunication stream action = - action `Exception.catch` \(err :: IOException) -> - throwIO - (SupervisorCommunicationFailed - stream - (exceptionText err)) - -captureOutput - :: ProverOutputStream - -> Handle - -> IORef CaptureBuffer - -> IO () -captureOutput stream handle capture = - captureCommunication (outputStream stream) go - where - go = do - bytes <- ByteString.hGetSome handle captureChunkSize - if ByteString.null bytes - then pure () - else do - exceeded <- appendCapturedChunk capture bytes - if exceeded - then - throwIO - (SupervisorOutputLimitExceeded stream) - else go - -outputStream :: ProverOutputStream -> ProverStream -outputStream = \case - ProverOutputStdout -> - ProverStdout - ProverOutputStderr -> - ProverStderr - -captureLifecycle :: IO a -> IO a -captureLifecycle action = - action `Exception.catch` \(err :: IOException) -> - throwIO (SupervisorLifecycleFailed (exceptionText err)) - -emptyCaptureBuffer :: CaptureBuffer -emptyCaptureBuffer = - CaptureBuffer - { captureByteCount = 0 - , captureChunksReversed = [] - } - -appendCapturedChunk - :: IORef CaptureBuffer - -> ByteString.ByteString - -> IO Bool -appendCapturedChunk capture bytes = - atomicModifyIORef' capture \buffer@CaptureBuffer{..} -> - let remaining = - vampireOutputByteLimit - captureByteCount - retained = - ByteString.take remaining bytes - retainedLength = - ByteString.length retained - buffer' = - buffer - { captureByteCount = - captureByteCount + retainedLength - , captureChunksReversed = - if ByteString.null retained - then captureChunksReversed - else retained : captureChunksReversed - } - in (buffer', ByteString.length bytes > remaining) - -capturedStreams - :: IORef CaptureBuffer - -> IORef CaptureBuffer - -> IO PartialCapturedStreams -capturedStreams stdoutCapture stderrCapture = - PartialCapturedStreams - <$> capturedBytes stdoutCapture - <*> capturedBytes stderrCapture - -capturedBytes :: IORef CaptureBuffer -> IO ByteString.ByteString -capturedBytes capture = - ByteString.concat - . reverse - . captureChunksReversed - <$> readIORef capture - -boundedTranscriptBytes :: Int -boundedTranscriptBytes = 32 * 1024 - -boundedTranscriptHalf :: Int -boundedTranscriptHalf = boundedTranscriptBytes `div` 2 - -boundedBytes :: ByteString.ByteString -> BoundedBytes -boundedBytes bytes = - let original = ByteString.length bytes - in if original <= boundedTranscriptBytes - then - BoundedBytes - { boundedBytesOriginalCount = original - , boundedBytesRetained = bytes - , boundedBytesTruncated = False - } - else - BoundedBytes - { boundedBytesOriginalCount = original - , boundedBytesRetained = - ByteString.take boundedTranscriptHalf bytes - <> ByteString.drop - (original - boundedTranscriptHalf) - bytes - , boundedBytesTruncated = True - } - -boundedText :: Text -> Text -boundedText = - decodeBoundedBytes . boundedBytes . TextEncoding.encodeUtf8 - -decodeBoundedBytes :: BoundedBytes -> Text -decodeBoundedBytes = - TextEncoding.decodeUtf8With TextEncodingError.lenientDecode - . boundedBytesRetained - -boundedCapturedStreams - :: PartialCapturedStreams - -> BoundedCapturedStreams -boundedCapturedStreams PartialCapturedStreams{..} = - BoundedCapturedStreams - { boundedStdout = boundedBytes partialStdout - , boundedStderr = boundedBytes partialStderr - } - -boundedTranscriptDiagnostic - :: Text - -> CompletedTranscript - -> BoundedDiagnostic -boundedTranscriptDiagnostic summary CompletedTranscript{completedStreams = streams} = - BoundedDiagnostic - { boundedDiagnosticSummary = boundedText summary - , boundedDiagnosticStdout = - boundedBytes - (TextEncoding.encodeUtf8 (completedStdout streams)) - , boundedDiagnosticStderr = - boundedBytes - (TextEncoding.encodeUtf8 (completedStderr streams)) - } - -renderBoundedDiagnostic :: BoundedDiagnostic -> Text -renderBoundedDiagnostic BoundedDiagnostic{..} = - Text.unlines - [ boundedDiagnosticSummary - , renderBoundedStream "stdout" boundedDiagnosticStdout - , renderBoundedStream "stderr" boundedDiagnosticStderr - ] - -renderBoundedStream :: Text -> BoundedBytes -> Text -renderBoundedStream streamLabel bytes = - streamLabel - <> (if boundedBytesTruncated bytes - then - " (retained first and last 16 KiB of " - <> Text.pack (show (boundedBytesOriginalCount bytes)) - <> " bytes)" - else "") - <> ":\n" - <> decodeBoundedBytes bytes - -supervisorAbortError - :: FilePath - -> PartialCapturedStreams - -> SupervisorAbort - -> ProverProcessError -supervisorAbortError executable partial = \case - SupervisorCommunicationFailed stream message -> - ProverCommunicationFailed executable stream (boundedText message) - SupervisorOutputLimitExceeded stream -> - ProverOutputLimitExceeded - executable - stream - (boundedCapturedStreams partial) - SupervisorLifecycleFailed message -> - ProverLifecycleFailed executable (boundedText message) - -wallTimeoutMicroseconds :: TimeLimit -> Int -wallTimeoutMicroseconds (Seconds seconds) = - fromInteger - (min - (toInteger (maxBound :: Int)) - ((toInteger seconds + vampireWallGraceSeconds) - * 1000000)) - -forceTerminateProcessGroup - :: ProcessGroupID - -> ProcessHandle - -> IO () -forceTerminateProcessGroup processGroup processHandle = - Exception.uninterruptibleMask_ do - terminateRemainingProcessGroup processGroup - _ <- waitForProcess processHandle - pure () - -terminateRemainingProcessGroup :: ProcessGroupID -> IO () -terminateRemainingProcessGroup processGroup = - ignoreMissingProcess - (signalProcessGroup sigKILL processGroup) - -ignoreMissingProcess :: IO () -> IO () -ignoreMissingProcess action = - action `Exception.catch` \(err :: IOException) -> - if isDoesNotExistError err - then pure () - else throwIO err - -decodeOutput - :: FilePath - -> ProverOutputStream - -> ByteString.ByteString - -> Either ProverProcessError Text -decodeOutput executable stream bytes = - case TextEncoding.decodeUtf8' bytes of - Left err -> - Left - (ProverOutputMalformedUtf8 - executable - stream - (boundedText (Text.pack (show err)))) - Right output -> - Right output - -exceptionText :: IOException -> Text -exceptionText = - Text.pack . displayException - -classifyVampireCompleted - :: VampireTaskMode - -> CompletedTranscript - -> Either VampireProtocolError CanonicalAtpOutcome -classifyVampireCompleted mode CompletedTranscript{..} = - case completedExitCode of - ExitFailure _ -> - classifyVampireProtocol mode completedExitCode [] - ExitSuccess -> do - statuses <- statusesFromCompleteStreams completedStreams - classifyVampireProtocol mode completedExitCode statuses - -statusesFromCompleteStreams - :: CompleteCapturedStreams - -> Either VampireProtocolError [VampireStatus] -statusesFromCompleteStreams CompleteCapturedStreams{..} - | Set.null malformed = - Right statuses - | otherwise = - Left (MalformedVampireStatusLines malformed) - where - (malformed, statuses) = - foldMap classifyLine - (Text.lines completedStdout <> Text.lines completedStderr) - - classifyLine line = - case parseMaybe vampireStatusParser line of - Just status -> - (mempty, [status]) - Nothing - | "SZS status" `Text.isInfixOf` line -> - (Set.singleton line, []) - | otherwise -> - mempty - -vampireStatusFromText :: Text -> VampireStatus -vampireStatusFromText = \case - "Theorem" -> StatusTheorem - "CounterSatisfiable" -> StatusCounterSatisfiable - "ContradictoryAxioms" -> StatusContradictoryAxioms - "Timeout" -> StatusTimeout - "ResourceOut" -> StatusResourceOut - "GaveUp" -> StatusGaveUp - "Unknown" -> StatusUnknown - status -> UnsupportedStatus status - --- | Parse a Vampire SZS status line. --- --- Recognizes both standard lines like: --- % SZS status Timeout for 123 --- and lines prefixed by worker ids (seen with portfolio output), e.g.: --- % (2581105)SZS status Timeout for -vampireStatusParser :: Parsec Void Text VampireStatus -vampireStatusParser = do - _ <- Char.char '%' - Char.hspace - optional do - _ <- Char.char '(' - _ <- some Char.digitChar - _ <- Char.char ')' - Char.hspace - _ <- chunk "SZS" - Char.hspace1 - _ <- chunk "status" - Char.hspace1 - status <- - takeWhile1P - (Just "SZS status") - (\character -> character /= ' ' && character /= '\t') - _ <- takeRest - pure (vampireStatusFromText status) - -nominalDiffTimeToText :: NominalDiffTime -> Text -nominalDiffTimeToText delta = - toText (nominalDiffTimeToTextBuilder delta) - -nominalDiffTimeToTextBuilder :: NominalDiffTime -> TextBuilder -nominalDiffTimeToTextBuilder delta = - case hours of - 0 -> - padded minutes - <> ":" - <> padded restSeconds - <> "." - <> padded restCentis - _ -> - padded hours - <> ":" - <> padded restMinutes - <> ":" - <> padded restSeconds - where - padded n = - if n < 10 - then char '0' <> decimal n - else decimal n - centiseconds = - truncate (100 * nominalDiffTimeToSeconds delta) :: Int - (seconds, restCentis) = divMod centiseconds 100 - (minutes, restSeconds) = divMod seconds 60 - (hours, restMinutes) = divMod minutes 60 - -timeDifferenceToText :: UTCTime -> UTCTime -> Text -timeDifferenceToText startTime endTime = - nominalDiffTimeToText (diffUTCTime endTime startTime) |