From ea63507e7f8f32f68b0192fbcdbd3fae0246b5ea Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Nov 2026 11:20:29 +0100 Subject: [PATCH] SSA: Split reads in MakeSsa based on explicit/implicit instead of certain. --- .../code/csharp/dataflow/internal/BaseSSA.qll | 4 +++ .../code/csharp/dataflow/internal/SsaImpl.qll | 4 +++ .../code/java/dataflow/internal/BaseSSA.qll | 4 ++- .../code/java/dataflow/internal/SsaImpl.qll | 4 ++- shared/ssa/codeql/ssa/Ssa.qll | 35 ++++++++++++++----- 5 files changed, 41 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 ccefca61186e..8f3eea408d2f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll @@ -149,5 +149,9 @@ private module BaseSsaImpl { i = -1 and w.isParameterInit(v) } + + predicate explicitRead(Expr e, SsaImplInput::SourceVariable v) { + e.(AssignableRead).getTarget() = v + } } } diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll index ce14d388e453..a7e948cddbac 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll @@ -76,6 +76,10 @@ private module SsaInput implements Impl::SsaInputSig { w.isParameterInit(p) ) } + + predicate explicitRead(Expr e, SsaImplInput::SourceVariable v) { + v.getAnAccess().(AssignableRead) = e + } } module Ssa_ = Impl::MakeSsa; diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll index ec480a6c0cc5..96dcfa001842 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll @@ -210,6 +210,8 @@ private module SsaInput implements Impl::SsaInputSig { i = -1 ) } + + predicate explicitRead(Expr e, BaseSsaSourceVariable v) { e = v.getAnAccess().(VarRead) } } module Ssa = Impl::MakeSsa; @@ -223,7 +225,7 @@ private module Cached { cached predicate captures(SsaImplicitEntryDefinition init, SsaDefinition capturedvar) { exists(BasicBlock bb, int i | - Ssa::ssaDefReachesUncertainRead(_, capturedvar, bb, i) and + Ssa::ssaDefReachesImplicitRead(capturedvar, bb, i) and variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i) ) } diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll index c69d6ed5f812..6f978406efa8 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll @@ -231,6 +231,8 @@ private module SsaInput implements Impl::SsaInputSig { i = -1 ) } + + predicate explicitRead(Expr e, SourceVariable v) { e = v.getAnAccess().(VarRead) } } module Ssa = Impl::MakeSsa; @@ -488,7 +490,7 @@ private module Cached { cached predicate captures(SsaImplicitEntryDefinition init, SsaDefinition capturedvar) { exists(BasicBlock bb, int i | - Ssa::ssaDefReachesUncertainRead(_, capturedvar, bb, i) and + Ssa::ssaDefReachesImplicitRead(capturedvar, bb, i) and variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i) ) } diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 9670655856d3..10c3e0f01eb5 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -1055,6 +1055,10 @@ module Make< class Parameter; + /** + * An explicit variable write. That is, a write for which there is an AST + * node representing it, for example an assignment expression or a parameter. + */ class VariableWrite { /** Gets the expression representing this write, if any. */ Expr asExpr(); @@ -1080,7 +1084,16 @@ module Make< Location getLocation(); } + /** + * Holds if `w` is an explicit write of `v` at the given location in the CFG. + */ predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SourceVariable v); + + /** + * Holds if `e` reads the value of `v`. These are the reads that are + * included in the `SsaDefinition.getARead()` member predicate. + */ + predicate explicitRead(Expr e, SourceVariable v); } /** @@ -1096,21 +1109,27 @@ module Make< private import SsaInput private import Cached + private predicate explicitRead(Expr e, BasicBlock bb, int i, SourceVariable v) { + explicitRead(e, v) and + e.getControlFlowNode() = bb.getNode(i) + } + cached private module Cached { cached - predicate ssaDefReachesCertainRead(Definition def, Expr e) { + predicate ssaDefReachesExplicitRead(Definition def, Expr e) { exists(SourceVariable v, BasicBlock bb, int i | ssaDefReachesRead(v, def, bb, i) and - variableRead(bb, i, v, true) and - e.getControlFlowNode() = bb.getNode(i) + explicitRead(e, bb, i, v) ) } cached - predicate ssaDefReachesUncertainRead(SourceVariable v, Definition def, BasicBlock bb, int i) { - ssaDefReachesRead(v, def, bb, i) and - variableRead(bb, i, v, false) + predicate ssaDefReachesImplicitRead(Definition def, BasicBlock bb, int i) { + exists(SourceVariable v | + ssaDefReachesRead(v, def, bb, i) and + not explicitRead(_, bb, i, v) + ) } cached @@ -1130,7 +1149,7 @@ module Make< predicate revRef() { any() } } - additional predicate ssaDefReachesUncertainRead = Cached::ssaDefReachesUncertainRead/4; + additional predicate ssaDefReachesImplicitRead = Cached::ssaDefReachesImplicitRead/3; additional predicate ssaCachedStageRevRef1 = Cached::revRef/0; @@ -1152,7 +1171,7 @@ module Make< } /** Gets a read of this SSA definition. */ - Expr getARead() { ssaDefReachesCertainRead(this, result) } + Expr getARead() { ssaDefReachesExplicitRead(this, result) } /** * Holds if this SSA definition is live at the end of basic block `bb`.