Skip to content

Commit

Permalink
Handle inconsistent ground truth and SMT unknowns when checking `ensu…
Browse files Browse the repository at this point in the history 
…res` (#4063)

When checking `ensures` conditions of rewrite rules with the SMT solver,
we must mark rewrite as trivial if the ground truth is inconsistent. If
the SMT solver returns unknown, we must abort rewriting.

Previously, we were swallowing both of there cases and finalizing the
rewrite step successfully. This behavior of Booster went undetected for
a long time since we would usually abort rewriting or detect a vacuous
state at the next step, resulting in wasted work but no unsoundness.

We also tweak the return type of `checkPredicates` to convey addition
information why the result is unknown. This will be useful when we start
tolerating SMT unknowns and branching on that.
  • Loading branch information
@geo2a
geo2a authored Oct 17, 2024
1 parent 4347105 commit ad8a7ff
Show file tree
Hide file tree
Showing 7 changed files with 142 additions and 260 deletions.
4 changes: 2 additions & 2 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -363,7 +363,7 @@ respond stateVar request =
withContext CtxGetModel $
withContext CtxSMT $
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
pure $ SMT.IsUnknown "No predicates or substitutions given"
pure $ SMT.IsUnknown (SMT.SMTUnknownReason "No predicates or substitutions given")
else do
solver <- SMT.initSolver def smtOptions
result <- SMT.getModelFor solver boolPs suppliedSubst
Expand Down Expand Up @@ -407,7 +407,7 @@ respond stateVar request =
, substitution = Nothing
}
SMT.IsUnknown reason -> do
logMessage $ "SMT result: Unknown - " <> reason
logMessage $ "SMT result: Unknown - " <> show reason
pure . Right . RpcTypes.GetModel $
RpcTypes.GetModelResult
{ satisfiable = RpcTypes.Unknown
Expand Down
40 changes: 29 additions & 11 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -438,18 +438,11 @@ applyRule pat@Pattern{ceilConditions} rule =

-- check unclear requires-clauses in the context of known constraints (priorKnowledge)
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
let smtUnclear = do
withContext CtxConstraint . withContext CtxAbort . logMessage $
WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $
renderOneLineText $
"Uncertain about condition(s) in a rule:"
<+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear)
failRewrite $
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
map coerce stillUnclear
SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case
SMT.IsUnknown{} ->
smtUnclear -- abort rewrite if a solver result was Unknown
SMT.IsUnknown reason -> do
-- abort rewrite if a solver result was Unknown
withContext CtxAbort $ logMessage reason
smtUnclear stillUnclear
SMT.IsInvalid -> do
-- requires is actually false given the prior
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
Expand All @@ -467,10 +460,23 @@ applyRule pat@Pattern{ceilConditions} rule =

-- check all new constraints together with the known side constraints
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
-- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions.
-- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)).
(lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case
SMT.IsInvalid -> do
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
SMT.IsUnknown SMT.InconsistentGroundTruth -> do
withContext CtxSuccess $ logMessage ("Ground truth is #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
SMT.IsUnknown SMT.ImplicationIndeterminate -> do
-- the new constraint is satisfiable, continue
pure ()
SMT.IsUnknown reason -> do
-- abort rewrite if a solver result was Unknown for a reason other
-- then SMT.ImplicationIndeterminate of SMT.InconsistentGroundTruth
withContext CtxAbort $ logMessage reason
smtUnclear newConstraints
_other ->
pure ()

Expand All @@ -482,6 +488,18 @@ applyRule pat@Pattern{ceilConditions} rule =
lift . RewriteT . lift . modify $ \s -> s{equations = mempty}
pure newConstraints

smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) ()
smtUnclear predicates = do
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
withContext CtxConstraint . withContext CtxAbort . logMessage $
WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> predicates)]) $
renderOneLineText $
"Uncertain about condition(s) in a rule:"
<+> (hsep . punctuate comma . map (pretty' @mods) $ predicates)
failRewrite $
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
map coerce predicates

{- | Reason why a rewrite did not produce a result. Contains additional
information for logging what happened during the rewrite.
-}
Expand Down
42 changes: 34 additions & 8 deletions booster/library/Booster/SMT/Interface.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ module Booster.SMT.Interface (
SMTOptions (..), -- re-export
defaultSMTOptions, -- re-export
SMTError (..),
UnknownReason (..),
initSolver,
noSolver,
finaliseSolver,
Expand All @@ -33,6 +34,7 @@ import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.State
import Data.Aeson (object, (.=))
import Data.Aeson.Types (FromJSON (..), ToJSON (..))
import Data.ByteString.Char8 qualified as BS
import Data.Coerce
import Data.Data (Proxy)
Expand All @@ -44,6 +46,14 @@ import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text as Text (Text, pack, unlines, unwords)
import Deriving.Aeson (
CamelToKebab,
CustomJSON (..),
FieldLabelModifier,
OmitNothingFields,
StripPrefix,
)
import GHC.Generics (Generic)
import Prettyprinter (Pretty, backslash, hsep, punctuate, slash, (<+>))
import SMTLIB.Backends.Process qualified as Backend

Expand Down Expand Up @@ -188,12 +198,28 @@ finaliseSolver ctxt = do
Log.logMessage ("Closing SMT solver" :: Text)
destroyContext ctxt

pattern IsUnknown :: unknown -> Either unknown b
data UnknownReason
= -- | SMT prelude is UNSAT
InconsistentGroundTruth
| -- | (P, not P) is (SAT, SAT)
ImplicationIndeterminate
| -- | SMT solver returned unknown
SMTUnknownReason Text
deriving (Show, Eq, Generic)
deriving
(FromJSON, ToJSON)
via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] UnknownReason

instance Log.ToLogFormat UnknownReason where
toTextualLog = pack . show
toJSONLog = toJSON

pattern IsUnknown :: UnknownReason -> Either UnknownReason b
pattern IsUnknown u = Left u

newtype IsSat' a = IsSat' (Maybe a) deriving (Functor)

type IsSatResult a = Either Text (IsSat' a)
type IsSatResult a = Either UnknownReason (IsSat' a)

pattern IsSat :: a -> IsSatResult a
pattern IsSat a = Right (IsSat' (Just a))
Expand Down Expand Up @@ -243,7 +269,7 @@ isSatReturnTransState ctxt ps subst
SMT.runCmd CheckSat >>= \case
Sat -> pure $ IsSat transState
Unsat -> pure IsUnsat
Unknown reason -> retry (solve smtToCheck transState) (pure $ IsUnknown reason)
Unknown reason -> retry (solve smtToCheck transState) (pure $ IsUnknown (SMTUnknownReason reason))
other -> do
let msg = "Unexpected result while calling 'check-sat': " <> show other
Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg
Expand Down Expand Up @@ -347,7 +373,7 @@ mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded]

newtype IsValid' = IsValid' Bool

type IsValidResult = Either (Maybe Text) IsValid'
type IsValidResult = Either UnknownReason IsValid'

pattern IsValid, IsInvalid :: IsValidResult
pattern IsValid = Right (IsValid' True)
Expand Down Expand Up @@ -418,14 +444,14 @@ checkPredicates ctxt givenPs givenSubst psToCheck
hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck))
result <- interactWithSolver smtGiven sexprsToCheck
case result of
(Unsat, Unsat) -> pure $ IsUnknown Nothing -- defensive choice for inconsistent ground truth
(Unsat, Unsat) -> pure $ IsUnknown InconsistentGroundTruth
(Sat, Sat) -> do
Log.logMessage ("Implication not determined" :: Text)
pure $ IsUnknown Nothing
pure $ IsUnknown ImplicationIndeterminate
(Sat, Unsat) -> pure IsValid
(Unsat, Sat) -> pure IsInvalid
(Unknown reason, _) -> retry (solve smtGiven sexprsToCheck transState) (pure $ IsUnknown $ Just reason)
(_, Unknown reason) -> retry (solve smtGiven sexprsToCheck transState) (pure $ IsUnknown $ Just reason)
(Unknown reason, _) -> retry (solve smtGiven sexprsToCheck transState) (pure . IsUnknown . SMTUnknownReason $ reason)
(_, Unknown reason) -> retry (solve smtGiven sexprsToCheck transState) (pure . IsUnknown . SMTUnknownReason $ reason)
other ->
throwSMT $
"Unexpected result while checking a condition: " <> Text.pack (show other)
Expand Down
2 changes: 1 addition & 1 deletion booster/test/rpc-integration/test-substitutions/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,6 @@ NB: Booster applies the given substitution before performing any action.
* `state-symbolic-bottom-predicate.execute`
- starts from `symbolic-subst`
- with an equation that is instantly false: `X = 1 +Int X`
- leading to a vacuous state in `kore-rpc-booster` after rewriting once,
- leading to a vacuous state in `kore-rpc-booster` and `booster-dev` at 0 steps,
- while `kore-rpc-dev` returns `stuck` instantly after 0 steps,
returning the exact input as `state`.
62 changes: 7 additions & 55 deletions booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev
View file
Original file line number Diff line number Diff line change
Expand Up @@ -225,61 +225,13 @@
}
},
{
"tag": "App",
"name": "Lbl'UndsPlus'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'UndsPlus'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "X",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "1"
}
]
},
{
"tag": "App",
"name": "Lbl'Unds'-Int'Unds'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "1"
}
]
}
]
"tag": "EVar",
"name": "X",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
}
]
}
Expand Down
Loading

0 comments on commit ad8a7ff

Please sign in to comment.