Java/C++/C#: flowCandFwdRead() refactor

This commit is contained in:
Tom Hvitved
2019-08-20 14:44:04 +02:00
parent 80e91cceb1
commit 7ab9c8b90d
18 changed files with 90 additions and 126 deletions

View File

@@ -1040,9 +1040,8 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
apf.headUsesContent(f)
)
or
exists(Content f, AccessPathFront apf0 |
flowCandFwdRead(f, node, fromArg, apf0, config) and
apf0.headUsesContent(f) and
exists(Content f |
flowCandFwdRead(f, node, fromArg, config) and
consCandFwd(f, apf, config)
)
}
@@ -1059,12 +1058,11 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
}
pragma[nomagic]
private predicate flowCandFwdRead(
Content f, Node node, boolean fromArg, AccessPathFront apf, Configuration config
) {
exists(Node mid |
private predicate flowCandFwdRead(Content f, Node node, boolean fromArg, Configuration config) {
exists(Node mid, AccessPathFront apf |
flowCandFwd(mid, fromArg, apf, config) and
read(mid, f, node) and
apf.headUsesContent(f) and
nodeCand(node, unbind(config))
)
}

View File

@@ -1040,9 +1040,8 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
apf.headUsesContent(f)
)
or
exists(Content f, AccessPathFront apf0 |
flowCandFwdRead(f, node, fromArg, apf0, config) and
apf0.headUsesContent(f) and
exists(Content f |
flowCandFwdRead(f, node, fromArg, config) and
consCandFwd(f, apf, config)
)
}
@@ -1059,12 +1058,11 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
}
pragma[nomagic]
private predicate flowCandFwdRead(
Content f, Node node, boolean fromArg, AccessPathFront apf, Configuration config
) {
exists(Node mid |
private predicate flowCandFwdRead(Content f, Node node, boolean fromArg, Configuration config) {
exists(Node mid, AccessPathFront apf |
flowCandFwd(mid, fromArg, apf, config) and
read(mid, f, node) and
apf.headUsesContent(f) and
nodeCand(node, unbind(config))
)
}

View File

@@ -1040,9 +1040,8 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
apf.headUsesContent(f)
)
or
exists(Content f, AccessPathFront apf0 |
flowCandFwdRead(f, node, fromArg, apf0, config) and
apf0.headUsesContent(f) and
exists(Content f |
flowCandFwdRead(f, node, fromArg, config) and
consCandFwd(f, apf, config)
)
}
@@ -1059,12 +1058,11 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
}
pragma[nomagic]
private predicate flowCandFwdRead(
Content f, Node node, boolean fromArg, AccessPathFront apf, Configuration config
) {
exists(Node mid |
private predicate flowCandFwdRead(Content f, Node node, boolean fromArg, Configuration config) {
exists(Node mid, AccessPathFront apf |
flowCandFwd(mid, fromArg, apf, config) and
read(mid, f, node) and
apf.headUsesContent(f) and
nodeCand(node, unbind(config))
)
}

View File

@@ -1040,9 +1040,8 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
apf.headUsesContent(f)
)
or
exists(Content f, AccessPathFront apf0 |
flowCandFwdRead(f, node, fromArg, apf0, config) and
apf0.headUsesContent(f) and
exists(Content f |
flowCandFwdRead(f, node, fromArg, config) and
consCandFwd(f, apf, config)
)
}
@@ -1059,12 +1058,11 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
}
pragma[nomagic]
private predicate flowCandFwdRead(
Content f, Node node, boolean fromArg, AccessPathFront apf, Configuration config
) {
exists(Node mid |
private predicate flowCandFwdRead(Content f, Node node, boolean fromArg, Configuration config) {
exists(Node mid, AccessPathFront apf |
flowCandFwd(mid, fromArg, apf, config) and
read(mid, f, node) and
apf.headUsesContent(f) and
nodeCand(node, unbind(config))
)
}

View File

@@ -1040,9 +1040,8 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
apf.headUsesContent(f)
)
or
exists(Content f, AccessPathFront apf0 |
flowCandFwdRead(f, node, fromArg, apf0, config) and
apf0.headUsesContent(f) and
exists(Content f |
flowCandFwdRead(f, node, fromArg, config) and
consCandFwd(f, apf, config)
)
}
@@ -1059,12 +1058,11 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
}
pragma[nomagic]
private predicate flowCandFwdRead(
Content f, Node node, boolean fromArg, AccessPathFront apf, Configuration config
) {
exists(Node mid |
private predicate flowCandFwdRead(Content f, Node node, boolean fromArg, Configuration config) {
exists(Node mid, AccessPathFront apf |
flowCandFwd(mid, fromArg, apf, config) and
read(mid, f, node) and
apf.headUsesContent(f) and
nodeCand(node, unbind(config))
)
}