Skip to content

Commit f66df15

Browse files
goodlyrottenapplegithub-actionsgeo2a
authored
Make SMTContext mandatory and merge Unknown with ReasonUnknown (#4003)
I have changed my mind and think we should have `SMTContext` mandatory and not an optional, as the current design makes it way too easy to give a default `Nothing` value when extending the code-base in the future. This then has the potential to re-introduce a similar bug. Another advantage tot his approach is the removal of the ugly pattern matching present each time we actually want to use the solver. Instead, in this PR, the `Maybe` is pushed into `SMTContext`, where the dummy/empty instance now has to be consciously built using the new `noSolver` function. The fallout is fairly minimal and we confide the logic of not having a solver to the SMT interface. I.e. the only places where not having a solver has a different behavior are: * `hardReset` - becomes a no-op when no solver handle is present * `runCmd` -> always returns the `Unknown` response when no solver exists This eliminates duplicate instances of handling an unknown response vs not having a solver, since in all instances of the current code-base, they are functionally the same. --------- Co-authored-by: github-actions <[email protected]> Co-authored-by: Georgy Lukyanov <[email protected]>
1 parent 3b90f2b commit f66df15

File tree

12 files changed

+222
-214
lines changed

12 files changed

+222
-214
lines changed

‎booster/library/Booster/Definition/Ceil.hs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import Booster.Log
1818
import Booster.Pattern.Bool
1919
import Booster.Pattern.Pretty
2020
import Booster.Pattern.Util (isConcrete, sortOfTerm)
21+
import Booster.SMT.Interface
2122
import Booster.Util (Flag (..))
2223
import Control.DeepSeq (NFData)
2324
import Control.Monad (foldM)
@@ -101,7 +102,8 @@ computeCeilRule ::
101102
computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
102103
| null computedAttributes.notPreservesDefinednessReasons = pure Nothing
103104
| otherwise = do
104-
(res, _) <- runEquationT def mllvm Nothing mempty mempty $ do
105+
ns <- noSolver
106+
(res, _) <- runEquationT def mllvm ns mempty mempty $ do
105107
lhsCeils <- Set.fromList <$> computeCeil lhs
106108
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
107109
let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList

‎booster/library/Booster/JsonRpc.hs

Lines changed: 11 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ import Control.Applicative ((<|>))
2020
import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
2121
import Control.Exception qualified as Exception
2222
import Control.Monad
23-
import Control.Monad.Extra (whenJust)
2423
import Control.Monad.IO.Class
2524
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
2625
import Crypto.Hash (SHA256 (..), hashWith)
@@ -145,10 +144,10 @@ respond stateVar request =
145144
, ceilConditions = pat.ceilConditions
146145
}
147146

148-
solver <- traverse (SMT.initSolver def) mSMTOptions
147+
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
149148
result <-
150149
performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat
151-
whenJust solver SMT.finaliseSolver
150+
SMT.finaliseSolver solver
152151
stop <- liftIO $ getTime Monotonic
153152
let duration =
154153
if fromMaybe False req.logTiming
@@ -228,7 +227,7 @@ respond stateVar request =
228227
| otherwise =
229228
Nothing
230229

231-
solver <- traverse (SMT.initSolver def) mSMTOptions
230+
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
232231

233232
result <- case internalised of
234233
Left patternErrors -> do
@@ -299,7 +298,7 @@ respond stateVar request =
299298
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
300299
(Left something, _) ->
301300
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something
302-
whenJust solver SMT.finaliseSolver
301+
SMT.finaliseSolver solver
303302
stop <- liftIO $ getTime Monotonic
304303

305304
let duration =
@@ -362,7 +361,7 @@ respond stateVar request =
362361
withContext CtxGetModel $
363362
withContext CtxSMT $
364363
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
365-
pure $ Left SMT.Unknown
364+
pure $ Left $ SMT.Unknown $ Just "No predicates or substitutions given"
366365
else do
367366
solver <- SMT.initSolver def smtOptions
368367
result <- SMT.getModelFor solver boolPs suppliedSubst
@@ -380,12 +379,7 @@ respond stateVar request =
380379
{ satisfiable = RpcTypes.Unsat
381380
, substitution = Nothing
382381
}
383-
Left SMT.ReasonUnknown{} ->
384-
RpcTypes.GetModelResult
385-
{ satisfiable = RpcTypes.Unknown
386-
, substitution = Nothing
387-
}
388-
Left SMT.Unknown ->
382+
Left SMT.Unknown{} ->
389383
RpcTypes.GetModelResult
390384
{ satisfiable = RpcTypes.Unknown
391385
, substitution = Nothing
@@ -485,7 +479,7 @@ respond stateVar request =
485479
MatchSuccess subst -> do
486480
let filteredConsequentPreds =
487481
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
488-
solver <- traverse (SMT.initSolver def) mSMTOptions
482+
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
489483

490484
if null filteredConsequentPreds
491485
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
@@ -555,7 +549,10 @@ handleSmtError = JsonRpcHandler $ \case
555549
let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
556550
externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
557551
allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
558-
pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds
552+
pure $
553+
RpcError.backendError $
554+
RpcError.SmtSolverError $
555+
RpcError.ErrorWithTerm (fromMaybe "UNKNOWN" reason) allPreds
559556
where
560557
runtimeError prefix err = do
561558
let msg = "SMT " <> prefix <> ": " <> err

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

Lines changed: 27 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ instance Pretty (PrettyWithModifiers mods EquationFailure) where
144144
data EquationConfig = EquationConfig
145145
{ definition :: KoreDefinition
146146
, llvmApi :: Maybe LLVM.API
147-
, smtSolver :: Maybe SMT.SMTContext
147+
, smtSolver :: SMT.SMTContext
148148
, maxRecursion :: Bound "Recursion"
149149
, maxIterations :: Bound "Iterations"
150150
, logger :: Logger LogMessage
@@ -281,7 +281,7 @@ runEquationT ::
281281
LoggerMIO io =>
282282
KoreDefinition ->
283283
Maybe LLVM.API ->
284-
Maybe SMT.SMTContext ->
284+
SMT.SMTContext ->
285285
SimplifierCache ->
286286
Set Predicate ->
287287
EquationT io a ->
@@ -394,7 +394,7 @@ evaluateTerm ::
394394
Direction ->
395395
KoreDefinition ->
396396
Maybe LLVM.API ->
397-
Maybe SMT.SMTContext ->
397+
SMT.SMTContext ->
398398
Set Predicate ->
399399
Term ->
400400
io (Either EquationFailure Term, SimplifierCache)
@@ -417,7 +417,7 @@ evaluatePattern ::
417417
LoggerMIO io =>
418418
KoreDefinition ->
419419
Maybe LLVM.API ->
420-
Maybe SMT.SMTContext ->
420+
SMT.SMTContext ->
421421
SimplifierCache ->
422422
Pattern ->
423423
io (Either EquationFailure Pattern, SimplifierCache)
@@ -462,7 +462,7 @@ evaluateConstraints ::
462462
LoggerMIO io =>
463463
KoreDefinition ->
464464
Maybe LLVM.API ->
465-
Maybe SMT.SMTContext ->
465+
SMT.SMTContext ->
466466
SimplifierCache ->
467467
Set Predicate ->
468468
io (Either EquationFailure (Set Predicate), SimplifierCache)
@@ -828,7 +828,7 @@ applyEquation term rule =
828828
-- could now be syntactically present in the path constraints, filter again
829829
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
830830

831-
mbSolver :: Maybe SMT.SMTContext <- (.smtSolver) <$> lift getConfig
831+
solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
832832

833833
-- check any conditions that are still unclear with the SMT solver
834834
-- (or abort if no solver is being used), abort if still unclear after
@@ -842,7 +842,7 @@ applyEquation term rule =
842842
liftIO $ Exception.throw other
843843
Right result ->
844844
pure result
845-
in maybe (pure Nothing) (lift . checkWithSmt) mbSolver >>= \case
845+
in lift (checkWithSmt solver) >>= \case
846846
Nothing -> do
847847
-- no solver or still unclear: abort
848848
throwE
@@ -882,23 +882,22 @@ applyEquation term rule =
882882
)
883883
ensured
884884
-- check all ensured conditions together with the path condition
885-
whenJust mbSolver $ \solver -> do
886-
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
887-
Right (Just False) -> do
888-
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
889-
throwE
890-
( \ctx ->
891-
ctx . logMessage $
892-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
893-
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
894-
, EnsuresFalse falseEnsures
895-
)
896-
Right _other ->
897-
pure ()
898-
Left SMT.SMTSolverUnknown{} ->
899-
pure ()
900-
Left other ->
901-
liftIO $ Exception.throw other
885+
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
886+
Right (Just False) -> do
887+
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
888+
throwE
889+
( \ctx ->
890+
ctx . logMessage $
891+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
892+
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
893+
, EnsuresFalse falseEnsures
894+
)
895+
Right _other ->
896+
pure ()
897+
Left SMT.SMTSolverUnknown{} ->
898+
pure ()
899+
Left other ->
900+
liftIO $ Exception.throw other
902901
lift $ pushConstraints $ Set.fromList ensuredConditions
903902
pure $ substituteInTerm subst rule.rhs
904903
where
@@ -1004,19 +1003,19 @@ simplifyConstraint ::
10041003
LoggerMIO io =>
10051004
KoreDefinition ->
10061005
Maybe LLVM.API ->
1007-
Maybe SMT.SMTContext ->
1006+
SMT.SMTContext ->
10081007
SimplifierCache ->
10091008
Set Predicate ->
10101009
Predicate ->
10111010
io (Either EquationFailure Predicate, SimplifierCache)
1012-
simplifyConstraint def mbApi mbSMT cache knownPredicates (Predicate p) = do
1013-
runEquationT def mbApi mbSMT cache knownPredicates $ (coerce <$>) . simplifyConstraint' True $ p
1011+
simplifyConstraint def mbApi smt cache knownPredicates (Predicate p) = do
1012+
runEquationT def mbApi smt cache knownPredicates $ (coerce <$>) . simplifyConstraint' True $ p
10141013

10151014
simplifyConstraints ::
10161015
LoggerMIO io =>
10171016
KoreDefinition ->
10181017
Maybe LLVM.API ->
1019-
Maybe SMT.SMTContext ->
1018+
SMT.SMTContext ->
10201019
SimplifierCache ->
10211020
[Predicate] ->
10221021
io (Either EquationFailure [Predicate], SimplifierCache)

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

Lines changed: 34 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ newtype RewriteT io a = RewriteT
7979
data RewriteConfig = RewriteConfig
8080
{ definition :: KoreDefinition
8181
, llvmApi :: Maybe LLVM.API
82-
, smtSolver :: Maybe SMT.SMTContext
82+
, smtSolver :: SMT.SMTContext
8383
, doTracing :: Flag "CollectRewriteTraces"
8484
, logger :: Logger LogMessage
8585
, prettyModifiers :: ModifiersRep
@@ -102,7 +102,7 @@ runRewriteT ::
102102
Flag "CollectRewriteTraces" ->
103103
KoreDefinition ->
104104
Maybe LLVM.API ->
105-
Maybe SMT.SMTContext ->
105+
SMT.SMTContext ->
106106
SimplifierCache ->
107107
RewriteT io a ->
108108
io (Either (RewriteFailed "Rewrite") (a, SimplifierCache))
@@ -355,7 +355,7 @@ applyRule pat@Pattern{ceilConditions} rule =
355355
stillUnclear <- lift $ filterOutKnownConstraints prior unclearRequires
356356

357357
-- check unclear requires-clauses in the context of known constraints (prior)
358-
mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask
358+
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
359359

360360
let smtUnclear = do
361361
withContext CtxConstraint . withContext CtxAbort . logMessage $
@@ -366,34 +366,23 @@ applyRule pat@Pattern{ceilConditions} rule =
366366
failRewrite $
367367
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
368368
map coerce stillUnclear
369-
case mbSolver of
370-
Just solver -> do
371-
checkAllRequires <-
372-
SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear)
373-
374-
case checkAllRequires of
375-
Left SMT.SMTSolverUnknown{} ->
376-
smtUnclear -- abort rewrite if a solver result was Unknown
377-
Left other ->
378-
liftIO $ Exception.throw other -- fail hard on other SMT errors
379-
Right (Just False) -> do
380-
-- requires is actually false given the prior
381-
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
382-
RewriteRuleAppT $ pure NotApplied
383-
Right (Just True) ->
384-
pure () -- can proceed
385-
Right Nothing ->
386-
smtUnclear -- no implication could be determined
387-
Nothing ->
388-
unless (null stillUnclear) $ do
389-
withContext CtxConstraint . withContext CtxAbort $
390-
logMessage $
391-
WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $
392-
renderOneLineText $
393-
"Uncertain about a condition(s) in rule, no SMT solver:"
394-
<+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear)
395-
failRewrite $
396-
RuleConditionUnclear rule (head stillUnclear)
369+
370+
checkAllRequires <-
371+
SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear)
372+
373+
case checkAllRequires of
374+
Left SMT.SMTSolverUnknown{} ->
375+
smtUnclear -- abort rewrite if a solver result was Unknown
376+
Left other ->
377+
liftIO $ Exception.throw other -- fail hard on other SMT errors
378+
Right (Just False) -> do
379+
-- requires is actually false given the prior
380+
withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
381+
RewriteRuleAppT $ pure NotApplied
382+
Right (Just True) ->
383+
pure () -- can proceed
384+
Right Nothing ->
385+
smtUnclear -- no implication could be determined
397386

398387
-- check ensures constraints (new) from rhs: stop and return `Trivial` if
399388
-- any are false, remove all that are trivially true, return the rest
@@ -405,17 +394,16 @@ applyRule pat@Pattern{ceilConditions} rule =
405394
catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures
406395

407396
-- check all new constraints together with the known side constraints
408-
whenJust mbSolver $ \solver ->
409-
(lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
410-
Right (Just False) -> do
411-
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
412-
RewriteRuleAppT $ pure Trivial
413-
Right _other ->
414-
pure ()
415-
Left SMT.SMTSolverUnknown{} ->
416-
pure ()
417-
Left other ->
418-
liftIO $ Exception.throw other
397+
(lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
398+
Right (Just False) -> do
399+
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
400+
RewriteRuleAppT $ pure Trivial
401+
Right _other ->
402+
pure ()
403+
Left SMT.SMTSolverUnknown{} ->
404+
pure ()
405+
Left other ->
406+
liftIO $ Exception.throw other
419407

420408
-- existential variables may be present in rule.rhs and rule.ensures,
421409
-- need to strip prefixes and freshen their names with respect to variables already
@@ -714,7 +702,7 @@ performRewrite ::
714702
Flag "CollectRewriteTraces" ->
715703
KoreDefinition ->
716704
Maybe LLVM.API ->
717-
Maybe SMT.SMTContext ->
705+
SMT.SMTContext ->
718706
-- | maximum depth
719707
Maybe Natural ->
720708
-- | cut point rule labels
@@ -723,7 +711,7 @@ performRewrite ::
723711
[Text] ->
724712
Pattern ->
725713
io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
726-
performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalLabels pat = do
714+
performRewrite doTracing def mLlvmLibrary smtSolver mbMaxDepth cutLabels terminalLabels pat = do
727715
(rr, RewriteStepsState{counter, traces}) <-
728716
flip runStateT rewriteStart $ doSteps False pat
729717
pure (counter, traces, rr)
@@ -748,7 +736,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
748736
simplifyP p = withContext CtxSimplify $ do
749737
st <- get
750738
let cache = st.simplifierCache
751-
evaluatePattern def mLlvmLibrary mSolver cache p >>= \(res, newCache) -> do
739+
evaluatePattern def mLlvmLibrary smtSolver cache p >>= \(res, newCache) -> do
752740
updateCache newCache
753741
case res of
754742
Right newPattern -> do
@@ -815,7 +803,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
815803
doTracing
816804
def
817805
mLlvmLibrary
818-
mSolver
806+
smtSolver
819807
simplifierCache
820808
(withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
821809
>>= \case

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,9 +81,8 @@ data Response
8181
= Success -- for command_
8282
| Sat
8383
| Unsat
84-
| Unknown
84+
| Unknown (Maybe Text)
8585
| Values [(SExpr, Value)]
86-
| ReasonUnknown Text
8786
| Error BS.ByteString
8887
deriving stock (Eq, Ord, Show)
8988

0 commit comments

Comments
 (0)