Dataflow: Introduce NodeRegions for use in isUnreachableInCall.

This commit is contained in:
Anders Schack-Mulligen
2024-04-25 15:36:26 +02:00
parent 486eaad566
commit bc8ca1af86
12 changed files with 142 additions and 31 deletions

View File

@@ -251,10 +251,18 @@ signature module InputSig<LocationSig Location> {
*/
predicate expectsContent(Node n, ContentSet c);
/** A set of `Node`s in a `DataFlowCallable`. */
class NodeRegion {
/** Holds if this region contains `n`. */
predicate contains(Node n);
int totalOrder();
}
/**
* Holds if the node `n` is unreachable when the call context is `call`.
* Holds if the nodes in `nr` are unreachable when the call context is `call`.
*/
predicate isUnreachableInCall(Node n, DataFlowCall call);
predicate isUnreachableInCall(NodeRegion nr, DataFlowCall call);
default int accessPathLimit() { result = 5 }

View File

@@ -350,7 +350,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
pragma[nomagic]
private predicate isUnreachableInCall1(NodeEx n, LocalCallContextSpecificCall cc) {
isUnreachableInCallCached(n.asNode(), cc.getCall())
exists(NodeRegion nr |
nr.contains(n.asNode()) and
isUnreachableInCallCached(nr, cc.getCall())
)
}
/**
@@ -5245,7 +5248,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
TSummaryCtx2 sc2, TSummaryCtx3 sc3, TSummaryCtx4 sc4, DataFlowType t, PartialAccessPath ap,
boolean isStoreStep
) {
not isUnreachableInCallCached(node.asNode(), cc.(CallContextSpecificCall).getCall()) and
not exists(NodeRegion nr |
nr.contains(node.asNode()) and
isUnreachableInCallCached(nr, cc.(CallContextSpecificCall).getCall())
) and
(
localFlowStepEx(mid.getNodeEx(), node, _) and
state = mid.getState() and

View File

@@ -465,10 +465,10 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
*/
pragma[nomagic]
predicate recordDataFlowCallSiteUnreachable(DataFlowCall call, DataFlowCallable callable) {
exists(Node n |
exists(NodeRegion nr |
relevantCallEdgeIn(call, callable) and
getNodeEnclosingCallable(n) = callable and
isUnreachableInCallCached(n, call)
getNodeRegionEnclosingCallable(nr) = callable and
isUnreachableInCallCached(nr, call)
)
}
@@ -659,7 +659,9 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
predicate expectsContentCached(Node n, ContentSet c) { expectsContent(n, c) }
cached
predicate isUnreachableInCallCached(Node n, DataFlowCall call) { isUnreachableInCall(n, call) }
predicate isUnreachableInCallCached(NodeRegion nr, DataFlowCall call) {
isUnreachableInCall(nr, call)
}
cached
predicate outNodeExt(Node n) {
@@ -1823,8 +1825,14 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
override predicate relevantFor(DataFlowCallable callable) { relevantLocalCCtx(call, callable) }
}
private DataFlowCallable getNodeRegionEnclosingCallable(NodeRegion nr) {
exists(Node n | nr.contains(n) | getNodeEnclosingCallable(n) = result)
}
private predicate relevantLocalCCtx(DataFlowCall call, DataFlowCallable callable) {
exists(Node n | getNodeEnclosingCallable(n) = callable and isUnreachableInCallCached(n, call))
exists(NodeRegion nr |
getNodeRegionEnclosingCallable(nr) = callable and isUnreachableInCallCached(nr, call)
)
}
/**

View File

@@ -187,8 +187,9 @@ module MakeConsistency<
}
query predicate unreachableNodeCCtx(Node n, DataFlowCall call, string msg) {
isUnreachableInCall(n, call) and
exists(DataFlowCallable c |
exists(DataFlowCallable c, NodeRegion nr |
isUnreachableInCall(nr, call) and
nr.contains(n) and
c = nodeGetEnclosingCallable(n) and
not viableCallable(call) = c
) and