From 145d3242a6858d0a6ceea4570a9357c5fb70db94 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 16 Apr 2026 13:30:47 +0200 Subject: [PATCH 1/5] C#: Instantiate shared SSA wrappers for BaseSSA. --- .../code/csharp/dataflow/internal/BaseSSA.qll | 50 +++++++++++++++---- 1 file changed, 40 insertions(+), 10 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll index 4f37508f9a2c..629cc8f7b1cd 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll @@ -12,7 +12,7 @@ module BaseSsa { * targeting local scope variable `v`. */ private predicate definitionAt( - AssignableDefinition def, BasicBlock bb, int i, SsaInput::SourceVariable v + AssignableDefinition def, BasicBlock bb, int i, SsaImplInput::SourceVariable v ) { bb.getNode(i) = def.getExpr().getControlFlowNode() and v = def.getTarget() and @@ -24,7 +24,7 @@ module BaseSsa { ) } - private predicate implicitEntryDef(Callable c, EntryBasicBlock bb, SsaInput::SourceVariable v) { + private predicate entryDef(Callable c, EntryBasicBlock bb, SsaImplInput::SourceVariable v) { exists(EntryBasicBlock entry | c = entry.getEnclosingCallable() and // In case `c` has multiple bodies, we want each body to get its own implicit @@ -79,7 +79,7 @@ module BaseSsa { } } - private module SsaInput implements SsaImplCommon::InputSig { + private module SsaImplInput implements SsaImplCommon::InputSig { class SourceVariable = SimpleLocalScopeVariable; predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) { @@ -88,7 +88,7 @@ module BaseSsa { if def.isCertain() then certain = true else certain = false ) or - implicitEntryDef(_, bb, v) and + entryDef(_, bb, v) and i = -1 and certain = true } @@ -102,7 +102,37 @@ module BaseSsa { } } - private module SsaImpl = SsaImplCommon::Make; + private module SsaImpl = SsaImplCommon::Make; + + private module SsaInput implements SsaImpl::SsaInputSig { + private import csharp as CS + + class Expr = CS::Expr; + + class Parameter = CS::Parameter; + + class VariableWrite extends AssignableDefinition { + Expr asExpr() { result = this.getExpr() } + + Expr getValue() { result = this.getSource() } + + predicate isParameterInit(Parameter p) { + this.(ImplicitParameterDefinition).getParameter() = p + } + } + + predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SsaImplInput::SourceVariable v) { + definitionAt(w, bb, i, v) + or + entryDef(_, bb, v) and + i = -1 and + w.isParameterInit(v) + } + } + + module Ssa = SsaImpl::MakeSsa; + + import Ssa class Definition extends SsaImpl::Definition { final AssignableRead getARead() { @@ -113,16 +143,16 @@ module BaseSsa { } final AssignableDefinition getDefinition() { - exists(BasicBlock bb, int i, SsaInput::SourceVariable v | + exists(BasicBlock bb, int i, SsaImplInput::SourceVariable v | this.definesAt(v, bb, i) and definitionAt(result, bb, i, v) ) } - final predicate isImplicitEntryDefinition(SsaInput::SourceVariable v) { + final predicate isImplicitEntryDefinition(SsaImplInput::SourceVariable v) { exists(BasicBlock bb | this.definesAt(v, bb, -1) and - implicitEntryDef(_, bb, v) + entryDef(_, bb, v) ) } @@ -139,9 +169,9 @@ module BaseSsa { override Location getLocation() { result = this.getDefinition().getLocation() or - exists(Callable c, BasicBlock bb, SsaInput::SourceVariable v | + exists(Callable c, BasicBlock bb, SsaImplInput::SourceVariable v | this.definesAt(v, bb, -1) and - implicitEntryDef(c, bb, v) and + entryDef(c, bb, v) and result = c.getLocation() ) } From bbd60031b15fe5eaf6b2b22c246cb86257e9d2bb Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 16 Apr 2026 13:58:21 +0200 Subject: [PATCH 2/5] C#: Replace references to old BaseSSA classes. --- .../code/csharp/dataflow/internal/BaseSSA.qll | 49 ------------------- .../code/csharp/dataflow/internal/Steps.qll | 4 +- .../semmle/code/csharp/dispatch/Dispatch.qll | 4 +- .../dataflow/ssa/BaseSsaConsistency.ql | 4 +- 4 files changed, 7 insertions(+), 54 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll index 629cc8f7b1cd..8cf9c85d6a1e 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll @@ -133,53 +133,4 @@ module BaseSsa { module Ssa = SsaImpl::MakeSsa; import Ssa - - class Definition extends SsaImpl::Definition { - final AssignableRead getARead() { - exists(BasicBlock bb, int i | - SsaImpl::ssaDefReachesRead(_, this, bb, i) and - result.getControlFlowNode() = bb.getNode(i) - ) - } - - final AssignableDefinition getDefinition() { - exists(BasicBlock bb, int i, SsaImplInput::SourceVariable v | - this.definesAt(v, bb, i) and - definitionAt(result, bb, i, v) - ) - } - - final predicate isImplicitEntryDefinition(SsaImplInput::SourceVariable v) { - exists(BasicBlock bb | - this.definesAt(v, bb, -1) and - entryDef(_, bb, v) - ) - } - - private Definition getAPhiInputOrPriorDefinition() { - result = this.(PhiNode).getAnInput() or - SsaImpl::uncertainWriteDefinitionInput(this, result) - } - - final Definition getAnUltimateDefinition() { - result = this.getAPhiInputOrPriorDefinition*() and - not result instanceof PhiNode - } - - override Location getLocation() { - result = this.getDefinition().getLocation() - or - exists(Callable c, BasicBlock bb, SsaImplInput::SourceVariable v | - this.definesAt(v, bb, -1) and - entryDef(c, bb, v) and - result = c.getLocation() - ) - } - } - - class PhiNode extends SsaImpl::PhiNode, Definition { - override Location getLocation() { result = this.getBasicBlock().getLocation() } - - final Definition getAnInput() { SsaImpl::phiHasInputFromBlock(this, result, _) } - } } diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/Steps.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/Steps.qll index 63cd0b65dc67..7e2709468d6a 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/Steps.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/Steps.qll @@ -15,8 +15,8 @@ module Steps { * Gets a read that may read the value assigned at definition `def`. */ private AssignableRead getARead(AssignableDefinition def) { - exists(BaseSsa::Definition ssaDef | - ssaDef.getAnUltimateDefinition().getDefinition() = def and + exists(BaseSsa::SsaDefinition ssaDef | + ssaDef.getAnUltimateDefinition().(BaseSsa::SsaExplicitWrite).getDefinition() = def and result = ssaDef.getARead() ) or diff --git a/csharp/ql/lib/semmle/code/csharp/dispatch/Dispatch.qll b/csharp/ql/lib/semmle/code/csharp/dispatch/Dispatch.qll index 10ea1c8eb524..6d535025a195 100644 --- a/csharp/ql/lib/semmle/code/csharp/dispatch/Dispatch.qll +++ b/csharp/ql/lib/semmle/code/csharp/dispatch/Dispatch.qll @@ -355,8 +355,8 @@ private module Internal { 1 < strictcount(this.getADynamicTarget().getUnboundDeclaration()) and c = this.getCall().getEnclosingCallable().getUnboundDeclaration() and ( - exists(BaseSsa::Definition def, Parameter p | - def.isImplicitEntryDefinition(p) and + exists(BaseSsa::SsaParameterInit def, Parameter p | + def.getParameter() = p and this.getSyntheticQualifier() = def.getARead() and p.getPosition() = i and c.getAParameter() = p and diff --git a/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql b/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql index 86e13215b0c4..5a754ef3041d 100644 --- a/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql +++ b/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql @@ -1,7 +1,9 @@ import csharp import semmle.code.csharp.dataflow.internal.BaseSSA -from AssignableRead ar, BaseSsa::Definition ssaDef, AssignableDefinition def, LocalScopeVariable v +from + AssignableRead ar, BaseSsa::SsaExplicitWrite ssaDef, AssignableDefinition def, + LocalScopeVariable v where ar = ssaDef.getARead() and def = ssaDef.getDefinition() and From ae7904f0c8b8ab7e8a1c688a906feee8816f4005 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 17 Apr 2026 14:32:40 +0200 Subject: [PATCH 3/5] C#: Fix BaseSSA caching. --- .../semmle/code/csharp/dataflow/internal/BaseSSA.qll | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll index 8cf9c85d6a1e..f5e7d22eb00a 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll @@ -7,6 +7,15 @@ module BaseSsa { private import AssignableDefinitions private import codeql.ssa.Ssa as SsaImplCommon + cached + private module BaseSsaStage { + cached + predicate ref() { any() } + + cached + predicate backref() { (exists(any(SsaDefinition def).getARead()) implies any()) } + } + /** * Holds if the `i`th node of basic block `bb` is assignable definition `def`, * targeting local scope variable `v`. @@ -83,6 +92,7 @@ module BaseSsa { class SourceVariable = SimpleLocalScopeVariable; predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) { + BaseSsaStage::ref() and exists(AssignableDefinition def | definitionAt(def, bb, i, v) and if def.isCertain() then certain = true else certain = false From b0c31badc24dc41d6ecf2af4c93a56c545d68ad0 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 17 Apr 2026 15:10:35 +0200 Subject: [PATCH 4/5] C#: Bugfix for multi-body baseSsa entry defs. --- csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll index f5e7d22eb00a..63a9e782250f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll @@ -33,7 +33,7 @@ module BaseSsa { ) } - private predicate entryDef(Callable c, EntryBasicBlock bb, SsaImplInput::SourceVariable v) { + private predicate entryDef(Callable c, BasicBlock bb, SsaImplInput::SourceVariable v) { exists(EntryBasicBlock entry | c = entry.getEnclosingCallable() and // In case `c` has multiple bodies, we want each body to get its own implicit From 4b8e4b40af7c49137ff935a336c4ba1608586935 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 22 Apr 2026 14:00:13 +0200 Subject: [PATCH 5/5] C#: Fix test. --- .../ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql b/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql index 5a754ef3041d..4748f516114c 100644 --- a/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql +++ b/csharp/ql/test/library-tests/dataflow/ssa/BaseSsaConsistency.ql @@ -11,5 +11,9 @@ where not exists(Ssa::ExplicitDefinition edef | edef.getADefinition() = def and edef.getARead() = ar + ) and + not exists(Ssa::ImplicitParameterDefinition edef | + edef.getParameter() = def.(AssignableDefinitions::ImplicitParameterDefinition).getParameter() and + edef.getARead() = ar ) select ar, def