Data flow: Sync files

This commit is contained in:
Tom Hvitved
2020-06-23 10:54:29 +02:00
parent 98ed2a18ac
commit ff751ac0f8
18 changed files with 288 additions and 288 deletions

View File

@@ -1051,8 +1051,12 @@ private predicate flowIntoCallNodeCand2(
}
private module LocalFlowBigStep {
private class BigStepBarrierNode extends Node {
BigStepBarrierNode() {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends Node {
FlowCheckNode() {
this instanceof CastNode or
clearsContent(this, _)
}
@@ -1072,7 +1076,7 @@ private module LocalFlowBigStep {
node instanceof OutNodeExt or
store(_, _, node, _) or
read(_, _, node) or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
)
}
@@ -1090,7 +1094,7 @@ private module LocalFlowBigStep {
read(node, _, next)
)
or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
or
config.isSink(node)
}
@@ -1134,14 +1138,14 @@ private module LocalFlowBigStep {
exists(Node mid |
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
localFlowStepNodeCand1(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
nodeCand2(node2, unbind(config))
)
or
exists(Node mid |
localFlowStepPlus(node1, mid, _, _, config, cc) and
additionalLocalFlowStepNodeCand2(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
preservesValue = false and
t = getErasedNodeTypeBound(node2) and
nodeCand2(node2, unbind(config))
@@ -1197,6 +1201,7 @@ private predicate flowCandFwd(
Configuration config
) {
flowCandFwd0(node, fromArg, argApf, apf, config) and
not apf.isClearedAt(node) and
if node instanceof CastingNode
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
else any()
@@ -1215,8 +1220,7 @@ private predicate flowCandFwd0(
or
exists(Node mid |
flowCandFwd(mid, fromArg, argApf, apf, config) and
localFlowBigStep(mid, node, true, _, config, _) and
not apf.isClearedAt(node)
localFlowBigStep(mid, node, true, _, config, _)
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1229,8 +1233,7 @@ private predicate flowCandFwd0(
nodeCand2(node, unbind(config)) and
jumpStep(mid, node, config) and
fromArg = false and
argApf = TAccessPathFrontNone() and
not apf.isClearedAt(node)
argApf = TAccessPathFrontNone()
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1255,8 +1258,7 @@ private predicate flowCandFwd0(
exists(TypedContent tc |
flowCandFwdRead(tc, node, fromArg, argApf, config) and
flowCandFwdConsCand(tc, apf, config) and
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config)) and
not apf.isClearedAt(node)
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config))
)
or
// flow into a callable
@@ -1312,8 +1314,7 @@ private predicate flowCandFwdIn(
) {
exists(ArgumentNode arg, boolean allowsFieldFlow |
flowCandFwd(arg, fromArg, argApf, apf, config) and
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config) and
not apf.isClearedAt(p)
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)
@@ -1326,8 +1327,7 @@ private predicate flowCandFwdOut(
) {
exists(ReturnNodeExt ret, boolean allowsFieldFlow |
flowCandFwd(ret, fromArg, argApf, apf, config) and
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config) and
not apf.isClearedAt(node)
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)

View File

@@ -1051,8 +1051,12 @@ private predicate flowIntoCallNodeCand2(
}
private module LocalFlowBigStep {
private class BigStepBarrierNode extends Node {
BigStepBarrierNode() {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends Node {
FlowCheckNode() {
this instanceof CastNode or
clearsContent(this, _)
}
@@ -1072,7 +1076,7 @@ private module LocalFlowBigStep {
node instanceof OutNodeExt or
store(_, _, node, _) or
read(_, _, node) or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
)
}
@@ -1090,7 +1094,7 @@ private module LocalFlowBigStep {
read(node, _, next)
)
or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
or
config.isSink(node)
}
@@ -1134,14 +1138,14 @@ private module LocalFlowBigStep {
exists(Node mid |
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
localFlowStepNodeCand1(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
nodeCand2(node2, unbind(config))
)
or
exists(Node mid |
localFlowStepPlus(node1, mid, _, _, config, cc) and
additionalLocalFlowStepNodeCand2(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
preservesValue = false and
t = getErasedNodeTypeBound(node2) and
nodeCand2(node2, unbind(config))
@@ -1197,6 +1201,7 @@ private predicate flowCandFwd(
Configuration config
) {
flowCandFwd0(node, fromArg, argApf, apf, config) and
not apf.isClearedAt(node) and
if node instanceof CastingNode
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
else any()
@@ -1215,8 +1220,7 @@ private predicate flowCandFwd0(
or
exists(Node mid |
flowCandFwd(mid, fromArg, argApf, apf, config) and
localFlowBigStep(mid, node, true, _, config, _) and
not apf.isClearedAt(node)
localFlowBigStep(mid, node, true, _, config, _)
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1229,8 +1233,7 @@ private predicate flowCandFwd0(
nodeCand2(node, unbind(config)) and
jumpStep(mid, node, config) and
fromArg = false and
argApf = TAccessPathFrontNone() and
not apf.isClearedAt(node)
argApf = TAccessPathFrontNone()
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1255,8 +1258,7 @@ private predicate flowCandFwd0(
exists(TypedContent tc |
flowCandFwdRead(tc, node, fromArg, argApf, config) and
flowCandFwdConsCand(tc, apf, config) and
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config)) and
not apf.isClearedAt(node)
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config))
)
or
// flow into a callable
@@ -1312,8 +1314,7 @@ private predicate flowCandFwdIn(
) {
exists(ArgumentNode arg, boolean allowsFieldFlow |
flowCandFwd(arg, fromArg, argApf, apf, config) and
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config) and
not apf.isClearedAt(p)
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)
@@ -1326,8 +1327,7 @@ private predicate flowCandFwdOut(
) {
exists(ReturnNodeExt ret, boolean allowsFieldFlow |
flowCandFwd(ret, fromArg, argApf, apf, config) and
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config) and
not apf.isClearedAt(node)
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)

View File

@@ -1051,8 +1051,12 @@ private predicate flowIntoCallNodeCand2(
}
private module LocalFlowBigStep {
private class BigStepBarrierNode extends Node {
BigStepBarrierNode() {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends Node {
FlowCheckNode() {
this instanceof CastNode or
clearsContent(this, _)
}
@@ -1072,7 +1076,7 @@ private module LocalFlowBigStep {
node instanceof OutNodeExt or
store(_, _, node, _) or
read(_, _, node) or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
)
}
@@ -1090,7 +1094,7 @@ private module LocalFlowBigStep {
read(node, _, next)
)
or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
or
config.isSink(node)
}
@@ -1134,14 +1138,14 @@ private module LocalFlowBigStep {
exists(Node mid |
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
localFlowStepNodeCand1(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
nodeCand2(node2, unbind(config))
)
or
exists(Node mid |
localFlowStepPlus(node1, mid, _, _, config, cc) and
additionalLocalFlowStepNodeCand2(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
preservesValue = false and
t = getErasedNodeTypeBound(node2) and
nodeCand2(node2, unbind(config))
@@ -1197,6 +1201,7 @@ private predicate flowCandFwd(
Configuration config
) {
flowCandFwd0(node, fromArg, argApf, apf, config) and
not apf.isClearedAt(node) and
if node instanceof CastingNode
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
else any()
@@ -1215,8 +1220,7 @@ private predicate flowCandFwd0(
or
exists(Node mid |
flowCandFwd(mid, fromArg, argApf, apf, config) and
localFlowBigStep(mid, node, true, _, config, _) and
not apf.isClearedAt(node)
localFlowBigStep(mid, node, true, _, config, _)
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1229,8 +1233,7 @@ private predicate flowCandFwd0(
nodeCand2(node, unbind(config)) and
jumpStep(mid, node, config) and
fromArg = false and
argApf = TAccessPathFrontNone() and
not apf.isClearedAt(node)
argApf = TAccessPathFrontNone()
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1255,8 +1258,7 @@ private predicate flowCandFwd0(
exists(TypedContent tc |
flowCandFwdRead(tc, node, fromArg, argApf, config) and
flowCandFwdConsCand(tc, apf, config) and
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config)) and
not apf.isClearedAt(node)
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config))
)
or
// flow into a callable
@@ -1312,8 +1314,7 @@ private predicate flowCandFwdIn(
) {
exists(ArgumentNode arg, boolean allowsFieldFlow |
flowCandFwd(arg, fromArg, argApf, apf, config) and
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config) and
not apf.isClearedAt(p)
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)
@@ -1326,8 +1327,7 @@ private predicate flowCandFwdOut(
) {
exists(ReturnNodeExt ret, boolean allowsFieldFlow |
flowCandFwd(ret, fromArg, argApf, apf, config) and
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config) and
not apf.isClearedAt(node)
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)

View File

@@ -1051,8 +1051,12 @@ private predicate flowIntoCallNodeCand2(
}
private module LocalFlowBigStep {
private class BigStepBarrierNode extends Node {
BigStepBarrierNode() {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends Node {
FlowCheckNode() {
this instanceof CastNode or
clearsContent(this, _)
}
@@ -1072,7 +1076,7 @@ private module LocalFlowBigStep {
node instanceof OutNodeExt or
store(_, _, node, _) or
read(_, _, node) or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
)
}
@@ -1090,7 +1094,7 @@ private module LocalFlowBigStep {
read(node, _, next)
)
or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
or
config.isSink(node)
}
@@ -1134,14 +1138,14 @@ private module LocalFlowBigStep {
exists(Node mid |
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
localFlowStepNodeCand1(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
nodeCand2(node2, unbind(config))
)
or
exists(Node mid |
localFlowStepPlus(node1, mid, _, _, config, cc) and
additionalLocalFlowStepNodeCand2(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
preservesValue = false and
t = getErasedNodeTypeBound(node2) and
nodeCand2(node2, unbind(config))
@@ -1197,6 +1201,7 @@ private predicate flowCandFwd(
Configuration config
) {
flowCandFwd0(node, fromArg, argApf, apf, config) and
not apf.isClearedAt(node) and
if node instanceof CastingNode
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
else any()
@@ -1215,8 +1220,7 @@ private predicate flowCandFwd0(
or
exists(Node mid |
flowCandFwd(mid, fromArg, argApf, apf, config) and
localFlowBigStep(mid, node, true, _, config, _) and
not apf.isClearedAt(node)
localFlowBigStep(mid, node, true, _, config, _)
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1229,8 +1233,7 @@ private predicate flowCandFwd0(
nodeCand2(node, unbind(config)) and
jumpStep(mid, node, config) and
fromArg = false and
argApf = TAccessPathFrontNone() and
not apf.isClearedAt(node)
argApf = TAccessPathFrontNone()
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1255,8 +1258,7 @@ private predicate flowCandFwd0(
exists(TypedContent tc |
flowCandFwdRead(tc, node, fromArg, argApf, config) and
flowCandFwdConsCand(tc, apf, config) and
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config)) and
not apf.isClearedAt(node)
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config))
)
or
// flow into a callable
@@ -1312,8 +1314,7 @@ private predicate flowCandFwdIn(
) {
exists(ArgumentNode arg, boolean allowsFieldFlow |
flowCandFwd(arg, fromArg, argApf, apf, config) and
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config) and
not apf.isClearedAt(p)
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)
@@ -1326,8 +1327,7 @@ private predicate flowCandFwdOut(
) {
exists(ReturnNodeExt ret, boolean allowsFieldFlow |
flowCandFwd(ret, fromArg, argApf, apf, config) and
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config) and
not apf.isClearedAt(node)
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)

View File

@@ -1051,8 +1051,12 @@ private predicate flowIntoCallNodeCand2(
}
private module LocalFlowBigStep {
private class BigStepBarrierNode extends Node {
BigStepBarrierNode() {
/**
* A node where some checking is required, and hence the big-step relation
* is not allowed to step over.
*/
private class FlowCheckNode extends Node {
FlowCheckNode() {
this instanceof CastNode or
clearsContent(this, _)
}
@@ -1072,7 +1076,7 @@ private module LocalFlowBigStep {
node instanceof OutNodeExt or
store(_, _, node, _) or
read(_, _, node) or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
)
}
@@ -1090,7 +1094,7 @@ private module LocalFlowBigStep {
read(node, _, next)
)
or
node instanceof BigStepBarrierNode
node instanceof FlowCheckNode
or
config.isSink(node)
}
@@ -1134,14 +1138,14 @@ private module LocalFlowBigStep {
exists(Node mid |
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
localFlowStepNodeCand1(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
nodeCand2(node2, unbind(config))
)
or
exists(Node mid |
localFlowStepPlus(node1, mid, _, _, config, cc) and
additionalLocalFlowStepNodeCand2(mid, node2, config) and
not mid instanceof BigStepBarrierNode and
not mid instanceof FlowCheckNode and
preservesValue = false and
t = getErasedNodeTypeBound(node2) and
nodeCand2(node2, unbind(config))
@@ -1197,6 +1201,7 @@ private predicate flowCandFwd(
Configuration config
) {
flowCandFwd0(node, fromArg, argApf, apf, config) and
not apf.isClearedAt(node) and
if node instanceof CastingNode
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
else any()
@@ -1215,8 +1220,7 @@ private predicate flowCandFwd0(
or
exists(Node mid |
flowCandFwd(mid, fromArg, argApf, apf, config) and
localFlowBigStep(mid, node, true, _, config, _) and
not apf.isClearedAt(node)
localFlowBigStep(mid, node, true, _, config, _)
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1229,8 +1233,7 @@ private predicate flowCandFwd0(
nodeCand2(node, unbind(config)) and
jumpStep(mid, node, config) and
fromArg = false and
argApf = TAccessPathFrontNone() and
not apf.isClearedAt(node)
argApf = TAccessPathFrontNone()
)
or
exists(Node mid, AccessPathFrontNil nil |
@@ -1255,8 +1258,7 @@ private predicate flowCandFwd0(
exists(TypedContent tc |
flowCandFwdRead(tc, node, fromArg, argApf, config) and
flowCandFwdConsCand(tc, apf, config) and
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config)) and
not apf.isClearedAt(node)
nodeCand2(node, _, _, unbindBool(apf.toBoolNonEmpty()), unbind(config))
)
or
// flow into a callable
@@ -1312,8 +1314,7 @@ private predicate flowCandFwdIn(
) {
exists(ArgumentNode arg, boolean allowsFieldFlow |
flowCandFwd(arg, fromArg, argApf, apf, config) and
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config) and
not apf.isClearedAt(p)
flowIntoCallNodeCand2(call, arg, p, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)
@@ -1326,8 +1327,7 @@ private predicate flowCandFwdOut(
) {
exists(ReturnNodeExt ret, boolean allowsFieldFlow |
flowCandFwd(ret, fromArg, argApf, apf, config) and
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config) and
not apf.isClearedAt(node)
flowOutOfCallNodeCand2(call, ret, node, allowsFieldFlow, config)
|
apf instanceof AccessPathFrontNil or allowsFieldFlow = true
)