hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-24 04:36:35 +01:00
Code Issues Packages Projects Releases Wiki Activity

C++: Add 'isAdditionalFlowStep' predicates for both configurations in the product dataflow library and use them to fix missing results in the 'cpp/overrun-write' query.

Browse Source
This commit is contained in:
Mathias Vorreiter Pedersen
2022-09-28 15:02:22 +01:00
parent ccbbb5754e
commit 769ff5c6f3
4 changed files with 94 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

87
cpp/ql/lib/experimental/semmle/code/cpp/dataflow/ProductFlow.qll
View File

@@ -20,7 +20,8 @@ module ProductFlow {
* `source1` and `source2` must belong to the same callable.
*/
predicate isSourcePair(
DataFlow::Node source1, string state1, DataFlow::Node source2, string state2
DataFlow::Node source1, DataFlow::FlowState state1, DataFlow::Node source2,
DataFlow::FlowState state2
) {
state1 = "" and
state2 = "" and
@@ -89,6 +90,49 @@ module ProductFlow {
*/
predicate isBarrierOut2(DataFlow::Node node) { none() }
/*
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
* the first projection of the product dataflow graph.
*/
predicate isAdditionalFlowStep1(DataFlow::Node node1, DataFlow::Node node2) { none() }
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
* the first projection of the product dataflow graph.
*
* This step is only applicable in `state1` and updates the flow state to `state2`.
*/
predicate isAdditionalFlowStep1(
DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
DataFlow::FlowState state2
) {
state1 instanceof DataFlow::FlowStateEmpty and
state2 instanceof DataFlow::FlowStateEmpty and
this.isAdditionalFlowStep1(node1, node2)
}
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
* the second projection of the product dataflow graph.
*/
predicate isAdditionalFlowStep2(DataFlow::Node node1, DataFlow::Node node2) { none() }
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
* the second projection of the product dataflow graph.
*
* This step is only applicable in `state1` and updates the flow state to `state2`.
*/
predicate isAdditionalFlowStep2(
DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
DataFlow::FlowState state2
) {
state1 instanceof DataFlow::FlowStateEmpty and
state2 instanceof DataFlow::FlowStateEmpty and
this.isAdditionalFlowStep2(node1, node2)
}
predicate hasFlowPath(
DataFlow::PathNode source1, DataFlow2::PathNode source2, DataFlow::PathNode sink1,
DataFlow2::PathNode sink2
@@ -103,46 +147,61 @@ module ProductFlow {
class Conf1 extends DataFlow::Configuration {
Conf1() { this = "Conf1" }
override predicate isSource(DataFlow::Node source, string state) {
override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
exists(Configuration conf | conf.isSourcePair(source, state, _, _))
}
override predicate isSink(DataFlow::Node sink, string state) {
override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) {
exists(Configuration conf | conf.isSinkPair(sink, state, _, _))
}
override predicate isBarrier(DataFlow::Node node, string state) {
override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
exists(Configuration conf | conf.isBarrier1(node, state))
}
override predicate isBarrierOut(DataFlow::Node node) {
exists(Configuration conf | conf.isBarrierOut1(node))
}
override predicate isAdditionalFlowStep(
DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
DataFlow::FlowState state2
) {
exists(Configuration conf | conf.isAdditionalFlowStep1(node1, state1, node2, state2))
}
}
class Conf2 extends DataFlow2::Configuration {
Conf2() { this = "Conf2" }
override predicate isSource(DataFlow::Node source, string state) {
exists(Configuration conf, DataFlow::Node source1 |
conf.isSourcePair(source1, _, source, state) and
any(Conf1 c).hasFlow(source1, _)
override predicate isSource(DataFlow::Node source, DataFlow::FlowState state) {
exists(Configuration conf, DataFlow::PathNode source1 |
conf.isSourcePair(source1.getNode(), source1.getState(), source, state) and
any(Conf1 c).hasFlowPath(source1, _)
)
}
override predicate isSink(DataFlow::Node sink, string state) {
exists(Configuration conf, DataFlow::Node sink1 |
conf.isSinkPair(sink1, _, sink, state) and any(Conf1 c).hasFlow(_, sink1)
override predicate isSink(DataFlow::Node sink, DataFlow::FlowState state) {
exists(Configuration conf, DataFlow::PathNode sink1 |
conf.isSinkPair(sink1.getNode(), sink1.getState(), sink, state) and
any(Conf1 c).hasFlowPath(_, sink1)
)
}
override predicate isBarrier(DataFlow::Node node, string state) {
override predicate isBarrier(DataFlow::Node node, DataFlow::FlowState state) {
exists(Configuration conf | conf.isBarrier2(node, state))
}
override predicate isBarrierOut(DataFlow::Node node) {
exists(Configuration conf | conf.isBarrierOut2(node))
}
override predicate isAdditionalFlowStep(
DataFlow::Node node1, DataFlow::FlowState state1, DataFlow::Node node2,
DataFlow::FlowState state2
) {
exists(Configuration conf | conf.isAdditionalFlowStep2(node1, state1, node2, state2))
}
}
}
@@ -150,7 +209,7 @@ module ProductFlow {
Configuration conf, DataFlow::PathNode source1, DataFlow2::PathNode source2,
DataFlow::PathNode node1, DataFlow2::PathNode node2
) {
conf.isSourcePair(node1.getNode(), _, node2.getNode(), _) and
conf.isSourcePair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState()) and
node1 = source1 and
node2 = source2
or
@@ -213,7 +272,7 @@ module ProductFlow {
) {
exists(DataFlow::PathNode mid1, DataFlow2::PathNode mid2 |
reachableInterprocEntry(conf, source1, source2, mid1, mid2) and
conf.isSinkPair(sink1.getNode(), _, sink2.getNode(), _) and
conf.isSinkPair(sink1.getNode(), sink1.getState(), sink2.getNode(), sink2.getState()) and
localPathStep1*(mid1, sink1) and
localPathStep2*(mid2, sink2)
)