mirror of
https://github.com/github/codeql.git
synced 2026-04-26 01:05:15 +02:00
Java/C++/C#: Sync.
This commit is contained in:
@@ -241,39 +241,36 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKind kind) {
|
||||
* Holds if `node` is reachable from a source in the given configuration
|
||||
* ignoring call contexts.
|
||||
*/
|
||||
private predicate nodeCandFwd1(Node node, boolean stored, Configuration config) {
|
||||
private predicate nodeCandFwd1(Node node, Configuration config) {
|
||||
not fullBarrier(node, config) and
|
||||
(
|
||||
config.isSource(node) and stored = false
|
||||
config.isSource(node)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
localFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalLocalFlowStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalLocalFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
jumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalJumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, _, node) and
|
||||
stored = true and
|
||||
not outBarrier(mid, config)
|
||||
)
|
||||
or
|
||||
@@ -281,26 +278,25 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, config) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node arg |
|
||||
nodeCandFwd1(arg, stored, config) and
|
||||
nodeCandFwd1(arg, config) and
|
||||
viableParamArg(_, node, arg)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
parameterValueFlowsToUpdate(p, mid) and
|
||||
viableParamArg(_, p, node.(PostUpdateNode).getPreUpdateNode())
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnNode ret, ReturnKind kind |
|
||||
nodeCandFwd1(ret, stored, config) and
|
||||
nodeCandFwd1(ret, config) and
|
||||
getReturnPosition(ret) = viableReturnPos(call, kind) and
|
||||
node = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -310,7 +306,7 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
pragma[nomagic]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -323,7 +319,7 @@ private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -336,66 +332,61 @@ private boolean unbindBool(boolean b) { result != b.booleanNot() }
|
||||
* configuration ignoring call contexts.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
nodeCandFwd1(node, false, config) and
|
||||
config.isSink(node) and
|
||||
stored = false
|
||||
private predicate nodeCand1(Node node, Configuration config) {
|
||||
nodeCandFwd1(node, config) and
|
||||
config.isSink(node)
|
||||
or
|
||||
nodeCandFwd1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
localFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalLocalFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
jumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalJumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, config) and
|
||||
(stored = false or stored = true)
|
||||
readCand1(f, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config) and
|
||||
stored = true
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node param |
|
||||
viableParamArg(_, param, node) and
|
||||
nodeCand1(param, stored, config)
|
||||
nodeCand1(param, config)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
parameterValueFlowsToUpdate(p, node) and
|
||||
viableParamArg(_, p, mid.getPreUpdateNode()) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnKind kind, OutNode out |
|
||||
nodeCand1(out, stored, config) and
|
||||
nodeCand1(out, config) and
|
||||
getReturnPosition(node) = viableReturnPos(call, kind) and
|
||||
out = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -409,24 +400,24 @@ pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(node, true, unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
nodeCand1(mid, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
@@ -493,7 +484,7 @@ pragma[noinline]
|
||||
private predicate simpleArgumentFlowsThrough0(
|
||||
DataFlowCall call, ArgumentNode arg, ReturnKind kind, DataFlowType t, Configuration config
|
||||
) {
|
||||
nodeCand1(arg, false, unbind(config)) and
|
||||
nodeCand1(arg, unbind(config)) and
|
||||
not outBarrier(arg, config) and
|
||||
exists(ParameterNode p, ReturnNode ret |
|
||||
simpleParameterFlow(p, ret, t, config) and
|
||||
@@ -513,7 +504,7 @@ private predicate simpleArgumentFlowsThrough(
|
||||
ArgumentNode arg, Node out, DataFlowType t, Configuration config
|
||||
) {
|
||||
exists(DataFlowCall call, ReturnKind kind |
|
||||
nodeCand1(out, false, unbind(config)) and
|
||||
nodeCand1(out, unbind(config)) and
|
||||
not inBarrier(out, config) and
|
||||
simpleArgumentFlowsThrough0(call, arg, kind, t, config) and
|
||||
out = getAnOutNode(call, kind)
|
||||
@@ -526,10 +517,10 @@ private predicate simpleArgumentFlowsThrough(
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate localFlowStepOrFlowThroughCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
localFlowStep(node1, node2, config)
|
||||
or
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
argumentValueFlowsThrough(node1, node2, _)
|
||||
}
|
||||
|
||||
@@ -542,7 +533,7 @@ pragma[noinline]
|
||||
private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
Node node1, Node node2, Configuration config
|
||||
) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
additionalLocalFlowStep(node1, node2, config)
|
||||
or
|
||||
simpleArgumentFlowsThrough(node1, node2, _, config)
|
||||
@@ -554,8 +545,8 @@ private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
* that this step is part of a path from a source to a sink.
|
||||
*/
|
||||
private predicate flowOutOfCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
(
|
||||
@@ -579,8 +570,8 @@ private predicate flowOutOfCallable(Node node1, Node node2, Configuration config
|
||||
*/
|
||||
private predicate flowIntoCallable(Node node1, Node node2, Configuration config) {
|
||||
viableParamArg(_, node2, node1) and
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config)
|
||||
}
|
||||
@@ -646,12 +637,12 @@ private predicate flowIntoCallable(
|
||||
* configuration taking simple call contexts into consideration.
|
||||
*/
|
||||
private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
config.isSource(node) and
|
||||
fromArg = false and
|
||||
stored = false
|
||||
or
|
||||
nodeCand1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, stored, config) and
|
||||
@@ -715,7 +706,7 @@ pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCand1(node, true, unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
nodeCandFwd2(mid, _, _, config) and
|
||||
store(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
|
||||
@@ -241,39 +241,36 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKind kind) {
|
||||
* Holds if `node` is reachable from a source in the given configuration
|
||||
* ignoring call contexts.
|
||||
*/
|
||||
private predicate nodeCandFwd1(Node node, boolean stored, Configuration config) {
|
||||
private predicate nodeCandFwd1(Node node, Configuration config) {
|
||||
not fullBarrier(node, config) and
|
||||
(
|
||||
config.isSource(node) and stored = false
|
||||
config.isSource(node)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
localFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalLocalFlowStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalLocalFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
jumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalJumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, _, node) and
|
||||
stored = true and
|
||||
not outBarrier(mid, config)
|
||||
)
|
||||
or
|
||||
@@ -281,26 +278,25 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, config) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node arg |
|
||||
nodeCandFwd1(arg, stored, config) and
|
||||
nodeCandFwd1(arg, config) and
|
||||
viableParamArg(_, node, arg)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
parameterValueFlowsToUpdate(p, mid) and
|
||||
viableParamArg(_, p, node.(PostUpdateNode).getPreUpdateNode())
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnNode ret, ReturnKind kind |
|
||||
nodeCandFwd1(ret, stored, config) and
|
||||
nodeCandFwd1(ret, config) and
|
||||
getReturnPosition(ret) = viableReturnPos(call, kind) and
|
||||
node = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -310,7 +306,7 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
pragma[nomagic]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -323,7 +319,7 @@ private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -336,66 +332,61 @@ private boolean unbindBool(boolean b) { result != b.booleanNot() }
|
||||
* configuration ignoring call contexts.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
nodeCandFwd1(node, false, config) and
|
||||
config.isSink(node) and
|
||||
stored = false
|
||||
private predicate nodeCand1(Node node, Configuration config) {
|
||||
nodeCandFwd1(node, config) and
|
||||
config.isSink(node)
|
||||
or
|
||||
nodeCandFwd1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
localFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalLocalFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
jumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalJumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, config) and
|
||||
(stored = false or stored = true)
|
||||
readCand1(f, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config) and
|
||||
stored = true
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node param |
|
||||
viableParamArg(_, param, node) and
|
||||
nodeCand1(param, stored, config)
|
||||
nodeCand1(param, config)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
parameterValueFlowsToUpdate(p, node) and
|
||||
viableParamArg(_, p, mid.getPreUpdateNode()) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnKind kind, OutNode out |
|
||||
nodeCand1(out, stored, config) and
|
||||
nodeCand1(out, config) and
|
||||
getReturnPosition(node) = viableReturnPos(call, kind) and
|
||||
out = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -409,24 +400,24 @@ pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(node, true, unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
nodeCand1(mid, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
@@ -493,7 +484,7 @@ pragma[noinline]
|
||||
private predicate simpleArgumentFlowsThrough0(
|
||||
DataFlowCall call, ArgumentNode arg, ReturnKind kind, DataFlowType t, Configuration config
|
||||
) {
|
||||
nodeCand1(arg, false, unbind(config)) and
|
||||
nodeCand1(arg, unbind(config)) and
|
||||
not outBarrier(arg, config) and
|
||||
exists(ParameterNode p, ReturnNode ret |
|
||||
simpleParameterFlow(p, ret, t, config) and
|
||||
@@ -513,7 +504,7 @@ private predicate simpleArgumentFlowsThrough(
|
||||
ArgumentNode arg, Node out, DataFlowType t, Configuration config
|
||||
) {
|
||||
exists(DataFlowCall call, ReturnKind kind |
|
||||
nodeCand1(out, false, unbind(config)) and
|
||||
nodeCand1(out, unbind(config)) and
|
||||
not inBarrier(out, config) and
|
||||
simpleArgumentFlowsThrough0(call, arg, kind, t, config) and
|
||||
out = getAnOutNode(call, kind)
|
||||
@@ -526,10 +517,10 @@ private predicate simpleArgumentFlowsThrough(
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate localFlowStepOrFlowThroughCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
localFlowStep(node1, node2, config)
|
||||
or
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
argumentValueFlowsThrough(node1, node2, _)
|
||||
}
|
||||
|
||||
@@ -542,7 +533,7 @@ pragma[noinline]
|
||||
private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
Node node1, Node node2, Configuration config
|
||||
) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
additionalLocalFlowStep(node1, node2, config)
|
||||
or
|
||||
simpleArgumentFlowsThrough(node1, node2, _, config)
|
||||
@@ -554,8 +545,8 @@ private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
* that this step is part of a path from a source to a sink.
|
||||
*/
|
||||
private predicate flowOutOfCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
(
|
||||
@@ -579,8 +570,8 @@ private predicate flowOutOfCallable(Node node1, Node node2, Configuration config
|
||||
*/
|
||||
private predicate flowIntoCallable(Node node1, Node node2, Configuration config) {
|
||||
viableParamArg(_, node2, node1) and
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config)
|
||||
}
|
||||
@@ -646,12 +637,12 @@ private predicate flowIntoCallable(
|
||||
* configuration taking simple call contexts into consideration.
|
||||
*/
|
||||
private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
config.isSource(node) and
|
||||
fromArg = false and
|
||||
stored = false
|
||||
or
|
||||
nodeCand1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, stored, config) and
|
||||
@@ -715,7 +706,7 @@ pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCand1(node, true, unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
nodeCandFwd2(mid, _, _, config) and
|
||||
store(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
|
||||
@@ -241,39 +241,36 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKind kind) {
|
||||
* Holds if `node` is reachable from a source in the given configuration
|
||||
* ignoring call contexts.
|
||||
*/
|
||||
private predicate nodeCandFwd1(Node node, boolean stored, Configuration config) {
|
||||
private predicate nodeCandFwd1(Node node, Configuration config) {
|
||||
not fullBarrier(node, config) and
|
||||
(
|
||||
config.isSource(node) and stored = false
|
||||
config.isSource(node)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
localFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalLocalFlowStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalLocalFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
jumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalJumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, _, node) and
|
||||
stored = true and
|
||||
not outBarrier(mid, config)
|
||||
)
|
||||
or
|
||||
@@ -281,26 +278,25 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, config) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node arg |
|
||||
nodeCandFwd1(arg, stored, config) and
|
||||
nodeCandFwd1(arg, config) and
|
||||
viableParamArg(_, node, arg)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
parameterValueFlowsToUpdate(p, mid) and
|
||||
viableParamArg(_, p, node.(PostUpdateNode).getPreUpdateNode())
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnNode ret, ReturnKind kind |
|
||||
nodeCandFwd1(ret, stored, config) and
|
||||
nodeCandFwd1(ret, config) and
|
||||
getReturnPosition(ret) = viableReturnPos(call, kind) and
|
||||
node = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -310,7 +306,7 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
pragma[nomagic]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -323,7 +319,7 @@ private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -336,66 +332,61 @@ private boolean unbindBool(boolean b) { result != b.booleanNot() }
|
||||
* configuration ignoring call contexts.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
nodeCandFwd1(node, false, config) and
|
||||
config.isSink(node) and
|
||||
stored = false
|
||||
private predicate nodeCand1(Node node, Configuration config) {
|
||||
nodeCandFwd1(node, config) and
|
||||
config.isSink(node)
|
||||
or
|
||||
nodeCandFwd1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
localFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalLocalFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
jumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalJumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, config) and
|
||||
(stored = false or stored = true)
|
||||
readCand1(f, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config) and
|
||||
stored = true
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node param |
|
||||
viableParamArg(_, param, node) and
|
||||
nodeCand1(param, stored, config)
|
||||
nodeCand1(param, config)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
parameterValueFlowsToUpdate(p, node) and
|
||||
viableParamArg(_, p, mid.getPreUpdateNode()) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnKind kind, OutNode out |
|
||||
nodeCand1(out, stored, config) and
|
||||
nodeCand1(out, config) and
|
||||
getReturnPosition(node) = viableReturnPos(call, kind) and
|
||||
out = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -409,24 +400,24 @@ pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(node, true, unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
nodeCand1(mid, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
@@ -493,7 +484,7 @@ pragma[noinline]
|
||||
private predicate simpleArgumentFlowsThrough0(
|
||||
DataFlowCall call, ArgumentNode arg, ReturnKind kind, DataFlowType t, Configuration config
|
||||
) {
|
||||
nodeCand1(arg, false, unbind(config)) and
|
||||
nodeCand1(arg, unbind(config)) and
|
||||
not outBarrier(arg, config) and
|
||||
exists(ParameterNode p, ReturnNode ret |
|
||||
simpleParameterFlow(p, ret, t, config) and
|
||||
@@ -513,7 +504,7 @@ private predicate simpleArgumentFlowsThrough(
|
||||
ArgumentNode arg, Node out, DataFlowType t, Configuration config
|
||||
) {
|
||||
exists(DataFlowCall call, ReturnKind kind |
|
||||
nodeCand1(out, false, unbind(config)) and
|
||||
nodeCand1(out, unbind(config)) and
|
||||
not inBarrier(out, config) and
|
||||
simpleArgumentFlowsThrough0(call, arg, kind, t, config) and
|
||||
out = getAnOutNode(call, kind)
|
||||
@@ -526,10 +517,10 @@ private predicate simpleArgumentFlowsThrough(
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate localFlowStepOrFlowThroughCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
localFlowStep(node1, node2, config)
|
||||
or
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
argumentValueFlowsThrough(node1, node2, _)
|
||||
}
|
||||
|
||||
@@ -542,7 +533,7 @@ pragma[noinline]
|
||||
private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
Node node1, Node node2, Configuration config
|
||||
) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
additionalLocalFlowStep(node1, node2, config)
|
||||
or
|
||||
simpleArgumentFlowsThrough(node1, node2, _, config)
|
||||
@@ -554,8 +545,8 @@ private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
* that this step is part of a path from a source to a sink.
|
||||
*/
|
||||
private predicate flowOutOfCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
(
|
||||
@@ -579,8 +570,8 @@ private predicate flowOutOfCallable(Node node1, Node node2, Configuration config
|
||||
*/
|
||||
private predicate flowIntoCallable(Node node1, Node node2, Configuration config) {
|
||||
viableParamArg(_, node2, node1) and
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config)
|
||||
}
|
||||
@@ -646,12 +637,12 @@ private predicate flowIntoCallable(
|
||||
* configuration taking simple call contexts into consideration.
|
||||
*/
|
||||
private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
config.isSource(node) and
|
||||
fromArg = false and
|
||||
stored = false
|
||||
or
|
||||
nodeCand1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, stored, config) and
|
||||
@@ -715,7 +706,7 @@ pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCand1(node, true, unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
nodeCandFwd2(mid, _, _, config) and
|
||||
store(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
|
||||
@@ -241,39 +241,36 @@ private ReturnPosition viableReturnPos(DataFlowCall call, ReturnKind kind) {
|
||||
* Holds if `node` is reachable from a source in the given configuration
|
||||
* ignoring call contexts.
|
||||
*/
|
||||
private predicate nodeCandFwd1(Node node, boolean stored, Configuration config) {
|
||||
private predicate nodeCandFwd1(Node node, Configuration config) {
|
||||
not fullBarrier(node, config) and
|
||||
(
|
||||
config.isSource(node) and stored = false
|
||||
config.isSource(node)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
localFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalLocalFlowStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalLocalFlowStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
jumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
stored = false
|
||||
nodeCandFwd1(mid, config) and
|
||||
additionalJumpStep(mid, node, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, _, node) and
|
||||
stored = true and
|
||||
not outBarrier(mid, config)
|
||||
)
|
||||
or
|
||||
@@ -281,26 +278,25 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, config) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node arg |
|
||||
nodeCandFwd1(arg, stored, config) and
|
||||
nodeCandFwd1(arg, config) and
|
||||
viableParamArg(_, node, arg)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
nodeCandFwd1(mid, stored, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
parameterValueFlowsToUpdate(p, mid) and
|
||||
viableParamArg(_, p, node.(PostUpdateNode).getPreUpdateNode())
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnNode ret, ReturnKind kind |
|
||||
nodeCandFwd1(ret, stored, config) and
|
||||
nodeCandFwd1(ret, config) and
|
||||
getReturnPosition(ret) = viableReturnPos(call, kind) and
|
||||
node = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -310,7 +306,7 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
pragma[nomagic]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -323,7 +319,7 @@ private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(mid, _, config) and
|
||||
nodeCandFwd1(mid, config) and
|
||||
store(mid, f, node)
|
||||
)
|
||||
}
|
||||
@@ -336,66 +332,61 @@ private boolean unbindBool(boolean b) { result != b.booleanNot() }
|
||||
* configuration ignoring call contexts.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
nodeCandFwd1(node, false, config) and
|
||||
config.isSink(node) and
|
||||
stored = false
|
||||
private predicate nodeCand1(Node node, Configuration config) {
|
||||
nodeCandFwd1(node, config) and
|
||||
config.isSink(node)
|
||||
or
|
||||
nodeCandFwd1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
localFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalLocalFlowStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
jumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
exists(Node mid |
|
||||
additionalJumpStep(node, mid, config) and
|
||||
nodeCand1(mid, stored, config) and
|
||||
stored = false
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, config) and
|
||||
(stored = false or stored = true)
|
||||
readCand1(f, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config) and
|
||||
stored = true
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(Node param |
|
||||
viableParamArg(_, param, node) and
|
||||
nodeCand1(param, stored, config)
|
||||
nodeCand1(param, config)
|
||||
)
|
||||
or
|
||||
// flow out of an argument
|
||||
exists(PostUpdateNode mid, ParameterNode p |
|
||||
parameterValueFlowsToUpdate(p, node) and
|
||||
viableParamArg(_, p, mid.getPreUpdateNode()) and
|
||||
nodeCand1(mid, stored, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
exists(DataFlowCall call, ReturnKind kind, OutNode out |
|
||||
nodeCand1(out, stored, config) and
|
||||
nodeCand1(out, config) and
|
||||
getReturnPosition(node) = viableReturnPos(call, kind) and
|
||||
out = getAnOutNode(call, kind)
|
||||
)
|
||||
@@ -409,24 +400,24 @@ pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCandFwd1(node, true, unbind(config)) and
|
||||
nodeCandFwd1(node, unbind(config)) and
|
||||
read(node, f, mid) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
nodeCand1(mid, _, config)
|
||||
nodeCand1(mid, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
nodeCand1(mid, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
not fullBarrier(node, config) and
|
||||
not inBarrier(node, config) and
|
||||
not outBarrier(node, config)
|
||||
@@ -493,7 +484,7 @@ pragma[noinline]
|
||||
private predicate simpleArgumentFlowsThrough0(
|
||||
DataFlowCall call, ArgumentNode arg, ReturnKind kind, DataFlowType t, Configuration config
|
||||
) {
|
||||
nodeCand1(arg, false, unbind(config)) and
|
||||
nodeCand1(arg, unbind(config)) and
|
||||
not outBarrier(arg, config) and
|
||||
exists(ParameterNode p, ReturnNode ret |
|
||||
simpleParameterFlow(p, ret, t, config) and
|
||||
@@ -513,7 +504,7 @@ private predicate simpleArgumentFlowsThrough(
|
||||
ArgumentNode arg, Node out, DataFlowType t, Configuration config
|
||||
) {
|
||||
exists(DataFlowCall call, ReturnKind kind |
|
||||
nodeCand1(out, false, unbind(config)) and
|
||||
nodeCand1(out, unbind(config)) and
|
||||
not inBarrier(out, config) and
|
||||
simpleArgumentFlowsThrough0(call, arg, kind, t, config) and
|
||||
out = getAnOutNode(call, kind)
|
||||
@@ -526,10 +517,10 @@ private predicate simpleArgumentFlowsThrough(
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate localFlowStepOrFlowThroughCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
localFlowStep(node1, node2, config)
|
||||
or
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
argumentValueFlowsThrough(node1, node2, _)
|
||||
}
|
||||
|
||||
@@ -542,7 +533,7 @@ pragma[noinline]
|
||||
private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
Node node1, Node node2, Configuration config
|
||||
) {
|
||||
nodeCand1(node1, _, config) and
|
||||
nodeCand1(node1, config) and
|
||||
additionalLocalFlowStep(node1, node2, config)
|
||||
or
|
||||
simpleArgumentFlowsThrough(node1, node2, _, config)
|
||||
@@ -554,8 +545,8 @@ private predicate additionalLocalFlowStepOrFlowThroughCallable(
|
||||
* that this step is part of a path from a source to a sink.
|
||||
*/
|
||||
private predicate flowOutOfCallable(Node node1, Node node2, Configuration config) {
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config) and
|
||||
(
|
||||
@@ -579,8 +570,8 @@ private predicate flowOutOfCallable(Node node1, Node node2, Configuration config
|
||||
*/
|
||||
private predicate flowIntoCallable(Node node1, Node node2, Configuration config) {
|
||||
viableParamArg(_, node2, node1) and
|
||||
nodeCand1(node1, _, unbind(config)) and
|
||||
nodeCand1(node2, _, config) and
|
||||
nodeCand1(node1, unbind(config)) and
|
||||
nodeCand1(node2, config) and
|
||||
not outBarrier(node1, config) and
|
||||
not inBarrier(node2, config)
|
||||
}
|
||||
@@ -646,12 +637,12 @@ private predicate flowIntoCallable(
|
||||
* configuration taking simple call contexts into consideration.
|
||||
*/
|
||||
private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
nodeCand1(node, config) and
|
||||
config.isSource(node) and
|
||||
fromArg = false and
|
||||
stored = false
|
||||
or
|
||||
nodeCand1(node, unbindBool(stored), unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
(
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, stored, config) and
|
||||
@@ -715,7 +706,7 @@ pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
nodeCand1(node, true, unbind(config)) and
|
||||
nodeCand1(node, unbind(config)) and
|
||||
nodeCandFwd2(mid, _, _, config) and
|
||||
store(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
|
||||
Reference in New Issue
Block a user