Merge pull request #13680 from jketema/product-default

C++: Add more default predicates to product flow
This commit is contained in:
Jeroen Ketema
2023-07-06 18:12:38 +02:00
committed by GitHub
4 changed files with 14 additions and 30 deletions

View File

@@ -0,0 +1,4 @@
---
category: feature
---
* The `ProductFlow::StateConfigSig` signature now includes default predicates for `isBarrier1`, `isBarrier2`, `isAdditionalFlowStep1`, and `isAdditionalFlowStep1`. Hence, it is no longer needed to provide `none()` implementations of these predicates if they are not needed.

View File

@@ -192,13 +192,13 @@ module ProductFlow {
* Holds if data flow through `node` is prohibited through the first projection of the product
* dataflow graph when the flow state is `state`.
*/
predicate isBarrier1(DataFlow::Node node, FlowState1 state);
default predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
/**
* Holds if data flow through `node` is prohibited through the second projection of the product
* dataflow graph when the flow state is `state`.
*/
predicate isBarrier2(DataFlow::Node node, FlowState2 state);
default predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
/**
* Holds if data flow through `node` is prohibited through the first projection of the product
@@ -237,9 +237,11 @@ module ProductFlow {
*
* This step is only applicable in `state1` and updates the flow state to `state2`.
*/
predicate isAdditionalFlowStep1(
default predicate isAdditionalFlowStep1(
DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
);
) {
none()
}
/**
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps in
@@ -253,9 +255,11 @@ module ProductFlow {
*
* This step is only applicable in `state1` and updates the flow state to `state2`.
*/
predicate isAdditionalFlowStep2(
default predicate isAdditionalFlowStep2(
DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
);
) {
none()
}
/**
* Holds if data flow into `node` is prohibited in the first projection of the product

View File

@@ -248,20 +248,10 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
)
}
predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
predicate isBarrier2(DataFlow::Node node, FlowState2 state) { none() }
predicate isBarrierOut2(DataFlow::Node node) {
node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
}
predicate isAdditionalFlowStep1(
DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
) {
none()
}
predicate isAdditionalFlowStep2(
DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
) {

View File

@@ -196,8 +196,6 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
isSinkImpl(_, sink1, sink2, state2)
}
predicate isBarrier1(DataFlow::Node node, FlowState1 state) { none() }
predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
node = Barrier2::getABarrierNode(state)
}
@@ -207,18 +205,6 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
predicate isBarrierOut2(DataFlow::Node node) {
node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
}
predicate isAdditionalFlowStep1(
DataFlow::Node node1, FlowState1 state1, DataFlow::Node node2, FlowState1 state2
) {
none()
}
predicate isAdditionalFlowStep2(
DataFlow::Node node1, FlowState2 state1, DataFlow::Node node2, FlowState2 state2
) {
none()
}
}
module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<AllocToInvalidPointerConfig>;