Skip to content

Commit

Permalink
Make Z3 call optional in evaluatePattern
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a committed Aug 21, 2024
1 parent 2359ddc commit 998eb07
Show file tree
Hide file tree
Showing 4 changed files with 87 additions and 59 deletions.
39 changes: 24 additions & 15 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,7 @@ respond stateVar request =
mLlvmLibrary
solver
mempty
ApplyEquations.CheckConstraintsConsistent
substPat

case evaluatedInitialPattern of
Expand Down Expand Up @@ -277,21 +278,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)
(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
63 changes: 37 additions & 26 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
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,39 +460,42 @@ 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, constraints, ceilConditions} = withPatternContext pat $ 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 ()
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
Expand Down
41 changes: 24 additions & 17 deletions booster/library/Booster/Pattern/Implies.hs
View file
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)
MatchSuccess subst -> do
let filteredConsequentPreds =
Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
Expand Down
3 changes: 2 additions & 1 deletion booster/library/Booster/Pattern/Rewrite.hs
View file
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 @@ -764,7 +765,7 @@ performRewrite rewriteConfig initialCache 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

0 comments on commit 998eb07

Please sign in to comment.