Dataflow: add plumbing for adding provenance to state-steps.

This commit is contained in:
Anders Schack-Mulligen
2024-09-19 10:31:09 +02:00
parent bee073dee5
commit c80627a3d3
32 changed files with 256 additions and 121 deletions

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {

View File

@@ -676,6 +676,12 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
}
}
import Impl<C>

View File

@@ -63,7 +63,7 @@ module TaintFlowMake<
Config::isSink(node) or
Config::isSink(node, _) or
Config::isAdditionalFlowStep(node, _, _) or
Config::isAdditionalFlowStep(node, _, _, _)
Config::isAdditionalFlowStep(node, _, _, _, _)
) and
defaultImplicitTaintRead(node, c)
}
@@ -108,6 +108,13 @@ module TaintFlowMake<
) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
predicate isAdditionalFlowStep(
DataFlowLang::Node node1, FlowState state1, DataFlowLang::Node node2, FlowState state2,
string model
) {
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
}
}
private module C implements DataFlowInternal::FullStateConfigSig {

View File

@@ -73,7 +73,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
* This step is only applicable in `state1` and updates the flow state to `state2`.
*/
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2);
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
);
/**
* Holds if an arbitrary number of implicit read steps of content `c` may be
@@ -153,7 +155,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate isBarrierOut(Node node, FlowState state) { none() }
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
none()
}
}
@@ -357,12 +361,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
}
private predicate additionalLocalStateStep(
NodeEx node1, FlowState s1, NodeEx node2, FlowState s2
NodeEx node1, FlowState s1, NodeEx node2, FlowState s2, string model
) {
exists(Node n1, Node n2 |
node1.asNodeOrImplicitRead() = n1 and
node2.asNode() = n2 and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2,
model) and
getNodeEnclosingCallable(n1) = getNodeEnclosingCallable(n2) and
stateStepFilter(node1, s1, node2, s2)
)
@@ -395,11 +400,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}
private predicate additionalJumpStateStep(NodeEx node1, FlowState s1, NodeEx node2, FlowState s2) {
private predicate additionalJumpStateStep(
NodeEx node1, FlowState s1, NodeEx node2, FlowState s2, string model
) {
exists(Node n1, Node n2 |
node1.asNodeOrImplicitRead() = n1 and
node2.asNode() = n2 and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2) and
Config::isAdditionalFlowStep(pragma[only_bind_into](n1), s1, pragma[only_bind_into](n2), s2,
model) and
getNodeEnclosingCallable(n1) != getNodeEnclosingCallable(n2) and
stateStepFilter(node1, s1, node2, s2) and
not Config::getAFeature() instanceof FeatureEqualSourceSinkCallContext
@@ -530,13 +538,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(NodeEx mid | fwdFlow(mid, cc) |
localFlowStepEx(mid, node, _) or
additionalLocalFlowStep(mid, node, _) or
additionalLocalStateStep(mid, _, node, _)
additionalLocalStateStep(mid, _, node, _, _)
)
or
exists(NodeEx mid | fwdFlow(mid, _) and cc = false |
jumpStepEx(mid, node) or
additionalJumpStep(mid, node, _) or
additionalJumpStateStep(mid, _, node, _)
additionalJumpStateStep(mid, _, node, _, _)
)
or
// store
@@ -677,8 +685,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate stateStepFwd(FlowState state1, FlowState state2) {
exists(NodeEx node1 |
additionalLocalStateStep(node1, state1, _, state2) or
additionalJumpStateStep(node1, state1, _, state2)
additionalLocalStateStep(node1, state1, _, state2, _) or
additionalJumpStateStep(node1, state1, _, state2, _)
|
fwdFlow(node1)
)
@@ -723,13 +731,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(NodeEx mid | revFlow(mid, toReturn) |
localFlowStepEx(node, mid, _) or
additionalLocalFlowStep(node, mid, _) or
additionalLocalStateStep(node, _, mid, _)
additionalLocalStateStep(node, _, mid, _, _)
)
or
exists(NodeEx mid | revFlow(mid, _) and toReturn = false |
jumpStepEx(node, mid) or
additionalJumpStep(node, mid, _) or
additionalJumpStateStep(node, _, mid, _)
additionalJumpStateStep(node, _, mid, _, _)
)
or
// store
@@ -847,8 +855,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate stateStepRev(FlowState state1, FlowState state2) {
exists(NodeEx node1, NodeEx node2 |
additionalLocalStateStep(node1, state1, node2, state2) or
additionalJumpStateStep(node1, state1, node2, state2)
additionalLocalStateStep(node1, state1, node2, state2, _) or
additionalJumpStateStep(node1, state1, node2, state2, _)
|
revFlow(node1, _) and
revFlow(node2, _) and
@@ -1068,8 +1076,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
) {
Stage1::revFlow(node1) and
Stage1::revFlow(node2) and
additionalLocalStateStep(node1, state1, node2, state2) and
label = "Config" and
additionalLocalStateStep(node1, state1, node2, state2, label) and
t = node2.getDataFlowType() and
lcc.relevantFor(node1.getEnclosingCallable()) and
not isUnreachableInCall1(node1, lcc) and
@@ -1621,7 +1628,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
exists(NodeEx mid, FlowState state0 |
fwdFlow(mid, state0, _, _, _, ap, apa) and
additionalJumpStateStep(mid, state0, node, state) and
additionalJumpStateStep(mid, state0, node, state, _) and
t = getNodeTyp(node) and
ap instanceof ApNil
)
@@ -2286,7 +2293,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
or
exists(NodeEx mid, FlowState state0 |
additionalJumpStateStep(node, state, mid, state0) and
additionalJumpStateStep(node, state, mid, state0, _) and
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, ap) and
ap instanceof ApNil
)
@@ -2651,7 +2658,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
additionalJumpStep(_, node, _)
or
additionalJumpStateStep(_, _, node, state)
additionalJumpStateStep(_, _, node, state, _)
or
node instanceof ParamNodeEx
or
@@ -2699,9 +2706,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(NodeEx next, FlowState s |
revFlow(next, s, pragma[only_bind_into](ap)) and ap instanceof ApNil
|
additionalJumpStateStep(node, state, next, s)
additionalJumpStateStep(node, state, next, s, _)
or
additionalLocalStateStep(node, state, next, s) and
additionalLocalStateStep(node, state, next, s, _) and
s != state
)
or
@@ -3246,10 +3253,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
t = getNodeTyp(node) and
ap instanceof ApNil
or
additionalJumpStateStep(mid, state0, node, state) and
additionalJumpStateStep(mid, state0, node, state, label) and
t = getNodeTyp(node) and
ap instanceof ApNil and
label = "Config"
ap instanceof ApNil
)
or
// flow into a callable
@@ -4799,7 +4805,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
or
additionalJumpStep(node1, node2, _)
or
additionalJumpStateStep(node1, _, node2, _)
additionalJumpStateStep(node1, _, node2, _, _)
or
// flow into callable
viableParamArgEx(_, node2, node1)
@@ -4913,10 +4919,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate relevantState(FlowState state) {
sourceNode(_, state) or
sinkNodeWithState(_, state) or
additionalLocalStateStep(_, state, _, _) or
additionalLocalStateStep(_, _, _, state) or
additionalJumpStateStep(_, state, _, _) or
additionalJumpStateStep(_, _, _, state)
additionalLocalStateStep(_, state, _, _, _) or
additionalLocalStateStep(_, _, _, state, _) or
additionalJumpStateStep(_, state, _, _, _) or
additionalJumpStateStep(_, _, _, state, _)
}
private predicate revSinkNode(NodeEx node, FlowState state) {
@@ -5252,7 +5258,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
t = node.getDataFlowType() and
ap = TPartialNil()
or
additionalLocalStateStep(mid.getNodeEx(), mid.getState(), node, state) and
additionalLocalStateStep(mid.getNodeEx(), mid.getState(), node, state, _) and
cc = mid.getCallContext() and
sc1 = mid.getSummaryCtx1() and
sc2 = mid.getSummaryCtx2() and
@@ -5287,7 +5293,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ap = TPartialNil() and
isStoreStep = false
or
additionalJumpStateStep(mid.getNodeEx(), mid.getState(), node, state) and
additionalJumpStateStep(mid.getNodeEx(), mid.getState(), node, state, _) and
cc = callContextNone() and
sc1 = TSummaryCtx1None() and
sc2 = TSummaryCtx2None() and
@@ -5559,7 +5565,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ap = TPartialNil() and
isStoreStep = false
or
additionalLocalStateStep(node, state, mid.getNodeEx(), mid.getState()) and
additionalLocalStateStep(node, state, mid.getNodeEx(), mid.getState(), _) and
sc1 = mid.getSummaryCtx1() and
sc2 = mid.getSummaryCtx2() and
sc3 = mid.getSummaryCtx3() and
@@ -5584,7 +5590,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
ap = TPartialNil() and
isStoreStep = false
or
additionalJumpStateStep(node, state, mid.getNodeEx(), mid.getState()) and
additionalJumpStateStep(node, state, mid.getNodeEx(), mid.getState(), _) and
sc1 = TRevSummaryCtx1None() and
sc2 = TRevSummaryCtx2None() and
sc3 = TRevSummaryCtx3None() and

View File

@@ -261,13 +261,17 @@ deprecated private module Config implements FullStateConfigSig {
model = ""
}
predicate isAdditionalFlowStep(Node node1, FlowState state1, Node node2, FlowState state2) {
predicate isAdditionalFlowStep(
Node node1, FlowState state1, Node node2, FlowState state2, string model
) {
getConfig(state1).isAdditionalFlowStep(node1, getState(state1), node2, getState(state2)) and
getConfig(state2) = getConfig(state1)
getConfig(state2) = getConfig(state1) and
model = ""
or
not singleConfiguration() and
getConfig(state1).isAdditionalFlowStep(node1, node2) and
state2 = state1
state2 = state1 and
model = ""
}
predicate allowImplicitRead(Node node, ContentSet c) {