Skip to content

Commit b6f8807

Browse files
goodlyrottenapplegeo2a
goodlyrottenapple
and
geo2a
authored
Refactor booster smt (#4017)
The following changes were made: * SMT response in the hihg-level interface always returns a `Text` reason in the `Unknown` constructor * All the main functions, i.e. `isSat`, `checkPredicates` and `getModelFor` throw errors as Exceptions and return an `IsSatResult`, as the only error we are catching is the one thrown when the SMT result is unknown --------- Co-authored-by: Georgy Lukyanov <[email protected]>
1 parent 3ed541b commit b6f8807

File tree

8 files changed

+259
-275
lines changed

8 files changed

+259
-275
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 21 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ module Booster.JsonRpc (
1818

1919
import Control.Applicative ((<|>))
2020
import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
21-
import Control.Exception qualified as Exception
2221
import Control.Monad
2322
import Control.Monad.IO.Class
2423
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
@@ -66,7 +65,6 @@ import Booster.Pattern.Util (
6665
substituteInTerm,
6766
)
6867
import Booster.Prettyprinter (renderDefault, renderText)
69-
import Booster.SMT.Base qualified as SMT
7068
import Booster.SMT.Interface qualified as SMT
7169
import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
7270
import Booster.Syntax.Json.Externalise
@@ -368,32 +366,16 @@ respond stateVar request =
368366
withContext CtxGetModel $
369367
withContext CtxSMT $
370368
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
371-
pure $ Left $ SMT.Unknown $ Just "No predicates or substitutions given"
369+
pure $ SMT.IsUnknown "No predicates or substitutions given"
372370
else do
373371
solver <- SMT.initSolver def smtOptions
374372
result <- SMT.getModelFor solver boolPs suppliedSubst
375373
SMT.finaliseSolver solver
376-
case result of
377-
Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
378-
Right response -> pure response
379-
withContext CtxGetModel $
380-
withContext CtxSMT $
374+
pure result
375+
withContext CtxGetModel $ withContext CtxSMT $ case smtResult of
376+
SMT.IsSat subst -> do
381377
logMessage $
382-
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
383-
pure . Right . RpcTypes.GetModel $ case smtResult of
384-
Left SMT.Unsat ->
385-
RpcTypes.GetModelResult
386-
{ satisfiable = RpcTypes.Unsat
387-
, substitution = Nothing
388-
}
389-
Left SMT.Unknown{} ->
390-
RpcTypes.GetModelResult
391-
{ satisfiable = RpcTypes.Unknown
392-
, substitution = Nothing
393-
}
394-
Left other ->
395-
error $ "Unexpected result " <> show other <> " from getModelFor"
396-
Right subst ->
378+
"SMT result: " <> pack ((("Subst: " <>) . show . Map.size) subst)
397379
let sort = fromMaybe (error "Unknown sort in input") $ sortOfJson req.state.term
398380
substitution
399381
| Map.null subst = Nothing
@@ -415,10 +397,25 @@ respond stateVar request =
415397
(externaliseTerm term)
416398
| (var, term) <- Map.assocs subst
417399
]
418-
in RpcTypes.GetModelResult
400+
pure . Right . RpcTypes.GetModel $
401+
RpcTypes.GetModelResult
419402
{ satisfiable = RpcTypes.Sat
420403
, substitution
421404
}
405+
SMT.IsUnsat -> do
406+
logMessage ("SMT result: Unsat" :: Text)
407+
pure . Right . RpcTypes.GetModel $
408+
RpcTypes.GetModelResult
409+
{ satisfiable = RpcTypes.Unsat
410+
, substitution = Nothing
411+
}
412+
SMT.IsUnknown reason -> do
413+
logMessage $ "SMT result: Unknown - " <> reason
414+
pure . Right . RpcTypes.GetModel $
415+
RpcTypes.GetModelResult
416+
{ satisfiable = RpcTypes.Unknown
417+
, substitution = Nothing
418+
}
422419
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxImplies $ do
423420
-- internalise given constrained term
424421
let internalised =
@@ -552,14 +549,6 @@ handleSmtError :: JsonRpcHandler
552549
handleSmtError = JsonRpcHandler $ \case
553550
SMT.GeneralSMTError err -> runtimeError "problem" err
554551
SMT.SMTTranslationError err -> runtimeError "translation" err
555-
SMT.SMTSolverUnknown reason premises preds -> do
556-
let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
557-
externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
558-
allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
559-
pure $
560-
RpcError.backendError $
561-
RpcError.SmtSolverError $
562-
RpcError.ErrorWithTerm (fromMaybe "UNKNOWN" reason) allPreds
563552
where
564553
runtimeError prefix err = do
565554
let msg = "SMT " <> prefix <> ": " <> err

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

Lines changed: 27 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,6 @@ module Booster.Pattern.ApplyEquations (
2727
evaluateConstraints,
2828
) where
2929

30-
import Control.Exception qualified as Exception (throw)
3130
import Control.Monad
3231
import Control.Monad.Extra (fromMaybeM, whenJust)
3332
import Control.Monad.IO.Class (MonadIO (..))
@@ -867,40 +866,31 @@ applyEquation term rule =
867866
-- check any conditions that are still unclear with the SMT solver
868867
-- (or abort if no solver is being used), abort if still unclear after
869868
unless (null stillUnclear) $
870-
let checkWithSmt :: SMT.SMTContext -> EquationT io (Maybe Bool)
871-
checkWithSmt smt =
872-
SMT.checkPredicates smt knownPredicates mempty (Set.fromList stillUnclear) >>= \case
873-
Left SMT.SMTSolverUnknown{} -> do
874-
pure Nothing
875-
Left other ->
876-
liftIO $ Exception.throw other
877-
Right result ->
878-
pure result
879-
in lift (checkWithSmt solver) >>= \case
880-
Nothing -> do
881-
-- no solver or still unclear: abort
882-
throwE
883-
( \ctx ->
884-
ctx . logMessage $
885-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
886-
renderOneLineText
887-
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
888-
)
889-
, IndeterminateCondition stillUnclear
890-
)
891-
Just False -> do
892-
-- actually false given path condition: fail
893-
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
894-
throwE
895-
( \ctx ->
896-
ctx . logMessage $
897-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
898-
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
899-
, ConditionFalse failedP
900-
)
901-
Just True -> do
902-
-- can proceed
903-
pure ()
869+
lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case
870+
SMT.IsUnknown{} -> do
871+
-- no solver or still unclear: abort
872+
throwE
873+
( \ctx ->
874+
ctx . logMessage $
875+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
876+
renderOneLineText
877+
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
878+
)
879+
, IndeterminateCondition stillUnclear
880+
)
881+
SMT.IsInvalid -> do
882+
-- actually false given path condition: fail
883+
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
884+
throwE
885+
( \ctx ->
886+
ctx . logMessage $
887+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
888+
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
889+
, ConditionFalse failedP
890+
)
891+
SMT.IsValid{} -> do
892+
-- can proceed
893+
pure ()
904894

905895
-- check ensured conditions, filter any
906896
-- true ones, prune if any is false
@@ -917,7 +907,7 @@ applyEquation term rule =
917907
ensured
918908
-- check all ensured conditions together with the path condition
919909
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
920-
Right (Just False) -> do
910+
SMT.IsInvalid -> do
921911
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
922912
throwE
923913
( \ctx ->
@@ -926,12 +916,8 @@ applyEquation term rule =
926916
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
927917
, EnsuresFalse falseEnsures
928918
)
929-
Right _other ->
930-
pure ()
931-
Left SMT.SMTSolverUnknown{} ->
919+
_ ->
932920
pure ()
933-
Left other ->
934-
liftIO $ Exception.throw other
935921
lift $ pushConstraints $ Set.fromList ensuredConditions
936922
-- when a new path condition is added, invalidate the equation cache
937923
unless (null ensuredConditions) $ do

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

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ module Booster.Pattern.Rewrite (
2121
) where
2222

2323
import Control.Applicative ((<|>))
24-
import Control.Exception qualified as Exception (throw)
2524
import Control.Monad
2625
import Control.Monad.Extra (whenJust)
2726
import Control.Monad.IO.Class (MonadIO (..))
@@ -364,22 +363,15 @@ applyRule pat@Pattern{ceilConditions} rule =
364363
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
365364
map coerce stillUnclear
366365

367-
checkAllRequires <-
368-
SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear)
369-
370-
case checkAllRequires of
371-
Left SMT.SMTSolverUnknown{} ->
366+
SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear) >>= \case
367+
SMT.IsUnknown{} ->
372368
smtUnclear -- abort rewrite if a solver result was Unknown
373-
Left other ->
374-
liftIO $ Exception.throw other -- fail hard on other SMT errors
375-
Right (Just False) -> do
369+
SMT.IsInvalid -> do
376370
-- requires is actually false given the prior
377371
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
378372
RewriteRuleAppT $ pure NotApplied
379-
Right (Just True) ->
373+
SMT.IsValid ->
380374
pure () -- can proceed
381-
Right Nothing ->
382-
smtUnclear -- no implication could be determined
383375

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

393385
-- check all new constraints together with the known side constraints
394386
(lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
395-
Right (Just False) -> do
387+
SMT.IsInvalid -> do
396388
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
397389
RewriteRuleAppT $ pure Trivial
398-
Right _other ->
399-
pure ()
400-
Left SMT.SMTSolverUnknown{} ->
390+
_other ->
401391
pure ()
402-
Left other ->
403-
liftIO $ Exception.throw other
404392

405393
-- if a new constraint is going to be added, the equation cache is invalid
406394
unless (null newConstraints) $ do

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

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
{-# LANGUAGE DeriveDataTypeable #-}
2+
{-# LANGUAGE DeriveFunctor #-}
23
{-# LANGUAGE DeriveLift #-}
34

45
{- |
@@ -77,14 +78,17 @@ data QueryCommand
7778
| GetReasonUnknown
7879
deriving stock (Eq, Ord, Show)
7980

80-
data Response
81+
data Response' reason
8182
= Success -- for command_
8283
| Sat
8384
| Unsat
84-
| Unknown (Maybe Text)
85+
| Unknown reason
8586
| Values [(SExpr, Value)]
8687
| Error BS.ByteString
87-
deriving stock (Eq, Ord, Show)
88+
deriving stock (Eq, Ord, Show, Functor)
89+
90+
type Response = Response' Text
91+
type ResponseUnresolved = Response' (Maybe Text)
8892

8993
-- Common values returned by SMT solvers.
9094
data Value

0 commit comments

Comments
 (0)