summaryrefslogtreecommitdiff
path: root/source/Test/Unit/Provers.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Test/Unit/Provers.hs')
-rw-r--r--source/Test/Unit/Provers.hs1159
1 files changed, 0 insertions, 1159 deletions
diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs
deleted file mode 100644
index 0d0cf1b..0000000
--- a/source/Test/Unit/Provers.hs
+++ /dev/null
@@ -1,1159 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Test.Unit.Provers (unitTests) where
-
-import Base hiding (Empty)
-import Checking.Backend.Problem
-import Checking.Core
-import Felix.Provers
-
-import Control.Concurrent
- ( newEmptyMVar
- , putMVar
- , takeMVar
- , threadDelay
- )
-import Control.Exception (bracket)
-import Control.Exception qualified as Exception
-import Control.Monad (when)
-import Data.IORef
- ( atomicModifyIORef'
- , newIORef
- , readIORef
- , writeIORef
- )
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Text.IO qualified as Text
-import Data.Vector qualified as Vector
-import Report.Location (Location(..))
-import System.Directory qualified as Directory
-import System.Exit (ExitCode(..))
-import System.FilePath.Posix ((</>))
-import System.Posix.Signals
- ( nullSignal
- , sigTERM
- , signalProcess
- )
-import System.Posix.Types (ProcessID)
-import System.Timeout qualified as Timeout
-import Test.Tasty
-import Test.Tasty.HUnit
-import Text.Read (readMaybe)
-import Text.Megaparsec (parseMaybe)
-import UnliftIO.Async (cancel, mapConcurrently, withAsync)
-import UnliftIO.Async qualified as Async
-
-unitTests :: TestTree
-unitTests =
- testGroup "Provers"
- [ vampireStatusParserTests
- , vampireClassifierTests
- , jobsSelectionTests
- , slowAtpReportTests
- , vampireExecutorTests
- , vampireProcessTests
- ]
-
-jobsSelectionTests :: TestTree
-jobsSelectionTests =
- testGroup "effective jobs"
- [ testCase "uses a positive override exactly" do
- detectorCalled <- newIORef False
- selected <- selectEffectiveJobs
- (effectiveJobs 3)
- (writeIORef detectorCalled True >> pure 99)
- selected `shouldBe` positiveJobs 3
- readIORef detectorCalled >>= (`shouldBe` False)
- , testCase "rounds automatic jobs to one third of detected processors" do
- for_
- [(8, 3), (16, 5), (24, 8), (32, 11)]
- \(detected, expected) -> do
- selected <- selectEffectiveJobs Nothing (pure detected)
- selected `shouldBe` positiveJobs expected
- , testCase "falls back to one after bad detection" do
- nonPositive <- selectEffectiveJobs Nothing (pure 0)
- nonPositive `shouldBe` positiveJobs 1
- failed <- selectEffectiveJobs Nothing
- (Exception.throwIO (userError "processor detection failed"))
- failed `shouldBe` positiveJobs 1
- ]
-
-slowAtpReportTests :: TestTree
-slowAtpReportTests =
- testGroup "slow ATP report"
- [ testCase "applies the threshold and retains the twelve slowest" do
- prepared <- preparedTypedTask 0
- let requestId =
- preparedVerificationRequestId
- (preparedTypedProverRequest prepared)
- task nanoseconds position =
- SlowAtpTask
- { slowAtpDuration =
- atpDurationFromNanoseconds nanoseconds
- , slowAtpOutcome = SlowAtpAccepted
- , slowAtpPosition = workPosition 1 position
- , slowAtpLocation = testLocation
- , slowAtpRequestId = requestId
- }
- report = slowAtpReportFromTasks
- ( task 4999999999 0
- : [ task (5000000000 + fromIntegral position) position
- | position <- [0..13]
- ]
- )
- slowAtpQualifyingTaskCount report `shouldBe` 14
- length (slowAtpTasks report) `shouldBe` 12
- slowAtpOmittedTaskCount report `shouldBe` 2
- atpDurationNanoseconds
- (slowAtpDuration
- (fromMaybe
- (error "slow report unexpectedly empty")
- (listToMaybe (slowAtpTasks report))))
- `shouldBe` 5000000013
- , testCase "keeps earlier source positions on equal durations" do
- prepared <- preparedTypedTask 0
- let requestId =
- preparedVerificationRequestId
- (preparedTypedProverRequest prepared)
- task position =
- SlowAtpTask
- { slowAtpDuration =
- atpDurationFromNanoseconds 5000000000
- , slowAtpOutcome = SlowAtpAccepted
- , slowAtpPosition = workPosition 1 position
- , slowAtpLocation = testLocation
- , slowAtpRequestId = requestId
- }
- report = slowAtpReportFromTasks (task <$> [1..13])
- (workPositionLocalRequestOrdinal . slowAtpPosition
- <$> slowAtpTasks report)
- `shouldBe` [1..12]
- ]
-
-vampireExecutorTests :: TestTree
-vampireExecutorTests =
- testGroup "bounded Vampire executor"
- [ testCase "records completed qualifying tasks with runtime context" do
- prepared <- preparedTypedTask 0
- clock <- scriptedClock [10, 5000000010]
- let position = workPosition 2 3
- withFakeVampire
- [ "cat >/dev/null"
- , "printf '%s\n' '% SZS status Theorem for fake'"
- ]
- \vampireCommand ->
- withVampireExecutorUsingClock
- clock
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- handle <- submitVampireRequest
- owner
- position
- testLocation
- (preparedTypedProverRequest prepared)
- awaitVampireRequest handle
- >>= assertAcceptedRequest prepared
- report <- vampireExecutorSlowAtpReport executor
- slowAtpQualifyingTaskCount report `shouldBe` 1
- case slowAtpTasks report of
- [task] -> do
- atpDurationNanoseconds
- (slowAtpDuration task)
- `shouldBe` 5000000000
- slowAtpOutcome task `shouldBe` SlowAtpAccepted
- slowAtpPosition task `shouldBe` position
- slowAtpLocation task `shouldBe` testLocation
- slowAtpRequestId task `shouldBe`
- preparedVerificationRequestId
- (preparedTypedProverRequest prepared)
- tasks ->
- assertFailure
- ("unexpected slow-task report: "
- <> show tasks)
- , testCase "does not report a cancelled partial task" do
- prepared <- preparedTypedTask 0
- clock <- scriptedClock [0, 6000000000]
- withProcessGroupFake
- defaultTimeLimit
- []
- \pidFile vampireCommand ->
- withVampireExecutorUsingClock
- clock
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- handle <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- processIds <- waitForProcessIds pidFile
- cancelVampireRequest handle
- report <- vampireExecutorSlowAtpReport executor
- slowAtpQualifyingTaskCount report `shouldBe` 0
- assertBool "cancelled report is empty"
- (null (slowAtpTasks report))
- assertProcessesGone processIds
- , testCase "opaque handles complete out of submission order" do
- prepared <- preparedTypedTask 0
- firstStarted <- newEmptyMVar
- releaseFirst <- newEmptyMVar
- withFakeVampire
- [ "cat >/dev/null"
- , "printf '%s\n' '% SZS status Theorem for fake'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 2)
- vampireCommand
- (\position _request ->
- when
- (workPositionLocalRequestOrdinal position == 1)
- (putMVar firstStarted () >> takeMVar releaseFirst))
- \executor -> withVampireRequestOwner executor \owner -> do
- first <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- takeMVar firstStarted
- second <- submitVampireRequest
- owner
- (workPosition 1 2)
- testLocation
- (preparedTypedProverRequest prepared)
- secondCompletion <- awaitVampireRequest second
- assertAcceptedRequest prepared secondCompletion
- putMVar releaseFirst ()
- firstCompletion <- awaitVampireRequest first
- assertAcceptedRequest prepared firstCompletion
- , testCase "validates request identity before a rejection" do
- submitted <- preparedTypedTask 0
- mismatched <- preparedTypedTask 1
- withFakeVampire
- [ "cat >/dev/null"
- , "printf '%s\n' '% SZS status CounterSatisfiable for fake'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- handle <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest submitted)
- outcome <- Exception.try
- (awaitPreparedVampireRequest
- (preparedTypedProverRequest mismatched)
- handle)
- case outcome of
- Left (failure :: VampireExecutorFault) ->
- assertBool
- "request mismatch is an integrity fault"
- ("wrong request id"
- `Text.isInfixOf`
- Text.pack (show failure))
- Right answer ->
- assertFailure
- ("mismatched rejection was accepted: "
- <> show answer)
- , testCase "runs requests through the bounded worker pool" do
- prepared <- preparedTypedTask 0
- withFakeVampire
- [ "previous=''"
- , "found=0"
- , "for argument in \"$@\"; do"
- , " if [ \"$previous\" = '--cores' ]; then"
- , " [ \"$argument\" = '2' ] || exit 17"
- , " found=1"
- , " fi"
- , " previous=$argument"
- , "done"
- , "[ \"$found\" = '1' ] || exit 18"
- , "cat >/dev/null"
- , "sleep 0.2"
- , "printf '%s\n' '% SZS status Theorem for fake'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 2)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- answers <- mapConcurrently
- (\ordinal ->
- runPreparedTypedProverWithExecutor
- owner
- (workPosition 1 ordinal)
- testLocation
- prepared)
- [1..4]
- traverse_ assertProved answers
- , testCase "propagates observer failure to the submitter" do
- prepared <- preparedTypedTask 0
- withFakeVampire
- [ "cat >/dev/null"
- , "printf '%s\n' '% SZS status Theorem for fake'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request ->
- Exception.throwIO
- (userError "observer failed"))
- \executor -> withVampireRequestOwner executor \owner -> do
- result <- Exception.try
- (runPreparedTypedProverWithExecutor
- owner
- (workPosition 1 1)
- testLocation
- prepared)
- case result of
- Left (failure :: VampireExecutorFault) ->
- assertBool
- "global executor fault"
- ("observer failed"
- `Text.isInfixOf`
- Text.pack (show failure))
- Right answer ->
- assertFailure
- ("observer failure was lost: "
- <> show answer)
- , testCase "cancels queued and running jobs independently" do
- prepared <- preparedTypedTask 0
- withProcessGroupFake
- defaultTimeLimit
- []
- \pidFile vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner ->
- withAsync
- (runPreparedTypedProverWithExecutor
- owner
- (workPosition 1 1)
- testLocation
- prepared)
- \running -> do
- processIds <- waitForProcessIds pidFile
- queuedSubmitted <- newEmptyMVar
- withAsync
- (do
- handle <- submitVampireRequest
- owner
- (workPosition 2 1)
- testLocation
- (preparedTypedProverRequest prepared)
- putMVar queuedSubmitted ()
- awaitPreparedVampireRequest
- (preparedTypedProverRequest prepared)
- handle)
- \queued -> do
- takeMVar queuedSubmitted
- cancel queued
- cancel running
- assertProcessesGone processIds
- , testCase "explicit cancellation completes queued and running handles" do
- prepared <- preparedTypedTask 0
- withProcessGroupFake
- defaultTimeLimit
- []
- \pidFile vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- running <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- processIds <- waitForProcessIds pidFile
- queued <- submitVampireRequest
- owner
- (workPosition 1 2)
- testLocation
- (preparedTypedProverRequest prepared)
- cancelVampireRequest queued
- awaitVampireRequest queued
- >>= assertCancelled prepared
- cancelVampireRequest running
- awaitVampireRequest running
- >>= assertCancelled prepared
- assertProcessesGone processIds
- , testCase "structured shutdown wakes waiter and full-queue submitter" do
- prepared <- preparedTypedTask 0
- withProcessGroupFake
- defaultTimeLimit
- []
- \pidFile vampireCommand -> do
- (waiter, blockedSubmit, processIds) <-
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor ->
- withVampireRequestOwner executor \owner -> do
- running <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- processIds <- waitForProcessIds pidFile
- _queuedOne <- submitVampireRequest
- owner
- (workPosition 1 2)
- testLocation
- (preparedTypedProverRequest prepared)
- _queuedTwo <- submitVampireRequest
- owner
- (workPosition 1 3)
- testLocation
- (preparedTypedProverRequest prepared)
- waiter <- Async.async
- (awaitVampireRequest running)
- submitStarted <- newEmptyMVar
- blockedSubmit <- Async.async do
- putMVar submitStarted ()
- submitVampireRequest
- owner
- (workPosition 1 4)
- testLocation
- (preparedTypedProverRequest prepared)
- takeMVar submitStarted
- pure (waiter, blockedSubmit, processIds)
- Async.waitCatch waiter >>= \case
- Right completion ->
- assertCancelled prepared completion
- Left failure ->
- assertFailure
- ("shutdown waiter failed: " <> show failure)
- Async.waitCatch blockedSubmit >>= \case
- Left failure ->
- assertBool
- "backpressured submit observes owner shutdown"
- ("VampireRequestOwnerClosed"
- `Text.isInfixOf`
- Text.pack (show failure))
- Right _handle ->
- assertFailure
- "backpressured submit survived structured shutdown"
- assertProcessesGone processIds
- , testCase "worker fault wakes a waiter and a full-queue submitter" do
- prepared <- preparedTypedTask 0
- observerEntered <- newEmptyMVar
- failObserver <- newEmptyMVar
- withFakeVampire
- [ "cat >/dev/null"
- , "printf '%s\n' '% SZS status Theorem for fake'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\position _request ->
- when
- (workPositionLocalRequestOrdinal position == 1)
- (putMVar observerEntered ()
- >> takeMVar failObserver
- >> Exception.throwIO
- (userError "fatal observer fault")))
- \executor -> withVampireRequestOwner executor \owner -> do
- first <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- takeMVar observerEntered
- _second <- submitVampireRequest
- owner
- (workPosition 1 2)
- testLocation
- (preparedTypedProverRequest prepared)
- _third <- submitVampireRequest
- owner
- (workPosition 1 3)
- testLocation
- (preparedTypedProverRequest prepared)
- withAsync
- (submitVampireRequest
- owner
- (workPosition 1 4)
- testLocation
- (preparedTypedProverRequest prepared))
- \blockedSubmit -> do
- putMVar failObserver ()
- awaitFault (awaitVampireRequest first)
- Async.waitCatch blockedSubmit >>= \case
- Left failure ->
- assertExecutorFault failure
- Right _handle ->
- assertFailure
- "full-queue submission survived executor fault"
- , testCase "declared launch failure remains request-local" do
- prepared <- preparedTypedTask 0
- let missing = vampire
- "/definitely/missing/felix-vampire"
- defaultTimeLimit
- defaultMemoryLimit
- withVampireExecutor
- (positiveJobs 1)
- missing
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- handle <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- completion <- awaitVampireRequest handle
- assertCompletionRequest prepared completion
- case vampireCompletionTerminal completion of
- VampireProcessFailed ProverLaunchFailed{} -> pure ()
- terminal ->
- assertFailure
- ("expected a local launch failure, got "
- <> show terminal)
- , testCase "protocol failure is distinct from ATP rejection" do
- prepared <- preparedTypedTask 0
- withFakeVampire
- [ "cat >/dev/null"
- , "printf '%s\n' 'completed without an SZS status'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- handle <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- completion <- awaitVampireRequest handle
- assertCompletionRequest prepared completion
- case vampireCompletionTerminal completion of
- VampireProtocolFailed{} -> pure ()
- terminal ->
- assertFailure
- ("expected a protocol terminal, got "
- <> show terminal)
- , testCase "completed rejection diagnostics are compact" do
- prepared <- preparedTypedTask 0
- let headMarker :: Text
- headMarker = "HEAD-MARKER"
- tailMarker :: Text
- tailMarker = "TAIL-MARKER"
- status :: Text
- status = "% SZS status CounterSatisfiable for fake"
- originalByteCount =
- Text.length headMarker
- + 1048576
- + Text.length tailMarker + 1
- + Text.length status + 1
- withFakeVampire
- [ "printf '%s' 'HEAD-MARKER'"
- , "head -c 1048576 /dev/zero"
- , "printf '%s\n' 'TAIL-MARKER'"
- , "printf '%s\n' '% SZS status CounterSatisfiable for fake'"
- ]
- \vampireCommand ->
- withVampireExecutor
- (positiveJobs 1)
- vampireCommand
- (\_position _request -> pure ())
- \executor -> withVampireRequestOwner executor \owner -> do
- handle <- submitVampireRequest
- owner
- (workPosition 1 1)
- testLocation
- (preparedTypedProverRequest prepared)
- completion <- awaitVampireRequest handle
- case renderVampireTerminalDiagnostic
- (vampireCompletionTerminal completion) of
- Just diagnostic -> do
- assertBool
- "retained diagnostic is bounded"
- (Text.length diagnostic < 70000)
- assertBool
- "truncation is reported"
- ("retained first and last 16 KiB"
- `Text.isInfixOf` diagnostic)
- assertBool
- "original byte count is reported"
- (("of "
- <> Text.pack
- (show originalByteCount)
- <> " bytes)")
- `Text.isInfixOf` diagnostic)
- assertBool
- "diagnostic head is retained"
- (headMarker `Text.isInfixOf` diagnostic)
- assertBool
- "diagnostic tail is retained"
- (tailMarker `Text.isInfixOf` diagnostic)
- Nothing ->
- assertFailure "expected a rejected terminal"
- ]
-
-positiveJobs :: Int -> EffectiveJobs
-positiveJobs amount =
- fromMaybe
- (error "test requested a non-positive job count")
- (effectiveJobs amount)
-
-scriptedClock :: [Word64] -> IO (IO Word64)
-scriptedClock ticks = do
- remaining <- newIORef ticks
- pure
- (atomicModifyIORef' remaining \case
- next : rest -> (rest, next)
- [] -> error "test monotonic clock exhausted")
-
-testLocation :: Location
-testLocation = Location maxBound
-
-vampireStatusParserTests :: TestTree
-vampireStatusParserTests =
- testGroup "Vampire status parser"
- [ testCase "parses canonical status lines" do
- parseMaybe
- vampireStatusParser
- "% SZS status ContradictoryAxioms for 2260"
- `shouldBe` Just StatusContradictoryAxioms
- , testCase "parses worker-prefixed status lines" do
- parseMaybe
- vampireStatusParser
- "% (2581105)SZS status Timeout for "
- `shouldBe` Just StatusTimeout
- , testCase "parses ResourceOut status" do
- parseMaybe
- vampireStatusParser
- "% SZS status ResourceOut for 2260"
- `shouldBe` Just StatusResourceOut
- , testCase "retains unsupported status values" do
- parseMaybe
- vampireStatusParser
- "% SZS status AlienResult for 2260"
- `shouldBe` Just (UnsupportedStatus "AlienResult")
- ]
-
-vampireClassifierTests :: TestTree
-vampireClassifierTests =
- testGroup "Vampire completed transcript classifier"
- [ testCase "maps each terminal status in both task modes" do
- classify DirectTask [StatusTheorem]
- `shouldBe` Right Proved
- classify DirectTask [StatusCounterSatisfiable]
- `shouldBe` Right Counterexample
- classify DirectTask [StatusContradictoryAxioms]
- `shouldBe` Right ContradictoryInput
- classify IndirectTask [StatusContradictoryAxioms]
- `shouldBe` Right Proved
- , testCase "maps every resource status to indeterminate" do
- for_ indeterminateStatuses \status ->
- classify DirectTask [status]
- `shouldBe` Right Indeterminate
- , testCase "lets a unique terminal outcome override resource statuses" do
- for_ indeterminateStatuses \status ->
- classify DirectTask [status, StatusTheorem]
- `shouldBe` Right Proved
- , testCase "accepts duplicate and equivalent terminal statuses" do
- classify DirectTask [StatusTheorem, StatusTheorem]
- `shouldBe` Right Proved
- classify
- IndirectTask
- [StatusTheorem, StatusContradictoryAxioms]
- `shouldBe` Right Proved
- , testCase "rejects every pair of different terminal outcomes" do
- for_ conflictingTerminalCases
- \(mode, statuses, outcomes) ->
- classify mode statuses
- `shouldBe`
- Left (ConflictingTerminalOutcomes outcomes)
- , testCase "is independent of status order" do
- for_ orderCases \(mode, statuses) ->
- classify mode statuses
- `shouldBe` classify mode (reverse statuses)
- , testCase "rejects unsupported status values" do
- classify
- DirectTask
- [StatusTheorem, UnsupportedStatus "AlienResult"]
- `shouldBe`
- Left
- (UnsupportedVampireStatuses
- (Set.singleton "AlienResult"))
- , testCase "rejects a successful exit without an outcome" do
- classify DirectTask []
- `shouldBe` Left MissingVampireOutcome
- , testCase "rejects every status after a nonzero exit" do
- classifyVampireProtocol
- DirectTask
- (ExitFailure 7)
- [StatusTheorem]
- `shouldBe`
- Left (UnsuccessfulVampireExit (ExitFailure 7))
- ]
-
-vampireProcessTests :: TestTree
-vampireProcessTests =
- testGroup "Vampire process boundary"
- [ testCase "classifies statuses from both completed streams" do
- answer <- runFakeVampire
- [ "printf '%s\\n' '% SZS status Timeout for fake'"
- , "printf '%s\\n' '% SZS status Theorem for fake' >&2"
- , "exit 0"
- ]
- assertProved answer
- , testCase "rejects a split-stream terminal conflict" do
- answer <- runFakeVampire
- [ "printf '%s\\n' '% SZS status Theorem for fake'"
- , "printf '%s\\n' '% SZS status CounterSatisfiable for fake' >&2"
- , "exit 0"
- ]
- assertProtocolError "ConflictingTerminalOutcomes" answer
- , testCase "rejects a theorem from a nonzero exit" do
- answer <- runFakeVampire
- [ "printf '%s\\n' '% SZS status Theorem for fake'"
- , "exit 7"
- ]
- assertProtocolError "ExitFailure 7" answer
- , testCase "rejects malformed UTF-8 output" do
- answer <- runFakeVampire
- [ "printf '\\377'"
- , "exit 0"
- ]
- case answer of
- Left
- (ProverOutputMalformedUtf8
- _
- ProverOutputStdout
- _) ->
- pure ()
- result ->
- assertFailure
- ("expected malformed stdout, got " <> show result)
- , testCase "returns a broken stdin pipe" do
- prepared <- preparedTypedTask 20000
- result <- withFakeVampire
- [ "exec 0<&-"
- , "sleep 1"
- ]
- \vampireCommand ->
- runPreparedTypedProver vampireCommand prepared
- case result of
- Left (ProverCommunicationFailed _ ProverStdin _) ->
- pure ()
- processResult ->
- assertFailure
- ("expected a communication failure, got "
- <> show processResult)
- , testCase "drains output while feeding prover input" do
- prepared <- preparedTypedTask 20000
- guardedAnswer <- Timeout.timeout
- 30000000
- (withFakeVampire
- [ "head -c 1048576 /dev/zero &"
- , "head -c 1048576 /dev/zero >&2 &"
- , "wait"
- , "printf '\\n'"
- , "printf '\\n' >&2"
- , "cat >/dev/null"
- , "printf '%s\\n' '% SZS status Theorem for fake'"
- , "exit 0"
- ]
- \vampireCommand -> do
- runPreparedTypedProver vampireCommand prepared)
- case guardedAnswer of
- Nothing ->
- assertFailure "prover communication did not finish"
- Just answer ->
- assertProved answer
- , testCase "reports signal termination separately" do
- prepared <- preparedTypedTask 0
- result <- withFakeVampire
- [ "kill -TERM $$"
- ]
- \vampireCommand ->
- runPreparedTypedProver vampireCommand prepared
- case result of
- Left
- (ProverTerminatedBySignal
- _
- signalNumber
- _) ->
- assertEqual
- "termination signal"
- (fromIntegral sigTERM)
- signalNumber
- processResult ->
- assertFailure
- ("expected signal termination, got "
- <> show processResult)
- , testCase "deadline terminates and reaps the process group" do
- prepared <- preparedTypedTask 0
- withProcessGroupFake
- (Seconds 0)
- []
- \pidFile vampireCommand -> do
- result <-
- runPreparedTypedProver vampireCommand prepared
- assertTimedOut result
- processIds <- readProcessIds pidFile
- assertProcessesGone processIds
- , testCase "output exhaustion terminates the process group" do
- prepared <- preparedTypedTask 0
- withProcessGroupFake
- defaultTimeLimit
- [ "head -c 33554432 /dev/zero"
- ]
- \pidFile vampireCommand -> do
- result <-
- runPreparedTypedProver vampireCommand prepared
- case result of
- Left
- (ProverOutputLimitExceeded
- _
- ProverOutputStdout
- _) ->
- pure ()
- processResult ->
- assertFailure
- ("expected stdout limit exhaustion, got "
- <> show processResult)
- processIds <- readProcessIds pidFile
- assertProcessesGone processIds
- , testCase "cancellation terminates and reaps the process group" do
- prepared <- preparedTypedTask 0
- withProcessGroupFake
- defaultTimeLimit
- []
- \pidFile vampireCommand ->
- withAsync
- (runPreparedTypedProver vampireCommand prepared)
- \worker -> do
- processIds <- waitForProcessIds pidFile
- cancel worker
- assertProcessesGone processIds
- ]
-
-classify
- :: VampireTaskMode
- -> [VampireStatus]
- -> Either VampireProtocolError CanonicalAtpOutcome
-classify mode =
- classifyVampireProtocol mode ExitSuccess
-
-indeterminateStatuses :: [VampireStatus]
-indeterminateStatuses =
- [ StatusTimeout
- , StatusResourceOut
- , StatusGaveUp
- , StatusUnknown
- ]
-
-conflictingTerminalCases
- :: [(VampireTaskMode, [VampireStatus], Set CanonicalAtpOutcome)]
-conflictingTerminalCases =
- [ ( DirectTask
- , [StatusTheorem, StatusCounterSatisfiable]
- , Set.fromList [Proved, Counterexample]
- )
- , ( DirectTask
- , [StatusTheorem, StatusContradictoryAxioms]
- , Set.fromList [Proved, ContradictoryInput]
- )
- , ( DirectTask
- , [StatusCounterSatisfiable, StatusContradictoryAxioms]
- , Set.fromList [Counterexample, ContradictoryInput]
- )
- , ( IndirectTask
- , [StatusTheorem, StatusCounterSatisfiable]
- , Set.fromList [Proved, Counterexample]
- )
- , ( IndirectTask
- , [StatusCounterSatisfiable, StatusContradictoryAxioms]
- , Set.fromList [Proved, Counterexample]
- )
- ]
-
-orderCases :: [(VampireTaskMode, [VampireStatus])]
-orderCases =
- [ (DirectTask, StatusTheorem : indeterminateStatuses)
- , (DirectTask, [StatusTheorem, StatusCounterSatisfiable])
- , (IndirectTask, [StatusTheorem, StatusContradictoryAxioms])
- , (DirectTask, [UnsupportedStatus "B", UnsupportedStatus "A"])
- ]
-
-assertProved
- :: Either ProverProcessError ProverAnswer
- -> Assertion
-assertProved = \case
- Right Yes ->
- pure ()
- answer ->
- assertFailure ("expected a proof, got " <> show answer)
-
-assertAcceptedRequest
- :: PreparedTypedProverTask ref local origin global
- -> VampireCompletion
- -> Assertion
-assertAcceptedRequest prepared completion = do
- assertCompletionRequest prepared completion
- case vampireCompletionTerminal completion of
- VampireAccepted -> pure ()
- terminal ->
- assertFailure ("expected an accepted terminal, got " <> show terminal)
-
-assertCompletionRequest
- :: PreparedTypedProverTask ref local origin global
- -> VampireCompletion
- -> Assertion
-assertCompletionRequest prepared completion =
- vampireCompletionRequestId completion
- `shouldBe`
- preparedVerificationRequestId
- (preparedTypedProverRequest prepared)
-
-assertCancelled
- :: PreparedTypedProverTask ref local origin global
- -> VampireCompletion
- -> Assertion
-assertCancelled prepared completion = do
- assertCompletionRequest prepared completion
- vampireCompletionTerminal completion `shouldBe` VampireCancelled
-
-awaitFault :: IO value -> Assertion
-awaitFault action = do
- result <- Exception.try action
- case result of
- Left failure -> assertExecutorFault failure
- Right _value -> assertFailure "expected a global executor fault"
-
-assertExecutorFault :: Exception.SomeException -> Assertion
-assertExecutorFault failure =
- case Exception.fromException failure :: Maybe VampireExecutorFault of
- Just _fault -> pure ()
- Nothing ->
- assertFailure
- ("expected VampireExecutorFault, got " <> show failure)
-
-assertProtocolError
- :: Text
- -> Either ProverProcessError ProverAnswer
- -> Assertion
-assertProtocolError expected = \case
- Right (Error _label diagnostic) ->
- assertBool
- ( "expected protocol error containing "
- <> show expected
- <> ", got "
- <> show diagnostic
- )
- (expected `Text.isInfixOf` diagnostic)
- answer ->
- assertFailure ("expected a protocol error, got " <> show answer)
-
-assertTimedOut
- :: Either ProverProcessError a
- -> Assertion
-assertTimedOut = \case
- Left ProverTimedOut{} ->
- pure ()
- result ->
- assertFailure ("expected prover timeout, got " <> showResult result)
- where
- showResult = \case
- Left err ->
- show err
- Right _ ->
- "successful process result"
-
-withProcessGroupFake
- :: TimeLimit
- -> [String]
- -> (FilePath -> Vampire -> IO a)
- -> IO a
-withProcessGroupFake timeLimit body action =
- withFakeVampireIn
- (\temp ->
- let pidFile = temp </> "process-ids"
- in [ "trap '' TERM"
- , "sleep 60 &"
- , "printf '%s %s\\n' \"$$\" \"$!\" > " <> pidFile
- ]
- <> body
- <> ["wait"])
- timeLimit
- \temp ->
- action (temp </> "process-ids")
-
-readProcessIds :: FilePath -> IO [ProcessID]
-readProcessIds path = do
- contents <- Text.readFile path
- case traverse
- (readMaybe . Text.unpack)
- (Text.words contents) of
- Just processIds@[_leader, _descendant] ->
- pure processIds
- _ ->
- assertFailure
- ("expected leader and descendant process ids, got "
- <> show contents)
-
-waitForProcessIds :: FilePath -> IO [ProcessID]
-waitForProcessIds path = do
- guarded <- Timeout.timeout 10000000 loop
- case guarded of
- Just processIds ->
- pure processIds
- Nothing ->
- assertFailure "fake prover did not publish its process ids"
- where
- loop = do
- exists <- Directory.doesFileExist path
- if exists
- then readProcessIds path
- else do
- threadDelay 10000
- loop
-
-assertProcessesGone :: [ProcessID] -> Assertion
-assertProcessesGone processIds = do
- guarded <- Timeout.timeout 10000000 loop
- case guarded of
- Just () ->
- pure ()
- Nothing ->
- assertFailure
- ("supervisor left processes running: "
- <> show processIds)
- where
- loop = do
- alive <- traverse processIsAlive processIds
- if or alive
- then do
- threadDelay 10000
- loop
- else pure ()
-
-processIsAlive :: ProcessID -> IO Bool
-processIsAlive processId =
- (signalProcess nullSignal processId >> pure True)
- `Exception.catch` \(err :: Exception.IOException) ->
- if isDoesNotExistError err
- then pure False
- else throwIO err
-
-runFakeVampire
- :: [String]
- -> IO (Either ProverProcessError ProverAnswer)
-runFakeVampire scriptLines =
- withFakeVampire
- (["cat >/dev/null"] <> scriptLines)
- \vampireCommand -> do
- prepared <- preparedTypedTask 0
- runPreparedTypedProver vampireCommand prepared
-
-withFakeVampire
- :: [String]
- -> (Vampire -> IO a)
- -> IO a
-withFakeVampire scriptLines action =
- withFakeVampireIn
- (const scriptLines)
- defaultTimeLimit
- (const action)
-
-withFakeVampireIn
- :: (FilePath -> [String])
- -> TimeLimit
- -> (FilePath -> Vampire -> IO a)
- -> IO a
-withFakeVampireIn makeScript timeLimit action =
- withTemporaryDirectory "felix-fake-vampire" \temp -> do
- let executablePath = temp </> "vampire"
- writeFile executablePath
- (unlines
- ( [ "#!/bin/sh"
- ]
- <> makeScript temp
- ))
- permissions <- Directory.getPermissions executablePath
- Directory.setPermissions executablePath
- (Directory.setOwnerExecutable True permissions)
- action
- temp
- (vampire
- executablePath
- timeLimit
- defaultMemoryLimit)
-
-withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a
-withTemporaryDirectory template =
- bracket create Directory.removePathForcibly
- where
- create = do
- systemTemp <- Directory.getTemporaryDirectory
- (path, handle) <- openTempFile systemTemp template
- hClose handle
- Directory.removeFile path
- Directory.createDirectory path
- pure path
-
-shouldBe :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion
-shouldBe =
- flip (assertEqual "")
-
-preparedTypedTask
- :: Int
- -> IO (PreparedTypedProverTask Int Void Void Void)
-preparedTypedTask factCount = do
- checked <- expectRight
- (checkScopedCanonicalCore
- (const Nothing)
- []
- propositionTerm)
- proposition <- expectRight
- (supportedProposition Vector.empty checked)
- capability <- expectRight
- (classifySupportedProposition (const Nothing) proposition)
- let facts =
- Vector.generate
- factCount
- (\reference ->
- typedBackendFact reference proposition capability)
- problem <- expectRight
- (planTypedProblem
- (const Nothing)
- facts
- proposition
- []
- []
- FirstOrderLocals
- ExplicitHigherOrderJustification)
- expectRight (prepareTypedProverTask DirectTask problem)
- where
- propositionTerm =
- CEq TySet
- (CIntrinsic Empty)
- (CIntrinsic Empty)
-
-expectRight :: Show error => Either error value -> IO value
-expectRight = \case
- Left failure ->
- assertFailure (show failure) >> fail "unreachable"
- Right value ->
- pure value
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:49:04 +0000