Skip to content

Refactor booster smt #4017

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 13 commits into from
Aug 7, 2024
Merged

Refactor booster smt #4017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
7ca620f
Use the same code to update SMT options on retries
geo2a Aug 5, 2024
a214d48
Refactor SMT.Response
geo2a Aug 6, 2024
046a1b2
Rename ResponseMay to ResponseUnresolved
geo2a Aug 6, 2024
b738d80
Merge remote-tracking branch 'origin/master' into georgy/refactor-boo…
goodlyrottenapple Aug 6, 2024
cc76bc8
big refactor
goodlyrottenapple Aug 6, 2024
2a391e4
revert the need for MonadCatch
goodlyrottenapple Aug 6, 2024
e61c48e
fourmolu
goodlyrottenapple Aug 6, 2024
7794b6e
Add separate IsValidResult for checkPredicates
goodlyrottenapple Aug 7, 2024
28ed5be
fix
goodlyrottenapple Aug 7, 2024
f011f16
fix comment
goodlyrottenapple Aug 7, 2024
bf90f72
remove monadcatch/throw
goodlyrottenapple Aug 7, 2024
0b6b793
restore logging
goodlyrottenapple Aug 7, 2024
08323dc
Merge branch 'master' into georgy/refactor-booster-smt
goodlyrottenapple Aug 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 21 additions & 32 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ module Booster.JsonRpc (

import Control.Applicative ((<|>))
import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
import Control.Exception qualified as Exception
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
Expand Down Expand Up @@ -66,7 +65,6 @@ import Booster.Pattern.Util (
substituteInTerm,
)
import Booster.Prettyprinter (renderDefault, renderText)
import Booster.SMT.Base qualified as SMT
import Booster.SMT.Interface qualified as SMT
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
import Booster.Syntax.Json.Externalise
Expand Down Expand Up @@ -368,32 +366,16 @@ respond stateVar request =
withContext CtxGetModel $
withContext CtxSMT $
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
pure $ Left $ SMT.Unknown $ Just "No predicates or substitutions given"
pure $ SMT.IsUnknown "No predicates or substitutions given"
else do
solver <- SMT.initSolver def smtOptions
result <- SMT.getModelFor solver boolPs suppliedSubst
SMT.finaliseSolver solver
case result of
Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
Right response -> pure response
withContext CtxGetModel $
withContext CtxSMT $
pure result
withContext CtxGetModel $ withContext CtxSMT $ case smtResult of
SMT.IsSat subst -> do
logMessage $
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
pure . Right . RpcTypes.GetModel $ case smtResult of
Left SMT.Unsat ->
RpcTypes.GetModelResult
{ satisfiable = RpcTypes.Unsat
, substitution = Nothing
}
Left SMT.Unknown{} ->
RpcTypes.GetModelResult
{ satisfiable = RpcTypes.Unknown
, substitution = Nothing
}
Left other ->
error $ "Unexpected result " <> show other <> " from getModelFor"
Right subst ->
"SMT result: " <> pack ((("Subst: " <>) . show . Map.size) subst)
let sort = fromMaybe (error "Unknown sort in input") $ sortOfJson req.state.term
substitution
| Map.null subst = Nothing
Expand All @@ -415,10 +397,25 @@ respond stateVar request =
(externaliseTerm term)
| (var, term) <- Map.assocs subst
]
in RpcTypes.GetModelResult
pure . Right . RpcTypes.GetModel $
RpcTypes.GetModelResult
{ satisfiable = RpcTypes.Sat
, substitution
}
SMT.IsUnsat -> do
logMessage ("SMT result: Unsat" :: Text)
pure . Right . RpcTypes.GetModel $
RpcTypes.GetModelResult
{ satisfiable = RpcTypes.Unsat
, substitution = Nothing
}
SMT.IsUnknown reason -> do
logMessage $ "SMT result: Unknown - " <> reason
pure . Right . RpcTypes.GetModel $
RpcTypes.GetModelResult
{ satisfiable = RpcTypes.Unknown
, substitution = Nothing
}
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxImplies $ do
-- internalise given constrained term
let internalised =
Expand Down Expand Up @@ -552,14 +549,6 @@ handleSmtError :: JsonRpcHandler
handleSmtError = JsonRpcHandler $ \case
SMT.GeneralSMTError err -> runtimeError "problem" err
SMT.SMTTranslationError err -> runtimeError "translation" err
SMT.SMTSolverUnknown reason premises preds -> do
let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
pure $
RpcError.backendError $
RpcError.SmtSolverError $
RpcError.ErrorWithTerm (fromMaybe "UNKNOWN" reason) allPreds
where
runtimeError prefix err = do
let msg = "SMT " <> prefix <> ": " <> err
Expand Down
68 changes: 27 additions & 41 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ module Booster.Pattern.ApplyEquations (
evaluateConstraints,
) where

import Control.Exception qualified as Exception (throw)
import Control.Monad
import Control.Monad.Extra (fromMaybeM, whenJust)
import Control.Monad.IO.Class (MonadIO (..))
Expand Down Expand Up @@ -867,40 +866,31 @@ applyEquation term rule =
-- check any conditions that are still unclear with the SMT solver
-- (or abort if no solver is being used), abort if still unclear after
unless (null stillUnclear) $
let checkWithSmt :: SMT.SMTContext -> EquationT io (Maybe Bool)
checkWithSmt smt =
SMT.checkPredicates smt knownPredicates mempty (Set.fromList stillUnclear) >>= \case
Left SMT.SMTSolverUnknown{} -> do
pure Nothing
Left other ->
liftIO $ Exception.throw other
Right result ->
pure result
in lift (checkWithSmt solver) >>= \case
Nothing -> do
-- no solver or still unclear: abort
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
renderOneLineText
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
)
, IndeterminateCondition stillUnclear
)
Just False -> do
-- actually false given path condition: fail
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
, ConditionFalse failedP
)
Just True -> do
-- can proceed
pure ()
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
SMT.IsUnknown{} -> do
-- no solver or still unclear: abort
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
renderOneLineText
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
)
, IndeterminateCondition stillUnclear
)
SMT.IsInvalid -> do
-- actually false given path condition: fail
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
, ConditionFalse failedP
)
SMT.IsValid{} -> do
-- can proceed
pure ()

-- check ensured conditions, filter any
-- true ones, prune if any is false
Expand All @@ -917,7 +907,7 @@ applyEquation term rule =
ensured
-- check all ensured conditions together with the path condition
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
Right (Just False) -> do
SMT.IsInvalid -> do
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
throwE
( \ctx ->
Expand All @@ -926,12 +916,8 @@ applyEquation term rule =
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
, EnsuresFalse falseEnsures
)
Right _other ->
pure ()
Left SMT.SMTSolverUnknown{} ->
_ ->
pure ()
Left other ->
liftIO $ Exception.throw other
lift $ pushConstraints $ Set.fromList ensuredConditions
-- when a new path condition is added, invalidate the equation cache
unless (null ensuredConditions) $ do
Expand Down
24 changes: 6 additions & 18 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ module Booster.Pattern.Rewrite (
) where

import Control.Applicative ((<|>))
import Control.Exception qualified as Exception (throw)
import Control.Monad
import Control.Monad.Extra (whenJust)
import Control.Monad.IO.Class (MonadIO (..))
Expand Down Expand Up @@ -364,22 +363,15 @@ applyRule pat@Pattern{ceilConditions} rule =
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
map coerce stillUnclear

checkAllRequires <-
SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear)

case checkAllRequires of
Left SMT.SMTSolverUnknown{} ->
SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear) >>= \case
SMT.IsUnknown{} ->
smtUnclear -- abort rewrite if a solver result was Unknown
Left other ->
liftIO $ Exception.throw other -- fail hard on other SMT errors
Right (Just False) -> do
SMT.IsInvalid -> do
-- requires is actually false given the prior
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure NotApplied
Right (Just True) ->
SMT.IsValid ->
pure () -- can proceed
Right Nothing ->
smtUnclear -- no implication could be determined

-- check ensures constraints (new) from rhs: stop and return `Trivial` if
-- any are false, remove all that are trivially true, return the rest
Expand All @@ -392,15 +384,11 @@ applyRule pat@Pattern{ceilConditions} rule =

-- check all new constraints together with the known side constraints
(lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
Right (Just False) -> do
SMT.IsInvalid -> do
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
RewriteRuleAppT $ pure Trivial
Right _other ->
pure ()
Left SMT.SMTSolverUnknown{} ->
_other ->
pure ()
Left other ->
liftIO $ Exception.throw other

-- if a new constraint is going to be added, the equation cache is invalid
unless (null newConstraints) $ do
Expand Down
10 changes: 7 additions & 3 deletions booster/library/Booster/SMT/Base.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveLift #-}

{- |
Expand Down Expand Up @@ -77,14 +78,17 @@ data QueryCommand
| GetReasonUnknown
deriving stock (Eq, Ord, Show)

data Response
data Response' reason
= Success -- for command_
| Sat
| Unsat
| Unknown (Maybe Text)
| Unknown reason
| Values [(SExpr, Value)]
| Error BS.ByteString
deriving stock (Eq, Ord, Show)
deriving stock (Eq, Ord, Show, Functor)

type Response = Response' Text
type ResponseUnresolved = Response' (Maybe Text)

-- Common values returned by SMT solvers.
data Value
Expand Down
Loading
Loading