Skip to content
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.

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

Ssa: Refactor shared SSA in preparation for eliminating phi-read definitions #18819

Merged
merged 30 commits into from
Feb 21, 2025
Merged
Show file tree
Hide file tree
Changes from 28 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
3822d14
SSA: Elaborate qldoc.
aschackmull Feb 11, 2025
36613e1
SSA: Remove superfluous conjunct (implied by refRank).
aschackmull Feb 11, 2025
b62432f
SSA: Remove superfluous boolean.
aschackmull Feb 14, 2025
c5e2884
SSA: Remove superfluous column from liveAtRank.
aschackmull Feb 14, 2025
5723d27
SSA: Make inReadDominanceFrontier a bit smaller without affecting phi…
aschackmull Feb 14, 2025
f80cd97
SSA: Factor out phi-read construction in its own predicate.
aschackmull Feb 17, 2025
81b3035
SSA: Inline predicate
aschackmull Feb 17, 2025
613323e
SSA: Copy parts of SsaDefReaches verbatim to new module.
aschackmull Feb 17, 2025
ea08c60
SSA: Copy 3 predicates from the outer scope verbatim into the new Rea…
aschackmull Feb 17, 2025
6e272d0
SSA: Ignore phi-reads in the new def-reaches module.
aschackmull Feb 17, 2025
77ccff6
SSA: Replace exported def-reaches predicates (behaviour-preserving).
aschackmull Feb 17, 2025
7e441d9
SSA: Fold getImmediateBasicBlockDominator into loop-invariant predicate.
aschackmull Feb 17, 2025
a4fee2e
SSA: Minor perf tweak to reduce tuple duplication.
aschackmull Feb 17, 2025
d5ac5b4
SSA: Replace uncertainWriteDefinitionInput implementation.
aschackmull Feb 17, 2025
11166fc
SSA: Restrict phi-read creation to be based on reachable reads.
aschackmull Feb 17, 2025
411aff6
SSA: Refactor ranking into parameterised module.
aschackmull Feb 17, 2025
d6dc91d
SSA: Inline predicate to simplify negation.
aschackmull Feb 17, 2025
35f50ba
SSA: Reimplement use-use.
aschackmull Feb 17, 2025
194afbb
Java: Simplify SSA for variable capture.
aschackmull Feb 18, 2025
cf2136f
SSA: Export simple firstUse and adjacentUseUse predicates.
aschackmull Feb 18, 2025
5379506
Java: Use firstUse and adjacentUseUse predicates.
aschackmull Feb 18, 2025
291ea6f
Java: Move SSA data flow test and extend it to cover phi-read input e…
aschackmull Feb 18, 2025
ed40035
C#/Ruby/Rust: Fix bug in adjacentReadPairSameVar.
aschackmull Feb 19, 2025
17ae747
C#: Switch use-use predicates to new implementation.
aschackmull Feb 19, 2025
b0a5e62
C#: Clean up unused.
aschackmull Feb 19, 2025
4ddc5c9
Ruby: Switch use-use predicates to new implementation.
aschackmull Feb 19, 2025
7e59603
Rust: Switch use-use predicates to new implementation.
aschackmull Feb 19, 2025
b76e5f5
SSA: Deprecate unused predicate.
aschackmull Feb 19, 2025
8e609b1
Ruby: Accept qltest change.
aschackmull Feb 20, 2025
8c0cc07
Ssa: Fix qldoc duplicate word.
aschackmull Feb 20, 2025
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
43 changes: 11 additions & 32 deletions csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -734,15 +734,15 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
}

pragma[noinline]
private predicate adjacentDefRead(
deprecated private predicate adjacentDefRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
SsaInput::SourceVariable v
) {
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}

private predicate adjacentDefReachesRead(
deprecated private predicate adjacentDefReachesRead(
Definition def, SsaInput::SourceVariable v, SsaInput::BasicBlock bb1, int i1,
SsaInput::BasicBlock bb2, int i2
) {
Expand All @@ -760,18 +760,7 @@ private predicate adjacentDefReachesRead(
)
}

/** Same as `adjacentDefRead`, but skips uncertain reads. */
pragma[nomagic]
private predicate adjacentDefSkipUncertainReads(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
exists(SsaInput::SourceVariable v |
adjacentDefReachesRead(def, v, bb1, i1, bb2, i2) and
SsaInput::variableRead(bb2, i2, v, true)
)
}

private predicate adjacentDefReachesUncertainRead(
deprecated private predicate adjacentDefReachesUncertainRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
exists(SsaInput::SourceVariable v |
Expand Down Expand Up @@ -933,10 +922,8 @@ private module Cached {
*/
cached
predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
def.definesAt(_, bb1, i1) and
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
cfn = bb2.getNode(i2)
exists(ControlFlow::BasicBlock bb, int i |
Impl::firstUse(def, bb, i, true) and cfn = bb.getNode(i)
)
}

Expand All @@ -947,25 +934,17 @@ private module Cached {
*/
cached
predicate adjacentReadPairSameVar(Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
exists(
ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2,
Ssa::SourceVariable v
|
Impl::ssaDefReachesRead(v, def, bb1, i1) and
Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
cfn1 = bb1.getNode(i1) and
variableReadActual(bb1, i1, _) and
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
cfn2 = bb2.getNode(i2)
)
}

cached
predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
Impl::lastRefRedef(def, bb, i, next) and
not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
or
exists(SsaInput::BasicBlock bb0, int i0 |
Impl::lastRefRedef(def, bb0, i0, next) and
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
)
}

cached
Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
Impl::uncertainWriteDefinitionInput(def, result)
Expand Down
80 changes: 12 additions & 68 deletions java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -490,26 +490,11 @@ private module Cached {
)
}

pragma[nomagic]
private predicate captureDefReaches(Definition def, SsaInput::BasicBlock bb2, int i2) {
variableCapture(def.getSourceVariable(), _, _, _) and
exists(SsaInput::BasicBlock bb1, int i1 |
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
def.definesAt(_, bb1, i1)
)
or
exists(SsaInput::BasicBlock bb3, int i3 |
captureDefReaches(def, bb3, i3) and
SsaInput::variableRead(bb3, i3, _, _) and
Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
)
}

/** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
cached
predicate captures(SsaImplicitInit init, SsaVariable capturedvar) {
exists(BasicBlock bb, int i |
captureDefReaches(capturedvar, bb, i) and
Impl::ssaDefReachesRead(_, capturedvar, bb, i) and
variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i)
)
}
Expand All @@ -523,34 +508,15 @@ private module Cached {
Impl::uncertainWriteDefinitionInput(redef, def)
}

pragma[nomagic]
private predicate defReaches(Definition def, DataFlowIntegration::Node node) {
exists(DataFlowIntegration::SsaDefinitionExtNode nodeFrom |
nodeFrom.getDefinitionExt() = def and
DataFlowIntegrationImpl::localFlowStep(_, nodeFrom, node, false)
)
or
exists(DataFlowIntegration::Node mid |
defReaches(def, mid) and
DataFlowIntegrationImpl::localFlowStep(_, mid, node, _)
|
// flow into phi input node
mid instanceof DataFlowIntegration::SsaInputNode
or
// flow into definition
mid instanceof DataFlowIntegration::SsaDefinitionExtNode
)
}

/**
* Holds if the value defined at `def` can reach `use` without passing through
* any other uses, but possibly through phi nodes and uncertain implicit updates.
*/
cached
predicate firstUse(Definition def, VarRead use) {
exists(DataFlowIntegration::ExprNode nodeTo |
nodeTo.getExpr() = use and
defReaches(def, nodeTo)
exists(BasicBlock bb, int i |
Impl::firstUse(def, bb, i, _) and
use.getControlFlowNode() = bb.getNode(i)
)
}

Expand Down Expand Up @@ -609,40 +575,17 @@ private module Cached {

cached
module SsaPublic {
pragma[nomagic]
private predicate useReaches(VarRead use, DataFlowIntegration::Node node, boolean sameVar) {
exists(DataFlowIntegration::ExprNode nodeFrom |
nodeFrom.getExpr() = use and
DataFlowIntegration::localFlowStep(_, nodeFrom, node, true) and
sameVar = true
)
or
exists(DataFlowIntegration::Node mid, boolean sameVarMid |
useReaches(use, mid, sameVarMid) and
DataFlowIntegration::localFlowStep(_, mid, node, _)
|
exists(Impl::DefinitionExt def |
// flow into definition
def = mid.(DataFlowIntegration::SsaDefinitionExtNode).getDefinitionExt()
or
// flow into phi input node
def = mid.(DataFlowIntegration::SsaInputNode).getDefinitionExt()
|
if def instanceof Impl::PhiReadNode then sameVar = sameVarMid else sameVar = false
)
)
}

/**
* Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
* variable, that is, the value read in `use1` can reach `use2` without passing
* through any other use or any SSA definition of the variable.
*/
cached
predicate adjacentUseUseSameVar(VarRead use1, VarRead use2) {
exists(DataFlowIntegration::ExprNode nodeTo |
nodeTo.getExpr() = use2 and
useReaches(use1, nodeTo, true)
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
use1.getControlFlowNode() = bb1.getNode(i1) and
use2.getControlFlowNode() = bb2.getNode(i2) and
Impl::adjacentUseUse(bb1, i1, bb2, i2, _, true)
)
}

Expand All @@ -654,9 +597,10 @@ private module Cached {
*/
cached
predicate adjacentUseUse(VarRead use1, VarRead use2) {
exists(DataFlowIntegration::ExprNode nodeTo |
nodeTo.getExpr() = use2 and
useReaches(use1, nodeTo, _)
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
use1.getControlFlowNode() = bb1.getNode(i1) and
use2.getControlFlowNode() = bb2.getNode(i2) and
Impl::adjacentUseUse(bb1, i1, bb2, i2, _, _)
)
}
}
Expand Down
24 changes: 24 additions & 0 deletions java/ql/test/library-tests/dataflow/ssa/A.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
public class A {
Object source() { return null; }
void sink(Object o) { }

boolean isSafe(Object o) { return o == null; }

void foo() {
Object x = source();
if (!isSafe(x)) {
x = null;
}
sink(x);

x = source();
if (!isSafe(x)) {
if (isSafe(x)) {
sink(x);
} else {
throw new RuntimeException();
}
}
sink(x);
}
}
Empty file.
31 changes: 31 additions & 0 deletions java/ql/test/library-tests/dataflow/ssa/test.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
import java
import semmle.code.java.controlflow.Guards
import semmle.code.java.dataflow.DataFlow

private predicate isSafe(Guard g, Expr checked, boolean branch) {
exists(MethodCall mc | g = mc |
mc.getMethod().hasName("isSafe") and
checked = mc.getAnArgument() and
branch = true
)
}

module TestConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
source.asExpr().(MethodCall).getMethod().hasName("source")
}

predicate isSink(DataFlow::Node sink) {
exists(MethodCall mc | mc.getMethod().hasName("sink") and mc.getAnArgument() = sink.asExpr())
}

predicate isBarrier(DataFlow::Node node) {
node = DataFlow::BarrierGuard<isSafe/3>::getABarrierNode()
}
}

module Flow = DataFlow::Global<TestConfig>;

from DataFlow::Node source, DataFlow::Node sink
where Flow::flow(source, sink)
select source, sink
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,6 @@ case String s when isSafe(s):
break;

}

String s2 = "string";

if (!isSafe(s2)) {
s2 = null;
}
sink(s2);
}

}
46 changes: 4 additions & 42 deletions ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -222,15 +222,6 @@ private predicate hasVariableReadWithCapturedWrite(
variableReadActualInOuterScope(bb, i, v, scope)
}

pragma[noinline]
private predicate adjacentDefRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
SsaInput::SourceVariable v
) {
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}

pragma[noinline]
deprecated private predicate adjacentDefReadExt(
DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
Expand All @@ -240,22 +231,6 @@ deprecated private predicate adjacentDefReadExt(
v = def.getSourceVariable()
}

private predicate adjacentDefReachesRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
def.definesAt(v, bb1, i1)
or
SsaInput::variableRead(bb1, i1, v, true)
)
or
exists(SsaInput::BasicBlock bb3, int i3 |
adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
SsaInput::variableRead(bb3, i3, _, false) and
Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
)
}

deprecated private predicate adjacentDefReachesReadExt(
DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
Expand All @@ -272,15 +247,6 @@ deprecated private predicate adjacentDefReachesReadExt(
)
}

/** Same as `adjacentDefRead`, but skips uncertain reads. */
pragma[nomagic]
private predicate adjacentDefSkipUncertainReads(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
SsaInput::variableRead(bb2, i2, _, true)
}

deprecated private predicate adjacentDefReachesUncertainReadExt(
DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
Expand Down Expand Up @@ -391,11 +357,7 @@ private module Cached {
*/
cached
predicate firstRead(Definition def, VariableReadAccessCfgNode read) {
exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 |
def.definesAt(_, bb1, i1) and
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
read = bb2.getNode(i2)
)
exists(Cfg::BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and read = bb.getNode(i))
}

/**
Expand All @@ -407,10 +369,10 @@ private module Cached {
predicate adjacentReadPair(
Definition def, VariableReadAccessCfgNode read1, VariableReadAccessCfgNode read2
) {
exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 |
exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2, LocalVariable v |
Impl::ssaDefReachesRead(v, def, bb1, i1) and
Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
read1 = bb1.getNode(i1) and
variableReadActual(bb1, i1, _) and
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
read2 = bb2.getNode(i2)
)
}
Expand Down
Loading
Loading