Skip to content

Commit

Permalink
Extend Unknown type, abort on unsafe unknown ensures
Browse files Browse the repository at this point in the history
  • Loading branch information
geo2a committed Oct 17, 2024
1 parent 748c998 commit bc44927
Show file tree
Hide file tree
Showing 5 changed files with 73 additions and 217 deletions.
4 changes: 2 additions & 2 deletions booster/library/Booster/JsonRpc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -365,7 +365,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 @@ -409,7 +409,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: 28 additions & 12 deletions booster/library/Booster/Pattern/Rewrite.hs
Original file line number Diff line number Diff line change
Expand Up @@ -307,7 +307,7 @@ applyRule pat@Pattern{ceilConditions} rule =
MatchSuccess matchingSubstitution -> do
-- existential variables may be present in rule.rhs and rule.ensures,
-- need to strip prefixes and freshen their names with respect to variables already
-- present in the input pattern and in the unification substitution
-- present in the input pattern and in the matching substitution
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution
Expand Down Expand Up @@ -498,18 +498,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 pat.substitution (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 @@ -534,15 +527,38 @@ 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 pat.substitution (Set.fromList newConstraints)) >>= \case
SMT.IsUnknown SMT.ImplicationIndeterminate -> do
pure ()
SMT.IsUnknown SMT.InconsistentGroundTruth -> do
withContext CtxWarn $ logMessage ("Ground truth is #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
SMT.IsInvalid -> do
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
SMT.IsUnknown reason -> do
-- abort rewrite if a solver result was Unknown for reason other then SMT.ImplicationIndeterminate
withContext CtxAbort $ logMessage reason
smtUnclear newConstraints
_other ->
pure ()

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
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

This file was deleted.

Loading

0 comments on commit bc44927

Please sign in to comment.