Skip to content

Commit f1d156f

Browse files
goodlyrottenapplegithub-actions
goodlyrottenapple
and
github-actions
authored
Preserve clause ordering of requires and ensures when internalisig rules in booster (#4037)
Fixes #4028 --------- Co-authored-by: github-actions <[email protected]>
1 parent 2faf6c1 commit f1d156f

File tree

21 files changed

+34116
-24066
lines changed

21 files changed

+34116
-24066
lines changed

‎booster/library/Booster/Definition/Base.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ emptyKoreDefinition attributes =
7272

7373
data RewriteRule (tag :: k) = RewriteRule
7474
{ lhs, rhs :: Term
75-
, requires, ensures :: Set Predicate
75+
, requires, ensures :: [Predicate]
7676
, attributes :: AxiomAttributes
7777
, computedAttributes :: ComputedAxiomAttributes
7878
, existentials :: Set Variable
@@ -86,7 +86,7 @@ data Alias = Alias
8686
{ name :: AliasName
8787
, params :: [Sort]
8888
, args :: [Variable]
89-
, rhs :: Pattern
89+
, rhs :: Term
9090
}
9191
deriving stock (Eq, Ord, Show, GHC.Generic)
9292
deriving anyclass (NFData)

‎booster/library/Booster/Definition/Ceil.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSumm
5858
then []
5959
else
6060
[ "requires"
61-
, Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) $ Set.toList rule.requires
61+
, Pretty.indent 2 . Pretty.vsep $ map (pretty' @mods) rule.requires
6262
]
6363
)
6464
<> [ Pretty.line
@@ -105,7 +105,7 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
105105
ns <- noSolver
106106
(res, _) <- runEquationT def mllvm ns mempty mempty $ do
107107
lhsCeils <- Set.fromList <$> computeCeil lhs
108-
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
108+
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires
109109
let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList
110110
rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs)
111111

‎booster/library/Booster/JsonRpc.hs

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ import Booster.Pattern.Rewrite (
5858
import Booster.Pattern.Util (
5959
freeVariables,
6060
sortOfPattern,
61+
sortOfTerm,
6162
substituteInPredicate,
6263
substituteInTerm,
6364
)
@@ -116,9 +117,9 @@ respond stateVar request =
116117
RpcError.CouldNotVerifyPattern
117118
[ patternErrorToRpcError patternError
118119
]
119-
Right (pat, substitution, unsupported) -> do
120+
Right (term, preds, ceils, substitution, unsupported) -> do
120121
unless (null unsupported) $ do
121-
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
122+
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfTerm term) unsupported) $
122123
logMessage ("ignoring unsupported predicate parts" :: Text)
123124
let cutPoints = fromMaybe [] req.cutPointRules
124125
terminals = fromMaybe [] req.terminalRules
@@ -133,9 +134,9 @@ respond stateVar request =
133134
-- apply the given substitution before doing anything else
134135
let substPat =
135136
Pattern
136-
{ term = substituteInTerm substitution pat.term
137-
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
138-
, ceilConditions = pat.ceilConditions
137+
{ term = substituteInTerm substitution term
138+
, constraints = Set.fromList $ map (substituteInPredicate substitution) preds
139+
, ceilConditions = ceils
139140
}
140141
-- remember all variables used in the substitutions
141142
substVars =
@@ -280,7 +281,7 @@ respond stateVar request =
280281
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
281282
logMessage ("ignoring unsupported predicate parts" :: Text)
282283
-- apply the given substitution before doing anything else
283-
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
284+
let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
284285
withContext CtxConstraint $
285286
ApplyEquations.simplifyConstraints
286287
def
@@ -295,7 +296,7 @@ respond stateVar request =
295296
sortOfJson req.state.term
296297
result =
297298
map (externalisePredicate predicateSort) newPreds
298-
<> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
299+
<> map (externaliseCeil predicateSort) ps.ceilPredicates
299300
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
300301
<> ps.unsupported
301302

@@ -350,10 +351,10 @@ respond stateVar request =
350351
( Text.unlines $
351352
map
352353
(renderText . ("#Ceil:" <>) . pretty' @mods)
353-
(Set.toList ps.ceilPredicates)
354+
ps.ceilPredicates
354355
<> map prettyPattern ps.unsupported
355356
)
356-
pure (Set.toList ps.boolPredicates, ps.substitution)
357+
pure (ps.boolPredicates, ps.substitution)
357358

358359
smtResult <-
359360
if null boolPs && Map.null suppliedSubst

‎booster/library/Booster/JsonRpc/Utils.hs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,6 @@ import Booster.Syntax.Json.Internalise
3939
import Data.Binary.Builder (fromLazyByteString, toLazyByteString)
4040
import Data.List (intersperse)
4141
import Data.Map qualified as Map
42-
import Data.Set qualified as Set
4342
import Data.Text.Encoding qualified as Text
4443
import Kore.JsonRpc.Error qualified as RpcError
4544
import Kore.JsonRpc.Types
@@ -252,11 +251,11 @@ diffBy def pat1 pat2 =
252251
[ "Conditions:"
253252
: fmap
254253
(Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated])
255-
(Set.toList ps.boolPredicates)
254+
ps.boolPredicates
256255
, "Ceil conditions:"
257256
: map
258257
(Pretty.indent 4 . pretty . PrettyWithModifiers @['Decoded, 'Truncated])
259-
(Set.toList ps.ceilPredicates)
258+
ps.ceilPredicates
260259
, "Substitutions:"
261260
: fmap
262261
(Pretty.indent 4)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1014,7 +1014,7 @@ applyEquation term rule =
10141014
let ensured =
10151015
concatMap
10161016
(splitBoolPredicates . substituteInPredicate matchingSubst)
1017-
(Set.toList rule.ensures)
1017+
rule.ensures
10181018
ensuredConditions <-
10191019
-- throws if an ensured condition found to be false
10201020
catMaybes

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -204,8 +204,8 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
204204
(Right IsTop{}, _) ->
205205
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $
206206
"The check implication step expects the antecedent term to be function-like."
207-
( Right (IsPattern (existsL, (patL, substitutionL, unsupportedL)))
208-
, Right (IsPattern (existsR, (patR, substitutionR, unsupportedR)))
207+
( Right (IsPattern (existsL, patL, substitutionL, unsupportedL))
208+
, Right (IsPattern (existsR, patR, substitutionR, unsupportedR))
209209
) ->
210210
checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR
211211
(Right IsPattern{}, Right (IsTop sort)) ->

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -461,8 +461,7 @@ applyRule pat@Pattern{ceilConditions} rule =
461461
checkEnsures matchingSubst = do
462462
-- apply substitution to rule requires
463463
let ruleEnsures =
464-
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) $
465-
Set.toList rule.ensures
464+
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
466465
newConstraints <-
467466
catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures
468467

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ module Booster.Pattern.Util (
1010
substituteInPredicate,
1111
modifyVariables,
1212
modifyVariablesInT,
13+
modifyVariablesInP,
1314
modifyVarName,
1415
modifyVarNameConcreteness,
1516
freeVariables,
@@ -107,7 +108,7 @@ modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern
107108
modifyVariables f p =
108109
Pattern
109110
{ term = modifyVariablesInT f p.term
110-
, constraints = Set.map (coerce $ modifyVariablesInT f) p.constraints
111+
, constraints = Set.map (modifyVariablesInP f) p.constraints
111112
, ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions
112113
}
113114

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

120+
modifyVariablesInP :: (Variable -> Variable) -> Predicate -> Predicate
121+
modifyVariablesInP = coerce modifyVariablesInT
122+
119123
modifyVarName :: (VarName -> VarName) -> Variable -> Variable
120124
modifyVarName f v = v{variableName = f v.variableName}
121125

‎booster/library/Booster/SMT/Translate.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -188,12 +188,12 @@ equationToSMTLemma equation
188188
-- if requires empty: just (= (lhs) (rhs))
189189
-- if requires not empty: (=> (requires) (= (lhs) (rhs)))
190190
lemmaRaw <-
191-
if Set.null equation.requires
191+
if null equation.requires
192192
then pure equationRaw
193193
else do
194194
smtPremise <-
195195
foldl1 SMT.and
196-
<$> mapM (translateTerm . \(Predicate t) -> t) (Set.toList equation.requires)
196+
<$> mapM (translateTerm . \(Predicate t) -> t) equation.requires
197197
pure $ SMT.implies smtPremise equationRaw
198198
-- NB ensures has no SMT implications (single shot sat-check)
199199

@@ -247,13 +247,13 @@ equationToSMTLemma equation
247247
( pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.lhs)
248248
<> " == "
249249
<> pretty (PrettyWithModifiers @['Decoded, 'Truncated] equation.rhs)
250-
: if Set.null equation.requires
250+
: if null equation.requires
251251
then []
252252
else
253253
" requires"
254254
: map
255255
((Pretty.indent 4 . pretty) . (PrettyWithModifiers @['Decoded, 'Truncated]))
256-
(Set.toList equation.requires)
256+
equation.requires
257257
)
258258
lemmaComment = BS.pack (Pretty.renderDefault prettyLemma)
259259

‎booster/library/Booster/Syntax/Json/Internalise.hs

Lines changed: 39 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -107,8 +107,8 @@ data InternalisedPredicate
107107
deriving stock (Eq, Show)
108108

109109
data InternalisedPredicates = InternalisedPredicates
110-
{ boolPredicates :: Set Internal.Predicate
111-
, ceilPredicates :: Set Internal.Ceil
110+
{ boolPredicates :: [Internal.Predicate]
111+
, ceilPredicates :: [Internal.Ceil]
112112
, substitution :: Map Internal.Variable Internal.Term
113113
, unsupported :: [Syntax.KorePattern]
114114
}
@@ -117,8 +117,8 @@ data InternalisedPredicates = InternalisedPredicates
117117
instance FromModifiersT mods => Pretty (PrettyWithModifiers mods InternalisedPredicates) where
118118
pretty (PrettyWithModifiers ps) =
119119
Pretty.vsep $
120-
("Bool predicates: " : map (pretty' @mods) (Set.toList ps.boolPredicates))
121-
<> ("Ceil predicates: " : map (pretty' @mods) (Set.toList ps.ceilPredicates))
120+
("Bool predicates: " : map (pretty' @mods) ps.boolPredicates)
121+
<> ("Ceil predicates: " : map (pretty' @mods) ps.ceilPredicates)
122122
<> ( "Substitution: "
123123
: map
124124
(\(v, t) -> pretty' @mods v Pretty.<+> "->" Pretty.<+> pretty' @mods t)
@@ -145,7 +145,14 @@ internalisePattern ::
145145
Maybe [Syntax.Id] ->
146146
KoreDefinition ->
147147
Syntax.KorePattern ->
148-
Except PatternError (Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
148+
Except
149+
PatternError
150+
( Internal.Term
151+
, [Internal.Predicate]
152+
, [Internal.Ceil]
153+
, Map Internal.Variable Internal.Term
154+
, [Syntax.KorePattern]
155+
)
149156
internalisePattern allowAlias checkSubsorts sortVars definition p = do
150157
(terms, predicates) <- partitionM isTermM $ explodeAnd p
151158

@@ -157,11 +164,9 @@ internalisePattern allowAlias checkSubsorts sortVars definition p = do
157164
internalPs <-
158165
internalisePredicates allowAlias checkSubsorts sortVars definition predicates
159166
pure
160-
( Internal.Pattern
161-
{ term
162-
, constraints = internalPs.boolPredicates
163-
, ceilConditions = Set.toList internalPs.ceilPredicates
164-
}
167+
( term
168+
, internalPs.boolPredicates
169+
, internalPs.ceilPredicates
165170
, internalPs.substitution
166171
, internalPs.unsupported
167172
)
@@ -196,7 +201,7 @@ internalisePatternOrTopOrBottom ::
196201
Except
197202
PatternError
198203
( PatternOrTopOrBottom
199-
([Internal.Variable], (Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern]))
204+
([Internal.Variable], Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
200205
)
201206
internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition existentials p = do
202207
let exploded = explodeAnd p
@@ -210,7 +215,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
210215
variableSort <- lookupInternalSort sortVars definition.sorts p sort
211216
let variableName = textToBS var.getId
212217
pure $ Internal.Variable{variableSort, variableName}
213-
IsPattern . (existentialVars,) <$> internalisePattern allowAlias checkSubsorts sortVars definition p
218+
(term, preds, ceilConditions, subst, unknown) <-
219+
internalisePattern allowAlias checkSubsorts sortVars definition p
220+
pure $
221+
IsPattern
222+
( existentialVars
223+
, Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions}
224+
, subst
225+
, unknown
226+
)
214227
where
215228
isTop = \case
216229
[Syntax.KJTop{sort}] -> Just $ IsTop sort
@@ -234,9 +247,13 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa
234247
internalisePredicates allowAlias checkSubsorts sortVars definition [syntaxPatt]
235248
)
236249
<|> ( withExcept (: []) $ do
237-
(pat, substitution, unsupported) <-
250+
(term, constrs, ceilConditions, substitution, unsupported) <-
238251
internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt
239-
pure $ TermAndPredicates pat substitution unsupported
252+
pure $
253+
TermAndPredicates
254+
Internal.Pattern{term, constraints = Set.fromList constrs, ceilConditions}
255+
substitution
256+
unsupported
240257
)
241258

242259
lookupInternalSort ::
@@ -412,8 +429,8 @@ internalisePredicates allowAlias checkSubsorts sortVars definition ps = do
412429

413430
pure
414431
InternalisedPredicates
415-
{ boolPredicates = Set.fromList $ [p | BoolPred p <- internalised] <> moreEquations
416-
, ceilPredicates = Set.fromList $ [p | CeilPred p <- internalised]
432+
{ boolPredicates = [p | BoolPred p <- internalised] <> moreEquations
433+
, ceilPredicates = [p | CeilPred p <- internalised]
417434
, substitution
418435
, unsupported = [p | UnsupportedPred p <- internalised]
419436
}
@@ -682,6 +699,8 @@ data PatternError
682699
| UnknownSymbol Syntax.Id Syntax.KorePattern
683700
| MacroOrAliasSymbolNotAllowed Syntax.Id Syntax.KorePattern
684701
| SubstitutionNotAllowed
702+
| PredicateNotAllowed
703+
| CeilNotAllowed
685704
| IncorrectSymbolArity Syntax.KorePattern Syntax.Id Int Int
686705
deriving stock (Eq, Show)
687706

@@ -715,6 +734,8 @@ patternErrorToRpcError = \case
715734
MacroOrAliasSymbolNotAllowed sym p ->
716735
wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p
717736
SubstitutionNotAllowed -> RpcError.ErrorOnly "Substitution predicates are not allowed here"
737+
PredicateNotAllowed -> RpcError.ErrorOnly "Predicates are not allowed here"
738+
CeilNotAllowed -> RpcError.ErrorOnly "Ceil predicates are not allowed here"
718739
IncorrectSymbolArity p s expected got ->
719740
wrap
720741
( "Inconsistent pattern. Symbol '"
@@ -740,6 +761,8 @@ logPatternError = \case
740761
UnknownSymbol sym p -> withKorePatternContext p $ logMessage $ "Unknown symbol '" <> Syntax.getId sym <> "'"
741762
MacroOrAliasSymbolNotAllowed sym p -> withKorePatternContext p $ logMessage $ "Symbol '" <> Syntax.getId sym <> "' is a macro/alias"
742763
SubstitutionNotAllowed -> logMessage ("Substitution predicates are not allowed here" :: Text)
764+
PredicateNotAllowed -> logMessage ("Predicates are not allowed here" :: Text)
765+
CeilNotAllowed -> logMessage ("Ceil predicates are not allowed here" :: Text)
743766
IncorrectSymbolArity p s expected got ->
744767
withKorePatternContext p $
745768
logMessage $

0 commit comments

Comments
 (0)