From c674ab233a363135635bf7ecdb3971ac9de564ca Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 14 Jul 2025 12:41:42 +1000 Subject: [PATCH 1/3] consider function calls under injections in subject indeterminate (do not fail rewrite) --- booster/library/Booster/Pattern/Match.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 1fbc9d31c8..5e13c4b671 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -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 #-} From 1c82261991f54a334b85c0d3690c3c2600a8a0ef Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 15 Jul 2025 10:46:48 +1000 Subject: [PATCH 2/3] apply known replacements from path conditions during evaluation --- .../library/Booster/Pattern/ApplyEquations.hs | 44 +++++++++++++++---- booster/library/Booster/Pattern/Match.hs | 2 +- 2 files changed, 36 insertions(+), 10 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index cd4df2fae7..d163e60c79 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -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) @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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] diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 5e13c4b671..cff7abacb5 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -355,7 +355,7 @@ matchInj -- 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? + isSubsort <- -- rule requires a more specific sort? lift . withExcept (MatchFailed . SubsortingError) $ checkSubsort subsorts source1 source2 if isSubsort From 04997938cd1f2c6b4c1d16ae12bfb627f7e66057 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 15 Jul 2025 11:07:12 +1000 Subject: [PATCH 3/3] adjust integration test expectation (lookup replacement) --- .../response-001.booster-dev | 120 ++++-------------- 1 file changed, 28 insertions(+), 92 deletions(-) diff --git a/booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev b/booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev index 722051b4dc..e642edff2b 100644 --- a/booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev +++ b/booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev @@ -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", @@ -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", @@ -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", @@ -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",