From bc44927832c301f845d9fe8e3682442b8f8bb27e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 10:39:16 +0200 Subject: [PATCH] Extend Unknown type, abort on unsafe unknown ensures --- booster/library/Booster/JsonRpc.hs | 4 +- booster/library/Booster/Pattern/Rewrite.hs | 40 +++-- booster/library/Booster/SMT/Interface.hs | 42 ++++- ...onse-symbolic-bottom-predicate.booster-dev | 151 ------------------ .../response-symbolic-bottom-predicate.json | 53 ++---- 5 files changed, 73 insertions(+), 217 deletions(-) delete mode 100644 booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index ff06f9b350..e834ca8003 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -365,7 +365,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 @@ -409,7 +409,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 8d2e203b8c..3f1c5bf0cd 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -307,7 +307,7 @@ applyRule pat@Pattern{ceilConditions} rule = MatchSuccess matchingSubstitution -> do -- existential variables may be present in rule.rhs and rule.ensures, -- need to strip prefixes and freshen their names with respect to variables already - -- present in the input pattern and in the unification substitution + -- present in the input pattern and in the matching substitution varsFromInput <- lift . RewriteT $ asks (.varsToAvoid) let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution @@ -498,18 +498,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 pat.substitution (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) @@ -534,15 +527,38 @@ 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 pat.substitution (Set.fromList newConstraints)) >>= \case + SMT.IsUnknown SMT.ImplicationIndeterminate -> do + pure () + SMT.IsUnknown SMT.InconsistentGroundTruth -> do + withContext CtxWarn $ logMessage ("Ground truth is #Bottom." :: Text) + RewriteRuleAppT $ pure Trivial SMT.IsInvalid -> do withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure Trivial + SMT.IsUnknown reason -> do + -- abort rewrite if a solver result was Unknown for reason other then SMT.ImplicationIndeterminate + withContext CtxAbort $ logMessage reason + smtUnclear newConstraints _other -> pure () 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/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev deleted file mode 100644 index 9a01a8013e..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ /dev/null @@ -1,151 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - } - } - } - } -} \ No newline at end of file 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 992a21f0e1..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" } ] }, @@ -67,7 +67,7 @@ "args": [ { "tag": "EVar", - "name": "Y", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", @@ -111,41 +111,6 @@ ] } }, - "substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - } - }, "predicate": { "format": "KORE", "version": 1, @@ -190,22 +155,22 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "1" + } } ] }