From 1033f156472f508d391e5b329ffd3c0061309a28 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 17 Dec 2024 12:03:49 +0800 Subject: [PATCH] Fix detection of Marabou timeouts --- ChangeLog.md | 4 +++ .../src/Vehicle/Verify/Specification/IO.hs | 27 ++++++++++++++++--- .../Vehicle/Verify/Specification/Status.hs | 27 ++++--------------- vehicle/src/Vehicle/Verify/Verifier/Core.hs | 2 +- .../src/Vehicle/Verify/Verifier/Marabou.hs | 8 +++--- .../compile/acasXu/MarabouVerify.out.golden | 4 +-- .../compile/issue641/MarabouVerify.err.golden | 3 ++- .../compile/issue641/MarabouVerify.out.golden | 2 +- .../TestVerify.out.golden | 2 +- .../windController/MarabouVerify.out.golden | 2 +- .../windController/TestVerify.out.golden | 2 +- .../verifierTimeout/TestVerify.out.golden | 6 +++-- 12 files changed, 51 insertions(+), 38 deletions(-) diff --git a/ChangeLog.md b/ChangeLog.md index 8ab9ef9c4..0add71c3c 100644 --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,9 @@ # Changelog for Vehicle +## Version 0.16.1 + +* Fixed detection of Marabou timeouts. + ## Version 0.16 * Decreased type-checking time by ~50% diff --git a/vehicle/src/Vehicle/Verify/Specification/IO.hs b/vehicle/src/Vehicle/Verify/Specification/IO.hs index 484f15f12..c4de63e12 100644 --- a/vehicle/src/Vehicle/Verify/Specification/IO.hs +++ b/vehicle/src/Vehicle/Verify/Specification/IO.hs @@ -447,7 +447,6 @@ verifyQuery queryMetaData@(QueryMetaData queryAddress metaNetwork reconstruction (verifierSettings, verificationCache, progressBar) <- ask let queryFile = calculateQueryFileName verificationCache queryAddress - tell (Sum 1) errorOrResult <- runExceptT $ do result <- invokeVerifier verifierSettings metaNetwork queryFile liftIO $ incProgress progressBar 1 @@ -467,7 +466,9 @@ verifyQuery queryMetaData@(QueryMetaData queryAddress metaNetwork reconstruction case errorOrResult of Left err -> throwError (queryMetaData, err) - Right result -> return result + Right result -> do + tell (Sum 1) + return result invokeVerifier :: (MonadVerifyQuery m) => @@ -575,8 +576,28 @@ outputPropertyResult :: m () outputPropertyResult verifierSettings verificationCache address result = do let VerifierSettings {..} = verifierSettings - VIO.writeStdoutLn (layoutAsText $ " result: " <> pretty result) + + -- Write the result to the cache writePropertyResult verificationCache address (isVerified result) + + -- Print result to command line + let verifierName = pretty (verifierID verifier) + let (verified, evidenceText) = case result of + PropertyCompleted maybeResult -> do + case maybeResult of + Trivial status -> (Just status, "(trivial)") + NonTrivial (negated, status) -> do + let witnessText = if negated then "counterexample" else "witness" + case status of + UnSAT -> (Just negated, verifierName <+> "proved no" <+> witnessText <+> "exists") + SAT Nothing -> (Just (not negated), verifierName <+> "found no" <> witnessText) + SAT Just {} -> (Just (not negated), verifierName <+> "found a" <+> witnessText) + PropertyErrored (_, err) -> do + let cause = if isTimeoutError err then "timed out" else "errored" + (Nothing, verifierName <+> cause) + VIO.writeStdoutLn (layoutAsText $ " result: " <> pretty (statusSymbol verified) <+> "-" <+> evidenceText) + + -- Output any additional information case result of PropertyCompleted status -> case status of NonTrivial (_, SAT (Just (UserVariableAssignment assignments))) -> do diff --git a/vehicle/src/Vehicle/Verify/Specification/Status.hs b/vehicle/src/Vehicle/Verify/Specification/Status.hs index 59f14f03d..e81fc9a8f 100644 --- a/vehicle/src/Vehicle/Verify/Specification/Status.hs +++ b/vehicle/src/Vehicle/Verify/Specification/Status.hs @@ -2,7 +2,6 @@ module Vehicle.Verify.Specification.Status where import Data.List.Split (chunksOf) import Data.Set (Set) -import Data.Text (Text) import System.Console.ANSI (Color (..)) import Vehicle.Compile.Prelude import Vehicle.Data.Builtin.Standard @@ -56,33 +55,17 @@ instance IsVerified PropertyStatus where NonTrivial (negated, result) -> evaluateQuery negated result PropertyErrored {} -> False -instance Pretty PropertyStatus where - pretty propertyStatus = do - let (verified, evidenceText) = case propertyStatus of - PropertyCompleted maybeResult -> do - case maybeResult of - Trivial status -> (status, "(trivial)") - NonTrivial (negated, status) -> do - let witnessText = if negated then "counterexample" else "witness" - case status of - UnSAT -> (negated, "proved no" <+> witnessText <+> "exists") - SAT Nothing -> (not negated, "no" <> witnessText <+> "found") - SAT Just {} -> (not negated, witnessText <+> "found") - PropertyErrored (_, err) -> (False, if isTimeoutError err then "verifier timed out" else "verifier errored") - pretty (statusSymbol verified) <+> "-" <+> evidenceText - -------------------------------------------------------------------------------- -- Verification status of a multi property -statusSymbol :: Bool -> String +statusSymbol :: Maybe Bool -> String statusSymbol verified = do - let (colour, symbol) = if verified then (Green, "🗸") else (Red, "✗") + let (colour, symbol) = case verified of + Just True -> (Green, "🗸") + Nothing -> (Yellow, "?") + Just False -> (Red, "✗") setTextColour colour symbol -prettyNameAndStatus :: Text -> Bool -> Doc a -prettyNameAndStatus name verified = do - pretty (statusSymbol verified) <+> pretty name - prettyUserVariableAssignment :: (Name, RationalTensor) -> Doc a prettyUserVariableAssignment (var, variableValue) = pretty var <> ":" <+> pretty variableValue diff --git a/vehicle/src/Vehicle/Verify/Verifier/Core.hs b/vehicle/src/Vehicle/Verify/Verifier/Core.hs index 23f727baa..97c448c36 100644 --- a/vehicle/src/Vehicle/Verify/Verifier/Core.hs +++ b/vehicle/src/Vehicle/Verify/Verifier/Core.hs @@ -25,7 +25,7 @@ data VerifierID instance Show VerifierID where show = \case Marabou -> "Marabou" - TestVerifier -> "Test" + TestVerifier -> "TestVerifier" instance Pretty VerifierID where pretty = pretty . show diff --git a/vehicle/src/Vehicle/Verify/Verifier/Marabou.hs b/vehicle/src/Vehicle/Verify/Verifier/Marabou.hs index fb1b8da5d..36b31326f 100644 --- a/vehicle/src/Vehicle/Verify/Verifier/Marabou.hs +++ b/vehicle/src/Vehicle/Verify/Verifier/Marabou.hs @@ -36,11 +36,13 @@ prepareMarabouArgs metaNetwork queryFile = case metaNetwork of parseMarabouOutput :: ParseVerifierOutput parseMarabouOutput output = do let outputLines = fmap Text.pack (lines output) - let resultIndex = findIndex (\v -> v == "sat" || v == "unsat" || v == "timeout") outputLines + let resultIndex = findIndex (\v -> v == "sat" || v == "unsat" || v == "Timeout") outputLines case resultIndex of - Nothing -> throwError $ VerifierOutputMalformed "Cannot find 'sat' or 'unsat'" + Nothing -> do + logDebug MinDetail $ pretty output + throwError $ VerifierOutputMalformed "Cannot find 'sat', 'unsat' or 'timeout'" Just i - | outputLines !! i == "timeout" -> throwError VerifierTimedOut + | outputLines !! i == "Timeout" -> throwError VerifierTimedOut | outputLines !! i == "unsat" -> return UnSAT | otherwise -> do let assignmentOutput = drop (i + 1) outputLines diff --git a/vehicle/tests/golden/compile/acasXu/MarabouVerify.out.golden b/vehicle/tests/golden/compile/acasXu/MarabouVerify.out.golden index 837d2f10c..edbe8f180 100644 --- a/vehicle/tests/golden/compile/acasXu/MarabouVerify.out.golden +++ b/vehicle/tests/golden/compile/acasXu/MarabouVerify.out.golden @@ -1,4 +1,4 @@ Verifying properties: property3 [......................................................] 0/1 queries property3 [======================================================] 1/1 queries - result: ✗ - counterexample found - x: [ 1799.988667, 5.2420604112e-2, 3.09999732192, 980.0, 1055.5284 ] + result: ✗ - Marabou found a counterexample + x: [ 1799.988667, 5.9998124016e-2, 3.09999732192, 980.0, 1089.0516 ] diff --git a/vehicle/tests/golden/compile/issue641/MarabouVerify.err.golden b/vehicle/tests/golden/compile/issue641/MarabouVerify.err.golden index 38152fbc0..8fc8ecbf2 100644 --- a/vehicle/tests/golden/compile/issue641/MarabouVerify.err.golden +++ b/vehicle/tests/golden/compile/issue641/MarabouVerify.err.golden @@ -6,7 +6,8 @@ In order to provide support, Vehicle has automatically converted the strict ineq See https://github.com/vehicle-lang/vehicle/issues/74 for further details. -Warning: In property 'p', in queries 1 and 2 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - queries 1 and 2 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/compile/issue641/MarabouVerify.out.golden b/vehicle/tests/golden/compile/issue641/MarabouVerify.out.golden index 64c3d2510..41ca94cfe 100644 --- a/vehicle/tests/golden/compile/issue641/MarabouVerify.out.golden +++ b/vehicle/tests/golden/compile/issue641/MarabouVerify.out.golden @@ -1,4 +1,4 @@ Verifying properties: p [..............................................................] 0/2 queries p [===============================>..............................] 1/2 queries p [==============================================================] 2/2 queries - result: 🗸 - witness found + result: 🗸 - Marabou found a witness diff --git a/vehicle/tests/golden/compile/simple-fourierMotzkin/TestVerify.out.golden b/vehicle/tests/golden/compile/simple-fourierMotzkin/TestVerify.out.golden index 793384232..f6388839c 100644 --- a/vehicle/tests/golden/compile/simple-fourierMotzkin/TestVerify.out.golden +++ b/vehicle/tests/golden/compile/simple-fourierMotzkin/TestVerify.out.golden @@ -1,4 +1,4 @@ Verifying properties: underConstrainedVars [...........................................] 0/1 queries underConstrainedVars [===========================================] 1/1 queries - result: 🗸 - witness found + result: 🗸 - TestVerifier found a witness x: [ -9.3, 9.5, -1.0, 3.0, 0.0 ] diff --git a/vehicle/tests/golden/compile/windController/MarabouVerify.out.golden b/vehicle/tests/golden/compile/windController/MarabouVerify.out.golden index 16c352bed..4034f99a9 100644 --- a/vehicle/tests/golden/compile/windController/MarabouVerify.out.golden +++ b/vehicle/tests/golden/compile/windController/MarabouVerify.out.golden @@ -1,3 +1,3 @@ Verifying properties: safe [...........................................................] 0/2 queries safe [=============================>.............................] 1/2 queries safe [===========================================================] 2/2 queries - result: 🗸 - proved no counterexample exists + result: 🗸 - Marabou proved no counterexample exists diff --git a/vehicle/tests/golden/compile/windController/TestVerify.out.golden b/vehicle/tests/golden/compile/windController/TestVerify.out.golden index df14fa481..dea84b512 100644 --- a/vehicle/tests/golden/compile/windController/TestVerify.out.golden +++ b/vehicle/tests/golden/compile/windController/TestVerify.out.golden @@ -1,4 +1,4 @@ Verifying properties: safe [...........................................................] 0/2 queries - result: ✗ - counterexample found + result: ✗ - TestVerifier found a counterexample x: [ -2.4, -1.6 ] diff --git a/vehicle/tests/golden/error/other-verifier/verifierTimeout/TestVerify.out.golden b/vehicle/tests/golden/error/other-verifier/verifierTimeout/TestVerify.out.golden index 39e009256..d504d272f 100644 --- a/vehicle/tests/golden/error/other-verifier/verifierTimeout/TestVerify.out.golden +++ b/vehicle/tests/golden/error/other-verifier/verifierTimeout/TestVerify.out.golden @@ -1,3 +1,5 @@ Verifying properties: - p1 [.............................................................] 0/1 queries result: ✗ - verifier timed out - p2 [.............................................................] 0/1 queries result: ✗ - verifier timed out + p1 [.............................................................] 0/1 queries + result: ? - TestVerifier timed out + p2 [.............................................................] 0/1 queries + result: ? - TestVerifier timed out