Skip to content

Commit ad8a7ff

Browse files
geo2ageo2a
authored
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.
1 parent 4347105 commit ad8a7ff

File tree

7 files changed

+142
-260
lines changed

7 files changed

+142
-260
lines changed

‎booster/library/Booster/JsonRpc.hs

+2-2
Original file line numberDiff line numberDiff line change
@@ -363,7 +363,7 @@ respond stateVar request =
363363
withContext CtxGetModel $
364364
withContext CtxSMT $
365365
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
366-
pure $ SMT.IsUnknown "No predicates or substitutions given"
366+
pure $ SMT.IsUnknown (SMT.SMTUnknownReason "No predicates or substitutions given")
367367
else do
368368
solver <- SMT.initSolver def smtOptions
369369
result <- SMT.getModelFor solver boolPs suppliedSubst
@@ -407,7 +407,7 @@ respond stateVar request =
407407
, substitution = Nothing
408408
}
409409
SMT.IsUnknown reason -> do
410-
logMessage $ "SMT result: Unknown - " <> reason
410+
logMessage $ "SMT result: Unknown - " <> show reason
411411
pure . Right . RpcTypes.GetModel $
412412
RpcTypes.GetModelResult
413413
{ satisfiable = RpcTypes.Unknown

‎booster/library/Booster/Pattern/Rewrite.hs

+29-11
Original file line numberDiff line numberDiff line change
@@ -438,18 +438,11 @@ applyRule pat@Pattern{ceilConditions} rule =
438438

439439
-- check unclear requires-clauses in the context of known constraints (priorKnowledge)
440440
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
441-
let smtUnclear = do
442-
withContext CtxConstraint . withContext CtxAbort . logMessage $
443-
WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $
444-
renderOneLineText $
445-
"Uncertain about condition(s) in a rule:"
446-
<+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear)
447-
failRewrite $
448-
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
449-
map coerce stillUnclear
450441
SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case
451-
SMT.IsUnknown{} ->
452-
smtUnclear -- abort rewrite if a solver result was Unknown
442+
SMT.IsUnknown reason -> do
443+
-- abort rewrite if a solver result was Unknown
444+
withContext CtxAbort $ logMessage reason
445+
smtUnclear stillUnclear
453446
SMT.IsInvalid -> do
454447
-- requires is actually false given the prior
455448
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
@@ -467,10 +460,23 @@ applyRule pat@Pattern{ceilConditions} rule =
467460

468461
-- check all new constraints together with the known side constraints
469462
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
463+
-- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions.
464+
-- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)).
470465
(lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case
471466
SMT.IsInvalid -> do
472467
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
473468
RewriteRuleAppT $ pure Trivial
469+
SMT.IsUnknown SMT.InconsistentGroundTruth -> do
470+
withContext CtxSuccess $ logMessage ("Ground truth is #Bottom." :: Text)
471+
RewriteRuleAppT $ pure Trivial
472+
SMT.IsUnknown SMT.ImplicationIndeterminate -> do
473+
-- the new constraint is satisfiable, continue
474+
pure ()
475+
SMT.IsUnknown reason -> do
476+
-- abort rewrite if a solver result was Unknown for a reason other
477+
-- then SMT.ImplicationIndeterminate of SMT.InconsistentGroundTruth
478+
withContext CtxAbort $ logMessage reason
479+
smtUnclear newConstraints
474480
_other ->
475481
pure ()
476482

@@ -482,6 +488,18 @@ applyRule pat@Pattern{ceilConditions} rule =
482488
lift . RewriteT . lift . modify $ \s -> s{equations = mempty}
483489
pure newConstraints
484490

491+
smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) ()
492+
smtUnclear predicates = do
493+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
494+
withContext CtxConstraint . withContext CtxAbort . logMessage $
495+
WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> predicates)]) $
496+
renderOneLineText $
497+
"Uncertain about condition(s) in a rule:"
498+
<+> (hsep . punctuate comma . map (pretty' @mods) $ predicates)
499+
failRewrite $
500+
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
501+
map coerce predicates
502+
485503
{- | Reason why a rewrite did not produce a result. Contains additional
486504
information for logging what happened during the rewrite.
487505
-}

‎booster/library/Booster/SMT/Interface.hs

+34-8
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ module Booster.SMT.Interface (
1212
SMTOptions (..), -- re-export
1313
defaultSMTOptions, -- re-export
1414
SMTError (..),
15+
UnknownReason (..),
1516
initSolver,
1617
noSolver,
1718
finaliseSolver,
@@ -33,6 +34,7 @@ import Control.Monad
3334
import Control.Monad.IO.Class
3435
import Control.Monad.Trans.State
3536
import Data.Aeson (object, (.=))
37+
import Data.Aeson.Types (FromJSON (..), ToJSON (..))
3638
import Data.ByteString.Char8 qualified as BS
3739
import Data.Coerce
3840
import Data.Data (Proxy)
@@ -44,6 +46,14 @@ import Data.Map qualified as Map
4446
import Data.Set (Set)
4547
import Data.Set qualified as Set
4648
import Data.Text as Text (Text, pack, unlines, unwords)
49+
import Deriving.Aeson (
50+
CamelToKebab,
51+
CustomJSON (..),
52+
FieldLabelModifier,
53+
OmitNothingFields,
54+
StripPrefix,
55+
)
56+
import GHC.Generics (Generic)
4757
import Prettyprinter (Pretty, backslash, hsep, punctuate, slash, (<+>))
4858
import SMTLIB.Backends.Process qualified as Backend
4959

@@ -188,12 +198,28 @@ finaliseSolver ctxt = do
188198
Log.logMessage ("Closing SMT solver" :: Text)
189199
destroyContext ctxt
190200

191-
pattern IsUnknown :: unknown -> Either unknown b
201+
data UnknownReason
202+
= -- | SMT prelude is UNSAT
203+
InconsistentGroundTruth
204+
| -- | (P, not P) is (SAT, SAT)
205+
ImplicationIndeterminate
206+
| -- | SMT solver returned unknown
207+
SMTUnknownReason Text
208+
deriving (Show, Eq, Generic)
209+
deriving
210+
(FromJSON, ToJSON)
211+
via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] UnknownReason
212+
213+
instance Log.ToLogFormat UnknownReason where
214+
toTextualLog = pack . show
215+
toJSONLog = toJSON
216+
217+
pattern IsUnknown :: UnknownReason -> Either UnknownReason b
192218
pattern IsUnknown u = Left u
193219

194220
newtype IsSat' a = IsSat' (Maybe a) deriving (Functor)
195221

196-
type IsSatResult a = Either Text (IsSat' a)
222+
type IsSatResult a = Either UnknownReason (IsSat' a)
197223

198224
pattern IsSat :: a -> IsSatResult a
199225
pattern IsSat a = Right (IsSat' (Just a))
@@ -243,7 +269,7 @@ isSatReturnTransState ctxt ps subst
243269
SMT.runCmd CheckSat >>= \case
244270
Sat -> pure $ IsSat transState
245271
Unsat -> pure IsUnsat
246-
Unknown reason -> retry (solve smtToCheck transState) (pure $ IsUnknown reason)
272+
Unknown reason -> retry (solve smtToCheck transState) (pure $ IsUnknown (SMTUnknownReason reason))
247273
other -> do
248274
let msg = "Unexpected result while calling 'check-sat': " <> show other
249275
Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg
@@ -347,7 +373,7 @@ mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded]
347373

348374
newtype IsValid' = IsValid' Bool
349375

350-
type IsValidResult = Either (Maybe Text) IsValid'
376+
type IsValidResult = Either UnknownReason IsValid'
351377

352378
pattern IsValid, IsInvalid :: IsValidResult
353379
pattern IsValid = Right (IsValid' True)
@@ -418,14 +444,14 @@ checkPredicates ctxt givenPs givenSubst psToCheck
418444
hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck))
419445
result <- interactWithSolver smtGiven sexprsToCheck
420446
case result of
421-
(Unsat, Unsat) -> pure $ IsUnknown Nothing -- defensive choice for inconsistent ground truth
447+
(Unsat, Unsat) -> pure $ IsUnknown InconsistentGroundTruth
422448
(Sat, Sat) -> do
423449
Log.logMessage ("Implication not determined" :: Text)
424-
pure $ IsUnknown Nothing
450+
pure $ IsUnknown ImplicationIndeterminate
425451
(Sat, Unsat) -> pure IsValid
426452
(Unsat, Sat) -> pure IsInvalid
427-
(Unknown reason, _) -> retry (solve smtGiven sexprsToCheck transState) (pure $ IsUnknown $ Just reason)
428-
(_, Unknown reason) -> retry (solve smtGiven sexprsToCheck transState) (pure $ IsUnknown $ Just reason)
453+
(Unknown reason, _) -> retry (solve smtGiven sexprsToCheck transState) (pure . IsUnknown . SMTUnknownReason $ reason)
454+
(_, Unknown reason) -> retry (solve smtGiven sexprsToCheck transState) (pure . IsUnknown . SMTUnknownReason $ reason)
429455
other ->
430456
throwSMT $
431457
"Unexpected result while checking a condition: " <> Text.pack (show other)

‎booster/test/rpc-integration/test-substitutions/README.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,6 @@ NB: Booster applies the given substitution before performing any action.
4242
* `state-symbolic-bottom-predicate.execute`
4343
- starts from `symbolic-subst`
4444
- with an equation that is instantly false: `X = 1 +Int X`
45-
- leading to a vacuous state in `kore-rpc-booster` after rewriting once,
45+
- leading to a vacuous state in `kore-rpc-booster` and `booster-dev` at 0 steps,
4646
- while `kore-rpc-dev` returns `stuck` instantly after 0 steps,
4747
returning the exact input as `state`.

‎booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev

+7-55
Original file line numberDiff line numberDiff line change
@@ -225,61 +225,13 @@
225225
}
226226
},
227227
{
228-
"tag": "App",
229-
"name": "Lbl'UndsPlus'Int'Unds'",
230-
"sorts": [],
231-
"args": [
232-
{
233-
"tag": "App",
234-
"name": "Lbl'UndsPlus'Int'Unds'",
235-
"sorts": [],
236-
"args": [
237-
{
238-
"tag": "EVar",
239-
"name": "X",
240-
"sort": {
241-
"tag": "SortApp",
242-
"name": "SortInt",
243-
"args": []
244-
}
245-
},
246-
{
247-
"tag": "DV",
248-
"sort": {
249-
"tag": "SortApp",
250-
"name": "SortInt",
251-
"args": []
252-
},
253-
"value": "1"
254-
}
255-
]
256-
},
257-
{
258-
"tag": "App",
259-
"name": "Lbl'Unds'-Int'Unds'",
260-
"sorts": [],
261-
"args": [
262-
{
263-
"tag": "DV",
264-
"sort": {
265-
"tag": "SortApp",
266-
"name": "SortInt",
267-
"args": []
268-
},
269-
"value": "0"
270-
},
271-
{
272-
"tag": "DV",
273-
"sort": {
274-
"tag": "SortApp",
275-
"name": "SortInt",
276-
"args": []
277-
},
278-
"value": "1"
279-
}
280-
]
281-
}
282-
]
228+
"tag": "EVar",
229+
"name": "X",
230+
"sort": {
231+
"tag": "SortApp",
232+
"name": "SortInt",
233+
"args": []
234+
}
283235
}
284236
]
285237
}

0 commit comments

Comments
 (0)