mirror of
https://github.com/github/codeql.git
synced 2026-07-09 13:35:38 +02:00
1244 lines
45 KiB
Plaintext
1244 lines
45 KiB
Plaintext
/**
|
|
* Provides an implementation of global (interprocedural) data flow. This file
|
|
* adds a global analysis, mainly exposed through the `Global` and `GlobalWithState`
|
|
* modules.
|
|
*/
|
|
overlay[local?]
|
|
module;
|
|
|
|
private import codeql.util.Location
|
|
|
|
/** Provides language-specific data flow parameters. */
|
|
signature module InputSig<LocationSig Location> {
|
|
/**
|
|
* A node in the data flow graph.
|
|
*/
|
|
class Node {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
|
|
/** Gets the location of this node. */
|
|
Location getLocation();
|
|
}
|
|
|
|
class ParameterNode extends Node;
|
|
|
|
class ArgumentNode extends Node;
|
|
|
|
class ReturnNode extends Node {
|
|
ReturnKind getKind();
|
|
}
|
|
|
|
/**
|
|
* A node in the data flow graph that represents an output of a call.
|
|
*/
|
|
class OutNode extends Node;
|
|
|
|
/**
|
|
* A node in the data flow graph representing the value of some other node
|
|
* after an operation that might have changed its state. A typical example is
|
|
* an argument, which may have been modified by the callee. For example,
|
|
* consider the following code calling a setter method:
|
|
* ```
|
|
* x.setFoo(y);
|
|
* ```
|
|
* The post-update node for the argument node `x` is the node representing the
|
|
* value of `x` after the field `foo` has been updated.
|
|
*/
|
|
class PostUpdateNode extends Node {
|
|
/**
|
|
* Gets the pre-update node, that is, the node that represents the same
|
|
* value prior to the operation.
|
|
*/
|
|
Node getPreUpdateNode();
|
|
}
|
|
|
|
class CastNode extends Node;
|
|
|
|
predicate isParameterNode(ParameterNode p, DataFlowCallable c, ParameterPosition pos);
|
|
|
|
predicate isArgumentNode(ArgumentNode n, DataFlowCall call, ArgumentPosition pos);
|
|
|
|
DataFlowCallable nodeGetEnclosingCallable(Node node);
|
|
|
|
DataFlowType getNodeType(Node node);
|
|
|
|
/**
|
|
* Gets a special type to use for parameter node `p` belonging to callables with a
|
|
* source node where a source call context `FlowFeature` is used, if any.
|
|
*
|
|
* This can be used to prevent lambdas from being resolved, when a concrete call
|
|
* context is needed. Example:
|
|
*
|
|
* ```csharp
|
|
* void Foo(Action<string> a)
|
|
* {
|
|
* var x = Source();
|
|
* a(x); // (1)
|
|
* a = s => Sink(s); // (2)
|
|
* a(x); // (3)
|
|
* }
|
|
*
|
|
* void Bar()
|
|
* {
|
|
* Foo(s => Sink(s)); // (4)
|
|
* }
|
|
* ```
|
|
*
|
|
* If a source call context flow feature is used, `a` can be assigned a special
|
|
* type that is incompatible with the type of _any_ lambda expression, which will
|
|
* prevent the call edge from (1) to (4). Note that the call edge from (3) to (2)
|
|
* will still be valid.
|
|
*/
|
|
default DataFlowType getSourceContextParameterNodeType(Node p) { none() }
|
|
|
|
predicate nodeIsHidden(Node node);
|
|
|
|
class DataFlowExpr;
|
|
|
|
/** Gets the node corresponding to `e`. */
|
|
Node exprNode(DataFlowExpr e);
|
|
|
|
class DataFlowCall {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
|
|
/** Gets the location of this call. */
|
|
Location getLocation();
|
|
|
|
DataFlowCallable getEnclosingCallable();
|
|
}
|
|
|
|
class DataFlowCallable {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
|
|
/** Gets the location of this callable. */
|
|
Location getLocation();
|
|
}
|
|
|
|
class ReturnKind {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
}
|
|
|
|
/** Gets a viable implementation of the target of the given `Call`. */
|
|
DataFlowCallable viableCallable(DataFlowCall c);
|
|
|
|
/**
|
|
* Holds if the set of viable implementations that can be called by `call`
|
|
* might be improved by knowing the call context.
|
|
*/
|
|
default predicate mayBenefitFromCallContext(DataFlowCall call) { none() }
|
|
|
|
/**
|
|
* Gets a viable dispatch target of `call` in the context `ctx`. This is
|
|
* restricted to those `call`s for which a context might make a difference.
|
|
*/
|
|
default DataFlowCallable viableImplInCallContext(DataFlowCall call, DataFlowCall ctx) { none() }
|
|
|
|
/**
|
|
* Gets a node that can read the value returned from `call` with return kind
|
|
* `kind`.
|
|
*/
|
|
OutNode getAnOutNode(DataFlowCall call, ReturnKind kind);
|
|
|
|
/**
|
|
* A type for a data flow node.
|
|
*
|
|
* This may or may not coincide with any type system existing for the source
|
|
* language, but should minimally include unique types for individual closure
|
|
* expressions (typically lambdas).
|
|
*/
|
|
class DataFlowType {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
}
|
|
|
|
/**
|
|
* Holds if `t1` and `t2` are compatible types.
|
|
*
|
|
* This predicate must be symmetric and reflexive.
|
|
*
|
|
* This predicate is used in the following way: If the data flow library
|
|
* tracks an object from node `n1` to `n2` using solely value-preserving
|
|
* steps, then it will check that the types of `n1` and `n2` are compatible.
|
|
* If they are not, then flow will be blocked.
|
|
*/
|
|
predicate compatibleTypes(DataFlowType t1, DataFlowType t2);
|
|
|
|
/**
|
|
* Holds if `t1` is strictly stronger than `t2`. That is, `t1` is a strict
|
|
* subtype of `t2`.
|
|
*
|
|
* This predicate must be transitive and imply `compatibleTypes(t1, t2)`.
|
|
*/
|
|
predicate typeStrongerThan(DataFlowType t1, DataFlowType t2);
|
|
|
|
class Content {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
}
|
|
|
|
/**
|
|
* Holds if access paths with `c` at their head always should be tracked at
|
|
* high precision. This disables adaptive access path precision for such
|
|
* access paths. This may be beneficial for content that indicates an
|
|
* element of an array or container.
|
|
*/
|
|
predicate forceHighPrecision(Content c);
|
|
|
|
/**
|
|
* An entity that represents a set of `Content`s.
|
|
*
|
|
* The set may be interpreted differently depending on whether it is
|
|
* stored into (`getAStoreContent`) or read from (`getAReadContent`).
|
|
*/
|
|
class ContentSet {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
|
|
/** Gets a content that may be stored into when storing into this set. */
|
|
Content getAStoreContent();
|
|
|
|
/** Gets a content that may be read from when reading from this set. */
|
|
Content getAReadContent();
|
|
}
|
|
|
|
/**
|
|
* A content approximation. A content approximation corresponds to one or
|
|
* more `Content`s, and is used to provide an in-between level of precision
|
|
* for pruning.
|
|
*/
|
|
class ContentApprox {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
}
|
|
|
|
/**
|
|
* Gets the content approximation for content `c`.
|
|
*/
|
|
ContentApprox getContentApprox(Content c);
|
|
|
|
class ParameterPosition {
|
|
/** Gets a textual representation of this element. */
|
|
bindingset[this]
|
|
string toString();
|
|
}
|
|
|
|
class ArgumentPosition {
|
|
/** Gets a textual representation of this element. */
|
|
bindingset[this]
|
|
string toString();
|
|
}
|
|
|
|
/**
|
|
* Holds if the parameter position `ppos` matches the argument position
|
|
* `apos`.
|
|
*/
|
|
predicate parameterMatch(ParameterPosition ppos, ArgumentPosition apos);
|
|
|
|
/**
|
|
* Holds if there is a simple local flow step from `node1` to `node2`. These
|
|
* are the value-preserving intra-callable flow steps.
|
|
*/
|
|
predicate simpleLocalFlowStep(Node node1, Node node2, string model);
|
|
|
|
/**
|
|
* Holds if the data-flow step from `node1` to `node2` can be used to
|
|
* determine where side-effects may return from a callable.
|
|
*/
|
|
bindingset[node1, node2]
|
|
default predicate validParameterAliasStep(Node node1, Node node2) { any() }
|
|
|
|
/**
|
|
* Holds if data can flow from `node1` to `node2` through a non-local step
|
|
* that does not follow a call edge. For example, a step through a global
|
|
* variable.
|
|
*/
|
|
predicate jumpStep(Node node1, Node node2);
|
|
|
|
/**
|
|
* Holds if data can flow from `node1` to `node2` via a read of `c`. Thus,
|
|
* `node1` references an object with a content `c.getAReadContent()` whose
|
|
* value ends up in `node2`.
|
|
*/
|
|
predicate readStep(Node node1, ContentSet c, Node node2);
|
|
|
|
/**
|
|
* Holds if data can flow from `node1` to `node2` via a store into `c`. Thus,
|
|
* `node2` references an object with a content `c.getAStoreContent()` that
|
|
* contains the value of `node1`.
|
|
*/
|
|
predicate storeStep(Node node1, ContentSet c, Node node2);
|
|
|
|
/**
|
|
* Holds if values stored inside content `c` are cleared at node `n`. For example,
|
|
* any value stored inside `f` is cleared at the pre-update node associated with `x`
|
|
* in `x.f = newValue`.
|
|
*/
|
|
predicate clearsContent(Node n, ContentSet c);
|
|
|
|
/**
|
|
* Holds if the value that is being tracked is expected to be stored inside content `c`
|
|
* at node `n`.
|
|
*/
|
|
predicate expectsContent(Node n, ContentSet c);
|
|
|
|
/** A set of `Node`s in a `DataFlowCallable`. */
|
|
class NodeRegion {
|
|
/** Holds if this region contains `n`. */
|
|
predicate contains(Node n);
|
|
}
|
|
|
|
/**
|
|
* Holds if the nodes in `nr` are unreachable when the call context is `call`.
|
|
*/
|
|
predicate isUnreachableInCall(NodeRegion nr, DataFlowCall call);
|
|
|
|
default int accessPathLimit() { result = 5 }
|
|
|
|
/**
|
|
* Holds if flow is allowed to pass from parameter `p` and back to itself as a
|
|
* side-effect, resulting in a summary from `p` to itself.
|
|
*
|
|
* One example would be to allow flow like `p.foo = p.bar;`, which is disallowed
|
|
* by default as a heuristic.
|
|
*/
|
|
predicate allowParameterReturnInSelf(ParameterNode p);
|
|
|
|
/**
|
|
* Holds if the value of `node2` is given by `node1`.
|
|
*
|
|
* This predicate is combined with type information in the following way: If
|
|
* the data flow library is able to compute an improved type for `node1` then
|
|
* it will also conclude that this type applies to `node2`. Vice versa, if
|
|
* `node2` must be visited along a flow path, then any type known for `node2`
|
|
* must also apply to `node1`.
|
|
*/
|
|
predicate localMustFlowStep(Node node1, Node node2);
|
|
|
|
class LambdaCallKind;
|
|
|
|
/** Holds if `creation` is an expression that creates a lambda of kind `kind` for `c`. */
|
|
predicate lambdaCreation(Node creation, LambdaCallKind kind, DataFlowCallable c);
|
|
|
|
/** Holds if `call` is a lambda call of kind `kind` where `receiver` is the lambda expression. */
|
|
predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver);
|
|
|
|
/** Extra data-flow steps needed for lambda flow analysis. */
|
|
predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue);
|
|
|
|
predicate knownSourceModel(Node source, string model);
|
|
|
|
predicate knownSinkModel(Node sink, string model);
|
|
|
|
/**
|
|
* Holds if `n` should never be skipped over in the `PathGraph` and in path
|
|
* explanations.
|
|
*/
|
|
default predicate neverSkipInPathGraph(Node n) { none() }
|
|
|
|
/**
|
|
* Gets an additional term that is added to the `join` and `branch` computations to reflect
|
|
* an additional forward or backwards branching factor that is not taken into account
|
|
* when calculating the (virtual) dispatch cost.
|
|
*
|
|
* Argument `arg` is part of a path from a source to a sink, and `p` is the target parameter.
|
|
*/
|
|
default int getAdditionalFlowIntoCallNodeTerm(ArgumentNode arg, ParameterNode p) { none() }
|
|
|
|
/**
|
|
* A second-level control-flow scope in a callable.
|
|
*
|
|
* This is used to provide a more fine-grained separation of a callable
|
|
* context for the purpose of identifying uncertain control flow. For most
|
|
* languages, this is not needed, as this separation is handled through
|
|
* virtual dispatch, but for some cases (for example, C++) this can be used to
|
|
* identify, for example, large top-level switch statements acting like
|
|
* virtual dispatch.
|
|
*/
|
|
class DataFlowSecondLevelScope {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
}
|
|
|
|
/** Gets the second-level scope containing the node `n`, if any. */
|
|
default DataFlowSecondLevelScope getSecondLevelScope(Node n) { none() }
|
|
|
|
bindingset[call, p, arg]
|
|
default predicate golangSpecificParamArgFilter(
|
|
DataFlowCall call, ParameterNode p, ArgumentNode arg
|
|
) {
|
|
any()
|
|
}
|
|
|
|
/** Gets the default value for the `fieldFlowBranchLimit` */
|
|
default int defaultFieldFlowBranchLimit() { result = 2 }
|
|
|
|
/** Holds if `fieldFlowBranchLimit` should be ignored for flow going into/out of `c`. */
|
|
default predicate ignoreFieldFlowBranchLimit(DataFlowCallable c) { none() }
|
|
|
|
/**
|
|
* Holds if the evaluator is currently evaluating with an overlay. The
|
|
* implementation of this predicate needs to be `overlay[local]`. For a
|
|
* language with no overlay support, `none()` is a valid implementation.
|
|
*
|
|
* When called from a local predicate, this predicate holds if we are in the
|
|
* overlay-only local evaluation. When called from a global predicate, this
|
|
* predicate holds if we are evaluating globally with overlay and base both
|
|
* visible.
|
|
*/
|
|
default predicate isEvaluatingInOverlay() { none() }
|
|
}
|
|
|
|
module Configs<LocationSig Location, InputSig<Location> Lang> {
|
|
private import Lang
|
|
private import internal.DataFlowImplCommon::MakeImplCommon<Location, Lang>
|
|
import DataFlowImplCommonPublic
|
|
|
|
/** An input configuration for data flow. */
|
|
signature module ConfigSig {
|
|
/**
|
|
* Holds if `source` is a relevant data flow source.
|
|
*/
|
|
predicate isSource(Node source);
|
|
|
|
/**
|
|
* Holds if `sink` is a relevant data flow sink.
|
|
*/
|
|
predicate isSink(Node sink);
|
|
|
|
/**
|
|
* Holds if data flow through `node` is prohibited. This completely removes
|
|
* `node` from the data flow graph.
|
|
*/
|
|
default predicate isBarrier(Node node) { none() }
|
|
|
|
/** Holds if data flow into `node` is prohibited. */
|
|
default predicate isBarrierIn(Node node) { none() }
|
|
|
|
/** Holds if data flow out of `node` is prohibited. */
|
|
default predicate isBarrierOut(Node node) { none() }
|
|
|
|
/**
|
|
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
|
|
*/
|
|
default predicate isAdditionalFlowStep(Node node1, Node node2) { none() }
|
|
|
|
/**
|
|
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
|
* taken at `node`.
|
|
*/
|
|
default predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
|
|
|
/**
|
|
* Holds if `node` should never be skipped over in the `PathGraph` and in path
|
|
* explanations.
|
|
*/
|
|
default predicate neverSkip(Node node) {
|
|
isAdditionalFlowStep(node, _) or isAdditionalFlowStep(_, node)
|
|
}
|
|
|
|
/**
|
|
* Gets the virtual dispatch branching limit when calculating field flow.
|
|
* This can be overridden to a smaller value to improve performance (a
|
|
* value of 0 disables field flow), or a larger value to get more results.
|
|
*/
|
|
default int fieldFlowBranchLimit() { result = Lang::defaultFieldFlowBranchLimit() }
|
|
|
|
/** Gets the access path limit. */
|
|
default int accessPathLimit() { result = Lang::accessPathLimit() }
|
|
|
|
/**
|
|
* Gets a data flow configuration feature to add restrictions to the set of
|
|
* valid flow paths.
|
|
*
|
|
* - `FeatureHasSourceCallContext`:
|
|
* Assume that sources have some existing call context to disallow
|
|
* conflicting return-flow directly following the source.
|
|
* - `FeatureHasSinkCallContext`:
|
|
* Assume that sinks have some existing call context to disallow
|
|
* conflicting argument-to-parameter flow directly preceding the sink.
|
|
* - `FeatureEqualSourceSinkCallContext`:
|
|
* Implies both of the above and additionally ensures that the entire flow
|
|
* path preserves the call context.
|
|
*
|
|
* These features are generally not relevant for typical end-to-end data flow
|
|
* queries, but should only be used for constructing paths that need to
|
|
* somehow be pluggable in another path context.
|
|
*/
|
|
default FlowFeature getAFeature() { none() }
|
|
|
|
/**
|
|
* Holds if hidden nodes should be included in the data flow graph.
|
|
*
|
|
* This feature should only be used for debugging or when the data flow graph
|
|
* is not visualized (as it is in a `path-problem` query).
|
|
*/
|
|
default predicate includeHiddenNodes() { none() }
|
|
|
|
/**
|
|
* Holds if sources and sinks should be filtered to only include those that
|
|
* may lead to a flow path with either a source or a sink in the location
|
|
* range given by `AlertFiltering`. This only has an effect when running
|
|
* in diff-informed incremental mode.
|
|
*
|
|
* This flag should only be applied to flow configurations whose results
|
|
* are used directly in a query result.
|
|
*/
|
|
default predicate observeDiffInformedIncrementalMode() { none() }
|
|
|
|
/**
|
|
* Gets a location that will be associated with the given `source` in a
|
|
* diff-informed query that uses this configuration (see
|
|
* `observeDiffInformedIncrementalMode`). By default, this is the location
|
|
* of the source itself, but this predicate should include any locations
|
|
* that are reported as the primary-location of the query or as an
|
|
* additional location ("$@" interpolation). Queries with `@kind path-problem`
|
|
* that override this predicate should also return the location of the source
|
|
* itself. For a query that doesn't report the source at all, this predicate
|
|
* should be `none()`.
|
|
*/
|
|
default Location getASelectedSourceLocation(Node source) { result = source.getLocation() }
|
|
|
|
/**
|
|
* Gets a location that will be associated with the given `sink` in a
|
|
* diff-informed query that uses this configuration (see
|
|
* `observeDiffInformedIncrementalMode`). By default, this is the location
|
|
* of the sink itself, but this predicate should include any locations
|
|
* that are reported as the primary-location of the query or as an
|
|
* additional location ("$@" interpolation). Queries with `@kind path-problem`
|
|
* that override this predicate should also return the location of the sink
|
|
* itself. For a query that doesn't report the sink at all, this predicate
|
|
* should be `none()`.
|
|
*/
|
|
default Location getASelectedSinkLocation(Node sink) { result = sink.getLocation() }
|
|
}
|
|
|
|
/** An input configuration for data flow using flow state. */
|
|
signature module StateConfigSig {
|
|
bindingset[this]
|
|
class FlowState;
|
|
|
|
/**
|
|
* Holds if `source` is a relevant data flow source with the given initial
|
|
* `state`.
|
|
*/
|
|
predicate isSource(Node source, FlowState state);
|
|
|
|
/**
|
|
* Holds if `sink` is a relevant data flow sink accepting `state`.
|
|
*/
|
|
predicate isSink(Node sink, FlowState state);
|
|
|
|
/**
|
|
* Holds if `sink` is a relevant data flow sink for any state.
|
|
*/
|
|
default predicate isSink(Node sink) { none() }
|
|
|
|
/**
|
|
* Holds if data flow through `node` is prohibited. This completely removes
|
|
* `node` from the data flow graph.
|
|
*/
|
|
default predicate isBarrier(Node node) { none() }
|
|
|
|
/**
|
|
* Holds if data flow through `node` is prohibited when the flow state is
|
|
* `state`.
|
|
*/
|
|
default predicate isBarrier(Node node, FlowState state) { none() }
|
|
|
|
/** Holds if data flow into `node` is prohibited. */
|
|
default predicate isBarrierIn(Node node) { none() }
|
|
|
|
/** Holds if data flow into `node` is prohibited when the target flow state is `state`. */
|
|
default predicate isBarrierIn(Node node, FlowState state) { none() }
|
|
|
|
/** Holds if data flow out of `node` is prohibited. */
|
|
default predicate isBarrierOut(Node node) { none() }
|
|
|
|
/** Holds if data flow out of `node` is prohibited when the originating flow state is `state`. */
|
|
default predicate isBarrierOut(Node node, FlowState state) { none() }
|
|
|
|
/**
|
|
* Holds if data may flow from `node1` to `node2` in addition to the normal data-flow steps.
|
|
*/
|
|
default predicate isAdditionalFlowStep(Node node1, Node node2) { none() }
|
|
|
|
/**
|
|
* 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`.
|
|
*/
|
|
default predicate isAdditionalFlowStep(
|
|
Node node1, FlowState state1, Node node2, FlowState state2
|
|
) {
|
|
none()
|
|
}
|
|
|
|
/**
|
|
* Holds if an arbitrary number of implicit read steps of content `c` may be
|
|
* taken at `node`.
|
|
*/
|
|
default predicate allowImplicitRead(Node node, ContentSet c) { none() }
|
|
|
|
/**
|
|
* Holds if `node` should never be skipped over in the `PathGraph` and in path
|
|
* explanations.
|
|
*/
|
|
default predicate neverSkip(Node node) {
|
|
isAdditionalFlowStep(node, _) or
|
|
isAdditionalFlowStep(_, node) or
|
|
isAdditionalFlowStep(node, _, _, _) or
|
|
isAdditionalFlowStep(_, _, node, _)
|
|
}
|
|
|
|
/**
|
|
* Gets the virtual dispatch branching limit when calculating field flow.
|
|
* This can be overridden to a smaller value to improve performance (a
|
|
* value of 0 disables field flow), or a larger value to get more results.
|
|
*/
|
|
default int fieldFlowBranchLimit() { result = Lang::defaultFieldFlowBranchLimit() }
|
|
|
|
/** Gets the access path limit. */
|
|
default int accessPathLimit() { result = Lang::accessPathLimit() }
|
|
|
|
/**
|
|
* Gets a data flow configuration feature to add restrictions to the set of
|
|
* valid flow paths.
|
|
*
|
|
* - `FeatureHasSourceCallContext`:
|
|
* Assume that sources have some existing call context to disallow
|
|
* conflicting return-flow directly following the source.
|
|
* - `FeatureHasSinkCallContext`:
|
|
* Assume that sinks have some existing call context to disallow
|
|
* conflicting argument-to-parameter flow directly preceding the sink.
|
|
* - `FeatureEqualSourceSinkCallContext`:
|
|
* Implies both of the above and additionally ensures that the entire flow
|
|
* path preserves the call context.
|
|
*
|
|
* These features are generally not relevant for typical end-to-end data flow
|
|
* queries, but should only be used for constructing paths that need to
|
|
* somehow be pluggable in another path context.
|
|
*/
|
|
default FlowFeature getAFeature() { none() }
|
|
|
|
/**
|
|
* Holds if hidden nodes should be included in the data flow graph.
|
|
*
|
|
* This feature should only be used for debugging or when the data flow graph
|
|
* is not visualized (as it is in a `path-problem` query).
|
|
*/
|
|
default predicate includeHiddenNodes() { none() }
|
|
|
|
/**
|
|
* Holds if sources and sinks should be filtered to only include those that
|
|
* may lead to a flow path with either a source or a sink in the location
|
|
* range given by `AlertFiltering`. This only has an effect when running
|
|
* in diff-informed incremental mode.
|
|
*
|
|
* This flag should only be applied to flow configurations whose results
|
|
* are used directly in a query result.
|
|
*/
|
|
default predicate observeDiffInformedIncrementalMode() { none() }
|
|
|
|
/**
|
|
* Gets a location that will be associated with the given `source` in a
|
|
* diff-informed query that uses this configuration (see
|
|
* `observeDiffInformedIncrementalMode`). By default, this is the location
|
|
* of the source itself, but this predicate should include any locations
|
|
* that are reported as the primary-location of the query or as an
|
|
* additional location ("$@" interpolation). Queries with `@kind path-problem`
|
|
* that override this predicate should also return the location of the source
|
|
* itself. For a query that doesn't report the source at all, this predicate
|
|
* should be `none()`.
|
|
*/
|
|
default Location getASelectedSourceLocation(Node source) { result = source.getLocation() }
|
|
|
|
/**
|
|
* Gets a location that will be associated with the given `sink` in a
|
|
* diff-informed query that uses this configuration (see
|
|
* `observeDiffInformedIncrementalMode`). By default, this is the location
|
|
* of the sink itself, but this predicate should include any locations
|
|
* that are reported as the primary-location of the query or as an
|
|
* additional location ("$@" interpolation). Queries with `@kind path-problem`
|
|
* that override this predicate should also return the location of the sink
|
|
* itself. For a query that doesn't report the sink at all, this predicate
|
|
* should be `none()`.
|
|
*/
|
|
default Location getASelectedSinkLocation(Node sink) { result = sink.getLocation() }
|
|
}
|
|
}
|
|
|
|
/** A type with `toString`. */
|
|
private signature class TypeWithToString {
|
|
string toString();
|
|
}
|
|
|
|
import PathGraphSigMod
|
|
|
|
private module PathGraphSigMod {
|
|
signature module PathGraphSig<TypeWithToString PathNode> {
|
|
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
|
|
predicate edges(PathNode a, PathNode b, string key, string val);
|
|
|
|
/** Holds if `n` is a node in the graph of data flow path explanations. */
|
|
predicate nodes(PathNode n, string key, string val);
|
|
|
|
/**
|
|
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
|
|
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
|
|
* `ret -> out` is summarized as the edge `arg -> out`.
|
|
*/
|
|
predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out);
|
|
}
|
|
}
|
|
|
|
private module DataFlowMakeCore<LocationSig Location, InputSig<Location> Lang> {
|
|
private import Lang
|
|
import Configs<Location, Lang>
|
|
|
|
/**
|
|
* Gets the exploration limit for `partialFlow` and `partialFlowRev`
|
|
* measured in approximate number of interprocedural steps.
|
|
*/
|
|
signature int explorationLimitSig();
|
|
|
|
/**
|
|
* The output of a global data flow computation.
|
|
*/
|
|
signature module GlobalFlowSig {
|
|
/**
|
|
* A `Node` augmented with a call context (except for sinks) and an access path.
|
|
* Only those `PathNode`s that are reachable from a source, and which can reach a sink, are generated.
|
|
*/
|
|
class PathNode;
|
|
|
|
/**
|
|
* Holds if data can flow from `source` to `sink`.
|
|
*
|
|
* The corresponding paths are generated from the end-points and the graph
|
|
* included in the module `PathGraph`.
|
|
*/
|
|
predicate flowPath(PathNode source, PathNode sink);
|
|
|
|
/**
|
|
* Holds if data can flow from `source` to `sink`.
|
|
*/
|
|
predicate flow(Node source, Node sink);
|
|
|
|
/**
|
|
* Holds if data can flow from some source to `sink`.
|
|
*/
|
|
predicate flowTo(Node sink);
|
|
|
|
/**
|
|
* Holds if data can flow from some source to `sink`.
|
|
*/
|
|
predicate flowToExpr(DataFlowExpr sink);
|
|
}
|
|
|
|
signature class PathNodeSig {
|
|
/** Gets a textual representation of this element. */
|
|
string toString();
|
|
|
|
/** Gets the underlying `Node`. */
|
|
Node getNode();
|
|
|
|
/** Gets the location of this node. */
|
|
Location getLocation();
|
|
}
|
|
|
|
import PathGraphSigMod
|
|
|
|
/**
|
|
* Constructs a `PathGraph` from two `PathGraph`s by disjoint union.
|
|
*/
|
|
module MergePathGraph<
|
|
PathNodeSig PathNode1, PathNodeSig PathNode2, PathGraphSig<PathNode1> Graph1,
|
|
PathGraphSig<PathNode2> Graph2>
|
|
{
|
|
private newtype TPathNode =
|
|
TPathNode1(PathNode1 p) or
|
|
TPathNode2(PathNode2 p)
|
|
|
|
/** A node in a graph of path explanations that is formed by disjoint union of the two given graphs. */
|
|
class PathNode extends TPathNode {
|
|
/** Gets this as a projection on the first given `PathGraph`. */
|
|
PathNode1 asPathNode1() { this = TPathNode1(result) }
|
|
|
|
/** Gets this as a projection on the second given `PathGraph`. */
|
|
PathNode2 asPathNode2() { this = TPathNode2(result) }
|
|
|
|
/** Gets a textual representation of this element. */
|
|
string toString() {
|
|
result = this.asPathNode1().toString() or
|
|
result = this.asPathNode2().toString()
|
|
}
|
|
|
|
/** Gets the underlying `Node`. */
|
|
Node getNode() {
|
|
result = this.asPathNode1().getNode() or
|
|
result = this.asPathNode2().getNode()
|
|
}
|
|
|
|
/** Gets the location of this node. */
|
|
Location getLocation() { result = this.getNode().getLocation() }
|
|
}
|
|
|
|
/**
|
|
* Provides the query predicates needed to include a graph in a path-problem query.
|
|
*/
|
|
module PathGraph implements PathGraphSig<PathNode> {
|
|
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
|
|
query predicate edges(PathNode a, PathNode b, string key, string val) {
|
|
Graph1::edges(a.asPathNode1(), b.asPathNode1(), key, val) or
|
|
Graph2::edges(a.asPathNode2(), b.asPathNode2(), key, val)
|
|
}
|
|
|
|
/** Holds if `n` is a node in the graph of data flow path explanations. */
|
|
query predicate nodes(PathNode n, string key, string val) {
|
|
Graph1::nodes(n.asPathNode1(), key, val) or
|
|
Graph2::nodes(n.asPathNode2(), key, val)
|
|
}
|
|
|
|
/**
|
|
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
|
|
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
|
|
* `ret -> out` is summarized as the edge `arg -> out`.
|
|
*/
|
|
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
|
|
Graph1::subpaths(arg.asPathNode1(), par.asPathNode1(), ret.asPathNode1(), out.asPathNode1()) or
|
|
Graph2::subpaths(arg.asPathNode2(), par.asPathNode2(), ret.asPathNode2(), out.asPathNode2())
|
|
}
|
|
}
|
|
}
|
|
|
|
/**
|
|
* Constructs a `PathGraph` from three `PathGraph`s by disjoint union.
|
|
*/
|
|
module MergePathGraph3<
|
|
PathNodeSig PathNode1, PathNodeSig PathNode2, PathNodeSig PathNode3,
|
|
PathGraphSig<PathNode1> Graph1, PathGraphSig<PathNode2> Graph2, PathGraphSig<PathNode3> Graph3>
|
|
{
|
|
private module MergedInner = MergePathGraph<PathNode1, PathNode2, Graph1, Graph2>;
|
|
|
|
private module Merged =
|
|
MergePathGraph<MergedInner::PathNode, PathNode3, MergedInner::PathGraph, Graph3>;
|
|
|
|
/** A node in a graph of path explanations that is formed by disjoint union of the three given graphs. */
|
|
class PathNode instanceof Merged::PathNode {
|
|
/** Gets this as a projection on the first given `PathGraph`. */
|
|
PathNode1 asPathNode1() { result = super.asPathNode1().asPathNode1() }
|
|
|
|
/** Gets this as a projection on the second given `PathGraph`. */
|
|
PathNode2 asPathNode2() { result = super.asPathNode1().asPathNode2() }
|
|
|
|
/** Gets this as a projection on the third given `PathGraph`. */
|
|
PathNode3 asPathNode3() { result = super.asPathNode2() }
|
|
|
|
/** Gets a textual representation of this element. */
|
|
string toString() { result = super.toString() }
|
|
|
|
/** Gets the underlying `Node`. */
|
|
Node getNode() { result = super.getNode() }
|
|
|
|
/** Gets the location of this node. */
|
|
Location getLocation() { result = super.getLocation() }
|
|
}
|
|
|
|
/**
|
|
* Provides the query predicates needed to include a graph in a path-problem query.
|
|
*/
|
|
module PathGraph implements PathGraphSig<PathNode> {
|
|
/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
|
|
query predicate edges(PathNode a, PathNode b, string key, string val) {
|
|
Merged::PathGraph::edges(a, b, key, val)
|
|
}
|
|
|
|
/** Holds if `n` is a node in the graph of data flow path explanations. */
|
|
query predicate nodes(PathNode n, string key, string val) {
|
|
Merged::PathGraph::nodes(n, key, val)
|
|
}
|
|
|
|
/**
|
|
* Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
|
|
* a subpath between `par` and `ret` with the connecting edges `arg -> par` and
|
|
* `ret -> out` is summarized as the edge `arg -> out`.
|
|
*/
|
|
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
|
|
Merged::PathGraph::subpaths(arg, par, ret, out)
|
|
}
|
|
}
|
|
}
|
|
|
|
/**
|
|
* Generates a `PathGraph` in which equivalent path nodes are merged, in order to avoid duplicate paths.
|
|
*/
|
|
module DeduplicatePathGraph<PathNodeSig InputPathNode, PathGraphSig<InputPathNode> Graph> {
|
|
// NOTE: there is a known limitation in that this module cannot see which nodes are sources or sinks.
|
|
// This only matters in the rare case where a sink PathNode has a non-empty set of succesors, and there is a
|
|
// non-sink PathNode with the same `(node, toString)` value and the same successors, but is transitively
|
|
// reachable from a different set of PathNodes. (And conversely for sources).
|
|
//
|
|
pragma[nomagic]
|
|
private InputPathNode getAPathNode(Node node, string toString) {
|
|
result.getNode() = node and
|
|
Graph::nodes(result, _, toString)
|
|
}
|
|
|
|
private signature predicate collapseCandidateSig(Node node, string toString);
|
|
|
|
private signature predicate stepSig(
|
|
InputPathNode node1, InputPathNode node2, string key, string val
|
|
);
|
|
|
|
private signature predicate subpathStepSig(
|
|
InputPathNode arg, InputPathNode param, InputPathNode ret, InputPathNode out
|
|
);
|
|
|
|
/**
|
|
* Performs a forward or backward pass computing which `(node, toString)` pairs can subsume their corresponding
|
|
* path nodes.
|
|
*
|
|
* This is similar to automaton minimization, but for an NFA. Since minimizing an NFA is NP-hard (and does not have
|
|
* a unique minimal NFA), we operate with the simpler model: for a given `(node, toString)` pair, either all
|
|
* corresponding path nodes are merged, or none are merged.
|
|
*
|
|
* Comments are written as if this checks for outgoing edges and propagates backward, though the module is also
|
|
* used to perform the opposite direction.
|
|
*/
|
|
private module MakeDiscriminatorPass<
|
|
collapseCandidateSig/2 collapseCandidate, stepSig/4 step, subpathStepSig/4 subpathStep>
|
|
{
|
|
/**
|
|
* Gets the number of `(key, val, node, toString)` tuples reachable in one step from `pathNode`.
|
|
*
|
|
* That is, two edges are counted as one if their target nodes are the same after projection, and the edges have the
|
|
* same `(key, val)`.
|
|
*/
|
|
private int getOutDegreeFromPathNode(InputPathNode pathNode) {
|
|
result =
|
|
count(Node node, string toString, string key, string val |
|
|
step(pathNode, getAPathNode(node, toString), key, val)
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Gets the number of `(key, val, node2, toString2)` pairs reachable in one step from path nodes corresponding to `(node, toString)`.
|
|
*/
|
|
private int getOutDegreeFromNode(Node node, string toString) {
|
|
result =
|
|
strictcount(Node node2, string toString2, string key, string val |
|
|
step(getAPathNode(node, toString), getAPathNode(node2, toString2), key, val)
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Like `getOutDegreeFromPathNode` except counts `subpath` tuples.
|
|
*/
|
|
private int getSubpathOutDegreeFromPathNode(InputPathNode pathNode) {
|
|
result =
|
|
count(Node n1, string s1, Node n2, string s2, Node n3, string s3 |
|
|
subpathStep(pathNode, getAPathNode(n1, s1), getAPathNode(n2, s2), getAPathNode(n3, s3))
|
|
)
|
|
}
|
|
|
|
/**
|
|
* Like `getOutDegreeFromNode` except counts `subpath` tuples.
|
|
*/
|
|
private int getSubpathOutDegreeFromNode(Node node, string toString) {
|
|
result =
|
|
strictcount(Node n1, string s1, Node n2, string s2, Node n3, string s3 |
|
|
subpathStep(getAPathNode(node, toString), getAPathNode(n1, s1), getAPathNode(n2, s2),
|
|
getAPathNode(n3, s3))
|
|
)
|
|
}
|
|
|
|
/** Gets a successor of `node`, including subpath flow-through, but not enter or exit subpath steps. */
|
|
InputPathNode stepEx(InputPathNode node) {
|
|
step(node, result, _, _) and
|
|
not result = enterSubpathStep(node) and
|
|
not result = exitSubpathStep(node)
|
|
or
|
|
// Assuming the input is pruned properly, all subpaths have flow-through.
|
|
// This step should be in 'step' as well, but include it here for clarity as we rely on it.
|
|
subpathStep(node, _, _, result)
|
|
}
|
|
|
|
InputPathNode enterSubpathStep(InputPathNode node) { subpathStep(node, result, _, _) }
|
|
|
|
InputPathNode exitSubpathStep(InputPathNode node) { subpathStep(_, _, node, result) }
|
|
|
|
/** Holds if `(node, toString)` cannot be collapsed (but was a candidate for being collapsed). */
|
|
predicate discriminatedPair(Node node, string toString, boolean hasEnter) {
|
|
collapseCandidate(node, toString) and
|
|
hasEnter = false and
|
|
(
|
|
// Check if all corresponding PathNodes have the same successor sets when projected to `(node, toString)`.
|
|
// To do this, we check that each successor set has the same size as the union of the succesor sets.
|
|
// - If the successor sets are equal, then they are also equal to their union, and so have the correct size.
|
|
// - Conversely, if two successor sets are not equal, one of them must be missing an element that is present
|
|
// in the union, but must still be a subset of the union, and thus be strictly smaller than the union.
|
|
getOutDegreeFromPathNode(getAPathNode(node, toString)) <
|
|
getOutDegreeFromNode(node, toString)
|
|
or
|
|
// Same as above but counting associated subpath triples instead
|
|
getSubpathOutDegreeFromPathNode(getAPathNode(node, toString)) <
|
|
getSubpathOutDegreeFromNode(node, toString)
|
|
)
|
|
or
|
|
collapseCandidate(node, toString) and
|
|
(
|
|
// Retain flow state if one of the successors requires it to be retained
|
|
discriminatedPathNode(stepEx(getAPathNode(node, toString)), hasEnter)
|
|
or
|
|
// Propagate backwards from parameter to argument
|
|
discriminatedPathNode(enterSubpathStep(getAPathNode(node, toString)), false) and
|
|
hasEnter = false
|
|
or
|
|
// Propagate backwards from out to return
|
|
discriminatedPathNode(exitSubpathStep(getAPathNode(node, toString)), _) and
|
|
hasEnter = true
|
|
)
|
|
}
|
|
|
|
/** Holds if `pathNode` cannot be collapsed. */
|
|
private predicate discriminatedPathNode(InputPathNode pathNode, boolean hasEnter) {
|
|
exists(Node node, string toString |
|
|
discriminatedPair(node, toString, hasEnter) and
|
|
getAPathNode(node, toString) = pathNode
|
|
)
|
|
}
|
|
|
|
/** Holds if `(node, toString)` cannot be collapsed (but was a candidate for being collapsed). */
|
|
predicate discriminatedPair(Node node, string toString) {
|
|
discriminatedPair(node, toString, _)
|
|
}
|
|
|
|
/** Holds if `pathNode` cannot be collapsed. */
|
|
predicate discriminatedPathNode(InputPathNode pathNode) { discriminatedPathNode(pathNode, _) }
|
|
}
|
|
|
|
private InputPathNode getUniqPathNode(Node node, string toString) {
|
|
result = unique(InputPathNode pathNode | pathNode = getAPathNode(node, toString))
|
|
}
|
|
|
|
private predicate initialCandidate(Node node, string toString) {
|
|
exists(getAPathNode(node, toString)) and not exists(getUniqPathNode(node, toString))
|
|
}
|
|
|
|
private module Pass1 =
|
|
MakeDiscriminatorPass<initialCandidate/2, Graph::edges/4, Graph::subpaths/4>;
|
|
|
|
private predicate edgesRev(InputPathNode node1, InputPathNode node2, string key, string val) {
|
|
Graph::edges(node2, node1, key, val)
|
|
}
|
|
|
|
private predicate subpathsRev(
|
|
InputPathNode n1, InputPathNode n2, InputPathNode n3, InputPathNode n4
|
|
) {
|
|
Graph::subpaths(n4, n3, n2, n1)
|
|
}
|
|
|
|
private module Pass2 =
|
|
MakeDiscriminatorPass<Pass1::discriminatedPair/2, edgesRev/4, subpathsRev/4>;
|
|
|
|
private newtype TPathNode =
|
|
TPreservedPathNode(InputPathNode node) {
|
|
Pass2::discriminatedPathNode(node) or node = getUniqPathNode(_, _)
|
|
} or
|
|
TCollapsedPathNode(Node node, string toString) {
|
|
initialCandidate(node, toString) and
|
|
not Pass2::discriminatedPair(node, toString)
|
|
}
|
|
|
|
/** A node in the path graph after equivalent nodes have been collapsed. */
|
|
class PathNode extends TPathNode {
|
|
private Node asCollapsedNode() { this = TCollapsedPathNode(result, _) }
|
|
|
|
private InputPathNode asPreservedNode() { this = TPreservedPathNode(result) }
|
|
|
|
/** Gets a correspondng node in the original graph. */
|
|
InputPathNode getAnOriginalPathNode() {
|
|
exists(Node node, string toString |
|
|
this = TCollapsedPathNode(node, toString) and
|
|
result = getAPathNode(node, toString)
|
|
)
|
|
or
|
|
result = this.asPreservedNode()
|
|
}
|
|
|
|
/** Gets a string representation of this node. */
|
|
string toString() {
|
|
result = this.asPreservedNode().toString() or this = TCollapsedPathNode(_, result)
|
|
}
|
|
|
|
/** Gets the location of this node. */
|
|
Location getLocation() { result = this.getAnOriginalPathNode().getLocation() }
|
|
|
|
/** Gets the corresponding data-flow node. */
|
|
Node getNode() {
|
|
result = this.asCollapsedNode()
|
|
or
|
|
result = this.asPreservedNode().getNode()
|
|
}
|
|
}
|
|
|
|
/**
|
|
* Provides the query predicates needed to include a graph in a path-problem query.
|
|
*/
|
|
module PathGraph implements PathGraphSig<PathNode> {
|
|
query predicate nodes(PathNode node, string key, string val) {
|
|
Graph::nodes(node.getAnOriginalPathNode(), key, val)
|
|
}
|
|
|
|
query predicate edges(PathNode node1, PathNode node2, string key, string val) {
|
|
Graph::edges(node1.getAnOriginalPathNode(), node2.getAnOriginalPathNode(), key, val)
|
|
}
|
|
|
|
query predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out) {
|
|
// Note: this may look suspiciously simple, but it's not an oversight. Even if the caller needs to retain state,
|
|
// it is entirely possible to step through a subpath in which state has been projected away.
|
|
Graph::subpaths(arg.getAnOriginalPathNode(), par.getAnOriginalPathNode(),
|
|
ret.getAnOriginalPathNode(), out.getAnOriginalPathNode())
|
|
}
|
|
}
|
|
|
|
// 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.
|
|
*/
|
|
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() { none() }
|
|
}
|
|
|
|
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"
|
|
}
|
|
|
|
predicate observeOverlayInformedIncrementalMode() { none() }
|
|
}
|
|
|
|
private module Stage1 = ImplStage1<C>;
|
|
|
|
import Stage1::PartialFlow
|
|
|
|
private module Flow = Impl<C, Stage1::Stage1WithState>;
|
|
|
|
import Flow
|
|
}
|
|
}
|
|
|
|
module DataFlowMakeOverlay<LocationSig Location, InputSig<Location> Lang> {
|
|
import DataFlowMake<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
|
|
}
|
|
}
|