Skip to content

Commit

Permalink
Merge pull request #18819 from aschackmull/ssa/refactor-phiread3
Browse files Browse the repository at this point in the history
Ssa: Refactor shared SSA in preparation for eliminating phi-read definitions
  • Loading branch information
aschackmull authored Feb 21, 2025
2 parents 26da997 + 8c0cc07 commit 1c616d1
Show file tree
Hide file tree
Showing 10 changed files with 448 additions and 280 deletions.
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
7 changes: 0 additions & 7 deletions java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java
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
1 change: 0 additions & 1 deletion ruby/ql/test/library-tests/variables/ssa.expected
Original file line number Diff line number Diff line change
Expand Up @@ -527,7 +527,6 @@ adjacentReads
| nested_scopes.rb:8:5:35:7 | self (N) | nested_scopes.rb:8:5:35:7 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:34:7:34:12 | self |
| nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:14:16:14:16 | a | nested_scopes.rb:15:11:15:11 | a |
| nested_scopes.rb:27:7:29:9 | self (show) | nested_scopes.rb:27:7:29:9 | self | nested_scopes.rb:28:11:28:16 | self | nested_scopes.rb:28:16:28:16 | self |
| nested_scopes.rb:30:16:30:19 | self (class << ...) | nested_scopes.rb:30:7:33:9 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:32:11:32:16 | self |
| parameters.rb:1:9:5:3 | <captured entry> self | parameters.rb:1:1:62:1 | self | parameters.rb:3:4:3:9 | self | parameters.rb:4:4:4:9 | self |
| parameters.rb:7:26:7:31 | pizzas | parameters.rb:7:26:7:31 | pizzas | parameters.rb:8:6:8:11 | pizzas | parameters.rb:11:14:11:19 | pizzas |
| parameters.rb:25:1:28:3 | self (opt_param) | parameters.rb:25:1:28:3 | self | parameters.rb:26:3:26:11 | self | parameters.rb:27:3:27:11 | self |
Expand Down
Loading

0 comments on commit 1c616d1

Please sign in to comment.