DataFlow: Adress comments on overlay informed dataflow

This commit is contained in:
Alex Eyers-Taylor
2025-10-03 20:39:41 +01:00
committed by Alexander Eyers-Taylor
parent 7a8d2392ee
commit 193cd46a76
4 changed files with 19 additions and 20 deletions

View File

@@ -657,10 +657,8 @@ private module PathGraphSigMod {
}
}
module DataFlowMakeCore<LocationSig Location, InputSig<Location> Lang> {
private module DataFlowMakeCore<LocationSig Location, InputSig<Location> Lang> {
private import Lang
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
import Configs<Location, Lang>
/**
@@ -1166,7 +1164,7 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
}
module DataFlowMakeOverlay<LocationSig Location, InputSig<Location> Lang> {
import DataFlowMakeCore<Location, Lang>
import DataFlowMake<Location, Lang>
private import Lang
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>

View File

@@ -52,7 +52,7 @@ private module TaintFlowMakeCore<
InputSig<Location, DataFlowLang> TaintTrackingLang>
{
import TaintTrackingLang
import DF::DataFlowMakeCore<Location, DataFlowLang> as DataFlow
import DF::DataFlowMake<Location, DataFlowLang> as DataFlow
import MakeImpl<Location, DataFlowLang> as DataFlowInternal
import MakeImplStage1<Location, DataFlowLang> as DataFlowInternalStage1
@@ -295,7 +295,7 @@ module TaintFlowMake<
import Stage1::PartialFlow
private module Flow = DataFlowInternal::OverlayImpl<C, Stage1::Stage1WithState>;
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1WithState>;
import Flow
}
@@ -407,7 +407,7 @@ module TaintFlowMakeOverlay<
import Stage1::PartialFlow
private module Flow = DataFlowInternal::Impl<C, Stage1::Stage1WithState>;
private module Flow = DataFlowInternal::OverlayImpl<C, Stage1::Stage1WithState>;
import Flow
}

View File

@@ -15,7 +15,7 @@ private import DataFlowImplStage1
module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private import Lang
private import DataFlowMakeCore<Location, Lang>
private import DataFlowMake<Location, Lang>
private import MakeImplStage1<Location, Lang>
private import DataFlowImplCommon::MakeImplCommon<Location, Lang>
private import DataFlowImplCommonPublic
@@ -145,7 +145,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
/**
* Holds if sources and sinks should be filtered to only include those that
* are in the overlay database. This only has an effect when running
* may lead to a flow path with either a source or a sink in the overlay database.
* This only has an effect when running
* in overlay-informed incremental mode. This should be used in conjunction
* with the `OverlayImpl` implementation to merge the base results back in.
*/
@@ -184,22 +185,22 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* 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>;
private module Flow = Impl<Config, Stage1>;
import Base
import Flow
/**
* 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)
private predicate flowLocal(Node source, Node sink) = forceLocal(Flow::flow/2)(source, sink)
/**
* Holds if data can flow from `source` to `sink`.
*/
predicate flow(Node source, Node sink) {
Base::flow(source, sink)
Flow::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.
@@ -208,15 +209,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
/**
* Holds if data can flow from some source to `sink`.
* This predicate that only has results local to the overlay/base database.
* This is a local predicate that only has results local to the overlay/base database.
*/
predicate flowToLocal(Node sink) = forceLocal(Base::flowTo/1)(sink)
predicate flowToLocal(Node sink) = forceLocal(Flow::flowTo/1)(sink)
/**
* Holds if data can flow from some source to `sink`.
*/
predicate flowTo(Node sink) {
Base::flowTo(sink)
Flow::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.

View File

@@ -149,17 +149,17 @@ module MakeImplStage1<LocationSig Location, InputSig<Location> Lang> {
*
* Shared between sources and sinks.
*/
pragma[inline]
overlay[global]
pragma[inline]
private predicate nonDiffInformedFilter(Node node) {
// If we are in base-only global evaluation, do not filter out any sources.
// If we are in base-only global evaluation, do not filter out any sources/sinks.
not isEvaluatingInOverlay()
or
// If the configuration doesn't merge overlays, do not filter out any sources.
// If the configuration doesn't merge overlays, do not filter out any sources/sinks.
not Config::observeOverlayInformedIncrementalMode()
or
// If we are in global evaluation with an overlay present, restrict
// sources to those visible in the overlay.
// sources/sinks to those visible in the overlay.
isOverlayNode(node)
}