hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-30 19:26:02 +02:00
Code Issues Packages Projects Releases Wiki Activity

Data flow: Tweak two join-orders

Browse Source 
Before
```
[2022-04-06 13:19:29] (96s) Tuple counts for DataFlowImpl2::Stage1::revFlowConsCand#7ad53399#ff/2@i14#aa10f2wi after 4.4s:
                      10681    ~0%     {2} r1 = SCAN DataFlowImpl2::Stage1::revFlow#7ad53399#fff#prev_delta OUTPUT In.0, In.2 'config'
                      982      ~1%     {3} r2 = JOIN r1 WITH DataFlowImpl2::readSet#7ad53399#ffff_2301#join_rhs ON FIRST 2 OUTPUT Rhs.3, Lhs.1 'config', Rhs.2
                      83691528 ~2%     {3} r3 = JOIN r2 WITH DataFlowPublic::ContentSet::getAReadContent#dispred#f0820431#ff ON FIRST 1 OUTPUT Lhs.1 'config', Lhs.2, Rhs.1 'c'
                      83581763 ~2%     {3} r4 = r3 AND NOT DataFlowImpl2::Stage1::revFlowConsCand#7ad53399#ff#prev(Lhs.2 'c', Lhs.0 'config')
                      83581763 ~0%     {3} r5 = SCAN r4 OUTPUT In.2 'c', In.0 'config', In.1
                      0        ~0%     {3} r6 = JOIN r5 WITH DataFlowImpl2::Stage1::fwdFlowConsCand#7ad53399#ff ON FIRST 2 OUTPUT Lhs.2, Lhs.1 'config', Lhs.0 'c'
                      0        ~0%     {2} r7 = JOIN r6 WITH DataFlowImpl2::Stage1::fwdFlow#7ad53399#2#fff_02#join_rhs ON FIRST 2 OUTPUT Lhs.2 'c', Lhs.1 'config'
                                       return r7
```

After
```
[2022-04-06 13:44:38] (6s) Tuple counts for DataFlowImpl2::Stage1::revFlowConsCand#7ad53399#ff/2@i14#5abbf2wn after 6ms:
                      10681  ~0%     {2} r1 = SCAN DataFlowImpl2::Stage1::revFlow#7ad53399#fff#prev_delta OUTPUT In.0, In.2 'config'
                      982    ~1%     {3} r2 = JOIN r1 WITH DataFlowImpl2::readSet#7ad53399#ffff_2301#join_rhs ON FIRST 2 OUTPUT Rhs.3, Lhs.1 'config', Rhs.2
                      109765 ~0%     {3} r3 = JOIN r2 WITH DataFlowImpl2::Stage1::fwdFlowConsCandSet#7ad53399#fff#reorder_0_2_1 ON FIRST 2 OUTPUT Lhs.1 'config', Lhs.2, Rhs.2 'c'
                      0      ~0%     {3} r4 = r3 AND NOT DataFlowImpl2::Stage1::revFlowConsCand#7ad53399#ff#prev(Lhs.2 'c', Lhs.0 'config')
                      0      ~0%     {3} r5 = SCAN r4 OUTPUT In.1, In.0 'config', In.2 'c'
                      0      ~0%     {2} r6 = JOIN r5 WITH DataFlowImpl2::Stage1::fwdFlow#7ad53399#2#fff_02#join_rhs ON FIRST 2 OUTPUT Lhs.2 'c', Lhs.1 'config'
                                     return r6
```
This commit is contained in:
Tom Hvitved
2022-04-06 13:52:30 +02:00
parent cee527e03a
commit 4099d1318f
29 changed files with 377 additions and 348 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}

25
java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll
View File

@@ -648,7 +648,7 @@ private module Stage1 {
// read
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, config)
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -693,12 +693,13 @@ private module Stage1 {
}
/**
* Holds if `c` may be interpreted in a read as the target of some store,
* in the flow covered by `fwdFlow`.
* Holds if `cs` may be interpreted in a read as the target of some store
* into `c`, in the flow covered by `fwdFlow`.
*/
pragma[nomagic]
private predicate fwdFlowConsCandSet(ContentSet c, Configuration config) {
fwdFlowConsCand(c.getAReadContent(), config)
private predicate fwdFlowConsCandSet(ContentSet cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
@@ -795,7 +796,7 @@ private module Stage1 {
// read
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -821,10 +822,10 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowConsCand(Content c, Configuration config) {
exists(NodeEx mid, NodeEx node |
exists(NodeEx mid, NodeEx node, ContentSet cs |
fwdFlow(node, pragma[only_bind_into](config)) and
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
readSet(node, cs, mid, config) and
fwdFlowConsCandSet(cs, c, pragma[only_bind_into](config)) and
revFlow(pragma[only_bind_into](mid), _, pragma[only_bind_into](config))
)
}
@@ -840,7 +841,7 @@ private module Stage1 {
) {
exists(NodeEx mid |
revFlow(mid, toReturn, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, pragma[only_bind_into](config)) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
storeSet(node, c, mid, _, _, config)
)
}
@@ -851,9 +852,9 @@ private module Stage1 {
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowConsCand(c, pragma[only_bind_into](conf)) and
exists(ContentSet cs |
revFlowStoreSet(cs, _, _, conf) and
revFlowStoreSet(cs, _, _, pragma[only_bind_into](conf)) and
c = cs.getAStoreContent()
)
}