mirror of
https://github.com/github/codeql.git
synced 2026-04-25 16:55:19 +02:00
Java/C++/C#: Improve data flow join orders for field flow
This commit is contained in:
@@ -257,9 +257,8 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
@@ -287,9 +286,18 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
@@ -337,10 +345,9 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, unbind(config)) and
|
||||
nodeCand1(mid, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -377,6 +384,7 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -387,6 +395,15 @@ private predicate readCand1(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
not fullBarrier(node, config) and
|
||||
@@ -648,9 +665,8 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd2Read(f, node, fromArg, config) and
|
||||
storeCandFwd2(f, unbind(config)) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
@@ -674,6 +690,7 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -684,6 +701,15 @@ private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd2Read(Content f, Node node, boolean fromArg, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is part of a path from a source to a sink in the given
|
||||
* configuration taking simple call contexts into consideration.
|
||||
@@ -721,10 +747,9 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand2Store(f, node, toReturn, config) and
|
||||
readCand2(f, unbind(config)) and
|
||||
nodeCand2(mid, toReturn, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -755,6 +780,7 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -765,16 +791,21 @@ private predicate readCand2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node n1, Node n2 |
|
||||
store(n1, f, n2) and
|
||||
nodeCand2(n1, _, _, conf) and
|
||||
nodeCand2(n2, _, _, unbind(conf))
|
||||
pragma[noinline]
|
||||
private predicate nodeCand2Store(Content f, Node node, boolean toReturn, Configuration config) {
|
||||
exists(Node mid |
|
||||
store(node, f, mid) and
|
||||
nodeCand2(mid, toReturn, true, config)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node node |
|
||||
nodeCand2Store(f, node, _, conf) and
|
||||
nodeCand2(node, _, _, unbind(conf))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of both a store and a read in the path graph
|
||||
@@ -783,7 +814,7 @@ private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[noinline]
|
||||
private predicate readStoreCand(Content f, Configuration conf) {
|
||||
storeCand(f, conf) and
|
||||
readCand(f, conf)
|
||||
readCand2(f, conf)
|
||||
}
|
||||
|
||||
private predicate nodeCand(Node node, Configuration config) { nodeCand2(node, _, _, config) }
|
||||
@@ -1009,15 +1040,14 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
|
||||
apf.headUsesContent(f)
|
||||
)
|
||||
or
|
||||
exists(Node mid, Content f, AccessPathFront apf0 |
|
||||
flowCandFwd(mid, fromArg, apf0, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, config) and
|
||||
exists(Content f, AccessPathFront apf0 |
|
||||
flowCandFwdRead(f, node, apf0, fromArg, config) and
|
||||
apf0.headUsesContent(f) and
|
||||
consCandFwd(f, apf, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCandFwd(Content f, AccessPathFront apf, Configuration config) {
|
||||
exists(Node mid, Node n |
|
||||
flowCandFwd(mid, _, apf, config) and
|
||||
@@ -1028,6 +1058,17 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandFwdRead(
|
||||
Content f, Node node, AccessPathFront apf, boolean fromArg, Configuration config
|
||||
) {
|
||||
exists(Node mid |
|
||||
flowCandFwd(mid, fromArg, apf, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from a source to `node` with the given `apf` and
|
||||
* from there flow to a sink.
|
||||
@@ -1118,6 +1159,7 @@ private predicate flowCandRead(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandStore(
|
||||
Node node, Content f, boolean toReturn, AccessPathFront apf0, Configuration config
|
||||
) {
|
||||
@@ -1127,6 +1169,7 @@ private predicate flowCandStore(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCand(Content f, AccessPathFront apf, Configuration config) {
|
||||
consCandFwd(f, apf, config) and
|
||||
exists(Node n, AccessPathFront apf0 |
|
||||
|
||||
@@ -257,9 +257,8 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
@@ -287,9 +286,18 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
@@ -337,10 +345,9 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, unbind(config)) and
|
||||
nodeCand1(mid, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -377,6 +384,7 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -387,6 +395,15 @@ private predicate readCand1(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
not fullBarrier(node, config) and
|
||||
@@ -648,9 +665,8 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd2Read(f, node, fromArg, config) and
|
||||
storeCandFwd2(f, unbind(config)) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
@@ -674,6 +690,7 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -684,6 +701,15 @@ private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd2Read(Content f, Node node, boolean fromArg, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is part of a path from a source to a sink in the given
|
||||
* configuration taking simple call contexts into consideration.
|
||||
@@ -721,10 +747,9 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand2Store(f, node, toReturn, config) and
|
||||
readCand2(f, unbind(config)) and
|
||||
nodeCand2(mid, toReturn, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -755,6 +780,7 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -765,16 +791,21 @@ private predicate readCand2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node n1, Node n2 |
|
||||
store(n1, f, n2) and
|
||||
nodeCand2(n1, _, _, conf) and
|
||||
nodeCand2(n2, _, _, unbind(conf))
|
||||
pragma[noinline]
|
||||
private predicate nodeCand2Store(Content f, Node node, boolean toReturn, Configuration config) {
|
||||
exists(Node mid |
|
||||
store(node, f, mid) and
|
||||
nodeCand2(mid, toReturn, true, config)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node node |
|
||||
nodeCand2Store(f, node, _, conf) and
|
||||
nodeCand2(node, _, _, unbind(conf))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of both a store and a read in the path graph
|
||||
@@ -783,7 +814,7 @@ private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[noinline]
|
||||
private predicate readStoreCand(Content f, Configuration conf) {
|
||||
storeCand(f, conf) and
|
||||
readCand(f, conf)
|
||||
readCand2(f, conf)
|
||||
}
|
||||
|
||||
private predicate nodeCand(Node node, Configuration config) { nodeCand2(node, _, _, config) }
|
||||
@@ -1009,15 +1040,14 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
|
||||
apf.headUsesContent(f)
|
||||
)
|
||||
or
|
||||
exists(Node mid, Content f, AccessPathFront apf0 |
|
||||
flowCandFwd(mid, fromArg, apf0, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, config) and
|
||||
exists(Content f, AccessPathFront apf0 |
|
||||
flowCandFwdRead(f, node, apf0, fromArg, config) and
|
||||
apf0.headUsesContent(f) and
|
||||
consCandFwd(f, apf, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCandFwd(Content f, AccessPathFront apf, Configuration config) {
|
||||
exists(Node mid, Node n |
|
||||
flowCandFwd(mid, _, apf, config) and
|
||||
@@ -1028,6 +1058,17 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandFwdRead(
|
||||
Content f, Node node, AccessPathFront apf, boolean fromArg, Configuration config
|
||||
) {
|
||||
exists(Node mid |
|
||||
flowCandFwd(mid, fromArg, apf, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from a source to `node` with the given `apf` and
|
||||
* from there flow to a sink.
|
||||
@@ -1118,6 +1159,7 @@ private predicate flowCandRead(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandStore(
|
||||
Node node, Content f, boolean toReturn, AccessPathFront apf0, Configuration config
|
||||
) {
|
||||
@@ -1127,6 +1169,7 @@ private predicate flowCandStore(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCand(Content f, AccessPathFront apf, Configuration config) {
|
||||
consCandFwd(f, apf, config) and
|
||||
exists(Node n, AccessPathFront apf0 |
|
||||
|
||||
@@ -257,9 +257,8 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
@@ -287,9 +286,18 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
@@ -337,10 +345,9 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, unbind(config)) and
|
||||
nodeCand1(mid, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -377,6 +384,7 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -387,6 +395,15 @@ private predicate readCand1(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
not fullBarrier(node, config) and
|
||||
@@ -648,9 +665,8 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd2Read(f, node, fromArg, config) and
|
||||
storeCandFwd2(f, unbind(config)) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
@@ -674,6 +690,7 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -684,6 +701,15 @@ private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd2Read(Content f, Node node, boolean fromArg, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is part of a path from a source to a sink in the given
|
||||
* configuration taking simple call contexts into consideration.
|
||||
@@ -721,10 +747,9 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand2Store(f, node, toReturn, config) and
|
||||
readCand2(f, unbind(config)) and
|
||||
nodeCand2(mid, toReturn, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -755,6 +780,7 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -765,16 +791,21 @@ private predicate readCand2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node n1, Node n2 |
|
||||
store(n1, f, n2) and
|
||||
nodeCand2(n1, _, _, conf) and
|
||||
nodeCand2(n2, _, _, unbind(conf))
|
||||
pragma[noinline]
|
||||
private predicate nodeCand2Store(Content f, Node node, boolean toReturn, Configuration config) {
|
||||
exists(Node mid |
|
||||
store(node, f, mid) and
|
||||
nodeCand2(mid, toReturn, true, config)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node node |
|
||||
nodeCand2Store(f, node, _, conf) and
|
||||
nodeCand2(node, _, _, unbind(conf))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of both a store and a read in the path graph
|
||||
@@ -783,7 +814,7 @@ private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[noinline]
|
||||
private predicate readStoreCand(Content f, Configuration conf) {
|
||||
storeCand(f, conf) and
|
||||
readCand(f, conf)
|
||||
readCand2(f, conf)
|
||||
}
|
||||
|
||||
private predicate nodeCand(Node node, Configuration config) { nodeCand2(node, _, _, config) }
|
||||
@@ -1009,15 +1040,14 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
|
||||
apf.headUsesContent(f)
|
||||
)
|
||||
or
|
||||
exists(Node mid, Content f, AccessPathFront apf0 |
|
||||
flowCandFwd(mid, fromArg, apf0, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, config) and
|
||||
exists(Content f, AccessPathFront apf0 |
|
||||
flowCandFwdRead(f, node, apf0, fromArg, config) and
|
||||
apf0.headUsesContent(f) and
|
||||
consCandFwd(f, apf, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCandFwd(Content f, AccessPathFront apf, Configuration config) {
|
||||
exists(Node mid, Node n |
|
||||
flowCandFwd(mid, _, apf, config) and
|
||||
@@ -1028,6 +1058,17 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandFwdRead(
|
||||
Content f, Node node, AccessPathFront apf, boolean fromArg, Configuration config
|
||||
) {
|
||||
exists(Node mid |
|
||||
flowCandFwd(mid, fromArg, apf, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from a source to `node` with the given `apf` and
|
||||
* from there flow to a sink.
|
||||
@@ -1118,6 +1159,7 @@ private predicate flowCandRead(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandStore(
|
||||
Node node, Content f, boolean toReturn, AccessPathFront apf0, Configuration config
|
||||
) {
|
||||
@@ -1127,6 +1169,7 @@ private predicate flowCandStore(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCand(Content f, AccessPathFront apf, Configuration config) {
|
||||
consCandFwd(f, apf, config) and
|
||||
exists(Node n, AccessPathFront apf0 |
|
||||
|
||||
@@ -257,9 +257,8 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
@@ -287,9 +286,18 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
@@ -337,10 +345,9 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, unbind(config)) and
|
||||
nodeCand1(mid, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -377,6 +384,7 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -387,6 +395,15 @@ private predicate readCand1(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
not fullBarrier(node, config) and
|
||||
@@ -648,9 +665,8 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd2Read(f, node, fromArg, config) and
|
||||
storeCandFwd2(f, unbind(config)) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
@@ -674,6 +690,7 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -684,6 +701,15 @@ private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd2Read(Content f, Node node, boolean fromArg, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is part of a path from a source to a sink in the given
|
||||
* configuration taking simple call contexts into consideration.
|
||||
@@ -721,10 +747,9 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand2Store(f, node, toReturn, config) and
|
||||
readCand2(f, unbind(config)) and
|
||||
nodeCand2(mid, toReturn, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -755,6 +780,7 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -765,16 +791,21 @@ private predicate readCand2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node n1, Node n2 |
|
||||
store(n1, f, n2) and
|
||||
nodeCand2(n1, _, _, conf) and
|
||||
nodeCand2(n2, _, _, unbind(conf))
|
||||
pragma[noinline]
|
||||
private predicate nodeCand2Store(Content f, Node node, boolean toReturn, Configuration config) {
|
||||
exists(Node mid |
|
||||
store(node, f, mid) and
|
||||
nodeCand2(mid, toReturn, true, config)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node node |
|
||||
nodeCand2Store(f, node, _, conf) and
|
||||
nodeCand2(node, _, _, unbind(conf))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of both a store and a read in the path graph
|
||||
@@ -783,7 +814,7 @@ private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[noinline]
|
||||
private predicate readStoreCand(Content f, Configuration conf) {
|
||||
storeCand(f, conf) and
|
||||
readCand(f, conf)
|
||||
readCand2(f, conf)
|
||||
}
|
||||
|
||||
private predicate nodeCand(Node node, Configuration config) { nodeCand2(node, _, _, config) }
|
||||
@@ -1009,15 +1040,14 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
|
||||
apf.headUsesContent(f)
|
||||
)
|
||||
or
|
||||
exists(Node mid, Content f, AccessPathFront apf0 |
|
||||
flowCandFwd(mid, fromArg, apf0, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, config) and
|
||||
exists(Content f, AccessPathFront apf0 |
|
||||
flowCandFwdRead(f, node, apf0, fromArg, config) and
|
||||
apf0.headUsesContent(f) and
|
||||
consCandFwd(f, apf, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCandFwd(Content f, AccessPathFront apf, Configuration config) {
|
||||
exists(Node mid, Node n |
|
||||
flowCandFwd(mid, _, apf, config) and
|
||||
@@ -1028,6 +1058,17 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandFwdRead(
|
||||
Content f, Node node, AccessPathFront apf, boolean fromArg, Configuration config
|
||||
) {
|
||||
exists(Node mid |
|
||||
flowCandFwd(mid, fromArg, apf, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from a source to `node` with the given `apf` and
|
||||
* from there flow to a sink.
|
||||
@@ -1118,6 +1159,7 @@ private predicate flowCandRead(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandStore(
|
||||
Node node, Content f, boolean toReturn, AccessPathFront apf0, Configuration config
|
||||
) {
|
||||
@@ -1127,6 +1169,7 @@ private predicate flowCandStore(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCand(Content f, AccessPathFront apf, Configuration config) {
|
||||
consCandFwd(f, apf, config) and
|
||||
exists(Node n, AccessPathFront apf0 |
|
||||
|
||||
@@ -257,9 +257,8 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd1Read(f, node, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
(stored = false or stored = true) and
|
||||
not inBarrier(node, config)
|
||||
@@ -287,9 +286,18 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd1Read(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd1(mid, true, config) and
|
||||
read(mid, f, node)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
not fullBarrier(node, config) and
|
||||
@@ -337,10 +345,9 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand1Store(f, node, config) and
|
||||
readCand1(f, unbind(config)) and
|
||||
nodeCand1(mid, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -377,6 +384,7 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand1(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -387,6 +395,15 @@ private predicate readCand1(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCand1Store(Content f, Node node, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCand1(mid, true, config) and
|
||||
storeCandFwd1(f, unbind(config)) and
|
||||
store(node, f, mid)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate throughFlowNodeCand(Node node, Configuration config) {
|
||||
nodeCand1(node, false, config) and
|
||||
not fullBarrier(node, config) and
|
||||
@@ -648,9 +665,8 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Node mid, Content f |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
exists(Content f |
|
||||
nodeCandFwd2Read(f, node, fromArg, config) and
|
||||
storeCandFwd2(f, unbind(config)) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
@@ -674,6 +690,7 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
|
||||
/**
|
||||
* Holds if `f` is the target of a store in the flow covered by `nodeCandFwd2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -684,6 +701,15 @@ private predicate storeCandFwd2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate nodeCandFwd2Read(Content f, Node node, boolean fromArg, Configuration config) {
|
||||
exists(Node mid |
|
||||
nodeCandFwd2(mid, fromArg, true, config) and
|
||||
read(mid, f, node) and
|
||||
readCand1(f, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` is part of a path from a source to a sink in the given
|
||||
* configuration taking simple call contexts into consideration.
|
||||
@@ -721,10 +747,9 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Node mid, Content f |
|
||||
store(node, f, mid) and
|
||||
exists(Content f |
|
||||
nodeCand2Store(f, node, toReturn, config) and
|
||||
readCand2(f, unbind(config)) and
|
||||
nodeCand2(mid, toReturn, true, config) and
|
||||
(stored = false or stored = true)
|
||||
)
|
||||
or
|
||||
@@ -755,6 +780,7 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
|
||||
/**
|
||||
* Holds if `f` is the target of a read in the flow covered by `nodeCand2`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate readCand2(Content f, Configuration config) {
|
||||
exists(Node mid, Node node |
|
||||
useFieldFlow(config) and
|
||||
@@ -765,16 +791,21 @@ private predicate readCand2(Content f, Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node n1, Node n2 |
|
||||
store(n1, f, n2) and
|
||||
nodeCand2(n1, _, _, conf) and
|
||||
nodeCand2(n2, _, _, unbind(conf))
|
||||
pragma[noinline]
|
||||
private predicate nodeCand2Store(Content f, Node node, boolean toReturn, Configuration config) {
|
||||
exists(Node mid |
|
||||
store(node, f, mid) and
|
||||
nodeCand2(mid, toReturn, true, config)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[nomagic]
|
||||
private predicate storeCand(Content f, Configuration conf) {
|
||||
exists(Node node |
|
||||
nodeCand2Store(f, node, _, conf) and
|
||||
nodeCand2(node, _, _, unbind(conf))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `f` is the target of both a store and a read in the path graph
|
||||
@@ -783,7 +814,7 @@ private predicate readCand(Content f, Configuration conf) { readCand2(f, conf) }
|
||||
pragma[noinline]
|
||||
private predicate readStoreCand(Content f, Configuration conf) {
|
||||
storeCand(f, conf) and
|
||||
readCand(f, conf)
|
||||
readCand2(f, conf)
|
||||
}
|
||||
|
||||
private predicate nodeCand(Node node, Configuration config) { nodeCand2(node, _, _, config) }
|
||||
@@ -1009,15 +1040,14 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
|
||||
apf.headUsesContent(f)
|
||||
)
|
||||
or
|
||||
exists(Node mid, Content f, AccessPathFront apf0 |
|
||||
flowCandFwd(mid, fromArg, apf0, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, config) and
|
||||
exists(Content f, AccessPathFront apf0 |
|
||||
flowCandFwdRead(f, node, apf0, fromArg, config) and
|
||||
apf0.headUsesContent(f) and
|
||||
consCandFwd(f, apf, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCandFwd(Content f, AccessPathFront apf, Configuration config) {
|
||||
exists(Node mid, Node n |
|
||||
flowCandFwd(mid, _, apf, config) and
|
||||
@@ -1028,6 +1058,17 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandFwdRead(
|
||||
Content f, Node node, AccessPathFront apf, boolean fromArg, Configuration config
|
||||
) {
|
||||
exists(Node mid |
|
||||
flowCandFwd(mid, fromArg, apf, config) and
|
||||
read(mid, f, node) and
|
||||
nodeCand(node, unbind(config))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from a source to `node` with the given `apf` and
|
||||
* from there flow to a sink.
|
||||
@@ -1118,6 +1159,7 @@ private predicate flowCandRead(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate flowCandStore(
|
||||
Node node, Content f, boolean toReturn, AccessPathFront apf0, Configuration config
|
||||
) {
|
||||
@@ -1127,6 +1169,7 @@ private predicate flowCandStore(
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate consCand(Content f, AccessPathFront apf, Configuration config) {
|
||||
consCandFwd(f, apf, config) and
|
||||
exists(Node n, AccessPathFront apf0 |
|
||||
|
||||
Reference in New Issue
Block a user