Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ private RefType boxIfNeeded(J::Type t) {

/** Provides the input types and predicates for instantiation of `UniversalFlow`. */
module FlowStepsInput implements UniversalFlow::UniversalFlowInput<Location> {
overlay[local]
private newtype TFlowNode =
TField(Field f) { not f.getType() instanceof PrimitiveType } or
TSsa(Base::SsaDefinition ssa) { not ssa.getSourceVariable().getType() instanceof PrimitiveType } or
Expand All @@ -34,6 +35,7 @@ module FlowStepsInput implements UniversalFlow::UniversalFlowInput<Location> {
/**
* A `Field`, `BaseSsaVariable`, `Expr`, or `Method`.
*/
overlay[local]
class FlowNode extends TFlowNode {
/** Gets a textual representation of this element. */
string toString() {
Expand Down Expand Up @@ -158,6 +160,10 @@ module FlowStepsInput implements UniversalFlow::UniversalFlowInput<Location> {
// reflection and are thus not always null.
exists(n.asField())
}

private import semmle.code.java.Overlay as Overlay

predicate isEvaluatingInOverlay() { Overlay::isOverlay() }
}

private module Input implements TypeFlowInput<Location> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -129,31 +129,35 @@ private predicate safeCallable(Callable c) {
c.hasQualifiedName("org.apache.commons.lang3", "StringUtils", "join")
}

overlay[local]
private predicate collectionWithPossibleMutationBase(FlowNode n) {
not unmodifiableCollection(n) and
exists(Expr e |
n.asExpr() = e and
(e.getType() instanceof CollectionType or e.getType() instanceof Array) and
not collectionAddition(_, e, _) and
not collectionStep(n, _)
|
exists(ArrayAccess aa | e = aa.getArray())
or
exists(Call c, Callable tgt | c.getAnArgument() = e or c.getQualifier() = e |
tgt = c.getCallee().getSourceDeclaration() and
not safeCallable(tgt)
)
)
}

/**
* Holds if `n` might be mutated in ways that adds elements that are not
* tracked by the `collectionAddition` predicate.
*/
private predicate collectionWithPossibleMutation(FlowNode n) {
collectionWithPossibleMutationBase(n)
or
not unmodifiableCollection(n) and
(
exists(Expr e |
n.asExpr() = e and
(e.getType() instanceof CollectionType or e.getType() instanceof Array) and
not collectionAddition(_, e, _) and
not collectionStep(n, _)
|
exists(ArrayAccess aa | e = aa.getArray())
or
exists(Call c, Callable tgt | c.getAnArgument() = e or c.getQualifier() = e |
tgt = c.getCallee().getSourceDeclaration() and
not safeCallable(tgt)
)
)
or
exists(FlowNode mid |
FlowStepsInput::step(n, mid) and
collectionWithPossibleMutation(mid)
)
exists(FlowNode mid |
FlowStepsInput::step(n, mid) and
collectionWithPossibleMutation(mid)
)
}

Expand Down
12 changes: 12 additions & 0 deletions shared/typeflow/codeql/typeflow/TypeFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,18 @@ signature module TypeFlowInput<LocationSig Location> {
*/
default predicate isExcludedFromNullAnalysis(TypeFlowNode n) { 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.
*/
predicate isEvaluatingInOverlay();

/** A type. */
class Type {
/** Gets a textual representation of this type. */
Expand Down
74 changes: 64 additions & 10 deletions shared/typeflow/codeql/typeflow/UniversalFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,18 @@ signature module UniversalFlowInput<LocationSig Location> {
* the null analysis determines that `n` is always null.
*/
default predicate isExcludedFromNullAnalysis(FlowNode n) { 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.
*/
predicate isEvaluatingInOverlay();
}

/**
Expand All @@ -68,23 +80,46 @@ signature module UniversalFlowInput<LocationSig Location> {
module Make<LocationSig Location, UniversalFlowInput<Location> I> {
private import I

overlay[local]
private predicate overlayNode(FlowNode n) { isEvaluatingInOverlay() and exists(n) }

overlay[global]
private predicate canReachOverlay(FlowNode n) {
overlayNode(n)
or
exists(FlowNode mid | canReachOverlay(mid) and step(n, mid))
}

bindingset[n]
private predicate relevantNode(FlowNode n) {
not isEvaluatingInOverlay()
or
canReachOverlay(n)
}

/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is
* functionally determined by `n2`.
*/
private predicate uniqStep(FlowNode n1, FlowNode n2) { n1 = unique(FlowNode n | step(n, n2)) }
private predicate uniqStep(FlowNode n1, FlowNode n2) {
n1 = unique(FlowNode n | step(n, n2)) and relevantNode(n2)
}

/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
* functionally determined by `n2`.
*/
private predicate joinStep(FlowNode n1, FlowNode n2) { step(n1, n2) and not uniqStep(n1, n2) }
private predicate joinStep(FlowNode n1, FlowNode n2) {
step(n1, n2) and not uniqStep(n1, n2) and relevantNode(n2)
}

/** Holds if `null` is the only value that flows to `n`. */
private predicate isNull(FlowNode n) {
isNullValue(n)
isNullValue(n) and
relevantNode(n)
or
not isExcludedFromNullAnalysis(n) and
relevantNode(n) and
(
exists(FlowNode mid | isNull(mid) and uniqStep(mid, n))
or
Expand Down Expand Up @@ -256,21 +291,24 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
private module Propagation implements PropPropagation {
class Prop = Unit;

predicate candProp(FlowNode n, Unit u) { hasProperty(n) and exists(u) }
predicate candProp(FlowNode n, Unit u) { hasPropertyImpl(n) and exists(u) }

predicate supportsProp = candProp/2;
}

/**
* Holds if all flow reaching `n` originates from nodes in
* `hasPropertyBase`.
*
* When evaluated in an overlay-merged context, this is restricted to nodes
* that can reach the overlay.
*/
predicate hasProperty(FlowNode n) {
private predicate hasPropertyImpl(FlowNode n) {
P::hasPropertyBase(n)
or
not P::barrier(n) and
(
exists(FlowNode mid | hasProperty(mid) and uniqStepNotNull(mid, n))
exists(FlowNode mid | hasPropertyImpl(mid) and uniqStepNotNull(mid, n))
or
// The following is an optimized version of
// `forex(FlowNode mid | joinStepNotNull(mid, n) | hasPropery(mid))`
Expand All @@ -284,6 +322,12 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
)
)
}

/**
* Holds if all flow reaching `n` originates from nodes in
* `hasPropertyBase`.
*/
predicate hasProperty(FlowNode n) = forceLocal(hasPropertyImpl/1)(n)
}

signature module PropertySig {
Expand All @@ -305,25 +349,28 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
private module Propagation implements PropPropagation {
class Prop = P::Prop;

predicate candProp = hasProperty/2;
predicate candProp = hasPropertyImpl/2;

bindingset[t]
predicate supportsProp(FlowNode n, Prop t) {
exists(Prop t0 | hasProperty(n, t0) and P::propImplies(t0, t))
exists(Prop t0 | hasPropertyImpl(n, t0) and P::propImplies(t0, t))
}
}

/**
* Holds if all flow reaching `n` originates from nodes in
* `hasPropertyBase`. The property `t` is taken from one of those origins
* such that all other origins imply `t`.
*
* When evaluated in an overlay-merged context, this is restricted to nodes
* that can reach the overlay.
*/
predicate hasProperty(FlowNode n, P::Prop t) {
private predicate hasPropertyImpl(FlowNode n, P::Prop t) {
P::hasPropertyBase(n, t)
or
not P::barrier(n) and
(
exists(FlowNode mid | hasProperty(mid, t) and uniqStepNotNull(mid, n))
exists(FlowNode mid | hasPropertyImpl(mid, t) and uniqStepNotNull(mid, n))
or
// The following is an optimized version of
// ```
Expand All @@ -349,5 +396,12 @@ module Make<LocationSig Location, UniversalFlowInput<Location> I> {
)
)
}

/**
* Holds if all flow reaching `n` originates from nodes in
* `hasPropertyBase`. The property `t` is taken from one of those origins
* such that all other origins imply `t`.
*/
predicate hasProperty(FlowNode n, P::Prop t) = forceLocal(hasPropertyImpl/2)(n, t)
}
}
2 changes: 2 additions & 0 deletions shared/typeflow/codeql/typeflow/internal/TypeFlowImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ module TypeFlow<LocationSig Location, TypeFlowInput<Location> I> {
predicate isNullValue = I::isNullValue/1;

predicate isExcludedFromNullAnalysis = I::isExcludedFromNullAnalysis/1;

predicate isEvaluatingInOverlay = I::isEvaluatingInOverlay/0;
}

private module UnivFlow = UniversalFlow::Make<Location, UfInput>;
Expand Down
Loading