C#: Adjust flow into phi nodes

This commit is contained in:
Tom Hvitved
2021-01-12 11:00:03 +01:00
parent 38b0f743cb
commit 6ffeaf8c2a
5 changed files with 70 additions and 41 deletions

View File

@@ -266,16 +266,15 @@ module LocalFlow {
}
/**
* Holds if `nodeFrom` is a last node referencing SSA definition `def`.
* Either an SSA definition node for `def` when there is no read of `def`,
* or a last read of `def`.
* Holds if `nodeFrom` is a last node referencing SSA definition `def`, which
* can reach `next`.
*/
private predicate localFlowSsaInput(Node nodeFrom, Ssa::Definition def) {
def = nodeFrom.(SsaDefinitionNode).getDefinition() and
not exists(def.getARead())
or
exists(AssignableRead read, ControlFlow::Node cfn | read = nodeFrom.asExprAtNode(cfn) |
def.getALastReadAtNode(cfn) = read
private predicate localFlowSsaInput(Node nodeFrom, Ssa::Definition def, Ssa::Definition next) {
exists(ControlFlow::BasicBlock bb, int i | SsaImpl::lastRefBeforeRedef(def, bb, i, next) |
def = nodeFrom.(SsaDefinitionNode).getDefinition() and
def.definesAt(_, bb, i)
or
nodeFrom.asExprAtNode(bb.getNode(i)) instanceof AssignableRead
)
}
@@ -302,14 +301,14 @@ module LocalFlow {
or
// Flow into phi node
exists(Ssa::PhiNode phi |
localFlowSsaInput(nodeFrom, def) and
localFlowSsaInput(nodeFrom, def, phi) and
phi = nodeTo.(SsaDefinitionNode).getDefinition() and
def = phi.getAnInput()
)
or
// Flow into uncertain SSA definition
exists(LocalFlow::UncertainExplicitSsaDefinition uncertain |
localFlowSsaInput(nodeFrom, def) and
localFlowSsaInput(nodeFrom, def, uncertain) and
uncertain = nodeTo.(SsaDefinitionNode).getDefinition() and
def = uncertain.getPriorDefinition()
)

View File

@@ -6,7 +6,7 @@ import csharp
import SsaImplCommon
/** A classification of variable reads. */
newtype TReadKind =
private newtype TReadKind =
/** An actual read. */
ActualRead() or
/**
@@ -49,7 +49,7 @@ newtype TReadKind =
RefReadBeforeWrite()
/** A classification of variable reads. */
class ReadKind extends TReadKind {
private class ReadKind extends TReadKind {
string toString() {
this = ActualRead() and
result = "ActualRead"
@@ -199,7 +199,7 @@ private module SourceVariableImpl {
rk = RefReadBeforeWrite()
}
private predicate outRefExitRead(ControlFlow::BasicBlock bb, int i, LocalScopeSourceVariable v) {
predicate outRefExitRead(ControlFlow::BasicBlock bb, int i, LocalScopeSourceVariable v) {
exists(ControlFlow::Nodes::AnnotatedExitNode exit |
exit.isNormal() and
exists(LocalScopeVariable lsv |
@@ -1130,7 +1130,6 @@ private module Cached {
) {
exists(Ssa::Definition def0, ControlFlow::BasicBlock bb, int i |
def = def0.getAnUltimateDefinition() and
lastRef(def0, bb, i) and
capturedReadOut(bb, i, def0.getSourceVariable(), cdef.getSourceVariable(), cdef.getCall(),
additionalCalls)
)
@@ -1199,12 +1198,28 @@ private module Cached {
variableRead(bb2, i2, _, any(ReadKind rk | rk.isPseudo()))
}
private predicate reachesLastRefRedef(
Definition def, ControlFlow::BasicBlock bb, int i, Definition next
) {
lastRefRedef(def, bb, i, next)
or
exists(ControlFlow::BasicBlock bb0, int i0 |
reachesLastRefRedef(def, bb0, i0, next) and
adjacentDefPseudoRead(def, bb, i, bb0, i0)
)
}
cached
predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
reachesLastRefRedef(def, bb, i, next) and
not variableRead(bb, i, def.getSourceVariable(), any(ReadKind rk | rk.isPseudo()))
}
private predicate reachesLastRef(Definition def, ControlFlow::BasicBlock bb, int i) {
lastRef(def, bb, i)
or
exists(ControlFlow::BasicBlock bb0, int i0 |
reachesLastRef(def, bb0, i0) and
variableRead(bb0, i0, _, any(ReadKind rk | rk.isPseudo())) and
adjacentDefPseudoRead(def, bb, i, bb0, i0)
)
}
@@ -1221,11 +1236,12 @@ private module Cached {
cached
predicate isLiveOutRefParameterDefinition(Ssa::Definition def, Parameter p) {
p.isOutOrRef() and
exists(Ssa::Definition def0, ControlFlow::BasicBlock bb, int i |
exists(Ssa::SourceVariable v, Ssa::Definition def0, ControlFlow::BasicBlock bb, int i |
v = def.getSourceVariable() and
p = v.getAssignable() and
def = def0.getAnUltimateDefinition() and
reachesLastRef(def0, bb, i) and
variableRead(bb, i, def0.getSourceVariable(), OutRefExitRead()) and
p = def0.getSourceVariable().getAssignable()
ssaDefReachesRead(_, def0, bb, i) and
outRefExitRead(bb, i, v)
)
}
}

View File

@@ -440,6 +440,28 @@ private module Cached {
defAdjacentRead(def, bb1, bb2, i2)
}
/**
* Holds if the node at index `i` in `bb` is a last reference to SSA definition
* `def`. The reference is last because it can reach another write `next`,
* without passing through another read or write.
*/
cached
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
// Next reference to `v` inside `bb` is a write
next.definesAt(v, bb, j) and
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
or
// Can reach a write using one or more steps
rnk = maxSsaRefRank(bb, v) and
exists(BasicBlock bb2 |
varBlockReaches(def, bb, bb2) and
next.definesAt(v, bb2, j) and
1 = ssaRefRank(bb2, j, v, SsaDef())
)
)
}
/**
* Holds if the node at index `i` in `bb` is a last reference to SSA
* definition `def`.
@@ -450,24 +472,16 @@ private module Cached {
*/
cached
predicate lastRef(Definition def, BasicBlock bb, int i) {
exists(int rnk, SourceVariable v | rnk = ssaDefRank(def, v, bb, i, _) |
// Next reference to `v` inside `bb` is a write
rnk + 1 = ssaRefRank(bb, _, v, SsaDef())
lastRefRedef(def, bb, i, _)
or
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
// Can reach exit directly
bb instanceof ExitBasicBlock
or
// No more references to `v` inside `bb`
rnk = maxSsaRefRank(bb, v) and
(
// Can reach exit directly
bb instanceof ExitBasicBlock
or
exists(BasicBlock bb2 | varBlockReaches(def, bb, bb2) |
// Can reach a write using one or more steps
1 = ssaRefRank(bb2, _, def.getSourceVariable(), SsaDef())
or
// Can reach a block using one or more steps, where `def` is no longer live
not defOccursInBlock(def, bb2, _) and
not ssaDefReachesEndOfBlock(bb2, def, _)
)
// Can reach a block using one or more steps, where `def` is no longer live
exists(BasicBlock bb2 | varBlockReaches(def, bb, bb2) |
not defOccursInBlock(def, bb2, _) and
not ssaDefReachesEndOfBlock(bb2, def, _)
)
)
}

View File

@@ -417,8 +417,8 @@
| LocalDataFlow.cs:367:23:367:24 | b1 | LocalDataFlow.cs:371:13:371:14 | access to parameter b1 |
| LocalDataFlow.cs:367:32:367:33 | b2 | LocalDataFlow.cs:374:17:374:18 | access to parameter b2 |
| LocalDataFlow.cs:373:13:373:25 | SSA def(x) | LocalDataFlow.cs:376:35:376:35 | access to local variable x |
| LocalDataFlow.cs:373:13:373:25 | SSA def(x) | LocalDataFlow.cs:382:9:382:17 | SSA phi(x) |
| LocalDataFlow.cs:373:17:373:25 | "tainted" | LocalDataFlow.cs:373:13:373:25 | SSA def(x) |
| LocalDataFlow.cs:376:35:376:35 | access to local variable x | LocalDataFlow.cs:382:9:382:17 | SSA phi(x) |
| LocalDataFlow.cs:381:13:381:29 | SSA def(x) | LocalDataFlow.cs:382:9:382:17 | SSA phi(x) |
| LocalDataFlow.cs:381:17:381:29 | "not tainted" | LocalDataFlow.cs:381:13:381:29 | SSA def(x) |
| LocalDataFlow.cs:382:9:382:17 | SSA phi(x) | LocalDataFlow.cs:382:15:382:15 | access to local variable x |
@@ -702,7 +702,6 @@
| SSA.cs:154:13:154:13 | access to parameter t | SSA.cs:154:13:154:13 | (...) ... |
| SSA.cs:154:13:154:13 | access to parameter t | SSA.cs:155:25:155:25 | access to parameter t |
| SSA.cs:155:25:155:25 | SSA def(t) | SSA.cs:152:17:152:28 | SSA phi(t) |
| SSA.cs:155:25:155:25 | access to parameter t | SSA.cs:152:17:152:28 | SSA phi(t) |
| SSA.cs:166:10:166:13 | this | SSA.cs:166:19:166:22 | this access |
| SSA.cs:168:22:168:28 | tainted | SSA.cs:173:24:173:30 | access to parameter tainted |
| SSA.cs:168:35:168:35 | i | SSA.cs:171:13:171:13 | access to parameter i |
@@ -710,6 +709,7 @@
| SSA.cs:170:27:170:28 | "" | SSA.cs:170:16:170:28 | SSA def(ssaSink5) |
| SSA.cs:171:13:171:15 | SSA def(i) | SSA.cs:174:20:174:20 | SSA phi(i) |
| SSA.cs:173:13:173:30 | SSA def(ssaSink5) | SSA.cs:176:21:176:28 | access to local variable ssaSink5 |
| SSA.cs:173:13:173:30 | SSA def(ssaSink5) | SSA.cs:180:9:180:24 | SSA phi(ssaSink5) |
| SSA.cs:173:24:173:30 | access to parameter tainted | SSA.cs:173:13:173:30 | SSA def(ssaSink5) |
| SSA.cs:174:20:174:20 | SSA phi(i) | SSA.cs:174:20:174:20 | access to parameter i |
| SSA.cs:174:20:174:22 | SSA def(i) | SSA.cs:174:20:174:20 | SSA phi(i) |

View File

@@ -527,8 +527,8 @@
| LocalDataFlow.cs:367:23:367:24 | b1 | LocalDataFlow.cs:371:13:371:14 | access to parameter b1 |
| LocalDataFlow.cs:367:32:367:33 | b2 | LocalDataFlow.cs:374:17:374:18 | access to parameter b2 |
| LocalDataFlow.cs:373:13:373:25 | SSA def(x) | LocalDataFlow.cs:376:35:376:35 | access to local variable x |
| LocalDataFlow.cs:373:13:373:25 | SSA def(x) | LocalDataFlow.cs:382:9:382:17 | SSA phi(x) |
| LocalDataFlow.cs:373:17:373:25 | "tainted" | LocalDataFlow.cs:373:13:373:25 | SSA def(x) |
| LocalDataFlow.cs:376:35:376:35 | access to local variable x | LocalDataFlow.cs:382:9:382:17 | SSA phi(x) |
| LocalDataFlow.cs:381:13:381:29 | SSA def(x) | LocalDataFlow.cs:382:9:382:17 | SSA phi(x) |
| LocalDataFlow.cs:381:17:381:29 | "not tainted" | LocalDataFlow.cs:381:13:381:29 | SSA def(x) |
| LocalDataFlow.cs:382:9:382:17 | SSA phi(x) | LocalDataFlow.cs:382:15:382:15 | access to local variable x |
@@ -828,7 +828,6 @@
| SSA.cs:154:13:154:13 | access to parameter t | SSA.cs:154:13:154:13 | (...) ... |
| SSA.cs:154:13:154:13 | access to parameter t | SSA.cs:155:25:155:25 | access to parameter t |
| SSA.cs:155:25:155:25 | SSA def(t) | SSA.cs:152:17:152:28 | SSA phi(t) |
| SSA.cs:155:25:155:25 | access to parameter t | SSA.cs:152:17:152:28 | SSA phi(t) |
| SSA.cs:166:10:166:13 | this | SSA.cs:166:19:166:22 | this access |
| SSA.cs:168:22:168:28 | tainted | SSA.cs:173:24:173:30 | access to parameter tainted |
| SSA.cs:168:35:168:35 | i | SSA.cs:171:13:171:13 | access to parameter i |
@@ -837,6 +836,7 @@
| SSA.cs:171:13:171:15 | ...-- | SSA.cs:171:13:171:19 | ... > ... |
| SSA.cs:171:13:171:15 | SSA def(i) | SSA.cs:174:20:174:20 | SSA phi(i) |
| SSA.cs:173:13:173:30 | SSA def(ssaSink5) | SSA.cs:176:21:176:28 | access to local variable ssaSink5 |
| SSA.cs:173:13:173:30 | SSA def(ssaSink5) | SSA.cs:180:9:180:24 | SSA phi(ssaSink5) |
| SSA.cs:173:24:173:30 | access to parameter tainted | SSA.cs:173:13:173:30 | SSA def(ssaSink5) |
| SSA.cs:174:20:174:20 | SSA phi(i) | SSA.cs:174:20:174:20 | access to parameter i |
| SSA.cs:174:20:174:22 | ...-- | SSA.cs:174:20:174:26 | ... > ... |