Skip to content

HOTFIXES not stuck on uneval.d functions, replacement from path condition #4117

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jul 16, 2025
Merged

HOTFIXES not stuck on uneval.d functions, replacement from path condition #4117

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
c674ab2
consider function calls under injections in subject indeterminate (do…
jberthold Jul 14, 2025
1c82261
apply known replacements from path conditions during evaluation
jberthold Jul 15, 2025
763d65b
Merge remote-tracking branch 'origin/master' into HOTFIX-not-stuck-on…
jberthold Jul 15, 2025
0499793
adjust integration test expectation (lookup replacement)
jberthold Jul 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 35 additions & 9 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ import Data.List (foldl1', intersperse, partition)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe (catMaybes, fromMaybe)
import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
import Data.Sequence (Seq (..), pattern (:<|))
import Data.Sequence qualified as Seq
import Data.Set (Set)
Expand Down Expand Up @@ -161,17 +161,20 @@ data EquationState = EquationState
, cache :: SimplifierCache
}

data SimplifierCache = SimplifierCache {llvm, equations :: Map Term Term}
data SimplifierCache = SimplifierCache {llvm, equations, pathConditions :: Map Term Term}
deriving stock (Show)

instance Semigroup SimplifierCache where
cache1 <> cache2 =
SimplifierCache (cache1.llvm <> cache2.llvm) (cache1.equations <> cache2.equations)
SimplifierCache
(cache1.llvm <> cache2.llvm)
(cache1.equations <> cache2.equations)
(cache1.pathConditions <> cache2.pathConditions)

instance Monoid SimplifierCache where
mempty = SimplifierCache mempty mempty
mempty = SimplifierCache mempty mempty mempty

data CacheTag = LLVM | Equations
data CacheTag = LLVM | Equations | PathConditions
deriving stock (Show)

instance ContextFor CacheTag where
Expand All @@ -192,9 +195,27 @@ startState cache known =
, recursionStack = []
, changed = False
, predicates = known
, cache
, -- replacements from predicates are rebuilt from the path conditions every time
cache = cache{pathConditions = buildReplacements known}
}

buildReplacements :: Set Predicate -> Map Term Term
buildReplacements = Map.fromList . mapMaybe toReplacement . Set.elems
where
toReplacement :: Predicate -> Maybe (Term, Term)
toReplacement = \case
Predicate (EqualsInt (v@DomainValue{}) t) -> Just (t, v)
Predicate (EqualsInt t (v@DomainValue{})) -> Just (t, v)
Predicate (EqualsBool (v@DomainValue{}) t) -> Just (t, v)
Predicate (EqualsBool t (v@DomainValue{})) -> Just (t, v)
_otherwise -> Nothing

cacheReset :: Monad io => EquationT io ()
cacheReset = eqState $ do
st@EquationState{predicates, cache} <- get
let newCache = cache{equations = mempty, pathConditions = buildReplacements predicates}
put st{cache = newCache}

eqState :: Monad io => StateT EquationState io a -> EquationT io a
eqState = EquationT . lift . lift

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

toCache :: LoggerMIO io => CacheTag -> Term -> Term -> EquationT io ()
toCache PathConditions _ _ = pure () -- never adding to the replacements
toCache LLVM orig result = eqState . modify $
\s -> s{cache = s.cache{llvm = Map.insert orig result s.cache.llvm}}
toCache Equations orig result = eqState $ do
Expand All @@ -261,6 +283,7 @@ fromCache tag t = eqState $ do
s <- get
case tag of
LLVM -> pure $ Map.lookup t s.cache.llvm
PathConditions -> pure $ Map.lookup t s.cache.pathConditions
Equations -> do
case Map.lookup t s.cache.equations of
Nothing -> pure Nothing
Expand Down Expand Up @@ -377,10 +400,14 @@ iterateEquations direction preference startTerm = do
-- NB llvmSimplify is idempotent. No need to iterate if
-- the equation evaluation does not change the term any more.
resetChanged
-- apply syntactic replacements of terms by domain values from path condition
replacedTerm <-
let simp = cached PathConditions $ traverseTerm BottomUp simp pure
in simp llvmResult
-- evaluate functions and simplify (recursively at each level)
newTerm <-
let simp = cached Equations $ traverseTerm direction simp (applyHooksAndEquations preference)
in simp llvmResult
in simp replacedTerm
changeFlag <- getChanged
if changeFlag
then checkForLoop newTerm >> resetChanged >> go newTerm
Expand Down Expand Up @@ -913,8 +940,7 @@ applyEquation term rule =
unless (null ensuredConditions) $ do
withContextFor Equations . logMessage $
("New ensured condition from evaluation, invalidating cache" :: Text)
lift . eqState . modify $
\s -> s{cache = s.cache{equations = mempty}}
lift cacheReset
pure $ substituteInTerm subst rule.rhs
where
filterOutKnownConstraints :: Set Predicate -> [Predicate] -> EquationT io [Predicate]
Expand Down
11 changes: 11 additions & 0 deletions booster/library/Booster/Pattern/Match.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -350,6 +350,17 @@ matchInj
if isSubsort
then bindVariable matchType v (Injection source2 source1 trm2)
else failWith (DifferentSorts trm1 trm2)
| FunctionApplication{} <- trm2 = do
-- Functions may have a more general sort than the actual result.
-- This means we cannot simply fail the rewrite: the match is
-- indeterminate if the function result is.
subsorts <- gets mSubsorts
isSubsort <- -- rule requires a more specific sort?
lift . withExcept (MatchFailed . SubsortingError) $
checkSubsort subsorts source1 source2
if isSubsort
then addIndeterminate trm1 trm2
else failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
| otherwise =
failWith (DifferentSorts (Injection source1 target1 trm1) (Injection source2 target2 trm2))
{-# INLINE matchInj #-}
Expand Down
120 changes: 28 additions & 92 deletions booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -463,29 +463,13 @@
"value": "0"
},
{
"tag": "App",
"name": "Lbllookup",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "VarS",
"sort": {
"tag": "SortApp",
"name": "SortMap",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
},
{
"tag": "App",
Expand Down Expand Up @@ -674,29 +658,13 @@
"value": "0"
},
{
"tag": "App",
"name": "Lbllookup",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "VarS",
"sort": {
"tag": "SortApp",
"name": "SortMap",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
},
{
"tag": "App",
Expand Down Expand Up @@ -3517,29 +3485,13 @@
"value": "0"
},
{
"tag": "App",
"name": "Lbllookup",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "VarS",
"sort": {
"tag": "SortApp",
"name": "SortMap",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
},
{
"tag": "App",
Expand Down Expand Up @@ -3733,29 +3685,13 @@
"value": "0"
},
{
"tag": "App",
"name": "Lbllookup",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "VarS",
"sort": {
"tag": "SortApp",
"name": "SortMap",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "115792089237316195423570985008687907853269984665640564039457584007913129639935"
},
{
"tag": "App",
Expand Down
Loading