Data flow: Revert reordering changes in flowStore and flowRead

This commit is contained in:
Tom Hvitved
2019-12-02 14:25:59 +01:00
parent 5baa133e6c
commit b3990c5a1d
19 changed files with 76 additions and 76 deletions

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and

View File

@@ -1536,19 +1536,19 @@ private predicate flow0(Node node, boolean toReturn, AccessPath ap, Configuratio
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowStore(ap0, f, node, toReturn, config) and flowStore(node, f, toReturn, ap0, config) and
pop(ap0, f, ap) pop(ap0, f, ap)
) )
or or
exists(Content f, AccessPath ap0 | exists(Content f, AccessPath ap0 |
flowRead(f, ap0, node, toReturn, config) and flowRead(node, f, toReturn, ap0, config) and
push(ap0, f, ap) push(ap0, f, ap)
) )
} }
pragma[nomagic] pragma[nomagic]
private predicate flowStore( private predicate flowStore(
AccessPath ap0, Content f, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
store(node, f, mid) and store(node, f, mid) and
@@ -1558,7 +1558,7 @@ private predicate flowStore(
pragma[nomagic] pragma[nomagic]
private predicate flowRead( private predicate flowRead(
Content f, AccessPath ap0, Node node, boolean toReturn, Configuration config Node node, Content f, boolean toReturn, AccessPath ap0, Configuration config
) { ) {
exists(Node mid | exists(Node mid |
read(node, f, mid) and read(node, f, mid) and