From 8e9c7c254dfac9e8a0e6cf169fdc092c581a4927 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 11:01:15 +0200 Subject: [PATCH 1/2] Abort on unsafe unknown reasons when checking ensures We abort when checking ensured conditions of rewrite rules if the ground truth is UNSAT or the SMT solver returned Unkwnon --- 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..6304391ad9 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 (..), + UnkwnonReason (..), 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 UnkwnonReason + = -- | 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 "_"]] UnkwnonReason + +instance Log.ToLogFormat UnkwnonReason where + toTextualLog = pack . show + toJSONLog = toJSON + +pattern IsUnknown :: UnkwnonReason -> Either UnkwnonReason 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 UnkwnonReason (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 UnkwnonReason 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 @@ } ] } - } - ] + ] + } } } } From cbd2c15890a5b50d42cdafa68191081d4aece871 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 13:27:36 +0200 Subject: [PATCH 2/2] Spelling --- booster/library/Booster/SMT/Interface.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 6304391ad9..731562f2d4 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -12,7 +12,7 @@ module Booster.SMT.Interface ( SMTOptions (..), -- re-export defaultSMTOptions, -- re-export SMTError (..), - UnkwnonReason (..), + UnknownReason (..), initSolver, noSolver, finaliseSolver, @@ -198,7 +198,7 @@ finaliseSolver ctxt = do Log.logMessage ("Closing SMT solver" :: Text) destroyContext ctxt -data UnkwnonReason +data UnknownReason = -- | SMT prelude is UNSAT InconsistentGroundTruth | -- | (P, not P) is (SAT, SAT) @@ -208,18 +208,18 @@ data UnkwnonReason deriving (Show, Eq, Generic) deriving (FromJSON, ToJSON) - via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] UnkwnonReason + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] UnknownReason -instance Log.ToLogFormat UnkwnonReason where +instance Log.ToLogFormat UnknownReason where toTextualLog = pack . show toJSONLog = toJSON -pattern IsUnknown :: UnkwnonReason -> Either UnkwnonReason b +pattern IsUnknown :: UnknownReason -> Either UnknownReason b pattern IsUnknown u = Left u newtype IsSat' a = IsSat' (Maybe a) deriving (Functor) -type IsSatResult a = Either UnkwnonReason (IsSat' a) +type IsSatResult a = Either UnknownReason (IsSat' a) pattern IsSat :: a -> IsSatResult a pattern IsSat a = Right (IsSat' (Just a)) @@ -373,7 +373,7 @@ mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded] newtype IsValid' = IsValid' Bool -type IsValidResult = Either UnkwnonReason IsValid' +type IsValidResult = Either UnknownReason IsValid' pattern IsValid, IsInvalid :: IsValidResult pattern IsValid = Right (IsValid' True)