Java: Fix pruning in partialPathStep.

This commit is contained in:
Anders Schack-Mulligen
2019-10-08 11:17:47 +02:00
parent bf14889077
commit 20084fb3c0
19 changed files with 247 additions and 190 deletions

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and

View File

@@ -2218,16 +2218,19 @@ private module FlowExploration {
private predicate partialPathStep(
PartialPathNodePriv mid, Node node, CallContext cc, PartialAccessPath ap, Configuration config
) {
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
not isUnreachableInCall(node, cc.(CallContextSpecificCall).getCall()) and
(
localFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
ap = mid.getAp() and
config = mid.getConfiguration()
or
additionalLocalFlowStep(mid.getNode(), node, config) and
cc = mid.getCallContext() and
mid.getAp() instanceof PartialAccessPathNil and
ap = TPartialNil(getErasedRepr(node.getType())) and
config = mid.getConfiguration()
)
or
jumpStep(mid.getNode(), node, config) and
cc instanceof CallContextAny and