Skip to content

Commit d4ceaae

Browse files
jbertholdjberthold
committed
Merge remote-tracking branch 'origin/master' into EXPERIMENT-booster-interim-simplification
2 parents dbabf23 + e5a921f commit d4ceaae

File tree

77 files changed

+98658
-604
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

77 files changed

+98658
-604
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: 21 additions & 17 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)
@@ -61,6 +60,7 @@ import Booster.Pattern.Rewrite (
6160
performRewrite,
6261
)
6362
import Booster.Pattern.Util (
63+
freeVariables,
6464
sortOfPattern,
6565
substituteInPredicate,
6666
substituteInTerm,
@@ -145,11 +145,17 @@ respond stateVar request =
145145
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
146146
, ceilConditions = pat.ceilConditions
147147
}
148-
149-
solver <- traverse (SMT.initSolver def) mSMTOptions
148+
-- remember all variables used in the substitutions
149+
substVars =
150+
Set.unions
151+
[ Set.singleton v <> freeVariables e
152+
| (v, e) <- Map.assocs substitution
153+
]
154+
155+
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
150156
result <-
151-
performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals rewriteOpts.interimSimplification substPat
152-
whenJust solver SMT.finaliseSolver
157+
performRewrite doTracing def mLlvmLibrary solver substVars mbDepth cutPoints terminals rewriteOpts.interimSimplification substPat
158+
SMT.finaliseSolver solver
153159
stop <- liftIO $ getTime Monotonic
154160
let duration =
155161
if fromMaybe False req.logTiming
@@ -229,7 +235,7 @@ respond stateVar request =
229235
| otherwise =
230236
Nothing
231237

232-
solver <- traverse (SMT.initSolver def) mSMTOptions
238+
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
233239

234240
result <- case internalised of
235241
Left patternErrors -> do
@@ -300,7 +306,7 @@ respond stateVar request =
300306
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
301307
(Left something, _) ->
302308
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something
303-
whenJust solver SMT.finaliseSolver
309+
SMT.finaliseSolver solver
304310
stop <- liftIO $ getTime Monotonic
305311

306312
let duration =
@@ -363,7 +369,7 @@ respond stateVar request =
363369
withContext CtxGetModel $
364370
withContext CtxSMT $
365371
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
366-
pure $ Left SMT.Unknown
372+
pure $ Left $ SMT.Unknown $ Just "No predicates or substitutions given"
367373
else do
368374
solver <- SMT.initSolver def smtOptions
369375
result <- SMT.getModelFor solver boolPs suppliedSubst
@@ -381,12 +387,7 @@ respond stateVar request =
381387
{ satisfiable = RpcTypes.Unsat
382388
, substitution = Nothing
383389
}
384-
Left SMT.ReasonUnknown{} ->
385-
RpcTypes.GetModelResult
386-
{ satisfiable = RpcTypes.Unknown
387-
, substitution = Nothing
388-
}
389-
Left SMT.Unknown ->
390+
Left SMT.Unknown{} ->
390391
RpcTypes.GetModelResult
391392
{ satisfiable = RpcTypes.Unknown
392393
, substitution = Nothing
@@ -486,7 +487,7 @@ respond stateVar request =
486487
MatchSuccess subst -> do
487488
let filteredConsequentPreds =
488489
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
489-
solver <- traverse (SMT.initSolver def) mSMTOptions
490+
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
490491

491492
if null filteredConsequentPreds
492493
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
@@ -495,7 +496,7 @@ respond stateVar request =
495496
(Right newPreds, _) ->
496497
if all (== Pattern.Predicate TrueBool) newPreds
497498
then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
498-
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
499+
else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
499500
(Left other, _) ->
500501
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
501502

@@ -556,7 +557,10 @@ handleSmtError = JsonRpcHandler $ \case
556557
let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
557558
externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
558559
allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
559-
pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds
560+
pure $
561+
RpcError.backendError $
562+
RpcError.SmtSolverError $
563+
RpcError.ErrorWithTerm (fromMaybe "UNKNOWN" reason) allPreds
560564
where
561565
runtimeError prefix err = do
562566
let msg = "SMT " <> prefix <> ": " <> err

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

Lines changed: 47 additions & 38 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 ->
@@ -331,15 +331,14 @@ iterateEquations direction preference startTerm = do
331331
config <- getConfig
332332
currentCount <- countSteps
333333
when (coerce currentCount > config.maxIterations) $ do
334-
withContext CtxAbort $ do
335-
logWarn $
336-
renderOneLineText $
337-
"Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
338-
withContext CtxDetail $
339-
getPrettyModifiers >>= \case
340-
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
341-
logMessage . renderOneLineText $
342-
"Final term:" <+> pretty' @mods currentTerm
334+
logWarn $
335+
renderOneLineText $
336+
"Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
337+
withContext CtxDetail $
338+
getPrettyModifiers >>= \case
339+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
340+
logMessage . renderOneLineText $
341+
"Final term:" <+> pretty' @mods currentTerm
343342
throw $
344343
TooManyIterations currentCount startTerm currentTerm
345344
pushTerm currentTerm
@@ -395,7 +394,7 @@ evaluateTerm ::
395394
Direction ->
396395
KoreDefinition ->
397396
Maybe LLVM.API ->
398-
Maybe SMT.SMTContext ->
397+
SMT.SMTContext ->
399398
Set Predicate ->
400399
Term ->
401400
io (Either EquationFailure Term, SimplifierCache)
@@ -418,7 +417,7 @@ evaluatePattern ::
418417
LoggerMIO io =>
419418
KoreDefinition ->
420419
Maybe LLVM.API ->
421-
Maybe SMT.SMTContext ->
420+
SMT.SMTContext ->
422421
SimplifierCache ->
423422
Pattern ->
424423
io (Either EquationFailure Pattern, SimplifierCache)
@@ -431,13 +430,24 @@ evaluatePattern' ::
431430
Pattern ->
432431
EquationT io Pattern
433432
evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
434-
newTerm <- withTermContext term $ evaluateTerm' BottomUp term
433+
newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
435434
-- after evaluating the term, evaluate all (existing and
436435
-- newly-acquired) constraints, once
437436
traverse_ simplifyAssumedPredicate . predicates =<< getState
438437
-- this may yield additional new constraints, left unevaluated
439438
evaluatedConstraints <- predicates <$> getState
440439
pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
440+
where
441+
-- when TooManyIterations exception occurred while evaluating the top-level term,
442+
-- i.e. not in a recursive evaluation of a side-condition,
443+
-- it is safe to keep the partial result and ignore the exception.
444+
-- Otherwise we would be throwing away useful work.
445+
-- The exceptions thrown in recursion is caught in applyEquation.checkConstraint
446+
keepTopLevelResults :: LoggerMIO io => EquationFailure -> EquationT io Term
447+
keepTopLevelResults = \case
448+
TooManyIterations _ _ partialResult ->
449+
pure partialResult
450+
err -> throw err
441451

442452
-- evaluate the given predicate assuming all others
443453
simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
@@ -452,7 +462,7 @@ evaluateConstraints ::
452462
LoggerMIO io =>
453463
KoreDefinition ->
454464
Maybe LLVM.API ->
455-
Maybe SMT.SMTContext ->
465+
SMT.SMTContext ->
456466
SimplifierCache ->
457467
Set Predicate ->
458468
io (Either EquationFailure (Set Predicate), SimplifierCache)
@@ -818,7 +828,7 @@ applyEquation term rule =
818828
-- could now be syntactically present in the path constraints, filter again
819829
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
820830

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

823833
-- check any conditions that are still unclear with the SMT solver
824834
-- (or abort if no solver is being used), abort if still unclear after
@@ -832,7 +842,7 @@ applyEquation term rule =
832842
liftIO $ Exception.throw other
833843
Right result ->
834844
pure result
835-
in maybe (pure Nothing) (lift . checkWithSmt) mbSolver >>= \case
845+
in lift (checkWithSmt solver) >>= \case
836846
Nothing -> do
837847
-- no solver or still unclear: abort
838848
throwE
@@ -872,23 +882,22 @@ applyEquation term rule =
872882
)
873883
ensured
874884
-- check all ensured conditions together with the path condition
875-
whenJust mbSolver $ \solver -> do
876-
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
877-
Right (Just False) -> do
878-
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
879-
throwE
880-
( \ctx ->
881-
ctx . logMessage $
882-
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
883-
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
884-
, EnsuresFalse falseEnsures
885-
)
886-
Right _other ->
887-
pure ()
888-
Left SMT.SMTSolverUnknown{} ->
889-
pure ()
890-
Left other ->
891-
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
892901
lift $ pushConstraints $ Set.fromList ensuredConditions
893902
pure $ substituteInTerm subst rule.rhs
894903
where
@@ -994,19 +1003,19 @@ simplifyConstraint ::
9941003
LoggerMIO io =>
9951004
KoreDefinition ->
9961005
Maybe LLVM.API ->
997-
Maybe SMT.SMTContext ->
1006+
SMT.SMTContext ->
9981007
SimplifierCache ->
9991008
Set Predicate ->
10001009
Predicate ->
10011010
io (Either EquationFailure Predicate, SimplifierCache)
1002-
simplifyConstraint def mbApi mbSMT cache knownPredicates (Predicate p) = do
1003-
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
10041013

10051014
simplifyConstraints ::
10061015
LoggerMIO io =>
10071016
KoreDefinition ->
10081017
Maybe LLVM.API ->
1009-
Maybe SMT.SMTContext ->
1018+
SMT.SMTContext ->
10101019
SimplifierCache ->
10111020
[Predicate] ->
10121021
io (Either EquationFailure [Predicate], SimplifierCache)

0 commit comments

Comments
 (0)