summaryrefslogtreecommitdiff
path: root/source/Felix/Test/Unit/Provers.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Felix/Test/Unit/Provers.hs')
-rw-r--r--source/Felix/Test/Unit/Provers.hs1159
1 files changed, 1159 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/Provers.hs b/source/Felix/Test/Unit/Provers.hs
new file mode 100644
index 0000000..f1e3cc1
--- /dev/null
+++ b/source/Felix/Test/Unit/Provers.hs
@@ -0,0 +1,1159 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Felix.Test.Unit.Provers (unitTests) where
+
+import Base hiding (Empty)
+import Felix.Checking.Backend.Problem
+import Felix.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 Felix.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:58:57 +0000