Cpp: Replace sink inlining with a forward scan from source.

This commit is contained in:
Anders Schack-Mulligen
2024-09-24 15:26:35 +02:00
parent 590e93d8ed
commit 3a1b618a74
2 changed files with 42 additions and 6 deletions

View File

@@ -160,6 +160,26 @@ private module InvalidPointerToDerefBarrier {
}
}
/**
* BEWARE: This configuration uses an unrestricted sink, so accessing its full
* flow computation or any stages beyond the first 2 will likely diverge.
* Stage 1 will still be fast and we use it to restrict the subsequent sink
* computation.
*/
private module InvalidPointerReachesConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) { invalidPointerToDerefSource(_, _, source) }
predicate isSink(DataFlow::Node sink) { any() }
predicate isBarrier(DataFlow::Node node) { InvalidPointerToDerefConfig::isBarrier(node) }
int fieldFlowBranchLimit() { result = invalidPointerToDereferenceFieldFlowBranchLimit() }
}
private module InvalidPointerReachesFlow = DataFlow::Global<InvalidPointerReachesConfig>;
private import semmle.code.cpp.ir.dataflow.internal.DataFlowImplCommon as DataFlowImplCommon
/**
* A configuration to track flow from a pointer-arithmetic operation found
* by `AllocToInvalidPointerConfig` to a dereference of the pointer.
@@ -173,8 +193,13 @@ private module InvalidPointerToDerefConfig implements DataFlow::StateConfigSig {
invalidPointerToDerefSource(_, pai, source)
}
pragma[inline]
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _, _, _) }
predicate isSink(DataFlow::Node sink) {
exists(DataFlowImplCommon::NodeEx n |
InvalidPointerReachesFlow::Stages::Stage1::sinkNode(n, _) and
n.asNode() = sink and
isInvalidPointerDerefSink(sink, _, _, _, _)
)
}
predicate isSink(DataFlow::Node sink, FlowState pai) { none() }

View File

@@ -2773,8 +2773,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
}
/**
* INTERNAL: Only for debugging.
*
* Provides a graph representation of the data flow in this stage suitable for use in a `path-problem` query.
*/
additional module Graph {
@@ -4634,6 +4632,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
*/
predicate stageStats = Debug::stageStats/10;
private module Stage1alias = Stage1;
private module Stage2alias = Stage2;
private module Stage3alias = Stage3;
@@ -4643,11 +4643,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private module Stage5alias = Stage5;
/**
* INTERNAL: Only for debugging.
* INTERNAL: Subject to change without notice.
*
* Contains references to individual pruning stages.
*/
module Debug {
module Stages {
module Stage1 = Stage1alias;
module Stage2 = Stage2alias;
module Stage3 = Stage3alias;
@@ -4655,6 +4657,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
module Stage4 = Stage4alias;
module Stage5 = Stage5alias;
}
/**
* INTERNAL: Only for debugging.
*
* Contains references to individual pruning stages and stage statistics.
*/
module Debug {
import Stages
predicate stageStats1(
int n, string stage, int nodes, int fields, int conscand, int states, int tuples,