Skip to content

HOTFIX re-introduce indeterminate result for checkPredicates instead of exceptions #3908

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 1 commit into from
May 30, 2024
Merged

HOTFIX re-introduce indeterminate result for checkPredicates instead of exceptions #3908

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
43 changes: 25 additions & 18 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ module Booster.Pattern.Rewrite (
) where

import Control.Applicative ((<|>))
import Control.Exception qualified as Exception (throw)
import Control.Monad
import Control.Monad.Extra (whenJust)
import Control.Monad.IO.Class (MonadIO (..))
Expand Down Expand Up @@ -354,29 +355,30 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
-- check unclear requires-clauses in the context of known constraints (prior)
mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask

let smtUnclear = do
withContext "abort" . logMessage . renderOneLineText $
"Uncertain about condition(s) in a rule:" <+> pretty unclearRequires
failRewrite $
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
map coerce unclearRequires
case mbSolver of
Just solver -> do
checkAllRequires <- SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)
checkAllRequires <-
SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)

case checkAllRequires of
Left _ -> do
-- TODO: we could process SMTError here
-- unclear even with the prior
withContext "abort" $
logMessage $
renderOneLineText $
"Uncertain about a condition(s) in rule:" <+> pretty unclearRequires
failRewrite $
RuleConditionUnclear rule . coerce $
foldl1 AndTerm $
map coerce unclearRequires
Right False -> do
Left SMT.SMTSolverUnknown{} ->
smtUnclear -- abort rewrite if a solver result was Unknown
Left other ->
liftIO $ Exception.throw other -- fail hard on other SMT errors
Right (Just False) -> do
-- requires is actually false given the prior
withContext "failure" $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure NotApplied
Right True ->
-- can proceed
pure ()
Right (Just True) ->
pure () -- can proceed
Right Nothing ->
smtUnclear -- no implication could be determined
Nothing ->
unless (null unclearRequires) $ do
withContext "abort" $
Expand All @@ -398,10 +400,15 @@ 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
Right False -> do
Right (Just False) -> do
withContext "success" $ logMessage ("New constraints evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
_other -> pure ()
Right _other ->
pure ()
Left SMT.SMTSolverUnknown{} ->
pure ()
Left other ->
liftIO $ Exception.throw other

-- existential variables may be present in rule.rhs and rule.ensures,
-- need to strip prefixes and freshen their names with respect to variables already
Expand Down
29 changes: 15 additions & 14 deletions booster/library/Booster/SMT/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,9 +263,9 @@ checkPredicates ::
Set Predicate ->
Map Variable Term ->
Set Predicate ->
io (Either SMTError Bool)
io (Either SMTError (Maybe Bool))
Copy link
Member Author

Choose a reason for hiding this comment

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

Since the SMTSolverUnknown is not a "real error", we could also use a 4-fold dedicated result type here

data CheckPredicatesResult
    = PredicatesTrue
    | PredicatesFalse
    | PredicatesIndeterminate
    | UnknownResult

That means we can throw exceptions directly from here as we did before.
The current version puts the burden on the caller but leaves more flexibility.

checkPredicates ctxt givenPs givenSubst psToCheck
| null psToCheck = pure $ Right True
| null psToCheck = pure . Right $ Just True
| Left errMsg <- translated = Log.withContext "smt" $ do
Log.logErrorNS "booster" $ "SMT translation error: " <> errMsg
Log.logMessage $ "SMT translation error: " <> errMsg
Expand Down Expand Up @@ -297,34 +297,35 @@ checkPredicates ctxt givenPs givenSubst psToCheck
mapM_ smtRun smtGiven

consistent <- smtRun CheckSat
when (consistent /= Sat) $ do
void $ smtRun Pop
unless (consistent == Sat) $ do
let errMsg = ("Inconsistent ground truth, check returns Nothing" :: Text)
Log.logMessage errMsg
throwE $ GeneralSMTError errMsg
let ifConsistent check = if (consistent == Sat) then check else pure Unsat

-- save ground truth for 2nd check
smtRun_ Push

-- run check for K ∧ P and then for K ∧ !P
let allToCheck = SMT.List (Atom "and" : sexprsToCheck)

smtRun_ $ Assert "P" allToCheck
positive <- smtRun CheckSat
positive <- ifConsistent $ do
smtRun_ $ Assert "P" allToCheck
smtRun CheckSat
smtRun_ Pop
negative <- ifConsistent $ do
smtRun_ $ Assert "not P" (SMT.smtnot allToCheck)
smtRun CheckSat
smtRun_ Pop
smtRun_ $ Assert "not P" (SMT.smtnot allToCheck)
negative <- smtRun CheckSat
void $ smtRun Pop

Log.logMessage $
"Check of Given ∧ P and Given ∧ !P produced "
<> pack (show (positive, negative))

case (positive, negative) of
(Unsat, Unsat) -> throwSMT "Inconsistent ground truth: should have been caught above"
(Sat, Sat) -> throwE $ GeneralSMTError "Implication not determined"
(Sat, Unsat) -> pure True
(Unsat, Sat) -> pure False
(Unsat, Unsat) -> pure Nothing -- defensive choice for inconsistent ground truth
(Sat, Sat) -> pure Nothing -- implication not determined
(Sat, Unsat) -> pure $ Just True
(Unsat, Sat) -> pure $ Just False
(Unknown, _) -> do
smtRun GetReasonUnknown >>= \case
ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck
Expand Down
Loading