Skip to content

Commit

Permalink
Preserve clause ordering of requires and ensures when internalisi…
Browse files Browse the repository at this point in the history 
…g rules in booster (#4037)

Fixes #4028

---------

Co-authored-by: github-actions <[email protected]>
  • Loading branch information
@goodlyrottenapple
goodlyrottenapple and github-actions authored Aug 19, 2024
1 parent 2faf6c1 commit f1d156f
Show file tree
Hide file tree
Showing 21 changed files with 34,116 additions and 24,066 deletions.
4 changes: 2 additions & 2 deletions booster/library/Booster/Definition/Base.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ emptyKoreDefinition attributes =

data RewriteRule (tag :: k) = RewriteRule
{ lhs, rhs :: Term
, requires, ensures :: Set Predicate
, requires, ensures :: [Predicate]
, attributes :: AxiomAttributes
, computedAttributes :: ComputedAxiomAttributes
, existentials :: Set Variable
Expand All @@ -86,7 +86,7 @@ data Alias = Alias
{ name :: AliasName
, params :: [Sort]
, args :: [Variable]
, rhs :: Pattern
, rhs :: Term
}
deriving stock (Eq, Ord, Show, GHC.Generic)
deriving anyclass (NFData)
Expand Down
4 changes: 2 additions & 2 deletions booster/library/Booster/Definition/Ceil.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSumm
then []
else
[ "requires"
, Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) $ Set.toList rule.requires
, Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) rule.requires
]
)
<> [ Pretty.line
Expand Down Expand Up @@ -105,7 +105,7 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
ns <- noSolver
(res, _) <- runEquationT def mllvm ns mempty mempty $ do
lhsCeils <- Set.fromList <$> computeCeil lhs
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires
let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList
rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs)

Expand Down
19 changes: 10 additions & 9 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ import Booster.Pattern.Rewrite (
import Booster.Pattern.Util (
freeVariables,
sortOfPattern,
sortOfTerm,
substituteInPredicate,
substituteInTerm,
)
Expand Down Expand Up @@ -116,9 +117,9 @@ respond stateVar request =
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
Right (pat, substitution, unsupported) -> do
Right (term, preds, ceils, substitution, unsupported) -> do
unless (null unsupported) $ do
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfTerm term) unsupported) $
logMessage ("ignoring unsupported predicate parts" :: Text)
let cutPoints = fromMaybe [] req.cutPointRules
terminals = fromMaybe [] req.terminalRules
Expand All @@ -133,9 +134,9 @@ respond stateVar request =
-- apply the given substitution before doing anything else
let substPat =
Pattern
{ term = substituteInTerm substitution pat.term
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
, ceilConditions = pat.ceilConditions
{ term = substituteInTerm substitution term
, constraints = Set.fromList $ map (substituteInPredicate substitution) preds
, ceilConditions = ceils
}
-- remember all variables used in the substitutions
substVars =
Expand Down Expand Up @@ -280,7 +281,7 @@ respond stateVar request =
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
logMessage ("ignoring unsupported predicate parts" :: Text)
-- apply the given substitution before doing anything else
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
withContext CtxConstraint $
ApplyEquations.simplifyConstraints
def
Expand All @@ -295,7 +296,7 @@ respond stateVar request =
sortOfJson req.state.term
result =
map (externalisePredicate predicateSort) newPreds
<> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
<> map (externaliseCeil predicateSort) ps.ceilPredicates
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
<> ps.unsupported

Expand Down Expand Up @@ -350,10 +351,10 @@ respond stateVar request =
( Text.unlines $
map
(renderText . ("#Ceil:" <>) . pretty' @mods)
(Set.toList ps.ceilPredicates)
ps.ceilPredicates
<> map prettyPattern ps.unsupported
)
pure (Set.toList ps.boolPredicates, ps.substitution)
pure (ps.boolPredicates, ps.substitution)

smtResult <-
if null boolPs && Map.null suppliedSubst
Expand Down
5 changes: 2 additions & 3 deletions booster/library/Booster/JsonRpc/Utils.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@ import Booster.Syntax.Json.Internalise
import Data.Binary.Builder (fromLazyByteString, toLazyByteString)
import Data.List (intersperse)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Text.Encoding qualified as Text
import Kore.JsonRpc.Error qualified as RpcError
import Kore.JsonRpc.Types
Expand Down Expand Up @@ -252,11 +251,11 @@ diffBy def pat1 pat2 =
[ "Conditions:"
: fmap
(Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated])
(Set.toList ps.boolPredicates)
ps.boolPredicates
, "Ceil conditions:"
: map
(Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated])
(Set.toList ps.ceilPredicates)
ps.ceilPredicates
, "Substitutions:"
: fmap
(Pretty.indent 4)
Expand Down
2 changes: 1 addition & 1 deletion booster/library/Booster/Pattern/ApplyEquations.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1014,7 +1014,7 @@ applyEquation term rule =
let ensured =
concatMap
(splitBoolPredicates . substituteInPredicate matchingSubst)
(Set.toList rule.ensures)
rule.ensures
ensuredConditions <-
-- throws if an ensured condition found to be false
catMaybes
Expand Down
4 changes: 2 additions & 2 deletions booster/library/Booster/Pattern/Implies.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,8 +204,8 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
(Right IsTop{}, _) ->
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $
"The check implication step expects the antecedent term to be function-like."
( Right (IsPattern (existsL, (patL, substitutionL, unsupportedL)))
, Right (IsPattern (existsR, (patR, substitutionR, unsupportedR)))
( Right (IsPattern (existsL, patL, substitutionL, unsupportedL))
, Right (IsPattern (existsR, patR, substitutionR, unsupportedR))
) ->
checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR
(Right IsPattern{}, Right (IsTop sort)) ->
Expand Down
3 changes: 1 addition & 2 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -461,8 +461,7 @@ applyRule pat@Pattern{ceilConditions} rule =
checkEnsures matchingSubst = do
-- apply substitution to rule requires
let ruleEnsures =
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) $
Set.toList rule.ensures
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
newConstraints <-
catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures

Expand Down
6 changes: 5 additions & 1 deletion booster/library/Booster/Pattern/Util.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module Booster.Pattern.Util (
substituteInPredicate,
modifyVariables,
modifyVariablesInT,
modifyVariablesInP,
modifyVarName,
modifyVarNameConcreteness,
freeVariables,
Expand Down Expand Up @@ -107,7 +108,7 @@ modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern
modifyVariables f p =
Pattern
{ term = modifyVariablesInT f p.term
, constraints = Set.map (coerce $ modifyVariablesInT f) p.constraints
, constraints = Set.map (modifyVariablesInP f) p.constraints
, ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions
}

Expand All @@ -116,6 +117,9 @@ modifyVariablesInT f = cata $ \case
VarF v -> Var (f v)
other -> embed other

modifyVariablesInP :: (Variable -> Variable) -> Predicate -> Predicate
modifyVariablesInP = coerce modifyVariablesInT

modifyVarName :: (VarName -> VarName) -> Variable -> Variable
modifyVarName f v = v{variableName = f v.variableName}

Expand Down
8 changes: 4 additions & 4 deletions booster/library/Booster/SMT/Translate.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -188,12 +188,12 @@ equationToSMTLemma equation
-- if requires empty: just (= (lhs) (rhs))
-- if requires not empty: (=> (requires) (= (lhs) (rhs)))
lemmaRaw <-
if Set.null equation.requires
if null equation.requires
then pure equationRaw
else do
smtPremise <-
foldl1 SMT.and
<$> mapM (translateTerm . \(Predicate t) -> t) (Set.toList equation.requires)
<$> mapM (translateTerm . \(Predicate t) -> t) equation.requires
pure $ SMT.implies smtPremise equationRaw
-- NB ensures has no SMT implications (single shot sat-check)

Expand Down Expand Up @@ -247,13 +247,13 @@ equationToSMTLemma equation
( pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.lhs)
<> " == "
<> pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.rhs)
: if Set.null equation.requires
: if null equation.requires
then []
else
" requires"
: map
((Pretty.indent 4 . pretty) . (PrettyWithModifiers @['Decoded, 'Truncated]))
(Set.toList equation.requires)
equation.requires
)
lemmaComment = BS.pack (Pretty.renderDefault prettyLemma)

Expand Down
55 changes: 39 additions & 16 deletions booster/library/Booster/Syntax/Json/Internalise.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,8 @@ data InternalisedPredicate
deriving stock (Eq, Show)

data InternalisedPredicates = InternalisedPredicates
{ boolPredicates :: Set Internal.Predicate
, ceilPredicates :: Set Internal.Ceil
{ boolPredicates :: [Internal.Predicate]
, ceilPredicates :: [Internal.Ceil]
, substitution :: Map Internal.Variable Internal.Term
, unsupported :: [Syntax.KorePattern]
}
Expand All @@ -117,8 +117,8 @@ data InternalisedPredicates = InternalisedPredicates
instance FromModifiersT mods => Pretty (PrettyWithModifiers mods InternalisedPredicates) where
pretty (PrettyWithModifiers ps) =
Pretty.vsep $
("Bool predicates: " : map (pretty' @mods) (Set.toList ps.boolPredicates))
<> ("Ceil predicates: " : map (pretty' @mods) (Set.toList ps.ceilPredicates))
("Bool predicates: " : map (pretty' @mods) ps.boolPredicates)
<> ("Ceil predicates: " : map (pretty' @mods) ps.ceilPredicates)
<> ( "Substitution: "
: map
(\(v, t) -> pretty' @mods v Pretty.<+> "->" Pretty.<+> pretty' @mods t)
Expand All @@ -145,7 +145,14 @@ internalisePattern ::
Maybe [Syntax.Id] ->
KoreDefinition ->
Syntax.KorePattern ->
Except PatternError (Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
Except
PatternError
( Internal.Term
, [Internal.Predicate]
, [Internal.Ceil]
, Map Internal.Variable Internal.Term
, [Syntax.KorePattern]
)
internalisePattern allowAlias checkSubsorts sortVars definition p = do
(terms, predicates) <- partitionM isTermM $ explodeAnd p

Expand All @@ -157,11 +164,9 @@ internalisePattern allowAlias checkSubsorts sortVars definition p = do
internalPs <-
internalisePredicates allowAlias checkSubsorts sortVars definition predicates
pure
( Internal.Pattern
{ term
, constraints = internalPs.boolPredicates
, ceilConditions = Set.toList internalPs.ceilPredicates
}
( term
, internalPs.boolPredicates
, internalPs.ceilPredicates
, internalPs.substitution
, internalPs.unsupported
)
Expand Down Expand Up @@ -196,7 +201,7 @@ internalisePatternOrTopOrBottom ::
Except
PatternError
( PatternOrTopOrBottom
([Internal.Variable], (Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern]))
([Internal.Variable], Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
)
internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition existentials p = do
let exploded = explodeAnd p
Expand All @@ -210,7 +215,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
variableSort <- lookupInternalSort sortVars definition.sorts p sort
let variableName = textToBS var.getId
pure $ Internal.Variable{variableSort, variableName}
IsPattern . (existentialVars,) <$> internalisePattern allowAlias checkSubsorts sortVars definition p
(term, preds, ceilConditions, subst, unknown) <-
internalisePattern allowAlias checkSubsorts sortVars definition p
pure $
IsPattern
( existentialVars
, Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions}
, subst
, unknown
)
where
isTop = \case
[Syntax.KJTop{sort}] -> Just $ IsTop sort
Expand All @@ -234,9 +247,13 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa
internalisePredicates allowAlias checkSubsorts sortVars definition [syntaxPatt]
)
<|> ( withExcept (: []) $ do
(pat, substitution, unsupported) <-
(term, constrs, ceilConditions, substitution, unsupported) <-
internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt
pure $ TermAndPredicates pat substitution unsupported
pure $
TermAndPredicates
Internal.Pattern{term, constraints = Set.fromList constrs, ceilConditions}
substitution
unsupported
)

lookupInternalSort ::
Expand Down Expand Up @@ -412,8 +429,8 @@ internalisePredicates allowAlias checkSubsorts sortVars definition ps = do

pure
InternalisedPredicates
{ boolPredicates = Set.fromList $ [p | BoolPred p <- internalised] <> moreEquations
, ceilPredicates = Set.fromList $ [p | CeilPred p <- internalised]
{ boolPredicates = [p | BoolPred p <- internalised] <> moreEquations
, ceilPredicates = [p | CeilPred p <- internalised]
, substitution
, unsupported = [p | UnsupportedPred p <- internalised]
}
Expand Down Expand Up @@ -682,6 +699,8 @@ data PatternError
| UnknownSymbol Syntax.Id Syntax.KorePattern
| MacroOrAliasSymbolNotAllowed Syntax.Id Syntax.KorePattern
| SubstitutionNotAllowed
| PredicateNotAllowed
| CeilNotAllowed
| IncorrectSymbolArity Syntax.KorePattern Syntax.Id Int Int
deriving stock (Eq, Show)

Expand Down Expand Up @@ -715,6 +734,8 @@ patternErrorToRpcError = \case
MacroOrAliasSymbolNotAllowed sym p ->
wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p
SubstitutionNotAllowed -> RpcError.ErrorOnly "Substitution predicates are not allowed here"
PredicateNotAllowed -> RpcError.ErrorOnly "Predicates are not allowed here"
CeilNotAllowed -> RpcError.ErrorOnly "Ceil predicates are not allowed here"
IncorrectSymbolArity p s expected got ->
wrap
( "Inconsistent pattern. Symbol '"
Expand All @@ -740,6 +761,8 @@ logPatternError = \case
UnknownSymbol sym p -> withKorePatternContext p $ logMessage $ "Unknown symbol '" <> Syntax.getId sym <> "'"
MacroOrAliasSymbolNotAllowed sym p -> withKorePatternContext p $ logMessage $ "Symbol '" <> Syntax.getId sym <> "' is a macro/alias"
SubstitutionNotAllowed -> logMessage ("Substitution predicates are not allowed here" :: Text)
PredicateNotAllowed -> logMessage ("Predicates are not allowed here" :: Text)
CeilNotAllowed -> logMessage ("Ceil predicates are not allowed here" :: Text)
IncorrectSymbolArity p s expected got ->
withKorePatternContext p $
logMessage $
Expand Down
Loading

0 comments on commit f1d156f

Please sign in to comment.