From e9bb6ff417c7a5574ef3f1ff84637b029c10e9ca Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 31 Aug 2026 13:14:53 +0200 Subject: [PATCH 1/2] SSA: add opt-in definition reachability caching Allow language-specific SSA instantiations that cross multiple cached API stages to cache the complete definition-rank and end-of-block reachability fixed points. Keep the default factory demand-specialized so unrelated instantiations retain their existing evaluator behavior. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 07c775e7-cd7c-4e1c-8d97-5194ffd43e1a --- shared/ssa/codeql/ssa/Ssa.qll | 92 +++++++++++++++++++++++++++++++++-- 1 file changed, 87 insertions(+), 5 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 88c1e906ac5b..5dc13fdb7b88 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -253,6 +253,20 @@ private module LivenessCaching implements LivenessCachingSig { predicate enabled() { any() } } +private signature module DefinitionReachabilityCachingSig { + predicate enabled(); +} + +private module NoDefinitionReachabilityCaching implements DefinitionReachabilityCachingSig { + pragma[inline] + predicate enabled() { none() } +} + +private module DefinitionReachabilityCaching implements DefinitionReachabilityCachingSig { + pragma[inline] + predicate enabled() { any() } +} + /** * Provides an SSA implementation. * @@ -272,7 +286,7 @@ private module LivenessCaching implements LivenessCachingSig { */ private module MakeImpl< LocationSig Location, BB::CfgSig Cfg, InputSig Input, - LivenessCachingSig CacheLiveness> + LivenessCachingSig CacheLiveness, DefinitionReachabilityCachingSig CacheDefinitionReachability> { private import Cfg private import Input @@ -530,7 +544,22 @@ private module MakeImpl< * Holds if the SSA definition `def` reaches rank index `rnk` in its own * basic block `bb`. */ - predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) { + private predicate ssaDefReachesRankUncached( + BasicBlock bb, Definition def, int rnk, SourceVariable v + ) { + exists(int i | + rnk = refRank(bb, i, v, Def()) and + def.definesAt(v, bb, i) + ) + or + ssaDefReachesRank(bb, def, rnk - 1, v) and + rnk = refRank(bb, _, v, Read()) + } + + cached + private predicate ssaDefReachesRankCached( + BasicBlock bb, Definition def, int rnk, SourceVariable v + ) { exists(int i | rnk = refRank(bb, i, v, Def()) and def.definesAt(v, bb, i) @@ -540,6 +569,15 @@ private module MakeImpl< rnk = refRank(bb, _, v, Read()) } + pragma[inline] + predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) { + not CacheDefinitionReachability::enabled() and + ssaDefReachesRankUncached(bb, def, rnk, v) + or + CacheDefinitionReachability::enabled() and + ssaDefReachesRankCached(bb, def, rnk, v) + } + /** * Holds if `v` is live at the end of basic block `bb` with the same value as at * the end of the immediate dominator, `idom`, of `bb`. @@ -557,7 +595,30 @@ private module MakeImpl< * SSA definition of `v`. */ pragma[nomagic] - predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) { + private predicate ssaDefReachesEndOfBlockUncached( + BasicBlock bb, Definition def, SourceVariable v + ) { + exists(int last | + last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and + ssaDefReachesRank(bb, def, last, v) and + liveAtExit(bb, v) + ) + or + exists(BasicBlock idom | + // The construction of SSA form ensures that each read of a variable is + // dominated by its definition. An SSA definition therefore reaches a + // control flow node if it is the _closest_ SSA definition that dominates + // the node. If two definitions dominate a node then one must dominate the + // other, so therefore the definition of _closest_ is given by the dominator + // tree. Thus, reaching definitions can be calculated in terms of dominance. + ssaDefReachesEndOfBlock(idom, def, v) and + liveThrough(idom, bb, v) + ) + } + + pragma[nomagic] + cached + private predicate ssaDefReachesEndOfBlockCached(BasicBlock bb, Definition def, SourceVariable v) { exists(int last | last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and ssaDefReachesRank(bb, def, last, v) and @@ -576,6 +637,15 @@ private module MakeImpl< ) } + pragma[inline] + predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) { + not CacheDefinitionReachability::enabled() and + ssaDefReachesEndOfBlockUncached(bb, def, v) + or + CacheDefinitionReachability::enabled() and + ssaDefReachesEndOfBlockCached(bb, def, v) + } + /** * Holds if the SSA definition of `v` at `def` reaches index `i` in its own * basic block `bb`, without crossing another SSA definition of `v`. @@ -2236,7 +2306,7 @@ private module MakeImpl< module Make< LocationSig Location, BB::CfgSig Cfg, InputSig Input> { - import MakeImpl + import MakeImpl } /** @@ -2247,5 +2317,17 @@ module Make< module MakeWithCachedLiveness< LocationSig Location, BB::CfgSig Cfg, InputSig Input> { - import MakeImpl + import MakeImpl +} + +/** + * Provides an SSA implementation that caches complete source-variable liveness and + * definition-reachability relations. + * + * Use this when the same SSA instantiation is exposed through multiple cached API stages. + */ +module MakeWithCachedLivenessAndDefinitionReachability< + LocationSig Location, BB::CfgSig Cfg, InputSig Input> +{ + import MakeImpl } From fc71c20369d455a2ec5fb9969cafeabc62a03ccb Mon Sep 17 00:00:00 2001 From: yoff Date: Mon, 31 Aug 2026 13:15:13 +0200 Subject: [PATCH 2/2] Python: cache shared SSA definition reachability Select the opt-in cached definition-reachability factory for Python main SSA. The independent capture-SSA instantiation continues to use the default uncached factory. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: 07c775e7-cd7c-4e1c-8d97-5194ffd43e1a --- python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll index a07d9d62f0da..41657362c1f1 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/SsaImpl.qll @@ -256,7 +256,7 @@ private module SsaImplInput implements SsaImplCommon::InputSig as Impl +import SsaImplCommon::MakeWithCachedLivenessAndDefinitionReachability as Impl // Matching the cases in `SsaImplInput.variableWrite` above newtype TVariableWrite =