Skip to content

Commit b5d3b9f

Browse files
jbertholdjberthold
authored
4118 better indexing for rewrite rules (#4120)
Indexing is extended to * consider domain values * distinguish function and constructor symbols * use special indexes for internalised maps, sets, and lists Cell indexes form a (flat) lattice which is now explicit in a less-or-equal definition. ``` Anything ____________/ | \_______________________________________... / / | | \ \ IdxList..IdxSet IdxVal "x"..IdxVal "y" IdxCons "A".. IdxFun "f".. \_________| __ | ________|____________|____________/____... \ | / IdxNone ``` Rule selection now uses a function that selects all rule indexes which are (as a product lattice) greater than the _inverted_ term index (i.e., top element becomes bottom element), with all function indexes turned into `Anything` (top element) before the inversion. The new integration test shows why this is important for soundness. This addresses cases of unevaluated functions in indexed cells where previously booster would (likely) report `Stuck` or (unlikely) a wrong result, while the result should be `Aborted` (rules were excluded but they could apply depending on what kind of term the unevaluated function would return when evaluated). Fixes #4118
1 parent fbee2cb commit b5d3b9f

23 files changed

+3814
-1987
lines changed

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

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ import Booster.Definition.Attributes.Base
3030
import Booster.Definition.Base
3131
import Booster.Definition.Ceil (ComputeCeilSummary (..))
3232
import Booster.Pattern.Base
33-
import Booster.Pattern.Index (CellIndex (..), TermIndex (..))
33+
import Booster.Pattern.Index (TermIndex (..))
3434
import Booster.Pattern.Pretty
3535
import Booster.Prettyprinter
3636
import Booster.Util
@@ -111,16 +111,16 @@ instance Pretty Summary where
111111
: tableView prettyLabel prettyLabel summary.subSorts
112112
)
113113
<> ( "Rewrite rules by term index:"
114-
: tableView prettyTermIndex pretty summary.rewriteRules
114+
: tableView pretty pretty summary.rewriteRules
115115
)
116116
<> ( "Function equations by term index:"
117-
: tableView prettyTermIndex pretty summary.functionRules
117+
: tableView pretty pretty summary.functionRules
118118
)
119119
<> ( "Simplifications by term index:"
120-
: tableView prettyTermIndex pretty summary.simplifications
120+
: tableView pretty pretty summary.simplifications
121121
)
122122
<> ( "Ceils:"
123-
: tableView prettyTermIndex prettyCeilRule summary.ceils
123+
: tableView pretty prettyCeilRule summary.ceils
124124
)
125125
<> [mempty]
126126
where
@@ -140,13 +140,6 @@ instance Pretty Summary where
140140

141141
prettyLabel = either error (pretty . BS.unpack) . decodeLabel
142142

143-
prettyTermIndex :: TermIndex -> Doc a
144-
prettyTermIndex (TermIndex ixs) = Pretty.sep $ map prettyCellIndex ixs
145-
146-
prettyCellIndex Anything = "Anything"
147-
prettyCellIndex (TopSymbol sym) = prettyLabel sym
148-
prettyCellIndex None = "None"
149-
150143
prettyCeilRule :: RewriteRule r -> Doc a
151144
prettyCeilRule RewriteRule{lhs, rhs} =
152145
"#Ceil(" <+> pretty' @['Decoded, 'Truncated] lhs <+> ") =>" <+> pretty' @['Decoded, 'Truncated] rhs

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -802,7 +802,7 @@ applyEquations theory handler term = do
802802
withContext CtxAbort $ logMessage ("Index 'None'" :: Text)
803803
throw (IndexIsNone term)
804804
let
805-
indexes = Set.toList $ Idx.coveringIndexes index
805+
indexes = Set.toList $ Map.keysSet theory `Idx.covering` index
806806
equationsFor i = fromMaybe Map.empty $ Map.lookup i theory
807807
-- neither simplification nor function equations should need groups,
808808
-- since simplification priority is just a suggestion and function equations
@@ -1172,7 +1172,9 @@ simplifyConstraint' :: LoggerMIO io => Bool -> Term -> EquationT io Term
11721172
-- 'true \equals P' using simplifyBool if they are concrete, or using
11731173
-- evaluateTerm.
11741174
simplifyConstraint' recurseIntoEvalBool = \case
1175-
t@(Term TermAttributes{canBeEvaluated} _)
1175+
t@(Term TermAttributes{isEvaluated, canBeEvaluated} _)
1176+
| isEvaluated ->
1177+
pure t
11761178
| isConcrete t && canBeEvaluated -> do
11771179
mbApi <- (.llvmApi) <$> getConfig
11781180
case mbApi of

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

Lines changed: 129 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -7,34 +7,48 @@ Everything to do with term indexing.
77
module Booster.Pattern.Index (
88
CellIndex (..),
99
TermIndex (..),
10+
-- Flat lattice
11+
(^<=^),
12+
invert,
13+
-- compute index cover for rule selection
14+
covering,
15+
-- indexing
1016
compositeTermIndex,
1117
kCellTermIndex,
1218
termTopIndex,
13-
coveringIndexes,
19+
-- helpers
1420
hasNone,
21+
noFunctions,
1522
) where
1623

1724
import Control.Applicative (Alternative (..), asum)
1825
import Control.DeepSeq (NFData)
26+
import Data.ByteString.Char8 (ByteString, unpack)
1927
import Data.Functor.Foldable (embed, para)
2028
import Data.Maybe (fromMaybe)
2129
import Data.Set (Set)
2230
import Data.Set qualified as Set
2331
import GHC.Generics (Generic)
32+
import Prettyprinter (Doc, Pretty, pretty, sep)
2433

2534
import Booster.Pattern.Base
35+
import Booster.Util (decodeLabel)
2636

2737
{- | Index data allowing for a quick lookup of potential axioms.
2838
2939
A @Term@ is indexed by inspecting the top term component of one or
3040
more given cells. A @TermIndex@ is a list of @CellIndex@es.
3141
32-
The @CellIndex@ of a cell containing a @SymbolApplication@ node is the
33-
symbol at the top. Other terms that are not symbol applications have
34-
index @Anything@.
42+
The @CellIndex@ of a cell reflects the top constructor of the term.
43+
For @SymbolApplication@s, constructors and functions are distinguished,
44+
for @DomainValue@s, the actual value (as a string) is part of the index.
45+
Internalised collections have special indexes, Variables have index @Anything@.
46+
47+
NB Indexes are _unsorted_. For instance, @IdxVal "42"@ is the index of
48+
both String "42" _and_ Integer 42.
3549
3650
Rather than making the term indexing function partial, we introduce a
37-
unique bottom element @None@ to the index type (to make it a lattice).
51+
unique bottom element @IdxNone@ to the index type (to make it a lattice).
3852
This can then handle @AndTerm@ by indexing both arguments and
3953
combining them.
4054
@@ -47,52 +61,117 @@ newtype TermIndex = TermIndex [CellIndex]
4761
deriving anyclass (NFData)
4862

4963
data CellIndex
50-
= None -- bottom element
51-
| TopSymbol SymbolName
64+
= IdxNone -- bottom element
65+
| IdxCons SymbolName
66+
| IdxFun SymbolName
67+
| IdxVal ByteString
68+
| IdxMap
69+
| IdxList
70+
| IdxSet
5271
| Anything -- top element
53-
-- should we have | Value Sort ?? (see Term type)
5472
deriving stock (Eq, Ord, Show, Generic)
5573
deriving anyclass (NFData)
5674

57-
{- | Combines two indexes (an "infimum" function on the index lattice).
75+
{- | Index lattice class. This is mostly just a _flat lattice_ but also
76+
needs to support a special 'invert' method for the subject term index.
77+
-}
78+
class IndexLattice a where
79+
(^<=^) :: a -> a -> Bool
80+
81+
invert :: a -> a
82+
83+
{- | Partial less-or-equal for CellIndex (implies partial order)
84+
85+
Anything
86+
____________/ | \_______________________________________...
87+
/ / | | \ \
88+
IdxList ..IdxSet IdxVal "x"..IdxVal "y" IdxCons "A".. IdxFun "f"..
89+
\_________|__ | _______|____________|____________/____...
90+
\ | /
91+
IdxNone
92+
-}
93+
instance IndexLattice CellIndex where
94+
IdxNone ^<=^ _ = True
95+
a ^<=^ IdxNone = a == IdxNone
96+
_ ^<=^ Anything = True
97+
Anything ^<=^ a = a == Anything
98+
a ^<=^ b = a == b
99+
100+
invert IdxNone = Anything
101+
invert Anything = IdxNone
102+
invert a = a
103+
104+
-- | Partial less-or-equal for TermIndex (product lattice)
105+
instance IndexLattice TermIndex where
106+
TermIndex idxs1 ^<=^ TermIndex idxs2 = and $ zipWith (^<=^) idxs1 idxs2
107+
108+
invert (TermIndex idxs) = TermIndex (map invert idxs)
109+
110+
{- | Combines two indexes ("infimum" or "meet" function on the index lattice).
58111
59112
This is useful for terms containing an 'AndTerm': Any term that
60113
matches an 'AndTerm t1 t2' must match both 't1' and 't2', so 't1'
61114
and 't2' must have "compatible" indexes for this to be possible.
62115
-}
63116
instance Semigroup CellIndex where
64-
None <> _ = None
65-
_ <> None = None
117+
IdxNone <> _ = IdxNone
118+
_ <> IdxNone = IdxNone
66119
x <> Anything = x
67120
Anything <> x = x
68-
s@(TopSymbol s1) <> TopSymbol s2
69-
| s1 == s2 = s
70-
| otherwise = None -- incompatible indexes
121+
idx1 <> idx2
122+
| idx1 == idx2 = idx1
123+
| otherwise = IdxNone
71124

72-
{- | Compute all indexes that cover the given index, for rule lookup.
125+
-- | Pretty instances
126+
instance Pretty TermIndex where
127+
pretty (TermIndex ixs) = sep $ map pretty ixs
73128

74-
An index B is said to "cover" another index A if all parts of B are
75-
either equal to the respective parts of A, or 'Anything'.
129+
instance Pretty CellIndex where
130+
pretty IdxNone = "_|_"
131+
pretty Anything = "***"
132+
pretty (IdxCons sym) = "C--" <> prettyLabel sym
133+
pretty (IdxFun sym) = "F--" <> prettyLabel sym
134+
pretty (IdxVal sym) = "V--" <> prettyLabel sym
135+
pretty IdxMap = "Map"
136+
pretty IdxList = "List"
137+
pretty IdxSet = "Set"
76138

77-
When selecting candidate rules for a term, we must consider all
78-
rules whose index has either the exact same @CellIndex@ or
79-
@Anything@ at every position of their @TermIndex@.
80-
-}
81-
coveringIndexes :: TermIndex -> Set TermIndex
82-
coveringIndexes (TermIndex ixs) =
83-
Set.fromList . map TermIndex $ orAnything ixs
84-
where
85-
orAnything :: [CellIndex] -> [[CellIndex]]
86-
orAnything [] = [[]]
87-
orAnything (i : is) =
88-
let rest = orAnything is
89-
in map (i :) rest <> map (Anything :) rest
139+
prettyLabel :: ByteString -> Doc a
140+
prettyLabel = either error (pretty . unpack) . decodeLabel
90141

91-
{- | Check whether a @TermIndex@ has @None@ in any position (this
142+
{- | Check whether a @TermIndex@ has @IdxNone@ in any position (this
92143
means no match will be possible).
93144
-}
94145
hasNone :: TermIndex -> Bool
95-
hasNone (TermIndex ixs) = None `elem` ixs
146+
hasNone (TermIndex ixs) = IdxNone `elem` ixs
147+
148+
-- | turns IdxFun _ into Anything (for rewrite rule selection)
149+
noFunctions :: TermIndex -> TermIndex
150+
noFunctions (TermIndex ixs) = TermIndex (map funsAnything ixs)
151+
where
152+
funsAnything IdxFun{} = Anything
153+
funsAnything other = other
154+
155+
{- | Computes all indexes that "cover" the given index, for rule lookup.
156+
157+
An index B is said to "cover" an index A if all components of B are
158+
greater or equal to those of the respective component of A inverted.
159+
160+
* For components of A that are distinct from @Anything@, this means
161+
the component of B is equal to that of A or @Anything@.
162+
* For components of A that are @IdxNone@, the respective component of B
163+
_must_ be @Anything@. However, if A contains @IdxNone@ no match is
164+
possible anyway.
165+
* For components of A that are @Anything@, B can contain an
166+
arbitrary index (@IdxNone@ will again have no chance of a match,
167+
though).
168+
169+
When selecting candidate rules for a term, we must consider all
170+
rules whose index has either the exact same @CellIndex@ or
171+
@Anything@ at every position of their @TermIndex@.
172+
-}
173+
covering :: Set TermIndex -> TermIndex -> Set TermIndex
174+
covering prior ix = Set.filter (invert ix ^<=^) prior
96175

97176
-- | Indexes a term by the heads of K sequences in given cells.
98177
compositeTermIndex :: [SymbolName] -> Term -> TermIndex
@@ -162,11 +241,25 @@ stripSortInjections = \case
162241
termTopIndex :: Term -> TermIndex
163242
termTopIndex = TermIndex . (: []) . cellTopIndex
164243

244+
-- | Cell top indexes form a lattice with a flat partial ordering
165245
cellTopIndex :: Term -> CellIndex
166246
cellTopIndex = \case
167-
SymbolApplication symbol _ _ ->
168-
TopSymbol symbol.name
247+
ConsApplication symbol _ _ ->
248+
IdxCons symbol.name
249+
FunctionApplication symbol _ _ ->
250+
IdxFun symbol.name
251+
DomainValue _ v ->
252+
IdxVal v
253+
Var{} ->
254+
Anything
255+
KMap{} ->
256+
IdxMap
257+
KList{} ->
258+
IdxList
259+
KSet{} ->
260+
IdxSet
261+
-- look-through
262+
Injection _ _ t ->
263+
cellTopIndex t
169264
AndTerm t1 t2 ->
170265
cellTopIndex t1 <> cellTopIndex t2
171-
_other ->
172-
Anything

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

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,13 @@ rewriteStep cutLabels terminalLabels pat = do
179179
termIdx = getIndex pat.term
180180
when (Idx.hasNone termIdx) $ throw (TermIndexIsNone pat.term)
181181
let
182-
indexes = Set.toList $ Idx.coveringIndexes termIdx
182+
indexes =
183+
Set.toList $ Map.keysSet def.rewriteTheory `Idx.covering` Idx.noFunctions termIdx
184+
-- Function calls in the index have to be generalised to
185+
-- `Anything` for rewriting because they may evaluate to any
186+
-- category of terms. If there are any function calls in the
187+
-- subject, the rewrite can only succeed if the function call
188+
-- is matched to a variable.
183189
rulesFor i = fromMaybe Map.empty $ Map.lookup i def.rewriteTheory
184190
rules =
185191
map snd . Map.toAscList . Map.unionsWith (<>) $ map rulesFor indexes
@@ -761,7 +767,7 @@ data RewriteFailed k
761767
RewriteSortError (RewriteRule k) Term SortError
762768
| -- | An error was detected during matching
763769
InternalMatchError Text
764-
| -- | Term has index 'None', no rule should apply
770+
| -- | Term has index 'IdxNone', no rule should apply
765771
TermIndexIsNone Term
766772
deriving stock (Eq, Show)
767773

@@ -817,7 +823,7 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods (RewriteFailed
817823
, pretty $ show sortError
818824
]
819825
TermIndexIsNone term ->
820-
"Term index is None for term " <> pretty' @mods term
826+
"Term index is IdxNone for term " <> pretty' @mods term
821827
InternalMatchError err -> "An internal error occured" <> pretty err
822828

823829
ruleLabelOrLoc :: RewriteRule k -> Doc a

‎booster/test/internalisation/bool.kore.report‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -18,37 +18,37 @@ Subsorts:
1818
- SortBool: SortBool
1919
Rewrite rules by term index:
2020
Function equations by term index:
21-
- Lbl_=/=Bool_: /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (960, 8)
22-
- Lbl_andBool_: 4
21+
- F--Lbl_=/=Bool_: /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (960, 8)
22+
- F--Lbl_andBool_: 4
2323
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (933, 8)
2424
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (932, 8)
2525
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (934, 8)
2626
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (931, 8)
27-
- Lbl_andThenBool_: 4
27+
- F--Lbl_andThenBool_: 4
2828
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (938, 8)
2929
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (937, 8)
3030
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (939, 8)
3131
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (936, 8)
32-
- Lbl_impliesBool_: 4
32+
- F--Lbl_impliesBool_: 4
3333
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (958, 8)
3434
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (957, 8)
3535
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (956, 8)
3636
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (955, 8)
37-
- Lbl_orBool_: 4
37+
- F--Lbl_orBool_: 4
3838
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (948, 8)
3939
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (946, 8)
4040
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (947, 8)
4141
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (945, 8)
42-
- Lbl_orElseBool_: 4
42+
- F--Lbl_orElseBool_: 4
4343
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (953, 8)
4444
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (951, 8)
4545
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (952, 8)
4646
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (950, 8)
47-
- Lbl_xorBool_: 3
47+
- F--Lbl_xorBool_: 3
4848
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (943, 8)
4949
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (942, 8)
5050
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (941, 8)
51-
- LblnotBool_: 2
51+
- F--LblnotBool_: 2
5252
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (929, 8)
5353
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (928, 8)
5454
Simplifications by term index:

0 commit comments

Comments
 (0)