Skip to content

SSA: Split reads in MakeSsa based on explicit/implicit instead of certain/uncertain. #23071

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
aschackmull wants to merge 1 commit into
base: main
Choose a base branch
from
+41 −10
Open

SSA: Split reads in MakeSsa based on explicit/implicit instead of certain/uncertain. #23071

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,5 +149,9 @@ private module BaseSsaImpl {
i = -1 and
w.isParameterInit(v)
}

predicate explicitRead(Expr e, SsaImplInput::SourceVariable v) {
e.(AssignableRead).getTarget() = v
}
}
}
4 changes: 4 additions & 0 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<SsaInput>;
Expand Down
4 changes: 3 additions & 1 deletion java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<SsaInput>;
Expand All @@ -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)
)
}
Expand Down
4 changes: 3 additions & 1 deletion java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<SsaInput>;
Expand Down Expand Up @@ -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)
)
}
Expand Down
35 changes: 27 additions & 8 deletions shared/ssa/codeql/ssa/Ssa.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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);

@hvitved hvitved Nov 11, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When is not the same as

predicate explicitRead(Expr e, SourceVariable v) {
    exists(BasicBlock bb, int i |
      variableRead(bb, i, v, true) and
      e.getControlFlowNode() = bb.getNode(i)
    )
}

@aschackmull aschackmull Nov 11, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The whole point of the PR is to be able to distinguish the two. If we merely use variableRead(bb, i, v, true) and e.getControlFlowNode() = bb.getNode(i) then we make the assumption that the expression implies the variable - and furthermore, in this context we assume that the expression is the variable read. This is true for explicit reads where the expression is a concrete read of a specific variable, but there are several cases where we have certain reads (4th column = true in variableRead) that are implicit, so the expression at the cfg node of the read isn't the actual variable read. E.g. implicit this/self, which is tracked as an SSA variable in unified. Also, Go functions have an epilogue where return variables are implicitly read. These are reads that should have certain = true because they should be included in the data flow integration, but they should not be included in SsaVariable.getARead(), since that returns an expression that's assumed to equal the read.

}

/**
Expand All @@ -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
Expand All @@ -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;

Expand All @@ -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`.
Expand Down
Loading