From 393512f0d02e65148b3a21f10c7e48b1171550b7 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Tue, 25 Aug 2026 14:05:35 +0100 Subject: [PATCH 1/6] C++: Implement a pruning version of 'getAnUltimateDefinition'. --- .../cpp/ir/dataflow/internal/DataFlowUtil.qll | 2 + .../code/cpp/ir/dataflow/internal/SsaImpl.qll | 84 +++++++++++++++++-- 2 files changed, 79 insertions(+), 7 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll index 13d16375f236..17c3438f098a 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowUtil.qll @@ -1018,4 +1018,6 @@ module Ssa { class IndirectExplicitDefinition = SsaImpl::IndirectExplicitDefinition; class PhiNode = SsaImpl::PhiNode; + + import SsaImpl::Public } diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll index 432261dfe278..402925117c56 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll @@ -1405,14 +1405,80 @@ private class PhiCycle extends PhiCycleEquivalence::EquivalenceClass { } } -/** An static single assignment (SSA) definition. */ -class Definition extends SsaImpl::Definition { - private Definition getAPhiInputOrPriorDefinition() { - result = this.(PhiNode).getAnInput() - or - uncertainWriteDefinitionInput(this, result) +private Definition getAPhiInputOrPriorDefinition(Definition def) { + result = def.(PhiNode).getAnInput() + or + uncertainWriteDefinitionInput(def, result) +} + +module Public { + /** + * A module signature to define relevant ultimate definitions for an + * optimized version of `Definition.getAnUltimateDefinition`. + */ + signature module GetAnUltimateDefinitionSig { + /** + * Holds if `def` is a relevant definition. This defines the set + * of `Definition`s which may be returned by + * `GetAnUltimateDefinition::getAnUltimateDefinition`. + */ + predicate isRelevantUltimateDefinition(Definition def); + } + + /** + * A module which constructs an optimized version of + * ``` + * Definition.getAnUltimateDefinition + * ``` + * by restricting the set of possible ultimate definitions. + * + * Use this module by defining a module `M` which implements + * `GetAnUltimateDefinitionSig` and then call: + * ``` + * GetAnUltimateDefinition::getAnUltimateDefinition + * ``` + */ + module GetAnUltimateDefinition { + private import Sig + + private predicate relevantUltimateDefinition(Definition def) { + isRelevantUltimateDefinition(def) and + not def instanceof PhiNode + } + + private predicate fwd(Definition def) { + relevantUltimateDefinition(def) + or + exists(Definition def0 | + fwd(def0) and + def0 = getAPhiInputOrPriorDefinition(def) + ) + } + + private predicate step(Definition def1, Definition def2) { + fwd(def1) and + fwd(def2) and + def1 = getAPhiInputOrPriorDefinition(def2) + } + + /** + * Gets a definition that ultimately defines this SSA definition and is + * not itself a phi node. + * + * This predicate is restricted to ultimate definitions which + * satisfy `isRelevantUltimateDefinition`. + */ + Definition getAnUltimateDefinition(Definition def) { + step*(result, def) and + relevantUltimateDefinition(result) + } } +} +import Public + +/** An static single assignment (SSA) definition. */ +class Definition extends SsaImpl::Definition { /** * Holds if this SSA definition is live at the end of basic block `bb`. * That is, this definition reaches the end of basic block `bb`, at which @@ -1424,9 +1490,13 @@ class Definition extends SsaImpl::Definition { /** * Gets a definition that ultimately defines this SSA definition and is * not itself a phi node. + * + * Note: A more efficient implementation of this predicate exists. See the + * `GetAnUltimateDefinition` module for a description of how to access + * the more efficient implementation. */ final Definition getAnUltimateDefinition() { - result = this.getAPhiInputOrPriorDefinition*() and + result = getAPhiInputOrPriorDefinition*(this) and not result instanceof PhiNode } From 59170eeb0a18e3cf609b2cecede76a3faa6ef339 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Tue, 25 Aug 2026 14:08:28 +0100 Subject: [PATCH 2/6] C++: Use the optimized version of getAnUltimateDefinition in FlowSummaryImpl.qll. --- .../cpp/dataflow/internal/FlowSummaryImpl.qll | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll index 0eba3d5fc181..ecb60ba720ae 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll @@ -171,6 +171,23 @@ private module Input2 implements Impl::Private::InputSig2 { result = e.(ConversionCall).getQualifier().(LambdaExpression).getLambdaFunction() } + private module GetAnUltimateDefinitionInput implements Ssa::GetAnUltimateDefinitionSig { + predicate isRelevantUltimateDefinition(Ssa::Definition def) { + exists( + getFunctionFromExpr(def.(Ssa::DirectExplicitDefinition) + .getAssignedInstruction() + .(StoreInstruction) + .getSourceValue() + .getUnconvertedResultExpression()) + ) + } + } + + private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) { + result = + Ssa::GetAnUltimateDefinition::getAnUltimateDefinition(def) + } + class SourceSinkReportingElement extends Element { SourceSinkReportingElement() { this instanceof Expr or this instanceof Parameter } @@ -191,7 +208,7 @@ private module Input2 implements Impl::Private::InputSig2 { exists(Ssa::Definition def | def.getAUse().getDef().getUnconvertedResultExpression() = this and result = - getFunctionFromExpr(def.getAnUltimateDefinition() + getFunctionFromExpr(getAnUltimateDefinition(def) .(Ssa::DirectExplicitDefinition) .getAssignedInstruction() .(StoreInstruction) From 6214cd1bd8cbaf3b1cae680d772d696ab3f09e42 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Tue, 25 Aug 2026 14:15:58 +0100 Subject: [PATCH 3/6] C++: Cleanup. --- .../cpp/dataflow/internal/FlowSummaryImpl.qll | 33 +++++++++---------- 1 file changed, 16 insertions(+), 17 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll index ecb60ba720ae..efe18e0945ed 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/FlowSummaryImpl.qll @@ -171,21 +171,26 @@ private module Input2 implements Impl::Private::InputSig2 { result = e.(ConversionCall).getQualifier().(LambdaExpression).getLambdaFunction() } + private predicate isRelevantUltimateDefinition(Ssa::DirectExplicitDefinition def, Function f) { + f = + getFunctionFromExpr(def.getAssignedInstruction() + .(StoreInstruction) + .getSourceValue() + .getUnconvertedResultExpression()) + } + private module GetAnUltimateDefinitionInput implements Ssa::GetAnUltimateDefinitionSig { predicate isRelevantUltimateDefinition(Ssa::Definition def) { - exists( - getFunctionFromExpr(def.(Ssa::DirectExplicitDefinition) - .getAssignedInstruction() - .(StoreInstruction) - .getSourceValue() - .getUnconvertedResultExpression()) - ) + isRelevantUltimateDefinition(def, _) } } - private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) { - result = - Ssa::GetAnUltimateDefinition::getAnUltimateDefinition(def) + private predicate hasAnUltimateFunctionAccessDefinition(Ssa::Definition def, Function f) { + exists(Ssa::Definition ultimate | + ultimate = + Ssa::GetAnUltimateDefinition::getAnUltimateDefinition(def) and + isRelevantUltimateDefinition(ultimate, f) + ) } class SourceSinkReportingElement extends Element { @@ -207,13 +212,7 @@ private module Input2 implements Impl::Private::InputSig2 { // The expression is an SSA read of an assignment of a callable exists(Ssa::Definition def | def.getAUse().getDef().getUnconvertedResultExpression() = this and - result = - getFunctionFromExpr(getAnUltimateDefinition(def) - .(Ssa::DirectExplicitDefinition) - .getAssignedInstruction() - .(StoreInstruction) - .getSourceValue() - .getUnconvertedResultExpression()) + hasAnUltimateFunctionAccessDefinition(def, result) ) } From 891f2e1a4f9d160161548bfdc05e56965f41d4cc Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Tue, 25 Aug 2026 14:18:01 +0100 Subject: [PATCH 4/6] C++: Use the optimized version of getAnUltimateDefinition for iterator flow. --- .../ir/dataflow/internal/DataFlowPrivate.qll | 66 ++++++++++++------- 1 file changed, 41 insertions(+), 25 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll index 6b79671ce638..3a1b42645642 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll @@ -1977,13 +1977,23 @@ module IteratorFlow { } /** - * Gets an ultimate definition of `def`. - * - * Note: Unlike `def.getAnUltimateDefinition()` this predicate also - * traverses back through iterator increment and decrement operations. + * Holds if `write` is an instruction that writes to address `address` */ - private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) { - result = def.getAnUltimateDefinition() + private predicate isIteratorWrite(Instruction write, Operand address) { + exists(Ssa::DefImpl writeDef, IRBlock bb, int i | + writeDef.hasIndexInBlock(_, bb, i) and + bb.getInstruction(i) = write and + address = writeDef.getAddressOperand() + ) + } + + private module GetAnUltimateDefinitionInput implements Ssa::GetAnUltimateDefinitionSig { + predicate isRelevantUltimateDefinition(Ssa::Definition def) { fwd(_, def) } + } + + private Ssa::Definition getAnUltimateDefinitionStep(Ssa::Definition def) { + result = + Ssa::GetAnUltimateDefinition::getAnUltimateDefinition(def) or exists(IRBlock bb, int i, IteratorCrementCall crementCall, Ssa::SourceVariable sv | crementCall = def.getValue().asInstruction().(StoreInstruction).getSourceValue() and @@ -1993,14 +2003,28 @@ module IteratorFlow { ) } - /** - * Holds if `write` is an instruction that writes to address `address` - */ - private predicate isIteratorWrite(Instruction write, Operand address) { - exists(Ssa::DefImpl writeDef, IRBlock bb, int i | - writeDef.hasIndexInBlock(_, bb, i) and - bb.getInstruction(i) = write and - address = writeDef.getAddressOperand() + private predicate isSource(GetsIteratorCall beginCall, Ssa::Definition def) { + exists(StoreInstruction beginStore | + beginStore = def.getValue().asInstruction() and + operandForFullyConvertedCall(beginStore.getSourceValueOperand(), beginCall) + ) + } + + private predicate isSink(Instruction writeToDeref, Ssa::Definition def) { + exists(IteratorPointerDereferenceCall starCall, Operand address, IRBlock bbStar, int iStar | + isIteratorWrite(writeToDeref, address) and + operandForFullyConvertedCall(address, starCall) and + bbStar.getInstruction(iStar) = starCall and + Ssa::ssaDefReachesRead(_, def, bbStar, iStar) + ) + } + + private predicate fwd(GetsIteratorCall beginCall, Ssa::Definition def) { + isSource(beginCall, def) + or + exists(Ssa::Definition def0 | + fwd(beginCall, def0) and + def0 = getAnUltimateDefinitionStep(def) ) } @@ -2016,17 +2040,9 @@ module IteratorFlow { private predicate isIteratorStoreInstruction( GetsIteratorCall beginCall, Instruction writeToDeref ) { - exists( - StoreInstruction beginStore, IRBlock bbStar, int iStar, Ssa::Definition def, - IteratorPointerDereferenceCall starCall, Ssa::Definition ultimate, Operand address - | - isIteratorWrite(writeToDeref, address) and - operandForFullyConvertedCall(address, starCall) and - bbStar.getInstruction(iStar) = starCall and - Ssa::ssaDefReachesRead(_, def, bbStar, iStar) and - ultimate = getAnUltimateDefinition*(def) and - beginStore = ultimate.getValue().asInstruction() and - operandForFullyConvertedCall(beginStore.getSourceValueOperand(), beginCall) + exists(Ssa::Definition def | + fwd(beginCall, def) and + isSink(writeToDeref, def) ) } From ff0f892a3d0b53aa5cc36c6a0d0c1472557f20f4 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Tue, 25 Aug 2026 17:48:58 +0100 Subject: [PATCH 5/6] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll index 402925117c56..e42e09b5d7c6 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll @@ -1477,7 +1477,7 @@ module Public { import Public -/** An static single assignment (SSA) definition. */ +/** A static single assignment (SSA) definition. */ class Definition extends SsaImpl::Definition { /** * Holds if this SSA definition is live at the end of basic block `bb`. From 49600c17b752590c2bff7e01c8ee46afe8381c37 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Wed, 26 Aug 2026 12:54:41 +0100 Subject: [PATCH 6/6] C++: Add comments. --- .../code/cpp/ir/dataflow/internal/SsaImpl.qll | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll index e42e09b5d7c6..38fbf87a403b 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll @@ -1446,15 +1446,31 @@ module Public { not def instanceof PhiNode } + /** + * The `getAnUltimateDefinition` predicate uses an optimized step relation + * which is pruned to only those uncertain steps which lead back to a + * definition which satisfies `relevantUltimateDefinition`. This predicate + * computes the subset of `Definition`s which can lead back to definitions + * which satisfy `relevantUltimateDefinition`. + */ private predicate fwd(Definition def) { + // Base case: This definition is a relevant definition relevantUltimateDefinition(def) or exists(Definition def0 | + // Recursive case: `def0` is a relevant definition, and + // `def` is an uncertain step which takes us back to `def0`. fwd(def0) and def0 = getAPhiInputOrPriorDefinition(def) ) } + /** + * Holds if `def1 = getAPhiInputOrPriorDefinition(def2)`, and + * both `def1` and `def2` are part of a sequence of uncertain + * steps which lead back to a `Definition` which + * satisfies `relevantUltimateDefinition`. + */ private predicate step(Definition def1, Definition def2) { fwd(def1) and fwd(def2) and