Skip to content

Commit edf6e66

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 4fb57a8 + ad8a7ff commit edf6e66

File tree

7 files changed

+142
-260
lines changed

7 files changed

+142
-260
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 2 additions & 2 deletions
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

Lines changed: 29 additions & 11 deletions
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

Lines changed: 34 additions & 8 deletions
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 7 additions & 55 deletions
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)