Merge branch 'main' into redundantImport

This commit is contained in:
Erik Krogh Kristensen
2022-04-26 14:24:51 +02:00
889 changed files with 9741 additions and 3014 deletions

View File

@@ -1,3 +1,5 @@
## 1.1.0
## 1.0.7
## 1.0.6

View File

@@ -0,0 +1 @@
## 1.1.0

View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 1.0.7
lastReleaseVersion: 1.1.0

View File

@@ -1,5 +1,5 @@
name: codeql/csharp-solorigate-all
version: 1.1.0-dev
version: 1.1.1-dev
groups:
- csharp
- solorigate

View File

@@ -1,3 +1,5 @@
## 1.1.0
## 1.0.7
## 1.0.6

View File

@@ -0,0 +1 @@
## 1.1.0

View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 1.0.7
lastReleaseVersion: 1.1.0

View File

@@ -1,5 +1,5 @@
name: codeql/csharp-solorigate-queries
version: 1.1.0-dev
version: 1.1.1-dev
groups:
- csharp
- solorigate

View File

@@ -1,3 +1,9 @@
## 0.1.0
### Breaking Changes
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.
## 0.0.13
## 0.0.12

View File

@@ -1,4 +0,0 @@
---
category: breaking
---
The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.

View File

@@ -0,0 +1,4 @@
---
category: breaking
---
The signature of `allowImplicitRead` on `DataFlow::Configuration` and `TaintTracking::Configuration` has changed from `allowImplicitRead(DataFlow::Node node, DataFlow::Content c)` to `allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c)`.

View File

@@ -0,0 +1,5 @@
## 0.1.0
### Breaking Changes
* The recently added flow-state versions of `isBarrierIn`, `isBarrierOut`, `isSanitizerIn`, and `isSanitizerOut` in the data flow and taint tracking libraries have been removed.

View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 0.0.13
lastReleaseVersion: 0.1.0

View File

@@ -1,5 +1,5 @@
name: codeql/csharp-all
version: 0.1.0-dev
version: 0.1.1-dev
groups: csharp
dbscheme: semmlecode.csharp.dbscheme
extractor: csharp

View File

@@ -144,7 +144,7 @@ private class SummarizedCallableDefaultClearsContent extends Impl::Public::Summa
}
// By default, we assume that all stores into arguments are definite
override predicate clearsContent(ParameterPosition pos, DataFlow::Content content) {
override predicate clearsContent(ParameterPosition pos, DataFlow::ContentSet content) {
exists(SummaryComponentStack output, SummaryComponent target |
this.propagatesFlow(_, output, _) and
output.drop(_) =

View File

@@ -149,7 +149,7 @@ class AccessPath extends string instanceof AccessPath::Range {
* An access part token such as `Argument[1]` or `ReturnValue`, appearing in one or more access paths.
*/
class AccessPathToken extends string {
AccessPathToken() { this = getRawToken(any(AccessPath path), _) }
AccessPathToken() { this = getRawToken(_, _) }
private string getPart(int part) {
result = this.regexpCapture("([^\\[]+)(?:\\[([^\\]]*)\\])?", part)

View File

@@ -116,7 +116,7 @@ abstract class Configuration extends string {
* Holds if an arbitrary number of implicit read steps of content `c` may be
* taken at `node`.
*/
predicate allowImplicitRead(Node node, Content c) { none() }
predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Gets the virtual dispatch branching limit when calculating field flow.
@@ -485,8 +485,9 @@ private predicate additionalJumpStateStep(
)
}
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
read(node1.asNode(), c, node2.asNode()) and
pragma[nomagic]
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
readSet(node1.asNode(), c, node2.asNode()) and
stepFilter(node1, node2, config)
or
exists(Node n |
@@ -496,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
exists(ContentSet cs |
readSet(node1, cs, node2, config) and
c = cs.getAReadContent()
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate clearsContentEx(NodeEx n, Content c) {
exists(ContentSet cs |
clearsContentCached(n.asNode(), cs) and
c = cs.getAReadContent()
)
}
pragma[nomagic]
private predicate store(
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
) {
@@ -573,9 +593,9 @@ private module Stage1 {
)
or
// read
exists(Content c |
fwdFlowRead(c, node, cc, config) and
fwdFlowConsCand(c, config)
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -599,10 +619,10 @@ private module Stage1 {
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
pragma[nomagic]
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
exists(NodeEx mid |
fwdFlow(mid, cc, config) and
read(mid, c, node, config)
readSet(mid, c, node, config)
)
}
@@ -620,6 +640,16 @@ private module Stage1 {
)
}
/**
* 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 cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
exists(RetNodeEx ret |
@@ -712,9 +742,9 @@ private module Stage1 {
)
or
// read
exists(NodeEx mid, Content c |
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -740,10 +770,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))
)
}
@@ -762,6 +792,7 @@ private module Stage1 {
* Holds if `c` is the target of both a read and a store in the flow covered
* by `revFlow`.
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowStore(c, _, _, conf)
@@ -860,9 +891,9 @@ private module Stage1 {
pragma[nomagic]
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config))
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config))
}
pragma[nomagic]
@@ -872,7 +903,10 @@ private module Stage1 {
predicate revFlow(
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
) {
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
revFlow(node, toReturn, pragma[only_bind_into](config)) and
exists(state) and
exists(returnAp) and
exists(ap)
}
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
@@ -1149,7 +1183,7 @@ private module Stage2 {
bindingset[node, state, ap, config]
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
PrevStage::revFlowState(state, config) and
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
exists(ap) and
not stateBarrier(node, state, config)
}
@@ -1574,7 +1608,7 @@ private module Stage2 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -1729,9 +1763,9 @@ private module LocalFlowBigStep {
or
node.asNode() instanceof OutNodeExt
or
store(_, _, node, _, config)
Stage2::storeStepCand(_, _, _, node, _, config)
or
read(_, _, node, config)
Stage2::readStepCand(_, _, node, config)
or
node instanceof FlowCheckNode
or
@@ -1752,8 +1786,8 @@ private module LocalFlowBigStep {
additionalJumpStep(node, next, config) or
flowIntoCallNodeCand1(_, node, next, config) or
flowOutOfCallNodeCand1(_, node, next, config) or
store(node, _, next, _, config) or
read(node, _, next, config)
Stage2::storeStepCand(node, _, _, next, _, config) or
Stage2::readStepCand(node, _, next, config)
)
or
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
@@ -1926,7 +1960,24 @@ private module Stage3 {
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
PrevStage::revFlow(node, config) and
clearsContentCached(node.asNode(), c)
}
pragma[nomagic]
private predicate clearContent(NodeEx node, Content c, Configuration config) {
exists(ContentSet cs |
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
c = cs.getAReadContent() and
clearSet(node, cs, pragma[only_bind_into](config))
)
}
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap, Configuration config) {
clearContent(node, ap.getHead().getContent(), config)
}
pragma[nomagic]
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
@@ -1935,7 +1986,7 @@ private module Stage3 {
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
exists(state) and
exists(config) and
not clear(node, ap) and
not clear(node, ap, config) and
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
}
@@ -2363,7 +2414,7 @@ private module Stage3 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -3190,7 +3241,7 @@ private module Stage4 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -4202,7 +4253,7 @@ private module Subpaths {
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
store(n1, _, n2, _, _) or
read(n1, _, n2, _)
readSet(n1, _, n2, _)
)
}
@@ -4557,7 +4608,7 @@ private module FlowExploration {
or
exists(PartialPathNodeRev mid |
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
not clearsContentCached(node.asNode(), ap.getHead()) and
not clearsContentEx(node, ap.getHead()) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
@@ -4573,7 +4624,7 @@ private module FlowExploration {
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
not clearsContentEx(node, ap.getHead().getContent()) and
if node.asNode() instanceof CastingNode
then compatibleTypes(node.getDataFlowType(), ap.getType())
else any()

View File

@@ -116,7 +116,7 @@ abstract class Configuration extends string {
* Holds if an arbitrary number of implicit read steps of content `c` may be
* taken at `node`.
*/
predicate allowImplicitRead(Node node, Content c) { none() }
predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Gets the virtual dispatch branching limit when calculating field flow.
@@ -485,8 +485,9 @@ private predicate additionalJumpStateStep(
)
}
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
read(node1.asNode(), c, node2.asNode()) and
pragma[nomagic]
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
readSet(node1.asNode(), c, node2.asNode()) and
stepFilter(node1, node2, config)
or
exists(Node n |
@@ -496,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
exists(ContentSet cs |
readSet(node1, cs, node2, config) and
c = cs.getAReadContent()
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate clearsContentEx(NodeEx n, Content c) {
exists(ContentSet cs |
clearsContentCached(n.asNode(), cs) and
c = cs.getAReadContent()
)
}
pragma[nomagic]
private predicate store(
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
) {
@@ -573,9 +593,9 @@ private module Stage1 {
)
or
// read
exists(Content c |
fwdFlowRead(c, node, cc, config) and
fwdFlowConsCand(c, config)
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -599,10 +619,10 @@ private module Stage1 {
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
pragma[nomagic]
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
exists(NodeEx mid |
fwdFlow(mid, cc, config) and
read(mid, c, node, config)
readSet(mid, c, node, config)
)
}
@@ -620,6 +640,16 @@ private module Stage1 {
)
}
/**
* 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 cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
exists(RetNodeEx ret |
@@ -712,9 +742,9 @@ private module Stage1 {
)
or
// read
exists(NodeEx mid, Content c |
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -740,10 +770,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))
)
}
@@ -762,6 +792,7 @@ private module Stage1 {
* Holds if `c` is the target of both a read and a store in the flow covered
* by `revFlow`.
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowStore(c, _, _, conf)
@@ -860,9 +891,9 @@ private module Stage1 {
pragma[nomagic]
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config))
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config))
}
pragma[nomagic]
@@ -872,7 +903,10 @@ private module Stage1 {
predicate revFlow(
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
) {
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
revFlow(node, toReturn, pragma[only_bind_into](config)) and
exists(state) and
exists(returnAp) and
exists(ap)
}
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
@@ -1149,7 +1183,7 @@ private module Stage2 {
bindingset[node, state, ap, config]
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
PrevStage::revFlowState(state, config) and
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
exists(ap) and
not stateBarrier(node, state, config)
}
@@ -1574,7 +1608,7 @@ private module Stage2 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -1729,9 +1763,9 @@ private module LocalFlowBigStep {
or
node.asNode() instanceof OutNodeExt
or
store(_, _, node, _, config)
Stage2::storeStepCand(_, _, _, node, _, config)
or
read(_, _, node, config)
Stage2::readStepCand(_, _, node, config)
or
node instanceof FlowCheckNode
or
@@ -1752,8 +1786,8 @@ private module LocalFlowBigStep {
additionalJumpStep(node, next, config) or
flowIntoCallNodeCand1(_, node, next, config) or
flowOutOfCallNodeCand1(_, node, next, config) or
store(node, _, next, _, config) or
read(node, _, next, config)
Stage2::storeStepCand(node, _, _, next, _, config) or
Stage2::readStepCand(node, _, next, config)
)
or
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
@@ -1926,7 +1960,24 @@ private module Stage3 {
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
PrevStage::revFlow(node, config) and
clearsContentCached(node.asNode(), c)
}
pragma[nomagic]
private predicate clearContent(NodeEx node, Content c, Configuration config) {
exists(ContentSet cs |
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
c = cs.getAReadContent() and
clearSet(node, cs, pragma[only_bind_into](config))
)
}
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap, Configuration config) {
clearContent(node, ap.getHead().getContent(), config)
}
pragma[nomagic]
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
@@ -1935,7 +1986,7 @@ private module Stage3 {
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
exists(state) and
exists(config) and
not clear(node, ap) and
not clear(node, ap, config) and
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
}
@@ -2363,7 +2414,7 @@ private module Stage3 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -3190,7 +3241,7 @@ private module Stage4 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -4202,7 +4253,7 @@ private module Subpaths {
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
store(n1, _, n2, _, _) or
read(n1, _, n2, _)
readSet(n1, _, n2, _)
)
}
@@ -4557,7 +4608,7 @@ private module FlowExploration {
or
exists(PartialPathNodeRev mid |
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
not clearsContentCached(node.asNode(), ap.getHead()) and
not clearsContentEx(node, ap.getHead()) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
@@ -4573,7 +4624,7 @@ private module FlowExploration {
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
not clearsContentEx(node, ap.getHead().getContent()) and
if node.asNode() instanceof CastingNode
then compatibleTypes(node.getDataFlowType(), ap.getType())
else any()

View File

@@ -116,7 +116,7 @@ abstract class Configuration extends string {
* Holds if an arbitrary number of implicit read steps of content `c` may be
* taken at `node`.
*/
predicate allowImplicitRead(Node node, Content c) { none() }
predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Gets the virtual dispatch branching limit when calculating field flow.
@@ -485,8 +485,9 @@ private predicate additionalJumpStateStep(
)
}
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
read(node1.asNode(), c, node2.asNode()) and
pragma[nomagic]
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
readSet(node1.asNode(), c, node2.asNode()) and
stepFilter(node1, node2, config)
or
exists(Node n |
@@ -496,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
exists(ContentSet cs |
readSet(node1, cs, node2, config) and
c = cs.getAReadContent()
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate clearsContentEx(NodeEx n, Content c) {
exists(ContentSet cs |
clearsContentCached(n.asNode(), cs) and
c = cs.getAReadContent()
)
}
pragma[nomagic]
private predicate store(
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
) {
@@ -573,9 +593,9 @@ private module Stage1 {
)
or
// read
exists(Content c |
fwdFlowRead(c, node, cc, config) and
fwdFlowConsCand(c, config)
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -599,10 +619,10 @@ private module Stage1 {
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
pragma[nomagic]
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
exists(NodeEx mid |
fwdFlow(mid, cc, config) and
read(mid, c, node, config)
readSet(mid, c, node, config)
)
}
@@ -620,6 +640,16 @@ private module Stage1 {
)
}
/**
* 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 cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
exists(RetNodeEx ret |
@@ -712,9 +742,9 @@ private module Stage1 {
)
or
// read
exists(NodeEx mid, Content c |
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -740,10 +770,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))
)
}
@@ -762,6 +792,7 @@ private module Stage1 {
* Holds if `c` is the target of both a read and a store in the flow covered
* by `revFlow`.
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowStore(c, _, _, conf)
@@ -860,9 +891,9 @@ private module Stage1 {
pragma[nomagic]
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config))
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config))
}
pragma[nomagic]
@@ -872,7 +903,10 @@ private module Stage1 {
predicate revFlow(
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
) {
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
revFlow(node, toReturn, pragma[only_bind_into](config)) and
exists(state) and
exists(returnAp) and
exists(ap)
}
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
@@ -1149,7 +1183,7 @@ private module Stage2 {
bindingset[node, state, ap, config]
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
PrevStage::revFlowState(state, config) and
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
exists(ap) and
not stateBarrier(node, state, config)
}
@@ -1574,7 +1608,7 @@ private module Stage2 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -1729,9 +1763,9 @@ private module LocalFlowBigStep {
or
node.asNode() instanceof OutNodeExt
or
store(_, _, node, _, config)
Stage2::storeStepCand(_, _, _, node, _, config)
or
read(_, _, node, config)
Stage2::readStepCand(_, _, node, config)
or
node instanceof FlowCheckNode
or
@@ -1752,8 +1786,8 @@ private module LocalFlowBigStep {
additionalJumpStep(node, next, config) or
flowIntoCallNodeCand1(_, node, next, config) or
flowOutOfCallNodeCand1(_, node, next, config) or
store(node, _, next, _, config) or
read(node, _, next, config)
Stage2::storeStepCand(node, _, _, next, _, config) or
Stage2::readStepCand(node, _, next, config)
)
or
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
@@ -1926,7 +1960,24 @@ private module Stage3 {
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
PrevStage::revFlow(node, config) and
clearsContentCached(node.asNode(), c)
}
pragma[nomagic]
private predicate clearContent(NodeEx node, Content c, Configuration config) {
exists(ContentSet cs |
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
c = cs.getAReadContent() and
clearSet(node, cs, pragma[only_bind_into](config))
)
}
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap, Configuration config) {
clearContent(node, ap.getHead().getContent(), config)
}
pragma[nomagic]
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
@@ -1935,7 +1986,7 @@ private module Stage3 {
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
exists(state) and
exists(config) and
not clear(node, ap) and
not clear(node, ap, config) and
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
}
@@ -2363,7 +2414,7 @@ private module Stage3 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -3190,7 +3241,7 @@ private module Stage4 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -4202,7 +4253,7 @@ private module Subpaths {
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
store(n1, _, n2, _, _) or
read(n1, _, n2, _)
readSet(n1, _, n2, _)
)
}
@@ -4557,7 +4608,7 @@ private module FlowExploration {
or
exists(PartialPathNodeRev mid |
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
not clearsContentCached(node.asNode(), ap.getHead()) and
not clearsContentEx(node, ap.getHead()) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
@@ -4573,7 +4624,7 @@ private module FlowExploration {
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
not clearsContentEx(node, ap.getHead().getContent()) and
if node.asNode() instanceof CastingNode
then compatibleTypes(node.getDataFlowType(), ap.getType())
else any()

View File

@@ -116,7 +116,7 @@ abstract class Configuration extends string {
* Holds if an arbitrary number of implicit read steps of content `c` may be
* taken at `node`.
*/
predicate allowImplicitRead(Node node, Content c) { none() }
predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Gets the virtual dispatch branching limit when calculating field flow.
@@ -485,8 +485,9 @@ private predicate additionalJumpStateStep(
)
}
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
read(node1.asNode(), c, node2.asNode()) and
pragma[nomagic]
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
readSet(node1.asNode(), c, node2.asNode()) and
stepFilter(node1, node2, config)
or
exists(Node n |
@@ -496,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
exists(ContentSet cs |
readSet(node1, cs, node2, config) and
c = cs.getAReadContent()
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate clearsContentEx(NodeEx n, Content c) {
exists(ContentSet cs |
clearsContentCached(n.asNode(), cs) and
c = cs.getAReadContent()
)
}
pragma[nomagic]
private predicate store(
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
) {
@@ -573,9 +593,9 @@ private module Stage1 {
)
or
// read
exists(Content c |
fwdFlowRead(c, node, cc, config) and
fwdFlowConsCand(c, config)
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -599,10 +619,10 @@ private module Stage1 {
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
pragma[nomagic]
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
exists(NodeEx mid |
fwdFlow(mid, cc, config) and
read(mid, c, node, config)
readSet(mid, c, node, config)
)
}
@@ -620,6 +640,16 @@ private module Stage1 {
)
}
/**
* 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 cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
exists(RetNodeEx ret |
@@ -712,9 +742,9 @@ private module Stage1 {
)
or
// read
exists(NodeEx mid, Content c |
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -740,10 +770,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))
)
}
@@ -762,6 +792,7 @@ private module Stage1 {
* Holds if `c` is the target of both a read and a store in the flow covered
* by `revFlow`.
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowStore(c, _, _, conf)
@@ -860,9 +891,9 @@ private module Stage1 {
pragma[nomagic]
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config))
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config))
}
pragma[nomagic]
@@ -872,7 +903,10 @@ private module Stage1 {
predicate revFlow(
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
) {
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
revFlow(node, toReturn, pragma[only_bind_into](config)) and
exists(state) and
exists(returnAp) and
exists(ap)
}
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
@@ -1149,7 +1183,7 @@ private module Stage2 {
bindingset[node, state, ap, config]
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
PrevStage::revFlowState(state, config) and
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
exists(ap) and
not stateBarrier(node, state, config)
}
@@ -1574,7 +1608,7 @@ private module Stage2 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -1729,9 +1763,9 @@ private module LocalFlowBigStep {
or
node.asNode() instanceof OutNodeExt
or
store(_, _, node, _, config)
Stage2::storeStepCand(_, _, _, node, _, config)
or
read(_, _, node, config)
Stage2::readStepCand(_, _, node, config)
or
node instanceof FlowCheckNode
or
@@ -1752,8 +1786,8 @@ private module LocalFlowBigStep {
additionalJumpStep(node, next, config) or
flowIntoCallNodeCand1(_, node, next, config) or
flowOutOfCallNodeCand1(_, node, next, config) or
store(node, _, next, _, config) or
read(node, _, next, config)
Stage2::storeStepCand(node, _, _, next, _, config) or
Stage2::readStepCand(node, _, next, config)
)
or
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
@@ -1926,7 +1960,24 @@ private module Stage3 {
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
PrevStage::revFlow(node, config) and
clearsContentCached(node.asNode(), c)
}
pragma[nomagic]
private predicate clearContent(NodeEx node, Content c, Configuration config) {
exists(ContentSet cs |
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
c = cs.getAReadContent() and
clearSet(node, cs, pragma[only_bind_into](config))
)
}
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap, Configuration config) {
clearContent(node, ap.getHead().getContent(), config)
}
pragma[nomagic]
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
@@ -1935,7 +1986,7 @@ private module Stage3 {
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
exists(state) and
exists(config) and
not clear(node, ap) and
not clear(node, ap, config) and
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
}
@@ -2363,7 +2414,7 @@ private module Stage3 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -3190,7 +3241,7 @@ private module Stage4 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -4202,7 +4253,7 @@ private module Subpaths {
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
store(n1, _, n2, _, _) or
read(n1, _, n2, _)
readSet(n1, _, n2, _)
)
}
@@ -4557,7 +4608,7 @@ private module FlowExploration {
or
exists(PartialPathNodeRev mid |
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
not clearsContentCached(node.asNode(), ap.getHead()) and
not clearsContentEx(node, ap.getHead()) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
@@ -4573,7 +4624,7 @@ private module FlowExploration {
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
not clearsContentEx(node, ap.getHead().getContent()) and
if node.asNode() instanceof CastingNode
then compatibleTypes(node.getDataFlowType(), ap.getType())
else any()

View File

@@ -116,7 +116,7 @@ abstract class Configuration extends string {
* Holds if an arbitrary number of implicit read steps of content `c` may be
* taken at `node`.
*/
predicate allowImplicitRead(Node node, Content c) { none() }
predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Gets the virtual dispatch branching limit when calculating field flow.
@@ -485,8 +485,9 @@ private predicate additionalJumpStateStep(
)
}
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
read(node1.asNode(), c, node2.asNode()) and
pragma[nomagic]
private predicate readSet(NodeEx node1, ContentSet c, NodeEx node2, Configuration config) {
readSet(node1.asNode(), c, node2.asNode()) and
stepFilter(node1, node2, config)
or
exists(Node n |
@@ -496,6 +497,25 @@ private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration conf
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate read(NodeEx node1, Content c, NodeEx node2, Configuration config) {
exists(ContentSet cs |
readSet(node1, cs, node2, config) and
c = cs.getAReadContent()
)
}
// inline to reduce fan-out via `getAReadContent`
pragma[inline]
private predicate clearsContentEx(NodeEx n, Content c) {
exists(ContentSet cs |
clearsContentCached(n.asNode(), cs) and
c = cs.getAReadContent()
)
}
pragma[nomagic]
private predicate store(
NodeEx node1, TypedContent tc, NodeEx node2, DataFlowType contentType, Configuration config
) {
@@ -573,9 +593,9 @@ private module Stage1 {
)
or
// read
exists(Content c |
fwdFlowRead(c, node, cc, config) and
fwdFlowConsCand(c, config)
exists(ContentSet c |
fwdFlowReadSet(c, node, cc, config) and
fwdFlowConsCandSet(c, _, config)
)
or
// flow into a callable
@@ -599,10 +619,10 @@ private module Stage1 {
private predicate fwdFlow(NodeEx node, Configuration config) { fwdFlow(node, _, config) }
pragma[nomagic]
private predicate fwdFlowRead(Content c, NodeEx node, Cc cc, Configuration config) {
private predicate fwdFlowReadSet(ContentSet c, NodeEx node, Cc cc, Configuration config) {
exists(NodeEx mid |
fwdFlow(mid, cc, config) and
read(mid, c, node, config)
readSet(mid, c, node, config)
)
}
@@ -620,6 +640,16 @@ private module Stage1 {
)
}
/**
* 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 cs, Content c, Configuration config) {
fwdFlowConsCand(c, config) and
c = cs.getAReadContent()
}
pragma[nomagic]
private predicate fwdFlowReturnPosition(ReturnPosition pos, Cc cc, Configuration config) {
exists(RetNodeEx ret |
@@ -712,9 +742,9 @@ private module Stage1 {
)
or
// read
exists(NodeEx mid, Content c |
read(node, c, mid, config) and
fwdFlowConsCand(c, pragma[only_bind_into](config)) and
exists(NodeEx mid, ContentSet c |
readSet(node, c, mid, config) and
fwdFlowConsCandSet(c, _, pragma[only_bind_into](config)) and
revFlow(mid, toReturn, pragma[only_bind_into](config))
)
or
@@ -740,10 +770,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))
)
}
@@ -762,6 +792,7 @@ private module Stage1 {
* Holds if `c` is the target of both a read and a store in the flow covered
* by `revFlow`.
*/
pragma[nomagic]
private predicate revFlowIsReadAndStored(Content c, Configuration conf) {
revFlowConsCand(c, conf) and
revFlowStore(c, _, _, conf)
@@ -860,9 +891,9 @@ private module Stage1 {
pragma[nomagic]
predicate readStepCand(NodeEx n1, Content c, NodeEx n2, Configuration config) {
revFlowIsReadAndStored(c, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config))
revFlowIsReadAndStored(pragma[only_bind_into](c), pragma[only_bind_into](config)) and
read(n1, c, n2, pragma[only_bind_into](config)) and
revFlow(n2, pragma[only_bind_into](config))
}
pragma[nomagic]
@@ -872,7 +903,10 @@ private module Stage1 {
predicate revFlow(
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
) {
revFlow(node, toReturn, config) and exists(state) and exists(returnAp) and exists(ap)
revFlow(node, toReturn, pragma[only_bind_into](config)) and
exists(state) and
exists(returnAp) and
exists(ap)
}
private predicate throughFlowNodeCand(NodeEx node, Configuration config) {
@@ -1149,7 +1183,7 @@ private module Stage2 {
bindingset[node, state, ap, config]
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
PrevStage::revFlowState(state, config) and
PrevStage::revFlowState(state, pragma[only_bind_into](config)) and
exists(ap) and
not stateBarrier(node, state, config)
}
@@ -1574,7 +1608,7 @@ private module Stage2 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -1729,9 +1763,9 @@ private module LocalFlowBigStep {
or
node.asNode() instanceof OutNodeExt
or
store(_, _, node, _, config)
Stage2::storeStepCand(_, _, _, node, _, config)
or
read(_, _, node, config)
Stage2::readStepCand(_, _, node, config)
or
node instanceof FlowCheckNode
or
@@ -1752,8 +1786,8 @@ private module LocalFlowBigStep {
additionalJumpStep(node, next, config) or
flowIntoCallNodeCand1(_, node, next, config) or
flowOutOfCallNodeCand1(_, node, next, config) or
store(node, _, next, _, config) or
read(node, _, next, config)
Stage2::storeStepCand(node, _, _, next, _, config) or
Stage2::readStepCand(node, _, next, config)
)
or
exists(NodeEx next, FlowState s | Stage2::revFlow(next, s, config) |
@@ -1926,7 +1960,24 @@ private module Stage3 {
private predicate flowIntoCall = flowIntoCallNodeCand2/5;
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap) { ap.isClearedAt(node.asNode()) }
private predicate clearSet(NodeEx node, ContentSet c, Configuration config) {
PrevStage::revFlow(node, config) and
clearsContentCached(node.asNode(), c)
}
pragma[nomagic]
private predicate clearContent(NodeEx node, Content c, Configuration config) {
exists(ContentSet cs |
PrevStage::readStepCand(_, pragma[only_bind_into](c), _, pragma[only_bind_into](config)) and
c = cs.getAReadContent() and
clearSet(node, cs, pragma[only_bind_into](config))
)
}
pragma[nomagic]
private predicate clear(NodeEx node, Ap ap, Configuration config) {
clearContent(node, ap.getHead().getContent(), config)
}
pragma[nomagic]
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
@@ -1935,7 +1986,7 @@ private module Stage3 {
private predicate filter(NodeEx node, FlowState state, Ap ap, Configuration config) {
exists(state) and
exists(config) and
not clear(node, ap) and
not clear(node, ap, config) and
if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), ap.getType()) else any()
}
@@ -2363,7 +2414,7 @@ private module Stage3 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -3190,7 +3241,7 @@ private module Stage4 {
Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType, config) and
PrevStage::storeStepCand(node1, _, tc, node2, contentType, config) and
revFlowStore(ap2, c, ap1, node1, _, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
@@ -4202,7 +4253,7 @@ private module Subpaths {
exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() |
localFlowBigStep(n1, _, n2, _, _, _, _, _) or
store(n1, _, n2, _, _) or
read(n1, _, n2, _)
readSet(n1, _, n2, _)
)
}
@@ -4557,7 +4608,7 @@ private module FlowExploration {
or
exists(PartialPathNodeRev mid |
revPartialPathStep(mid, node, state, sc1, sc2, sc3, ap, config) and
not clearsContentCached(node.asNode(), ap.getHead()) and
not clearsContentEx(node, ap.getHead()) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
distSink(node.getEnclosingCallable(), config) <= config.explorationLimit()
@@ -4573,7 +4624,7 @@ private module FlowExploration {
partialPathStep(mid, node, state, cc, sc1, sc2, sc3, ap, config) and
not fullBarrier(node, config) and
not stateBarrier(node, state, config) and
not clearsContentCached(node.asNode(), ap.getHead().getContent()) and
not clearsContentEx(node, ap.getHead().getContent()) and
if node.asNode() instanceof CastingNode
then compatibleTypes(node.getDataFlowType(), ap.getType())
else any()

View File

@@ -326,7 +326,7 @@ private module Cached {
predicate jumpStepCached(Node node1, Node node2) { jumpStep(node1, node2) }
cached
predicate clearsContentCached(Node n, Content c) { clearsContent(n, c) }
predicate clearsContentCached(Node n, ContentSet c) { clearsContent(n, c) }
cached
predicate isUnreachableInCallCached(Node n, DataFlowCall call) { isUnreachableInCall(n, call) }
@@ -373,7 +373,7 @@ private module Cached {
// For reads, `x.f`, we want to check that the tracked type after the read (which
// is obtained by popping the head of the access path stack) is compatible with
// the type of `x.f`.
read(_, _, n)
readSet(_, _, n)
}
cached
@@ -469,7 +469,7 @@ private module Cached {
// read
exists(Node mid |
parameterValueFlowCand(p, mid, false) and
read(mid, _, node) and
readSet(mid, _, node) and
read = true
)
or
@@ -657,8 +657,10 @@ private module Cached {
* Holds if `arg` flows to `out` through a call using only
* value-preserving steps and a single read step, not taking call
* contexts into account, thus representing a getter-step.
*
* This predicate is exposed for testing only.
*/
predicate getterStep(ArgNode arg, Content c, Node out) {
predicate getterStep(ArgNode arg, ContentSet c, Node out) {
argumentValueFlowsThrough(arg, TReadStepTypesSome(_, c, _), out)
}
@@ -781,28 +783,30 @@ private module Cached {
parameterValueFlow(p, n.getPreUpdateNode(), TReadStepTypesNone())
}
cached
predicate readSet(Node node1, ContentSet c, Node node2) { readStep(node1, c, node2) }
private predicate store(
Node node1, Content c, Node node2, DataFlowType contentType, DataFlowType containerType
) {
storeStep(node1, c, node2) and
contentType = getNodeDataFlowType(node1) and
containerType = getNodeDataFlowType(node2)
or
exists(Node n1, Node n2 |
n1 = node1.(PostUpdateNode).getPreUpdateNode() and
n2 = node2.(PostUpdateNode).getPreUpdateNode()
|
argumentValueFlowsThrough(n2, TReadStepTypesSome(containerType, c, contentType), n1)
exists(ContentSet cs | c = cs.getAStoreContent() |
storeStep(node1, cs, node2) and
contentType = getNodeDataFlowType(node1) and
containerType = getNodeDataFlowType(node2)
or
read(n2, c, n1) and
contentType = getNodeDataFlowType(n1) and
containerType = getNodeDataFlowType(n2)
exists(Node n1, Node n2 |
n1 = node1.(PostUpdateNode).getPreUpdateNode() and
n2 = node2.(PostUpdateNode).getPreUpdateNode()
|
argumentValueFlowsThrough(n2, TReadStepTypesSome(containerType, cs, contentType), n1)
or
readSet(n2, cs, n1) and
contentType = getNodeDataFlowType(n1) and
containerType = getNodeDataFlowType(n2)
)
)
}
cached
predicate read(Node node1, Content c, Node node2) { readStep(node1, c, node2) }
/**
* Holds if data can flow from `node1` to `node2` via a direct assignment to
* `f`.
@@ -932,16 +936,16 @@ class CastingNode extends Node {
}
private predicate readStepWithTypes(
Node n1, DataFlowType container, Content c, Node n2, DataFlowType content
Node n1, DataFlowType container, ContentSet c, Node n2, DataFlowType content
) {
read(n1, c, n2) and
readSet(n1, c, n2) and
container = getNodeDataFlowType(n1) and
content = getNodeDataFlowType(n2)
}
private newtype TReadStepTypesOption =
TReadStepTypesNone() or
TReadStepTypesSome(DataFlowType container, Content c, DataFlowType content) {
TReadStepTypesSome(DataFlowType container, ContentSet c, DataFlowType content) {
readStepWithTypes(_, container, c, _, content)
}
@@ -950,7 +954,7 @@ private class ReadStepTypesOption extends TReadStepTypesOption {
DataFlowType getContainerType() { this = TReadStepTypesSome(result, _, _) }
Content getContent() { this = TReadStepTypesSome(_, result, _) }
ContentSet getContent() { this = TReadStepTypesSome(_, result, _) }
DataFlowType getContentType() { this = TReadStepTypesSome(_, _, result) }
@@ -1325,8 +1329,6 @@ abstract class AccessPathFront extends TAccessPathFront {
abstract boolean toBoolNonEmpty();
TypedContent getHead() { this = TFrontHead(result) }
predicate isClearedAt(Node n) { clearsContentCached(n, this.getHead().getContent()) }
}
class AccessPathFrontNil extends AccessPathFront, TFrontNil {

View File

@@ -252,3 +252,23 @@ class ElementContent extends Content, TElementContent {
override Location getLocation() { result instanceof EmptyLocation }
}
/**
* An entity that represents a set of `Content`s.
*
* The set may be interpreted differently depending on whether it is
* stored into (`getAStoreContent`) or read from (`getAReadContent`).
*/
class ContentSet instanceof Content {
/** Gets a content that may be stored into when storing into this set. */
Content getAStoreContent() { result = this }
/** Gets a content that may be read from when reading from this set. */
Content getAReadContent() { result = this }
/** Gets a textual representation of this content set. */
string toString() { result = super.toString() }
/** Gets the location of this content set. */
Location getLocation() { result = super.getLocation() }
}

View File

@@ -24,7 +24,7 @@ module Public {
class SummaryComponent extends TSummaryComponent {
/** Gets a textual representation of this summary component. */
string toString() {
exists(Content c | this = TContentSummaryComponent(c) and result = c.toString())
exists(ContentSet c | this = TContentSummaryComponent(c) and result = c.toString())
or
exists(ArgumentPosition pos |
this = TParameterSummaryComponent(pos) and result = "parameter " + pos
@@ -41,7 +41,7 @@ module Public {
/** Provides predicates for constructing summary components. */
module SummaryComponent {
/** Gets a summary component for content `c`. */
SummaryComponent content(Content c) { result = TContentSummaryComponent(c) }
SummaryComponent content(ContentSet c) { result = TContentSummaryComponent(c) }
/** Gets a summary component for a parameter at position `pos`. */
SummaryComponent parameter(ArgumentPosition pos) { result = TParameterSummaryComponent(pos) }
@@ -218,7 +218,7 @@ module Public {
* arguments at position `pos` to this callable.
*/
pragma[nomagic]
predicate clearsContent(ParameterPosition pos, Content content) { none() }
predicate clearsContent(ParameterPosition pos, ContentSet content) { none() }
}
}
@@ -231,7 +231,7 @@ module Private {
import AccessPathSyntax
newtype TSummaryComponent =
TContentSummaryComponent(Content c) or
TContentSummaryComponent(ContentSet c) or
TParameterSummaryComponent(ArgumentPosition pos) or
TArgumentSummaryComponent(ParameterPosition pos) or
TReturnSummaryComponent(ReturnKind rk)
@@ -540,7 +540,7 @@ module Private {
exists(SummarizedCallable c, SummaryComponentStack s, SummaryComponent head | head = s.head() |
n = summaryNodeInputState(c, s) and
(
exists(Content cont |
exists(ContentSet cont |
head = TContentSummaryComponent(cont) and result = getContentType(cont)
)
or
@@ -554,7 +554,7 @@ module Private {
or
n = summaryNodeOutputState(c, s) and
(
exists(Content cont |
exists(ContentSet cont |
head = TContentSummaryComponent(cont) and result = getContentType(cont)
)
or
@@ -669,7 +669,7 @@ module Private {
* Holds if there is a read step of content `c` from `pred` to `succ`, which
* is synthesized from a flow summary.
*/
predicate summaryReadStep(Node pred, Content c, Node succ) {
predicate summaryReadStep(Node pred, ContentSet c, Node succ) {
exists(SummarizedCallable sc, SummaryComponentStack s |
pred = summaryNodeInputState(sc, s.drop(1)) and
succ = summaryNodeInputState(sc, s) and
@@ -681,7 +681,7 @@ module Private {
* Holds if there is a store step of content `c` from `pred` to `succ`, which
* is synthesized from a flow summary.
*/
predicate summaryStoreStep(Node pred, Content c, Node succ) {
predicate summaryStoreStep(Node pred, ContentSet c, Node succ) {
exists(SummarizedCallable sc, SummaryComponentStack s |
pred = summaryNodeOutputState(sc, s) and
succ = summaryNodeOutputState(sc, s.drop(1)) and
@@ -708,7 +708,7 @@ module Private {
* `a` on line 2 to the post-update node for `a` on that line (via an intermediate
* node where field `b` is cleared).
*/
predicate summaryClearsContent(Node n, Content c) {
predicate summaryClearsContent(Node n, ContentSet c) {
exists(SummarizedCallable sc, ParameterPosition pos |
n = summaryNode(sc, TSummaryNodeClearsContentState(pos, true)) and
sc.clearsContent(pos, c)
@@ -730,7 +730,8 @@ module Private {
* In such cases, it is important to prevent use-use flow out of
* `arg` (see comment for `summaryClearsContent`).
*/
predicate summaryClearsContentArg(ArgNode arg, Content c) {
pragma[nomagic]
predicate summaryClearsContentArg(ArgNode arg, ContentSet c) {
exists(DataFlowCall call, SummarizedCallable sc, ParameterPosition ppos |
argumentPositionMatch(call, arg, ppos) and
viableParam(call, sc, ppos, _) and
@@ -775,7 +776,7 @@ module Private {
* NOTE: This step should not be used in global data-flow/taint-tracking, but may
* be useful to include in the exposed local data-flow/taint-tracking relations.
*/
predicate summaryGetterStep(ArgNode arg, Content c, Node out) {
predicate summaryGetterStep(ArgNode arg, ContentSet c, Node out) {
exists(ReturnKindExt rk, Node mid, ReturnNodeExt ret |
summaryReadStep(summaryArgParam(arg, rk, out), c, mid) and
summaryLocalStep(mid, ret, _) and
@@ -790,7 +791,7 @@ module Private {
* NOTE: This step should not be used in global data-flow/taint-tracking, but may
* be useful to include in the exposed local data-flow/taint-tracking relations.
*/
predicate summarySetterStep(ArgNode arg, Content c, Node out) {
predicate summarySetterStep(ArgNode arg, ContentSet c, Node out) {
exists(ReturnKindExt rk, Node mid, ReturnNodeExt ret |
summaryLocalStep(summaryArgParam(arg, rk, out), mid, _) and
summaryStoreStep(mid, c, ret) and
@@ -1130,7 +1131,7 @@ module Private {
if preservesValue = true then value = "value" else value = "taint"
)
or
exists(Content c |
exists(ContentSet c |
Private::Steps::summaryReadStep(a.asNode(), c, b.asNode()) and
value = "read (" + c + ")"
or

View File

@@ -161,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
this.isAdditionalTaintStep(node1, state1, node2, state2)
}
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
defaultImplicitTaintRead(node, c)
}

View File

@@ -161,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
this.isAdditionalTaintStep(node1, state1, node2, state2)
}
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
defaultImplicitTaintRead(node, c)
}

View File

@@ -161,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
this.isAdditionalTaintStep(node1, state1, node2, state2)
}
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
defaultImplicitTaintRead(node, c)
}

View File

@@ -161,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
this.isAdditionalTaintStep(node1, state1, node2, state2)
}
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
defaultImplicitTaintRead(node, c)
}

View File

@@ -161,7 +161,7 @@ abstract class Configuration extends DataFlow::Configuration {
this.isAdditionalTaintStep(node1, state1, node2, state2)
}
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::Content c) {
override predicate allowImplicitRead(DataFlow::Node node, DataFlow::ContentSet c) {
(this.isSink(node) or this.isAdditionalTaintStep(node, _)) and
defaultImplicitTaintRead(node, c)
}

View File

@@ -54,7 +54,7 @@ private class SystemCollectionsIEnumerableClearFlow extends SummarizedCallable {
this.hasName("Clear")
}
override predicate clearsContent(ParameterPosition pos, DataFlow::Content content) {
override predicate clearsContent(ParameterPosition pos, DataFlow::ContentSet content) {
pos.isThisParameter() and
content instanceof DataFlow::ElementContent
}

View File

@@ -32,7 +32,7 @@ private class SystemTextStringBuilderClearFlow extends SummarizedCallable {
this = any(SystemTextStringBuilderClass s).getAMethod("Clear")
}
override predicate clearsContent(ParameterPosition pos, DataFlow::Content content) {
override predicate clearsContent(ParameterPosition pos, DataFlow::ContentSet content) {
pos.isThisParameter() and
content instanceof DataFlow::ElementContent
}

View File

@@ -1,3 +1,5 @@
## 0.1.0
## 0.0.13
## 0.0.12

View File

@@ -0,0 +1 @@
## 0.1.0

View File

@@ -1,2 +1,2 @@
---
lastReleaseVersion: 0.0.13
lastReleaseVersion: 0.1.0

View File

@@ -1,5 +1,5 @@
name: codeql/csharp-queries
version: 0.1.0-dev
version: 0.1.1-dev
groups:
- csharp
- queries