diff options
Diffstat (limited to 'source/Test/Unit/Provers.hs')
| -rw-r--r-- | source/Test/Unit/Provers.hs | 287 |
1 files changed, 242 insertions, 45 deletions
diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs index d852755..22a6b5b 100644 --- a/source/Test/Unit/Provers.hs +++ b/source/Test/Unit/Provers.hs @@ -2,24 +2,24 @@ module Test.Unit.Provers (unitTests) where -import Base +import Base hiding (Empty) +import Checking.Backend.Problem +import Checking.Core import Provers -import Report.Location (pattern Nowhere) -import Syntax.Internal - ( Directness(..) - , Hypothesis(..) - , Marker(..) - , Task(..) - , pattern Top - ) import Control.Concurrent (threadDelay) import Control.Exception (bracket) import Control.Exception qualified as Exception import Control.Monad.Logger (runNoLoggingT) +import Data.IORef + ( 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 System.Directory qualified as Directory import System.Exit (ExitCode(..)) import System.FilePath.Posix ((</>)) @@ -34,16 +34,162 @@ import Test.Tasty import Test.Tasty.HUnit import Text.Read (readMaybe) import Text.Megaparsec (parseMaybe) -import UnliftIO.Async (cancel, withAsync) +import UnliftIO.Async (cancel, mapConcurrently, withAsync) unitTests :: TestTree unitTests = testGroup "Provers" [ vampireStatusParserTests , vampireClassifierTests + , jobsSelectionTests + , 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) + jobsSelectionEffectiveJobs selected + `shouldBe` positiveJobs 3 + jobsSelectionDetectedProcessors selected `shouldBe` Nothing + jobsSelectionWasOverridden selected `shouldBe` True + readIORef detectorCalled >>= (`shouldBe` False) + , testCase "leaves one detected logical processor free" do + selected <- selectEffectiveJobs Nothing (pure 8) + jobsSelectionEffectiveJobs selected + `shouldBe` positiveJobs 7 + jobsSelectionDetectedProcessors selected `shouldBe` Just 8 + jobsSelectionWasOverridden selected `shouldBe` False + , testCase "falls back to one after bad detection" do + nonPositive <- selectEffectiveJobs Nothing (pure 0) + jobsSelectionEffectiveJobs nonPositive + `shouldBe` positiveJobs 1 + failed <- selectEffectiveJobs Nothing + (Exception.throwIO (userError "processor detection failed")) + jobsSelectionEffectiveJobs failed + `shouldBe` positiveJobs 1 + jobsSelectionDetectedProcessors failed `shouldBe` Nothing + ] + +vampireExecutorTests :: TestTree +vampireExecutorTests = + testGroup "bounded Vampire executor" + [ testCase "bounds live one-core processes" do + prepared <- preparedTypedTask 0 + withFakeVampire + [ "previous=''" + , "found=0" + , "for argument in \"$@\"; do" + , " if [ \"$previous\" = '--cores' ]; then" + , " [ \"$argument\" = '1' ] || 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 -> do + answers <- mapConcurrently + (\ordinal -> + runNoLoggingT + (runPreparedTypedProverWithExecutor + executor + (workPosition 1 ordinal) + prepared)) + [1..4] + traverse_ assertProved answers + observed <- vampireExecutorObservation executor + vampireExecutorRunCount observed `shouldBe` 4 + vampireExecutorMaximumLiveCount observed + `shouldBe` 2 + , 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 -> do + result <- Exception.try + (runNoLoggingT + (runPreparedTypedProverWithExecutor + executor + (workPosition 1 1) + prepared)) + case result of + Left (failure :: Exception.IOException) -> + assertBool + "observer exception" + ("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 -> + withAsync + (runNoLoggingT + (runPreparedTypedProverWithExecutor + executor + (workPosition 1 1) + prepared)) + \running -> do + processIds <- waitForProcessIds pidFile + withAsync + (runNoLoggingT + (runPreparedTypedProverWithExecutor + executor + (workPosition 2 1) + prepared)) + \queued -> do + waitForSubmittedCount executor 2 + cancel queued + cancel running + observed <- vampireExecutorObservation + executor + vampireExecutorSubmittedCount observed + `shouldBe` 2 + vampireExecutorRunCount observed + `shouldBe` 1 + assertProcessesGone processIds + ] + +positiveJobs :: Int -> EffectiveJobs +positiveJobs amount = + fromMaybe + (error "test requested a non-positive job count") + (effectiveJobs amount) + vampireStatusParserTests :: TestTree vampireStatusParserTests = testGroup "Vampire status parser" @@ -165,12 +311,14 @@ vampireProcessTests = assertFailure ("expected malformed stdout, got " <> show result) , testCase "returns a broken stdin pipe" do + prepared <- preparedTypedTask 20000 result <- withFakeVampire [ "exec 0<&-" , "sleep 1" ] \vampireCommand -> - runVampireProcess vampireCommand largeTask + runNoLoggingT + (runPreparedTypedProver vampireCommand prepared) case result of Left (ProverCommunicationFailed _ ProverStdin _) -> pure () @@ -179,6 +327,7 @@ vampireProcessTests = ("expected a communication failure, got " <> show processResult) , testCase "drains output while feeding prover input" do + prepared <- preparedTypedTask 20000 guardedAnswer <- Timeout.timeout 30000000 (withFakeVampire @@ -192,21 +341,23 @@ vampireProcessTests = , "exit 0" ] \vampireCommand -> do - (_location, _formula, answer) <- - runNoLoggingT - (runProver vampireCommand largeTask) - pure answer) + runNoLoggingT + (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 -> - runVampireProcess vampireCommand directTask + runNoLoggingT + (runPreparedTypedProver vampireCommand prepared) case result of Left (ProverTerminatedBySignal @@ -222,27 +373,31 @@ vampireProcessTests = ("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 <- - runVampireProcess - vampireCommand - directTask + runNoLoggingT + (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 <- - runVampireProcess - vampireCommand - directTask + runNoLoggingT + (runPreparedTypedProver + vampireCommand + prepared) case result of Left (ProverOutputLimitExceeded @@ -257,14 +412,16 @@ vampireProcessTests = processIds <- readProcessIds pidFile assertProcessesGone processIds , testCase "cancellation terminates and reaps the process group" do + prepared <- preparedTypedTask 0 withProcessGroupFake defaultTimeLimit [] \pidFile vampireCommand -> withAsync - (runVampireProcess - vampireCommand - directTask) + (runNoLoggingT + (runPreparedTypedProver + vampireCommand + prepared)) \worker -> do processIds <- waitForProcessIds pidFile cancel worker @@ -408,6 +565,24 @@ waitForProcessIds path = do threadDelay 10000 loop +waitForSubmittedCount :: VampireExecutor -> Int -> Assertion +waitForSubmittedCount executor expected = do + guarded <- Timeout.timeout 10000000 loop + case guarded of + Just () -> + pure () + Nothing -> + assertFailure + ("executor did not submit " <> show expected <> " requests") + where + loop = do + observed <- vampireExecutorObservation executor + if vampireExecutorSubmittedCount observed >= expected + then pure () + else do + threadDelay 10000 + loop + assertProcessesGone :: [ProcessID] -> Assertion assertProcessesGone processIds = do guarded <- Timeout.timeout 10000000 loop @@ -442,9 +617,9 @@ runFakeVampire scriptLines = withFakeVampire (["cat >/dev/null"] <> scriptLines) \vampireCommand -> do - (_location, _formula, answer) <- runNoLoggingT - (runProver vampireCommand directTask) - pure answer + prepared <- preparedTypedTask 0 + runNoLoggingT + (runPreparedTypedProver vampireCommand prepared) withFakeVampire :: [String] @@ -496,21 +671,43 @@ shouldBe :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion shouldBe = flip (assertEqual "") -directTask :: Task -directTask = - Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = Marker "dummy" - , taskLocation = Nowhere - , taskConjecture = Top - } +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 + [] + [] + ExplicitGlobalPremises + FirstOrderLocals) + expectRight (prepareTypedProverTask DirectTask problem) + where + propositionTerm = + CEq TySet + (CIntrinsic Empty) + (CIntrinsic Empty) -largeTask :: Task -largeTask = - directTask - { taskHypotheses = - replicate - 20000 - (Hypothesis (Marker "large") Top) - } +expectRight :: Show error => Either error value -> IO value +expectRight = \case + Left failure -> + assertFailure (show failure) >> fail "unreachable" + Right value -> + pure value |