Skip to content
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

Jump to bottom

Handle inconsistent ground truth and SMT unknowns when checking ensures #4063

Merged
merged 2 commits into from
Oct 17, 2024
Merged

Handle inconsistent ground truth and SMT unknowns when checking ensures #4063

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8e9c7c2
Abort on unsafe unknown reasons when checking ensures
geo2a Oct 17, 2024
cbd2c15
Spelling
geo2a Oct 17, 2024
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
4 changes: 2 additions & 2 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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 (..),
UnkwnonReason (..),
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 UnkwnonReason
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
data UnkwnonReason
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 "_"]] 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))
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 UnkwnonReason 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
Open in desktop
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
Open in desktop
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
Loading