Dataflow: Sync.

This commit is contained in:
Anders Schack-Mulligen
2022-04-08 13:50:01 +02:00
parent 4ae59b530b
commit b521d64156
45 changed files with 280 additions and 1740 deletions

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -87,21 +87,9 @@ abstract class Configuration extends string {
/** Holds if data flow into `node` is prohibited. */
predicate isBarrierIn(Node node) { none() }
/**
* Holds if data flow into `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierIn(Node node, FlowState state) { none() }
/** Holds if data flow out of `node` is prohibited. */
predicate isBarrierOut(Node node) { none() }
/**
* Holds if data flow out of `node` is prohibited when the flow state is
* `state`
*/
predicate isBarrierOut(Node node, FlowState state) { none() }
/** Holds if data flow through nodes guarded by `guard` is prohibited. */
predicate isBarrierGuard(BarrierGuard guard) { none() }
@@ -321,7 +309,7 @@ private class RetNodeEx extends NodeEx {
ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
}
private predicate fullInBarrier(NodeEx node, Configuration config) {
private predicate inBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n)
@@ -330,16 +318,7 @@ private predicate fullInBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateInBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierIn(n, state)
|
config.isSource(n, state)
)
}
private predicate fullOutBarrier(NodeEx node, Configuration config) {
private predicate outBarrier(NodeEx node, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n)
@@ -348,15 +327,6 @@ private predicate fullOutBarrier(NodeEx node, Configuration config) {
)
}
private predicate stateOutBarrier(NodeEx node, FlowState state, Configuration config) {
exists(Node n |
node.asNode() = n and
config.isBarrierOut(n, state)
|
config.isSink(n, state)
)
}
pragma[nomagic]
private predicate fullBarrier(NodeEx node, Configuration config) {
exists(Node n | node.asNode() = n |
@@ -382,12 +352,6 @@ private predicate stateBarrier(NodeEx node, FlowState state, Configuration confi
exists(Node n | node.asNode() = n |
config.isBarrier(n, state)
or
config.isBarrierIn(n, state) and
not config.isSource(n, state)
or
config.isBarrierOut(n, state) and
not config.isSink(n, state)
or
exists(BarrierGuard g |
config.isBarrierGuard(g, state) and
n = g.getAGuardedNode()
@@ -420,8 +384,8 @@ private predicate sinkNode(NodeEx node, FlowState state, Configuration config) {
/** Provides the relevant barriers for a step from `node1` to `node2`. */
pragma[inline]
private predicate stepFilter(NodeEx node1, NodeEx node2, Configuration config) {
not fullOutBarrier(node1, config) and
not fullInBarrier(node2, config) and
not outBarrier(node1, config) and
not inBarrier(node2, config) and
not fullBarrier(node1, config) and
not fullBarrier(node2, config)
}
@@ -474,8 +438,6 @@ private predicate additionalLocalStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config)
)
@@ -517,8 +479,6 @@ private predicate additionalJumpStateStep(
config.isAdditionalFlowStep(n1, s1, n2, s2) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stepFilter(node1, node2, config) and
not stateOutBarrier(node1, s1, config) and
not stateInBarrier(node2, s2, config) and
not stateBarrier(node1, s1, config) and
not stateBarrier(node2, s2, config) and
not config.getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -918,8 +878,8 @@ private module Stage1 {
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
revFlow(node, true, config) and
fwdFlow(node, true, config) and
not fullInBarrier(node, config) and
not fullOutBarrier(node, config)
not inBarrier(node, config) and
not outBarrier(node, config)
}
/** Holds if flow may return from `callable`. */
@@ -1014,8 +974,8 @@ private predicate flowOutOfCallNodeCand1(
) {
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
Stage1::revFlow(ret, config) and
not fullOutBarrier(ret, config) and
not fullInBarrier(out, config)
not outBarrier(ret, config) and
not inBarrier(out, config)
}
pragma[nomagic]
@@ -1036,8 +996,8 @@ private predicate flowIntoCallNodeCand1(
) {
viableParamArgNodeCand1(call, p, arg, config) and
Stage1::revFlow(p, config) and
not fullOutBarrier(arg, config) and
not fullInBarrier(p, config)
not outBarrier(arg, config) and
not inBarrier(p, config)
}
/**

View File

@@ -109,16 +109,6 @@ abstract class Configuration extends DataFlow::Configuration {
/** Holds if taint propagation into `node` is prohibited. */
predicate isSanitizerIn(DataFlow::Node node) { none() }
/**
* Holds if taint propagation into `node` is prohibited when the flow state is
* `state`.
*/
predicate isSanitizerIn(DataFlow::Node node, DataFlow::FlowState state) { none() }
final override predicate isBarrierIn(DataFlow::Node node, DataFlow::FlowState state) {
this.isSanitizerIn(node, state)
}
final override predicate isBarrierIn(DataFlow::Node node) { this.isSanitizerIn(node) }
/** Holds if taint propagation out of `node` is prohibited. */
@@ -126,16 +116,6 @@ abstract class Configuration extends DataFlow::Configuration {
final override predicate isBarrierOut(DataFlow::Node node) { this.isSanitizerOut(node) }
/**
* Holds if taint propagation out of `node` is prohibited when the flow state is
* `state`.
*/
predicate isSanitizerOut(DataFlow::Node node, DataFlow::FlowState state) { none() }
final override predicate isBarrierOut(DataFlow::Node node, DataFlow::FlowState state) {
this.isSanitizerOut(node, state)
}
/** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }