Skip to content

Commit fbee2cb

Browse files
jbertholdjberthold
authored
HOTFIXES not stuck on uneval.d functions, replacement from path condition (#4117)
## Indeterminate result for function calls under injections When the rewrite subject contains a function call under an injection, the function's return sort may be more general than the sort expected by a rewrite rule that is being tried. This shows up as a failing match between two injections in rule LHS and subject. Previous code was declaring this a match failure for the rule but didn't abort the rewrite. The correct behaviour is to abort the rewrite (or to unify, which booster doesn't). Fixes a problem where booster would return `Stuck` which then falls back to legacy `kore-rpc` where progress can be made. It is still possible for booster to return `Stuck` when trying to match a function call (because of rule indexing which limits the amount of rules that could possibly apply. An expression with an unevaluated function call will never be rewritten by booster, but a modification of the indexing mechanism and rule selection is left for future work. ## Added replacement from path conditions into term evaluation When the path condition contains equations of the form `domain-value ==Int expression`, this information should be used to replace any syntactic occurrences of `expression` by the obviously simpler `domain-value` (`expression` should obviously not be another, different, domain value so it must be a function call or a more complex expression). This holds likewise for `==Bool` and for other domain equality operations, `==Int` and `==Bool` replacements are implemented. The replacement happens after LLVM evaluation but before any other hook or (function or simplification) equation application.
1 parent 9b319f1 commit fbee2cb

File tree

3 files changed

+74
-101
lines changed

3 files changed

+74
-101
lines changed

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

Lines changed: 35 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ import Data.List (foldl1', intersperse, partition)
4444
import Data.List.NonEmpty qualified as NonEmpty
4545
import Data.Map (Map)
4646
import Data.Map qualified as Map
47-
import Data.Maybe (catMaybes, fromMaybe)
47+
import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
4848
import Data.Sequence (Seq (..), pattern (:<|))
4949
import Data.Sequence qualified as Seq
5050
import Data.Set (Set)
@@ -161,17 +161,20 @@ data EquationState = EquationState
161161
, cache :: SimplifierCache
162162
}
163163

164-
data SimplifierCache = SimplifierCache {llvm, equations :: Map Term Term}
164+
data SimplifierCache = SimplifierCache {llvm, equations, pathConditions :: Map Term Term}
165165
deriving stock (Show)
166166

167167
instance Semigroup SimplifierCache where
168168
cache1 <> cache2 =
169-
SimplifierCache (cache1.llvm <> cache2.llvm) (cache1.equations <> cache2.equations)
169+
SimplifierCache
170+
(cache1.llvm <> cache2.llvm)
171+
(cache1.equations <> cache2.equations)
172+
(cache1.pathConditions <> cache2.pathConditions)
170173

171174
instance Monoid SimplifierCache where
172-
mempty = SimplifierCache mempty mempty
175+
mempty = SimplifierCache mempty mempty mempty
173176

174-
data CacheTag = LLVM | Equations
177+
data CacheTag = LLVM | Equations | PathConditions
175178
deriving stock (Show)
176179

177180
instance ContextFor CacheTag where
@@ -192,9 +195,27 @@ startState cache known =
192195
, recursionStack = []
193196
, changed = False
194197
, predicates = known
195-
, cache
198+
, -- replacements from predicates are rebuilt from the path conditions every time
199+
cache = cache{pathConditions = buildReplacements known}
196200
}
197201

202+
buildReplacements :: Set Predicate -> Map Term Term
203+
buildReplacements = Map.fromList . mapMaybe toReplacement . Set.elems
204+
where
205+
toReplacement :: Predicate -> Maybe (Term, Term)
206+
toReplacement = \case
207+
Predicate (EqualsInt (v@DomainValue{}) t) -> Just (t, v)
208+
Predicate (EqualsInt t (v@DomainValue{})) -> Just (t, v)
209+
Predicate (EqualsBool (v@DomainValue{}) t) -> Just (t, v)
210+
Predicate (EqualsBool t (v@DomainValue{})) -> Just (t, v)
211+
_otherwise -> Nothing
212+
213+
cacheReset :: Monad io => EquationT io ()
214+
cacheReset = eqState $ do
215+
st@EquationState{predicates, cache} <- get
216+
let newCache = cache{equations = mempty, pathConditions = buildReplacements predicates}
217+
put st{cache = newCache}
218+
198219
eqState :: Monad io => StateT EquationState io a -> EquationT io a
199220
eqState = EquationT . lift . lift
200221

@@ -237,6 +258,7 @@ popRecursion = do
237258
else eqState $ put s{recursionStack = tail s.recursionStack}
238259

239260
toCache :: LoggerMIO io => CacheTag -> Term -> Term -> EquationT io ()
261+
toCache PathConditions _ _ = pure () -- never adding to the replacements
240262
toCache LLVM orig result = eqState . modify $
241263
\s -> s{cache = s.cache{llvm = Map.insert orig result s.cache.llvm}}
242264
toCache Equations orig result = eqState $ do
@@ -261,6 +283,7 @@ fromCache tag t = eqState $ do
261283
s <- get
262284
case tag of
263285
LLVM -> pure $ Map.lookup t s.cache.llvm
286+
PathConditions -> pure $ Map.lookup t s.cache.pathConditions
264287
Equations -> do
265288
case Map.lookup t s.cache.equations of
266289
Nothing -> pure Nothing
@@ -377,10 +400,14 @@ iterateEquations direction preference startTerm = do
377400
-- NB llvmSimplify is idempotent. No need to iterate if
378401
-- the equation evaluation does not change the term any more.
379402
resetChanged
403+
-- apply syntactic replacements of terms by domain values from path condition
404+
replacedTerm <-
405+
let simp = cached PathConditions $ traverseTerm BottomUp simp pure
406+
in simp llvmResult
380407
-- evaluate functions and simplify (recursively at each level)
381408
newTerm <-
382409
let simp = cached Equations $ traverseTerm direction simp (applyHooksAndEquations preference)
383-
in simp llvmResult
410+
in simp replacedTerm
384411
changeFlag <- getChanged
385412
if changeFlag
386413
then checkForLoop newTerm >> resetChanged >> go newTerm
@@ -913,8 +940,7 @@ applyEquation term rule =
913940
unless (null ensuredConditions) $ do
914941
withContextFor Equations . logMessage $
915942
("New ensured condition from evaluation, invalidating cache" :: Text)
916-
lift . eqState . modify $
917-
\s -> s{cache = s.cache{equations = mempty}}
943+
lift cacheReset
918944
pure $ substituteInTerm subst rule.rhs
919945
where
920946
filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate]

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -350,6 +350,17 @@ matchInj
350350
if isSubsort
351351
then bindVariable matchType v (Injection source2 source1 trm2)
352352
else failWith (DifferentSorts trm1 trm2)
353+
| FunctionApplication{} <- trm2 = do
354+
-- Functions may have a more general sort than the actual result.
355+
-- This means we cannot simply fail the rewrite: the match is
356+
-- indeterminate if the function result is.
357+
subsorts <- gets mSubsorts
358+
isSubsort <- -- rule requires a more specific sort?
359+
lift . withExcept (MatchFailed . SubsortingError) $
360+
checkSubsort subsorts source1 source2
361+
if isSubsort
362+
then addIndeterminate trm1 trm2
363+
else failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
353364
| otherwise =
354365
failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
355366
{-# INLINE matchInj #-}

‎booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev‎

Lines changed: 28 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -463,29 +463,13 @@
463463
"value": "0"
464464
},
465465
{
466-
"tag": "App",
467-
"name": "Lbllookup",
468-
"sorts": [],
469-
"args": [
470-
{
471-
"tag": "EVar",
472-
"name": "VarS",
473-
"sort": {
474-
"tag": "SortApp",
475-
"name": "SortMap",
476-
"args": []
477-
}
478-
},
479-
{
480-
"tag": "DV",
481-
"sort": {
482-
"tag": "SortApp",
483-
"name": "SortInt",
484-
"args": []
485-
},
486-
"value": "0"
487-
}
488-
]
466+
"tag": "DV",
467+
"sort": {
468+
"tag": "SortApp",
469+
"name": "SortInt",
470+
"args": []
471+
},
472+
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
489473
},
490474
{
491475
"tag": "App",
@@ -674,29 +658,13 @@
674658
"value": "0"
675659
},
676660
{
677-
"tag": "App",
678-
"name": "Lbllookup",
679-
"sorts": [],
680-
"args": [
681-
{
682-
"tag": "EVar",
683-
"name": "VarS",
684-
"sort": {
685-
"tag": "SortApp",
686-
"name": "SortMap",
687-
"args": []
688-
}
689-
},
690-
{
691-
"tag": "DV",
692-
"sort": {
693-
"tag": "SortApp",
694-
"name": "SortInt",
695-
"args": []
696-
},
697-
"value": "0"
698-
}
699-
]
661+
"tag": "DV",
662+
"sort": {
663+
"tag": "SortApp",
664+
"name": "SortInt",
665+
"args": []
666+
},
667+
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
700668
},
701669
{
702670
"tag": "App",
@@ -3517,29 +3485,13 @@
35173485
"value": "0"
35183486
},
35193487
{
3520-
"tag": "App",
3521-
"name": "Lbllookup",
3522-
"sorts": [],
3523-
"args": [
3524-
{
3525-
"tag": "EVar",
3526-
"name": "VarS",
3527-
"sort": {
3528-
"tag": "SortApp",
3529-
"name": "SortMap",
3530-
"args": []
3531-
}
3532-
},
3533-
{
3534-
"tag": "DV",
3535-
"sort": {
3536-
"tag": "SortApp",
3537-
"name": "SortInt",
3538-
"args": []
3539-
},
3540-
"value": "0"
3541-
}
3542-
]
3488+
"tag": "DV",
3489+
"sort": {
3490+
"tag": "SortApp",
3491+
"name": "SortInt",
3492+
"args": []
3493+
},
3494+
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
35433495
},
35443496
{
35453497
"tag": "App",
@@ -3733,29 +3685,13 @@
37333685
"value": "0"
37343686
},
37353687
{
3736-
"tag": "App",
3737-
"name": "Lbllookup",
3738-
"sorts": [],
3739-
"args": [
3740-
{
3741-
"tag": "EVar",
3742-
"name": "VarS",
3743-
"sort": {
3744-
"tag": "SortApp",
3745-
"name": "SortMap",
3746-
"args": []
3747-
}
3748-
},
3749-
{
3750-
"tag": "DV",
3751-
"sort": {
3752-
"tag": "SortApp",
3753-
"name": "SortInt",
3754-
"args": []
3755-
},
3756-
"value": "0"
3757-
}
3758-
]
3688+
"tag": "DV",
3689+
"sort": {
3690+
"tag": "SortApp",
3691+
"name": "SortInt",
3692+
"args": []
3693+
},
3694+
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
37593695
},
37603696
{
37613697
"tag": "App",

0 commit comments

Comments
 (0)