C++: Update product flow to match data flow naming

This commit is contained in:
Jeroen Ketema
2023-03-24 09:15:41 +01:00
parent a38c3171dd
commit 9123657fd2
4 changed files with 13 additions and 13 deletions

View File

@@ -67,7 +67,7 @@ module ProductFlow {
default predicate isBarrierIn2(DataFlow::Node node) { none() }
}
module Make<ConfigSig Config> {
module Global<ConfigSig Config> {
private module StateConfig implements StateConfigSig {
class FlowState1 = Unit;
@@ -132,7 +132,7 @@ module ProductFlow {
predicate isBarrierIn2 = Config::isBarrierIn2/1;
}
import MakeWithState<StateConfig>
import GlobalWithState<StateConfig>
}
signature module StateConfigSig {
@@ -244,7 +244,7 @@ module ProductFlow {
default predicate isBarrierIn2(DataFlow::Node node) { none() }
}
module MakeWithState<StateConfigSig Config> {
module GlobalWithState<StateConfigSig Config> {
class PathNode1 = Flow1::PathNode;
class PathNode2 = Flow2::PathNode;
@@ -257,7 +257,7 @@ module ProductFlow {
class FlowState2 = Config::FlowState2;
predicate hasFlowPath(
predicate flowPath(
Flow1::PathNode source1, Flow2::PathNode source2, Flow1::PathNode sink1, Flow2::PathNode sink2
) {
reachable(source1, source2, sink1, sink2)
@@ -287,7 +287,7 @@ module ProductFlow {
predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn1(node) }
}
module Flow1 = DataFlow::MakeWithState<Config1>;
module Flow1 = DataFlow::GlobalWithState<Config1>;
module Config2 implements DataFlow::StateConfigSig {
class FlowState = FlowState2;
@@ -319,7 +319,7 @@ module ProductFlow {
predicate isBarrierIn(DataFlow::Node node) { Config::isBarrierIn2(node) }
}
module Flow2 = DataFlow::MakeWithState<Config2>;
module Flow2 = DataFlow::GlobalWithState<Config2>;
pragma[nomagic]
private predicate reachableInterprocEntry(

View File

@@ -61,7 +61,7 @@ module ArraySizeConfig implements ProductFlow::ConfigSig {
}
}
module ArraySizeFlow = ProductFlow::Make<ArraySizeConfig>;
module ArraySizeFlow = ProductFlow::Global<ArraySizeConfig>;
pragma[nomagic]
predicate isSinkPair1(
@@ -78,7 +78,7 @@ predicate isSinkPair1(
from
ArraySizeFlow::PathNode1 source1, ArraySizeFlow::PathNode2 source2,
ArraySizeFlow::PathNode1 sink1, ArraySizeFlow::PathNode2 sink2
where ArraySizeFlow::hasFlowPath(source1, source2, sink1, sink2)
where ArraySizeFlow::flowPath(source1, source2, sink1, sink2)
// TODO: pull delta out and display it
select sink1.getNode(), source1, sink1, "Off-by one error allocated at $@ bounded by $@.", source1,
source1.toString(), sink2, sink2.toString()

View File

@@ -132,14 +132,14 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
}
}
module StringSizeFlow = ProductFlow::MakeWithState<StringSizeConfig>;
module StringSizeFlow = ProductFlow::GlobalWithState<StringSizeConfig>;
from
StringSizeFlow::PathNode1 source1, StringSizeFlow::PathNode2 source2,
StringSizeFlow::PathNode1 sink1, StringSizeFlow::PathNode2 sink2, int overflow, int sinkState,
CallInstruction c, DataFlow::Node sourceNode, Expr buffer, string element
where
StringSizeFlow::hasFlowPath(source1, source2, sink1, sink2) and
StringSizeFlow::flowPath(source1, source2, sink1, sink2) and
sinkState = sink2.getState() and
isSinkPairImpl(c, sink1.getNode(), sink2.getNode(), overflow + sinkState, buffer) and
overflow > 0 and

View File

@@ -161,7 +161,7 @@ module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
}
}
module AllocToInvalidPointerFlow = ProductFlow::MakeWithState<AllocToInvalidPointerConfig>;
module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<AllocToInvalidPointerConfig>;
/**
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
@@ -246,7 +246,7 @@ predicate invalidPointerToDerefSource(
) {
exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 |
pragma[only_bind_out](p.getNode()) = sink1 and
AllocToInvalidPointerFlow::hasFlowPath(_, _, pragma[only_bind_into](p), _) and
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p), _) and
isSinkImpl(pai, sink1, _, _) and
bounded2(source.asInstruction(), pai, delta) and
delta >= 0
@@ -368,7 +368,7 @@ predicate hasFlowPath(
PointerArithmeticInstruction pai, string operation
) {
exists(InvalidPointerToDerefFlow::PathNode sink3, AllocToInvalidPointerFlow::PathNode1 sink1 |
AllocToInvalidPointerFlow::hasFlowPath(source1.asPathNode1(), _, sink1, _) and
AllocToInvalidPointerFlow::flowPath(source1.asPathNode1(), _, sink1, _) and
joinOn1(pai, sink1, source3) and
InvalidPointerToDerefFlow::flowPath(source3, sink3) and
joinOn2(sink3, sink.asSinkNode(), operation)