Java/C++/C#: Improve performance of pruning in field flow.

This commit is contained in:
Anders Schack-Mulligen
2019-08-22 15:26:33 +02:00
parent 23b74b5521
commit 6e97f22b43

View File

@@ -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))