Skip to content

Abort on "Unknown" side conditions, don't crash #3907

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 30, 2024
Merged

Abort on "Unknown" side conditions, don't crash #3907

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e8c8729
Abort on "Unknown" side conditions, don't crash
geo2a May 29, 2024
12c83a3
Put the predicates into the error value
geo2a May 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,8 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
checkAllRequires <- SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)

case checkAllRequires of
Nothing -> do
Left _ -> do
-- TODO: we could process SMTError here
Comment on lines +362 to +363
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should probably restrict this to the SMTSolverUnknown case. An SMTTranslationError is an entirely different case (and the General error was meant to cover infrastructure issues).

-- unclear even with the prior
withContext "abort" $
logMessage $
Expand All @@ -369,11 +370,11 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
RuleConditionUnclear rule . coerce $
foldl1 AndTerm $
map coerce unclearRequires
Just False -> do
Right False -> do
-- requires is actually false given the prior
withContext "failure" $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure NotApplied
Just True ->
Right True ->
-- can proceed
pure ()
Nothing ->
Expand All @@ -397,7 +398,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
-- check all new constraints together with the known side constraints
whenJust mbSolver $ \solver ->
(lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
Just False -> do
Right False -> do
withContext "success" $ logMessage ("New constraints evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
_other -> pure ()
Expand Down
28 changes: 13 additions & 15 deletions booster/library/Booster/SMT/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module Booster.SMT.Interface (
import Control.Exception (Exception, throw)
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Except
import Data.ByteString.Char8 qualified as BS
import Data.Coerce
import Data.Either (isLeft)
Expand Down Expand Up @@ -68,9 +68,6 @@ throwSMT = throw . GeneralSMTError
throwSMT' :: String -> a
throwSMT' = throwSMT . pack

throwUnknown :: Text -> Set Predicate -> Set Predicate -> a
throwUnknown reason premises preds = throw $ SMTSolverUnknown reason premises preds

smtTranslateError :: Text -> a
smtTranslateError = throw . SMTTranslationError

Expand Down Expand Up @@ -266,14 +263,14 @@ checkPredicates ::
Set Predicate ->
Map Variable Term ->
Set Predicate ->
io (Maybe Bool)
io (Either SMTError Bool)
checkPredicates ctxt givenPs givenSubst psToCheck
| null psToCheck = pure $ Just True -- or Nothing?
| null psToCheck = pure $ Right True
| Left errMsg <- translated = Log.withContext "smt" $ do
Log.logErrorNS "booster" $ "SMT translation error: " <> errMsg
Log.logMessage $ "SMT translation error: " <> errMsg
pure Nothing
| Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext "smt" $ runSMT ctxt . runMaybeT $ do
pure . Left . SMTTranslationError $ errMsg
| Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext "smt" $ runSMT ctxt . runExceptT $ do
Log.logMessage $
Text.unwords
[ "Checking"
Expand Down Expand Up @@ -302,8 +299,9 @@ checkPredicates ctxt givenPs givenSubst psToCheck
consistent <- smtRun CheckSat
when (consistent /= Sat) $ do
void $ smtRun Pop
Log.logMessage ("Inconsistent ground truth, check returns Nothing" :: Text)
fail "returns nothing"
let errMsg = ("Inconsistent ground truth, check returns Nothing" :: Text)
Log.logMessage errMsg
throwE $ GeneralSMTError errMsg
Comment on lines +302 to +304
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not really an "error", rather a defensive strategy to avoid jumping to unjustified conclusions


-- save ground truth for 2nd check
smtRun_ Push
Expand All @@ -324,22 +322,22 @@ checkPredicates ctxt givenPs givenSubst psToCheck

case (positive, negative) of
(Unsat, Unsat) -> throwSMT "Inconsistent ground truth: should have been caught above"
(Sat, Sat) -> fail "Implication not determined"
(Sat, Sat) -> throwE $ GeneralSMTError "Implication not determined"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here, this is actually a result (neither P nor not P are implied)

(Sat, Unsat) -> pure True
(Unsat, Sat) -> pure False
(Unknown, _) -> do
smtRun GetReasonUnknown >>= \case
ReasonUnknown reason -> throwUnknown reason givenPs psToCheck
ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck
other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other
(_, Unknown) -> do
smtRun GetReasonUnknown >>= \case
ReasonUnknown reason -> throwUnknown reason givenPs psToCheck
ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck
other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other
other -> throwSMT' $ "Unexpected result while checking a condition: " <> show other
where
smtRun_ :: SMTEncode c => c -> MaybeT (SMT io) ()
smtRun_ :: SMTEncode c => c -> ExceptT SMTError (SMT io) ()
smtRun_ = lift . SMT.runCmd_
smtRun :: SMTEncode c => c -> MaybeT (SMT io) Response
smtRun :: SMTEncode c => c -> ExceptT SMTError (SMT io) Response
smtRun = lift . SMT.runCmd

translated = SMT.runTranslator $ do
Expand Down
Loading