|
|
|
|
@@ -85,7 +85,7 @@ private import AdditionalFlowSteps
|
|
|
|
|
* define additional edges beyond the standard data flow edges (`isAdditionalFlowStep`)
|
|
|
|
|
* and prohibit intermediate flow nodes and edges (`isBarrier`).
|
|
|
|
|
*/
|
|
|
|
|
abstract class Configuration extends string {
|
|
|
|
|
abstract deprecated class Configuration extends string {
|
|
|
|
|
bindingset[this]
|
|
|
|
|
Configuration() { any() }
|
|
|
|
|
|
|
|
|
|
@@ -281,7 +281,9 @@ abstract class Configuration extends string {
|
|
|
|
|
* `isBarrierGuard` or `AdditionalBarrierGuardNode`.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate isBarrierGuardInternal(Configuration cfg, BarrierGuardNodeInternal guard) {
|
|
|
|
|
deprecated private predicate isBarrierGuardInternal(
|
|
|
|
|
Configuration cfg, BarrierGuardNodeInternal guard
|
|
|
|
|
) {
|
|
|
|
|
cfg.isBarrierGuard(guard)
|
|
|
|
|
or
|
|
|
|
|
guard.(AdditionalBarrierGuardNode).appliesTo(cfg)
|
|
|
|
|
@@ -330,12 +332,12 @@ abstract class FlowLabel extends string {
|
|
|
|
|
*
|
|
|
|
|
* This is an alias of `FlowLabel`, so the two types can be used interchangeably.
|
|
|
|
|
*/
|
|
|
|
|
class TaintKind = FlowLabel;
|
|
|
|
|
deprecated class TaintKind = FlowLabel;
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* A standard flow label, that is, either `FlowLabel::data()` or `FlowLabel::taint()`.
|
|
|
|
|
*/
|
|
|
|
|
class StandardFlowLabel extends FlowLabel {
|
|
|
|
|
deprecated class StandardFlowLabel extends FlowLabel {
|
|
|
|
|
StandardFlowLabel() { this = "data" or this = "taint" }
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
@@ -366,6 +368,7 @@ abstract private class BarrierGuardNodeInternal extends DataFlow::Node { }
|
|
|
|
|
* implementations of `blocks` will _both_ apply to any configuration that includes either of them.
|
|
|
|
|
*/
|
|
|
|
|
abstract class BarrierGuardNode extends BarrierGuardNodeInternal {
|
|
|
|
|
// TODO: deprecate this class; currently requires too much refactoring
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this node blocks expression `e` provided it evaluates to `outcome`.
|
|
|
|
|
*
|
|
|
|
|
@@ -382,8 +385,8 @@ abstract class BarrierGuardNode extends BarrierGuardNodeInternal {
|
|
|
|
|
/**
|
|
|
|
|
* Barrier guards derived from other barrier guards.
|
|
|
|
|
*/
|
|
|
|
|
abstract private class DerivedBarrierGuardNode extends BarrierGuardNodeInternal {
|
|
|
|
|
abstract predicate appliesTo(Configuration cfg);
|
|
|
|
|
abstract deprecated private class DerivedBarrierGuardNode extends BarrierGuardNodeInternal {
|
|
|
|
|
abstract deprecated predicate appliesTo(Configuration cfg);
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this node blocks expression `e` from flow of type `label`, provided it evaluates to `outcome`.
|
|
|
|
|
@@ -396,7 +399,7 @@ abstract private class DerivedBarrierGuardNode extends BarrierGuardNodeInternal
|
|
|
|
|
/**
|
|
|
|
|
* Barrier guards derived from `AdditionalSanitizerGuard`
|
|
|
|
|
*/
|
|
|
|
|
private class BarrierGuardNodeFromAdditionalSanitizerGuard extends BarrierGuardNodeInternal instanceof TaintTracking::AdditionalSanitizerGuardNode
|
|
|
|
|
deprecated private class BarrierGuardNodeFromAdditionalSanitizerGuard extends BarrierGuardNodeInternal instanceof TaintTracking::AdditionalSanitizerGuardNode
|
|
|
|
|
{ }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
@@ -405,7 +408,7 @@ private class BarrierGuardNodeFromAdditionalSanitizerGuard extends BarrierGuardN
|
|
|
|
|
* `label` is bound to the blocked label, or the empty string if all labels should be blocked.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardBlocksExpr(
|
|
|
|
|
deprecated private predicate barrierGuardBlocksExpr(
|
|
|
|
|
BarrierGuardNodeInternal guard, boolean outcome, Expr test, string label
|
|
|
|
|
) {
|
|
|
|
|
guard.(BarrierGuardNode).blocks(outcome, test) and label = ""
|
|
|
|
|
@@ -423,7 +426,7 @@ private predicate barrierGuardBlocksExpr(
|
|
|
|
|
* Holds if `guard` may block the flow of a value reachable through exploratory flow.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardIsRelevant(BarrierGuardNodeInternal guard) {
|
|
|
|
|
deprecated private predicate barrierGuardIsRelevant(BarrierGuardNodeInternal guard) {
|
|
|
|
|
exists(Expr e |
|
|
|
|
|
barrierGuardBlocksExpr(guard, _, e, _) and
|
|
|
|
|
isRelevantForward(e.flow(), _)
|
|
|
|
|
@@ -437,7 +440,7 @@ private predicate barrierGuardIsRelevant(BarrierGuardNodeInternal guard) {
|
|
|
|
|
* `label` is bound to the blocked label, or the empty string if all labels should be blocked.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardBlocksAccessPath(
|
|
|
|
|
deprecated private predicate barrierGuardBlocksAccessPath(
|
|
|
|
|
BarrierGuardNodeInternal guard, boolean outcome, AccessPath ap, string label
|
|
|
|
|
) {
|
|
|
|
|
barrierGuardIsRelevant(guard) and
|
|
|
|
|
@@ -450,7 +453,7 @@ private predicate barrierGuardBlocksAccessPath(
|
|
|
|
|
* This predicate is outlined to give the optimizer a hint about the join ordering.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardBlocksSsaRefinement(
|
|
|
|
|
deprecated private predicate barrierGuardBlocksSsaRefinement(
|
|
|
|
|
BarrierGuardNodeInternal guard, boolean outcome, SsaRefinementNode ref, string label
|
|
|
|
|
) {
|
|
|
|
|
barrierGuardIsRelevant(guard) and
|
|
|
|
|
@@ -466,7 +469,7 @@ private predicate barrierGuardBlocksSsaRefinement(
|
|
|
|
|
* `outcome` is bound to the outcome of `cond` for join-ordering purposes.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardUsedInCondition(
|
|
|
|
|
deprecated private predicate barrierGuardUsedInCondition(
|
|
|
|
|
BarrierGuardNodeInternal guard, ConditionGuardNode cond, boolean outcome
|
|
|
|
|
) {
|
|
|
|
|
barrierGuardIsRelevant(guard) and
|
|
|
|
|
@@ -485,7 +488,7 @@ private predicate barrierGuardUsedInCondition(
|
|
|
|
|
* `label` is bound to the blocked label, or the empty string if all labels should be blocked.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardBlocksNode(
|
|
|
|
|
deprecated private predicate barrierGuardBlocksNode(
|
|
|
|
|
BarrierGuardNodeInternal guard, DataFlow::Node nd, string label
|
|
|
|
|
) {
|
|
|
|
|
// 1) `nd` is a use of a refinement node that blocks its input variable
|
|
|
|
|
@@ -510,7 +513,7 @@ private predicate barrierGuardBlocksNode(
|
|
|
|
|
* `label` is bound to the blocked label, or the empty string if all labels should be blocked.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate barrierGuardBlocksEdge(
|
|
|
|
|
deprecated private predicate barrierGuardBlocksEdge(
|
|
|
|
|
BarrierGuardNodeInternal guard, DataFlow::Node pred, DataFlow::Node succ, string label
|
|
|
|
|
) {
|
|
|
|
|
exists(
|
|
|
|
|
@@ -531,7 +534,9 @@ private predicate barrierGuardBlocksEdge(
|
|
|
|
|
* This predicate exists to get a better join-order for the `barrierGuardBlocksEdge` predicate above.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private BasicBlock getADominatedBasicBlock(BarrierGuardNodeInternal guard, ConditionGuardNode cond) {
|
|
|
|
|
deprecated private BasicBlock getADominatedBasicBlock(
|
|
|
|
|
BarrierGuardNodeInternal guard, ConditionGuardNode cond
|
|
|
|
|
) {
|
|
|
|
|
barrierGuardIsRelevant(guard) and
|
|
|
|
|
guard.getEnclosingExpr() = cond.getTest() and
|
|
|
|
|
cond.dominates(result)
|
|
|
|
|
@@ -543,7 +548,9 @@ private BasicBlock getADominatedBasicBlock(BarrierGuardNodeInternal guard, Condi
|
|
|
|
|
*
|
|
|
|
|
* Only holds for barriers that should apply to all flow labels.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isBarrierEdgeRaw(Configuration cfg, DataFlow::Node pred, DataFlow::Node succ) {
|
|
|
|
|
deprecated private predicate isBarrierEdgeRaw(
|
|
|
|
|
Configuration cfg, DataFlow::Node pred, DataFlow::Node succ
|
|
|
|
|
) {
|
|
|
|
|
cfg.isBarrierEdge(pred, succ)
|
|
|
|
|
or
|
|
|
|
|
exists(BarrierGuardNodeInternal guard |
|
|
|
|
|
@@ -559,7 +566,9 @@ private predicate isBarrierEdgeRaw(Configuration cfg, DataFlow::Node pred, DataF
|
|
|
|
|
* Only holds for barriers that should apply to all flow labels.
|
|
|
|
|
*/
|
|
|
|
|
pragma[inline]
|
|
|
|
|
private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow::Node succ) {
|
|
|
|
|
deprecated private predicate isBarrierEdge(
|
|
|
|
|
Configuration cfg, DataFlow::Node pred, DataFlow::Node succ
|
|
|
|
|
) {
|
|
|
|
|
isBarrierEdgeRaw(cfg, pred, succ)
|
|
|
|
|
or
|
|
|
|
|
cfg.isBarrierOut(pred)
|
|
|
|
|
@@ -571,7 +580,7 @@ private predicate isBarrierEdge(Configuration cfg, DataFlow::Node pred, DataFlow
|
|
|
|
|
* Holds if there is a labeled barrier edge `pred -> succ` in `cfg` either through an explicit barrier edge
|
|
|
|
|
* or one implied by a barrier guard.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isLabeledBarrierEdgeRaw(
|
|
|
|
|
deprecated private predicate isLabeledBarrierEdgeRaw(
|
|
|
|
|
Configuration cfg, DataFlow::Node pred, DataFlow::Node succ, DataFlow::FlowLabel label
|
|
|
|
|
) {
|
|
|
|
|
cfg.isBarrierEdge(pred, succ, label)
|
|
|
|
|
@@ -587,7 +596,7 @@ private predicate isLabeledBarrierEdgeRaw(
|
|
|
|
|
* or one implied by a barrier guard, or by an out/in barrier for `pred` or `succ`, respectively.
|
|
|
|
|
*/
|
|
|
|
|
pragma[inline]
|
|
|
|
|
private predicate isLabeledBarrierEdge(
|
|
|
|
|
deprecated private predicate isLabeledBarrierEdge(
|
|
|
|
|
Configuration cfg, DataFlow::Node pred, DataFlow::Node succ, DataFlow::FlowLabel label
|
|
|
|
|
) {
|
|
|
|
|
isLabeledBarrierEdgeRaw(cfg, pred, succ, label)
|
|
|
|
|
@@ -600,7 +609,7 @@ private predicate isLabeledBarrierEdge(
|
|
|
|
|
/**
|
|
|
|
|
* A guard node that only blocks specific labels.
|
|
|
|
|
*/
|
|
|
|
|
abstract class LabeledBarrierGuardNode extends BarrierGuardNode {
|
|
|
|
|
abstract deprecated class LabeledBarrierGuardNode extends BarrierGuardNode {
|
|
|
|
|
override predicate blocks(boolean outcome, Expr e) { none() }
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
@@ -699,7 +708,7 @@ module PseudoProperties {
|
|
|
|
|
* A data flow node that should be considered a source for some specific configuration,
|
|
|
|
|
* in addition to any other sources that configuration may recognize.
|
|
|
|
|
*/
|
|
|
|
|
abstract class AdditionalSource extends DataFlow::Node {
|
|
|
|
|
abstract deprecated class AdditionalSource extends DataFlow::Node {
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this data flow node should be considered a source node for
|
|
|
|
|
* configuration `cfg`.
|
|
|
|
|
@@ -717,7 +726,7 @@ abstract class AdditionalSource extends DataFlow::Node {
|
|
|
|
|
* A data flow node that should be considered a sink for some specific configuration,
|
|
|
|
|
* in addition to any other sinks that configuration may recognize.
|
|
|
|
|
*/
|
|
|
|
|
abstract class AdditionalSink extends DataFlow::Node {
|
|
|
|
|
abstract deprecated class AdditionalSink extends DataFlow::Node {
|
|
|
|
|
/**
|
|
|
|
|
* Holds if this data flow node should be considered a sink node for
|
|
|
|
|
* configuration `cfg`.
|
|
|
|
|
@@ -751,7 +760,7 @@ private class FlowStepThroughImport extends SharedFlowStep {
|
|
|
|
|
* Summary steps through function calls are not taken into account.
|
|
|
|
|
*/
|
|
|
|
|
pragma[inline]
|
|
|
|
|
private predicate basicFlowStepNoBarrier(
|
|
|
|
|
deprecated private predicate basicFlowStepNoBarrier(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, PathSummary summary, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
// Local flow
|
|
|
|
|
@@ -790,7 +799,7 @@ private predicate basicFlowStepNoBarrier(
|
|
|
|
|
* and hence should only be used for purposes of approximation.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate exploratoryFlowStep(
|
|
|
|
|
deprecated private predicate exploratoryFlowStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
isRelevantForward(pred, cfg) and
|
|
|
|
|
@@ -809,7 +818,7 @@ private predicate exploratoryFlowStep(
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `nd` is a source node for configuration `cfg`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
|
|
|
|
|
deprecated private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
|
|
|
|
|
(cfg.isSource(nd) or nd.(AdditionalSource).isSourceFor(cfg)) and
|
|
|
|
|
lbl = cfg.getDefaultSourceLabel()
|
|
|
|
|
or
|
|
|
|
|
@@ -821,7 +830,7 @@ private predicate isSource(DataFlow::Node nd, DataFlow::Configuration cfg, FlowL
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `nd` is a sink node for configuration `cfg`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
|
|
|
|
|
deprecated private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLabel lbl) {
|
|
|
|
|
(cfg.isSink(nd) or nd.(AdditionalSink).isSinkFor(cfg)) and
|
|
|
|
|
lbl = any(StandardFlowLabel f)
|
|
|
|
|
or
|
|
|
|
|
@@ -834,7 +843,7 @@ private predicate isSink(DataFlow::Node nd, DataFlow::Configuration cfg, FlowLab
|
|
|
|
|
* Holds if there exists a load-step from `pred` to `succ` under configuration `cfg`,
|
|
|
|
|
* and the forwards exploratory flow has found a relevant store-step with the same property as the load-step.
|
|
|
|
|
*/
|
|
|
|
|
private predicate exploratoryLoadStep(
|
|
|
|
|
deprecated private predicate exploratoryLoadStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
exists(string prop | prop = getAForwardRelevantLoadProperty(cfg) |
|
|
|
|
|
@@ -851,7 +860,7 @@ private predicate exploratoryLoadStep(
|
|
|
|
|
* This private predicate is only used in `exploratoryLoadStep`, and exists as a separate predicate to give the compiler a hint about join-ordering.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private string getAForwardRelevantLoadProperty(DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private string getAForwardRelevantLoadProperty(DataFlow::Configuration cfg) {
|
|
|
|
|
exists(DataFlow::Node previous | isRelevantForward(previous, cfg) |
|
|
|
|
|
basicStoreStep(previous, _, result) or
|
|
|
|
|
isAdditionalStoreStep(previous, _, result, cfg)
|
|
|
|
|
@@ -865,7 +874,7 @@ private string getAForwardRelevantLoadProperty(DataFlow::Configuration cfg) {
|
|
|
|
|
*
|
|
|
|
|
* The properties from this predicate are used as a white-list of properties for load/store steps that should always be considered in the exploratory flow.
|
|
|
|
|
*/
|
|
|
|
|
private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
|
|
|
|
|
exists(string loadProp, string storeProp |
|
|
|
|
|
isAdditionalLoadStoreStep(_, _, loadProp, storeProp, cfg) and
|
|
|
|
|
storeProp != loadProp and
|
|
|
|
|
@@ -878,7 +887,7 @@ private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
|
|
|
|
|
* and somewhere in the program there exists a load-step that could possibly read the stored value.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate exploratoryForwardStoreStep(
|
|
|
|
|
deprecated private predicate exploratoryForwardStoreStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
exists(string prop |
|
|
|
|
|
@@ -896,7 +905,7 @@ private predicate exploratoryForwardStoreStep(
|
|
|
|
|
* and `succ` has been found to be relevant during the backwards exploratory flow,
|
|
|
|
|
* and the backwards exploratory flow has found a relevant load-step with the same property as the store-step.
|
|
|
|
|
*/
|
|
|
|
|
private predicate exploratoryBackwardStoreStep(
|
|
|
|
|
deprecated private predicate exploratoryBackwardStoreStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
exists(string prop | prop = getABackwardsRelevantStoreProperty(cfg) |
|
|
|
|
|
@@ -912,7 +921,7 @@ private predicate exploratoryBackwardStoreStep(
|
|
|
|
|
* This private predicate is only used in `exploratoryBackwardStoreStep`, and exists as a separate predicate to give the compiler a hint about join-ordering.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private string getABackwardsRelevantStoreProperty(DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private string getABackwardsRelevantStoreProperty(DataFlow::Configuration cfg) {
|
|
|
|
|
exists(DataFlow::Node mid | isRelevant(mid, cfg) |
|
|
|
|
|
basicLoadStep(mid, _, result) or
|
|
|
|
|
isAdditionalLoadStep(mid, _, result, cfg)
|
|
|
|
|
@@ -926,7 +935,7 @@ private string getABackwardsRelevantStoreProperty(DataFlow::Configuration cfg) {
|
|
|
|
|
*
|
|
|
|
|
* No call/return matching is done, so this is a relatively coarse over-approximation.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
|
|
|
|
isSource(nd, cfg, _) and isLive()
|
|
|
|
|
or
|
|
|
|
|
exists(DataFlow::Node mid |
|
|
|
|
|
@@ -942,7 +951,7 @@ private predicate isRelevantForward(DataFlow::Node nd, DataFlow::Configuration c
|
|
|
|
|
*
|
|
|
|
|
* No call/return matching is done, so this is a relatively coarse over-approximation.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
|
|
|
|
isRelevantForward(nd, cfg) and isSink(nd, cfg, _)
|
|
|
|
|
or
|
|
|
|
|
exists(DataFlow::Node mid | isRelevant(mid, cfg) | isRelevantBackStep(mid, nd, cfg))
|
|
|
|
|
@@ -951,7 +960,7 @@ private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
|
|
|
|
/**
|
|
|
|
|
* Holds if there is backwards data-flow step from `mid` to `nd` under `cfg`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isRelevantBackStep(
|
|
|
|
|
deprecated private predicate isRelevantBackStep(
|
|
|
|
|
DataFlow::Node mid, DataFlow::Node nd, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
exploratoryFlowStep(nd, mid, cfg)
|
|
|
|
|
@@ -965,7 +974,7 @@ private predicate isRelevantBackStep(
|
|
|
|
|
* either `pred` is an argument of `f` and `succ` the corresponding parameter, or
|
|
|
|
|
* `pred` is a variable definition whose value is captured by `f` at `succ`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate callInputStep(
|
|
|
|
|
deprecated private predicate callInputStep(
|
|
|
|
|
Function f, DataFlow::Node invk, DataFlow::Node pred, DataFlow::Node succ,
|
|
|
|
|
DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
@@ -995,7 +1004,7 @@ private predicate callInputStep(
|
|
|
|
|
* into account.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate reachableFromInput(
|
|
|
|
|
deprecated private predicate reachableFromInput(
|
|
|
|
|
Function f, DataFlow::Node invk, DataFlow::Node input, DataFlow::Node nd,
|
|
|
|
|
DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1014,7 +1023,7 @@ private predicate reachableFromInput(
|
|
|
|
|
* to a path represented by `oldSummary` yielding a path represented by `newSummary`.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate appendStep(
|
|
|
|
|
deprecated private predicate appendStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Configuration cfg, PathSummary oldSummary, DataFlow::Node succ,
|
|
|
|
|
PathSummary newSummary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1030,7 +1039,7 @@ private predicate appendStep(
|
|
|
|
|
* which is either an argument or a definition captured by the function, flows under
|
|
|
|
|
* configuration `cfg`, possibly through callees.
|
|
|
|
|
*/
|
|
|
|
|
private predicate flowThroughCall(
|
|
|
|
|
deprecated private predicate flowThroughCall(
|
|
|
|
|
DataFlow::Node input, DataFlow::Node output, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
exists(Function f, DataFlow::FunctionReturnNode ret |
|
|
|
|
|
@@ -1076,7 +1085,7 @@ private predicate flowThroughCall(
|
|
|
|
|
* along a path summarized by `summary`.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate storeStep(
|
|
|
|
|
deprecated private predicate storeStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, string prop, DataFlow::Configuration cfg,
|
|
|
|
|
PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1114,7 +1123,7 @@ private predicate storeStep(
|
|
|
|
|
/**
|
|
|
|
|
* Gets a dataflow-node for the operand of the await-expression `await`.
|
|
|
|
|
*/
|
|
|
|
|
private DataFlow::Node getAwaitOperand(DataFlow::Node await) {
|
|
|
|
|
deprecated private DataFlow::Node getAwaitOperand(DataFlow::Node await) {
|
|
|
|
|
exists(AwaitExpr awaitExpr |
|
|
|
|
|
result = awaitExpr.getOperand().getUnderlyingValue().flow() and
|
|
|
|
|
await.asExpr() = awaitExpr
|
|
|
|
|
@@ -1124,7 +1133,7 @@ private DataFlow::Node getAwaitOperand(DataFlow::Node await) {
|
|
|
|
|
/**
|
|
|
|
|
* Holds if property `prop` of `arg` is read inside a function and returned to the call `succ`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate parameterPropRead(
|
|
|
|
|
deprecated private predicate parameterPropRead(
|
|
|
|
|
DataFlow::Node arg, string prop, DataFlow::Node succ, DataFlow::Configuration cfg,
|
|
|
|
|
PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1136,7 +1145,7 @@ private predicate parameterPropRead(
|
|
|
|
|
|
|
|
|
|
// all the non-recursive parts of parameterPropRead outlined into a precomputed predicate
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate parameterPropReadStep(
|
|
|
|
|
deprecated private predicate parameterPropReadStep(
|
|
|
|
|
DataFlow::SourceNode parm, DataFlow::Node read, string prop, DataFlow::Configuration cfg,
|
|
|
|
|
DataFlow::Node arg, DataFlow::Node invk, Function f, DataFlow::Node succ
|
|
|
|
|
) {
|
|
|
|
|
@@ -1160,7 +1169,7 @@ private predicate parameterPropReadStep(
|
|
|
|
|
* Holds if `read` may flow into a return statement of `f` under configuration `cfg`
|
|
|
|
|
* (possibly through callees) along a path summarized by `summary`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate reachesReturn(
|
|
|
|
|
deprecated private predicate reachesReturn(
|
|
|
|
|
Function f, DataFlow::Node read, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
isRelevant(read, cfg) and
|
|
|
|
|
@@ -1178,7 +1187,7 @@ private predicate reachesReturn(
|
|
|
|
|
|
|
|
|
|
// used in `getARelevantProp`, outlined for performance
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private string getARelevantStoreProp(DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private string getARelevantStoreProp(DataFlow::Configuration cfg) {
|
|
|
|
|
exists(DataFlow::Node previous | isRelevant(previous, cfg) |
|
|
|
|
|
basicStoreStep(previous, _, result) or
|
|
|
|
|
isAdditionalStoreStep(previous, _, result, cfg)
|
|
|
|
|
@@ -1187,7 +1196,7 @@ private string getARelevantStoreProp(DataFlow::Configuration cfg) {
|
|
|
|
|
|
|
|
|
|
// used in `getARelevantProp`, outlined for performance
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private string getARelevantLoadProp(DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private string getARelevantLoadProp(DataFlow::Configuration cfg) {
|
|
|
|
|
exists(DataFlow::Node previous | isRelevant(previous, cfg) |
|
|
|
|
|
basicLoadStep(previous, _, result) or
|
|
|
|
|
isAdditionalLoadStep(previous, _, result, cfg)
|
|
|
|
|
@@ -1196,7 +1205,7 @@ private string getARelevantLoadProp(DataFlow::Configuration cfg) {
|
|
|
|
|
|
|
|
|
|
/** Gets the name of a property that is both loaded and stored according to the exploratory analysis. */
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private string getARelevantProp(DataFlow::Configuration cfg) {
|
|
|
|
|
deprecated private string getARelevantProp(DataFlow::Configuration cfg) {
|
|
|
|
|
result = getARelevantStoreProp(cfg) and
|
|
|
|
|
result = getARelevantLoadProp(cfg)
|
|
|
|
|
or
|
|
|
|
|
@@ -1206,7 +1215,7 @@ private string getARelevantProp(DataFlow::Configuration cfg) {
|
|
|
|
|
/**
|
|
|
|
|
* Holds if the property `prop` of the object `pred` should be loaded into `succ`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isAdditionalLoadStep(
|
|
|
|
|
deprecated private predicate isAdditionalLoadStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, string prop, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
LegacyFlowStep::loadStep(pred, succ, prop)
|
|
|
|
|
@@ -1217,7 +1226,7 @@ private predicate isAdditionalLoadStep(
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `pred` should be stored in the object `succ` under the property `prop`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isAdditionalStoreStep(
|
|
|
|
|
deprecated private predicate isAdditionalStoreStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, string prop, DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
LegacyFlowStep::storeStep(pred, succ, prop)
|
|
|
|
|
@@ -1228,7 +1237,7 @@ private predicate isAdditionalStoreStep(
|
|
|
|
|
/**
|
|
|
|
|
* Holds if the property `loadProp` should be copied from the object `pred` to the property `storeProp` of object `succ`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isAdditionalLoadStoreStep(
|
|
|
|
|
deprecated private predicate isAdditionalLoadStoreStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, string loadProp, string storeProp,
|
|
|
|
|
DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
@@ -1248,7 +1257,7 @@ private predicate isAdditionalLoadStoreStep(
|
|
|
|
|
* Holds if property `prop` of `pred` may flow into `succ` along a path summarized by
|
|
|
|
|
* `summary`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate loadStep(
|
|
|
|
|
deprecated private predicate loadStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, string prop, DataFlow::Configuration cfg,
|
|
|
|
|
PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1270,7 +1279,7 @@ private predicate loadStep(
|
|
|
|
|
* the flow that originally reached `base.startProp` used a call edge.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noopt]
|
|
|
|
|
private predicate reachableFromStoreBase(
|
|
|
|
|
deprecated private predicate reachableFromStoreBase(
|
|
|
|
|
string startProp, string endProp, DataFlow::Node base, DataFlow::Node nd,
|
|
|
|
|
DataFlow::Configuration cfg, TPathSummary summary, boolean onlyRelevantInCall
|
|
|
|
|
) {
|
|
|
|
|
@@ -1310,7 +1319,7 @@ private predicate reachableFromStoreBase(
|
|
|
|
|
)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
private boolean hasCall(PathSummary summary) { result = summary.hasCall() }
|
|
|
|
|
deprecated private boolean hasCall(PathSummary summary) { result = summary.hasCall() }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if the value of `pred` is written to a property of some base object, and that base
|
|
|
|
|
@@ -1320,7 +1329,7 @@ private boolean hasCall(PathSummary summary) { result = summary.hasCall() }
|
|
|
|
|
* In other words, `pred` may flow to `succ` through a property.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate flowThroughProperty(
|
|
|
|
|
deprecated private predicate flowThroughProperty(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
exists(PathSummary oldSummary, PathSummary newSummary |
|
|
|
|
|
@@ -1336,7 +1345,7 @@ private predicate flowThroughProperty(
|
|
|
|
|
* by `oldSummary`.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate storeToLoad(
|
|
|
|
|
deprecated private predicate storeToLoad(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg, PathSummary oldSummary,
|
|
|
|
|
PathSummary newSummary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1358,7 +1367,7 @@ private predicate storeToLoad(
|
|
|
|
|
* All of this is done under configuration `cfg`, and `arg` flows along a path
|
|
|
|
|
* summarized by `summary`, while `cb` is only tracked locally.
|
|
|
|
|
*/
|
|
|
|
|
private predicate summarizedHigherOrderCall(
|
|
|
|
|
deprecated private predicate summarizedHigherOrderCall(
|
|
|
|
|
DataFlow::Node arg, DataFlow::Node cb, int i, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
exists(
|
|
|
|
|
@@ -1388,7 +1397,7 @@ private predicate summarizedHigherOrderCall(
|
|
|
|
|
* @see `summarizedHigherOrderCall`.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate summarizedHigherOrderCallAux(
|
|
|
|
|
deprecated private predicate summarizedHigherOrderCallAux(
|
|
|
|
|
Function f, DataFlow::Node arg, DataFlow::Node innerArg, DataFlow::Configuration cfg,
|
|
|
|
|
PathSummary oldSummary, DataFlow::SourceNode cbParm, DataFlow::InvokeNode inner, int j,
|
|
|
|
|
DataFlow::Node cb
|
|
|
|
|
@@ -1426,7 +1435,7 @@ private predicate summarizedHigherOrderCallAux(
|
|
|
|
|
* invocation of the callback.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate higherOrderCall(
|
|
|
|
|
deprecated private predicate higherOrderCall(
|
|
|
|
|
DataFlow::Node arg, DataFlow::SourceNode callback, int i, DataFlow::Configuration cfg,
|
|
|
|
|
PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1462,7 +1471,7 @@ private predicate higherOrderCall(
|
|
|
|
|
* All of this is done under configuration `cfg`, and `arg` flows along a path
|
|
|
|
|
* summarized by `summary`, while `cb` is only tracked locally.
|
|
|
|
|
*/
|
|
|
|
|
private predicate flowIntoHigherOrderCall(
|
|
|
|
|
deprecated private predicate flowIntoHigherOrderCall(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Node succ, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
exists(DataFlow::FunctionNode cb, int i, PathSummary oldSummary |
|
|
|
|
|
@@ -1485,7 +1494,7 @@ private predicate flowIntoHigherOrderCall(
|
|
|
|
|
* Holds if there is a flow step from `pred` to `succ` described by `summary`
|
|
|
|
|
* under configuration `cfg`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate flowStep(
|
|
|
|
|
deprecated private predicate flowStep(
|
|
|
|
|
DataFlow::Node pred, DataFlow::Configuration cfg, DataFlow::Node succ, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
(
|
|
|
|
|
@@ -1513,7 +1522,7 @@ private predicate flowStep(
|
|
|
|
|
* in zero or more steps.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate flowsTo(
|
|
|
|
|
deprecated private predicate flowsTo(
|
|
|
|
|
PathNode flowsource, DataFlow::Node source, SinkPathNode flowsink, DataFlow::Node sink,
|
|
|
|
|
DataFlow::Configuration cfg
|
|
|
|
|
) {
|
|
|
|
|
@@ -1527,7 +1536,7 @@ private predicate flowsTo(
|
|
|
|
|
* `summary`.
|
|
|
|
|
*/
|
|
|
|
|
pragma[nomagic]
|
|
|
|
|
private predicate reachableFromSource(
|
|
|
|
|
deprecated private predicate reachableFromSource(
|
|
|
|
|
DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
exists(FlowLabel lbl |
|
|
|
|
|
@@ -1548,7 +1557,9 @@ private predicate reachableFromSource(
|
|
|
|
|
* Holds if `nd` can be reached from a source under `cfg`, and in turn a sink is
|
|
|
|
|
* reachable from `nd`, where the path from the source to `nd` is summarized by `summary`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary) {
|
|
|
|
|
deprecated private predicate onPath(
|
|
|
|
|
DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
reachableFromSource(nd, cfg, summary) and
|
|
|
|
|
isSink(nd, cfg, summary.getEndLabel()) and
|
|
|
|
|
not cfg.isBarrier(nd) and
|
|
|
|
|
@@ -1567,7 +1578,7 @@ private predicate onPath(DataFlow::Node nd, DataFlow::Configuration cfg, PathSum
|
|
|
|
|
* This predicate has been outlined from `onPath` to give the optimizer a hint about join-ordering.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate onPathStep(
|
|
|
|
|
deprecated private predicate onPathStep(
|
|
|
|
|
DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary, PathSummary stepSummary,
|
|
|
|
|
DataFlow::Node mid
|
|
|
|
|
) {
|
|
|
|
|
@@ -1579,26 +1590,30 @@ private predicate onPathStep(
|
|
|
|
|
* Holds if there is a configuration that has at least one source and at least one sink.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate isLive() {
|
|
|
|
|
deprecated private predicate isLive() {
|
|
|
|
|
exists(DataFlow::Configuration cfg | isSource(_, cfg, _) and isSink(_, cfg, _))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* A data flow node on an inter-procedural path from a source.
|
|
|
|
|
*/
|
|
|
|
|
private newtype TPathNode =
|
|
|
|
|
MkSourceNode(DataFlow::Node nd, DataFlow::Configuration cfg) { isSourceNode(nd, cfg, _) } or
|
|
|
|
|
MkMidNode(DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary) {
|
|
|
|
|
deprecated private newtype TPathNode =
|
|
|
|
|
deprecated MkSourceNode(DataFlow::Node nd, DataFlow::Configuration cfg) {
|
|
|
|
|
isSourceNode(nd, cfg, _)
|
|
|
|
|
} or
|
|
|
|
|
deprecated MkMidNode(DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary) {
|
|
|
|
|
isLive() and
|
|
|
|
|
onPath(nd, cfg, summary)
|
|
|
|
|
} or
|
|
|
|
|
MkSinkNode(DataFlow::Node nd, DataFlow::Configuration cfg) { isSinkNode(nd, cfg, _) }
|
|
|
|
|
deprecated MkSinkNode(DataFlow::Node nd, DataFlow::Configuration cfg) { isSinkNode(nd, cfg, _) }
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Holds if `nd` is a source node for configuration `cfg`, and there is a path from `nd` to a sink
|
|
|
|
|
* with the given `summary`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isSourceNode(DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary) {
|
|
|
|
|
deprecated private predicate isSourceNode(
|
|
|
|
|
DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
exists(FlowLabel lbl | summary = PathSummary::level(lbl) |
|
|
|
|
|
isSource(nd, cfg, lbl) and
|
|
|
|
|
isLive() and
|
|
|
|
|
@@ -1610,7 +1625,9 @@ private predicate isSourceNode(DataFlow::Node nd, DataFlow::Configuration cfg, P
|
|
|
|
|
* Holds if `nd` is a sink node for configuration `cfg`, and there is a path from a source to `nd`
|
|
|
|
|
* with the given `summary`.
|
|
|
|
|
*/
|
|
|
|
|
private predicate isSinkNode(DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary) {
|
|
|
|
|
deprecated private predicate isSinkNode(
|
|
|
|
|
DataFlow::Node nd, DataFlow::Configuration cfg, PathSummary summary
|
|
|
|
|
) {
|
|
|
|
|
isSink(nd, cfg, summary.getEndLabel()) and
|
|
|
|
|
isLive() and
|
|
|
|
|
onPath(nd, cfg, summary)
|
|
|
|
|
@@ -1623,7 +1640,9 @@ private predicate isSinkNode(DataFlow::Node nd, DataFlow::Configuration cfg, Pat
|
|
|
|
|
* from computing a cross-product of all path nodes belonging to the same configuration.
|
|
|
|
|
*/
|
|
|
|
|
bindingset[cfg, result]
|
|
|
|
|
private DataFlow::Configuration id(DataFlow::Configuration cfg) { result >= cfg and cfg >= result }
|
|
|
|
|
deprecated private DataFlow::Configuration id(DataFlow::Configuration cfg) {
|
|
|
|
|
result >= cfg and cfg >= result
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* A data-flow node on an inter-procedural path from a source to a sink.
|
|
|
|
|
@@ -1641,7 +1660,7 @@ private DataFlow::Configuration id(DataFlow::Configuration cfg) { result >= cfg
|
|
|
|
|
* some source to the node with the given summary that can be extended to a path to some sink node,
|
|
|
|
|
* all under the configuration.
|
|
|
|
|
*/
|
|
|
|
|
class PathNode extends TPathNode {
|
|
|
|
|
deprecated class PathNode extends TPathNode {
|
|
|
|
|
DataFlow::Node nd;
|
|
|
|
|
Configuration cfg;
|
|
|
|
|
|
|
|
|
|
@@ -1697,7 +1716,7 @@ class PathNode extends TPathNode {
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/** Gets the mid node corresponding to `src`. */
|
|
|
|
|
private MidPathNode initialMidNode(SourcePathNode src) {
|
|
|
|
|
deprecated private MidPathNode initialMidNode(SourcePathNode src) {
|
|
|
|
|
exists(DataFlow::Node nd, Configuration cfg, PathSummary summary |
|
|
|
|
|
result.wraps(nd, cfg, summary) and
|
|
|
|
|
src = MkSourceNode(nd, cfg) and
|
|
|
|
|
@@ -1706,7 +1725,7 @@ private MidPathNode initialMidNode(SourcePathNode src) {
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/** Gets the mid node corresponding to `snk`. */
|
|
|
|
|
private MidPathNode finalMidNode(SinkPathNode snk) {
|
|
|
|
|
deprecated private MidPathNode finalMidNode(SinkPathNode snk) {
|
|
|
|
|
exists(DataFlow::Node nd, Configuration cfg, PathSummary summary |
|
|
|
|
|
result.wraps(nd, cfg, summary) and
|
|
|
|
|
snk = MkSinkNode(nd, cfg) and
|
|
|
|
|
@@ -1721,7 +1740,7 @@ private MidPathNode finalMidNode(SinkPathNode snk) {
|
|
|
|
|
* This helper predicate exists to clarify the intended join order in `getASuccessor` below.
|
|
|
|
|
*/
|
|
|
|
|
pragma[noinline]
|
|
|
|
|
private predicate midNodeStep(
|
|
|
|
|
deprecated private predicate midNodeStep(
|
|
|
|
|
PathNode nd, DataFlow::Node predNd, Configuration cfg, PathSummary summary, DataFlow::Node succNd,
|
|
|
|
|
PathSummary newSummary
|
|
|
|
|
) {
|
|
|
|
|
@@ -1732,7 +1751,7 @@ private predicate midNodeStep(
|
|
|
|
|
/**
|
|
|
|
|
* Gets a node to which data from `nd` may flow in one step.
|
|
|
|
|
*/
|
|
|
|
|
private PathNode getASuccessor(PathNode nd) {
|
|
|
|
|
deprecated private PathNode getASuccessor(PathNode nd) {
|
|
|
|
|
// source node to mid node
|
|
|
|
|
result = initialMidNode(nd)
|
|
|
|
|
or
|
|
|
|
|
@@ -1746,7 +1765,7 @@ private PathNode getASuccessor(PathNode nd) {
|
|
|
|
|
nd = finalMidNode(result)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
private PathNode getASuccessorIfHidden(PathNode nd) {
|
|
|
|
|
deprecated private PathNode getASuccessorIfHidden(PathNode nd) {
|
|
|
|
|
nd.(MidPathNode).isHidden() and
|
|
|
|
|
result = getASuccessor(nd)
|
|
|
|
|
}
|
|
|
|
|
@@ -1758,7 +1777,7 @@ private PathNode getASuccessorIfHidden(PathNode nd) {
|
|
|
|
|
* is a configuration such that `nd` is on a path from a source to a sink under `cfg`
|
|
|
|
|
* summarized by `summary`.
|
|
|
|
|
*/
|
|
|
|
|
class MidPathNode extends PathNode, MkMidNode {
|
|
|
|
|
deprecated class MidPathNode extends PathNode, MkMidNode {
|
|
|
|
|
PathSummary summary;
|
|
|
|
|
|
|
|
|
|
MidPathNode() { this = MkMidNode(nd, cfg, summary) }
|
|
|
|
|
@@ -1779,6 +1798,7 @@ class MidPathNode extends PathNode, MkMidNode {
|
|
|
|
|
module PathNode {
|
|
|
|
|
/** Holds if `nd` should be hidden in data flow paths. */
|
|
|
|
|
predicate shouldNodeBeHidden(DataFlow::Node nd) {
|
|
|
|
|
// TODO: move to DataFlowPrivate
|
|
|
|
|
// Skip phi, refinement, and capture nodes
|
|
|
|
|
nd.(DataFlow::SsaDefinitionNode).getSsaVariable().getDefinition() instanceof
|
|
|
|
|
SsaImplicitDefinition
|
|
|
|
|
@@ -1809,21 +1829,21 @@ module PathNode {
|
|
|
|
|
/**
|
|
|
|
|
* A path node corresponding to a flow source.
|
|
|
|
|
*/
|
|
|
|
|
class SourcePathNode extends PathNode, MkSourceNode {
|
|
|
|
|
deprecated class SourcePathNode extends PathNode, MkSourceNode {
|
|
|
|
|
SourcePathNode() { this = MkSourceNode(nd, cfg) }
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* A path node corresponding to a flow sink.
|
|
|
|
|
*/
|
|
|
|
|
class SinkPathNode extends PathNode, MkSinkNode {
|
|
|
|
|
deprecated class SinkPathNode extends PathNode, MkSinkNode {
|
|
|
|
|
SinkPathNode() { this = MkSinkNode(nd, cfg) }
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* Provides the query predicates needed to include a graph in a path-problem query.
|
|
|
|
|
*/
|
|
|
|
|
module PathGraph {
|
|
|
|
|
deprecated module PathGraph {
|
|
|
|
|
/** Holds if `nd` is a node in the graph of data flow path explanations. */
|
|
|
|
|
query predicate nodes(PathNode nd) { not nd.(MidPathNode).isHidden() }
|
|
|
|
|
|
|
|
|
|
@@ -1877,7 +1897,7 @@ module PathGraph {
|
|
|
|
|
/**
|
|
|
|
|
* Gets a logical `and` expression, or parenthesized expression, that contains `guard`.
|
|
|
|
|
*/
|
|
|
|
|
private Expr getALogicalAndParent(BarrierGuardNodeInternal guard) {
|
|
|
|
|
deprecated private Expr getALogicalAndParent(BarrierGuardNodeInternal guard) {
|
|
|
|
|
barrierGuardIsRelevant(guard) and result = guard.asExpr()
|
|
|
|
|
or
|
|
|
|
|
result.(LogAndExpr).getAnOperand() = getALogicalAndParent(guard)
|
|
|
|
|
@@ -1888,7 +1908,7 @@ private Expr getALogicalAndParent(BarrierGuardNodeInternal guard) {
|
|
|
|
|
/**
|
|
|
|
|
* Gets a logical `or` expression, or parenthesized expression, that contains `guard`.
|
|
|
|
|
*/
|
|
|
|
|
private Expr getALogicalOrParent(BarrierGuardNodeInternal guard) {
|
|
|
|
|
deprecated private Expr getALogicalOrParent(BarrierGuardNodeInternal guard) {
|
|
|
|
|
barrierGuardIsRelevant(guard) and result = guard.asExpr()
|
|
|
|
|
or
|
|
|
|
|
result.(LogOrExpr).getAnOperand() = getALogicalOrParent(guard)
|
|
|
|
|
@@ -1904,14 +1924,14 @@ private Expr getALogicalOrParent(BarrierGuardNodeInternal guard) {
|
|
|
|
|
* of the standard library. Override `Configuration::isBarrierGuard`
|
|
|
|
|
* for analysis-specific barrier guards.
|
|
|
|
|
*/
|
|
|
|
|
abstract class AdditionalBarrierGuardNode extends BarrierGuardNode {
|
|
|
|
|
abstract deprecated class AdditionalBarrierGuardNode extends BarrierGuardNode {
|
|
|
|
|
abstract predicate appliesTo(Configuration cfg);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
/**
|
|
|
|
|
* A function that returns the result of a barrier guard.
|
|
|
|
|
*/
|
|
|
|
|
private class BarrierGuardFunction extends Function {
|
|
|
|
|
deprecated private class BarrierGuardFunction extends Function {
|
|
|
|
|
DataFlow::ParameterNode sanitizedParameter;
|
|
|
|
|
BarrierGuardNodeInternal guard;
|
|
|
|
|
boolean guardOutcome;
|
|
|
|
|
@@ -1963,7 +1983,9 @@ private class BarrierGuardFunction extends Function {
|
|
|
|
|
/**
|
|
|
|
|
* A call that sanitizes an argument.
|
|
|
|
|
*/
|
|
|
|
|
private class AdditionalBarrierGuardCall extends DerivedBarrierGuardNode, DataFlow::CallNode {
|
|
|
|
|
deprecated private class AdditionalBarrierGuardCall extends DerivedBarrierGuardNode,
|
|
|
|
|
DataFlow::CallNode
|
|
|
|
|
{
|
|
|
|
|
BarrierGuardFunction f;
|
|
|
|
|
|
|
|
|
|
AdditionalBarrierGuardCall() { f.isBarrierCall(this, _, _, _) }
|
|
|
|
|
@@ -1984,7 +2006,7 @@ private class AdditionalBarrierGuardCall extends DerivedBarrierGuardNode, DataFl
|
|
|
|
|
* }
|
|
|
|
|
* ```
|
|
|
|
|
*/
|
|
|
|
|
private class CallAgainstEqualityCheck extends DerivedBarrierGuardNode {
|
|
|
|
|
deprecated private class CallAgainstEqualityCheck extends DerivedBarrierGuardNode {
|
|
|
|
|
BarrierGuardNodeInternal prev;
|
|
|
|
|
boolean polarity;
|
|
|
|
|
|
|
|
|
|
@@ -2026,7 +2048,7 @@ class VarAccessBarrier extends DataFlow::Node {
|
|
|
|
|
/**
|
|
|
|
|
* Holds if there is a path without unmatched return steps from `source` to `sink`.
|
|
|
|
|
*/
|
|
|
|
|
predicate hasPathWithoutUnmatchedReturn(SourcePathNode source, SinkPathNode sink) {
|
|
|
|
|
deprecated predicate hasPathWithoutUnmatchedReturn(SourcePathNode source, SinkPathNode sink) {
|
|
|
|
|
exists(MidPathNode mid |
|
|
|
|
|
source.getASuccessor*() = mid and
|
|
|
|
|
sink = mid.getASuccessor() and
|
|
|
|
|
|