Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
devops committed Oct 17, 2024
2 parents 4fb57a8 + ad8a7ff commit edf6e66
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 (..),
UnknownReason (..),
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 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 "_"]] UnknownReason

instance Log.ToLogFormat UnknownReason where
toTextualLog = pack . show
toJSONLog = toJSON

pattern IsUnknown :: UnknownReason -> Either UnknownReason 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 UnknownReason (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 UnknownReason 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 edf6e66

Please sign in to comment.