Skip to content

Commit 72d4801

Browse files
geo2ageo2a
committed
Make Z3 call optional in evaluatePattern
1 parent afaa394 commit 72d4801

File tree

4 files changed

+87
-59
lines changed

4 files changed

+87
-59
lines changed

‎booster/library/Booster/JsonRpc.hs

+24-15
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,7 @@ respond stateVar request =
154154
mLlvmLibrary
155155
solver
156156
mempty
157+
ApplyEquations.CheckConstraintsConsistent
157158
substPat
158159

159160
case evaluatedInitialPattern of
@@ -277,21 +278,29 @@ respond stateVar request =
277278
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
278279
, ceilConditions = pat.ceilConditions
279280
}
280-
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
281-
(Right newPattern, _) -> do
282-
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
283-
tSort = externaliseSort (sortOfPattern newPattern)
284-
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
285-
[] -> term
286-
ps -> KoreJson.KJAnd tSort $ term : ps
287-
pure $ Right (addHeader result)
288-
(Left ApplyEquations.SideConditionFalse{}, _) -> do
289-
let tSort = externaliseSort $ sortOfPattern pat
290-
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
291-
(Left (ApplyEquations.EquationLoop _terms), _) ->
292-
pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
293-
(Left other, _) ->
294-
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
281+
-- evaluate the pattern, checking the constrains for consistency
282+
ApplyEquations.evaluatePattern
283+
def
284+
mLlvmLibrary
285+
solver
286+
mempty
287+
ApplyEquations.CheckConstraintsConsistent
288+
substPat
289+
>>= \case
290+
(Right newPattern, _) -> do
291+
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
292+
tSort = externaliseSort (sortOfPattern newPattern)
293+
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
294+
[] -> term
295+
ps -> KoreJson.KJAnd tSort $ term : ps
296+
pure $ Right (addHeader result)
297+
(Left ApplyEquations.SideConditionFalse{}, _) -> do
298+
let tSort = externaliseSort $ sortOfPattern pat
299+
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
300+
(Left (ApplyEquations.EquationLoop _terms), _) ->
301+
pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
302+
(Left other, _) ->
303+
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
295304
-- predicate only
296305
Right (Predicates ps)
297306
| null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported ->

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

+37-26
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ License : BSD-3-Clause
1010
module Booster.Pattern.ApplyEquations (
1111
evaluateTerm,
1212
evaluatePattern,
13+
pattern CheckConstraintsConsistent,
14+
pattern NoCheckConstraintsConsistent,
1315
Direction (..),
1416
EquationT (..),
1517
runEquationT,
@@ -70,7 +72,7 @@ import Booster.Pattern.Util
7072
import Booster.Prettyprinter (renderOneLineText)
7173
import Booster.SMT.Interface qualified as SMT
7274
import Booster.Syntax.Json.Externalise (externaliseTerm)
73-
import Booster.Util (Bound (..))
75+
import Booster.Util (Bound (..), Flag (..))
7476
import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
7577
import Kore.Util (showHashHex)
7678

@@ -443,6 +445,12 @@ evaluateTerm' ::
443445
EquationT io Term
444446
evaluateTerm' direction = iterateEquations direction PreferFunctions
445447

448+
pattern CheckConstraintsConsistent :: Flag "CheckConstraintsConsistent"
449+
pattern CheckConstraintsConsistent = Flag True
450+
451+
pattern NoCheckConstraintsConsistent :: Flag "CheckConstraintsConsistent"
452+
pattern NoCheckConstraintsConsistent = Flag False
453+
446454
{- | Simplify a Pattern, processing its constraints independently.
447455
Returns either the first failure or the new pattern if no failure was encountered
448456
-}
@@ -452,39 +460,42 @@ evaluatePattern ::
452460
Maybe LLVM.API ->
453461
SMT.SMTContext ->
454462
SimplifierCache ->
463+
Flag "CheckConstraintsConsistent" ->
455464
Pattern ->
456465
io (Either EquationFailure Pattern, SimplifierCache)
457-
evaluatePattern def mLlvmLibrary smtSolver cache pat =
458-
runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
466+
evaluatePattern def mLlvmLibrary smtSolver cache doCheck pat =
467+
runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' doCheck $ pat
459468

460469
-- version for internal nested evaluation
461470
evaluatePattern' ::
462471
LoggerMIO io =>
472+
Flag "CheckConstraintsConsistent" ->
463473
Pattern ->
464474
EquationT io Pattern
465-
evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
466-
solver <- (.smtSolver) <$> getConfig
467-
-- check the pattern's constraints for satisfiability to ensure they are consistent
468-
consistent <-
469-
withContext CtxConstraint $ do
470-
withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure ()
471-
consistent <- SMT.isSat solver (Set.toList constraints)
472-
logMessage $
473-
"Constraints consistency check returns: " <> show consistent
474-
pure consistent
475-
case consistent of
476-
SMT.IsUnsat -> do
477-
-- the constraints are unsatisfiable, which means that the patten is Bottom
478-
throw . SideConditionFalse . collapseAndBools $ constraints
479-
SMT.IsUnknown{} -> do
480-
-- unlikely case of an Unknown response to a consistency check.
481-
-- continue to preserve the old behaviour.
482-
withContext CtxConstraint . logWarn . Text.pack $
483-
"Constraints consistency UNKNOWN: " <> show consistent
484-
pure ()
485-
SMT.IsSat{} ->
486-
-- constraints are consistent, continue
487-
pure ()
475+
evaluatePattern' doCheck pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
476+
when (coerce doCheck) $ do
477+
solver <- (.smtSolver) <$> getConfig
478+
-- check the pattern's constraints for satisfiability to ensure they are consistent
479+
consistent <-
480+
withContext CtxConstraint $ do
481+
withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure ()
482+
consistent <- SMT.isSat solver (Set.toList constraints)
483+
logMessage $
484+
"Constraints consistency check returns: " <> show consistent
485+
pure consistent
486+
case consistent of
487+
SMT.IsUnsat -> do
488+
-- the constraints are unsatisfiable, which means that the patten is Bottom
489+
throw . SideConditionFalse . collapseAndBools $ constraints
490+
SMT.IsUnknown{} -> do
491+
-- unlikely case of an Unknown response to a consistency check.
492+
-- continue to preserve the old behaviour.
493+
withContext CtxConstraint . logWarn . Text.pack $
494+
"Constraints consistency UNKNOWN: " <> show consistent
495+
pure ()
496+
SMT.IsSat{} ->
497+
-- constraints are consistent, continue
498+
pure ()
488499

489500
newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
490501
-- after evaluating the term, evaluate all (existing and newly-acquired) constraints, once

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

+24-17
Original file line numberDiff line numberDiff line change
@@ -136,24 +136,31 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
136136
(externaliseExistTerm existsL substPatL.term)
137137
(externaliseExistTerm existsR substPatR.term)
138138
MatchIndeterminate remainder ->
139-
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case
140-
(Right simplifedSubstPatL, _) ->
141-
if substPatL == simplifedSubstPatL
142-
then -- we are being conservative here for now and returning an error.
143-
-- since we have already simplified the LHS, we may want to eventually return implise, but the condition
144-
-- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
139+
ApplyEquations.evaluatePattern
140+
def
141+
mLlvmLibrary
142+
solver
143+
mempty
144+
ApplyEquations.CheckConstraintsConsistent
145+
substPatL
146+
>>= \case
147+
(Right simplifedSubstPatL, _) ->
148+
if substPatL == simplifedSubstPatL
149+
then -- we are being conservative here for now and returning an error.
150+
-- since we have already simplified the LHS, we may want to eventually return implise, but the condition
151+
-- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
145152

146-
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
147-
"match remainder: "
148-
<> renderDefault
149-
( hsep $
150-
punctuate comma $
151-
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
152-
NonEmpty.toList remainder
153-
)
154-
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR
155-
(Left err, _) ->
156-
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
153+
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
154+
"match remainder: "
155+
<> renderDefault
156+
( hsep $
157+
punctuate comma $
158+
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
159+
NonEmpty.toList remainder
160+
)
161+
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR
162+
(Left err, _) ->
163+
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
157164
MatchSuccess subst -> do
158165
let filteredConsequentPreds =
159166
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints

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

+2-1
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ import Booster.Pattern.ApplyEquations (
5454
SimplifierCache (..),
5555
evaluatePattern,
5656
simplifyConstraint,
57+
pattern NoCheckConstraintsConsistent,
5758
)
5859
import Booster.Pattern.Base
5960
import Booster.Pattern.Bool
@@ -764,7 +765,7 @@ performRewrite rewriteConfig initialCache pat = do
764765
simplifyP p = withContext CtxSimplify $ do
765766
st <- get
766767
let cache = st.simplifierCache
767-
evaluatePattern definition llvmApi smtSolver cache p >>= \(res, newCache) -> do
768+
evaluatePattern definition llvmApi smtSolver cache NoCheckConstraintsConsistent p >>= \(res, newCache) -> do
768769
updateCache newCache
769770
case res of
770771
Right newPattern -> do

0 commit comments

Comments
 (0)