DataFlow: Rearrange files to group the parts that can be shared with overlay aware.

This commit is contained in:
Alex Eyers-Taylor
2025-09-18 18:46:11 +01:00
committed by Alexander Eyers-Taylor
parent 18e33b193e
commit 8c02130bcf
2 changed files with 115 additions and 115 deletions

View File

@@ -691,59 +691,6 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
predicate flowToExpr(DataFlowExpr sink);
}
/**
* Constructs a global data flow computation.
*/
module Global<ConfigSig Config> implements GlobalFlowSig {
private module C implements FullStateConfigSig {
import DefaultState<Config>
import Config
predicate accessPathLimit = Config::accessPathLimit/0;
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
}
private module Stage1 = ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = Impl<C, Stage1::Stage1NoState>;
import Flow
}
/**
* Constructs a global data flow computation using flow state.
*/
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
private module C implements FullStateConfigSig {
import Config
predicate accessPathLimit = Config::accessPathLimit/0;
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"
}
}
private module Stage1 = ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = Impl<C, Stage1::Stage1WithState>;
import Flow
}
signature class PathNodeSig {
/** Gets a textual representation of this element. */
string toString();
@@ -1140,4 +1087,57 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
// Re-export the PathGraph so the user can import a single module and get both PathNode and the query predicates
import PathGraph
}
/**
* Constructs a global data flow computation.
*/
module Global<ConfigSig Config> implements GlobalFlowSig {
private module C implements FullStateConfigSig {
import DefaultState<Config>
import Config
predicate accessPathLimit = Config::accessPathLimit/0;
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
}
private module Stage1 = ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = Impl<C, Stage1::Stage1NoState>;
import Flow
}
/**
* Constructs a global data flow computation using flow state.
*/
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
private module C implements FullStateConfigSig {
import Config
predicate accessPathLimit = Config::accessPathLimit/0;
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"
}
}
private module Stage1 = ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = Impl<C, Stage1::Stage1WithState>;
import Flow
}
}

View File

@@ -83,68 +83,6 @@ module TaintFlowMake<
}
}
/**
* Constructs a global taint tracking computation.
*/
module Global<DataFlow::ConfigSig Config> implements DataFlow::GlobalFlowSig {
private module Config0 implements DataFlowInternal::FullStateConfigSig {
import DataFlowInternal::DefaultState<Config>
import Config
predicate isAdditionalFlowStep(
DataFlowLang::Node node1, DataFlowLang::Node node2, string model
) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
}
private module C implements DataFlowInternal::FullStateConfigSig {
import AddTaintDefaults<Config0>
}
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1NoState>;
import Flow
}
/**
* Constructs a global taint tracking computation using flow state.
*/
module GlobalWithState<DataFlow::StateConfigSig Config> implements DataFlow::GlobalFlowSig {
private module Config0 implements DataFlowInternal::FullStateConfigSig {
import Config
predicate isAdditionalFlowStep(
DataFlowLang::Node node1, DataFlowLang::Node node2, string model
) {
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 {
import AddTaintDefaults<Config0>
}
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1WithState>;
import Flow
}
signature int speculationLimitSig();
private module AddSpeculativeTaintSteps<
@@ -216,6 +154,68 @@ module TaintFlowMake<
}
}
/**
* Constructs a global taint tracking computation.
*/
module Global<DataFlow::ConfigSig Config> implements DataFlow::GlobalFlowSig {
private module Config0 implements DataFlowInternal::FullStateConfigSig {
import DataFlowInternal::DefaultState<Config>
import Config
predicate isAdditionalFlowStep(
DataFlowLang::Node node1, DataFlowLang::Node node2, string model
) {
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
}
}
private module C implements DataFlowInternal::FullStateConfigSig {
import AddTaintDefaults<Config0>
}
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1NoState>;
import Flow
}
/**
* Constructs a global taint tracking computation using flow state.
*/
module GlobalWithState<DataFlow::StateConfigSig Config> implements DataFlow::GlobalFlowSig {
private module Config0 implements DataFlowInternal::FullStateConfigSig {
import Config
predicate isAdditionalFlowStep(
DataFlowLang::Node node1, DataFlowLang::Node node2, string model
) {
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 {
import AddTaintDefaults<Config0>
}
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
import Stage1::PartialFlow
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1WithState>;
import Flow
}
/**
* Constructs a global taint tracking computation that also allows a given
* maximum number of speculative taint steps.