DataFlow: Allow stateless sinks.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-02 14:31:18 +02:00
parent 7bc8bf616f
commit b953c4a1cf
2 changed files with 38 additions and 11 deletions

View File

@@ -113,6 +113,11 @@ module Configs<DataFlowParameter Lang> {
*/
predicate isSink(Node sink, FlowState state);
/**
* Holds if `sink` is a relevant data flow sink.
*/
default predicate isSink(Node sink) { none() }
/**
* Holds if data flow through `node` is prohibited. This completely removes
* `node` from the data flow graph.

View File

@@ -33,6 +33,11 @@ module MakeImpl<DataFlowParameter Lang> {
*/
predicate isSink(Node sink, FlowState state);
/**
* Holds if `sink` is a relevant data flow sink for any state.
*/
predicate isSink(Node sink);
/**
* Holds if data flow through `node` is prohibited. This completely removes
* `node` from the data flow graph.
@@ -216,8 +221,11 @@ module MakeImpl<DataFlowParameter Lang> {
private predicate outBarrier(NodeEx node) {
exists(Node n |
node.asNode() = n and
Config::isBarrierOut(n) and
Config::isBarrierOut(n)
|
Config::isSink(n, _)
or
Config::isSink(n)
)
}
@@ -230,7 +238,8 @@ module MakeImpl<DataFlowParameter Lang> {
not Config::isSource(n, _)
or
Config::isBarrierOut(n) and
not Config::isSink(n, _)
not Config::isSink(n, _) and
not Config::isSink(n)
)
}
@@ -247,7 +256,7 @@ module MakeImpl<DataFlowParameter Lang> {
}
pragma[nomagic]
private predicate sinkNode(NodeEx node, FlowState state) {
private predicate sinkNodeWithState(NodeEx node, FlowState state) {
Config::isSink(node.asNode(), state) and
not fullBarrier(node) and
not stateBarrier(node, state)
@@ -645,6 +654,16 @@ module MakeImpl<DataFlowParameter Lang> {
)
}
additional predicate sinkNode(NodeEx node, FlowState state) {
fwdFlow(node) and
fwdFlowState(state) and
Config::isSink(node.asNode())
or
fwdFlow(node) and
fwdFlowState(state) and
sinkNodeWithState(node, state)
}
/**
* Holds if `node` is part of a path from a source to a sink.
*
@@ -659,12 +678,8 @@ module MakeImpl<DataFlowParameter Lang> {
pragma[nomagic]
private predicate revFlow0(NodeEx node, boolean toReturn) {
exists(FlowState state |
fwdFlow(node) and
sinkNode(node, state) and
fwdFlowState(state) and
if hasSinkCallCtx() then toReturn = true else toReturn = false
)
sinkNode(node, _) and
if hasSinkCallCtx() then toReturn = true else toReturn = false
or
exists(NodeEx mid | revFlow(mid, toReturn) |
localFlowStepEx(node, mid) or
@@ -920,6 +935,8 @@ module MakeImpl<DataFlowParameter Lang> {
/* End: Stage 1 logic. */
}
private predicate sinkNode = Stage1::sinkNode/2;
pragma[noinline]
private predicate localFlowStepNodeCand1(NodeEx node1, NodeEx node2) {
Stage1::revFlow(node2) and
@@ -3894,7 +3911,10 @@ module MakeImpl<DataFlowParameter Lang> {
}
private predicate interestingCallableSink(DataFlowCallable c) {
exists(Node n | Config::isSink(n, _) and c = getNodeEnclosingCallable(n))
exists(Node n | c = getNodeEnclosingCallable(n) |
Config::isSink(n, _) or
Config::isSink(n)
)
or
exists(DataFlowCallable mid | interestingCallableSink(mid) and callableStep(c, mid))
}
@@ -3926,8 +3946,10 @@ module MakeImpl<DataFlowParameter Lang> {
or
exists(Node n |
ce2 = TCallableSink() and
Config::isSink(n, _) and
ce1 = TCallable(getNodeEnclosingCallable(n))
|
Config::isSink(n, _) or
Config::isSink(n)
)
}