From ad8a7ff7cc242abd3257ddc3026b792fb929354b Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 14:28:55 +0200 Subject: [PATCH] Handle inconsistent ground truth and SMT unknowns when checking `ensures` (#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. --- booster/library/Booster/JsonRpc.hs | 4 +- booster/library/Booster/Pattern/Rewrite.hs | 40 ++++-- booster/library/Booster/SMT/Interface.hs | 42 ++++-- .../test-substitutions/README.md | 2 +- .../response-circular-equations.booster-dev | 62 +-------- ...onse-symbolic-bottom-predicate.booster-dev | 127 +++++------------- .../response-symbolic-bottom-predicate.json | 125 +++++------------ 7 files changed, 142 insertions(+), 260 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 12a493738b..979da2e731 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -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 @@ -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 diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 626ecd4d6d..39d6f71c2f 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -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) @@ -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 () @@ -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. -} diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index e131435080..731562f2d4 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -12,6 +12,7 @@ module Booster.SMT.Interface ( SMTOptions (..), -- re-export defaultSMTOptions, -- re-export SMTError (..), + UnknownReason (..), initSolver, noSolver, finaliseSolver, @@ -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) @@ -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 @@ -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)) @@ -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 @@ -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) @@ -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) diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md index 1c7a208f58..f6bf9f83bb 100644 --- a/booster/test/rpc-integration/test-substitutions/README.md +++ b/booster/test/rpc-integration/test-substitutions/README.md @@ -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`. diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index b012148190..259a441aeb 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -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": [] + } } ] } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev index 9aec4d5289..8196839aaa 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev @@ -2,8 +2,8 @@ "jsonrpc": "2.0", "id": 1, "result": { - "reason": "stuck", - "depth": 1, + "reason": "vacuous", + "depth": 0, "state": { "term": { "format": "KORE", @@ -46,7 +46,7 @@ "name": "SortState", "args": [] }, - "value": "a" + "value": "symbolic-subst" } ] }, @@ -115,114 +115,57 @@ "format": "KORE", "version": 1, "term": { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "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" - } - ] - } - ] - } + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, - "second": { + { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsPlus'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { "tag": "EVar", - "name": "Y", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", @@ -231,8 +174,8 @@ } ] } - } - ] + ] + } } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json index be972500f9..8196839aaa 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json @@ -3,7 +3,7 @@ "id": 1, "result": { "reason": "vacuous", - "depth": 1, + "depth": 0, "state": { "term": { "format": "KORE", @@ -46,7 +46,7 @@ "name": "SortState", "args": [] }, - "value": "a" + "value": "symbolic-subst" } ] }, @@ -115,114 +115,57 @@ "format": "KORE", "version": 1, "term": { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "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" - } - ] - } - ] - } + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, - "second": { + { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsPlus'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { "tag": "EVar", - "name": "Y", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", @@ -231,8 +174,8 @@ } ] } - } - ] + ] + } } } }