diff options
Diffstat (limited to 'source/Felix/Provers.hs')
| -rw-r--r-- | source/Felix/Provers.hs | 1860 |
1 files changed, 1860 insertions, 0 deletions
diff --git a/source/Felix/Provers.hs b/source/Felix/Provers.hs new file mode 100644 index 0000000..16ef655 --- /dev/null +++ b/source/Felix/Provers.hs @@ -0,0 +1,1860 @@ +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +module Felix.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 + , selectEffectiveJobs + , WorkPosition + , workPosition + , workPositionModuleOrdinal + , workPositionLocalRequestOrdinal + , VampireExecutor + , VampireExecutorFault + , VampireRequestOwner + , VampireHandle + , VampireTerminal(..) + , renderVampireTerminalDiagnostic + , VampireCompletion + , vampireCompletionRequestId + , vampireCompletionTerminal + , AtpDuration + , atpDurationNanoseconds + , atpDurationFromNanoseconds + , SlowAtpOutcome(..) + , SlowAtpTask(..) + , SlowAtpReport(..) + , slowAtpOmittedTaskCount + , slowAtpReportFromTasks + , withVampireExecutor + , withVampireExecutorUsingClock + , withVampireRequestOwner + , submitVampireRequest + , awaitVampireRequest + , awaitPreparedVampireRequest + , cancelVampireRequest + , runPreparedTypedProverWithExecutor + , vampireExecutorSlowAtpReport + ) where + +import Base +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem +import Felix.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 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.Map.Strict qualified as Map +import Data.Ord (Down(..)) +import Data.Text qualified as Text +import Data.Text.Encoding qualified as TextEncoding +import Data.Text.Encoding.Error qualified as TextEncodingError +import Numeric.Natural (Natural) +import Felix.Report.Location (Location) +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 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 + +-- | 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 EffectiveJobs +selectEffectiveJobs override detectProcessors = + case override of + Just selected -> + pure selected + 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 (EffectiveJobs automaticJobs) + where + fallback = pure (EffectiveJobs 1) + +-- | 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 + +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) + +preparedTypedProverLogicalProblem + :: PreparedTypedProverTask ref local origin global + -> TypedProblem ref local origin global +preparedTypedProverLogicalProblem + (PreparedTypedProverTask + problem + _request) = + problem + +preparedTypedProverRequest + :: PreparedTypedProverTask ref local origin global + -> PreparedVerificationRequest +preparedTypedProverRequest + (PreparedTypedProverTask + _problem + request) = + 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 + :: Vampire + -> PreparedTypedProverTask ref local origin global + -> IO (Either ProverProcessError ProverAnswer) +runPreparedTypedProver + vampireCommand = + runPreparedTypedProverWithObserver + (\_request -> pure ()) + vampireCommand + +runPreparedTypedProverWithObserver + :: (PreparedVerificationRequest -> IO ()) + -> Vampire + -> PreparedTypedProverTask ref local origin global + -> IO (Either ProverProcessError ProverAnswer) +runPreparedTypedProverWithObserver + observer + vampireCommand + (PreparedTypedProverTask + _problem + preparedRequest) = do + terminal <- runPreparedVerificationTerminal + observer + vampireCommand + preparedRequest + completionProverResult + preparedRequest + (VampireCompletion + (preparedVerificationRequestId preparedRequest) + terminal) + +-- | 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 ()) + , executorMonotonicClock :: !(IO Word64) + , executorSlowAtpAccumulator :: !(TVar SlowAtpAccumulator) + } + +data ExecutorJob = ExecutorJob + { executorJobPosition :: !WorkPosition + , executorJobLocation :: !Location + , 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 + , vampireHandleRequestId :: !Authority.PreparedRequestId + , vampireHandleCancelled :: !(TVar Bool) + , vampireHandleStarted :: !(TVar Bool) + , vampireHandleCompletion :: !(TMVar VampireCompletion) + } + +data VampireTerminal + = VampireAccepted + | VampireRejected !CanonicalAtpRejection !BoundedDiagnostic + | VampireProtocolFailed !BoundedDiagnostic + | VampireProcessFailed !ProverProcessError + | VampireCancelled + deriving (Show, Eq) + +data VampireCompletion = VampireCompletion + { vampireCompletionRequestId :: !Authority.PreparedRequestId + , vampireCompletionTerminal :: !VampireTerminal + } + deriving (Show, Eq) + +-- | Monotonic executor wall time in nanoseconds. +newtype AtpDuration = AtpDuration Word64 + deriving (Show, Eq, Ord) + +atpDurationNanoseconds :: AtpDuration -> Word64 +atpDurationNanoseconds (AtpDuration nanoseconds) = nanoseconds + +atpDurationFromNanoseconds :: Word64 -> AtpDuration +atpDurationFromNanoseconds = AtpDuration + +data SlowAtpOutcome + = SlowAtpAccepted + | SlowAtpRejected !CanonicalAtpRejection + | SlowAtpProtocolFailed + | SlowAtpProcessFailed + deriving (Show, Eq) + +data SlowAtpTask = SlowAtpTask + { slowAtpDuration :: !AtpDuration + , slowAtpOutcome :: !SlowAtpOutcome + , slowAtpPosition :: !WorkPosition + , slowAtpLocation :: !Location + , slowAtpRequestId :: !Authority.PreparedRequestId + } + deriving (Show, Eq) + +data SlowAtpReport = SlowAtpReport + { slowAtpQualifyingTaskCount :: !Int + , slowAtpTasks :: ![SlowAtpTask] + } + deriving (Show, Eq) + +slowAtpOmittedTaskCount :: SlowAtpReport -> Int +slowAtpOmittedTaskCount report = + slowAtpQualifyingTaskCount report - length (slowAtpTasks report) + +data SlowAtpRank = SlowAtpRank + !AtpDuration + !(Down WorkPosition) + deriving (Eq, Ord) + +data SlowAtpAccumulator = SlowAtpAccumulator + { slowAtpAccumulatorQualifyingTaskCount :: !Int + , slowAtpAccumulatorRetained :: !(Map.Map SlowAtpRank SlowAtpTask) + } + +slowAtpThreshold :: AtpDuration +slowAtpThreshold = AtpDuration 5000000000 + +slowAtpRetainedLimit :: Int +slowAtpRetainedLimit = 12 + +emptySlowAtpAccumulator :: SlowAtpAccumulator +emptySlowAtpAccumulator = SlowAtpAccumulator 0 Map.empty + +recordSlowAtpTask + :: SlowAtpTask + -> SlowAtpAccumulator + -> SlowAtpAccumulator +recordSlowAtpTask task accumulator + | slowAtpDuration task < slowAtpThreshold = accumulator + | otherwise = + accumulator + { slowAtpAccumulatorQualifyingTaskCount = + slowAtpAccumulatorQualifyingTaskCount accumulator + 1 + , slowAtpAccumulatorRetained = bounded + } + where + rank = SlowAtpRank + (slowAtpDuration task) + (Down (slowAtpPosition task)) + inserted = Map.insert rank task (slowAtpAccumulatorRetained accumulator) + bounded + | Map.size inserted > slowAtpRetainedLimit = Map.deleteMin inserted + | otherwise = inserted + +finalizeSlowAtpReport :: SlowAtpAccumulator -> SlowAtpReport +finalizeSlowAtpReport accumulator = + SlowAtpReport + { slowAtpQualifyingTaskCount = + slowAtpAccumulatorQualifyingTaskCount accumulator + , slowAtpTasks = + snd <$> Map.toDescList (slowAtpAccumulatorRetained accumulator) + } + +-- | Pure report construction used by policy tests and the executor. +slowAtpReportFromTasks :: [SlowAtpTask] -> SlowAtpReport +slowAtpReportFromTasks = + finalizeSlowAtpReport + . foldl' (flip recordSlowAtpTask) emptySlowAtpAccumulator + +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 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 + +-- | 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 = + withVampireExecutorUsingClock + getMonotonicTimeNSec + selected + command + observer + action + +-- | Executor constructor with an injected monotonic clock for focused timing +-- policy tests. Production callers use 'withVampireExecutor'. +withVampireExecutorUsingClock + :: IO Word64 + -> EffectiveJobs + -> Vampire + -> (WorkPosition -> PreparedVerificationRequest -> IO ()) + -> (VampireExecutor -> IO value) + -> IO value +withVampireExecutorUsingClock clock 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 + slowTasks <- newTVarIO emptySlowAtpAccumulator + let executor = + VampireExecutor + { executorQueue = queue + , executorState = state + , executorNextHandle = nextHandle + , executorCommand = command + , executorRequestObserver = observer + , executorMonotonicClock = clock + , executorSlowAtpAccumulator = slowTasks + } + 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 + :: VampireRequestOwner + -> WorkPosition + -> Location + -> PreparedTypedProverTask ref local origin global + -> IO (Either ProverProcessError ProverAnswer) +runPreparedTypedProverWithExecutor + owner + position + location + (PreparedTypedProverTask + _problem + preparedRequest) = do + handle <- submitVampireRequest owner position location preparedRequest + awaitPreparedVampireRequest preparedRequest handle + `Exception.onException` cancelVampireRequest handle + +vampireExecutorSlowAtpReport :: VampireExecutor -> IO SlowAtpReport +vampireExecutorSlowAtpReport executor = + finalizeSlowAtpReport + <$> readTVarIO (executorSlowAtpAccumulator executor) + +submitVampireRequest + :: VampireRequestOwner + -> WorkPosition + -> Location + -> PreparedVerificationRequest + -> IO VampireHandle +submitVampireRequest owner position location 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 + , vampireHandleRequestId = + preparedVerificationRequestId request + , vampireHandleCancelled = cancelled + , vampireHandleStarted = started + , vampireHandleCompletion = completion + } + job = + ExecutorJob + { executorJobPosition = position + , executorJobLocation = location + , executorJobRequest = request + , executorJobCancelled = cancelled + , executorJobStarted = started + , executorJobCompletion = completion + } + writeTBQueue (executorQueue executor) job + writeTVar + (requestOwnerState owner) + (RequestOwnerOpen (IntMap.insert ordinal acquired owned)) + pure acquired + 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 every +-- completion before any caller may interpret its terminal outcome. +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 completion = + VampireCompletion + (vampireHandleRequestId handle) + VampireCancelled + _ <- Exception.evaluate completion + atomically do + writeTVar (vampireHandleCancelled handle) True + started <- readTVar (vampireHandleStarted handle) + unless started + (void + (publishVampireTerminalSTM + (vampireHandleCompletion handle) + 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 + (preparedVerificationRequestId + (executorJobRequest job)) + (executorJobCompletion job) + terminal + JobCancelled -> do + cancel running + void (waitCatch running) + publishVampireTerminal + (preparedVerificationRequestId + (executorJobRequest job)) + (executorJobCompletion job) + VampireCancelled + JobExecutorStopped -> do + cancel running + void (waitCatch running) + +timedExecutorRun + :: VampireExecutor + -> ExecutorJob + -> IO VampireTerminal +timedExecutorRun executor job = Exception.mask \restore -> do + started <- executorMonotonicClock executor + terminal <- restore + (runPreparedVerificationTerminal + (executorRequestObserver executor (executorJobPosition job)) + (executorCommand executor) + (executorJobRequest job)) + finished <- executorMonotonicClock executor + let task = SlowAtpTask + { slowAtpDuration = AtpDuration (finished - started) + , slowAtpOutcome = slowAtpOutcomeFromTerminal terminal + , slowAtpPosition = executorJobPosition job + , slowAtpLocation = executorJobLocation job + , slowAtpRequestId = + preparedVerificationRequestId (executorJobRequest job) + } + atomically + (modifyTVar' + (executorSlowAtpAccumulator executor) + (recordSlowAtpTask task)) + pure terminal + +slowAtpOutcomeFromTerminal :: VampireTerminal -> SlowAtpOutcome +slowAtpOutcomeFromTerminal = \case + VampireAccepted -> SlowAtpAccepted + VampireRejected rejection _diagnostic -> SlowAtpRejected rejection + VampireProtocolFailed{} -> SlowAtpProtocolFailed + VampireProcessFailed{} -> SlowAtpProcessFailed + VampireCancelled -> + impossible "cancelled Vampire task was recorded as completed" + +publishVampireTerminal + :: Authority.PreparedRequestId + -> TMVar VampireCompletion + -> VampireTerminal + -> IO () +publishVampireTerminal requestId completionCell terminal = do + let completion = VampireCompletion requestId terminal + _ <- Exception.evaluate completion + void (atomically (publishVampireTerminalSTM completionCell completion)) + +publishVampireTerminalSTM + :: TMVar VampireCompletion + -> VampireCompletion + -> STM Bool +publishVampireTerminalSTM = tryPutTMVar + +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 + 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 = do + unless (actualId == expectedId) + (Exception.throwIO + (VampireExecutorFault + "Vampire completion has the wrong request id")) + case vampireCompletionTerminal completion of + VampireAccepted -> + pure + (Right + (ProvedAnswer + (AcceptedVampireRun actualId))) + 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 + expectedId = preparedVerificationRequestId request + actualId = vampireCompletionRequestId completion + 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) |