mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
DataFlow: Add code for merging base with overlay.
This commit is contained in:
committed by
Alexander Eyers-Taylor
parent
c49e2ab2da
commit
3c110f2eb8
@@ -657,7 +657,7 @@ private module PathGraphSigMod {
|
||||
}
|
||||
}
|
||||
|
||||
module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
|
||||
module DataFlowMakeCore<LocationSig Location, InputSig<Location> Lang> {
|
||||
private import Lang
|
||||
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
|
||||
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
|
||||
@@ -1099,6 +1099,13 @@ 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
|
||||
}
|
||||
}
|
||||
|
||||
module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
|
||||
import DataFlowMakeCore<Location, Lang>
|
||||
private import Lang
|
||||
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
|
||||
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
|
||||
|
||||
/**
|
||||
* Constructs a global data flow computation.
|
||||
@@ -1157,3 +1164,71 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
|
||||
import Flow
|
||||
}
|
||||
}
|
||||
|
||||
module DataFlowMakeOverlay<LocationSig Location, InputSig<Location> Lang> {
|
||||
import DataFlowMakeCore<Location, Lang>
|
||||
private import Lang
|
||||
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
|
||||
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
|
||||
|
||||
/**
|
||||
* 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"
|
||||
}
|
||||
|
||||
predicate observeOverlayInformedIncrementalMode() {
|
||||
not Config::observeDiffInformedIncrementalMode()
|
||||
}
|
||||
}
|
||||
|
||||
private module Stage1 = ImplStage1<C>;
|
||||
|
||||
import Stage1::PartialFlow
|
||||
|
||||
private module Flow = OverlayImpl<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"
|
||||
}
|
||||
|
||||
predicate observeOverlayInformedIncrementalMode() {
|
||||
not Config::observeDiffInformedIncrementalMode()
|
||||
}
|
||||
}
|
||||
|
||||
private module Stage1 = ImplStage1<C>;
|
||||
|
||||
import Stage1::PartialFlow
|
||||
|
||||
private module Flow = OverlayImpl<C, Stage1::Stage1WithState>;
|
||||
|
||||
import Flow
|
||||
}
|
||||
}
|
||||
|
||||
@@ -47,16 +47,16 @@ signature module InputSig<LocationSig Location, DF::InputSig<Location> Lang> {
|
||||
/**
|
||||
* Construct the modules for taint-tracking analyses.
|
||||
*/
|
||||
module TaintFlowMake<
|
||||
private module TaintFlowMakeCore<
|
||||
LocationSig Location, DF::InputSig<Location> DataFlowLang,
|
||||
InputSig<Location, DataFlowLang> TaintTrackingLang>
|
||||
{
|
||||
private import TaintTrackingLang
|
||||
private import DF::DataFlowMake<Location, DataFlowLang> as DataFlow
|
||||
private import MakeImpl<Location, DataFlowLang> as DataFlowInternal
|
||||
private import MakeImplStage1<Location, DataFlowLang> as DataFlowInternalStage1
|
||||
import TaintTrackingLang
|
||||
import DF::DataFlowMakeCore<Location, DataFlowLang> as DataFlow
|
||||
import MakeImpl<Location, DataFlowLang> as DataFlowInternal
|
||||
import MakeImplStage1<Location, DataFlowLang> as DataFlowInternalStage1
|
||||
|
||||
private module AddTaintDefaults<DataFlowInternal::FullStateConfigSig Config> implements
|
||||
module AddTaintDefaults<DataFlowInternal::FullStateConfigSig Config> implements
|
||||
DataFlowInternal::FullStateConfigSig
|
||||
{
|
||||
import Config
|
||||
@@ -85,7 +85,7 @@ module TaintFlowMake<
|
||||
|
||||
signature int speculationLimitSig();
|
||||
|
||||
private module AddSpeculativeTaintSteps<
|
||||
module AddSpeculativeTaintSteps<
|
||||
DataFlowInternal::FullStateConfigSig Config, speculationLimitSig/0 speculationLimit> implements
|
||||
DataFlowInternal::FullStateConfigSig
|
||||
{
|
||||
@@ -153,6 +153,13 @@ module TaintFlowMake<
|
||||
state1.getState() = state2.getState()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
module TaintFlowMake<
|
||||
LocationSig Location, DF::InputSig<Location> DataFlowLang,
|
||||
InputSig<Location, DataFlowLang> TaintTrackingLang>
|
||||
{
|
||||
private import TaintFlowMakeCore<Location, DataFlowLang, TaintTrackingLang>
|
||||
|
||||
/**
|
||||
* Constructs a global taint tracking computation.
|
||||
@@ -288,7 +295,161 @@ module TaintFlowMake<
|
||||
|
||||
import Stage1::PartialFlow
|
||||
|
||||
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1WithState>;
|
||||
private module Flow = DataFlowInternal::OverlayImpl<C, Stage1::Stage1WithState>;
|
||||
|
||||
import Flow
|
||||
}
|
||||
}
|
||||
|
||||
module TaintFlowMakeOverlay<
|
||||
LocationSig Location, DF::InputSig<Location> DataFlowLang,
|
||||
InputSig<Location, DataFlowLang> TaintTrackingLang>
|
||||
{
|
||||
private import TaintFlowMakeCore<Location, DataFlowLang, TaintTrackingLang>
|
||||
|
||||
/**
|
||||
* 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"
|
||||
}
|
||||
|
||||
predicate observeOverlayInformedIncrementalMode() {
|
||||
not Config::observeDiffInformedIncrementalMode()
|
||||
}
|
||||
}
|
||||
|
||||
private module C implements DataFlowInternal::FullStateConfigSig {
|
||||
import AddTaintDefaults<Config0>
|
||||
}
|
||||
|
||||
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
|
||||
|
||||
import Stage1::PartialFlow
|
||||
|
||||
private module Flow = DataFlowInternal::OverlayImpl<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"
|
||||
}
|
||||
|
||||
predicate observeOverlayInformedIncrementalMode() {
|
||||
not Config::observeDiffInformedIncrementalMode()
|
||||
}
|
||||
}
|
||||
|
||||
private module C implements DataFlowInternal::FullStateConfigSig {
|
||||
import AddTaintDefaults<Config0>
|
||||
}
|
||||
|
||||
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
|
||||
|
||||
import Stage1::PartialFlow
|
||||
|
||||
private module Flow = DataFlowInternal::OverlayImpl<C, Stage1::Stage1WithState>;
|
||||
|
||||
import Flow
|
||||
}
|
||||
|
||||
/**
|
||||
* Constructs a global taint tracking computation that also allows a given
|
||||
* maximum number of speculative taint steps.
|
||||
*/
|
||||
module SpeculativeGlobal<DataFlow::ConfigSig Config, speculationLimitSig/0 speculationLimit>
|
||||
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"
|
||||
}
|
||||
|
||||
predicate observeOverlayInformedIncrementalMode() {
|
||||
not Config::observeDiffInformedIncrementalMode()
|
||||
}
|
||||
}
|
||||
|
||||
private module C implements DataFlowInternal::FullStateConfigSig {
|
||||
import AddTaintDefaults<AddSpeculativeTaintSteps<Config0, speculationLimit/0>>
|
||||
}
|
||||
|
||||
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 using flow state that also
|
||||
* allows a given maximum number of speculative taint steps.
|
||||
*/
|
||||
module SpeculativeGlobalWithState<
|
||||
DataFlow::StateConfigSig Config, speculationLimitSig/0 speculationLimit> 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"
|
||||
}
|
||||
|
||||
predicate observeOverlayInformedIncrementalMode() {
|
||||
not Config::observeDiffInformedIncrementalMode()
|
||||
}
|
||||
}
|
||||
|
||||
private module C implements DataFlowInternal::FullStateConfigSig {
|
||||
import AddTaintDefaults<AddSpeculativeTaintSteps<Config0, speculationLimit/0>>
|
||||
}
|
||||
|
||||
private module Stage1 = DataFlowInternalStage1::ImplStage1<C>;
|
||||
|
||||
import Stage1::PartialFlow
|
||||
|
||||
private module Flow = DataFlowInternal::OverlayImpl<C, Stage1::Stage1WithState>;
|
||||
|
||||
import Flow
|
||||
}
|
||||
|
||||
@@ -15,7 +15,7 @@ private import DataFlowImplStage1
|
||||
|
||||
module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
|
||||
private import Lang
|
||||
private import DataFlowMake<Location, Lang>
|
||||
private import DataFlowMakeCore<Location, Lang>
|
||||
private import MakeImplStage1<Location, Lang>
|
||||
private import DataFlowImplCommon::MakeImplCommon<Location, Lang>
|
||||
private import DataFlowImplCommonPublic
|
||||
@@ -179,6 +179,56 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Constructs a data flow computation given a full input configuration, and
|
||||
* an initial stage 1 pruning with merging of overlay and base results.
|
||||
*/
|
||||
module OverlayImpl<FullStateConfigSig Config, Stage1Output<Config::FlowState> Stage1> {
|
||||
module Base = Impl<Config, Stage1>;
|
||||
|
||||
import Base
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to `sink`.
|
||||
*
|
||||
* This is a local predicate that only has results local to the overlay/base database.
|
||||
*/
|
||||
predicate flowLocal(Node source, Node sink) = forceLocal(Base::flow/2)(source, sink)
|
||||
|
||||
/**
|
||||
* Holds if data can flow from `source` to `sink`.
|
||||
*/
|
||||
predicate flow(Node source, Node sink) {
|
||||
Base::flow(source, sink)
|
||||
or
|
||||
// If we are overlay informed (i.e. we are not diff-informed), we
|
||||
// merge in the local results which includes the base database results.
|
||||
flowLocal(source, sink) and Config::observeOverlayInformedIncrementalMode()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from some source to `sink`.
|
||||
* This predicate that only has results local to the overlay/base database.
|
||||
*/
|
||||
predicate flowToLocal(Node sink) = forceLocal(Base::flowTo/1)(sink)
|
||||
|
||||
/**
|
||||
* Holds if data can flow from some source to `sink`.
|
||||
*/
|
||||
predicate flowTo(Node sink) {
|
||||
Base::flowTo(sink)
|
||||
or
|
||||
// If we are overlay informed (i.e. we are not diff-informed), we
|
||||
// merge in the local results which includes the base database results.
|
||||
flowToLocal(sink) and Config::observeOverlayInformedIncrementalMode()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if data can flow from some source to `sink`.
|
||||
*/
|
||||
predicate flowToExpr(Lang::DataFlowExpr sink) { flowTo(exprNode(sink)) }
|
||||
}
|
||||
|
||||
/**
|
||||
* Constructs a data flow computation given a full input configuration, and
|
||||
* an initial stage 1 pruning.
|
||||
|
||||
Reference in New Issue
Block a user