Skip to content

Commit

Permalink
Abort on unsafe unknown reasons when checking ensures
Browse files Browse the repository at this point in the history 
We abort when checking ensured conditions of rewrite rules
if the ground truth is UNSAT or the SMT solver returned Unkwnon
  • Loading branch information
@geo2a
geo2a committed Oct 17, 2024
1 parent 4347105 commit 8e9c7c2
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 (..),
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
= -- | 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
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 8e9c7c2

Please sign in to comment.