Skip to content

4012 evaluate pattern pruning #4020

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

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open

4012 evaluate pattern pruning #4020

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
a313ce8
Derive Show for SMT result types
geo2a Aug 7, 2024
0c0e203
Check consistency of the pattern's constraints before evaluating it
geo2a Aug 7, 2024
5999a66
Check pattern consistency before starting rewriting in `"execute"`
geo2a Aug 5, 2024
2f75bc2
Fix frontend warning in collectiontest.k
geo2a Aug 8, 2024
0de9517
Invert `--no-fallback-simplify` and `--no-post-exec-simplify` (new …
jberthold Aug 1, 2024
41e93b1
Update integration tests
geo2a Aug 7, 2024
2359ddc
Correct typos and test description
geo2a Aug 12, 2024
998eb07
Make Z3 call optional in evaluatePattern
geo2a Aug 20, 2024
598a00c
Fix unit tests
geo2a Aug 20, 2024
9c07a05
Don't check initial constraints when "assume-state-defined"
geo2a Aug 21, 2024
39e6abc
Rename "assume-state-define" to "assume-defined"
geo2a Aug 21, 2024
df4cfae
Return vacuous on undefined concrete terms
geo2a Aug 21, 2024
e155e58
Rename parameter in integration tests
geo2a Aug 21, 2024
586589f
Reorganize tests
geo2a Aug 21, 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
111 changes: 76 additions & 35 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,11 @@ respond stateVar request =
[ req.logSuccessfulRewrites
, req.logFailedRewrites
]
checkConstraintsConsistent =
case req.assumeDefined of
Nothing -> ApplyEquations.CheckConstraintsConsistent
Just False -> ApplyEquations.CheckConstraintsConsistent
Just True -> ApplyEquations.NoCheckConstraintsConsistent
-- apply the given substitution before doing anything else
let substPat =
Pattern
Expand All @@ -147,26 +152,54 @@ respond stateVar request =

solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions

logger <- getLogger
prettyModifiers <- getPrettyModifiers
let rewriteConfig =
RewriteConfig
{ definition = def
, llvmApi = mLlvmLibrary
, smtSolver = solver
, varsToAvoid = substVars
, doTracing
, logger
, prettyModifiers
, mbMaxDepth = mbDepth
, mbSimplify = rewriteOpts.interimSimplification
, cutLabels = cutPoints
, terminalLabels = terminals
}
result <-
performRewrite rewriteConfig substPat
SMT.finaliseSolver solver
pure $ execResponse req result substitution unsupported
-- check input pattern's consistency before starting rewriting
evaluatedInitialPattern <-
ApplyEquations.evaluatePattern
def
mLlvmLibrary
solver
mempty
checkConstraintsConsistent
substPat

let trivialResponse =
execResponse
req
(0, mempty, RewriteTrivial substPat)
substitution
unsupported

case evaluatedInitialPattern of
(Left ApplyEquations.SideConditionFalse{}, _) -> do
-- input pattern's constraints are Bottom, return Vacuous
pure trivialResponse
(Left ApplyEquations.UndefinedTerm{}, _) -> do
-- LLVM has stumbled upon an undefined term, the whole term is Bottom, return Vacuous
pure trivialResponse
(Left other, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
(Right newPattern, simplifierCache) -> do
logger <- getLogger
prettyModifiers <- getPrettyModifiers
let rewriteConfig =
RewriteConfig
{ definition = def
, llvmApi = mLlvmLibrary
, smtSolver = solver
, varsToAvoid = substVars
, doTracing
, logger
, prettyModifiers
, mbMaxDepth = mbDepth
, mbSimplify = rewriteOpts.interimSimplification
, cutLabels = cutPoints
, terminalLabels = terminals
}

result <-
performRewrite rewriteConfig simplifierCache newPattern
SMT.finaliseSolver solver
pure $ execResponse req result substitution unsupported
RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
-- block other request executions while modifying the server state
state <- liftIO $ takeMVar stateVar
Expand Down Expand Up @@ -255,21 +288,29 @@ respond stateVar request =
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
, ceilConditions = pat.ceilConditions
}
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
(Right newPattern, _) -> do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
tSort = externaliseSort (sortOfPattern newPattern)
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
[] -> term
ps -> KoreJson.KJAnd tSort $ term : ps
pure $ Right (addHeader result)
(Left ApplyEquations.SideConditionFalse{}, _) -> do
let tSort = externaliseSort $ sortOfPattern pat
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
(Left (ApplyEquations.EquationLoop _terms), _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
(Left other, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
-- evaluate the pattern, checking the constrains for consistency
ApplyEquations.evaluatePattern
def
mLlvmLibrary
solver
mempty
ApplyEquations.CheckConstraintsConsistent
substPat
>>= \case
(Right newPattern, _) -> do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
tSort = externaliseSort (sortOfPattern newPattern)
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
[] -> term
ps -> KoreJson.KJAnd tSort $ term : ps
pure $ Right (addHeader result)
(Left ApplyEquations.SideConditionFalse{}, _) -> do
let tSort = externaliseSort $ sortOfPattern pat
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
Comment on lines +307 to +309
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

...another place where we should probably catch UndefinedTerm and return KJBottom...

(Left (ApplyEquations.EquationLoop _terms), _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
(Left other, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
-- predicate only
Right (Predicates ps)
| null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported ->
Expand Down
48 changes: 42 additions & 6 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ License : BSD-3-Clause
module Booster.Pattern.ApplyEquations (
evaluateTerm,
evaluatePattern,
pattern CheckConstraintsConsistent,
pattern NoCheckConstraintsConsistent,
Direction (..),
EquationT (..),
runEquationT,
Expand Down Expand Up @@ -70,7 +72,7 @@ import Booster.Pattern.Util
import Booster.Prettyprinter (renderOneLineText)
import Booster.SMT.Interface qualified as SMT
import Booster.Syntax.Json.Externalise (externaliseTerm)
import Booster.Util (Bound (..))
import Booster.Util (Bound (..), Flag (..))
import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
import Kore.Util (showHashHex)

Expand Down Expand Up @@ -443,6 +445,12 @@ evaluateTerm' ::
EquationT io Term
evaluateTerm' direction = iterateEquations direction PreferFunctions

pattern CheckConstraintsConsistent :: Flag "CheckConstraintsConsistent"
pattern CheckConstraintsConsistent = Flag True

pattern NoCheckConstraintsConsistent :: Flag "CheckConstraintsConsistent"
pattern NoCheckConstraintsConsistent = Flag False

{- | Simplify a Pattern, processing its constraints independently.
Returns either the first failure or the new pattern if no failure was encountered
-}
Expand All @@ -452,20 +460,45 @@ evaluatePattern ::
Maybe LLVM.API ->
SMT.SMTContext ->
SimplifierCache ->
Flag "CheckConstraintsConsistent" ->
Pattern ->
io (Either EquationFailure Pattern, SimplifierCache)
evaluatePattern def mLlvmLibrary smtSolver cache pat =
runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
evaluatePattern def mLlvmLibrary smtSolver cache doCheck pat =
runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' doCheck $ pat

-- version for internal nested evaluation
evaluatePattern' ::
LoggerMIO io =>
Flag "CheckConstraintsConsistent" ->
Pattern ->
EquationT io Pattern
evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
evaluatePattern' doCheck pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
when (coerce doCheck) $ do
solver <- (.smtSolver) <$> getConfig
-- check the pattern's constraints for satisfiability to ensure they are consistent
consistent <-
withContext CtxConstraint $ do
withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure ()
consistent <- SMT.isSat solver (Set.toList constraints)
logMessage $
"Constraints consistency check returns: " <> show consistent
pure consistent
case consistent of
SMT.IsUnsat -> do
-- the constraints are unsatisfiable, which means that the patten is Bottom
throw . SideConditionFalse . collapseAndBools $ constraints
SMT.IsUnknown{} -> do
-- unlikely case of an Unknown response to a consistency check.
-- continue to preserve the old behaviour.
withContext CtxConstraint . logWarn . Text.pack $
"Constraints consistency UNKNOWN: " <> show consistent
pure ()
SMT.IsSat{} ->
-- constraints are consistent, continue
pure ()

newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
-- after evaluating the term, evaluate all (existing and
-- newly-acquired) constraints, once
-- after evaluating the term, evaluate all (existing and newly-acquired) constraints, once
traverse_ simplifyAssumedPredicate . predicates =<< getState
-- this may yield additional new constraints, left unevaluated
evaluatedConstraints <- predicates <$> getState
Expand All @@ -482,6 +515,9 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
pure partialResult
err -> throw err

collapseAndBools :: Set Predicate -> Predicate
collapseAndBools = coerce . foldAndBool . map coerce . Set.toList

-- evaluate the given predicate assuming all others
simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
simplifyAssumedPredicate p = do
Expand Down
41 changes: 24 additions & 17 deletions booster/library/Booster/Pattern/Implies.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,24 +136,31 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
(externaliseExistTerm existsL substPatL.term)
(externaliseExistTerm existsR substPatR.term)
MatchIndeterminate remainder ->
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case
(Right simplifedSubstPatL, _) ->
if substPatL == simplifedSubstPatL
then -- we are being conservative here for now and returning an error.
-- since we have already simplified the LHS, we may want to eventually return implise, but the condition
-- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
ApplyEquations.evaluatePattern
def
mLlvmLibrary
solver
mempty
ApplyEquations.CheckConstraintsConsistent
substPatL
>>= \case
(Right simplifedSubstPatL, _) ->
if substPatL == simplifedSubstPatL
then -- we are being conservative here for now and returning an error.
-- since we have already simplified the LHS, we may want to eventually return implise, but the condition
-- will contain the remainder as an equality contraint, predicating the implication on that equality being true.

pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
"match remainder: "
<> renderDefault
( hsep $
punctuate comma $
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
NonEmpty.toList remainder
)
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR
(Left err, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
"match remainder: "
<> renderDefault
( hsep $
punctuate comma $
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
NonEmpty.toList remainder
)
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR
(Left err, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
Comment on lines +162 to +163
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should probably also catch UndefinedTerm here... (but for now the endpoint anyway returns errors when it is unsure)

MatchSuccess subst -> do
let filteredConsequentPreds =
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
Expand Down
22 changes: 12 additions & 10 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ import Booster.Pattern.ApplyEquations (
SimplifierCache (..),
evaluatePattern,
simplifyConstraint,
pattern NoCheckConstraintsConsistent,
)
import Booster.Pattern.Base
import Booster.Pattern.Bool
Expand Down Expand Up @@ -715,9 +716,10 @@ performRewrite ::
forall io.
LoggerMIO io =>
RewriteConfig ->
SimplifierCache ->
Pattern ->
io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
performRewrite rewriteConfig pat = do
performRewrite rewriteConfig initialCache pat = do
(rr, RewriteStepsState{counter, traces}) <-
flip runStateT rewriteStart $ doSteps False pat
pure (counter, traces, rr)
Expand All @@ -733,6 +735,14 @@ performRewrite rewriteConfig pat = do
, terminalLabels
} = rewriteConfig

rewriteStart :: RewriteStepsState
rewriteStart =
RewriteStepsState
{ counter = 0
, traces = mempty
, simplifierCache = initialCache
}

logDepth = withContext CtxDepth . logMessage

depthReached n = maybe False (n >=) mbMaxDepth
Expand All @@ -755,7 +765,7 @@ performRewrite rewriteConfig pat = do
simplifyP p = withContext CtxSimplify $ do
st <- get
let cache = st.simplifierCache
evaluatePattern definition llvmApi smtSolver cache p >>= \(res, newCache) -> do
evaluatePattern definition llvmApi smtSolver cache NoCheckConstraintsConsistent p >>= \(res, newCache) -> do
updateCache newCache
case res of
Right newPattern -> do
Expand Down Expand Up @@ -930,11 +940,3 @@ data RewriteStepsState = RewriteStepsState
, traces :: !(Seq (RewriteTrace ()))
, simplifierCache :: SimplifierCache
}

rewriteStart :: RewriteStepsState
rewriteStart =
RewriteStepsState
{ counter = 0
, traces = mempty
, simplifierCache = mempty
}
4 changes: 2 additions & 2 deletions booster/library/Booster/SMT/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ finaliseSolver ctxt = do
pattern IsUnknown :: unknown -> Either unknown b
pattern IsUnknown u = Left u

newtype IsSat' a = IsSat' (Maybe a) deriving (Functor)
newtype IsSat' a = IsSat' (Maybe a) deriving (Functor, Show)

type IsSatResult a = Either Text (IsSat' a)

Expand Down Expand Up @@ -345,7 +345,7 @@ getModelFor ctxt ps subst
mkComment :: Pretty (PrettyWithModifiers '[Decoded] a) => a -> BS.ByteString
mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded]

newtype IsValid' = IsValid' Bool
newtype IsValid' = IsValid' Bool deriving (Show)

type IsValidResult = Either (Maybe Text) IsValid'

Expand Down
2 changes: 1 addition & 1 deletion booster/test/rpc-integration/resources/collectiontest.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ module COLLECTIONTEST
imports LIST
imports MAP

syntax State ::= State(Collection, Int) [klabel(State), symbol]
syntax State ::= State(Collection, Int) [symbol(State)]

syntax Collection ::= Set // | List | Map

Expand Down
Loading
Loading