mirror of
https://github.com/github/codeql.git
synced 2025-12-21 11:16:30 +01:00
Data flow: Sync files
This commit is contained in:
@@ -319,8 +319,6 @@ private class ParamNodeEx extends NodeEx {
|
||||
}
|
||||
|
||||
ParameterPosition getPosition() { this.isParameterOf(_, result) }
|
||||
|
||||
predicate allowParameterReturnInSelf() { allowParameterReturnInSelfCached(this.asNode()) }
|
||||
}
|
||||
|
||||
private class RetNodeEx extends NodeEx {
|
||||
@@ -608,6 +606,21 @@ private predicate hasSinkCallCtx(Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if flow from `p` to a return node of kind `kind` is allowed.
|
||||
*
|
||||
* We don't expect a parameter to return stored in itself, unless
|
||||
* explicitly allowed
|
||||
*/
|
||||
bindingset[p, kind]
|
||||
private predicate parameterFlowThroughAllowed(ParamNode p, ReturnKindExt kind) {
|
||||
exists(ParameterPosition pos | p.isParameterOf(_, pos) |
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
allowParameterReturnInSelfCached(p)
|
||||
)
|
||||
}
|
||||
|
||||
private module Stage1 implements StageSig {
|
||||
class Ap = Unit;
|
||||
|
||||
@@ -981,21 +994,22 @@ private module Stage1 implements StageSig {
|
||||
* candidate for the origin of a summary.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(ReturnKindExt kind |
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(DataFlowCallable c, ReturnKindExt kind |
|
||||
throughFlowNodeCand(p, config) and
|
||||
returnFlowCallableNodeCand(c, kind, config) and
|
||||
p.getEnclosingCallable() = c and
|
||||
exists(ap) and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(p.asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
throughFlowNodeCand(ret, config) and
|
||||
pos = ret.getReturnPosition()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(ArgNodeEx arg, boolean toReturn |
|
||||
@@ -1052,9 +1066,10 @@ private predicate viableReturnPosOutNodeCand1(
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Configuration config
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
viableReturnPosOutNodeCand1(call, pos, out, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
@@ -1090,7 +1105,7 @@ private predicate flowIntoCallNodeCand1(
|
||||
private int branch(NodeEx n1, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n1, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
flowOutOfCallNodeCand1(_, n1, _, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1102,7 +1117,7 @@ private int branch(NodeEx n1, Configuration conf) {
|
||||
private int join(NodeEx n2, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
flowOutOfCallNodeCand1(_, n, _, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1115,12 +1130,13 @@ private int join(NodeEx n2, Configuration conf) {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, ret, out, config) and
|
||||
flowOutOfCallNodeCand1(call, ret, pos, out, pragma[only_bind_into](config)) and
|
||||
exists(int b, int j |
|
||||
b = branch(ret, config) and
|
||||
j = join(out, config) and
|
||||
b = branch(ret, pragma[only_bind_into](config)) and
|
||||
j = join(out, pragma[only_bind_into](config)) and
|
||||
if b.minimum(j) <= config.fieldFlowBranchLimit()
|
||||
then allowsFieldFlow = true
|
||||
else allowsFieldFlow = false
|
||||
@@ -1156,7 +1172,9 @@ private signature module StageSig {
|
||||
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config);
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config);
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config);
|
||||
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config);
|
||||
|
||||
predicate storeStepCand(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, DataFlowType contentType,
|
||||
@@ -1222,7 +1240,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
);
|
||||
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
);
|
||||
|
||||
predicate flowIntoCall(
|
||||
@@ -1247,14 +1266,16 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughOutOfCall(
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, ReturnKindExt kind, NodeEx out,
|
||||
boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(_, ret.getEnclosingCallable(), _,
|
||||
pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
exists(ReturnPosition pos |
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
kind = pos.getKind() and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::returnMayFlowThrough(ret, pos, pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1262,29 +1283,32 @@ private module MkStage<StageSig PrevStage> {
|
||||
* configuration `config`.
|
||||
*
|
||||
* The call context `cc` records whether the node is reached through an
|
||||
* argument in a call, and if so, `argAp` records the access path of that
|
||||
* argument.
|
||||
* argument in a call, and if so, `summaryCtx` and `argAp` record the
|
||||
* corresponding parameter and access path of that argument, respectively.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate fwdFlow(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow0(node, state, cc, argAp, ap, config) and
|
||||
fwdFlow0(node, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::revFlow(node, state, unbindApa(getApprox(ap)), config) and
|
||||
filter(node, state, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlow0(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
sourceNode(node, state, config) and
|
||||
(if hasSourceCallCtx(config) then cc = ccSomeCall() else cc = ccNone()) and
|
||||
argAp = apNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
ap = getApNil(node)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
@@ -1295,65 +1319,72 @@ private module MkStage<StageSig PrevStage> {
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
jumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(mid, state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(mid, state0, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state0, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(mid, state0, node, state, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(TypedContent tc, Ap ap0 |
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, argAp, config) and
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, summaryCtx, argAp, config) and
|
||||
ap = apCons(tc, ap0)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Ap ap0, Content c |
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, argAp, config) and
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, summaryCtx, argAp, config) and
|
||||
fwdFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(ApApprox apa |
|
||||
fwdFlowIn(_, node, state, _, cc, _, ap, config) and
|
||||
fwdFlowIn(_, node, state, _, cc, _, _, ap, config) and
|
||||
apa = getApprox(ap) and
|
||||
if PrevStage::parameterMayFlowThrough(node, _, apa, config)
|
||||
then argAp = apSome(ap)
|
||||
else argAp = apNone()
|
||||
if PrevStage::parameterMayFlowThrough(node, apa, config)
|
||||
then (
|
||||
summaryCtx = TParamNodeSome(node.asNode()) and argAp = apSome(ap)
|
||||
) else (
|
||||
summaryCtx = TParamNodeNone() and argAp = apNone()
|
||||
)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
fwdFlowOutNotFromArg(node, state, cc, argAp, ap, config)
|
||||
fwdFlowOutNotFromArg(node, state, cc, summaryCtx, argAp, ap, config)
|
||||
or
|
||||
exists(DataFlowCall call, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ParamNode summaryCtx0, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, summaryCtx, argAp, summaryCtx0, argAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowStore(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
exists(DataFlowType contentType |
|
||||
fwdFlow(node1, state, cc, argAp, ap1, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, config) and
|
||||
PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
|
||||
typecheckStore(ap1, contentType)
|
||||
)
|
||||
@@ -1366,7 +1397,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
|
||||
exists(TypedContent tc |
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, config) and
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, _, config) and
|
||||
tc.getContent() = c and
|
||||
cons = apCons(tc, tail)
|
||||
)
|
||||
@@ -1374,21 +1405,21 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
fwdFlow(node1, state, cc, argAp, ap, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::readStepCand(node1, c, node2, config) and
|
||||
getHeadContent(ap) = c
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc, ApOption argAp,
|
||||
Ap ap, Configuration config
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow |
|
||||
fwdFlow(arg, state, outercc, argAp, ap, config) and
|
||||
fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, config) and
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1397,14 +1428,15 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutNotFromArg(
|
||||
NodeEx out, FlowState state, Cc ccOut, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx out, FlowState state, Cc ccOut, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(
|
||||
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
|
||||
DataFlowCallable inner
|
||||
|
|
||||
fwdFlow(ret, state, innercc, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, _, out, allowsFieldFlow, config) and
|
||||
inner = ret.getEnclosingCallable() and
|
||||
ccOut = getCallContextReturn(inner, call, innercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1413,12 +1445,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutFromArg(
|
||||
DataFlowCall call, NodeEx out, FlowState state, Ap argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, NodeEx out, FlowState state, ParamNode summaryCtx, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
exists(RetNodeEx ret, ReturnKindExt kind, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(summaryCtx), apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, kind, out, allowsFieldFlow, config) and
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(summaryCtx, kind)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1428,11 +1462,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIsEntered(
|
||||
DataFlowCall call, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, ParamNode p, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p |
|
||||
fwdFlowIn(call, p, _, cc, _, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
|
||||
exists(ParamNodeEx param |
|
||||
fwdFlowIn(call, param, _, cc, _, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(param, unbindApa(getApprox(ap)), config) and
|
||||
p = param.asNode()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1440,146 +1476,149 @@ private module MkStage<StageSig PrevStage> {
|
||||
private predicate storeStepFwd(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, config) and
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, _, config) and
|
||||
ap2 = apCons(tc, ap1) and
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, config)
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, _, config)
|
||||
}
|
||||
|
||||
private predicate readStepFwd(
|
||||
NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, config) and
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, _, config) and
|
||||
fwdFlowConsCand(ap1, c, ap2, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
|
||||
exists(Ap argAp0, NodeEx out, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(out, state, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlowOutFromArg(call, out, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
|
||||
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
|
||||
pragma[only_bind_into](config))
|
||||
)
|
||||
private predicate returnFlowsThrough(
|
||||
RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNode p, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(p), apSome(argAp), ap, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
parameterFlowThroughAllowed(p, pos.getKind())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughIntoCall(
|
||||
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
fwdFlow(arg, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, _, pragma[only_bind_into](config)) and
|
||||
callMayFlowThroughFwd(call, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate returnNodeMayFlowThrough(
|
||||
RetNodeEx ret, FlowState state, Ap ap, Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(_), ap, config)
|
||||
flowIntoCall(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), allowsFieldFlow,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
returnFlowsThrough(_, _, _, _, p.asNode(), _, _, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` with access path `ap` is part of a path from a source to a
|
||||
* sink in the configuration `config`.
|
||||
*
|
||||
* The Boolean `toReturn` records whether the node must be returned from the
|
||||
* enclosing callable in order to reach a sink, and if so, `returnAp` records
|
||||
* the access path of the returned value.
|
||||
* The parameter `returnCtx` records whether (and how) the node must be returned
|
||||
* from the enclosing callable in order to reach a sink, and if so, `returnAp`
|
||||
* records the access path of the returned value.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
revFlow0(node, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, ap, config)
|
||||
revFlow0(node, state, returnCtx, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlow0(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(node, state, _, _, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config) and
|
||||
sinkNode(node, state, config) and
|
||||
(if hasSinkCallCtx(config) then toReturn = true else toReturn = false) and
|
||||
(
|
||||
if hasSinkCallCtx(config)
|
||||
then returnCtx = TReturnCtxNoFlowThrough()
|
||||
else returnCtx = TReturnCtxNone()
|
||||
) and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
localStep(node, state, mid, state0, true, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, ap, config)
|
||||
revFlow(mid, state0, returnCtx, returnAp, ap, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
localStep(node, pragma[only_bind_into](state), mid, state0, false, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, state0, returnCtx, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
jumpStep(node, mid, config) and
|
||||
revFlow(mid, state, _, _, ap, config) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(node, mid, config) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(node, state, mid, state0, config) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, nil,
|
||||
pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Ap ap0, Content c |
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, toReturn, returnAp, config) and
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, returnCtx, returnAp, config) and
|
||||
revFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Ap ap0 |
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
readStepFwd(node, ap, _, mid, ap0, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
revFlowInNotToReturn(node, state, returnAp, ap, config) and
|
||||
toReturn = false
|
||||
returnCtx = TReturnCtxNone()
|
||||
or
|
||||
exists(DataFlowCall call, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ReturnPosition returnPos0, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
revFlowOut(_, node, state, _, _, ap, config) and
|
||||
toReturn = true and
|
||||
if returnNodeMayFlowThrough(node, state, ap, config)
|
||||
then returnAp = apSome(ap)
|
||||
else returnAp = apNone()
|
||||
exists(ReturnPosition pos |
|
||||
revFlowOut(_, node, pos, state, _, _, ap, config) and
|
||||
if returnFlowsThrough(node, pos, state, _, _, _, ap, config)
|
||||
then (
|
||||
returnCtx = TReturnCtxMaybeFlowThrough(pos) and
|
||||
returnAp = apSome(ap)
|
||||
) else (
|
||||
returnCtx = TReturnCtxNoFlowThrough() and returnAp = apNone()
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowStore(
|
||||
Ap ap0, Content c, Ap ap, NodeEx node, FlowState state, TypedContent tc, NodeEx mid,
|
||||
boolean toReturn, ApOption returnAp, Configuration config
|
||||
ReturnCtx returnCtx, ApOption returnAp, Configuration config
|
||||
) {
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
storeStepFwd(node, ap, tc, mid, ap0, config) and
|
||||
tc.getContent() = c
|
||||
}
|
||||
@@ -1599,12 +1638,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowOut(
|
||||
DataFlowCall call, RetNodeEx ret, FlowState state, boolean toReturn, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state, ReturnCtx returnCtx,
|
||||
ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(NodeEx out, boolean allowsFieldFlow |
|
||||
revFlow(out, state, toReturn, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
revFlow(out, state, returnCtx, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
}
|
||||
@@ -1614,7 +1653,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
ArgNodeEx arg, FlowState state, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, false, returnAp, ap, config) and
|
||||
revFlow(p, state, TReturnCtxNone(), returnAp, ap, config) and
|
||||
flowIntoCall(_, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
@@ -1622,12 +1661,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowInToReturn(
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, Ap returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnPosition returnPos, Ap returnAp,
|
||||
Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, true, apSome(returnAp), ap, config) and
|
||||
revFlow(p, state, TReturnCtxMaybeFlowThrough(returnPos), apSome(returnAp), ap, config) and
|
||||
flowThroughIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1638,11 +1679,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReturned(
|
||||
DataFlowCall call, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ReturnCtx returnCtx, ApOption returnAp, ReturnPosition pos, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, FlowState state, CcCall ccc |
|
||||
revFlowOut(call, ret, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(ret, state, ccc, apSome(_), ap, config) and
|
||||
revFlowOut(call, ret, pos, state, returnCtx, returnAp, ap, config) and
|
||||
returnFlowsThrough(ret, pos, state, ccc, _, _, ap, config) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
@@ -1713,40 +1755,39 @@ private module MkStage<StageSig PrevStage> {
|
||||
validAp(ap, config)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate parameterFlow(
|
||||
ParamNodeEx p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
|
||||
pragma[nomagic]
|
||||
private predicate parameterFlowsThroughRev(
|
||||
ParamNodeEx p, Ap ap, ReturnPosition returnPos, Configuration config
|
||||
) {
|
||||
revFlow(p, _, true, apSome(ap0), ap, config) and
|
||||
c = p.getEnclosingCallable()
|
||||
revFlow(p, _, TReturnCtxMaybeFlowThrough(returnPos), apSome(_), ap, config) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
}
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, FlowState state, Ap ap0, ReturnKindExt kind, ParameterPosition pos |
|
||||
parameterFlow(p, ap, ap0, c, config) and
|
||||
c = ret.getEnclosingCallable() and
|
||||
revFlow(pragma[only_bind_into](ret), pragma[only_bind_into](state), true, apSome(_),
|
||||
pragma[only_bind_into](ap0), pragma[only_bind_into](config)) and
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(ap), ap0, config) and
|
||||
kind = ret.getKind() and
|
||||
p.getPosition() = pos and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, ReturnPosition pos |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
exists(ParamNodeEx p, Ap ap |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(
|
||||
Ap returnAp0, ArgNodeEx arg, FlowState state, boolean toReturn, ApOption returnAp, Ap ap
|
||||
ReturnPosition returnPos0, Ap returnAp0, ArgNodeEx arg, FlowState state,
|
||||
ReturnCtx returnCtx, ApOption returnAp, Ap ap
|
||||
|
|
||||
revFlow(arg, state, toReturn, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
revFlow(arg, state, returnCtx, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1754,13 +1795,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, Configuration config
|
||||
) {
|
||||
fwd = true and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, config)) and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, config)) and
|
||||
fields = count(TypedContent f0 | fwdConsCand(f0, _, config)) and
|
||||
conscand = count(TypedContent f0, Ap ap | fwdConsCand(f0, ap, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, argAp, ap, config)
|
||||
count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, summaryCtx, argAp, ap, config)
|
||||
)
|
||||
or
|
||||
fwd = false and
|
||||
@@ -1769,8 +1810,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
conscand = count(TypedContent f0, Ap ap | consCand(f0, ap, config)) and
|
||||
states = count(FlowState state | revFlow(_, state, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, boolean b, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, b, retAp, ap, config)
|
||||
count(NodeEx n, FlowState state, ReturnCtx returnCtx, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, returnCtx, retAp, ap, config)
|
||||
)
|
||||
}
|
||||
/* End: Stage logic. */
|
||||
@@ -1915,7 +1956,7 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
|
||||
exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand1/5;
|
||||
|
||||
@@ -1951,9 +1992,10 @@ private module Stage2 implements StageSig {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand2(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand1(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
Stage2::revFlow(node2, pragma[only_bind_into](config)) and
|
||||
Stage2::revFlowAlias(node1, pragma[only_bind_into](config))
|
||||
}
|
||||
@@ -2021,8 +2063,8 @@ private module LocalFlowBigStep {
|
||||
exists(NodeEx next | Stage2::revFlow(next, state, config) |
|
||||
jumpStep(node, next, config) or
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
flowIntoCallNodeCand2(_, node, next, _, config) or
|
||||
flowOutOfCallNodeCand2(_, node, _, next, _, config) or
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
@@ -2163,7 +2205,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
|
||||
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap, config, _) and exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
@@ -2233,8 +2275,9 @@ private predicate flowCandSummaryCtx(
|
||||
NodeEx node, FlowState state, AccessPathFront argApf, Configuration config
|
||||
) {
|
||||
exists(AccessPathFront apf |
|
||||
Stage3::revFlow(node, state, true, _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), TAccessPathFrontSome(argApf), apf, config)
|
||||
Stage3::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), _, TAccessPathFrontSome(argApf), apf,
|
||||
config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2468,10 +2511,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
exists(FlowState state |
|
||||
flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand2(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
|
||||
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
|
||||
pragma[only_bind_into](config))
|
||||
@@ -2508,13 +2552,13 @@ private Configuration unbindConf(Configuration conf) {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeMayUseSummary0(
|
||||
NodeEx n, DataFlowCallable c, FlowState state, AccessPathApprox apa, Configuration config
|
||||
NodeEx n, ParamNodeEx p, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(AccessPathApprox apa0 |
|
||||
Stage4::parameterMayFlowThrough(_, c, _, _) and
|
||||
Stage4::revFlow(n, state, true, _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
|
||||
n.getEnclosingCallable() = c
|
||||
Stage4::parameterMayFlowThrough(p, _, _) and
|
||||
Stage4::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()),
|
||||
TAccessPathApproxSome(apa), apa0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2522,9 +2566,9 @@ pragma[nomagic]
|
||||
private predicate nodeMayUseSummary(
|
||||
NodeEx n, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(DataFlowCallable c |
|
||||
Stage4::parameterMayFlowThrough(_, c, apa, config) and
|
||||
nodeMayUseSummary0(n, c, state, apa, config)
|
||||
exists(ParamNodeEx p |
|
||||
Stage4::parameterMayFlowThrough(p, apa, config) and
|
||||
nodeMayUseSummary0(n, p, state, apa, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2532,7 +2576,7 @@ private newtype TSummaryCtx =
|
||||
TSummaryCtxNone() or
|
||||
TSummaryCtxSome(ParamNodeEx p, FlowState state, AccessPath ap) {
|
||||
exists(Configuration config |
|
||||
Stage4::parameterMayFlowThrough(p, _, ap.getApprox(), config) and
|
||||
Stage4::parameterMayFlowThrough(p, ap.getApprox(), config) and
|
||||
Stage4::revFlow(p, state, _, config)
|
||||
)
|
||||
}
|
||||
@@ -3453,17 +3497,11 @@ private predicate paramFlowsThrough(
|
||||
ReturnKindExt kind, FlowState state, CallContextCall cc, SummaryCtxSome sc, AccessPath ap,
|
||||
AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(PathNodeMid mid, RetNodeEx ret, ParameterPosition pos |
|
||||
exists(PathNodeMid mid, RetNodeEx ret |
|
||||
pathNode(mid, ret, state, cc, sc, ap, config, _) and
|
||||
kind = ret.getKind() and
|
||||
apa = ap.getApprox() and
|
||||
pos = sc.getParameterPos() and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
sc.getParamNode().allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(sc.getParamNode().asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -319,8 +319,6 @@ private class ParamNodeEx extends NodeEx {
|
||||
}
|
||||
|
||||
ParameterPosition getPosition() { this.isParameterOf(_, result) }
|
||||
|
||||
predicate allowParameterReturnInSelf() { allowParameterReturnInSelfCached(this.asNode()) }
|
||||
}
|
||||
|
||||
private class RetNodeEx extends NodeEx {
|
||||
@@ -608,6 +606,21 @@ private predicate hasSinkCallCtx(Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if flow from `p` to a return node of kind `kind` is allowed.
|
||||
*
|
||||
* We don't expect a parameter to return stored in itself, unless
|
||||
* explicitly allowed
|
||||
*/
|
||||
bindingset[p, kind]
|
||||
private predicate parameterFlowThroughAllowed(ParamNode p, ReturnKindExt kind) {
|
||||
exists(ParameterPosition pos | p.isParameterOf(_, pos) |
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
allowParameterReturnInSelfCached(p)
|
||||
)
|
||||
}
|
||||
|
||||
private module Stage1 implements StageSig {
|
||||
class Ap = Unit;
|
||||
|
||||
@@ -981,21 +994,22 @@ private module Stage1 implements StageSig {
|
||||
* candidate for the origin of a summary.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(ReturnKindExt kind |
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(DataFlowCallable c, ReturnKindExt kind |
|
||||
throughFlowNodeCand(p, config) and
|
||||
returnFlowCallableNodeCand(c, kind, config) and
|
||||
p.getEnclosingCallable() = c and
|
||||
exists(ap) and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(p.asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
throughFlowNodeCand(ret, config) and
|
||||
pos = ret.getReturnPosition()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(ArgNodeEx arg, boolean toReturn |
|
||||
@@ -1052,9 +1066,10 @@ private predicate viableReturnPosOutNodeCand1(
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Configuration config
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
viableReturnPosOutNodeCand1(call, pos, out, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
@@ -1090,7 +1105,7 @@ private predicate flowIntoCallNodeCand1(
|
||||
private int branch(NodeEx n1, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n1, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
flowOutOfCallNodeCand1(_, n1, _, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1102,7 +1117,7 @@ private int branch(NodeEx n1, Configuration conf) {
|
||||
private int join(NodeEx n2, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
flowOutOfCallNodeCand1(_, n, _, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1115,12 +1130,13 @@ private int join(NodeEx n2, Configuration conf) {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, ret, out, config) and
|
||||
flowOutOfCallNodeCand1(call, ret, pos, out, pragma[only_bind_into](config)) and
|
||||
exists(int b, int j |
|
||||
b = branch(ret, config) and
|
||||
j = join(out, config) and
|
||||
b = branch(ret, pragma[only_bind_into](config)) and
|
||||
j = join(out, pragma[only_bind_into](config)) and
|
||||
if b.minimum(j) <= config.fieldFlowBranchLimit()
|
||||
then allowsFieldFlow = true
|
||||
else allowsFieldFlow = false
|
||||
@@ -1156,7 +1172,9 @@ private signature module StageSig {
|
||||
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config);
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config);
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config);
|
||||
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config);
|
||||
|
||||
predicate storeStepCand(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, DataFlowType contentType,
|
||||
@@ -1222,7 +1240,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
);
|
||||
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
);
|
||||
|
||||
predicate flowIntoCall(
|
||||
@@ -1247,14 +1266,16 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughOutOfCall(
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, ReturnKindExt kind, NodeEx out,
|
||||
boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(_, ret.getEnclosingCallable(), _,
|
||||
pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
exists(ReturnPosition pos |
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
kind = pos.getKind() and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::returnMayFlowThrough(ret, pos, pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1262,29 +1283,32 @@ private module MkStage<StageSig PrevStage> {
|
||||
* configuration `config`.
|
||||
*
|
||||
* The call context `cc` records whether the node is reached through an
|
||||
* argument in a call, and if so, `argAp` records the access path of that
|
||||
* argument.
|
||||
* argument in a call, and if so, `summaryCtx` and `argAp` record the
|
||||
* corresponding parameter and access path of that argument, respectively.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate fwdFlow(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow0(node, state, cc, argAp, ap, config) and
|
||||
fwdFlow0(node, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::revFlow(node, state, unbindApa(getApprox(ap)), config) and
|
||||
filter(node, state, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlow0(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
sourceNode(node, state, config) and
|
||||
(if hasSourceCallCtx(config) then cc = ccSomeCall() else cc = ccNone()) and
|
||||
argAp = apNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
ap = getApNil(node)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
@@ -1295,65 +1319,72 @@ private module MkStage<StageSig PrevStage> {
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
jumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(mid, state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(mid, state0, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state0, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(mid, state0, node, state, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(TypedContent tc, Ap ap0 |
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, argAp, config) and
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, summaryCtx, argAp, config) and
|
||||
ap = apCons(tc, ap0)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Ap ap0, Content c |
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, argAp, config) and
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, summaryCtx, argAp, config) and
|
||||
fwdFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(ApApprox apa |
|
||||
fwdFlowIn(_, node, state, _, cc, _, ap, config) and
|
||||
fwdFlowIn(_, node, state, _, cc, _, _, ap, config) and
|
||||
apa = getApprox(ap) and
|
||||
if PrevStage::parameterMayFlowThrough(node, _, apa, config)
|
||||
then argAp = apSome(ap)
|
||||
else argAp = apNone()
|
||||
if PrevStage::parameterMayFlowThrough(node, apa, config)
|
||||
then (
|
||||
summaryCtx = TParamNodeSome(node.asNode()) and argAp = apSome(ap)
|
||||
) else (
|
||||
summaryCtx = TParamNodeNone() and argAp = apNone()
|
||||
)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
fwdFlowOutNotFromArg(node, state, cc, argAp, ap, config)
|
||||
fwdFlowOutNotFromArg(node, state, cc, summaryCtx, argAp, ap, config)
|
||||
or
|
||||
exists(DataFlowCall call, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ParamNode summaryCtx0, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, summaryCtx, argAp, summaryCtx0, argAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowStore(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
exists(DataFlowType contentType |
|
||||
fwdFlow(node1, state, cc, argAp, ap1, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, config) and
|
||||
PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
|
||||
typecheckStore(ap1, contentType)
|
||||
)
|
||||
@@ -1366,7 +1397,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
|
||||
exists(TypedContent tc |
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, config) and
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, _, config) and
|
||||
tc.getContent() = c and
|
||||
cons = apCons(tc, tail)
|
||||
)
|
||||
@@ -1374,21 +1405,21 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
fwdFlow(node1, state, cc, argAp, ap, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::readStepCand(node1, c, node2, config) and
|
||||
getHeadContent(ap) = c
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc, ApOption argAp,
|
||||
Ap ap, Configuration config
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow |
|
||||
fwdFlow(arg, state, outercc, argAp, ap, config) and
|
||||
fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, config) and
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1397,14 +1428,15 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutNotFromArg(
|
||||
NodeEx out, FlowState state, Cc ccOut, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx out, FlowState state, Cc ccOut, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(
|
||||
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
|
||||
DataFlowCallable inner
|
||||
|
|
||||
fwdFlow(ret, state, innercc, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, _, out, allowsFieldFlow, config) and
|
||||
inner = ret.getEnclosingCallable() and
|
||||
ccOut = getCallContextReturn(inner, call, innercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1413,12 +1445,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutFromArg(
|
||||
DataFlowCall call, NodeEx out, FlowState state, Ap argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, NodeEx out, FlowState state, ParamNode summaryCtx, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
exists(RetNodeEx ret, ReturnKindExt kind, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(summaryCtx), apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, kind, out, allowsFieldFlow, config) and
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(summaryCtx, kind)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1428,11 +1462,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIsEntered(
|
||||
DataFlowCall call, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, ParamNode p, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p |
|
||||
fwdFlowIn(call, p, _, cc, _, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
|
||||
exists(ParamNodeEx param |
|
||||
fwdFlowIn(call, param, _, cc, _, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(param, unbindApa(getApprox(ap)), config) and
|
||||
p = param.asNode()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1440,146 +1476,149 @@ private module MkStage<StageSig PrevStage> {
|
||||
private predicate storeStepFwd(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, config) and
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, _, config) and
|
||||
ap2 = apCons(tc, ap1) and
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, config)
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, _, config)
|
||||
}
|
||||
|
||||
private predicate readStepFwd(
|
||||
NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, config) and
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, _, config) and
|
||||
fwdFlowConsCand(ap1, c, ap2, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
|
||||
exists(Ap argAp0, NodeEx out, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(out, state, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlowOutFromArg(call, out, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
|
||||
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
|
||||
pragma[only_bind_into](config))
|
||||
)
|
||||
private predicate returnFlowsThrough(
|
||||
RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNode p, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(p), apSome(argAp), ap, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
parameterFlowThroughAllowed(p, pos.getKind())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughIntoCall(
|
||||
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
fwdFlow(arg, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, _, pragma[only_bind_into](config)) and
|
||||
callMayFlowThroughFwd(call, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate returnNodeMayFlowThrough(
|
||||
RetNodeEx ret, FlowState state, Ap ap, Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(_), ap, config)
|
||||
flowIntoCall(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), allowsFieldFlow,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
returnFlowsThrough(_, _, _, _, p.asNode(), _, _, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` with access path `ap` is part of a path from a source to a
|
||||
* sink in the configuration `config`.
|
||||
*
|
||||
* The Boolean `toReturn` records whether the node must be returned from the
|
||||
* enclosing callable in order to reach a sink, and if so, `returnAp` records
|
||||
* the access path of the returned value.
|
||||
* The parameter `returnCtx` records whether (and how) the node must be returned
|
||||
* from the enclosing callable in order to reach a sink, and if so, `returnAp`
|
||||
* records the access path of the returned value.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
revFlow0(node, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, ap, config)
|
||||
revFlow0(node, state, returnCtx, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlow0(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(node, state, _, _, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config) and
|
||||
sinkNode(node, state, config) and
|
||||
(if hasSinkCallCtx(config) then toReturn = true else toReturn = false) and
|
||||
(
|
||||
if hasSinkCallCtx(config)
|
||||
then returnCtx = TReturnCtxNoFlowThrough()
|
||||
else returnCtx = TReturnCtxNone()
|
||||
) and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
localStep(node, state, mid, state0, true, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, ap, config)
|
||||
revFlow(mid, state0, returnCtx, returnAp, ap, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
localStep(node, pragma[only_bind_into](state), mid, state0, false, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, state0, returnCtx, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
jumpStep(node, mid, config) and
|
||||
revFlow(mid, state, _, _, ap, config) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(node, mid, config) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(node, state, mid, state0, config) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, nil,
|
||||
pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Ap ap0, Content c |
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, toReturn, returnAp, config) and
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, returnCtx, returnAp, config) and
|
||||
revFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Ap ap0 |
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
readStepFwd(node, ap, _, mid, ap0, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
revFlowInNotToReturn(node, state, returnAp, ap, config) and
|
||||
toReturn = false
|
||||
returnCtx = TReturnCtxNone()
|
||||
or
|
||||
exists(DataFlowCall call, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ReturnPosition returnPos0, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
revFlowOut(_, node, state, _, _, ap, config) and
|
||||
toReturn = true and
|
||||
if returnNodeMayFlowThrough(node, state, ap, config)
|
||||
then returnAp = apSome(ap)
|
||||
else returnAp = apNone()
|
||||
exists(ReturnPosition pos |
|
||||
revFlowOut(_, node, pos, state, _, _, ap, config) and
|
||||
if returnFlowsThrough(node, pos, state, _, _, _, ap, config)
|
||||
then (
|
||||
returnCtx = TReturnCtxMaybeFlowThrough(pos) and
|
||||
returnAp = apSome(ap)
|
||||
) else (
|
||||
returnCtx = TReturnCtxNoFlowThrough() and returnAp = apNone()
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowStore(
|
||||
Ap ap0, Content c, Ap ap, NodeEx node, FlowState state, TypedContent tc, NodeEx mid,
|
||||
boolean toReturn, ApOption returnAp, Configuration config
|
||||
ReturnCtx returnCtx, ApOption returnAp, Configuration config
|
||||
) {
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
storeStepFwd(node, ap, tc, mid, ap0, config) and
|
||||
tc.getContent() = c
|
||||
}
|
||||
@@ -1599,12 +1638,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowOut(
|
||||
DataFlowCall call, RetNodeEx ret, FlowState state, boolean toReturn, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state, ReturnCtx returnCtx,
|
||||
ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(NodeEx out, boolean allowsFieldFlow |
|
||||
revFlow(out, state, toReturn, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
revFlow(out, state, returnCtx, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
}
|
||||
@@ -1614,7 +1653,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
ArgNodeEx arg, FlowState state, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, false, returnAp, ap, config) and
|
||||
revFlow(p, state, TReturnCtxNone(), returnAp, ap, config) and
|
||||
flowIntoCall(_, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
@@ -1622,12 +1661,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowInToReturn(
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, Ap returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnPosition returnPos, Ap returnAp,
|
||||
Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, true, apSome(returnAp), ap, config) and
|
||||
revFlow(p, state, TReturnCtxMaybeFlowThrough(returnPos), apSome(returnAp), ap, config) and
|
||||
flowThroughIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1638,11 +1679,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReturned(
|
||||
DataFlowCall call, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ReturnCtx returnCtx, ApOption returnAp, ReturnPosition pos, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, FlowState state, CcCall ccc |
|
||||
revFlowOut(call, ret, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(ret, state, ccc, apSome(_), ap, config) and
|
||||
revFlowOut(call, ret, pos, state, returnCtx, returnAp, ap, config) and
|
||||
returnFlowsThrough(ret, pos, state, ccc, _, _, ap, config) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
@@ -1713,40 +1755,39 @@ private module MkStage<StageSig PrevStage> {
|
||||
validAp(ap, config)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate parameterFlow(
|
||||
ParamNodeEx p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
|
||||
pragma[nomagic]
|
||||
private predicate parameterFlowsThroughRev(
|
||||
ParamNodeEx p, Ap ap, ReturnPosition returnPos, Configuration config
|
||||
) {
|
||||
revFlow(p, _, true, apSome(ap0), ap, config) and
|
||||
c = p.getEnclosingCallable()
|
||||
revFlow(p, _, TReturnCtxMaybeFlowThrough(returnPos), apSome(_), ap, config) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
}
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, FlowState state, Ap ap0, ReturnKindExt kind, ParameterPosition pos |
|
||||
parameterFlow(p, ap, ap0, c, config) and
|
||||
c = ret.getEnclosingCallable() and
|
||||
revFlow(pragma[only_bind_into](ret), pragma[only_bind_into](state), true, apSome(_),
|
||||
pragma[only_bind_into](ap0), pragma[only_bind_into](config)) and
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(ap), ap0, config) and
|
||||
kind = ret.getKind() and
|
||||
p.getPosition() = pos and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, ReturnPosition pos |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
exists(ParamNodeEx p, Ap ap |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(
|
||||
Ap returnAp0, ArgNodeEx arg, FlowState state, boolean toReturn, ApOption returnAp, Ap ap
|
||||
ReturnPosition returnPos0, Ap returnAp0, ArgNodeEx arg, FlowState state,
|
||||
ReturnCtx returnCtx, ApOption returnAp, Ap ap
|
||||
|
|
||||
revFlow(arg, state, toReturn, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
revFlow(arg, state, returnCtx, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1754,13 +1795,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, Configuration config
|
||||
) {
|
||||
fwd = true and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, config)) and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, config)) and
|
||||
fields = count(TypedContent f0 | fwdConsCand(f0, _, config)) and
|
||||
conscand = count(TypedContent f0, Ap ap | fwdConsCand(f0, ap, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, argAp, ap, config)
|
||||
count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, summaryCtx, argAp, ap, config)
|
||||
)
|
||||
or
|
||||
fwd = false and
|
||||
@@ -1769,8 +1810,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
conscand = count(TypedContent f0, Ap ap | consCand(f0, ap, config)) and
|
||||
states = count(FlowState state | revFlow(_, state, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, boolean b, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, b, retAp, ap, config)
|
||||
count(NodeEx n, FlowState state, ReturnCtx returnCtx, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, returnCtx, retAp, ap, config)
|
||||
)
|
||||
}
|
||||
/* End: Stage logic. */
|
||||
@@ -1915,7 +1956,7 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
|
||||
exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand1/5;
|
||||
|
||||
@@ -1951,9 +1992,10 @@ private module Stage2 implements StageSig {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand2(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand1(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
Stage2::revFlow(node2, pragma[only_bind_into](config)) and
|
||||
Stage2::revFlowAlias(node1, pragma[only_bind_into](config))
|
||||
}
|
||||
@@ -2021,8 +2063,8 @@ private module LocalFlowBigStep {
|
||||
exists(NodeEx next | Stage2::revFlow(next, state, config) |
|
||||
jumpStep(node, next, config) or
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
flowIntoCallNodeCand2(_, node, next, _, config) or
|
||||
flowOutOfCallNodeCand2(_, node, _, next, _, config) or
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
@@ -2163,7 +2205,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
|
||||
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap, config, _) and exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
@@ -2233,8 +2275,9 @@ private predicate flowCandSummaryCtx(
|
||||
NodeEx node, FlowState state, AccessPathFront argApf, Configuration config
|
||||
) {
|
||||
exists(AccessPathFront apf |
|
||||
Stage3::revFlow(node, state, true, _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), TAccessPathFrontSome(argApf), apf, config)
|
||||
Stage3::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), _, TAccessPathFrontSome(argApf), apf,
|
||||
config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2468,10 +2511,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
exists(FlowState state |
|
||||
flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand2(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
|
||||
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
|
||||
pragma[only_bind_into](config))
|
||||
@@ -2508,13 +2552,13 @@ private Configuration unbindConf(Configuration conf) {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeMayUseSummary0(
|
||||
NodeEx n, DataFlowCallable c, FlowState state, AccessPathApprox apa, Configuration config
|
||||
NodeEx n, ParamNodeEx p, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(AccessPathApprox apa0 |
|
||||
Stage4::parameterMayFlowThrough(_, c, _, _) and
|
||||
Stage4::revFlow(n, state, true, _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
|
||||
n.getEnclosingCallable() = c
|
||||
Stage4::parameterMayFlowThrough(p, _, _) and
|
||||
Stage4::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()),
|
||||
TAccessPathApproxSome(apa), apa0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2522,9 +2566,9 @@ pragma[nomagic]
|
||||
private predicate nodeMayUseSummary(
|
||||
NodeEx n, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(DataFlowCallable c |
|
||||
Stage4::parameterMayFlowThrough(_, c, apa, config) and
|
||||
nodeMayUseSummary0(n, c, state, apa, config)
|
||||
exists(ParamNodeEx p |
|
||||
Stage4::parameterMayFlowThrough(p, apa, config) and
|
||||
nodeMayUseSummary0(n, p, state, apa, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2532,7 +2576,7 @@ private newtype TSummaryCtx =
|
||||
TSummaryCtxNone() or
|
||||
TSummaryCtxSome(ParamNodeEx p, FlowState state, AccessPath ap) {
|
||||
exists(Configuration config |
|
||||
Stage4::parameterMayFlowThrough(p, _, ap.getApprox(), config) and
|
||||
Stage4::parameterMayFlowThrough(p, ap.getApprox(), config) and
|
||||
Stage4::revFlow(p, state, _, config)
|
||||
)
|
||||
}
|
||||
@@ -3453,17 +3497,11 @@ private predicate paramFlowsThrough(
|
||||
ReturnKindExt kind, FlowState state, CallContextCall cc, SummaryCtxSome sc, AccessPath ap,
|
||||
AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(PathNodeMid mid, RetNodeEx ret, ParameterPosition pos |
|
||||
exists(PathNodeMid mid, RetNodeEx ret |
|
||||
pathNode(mid, ret, state, cc, sc, ap, config, _) and
|
||||
kind = ret.getKind() and
|
||||
apa = ap.getApprox() and
|
||||
pos = sc.getParameterPos() and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
sc.getParamNode().allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(sc.getParamNode().asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -319,8 +319,6 @@ private class ParamNodeEx extends NodeEx {
|
||||
}
|
||||
|
||||
ParameterPosition getPosition() { this.isParameterOf(_, result) }
|
||||
|
||||
predicate allowParameterReturnInSelf() { allowParameterReturnInSelfCached(this.asNode()) }
|
||||
}
|
||||
|
||||
private class RetNodeEx extends NodeEx {
|
||||
@@ -608,6 +606,21 @@ private predicate hasSinkCallCtx(Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if flow from `p` to a return node of kind `kind` is allowed.
|
||||
*
|
||||
* We don't expect a parameter to return stored in itself, unless
|
||||
* explicitly allowed
|
||||
*/
|
||||
bindingset[p, kind]
|
||||
private predicate parameterFlowThroughAllowed(ParamNode p, ReturnKindExt kind) {
|
||||
exists(ParameterPosition pos | p.isParameterOf(_, pos) |
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
allowParameterReturnInSelfCached(p)
|
||||
)
|
||||
}
|
||||
|
||||
private module Stage1 implements StageSig {
|
||||
class Ap = Unit;
|
||||
|
||||
@@ -981,21 +994,22 @@ private module Stage1 implements StageSig {
|
||||
* candidate for the origin of a summary.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(ReturnKindExt kind |
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(DataFlowCallable c, ReturnKindExt kind |
|
||||
throughFlowNodeCand(p, config) and
|
||||
returnFlowCallableNodeCand(c, kind, config) and
|
||||
p.getEnclosingCallable() = c and
|
||||
exists(ap) and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(p.asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
throughFlowNodeCand(ret, config) and
|
||||
pos = ret.getReturnPosition()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(ArgNodeEx arg, boolean toReturn |
|
||||
@@ -1052,9 +1066,10 @@ private predicate viableReturnPosOutNodeCand1(
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Configuration config
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
viableReturnPosOutNodeCand1(call, pos, out, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
@@ -1090,7 +1105,7 @@ private predicate flowIntoCallNodeCand1(
|
||||
private int branch(NodeEx n1, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n1, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
flowOutOfCallNodeCand1(_, n1, _, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1102,7 +1117,7 @@ private int branch(NodeEx n1, Configuration conf) {
|
||||
private int join(NodeEx n2, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
flowOutOfCallNodeCand1(_, n, _, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1115,12 +1130,13 @@ private int join(NodeEx n2, Configuration conf) {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, ret, out, config) and
|
||||
flowOutOfCallNodeCand1(call, ret, pos, out, pragma[only_bind_into](config)) and
|
||||
exists(int b, int j |
|
||||
b = branch(ret, config) and
|
||||
j = join(out, config) and
|
||||
b = branch(ret, pragma[only_bind_into](config)) and
|
||||
j = join(out, pragma[only_bind_into](config)) and
|
||||
if b.minimum(j) <= config.fieldFlowBranchLimit()
|
||||
then allowsFieldFlow = true
|
||||
else allowsFieldFlow = false
|
||||
@@ -1156,7 +1172,9 @@ private signature module StageSig {
|
||||
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config);
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config);
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config);
|
||||
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config);
|
||||
|
||||
predicate storeStepCand(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, DataFlowType contentType,
|
||||
@@ -1222,7 +1240,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
);
|
||||
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
);
|
||||
|
||||
predicate flowIntoCall(
|
||||
@@ -1247,14 +1266,16 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughOutOfCall(
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, ReturnKindExt kind, NodeEx out,
|
||||
boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(_, ret.getEnclosingCallable(), _,
|
||||
pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
exists(ReturnPosition pos |
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
kind = pos.getKind() and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::returnMayFlowThrough(ret, pos, pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1262,29 +1283,32 @@ private module MkStage<StageSig PrevStage> {
|
||||
* configuration `config`.
|
||||
*
|
||||
* The call context `cc` records whether the node is reached through an
|
||||
* argument in a call, and if so, `argAp` records the access path of that
|
||||
* argument.
|
||||
* argument in a call, and if so, `summaryCtx` and `argAp` record the
|
||||
* corresponding parameter and access path of that argument, respectively.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate fwdFlow(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow0(node, state, cc, argAp, ap, config) and
|
||||
fwdFlow0(node, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::revFlow(node, state, unbindApa(getApprox(ap)), config) and
|
||||
filter(node, state, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlow0(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
sourceNode(node, state, config) and
|
||||
(if hasSourceCallCtx(config) then cc = ccSomeCall() else cc = ccNone()) and
|
||||
argAp = apNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
ap = getApNil(node)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
@@ -1295,65 +1319,72 @@ private module MkStage<StageSig PrevStage> {
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
jumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(mid, state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(mid, state0, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state0, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(mid, state0, node, state, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(TypedContent tc, Ap ap0 |
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, argAp, config) and
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, summaryCtx, argAp, config) and
|
||||
ap = apCons(tc, ap0)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Ap ap0, Content c |
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, argAp, config) and
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, summaryCtx, argAp, config) and
|
||||
fwdFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(ApApprox apa |
|
||||
fwdFlowIn(_, node, state, _, cc, _, ap, config) and
|
||||
fwdFlowIn(_, node, state, _, cc, _, _, ap, config) and
|
||||
apa = getApprox(ap) and
|
||||
if PrevStage::parameterMayFlowThrough(node, _, apa, config)
|
||||
then argAp = apSome(ap)
|
||||
else argAp = apNone()
|
||||
if PrevStage::parameterMayFlowThrough(node, apa, config)
|
||||
then (
|
||||
summaryCtx = TParamNodeSome(node.asNode()) and argAp = apSome(ap)
|
||||
) else (
|
||||
summaryCtx = TParamNodeNone() and argAp = apNone()
|
||||
)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
fwdFlowOutNotFromArg(node, state, cc, argAp, ap, config)
|
||||
fwdFlowOutNotFromArg(node, state, cc, summaryCtx, argAp, ap, config)
|
||||
or
|
||||
exists(DataFlowCall call, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ParamNode summaryCtx0, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, summaryCtx, argAp, summaryCtx0, argAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowStore(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
exists(DataFlowType contentType |
|
||||
fwdFlow(node1, state, cc, argAp, ap1, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, config) and
|
||||
PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
|
||||
typecheckStore(ap1, contentType)
|
||||
)
|
||||
@@ -1366,7 +1397,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
|
||||
exists(TypedContent tc |
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, config) and
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, _, config) and
|
||||
tc.getContent() = c and
|
||||
cons = apCons(tc, tail)
|
||||
)
|
||||
@@ -1374,21 +1405,21 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
fwdFlow(node1, state, cc, argAp, ap, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::readStepCand(node1, c, node2, config) and
|
||||
getHeadContent(ap) = c
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc, ApOption argAp,
|
||||
Ap ap, Configuration config
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow |
|
||||
fwdFlow(arg, state, outercc, argAp, ap, config) and
|
||||
fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, config) and
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1397,14 +1428,15 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutNotFromArg(
|
||||
NodeEx out, FlowState state, Cc ccOut, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx out, FlowState state, Cc ccOut, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(
|
||||
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
|
||||
DataFlowCallable inner
|
||||
|
|
||||
fwdFlow(ret, state, innercc, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, _, out, allowsFieldFlow, config) and
|
||||
inner = ret.getEnclosingCallable() and
|
||||
ccOut = getCallContextReturn(inner, call, innercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1413,12 +1445,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutFromArg(
|
||||
DataFlowCall call, NodeEx out, FlowState state, Ap argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, NodeEx out, FlowState state, ParamNode summaryCtx, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
exists(RetNodeEx ret, ReturnKindExt kind, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(summaryCtx), apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, kind, out, allowsFieldFlow, config) and
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(summaryCtx, kind)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1428,11 +1462,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIsEntered(
|
||||
DataFlowCall call, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, ParamNode p, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p |
|
||||
fwdFlowIn(call, p, _, cc, _, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
|
||||
exists(ParamNodeEx param |
|
||||
fwdFlowIn(call, param, _, cc, _, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(param, unbindApa(getApprox(ap)), config) and
|
||||
p = param.asNode()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1440,146 +1476,149 @@ private module MkStage<StageSig PrevStage> {
|
||||
private predicate storeStepFwd(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, config) and
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, _, config) and
|
||||
ap2 = apCons(tc, ap1) and
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, config)
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, _, config)
|
||||
}
|
||||
|
||||
private predicate readStepFwd(
|
||||
NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, config) and
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, _, config) and
|
||||
fwdFlowConsCand(ap1, c, ap2, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
|
||||
exists(Ap argAp0, NodeEx out, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(out, state, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlowOutFromArg(call, out, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
|
||||
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
|
||||
pragma[only_bind_into](config))
|
||||
)
|
||||
private predicate returnFlowsThrough(
|
||||
RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNode p, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(p), apSome(argAp), ap, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
parameterFlowThroughAllowed(p, pos.getKind())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughIntoCall(
|
||||
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
fwdFlow(arg, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, _, pragma[only_bind_into](config)) and
|
||||
callMayFlowThroughFwd(call, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate returnNodeMayFlowThrough(
|
||||
RetNodeEx ret, FlowState state, Ap ap, Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(_), ap, config)
|
||||
flowIntoCall(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), allowsFieldFlow,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
returnFlowsThrough(_, _, _, _, p.asNode(), _, _, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` with access path `ap` is part of a path from a source to a
|
||||
* sink in the configuration `config`.
|
||||
*
|
||||
* The Boolean `toReturn` records whether the node must be returned from the
|
||||
* enclosing callable in order to reach a sink, and if so, `returnAp` records
|
||||
* the access path of the returned value.
|
||||
* The parameter `returnCtx` records whether (and how) the node must be returned
|
||||
* from the enclosing callable in order to reach a sink, and if so, `returnAp`
|
||||
* records the access path of the returned value.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
revFlow0(node, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, ap, config)
|
||||
revFlow0(node, state, returnCtx, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlow0(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(node, state, _, _, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config) and
|
||||
sinkNode(node, state, config) and
|
||||
(if hasSinkCallCtx(config) then toReturn = true else toReturn = false) and
|
||||
(
|
||||
if hasSinkCallCtx(config)
|
||||
then returnCtx = TReturnCtxNoFlowThrough()
|
||||
else returnCtx = TReturnCtxNone()
|
||||
) and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
localStep(node, state, mid, state0, true, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, ap, config)
|
||||
revFlow(mid, state0, returnCtx, returnAp, ap, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
localStep(node, pragma[only_bind_into](state), mid, state0, false, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, state0, returnCtx, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
jumpStep(node, mid, config) and
|
||||
revFlow(mid, state, _, _, ap, config) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(node, mid, config) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(node, state, mid, state0, config) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, nil,
|
||||
pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Ap ap0, Content c |
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, toReturn, returnAp, config) and
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, returnCtx, returnAp, config) and
|
||||
revFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Ap ap0 |
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
readStepFwd(node, ap, _, mid, ap0, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
revFlowInNotToReturn(node, state, returnAp, ap, config) and
|
||||
toReturn = false
|
||||
returnCtx = TReturnCtxNone()
|
||||
or
|
||||
exists(DataFlowCall call, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ReturnPosition returnPos0, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
revFlowOut(_, node, state, _, _, ap, config) and
|
||||
toReturn = true and
|
||||
if returnNodeMayFlowThrough(node, state, ap, config)
|
||||
then returnAp = apSome(ap)
|
||||
else returnAp = apNone()
|
||||
exists(ReturnPosition pos |
|
||||
revFlowOut(_, node, pos, state, _, _, ap, config) and
|
||||
if returnFlowsThrough(node, pos, state, _, _, _, ap, config)
|
||||
then (
|
||||
returnCtx = TReturnCtxMaybeFlowThrough(pos) and
|
||||
returnAp = apSome(ap)
|
||||
) else (
|
||||
returnCtx = TReturnCtxNoFlowThrough() and returnAp = apNone()
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowStore(
|
||||
Ap ap0, Content c, Ap ap, NodeEx node, FlowState state, TypedContent tc, NodeEx mid,
|
||||
boolean toReturn, ApOption returnAp, Configuration config
|
||||
ReturnCtx returnCtx, ApOption returnAp, Configuration config
|
||||
) {
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
storeStepFwd(node, ap, tc, mid, ap0, config) and
|
||||
tc.getContent() = c
|
||||
}
|
||||
@@ -1599,12 +1638,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowOut(
|
||||
DataFlowCall call, RetNodeEx ret, FlowState state, boolean toReturn, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state, ReturnCtx returnCtx,
|
||||
ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(NodeEx out, boolean allowsFieldFlow |
|
||||
revFlow(out, state, toReturn, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
revFlow(out, state, returnCtx, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
}
|
||||
@@ -1614,7 +1653,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
ArgNodeEx arg, FlowState state, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, false, returnAp, ap, config) and
|
||||
revFlow(p, state, TReturnCtxNone(), returnAp, ap, config) and
|
||||
flowIntoCall(_, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
@@ -1622,12 +1661,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowInToReturn(
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, Ap returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnPosition returnPos, Ap returnAp,
|
||||
Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, true, apSome(returnAp), ap, config) and
|
||||
revFlow(p, state, TReturnCtxMaybeFlowThrough(returnPos), apSome(returnAp), ap, config) and
|
||||
flowThroughIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1638,11 +1679,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReturned(
|
||||
DataFlowCall call, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ReturnCtx returnCtx, ApOption returnAp, ReturnPosition pos, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, FlowState state, CcCall ccc |
|
||||
revFlowOut(call, ret, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(ret, state, ccc, apSome(_), ap, config) and
|
||||
revFlowOut(call, ret, pos, state, returnCtx, returnAp, ap, config) and
|
||||
returnFlowsThrough(ret, pos, state, ccc, _, _, ap, config) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
@@ -1713,40 +1755,39 @@ private module MkStage<StageSig PrevStage> {
|
||||
validAp(ap, config)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate parameterFlow(
|
||||
ParamNodeEx p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
|
||||
pragma[nomagic]
|
||||
private predicate parameterFlowsThroughRev(
|
||||
ParamNodeEx p, Ap ap, ReturnPosition returnPos, Configuration config
|
||||
) {
|
||||
revFlow(p, _, true, apSome(ap0), ap, config) and
|
||||
c = p.getEnclosingCallable()
|
||||
revFlow(p, _, TReturnCtxMaybeFlowThrough(returnPos), apSome(_), ap, config) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
}
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, FlowState state, Ap ap0, ReturnKindExt kind, ParameterPosition pos |
|
||||
parameterFlow(p, ap, ap0, c, config) and
|
||||
c = ret.getEnclosingCallable() and
|
||||
revFlow(pragma[only_bind_into](ret), pragma[only_bind_into](state), true, apSome(_),
|
||||
pragma[only_bind_into](ap0), pragma[only_bind_into](config)) and
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(ap), ap0, config) and
|
||||
kind = ret.getKind() and
|
||||
p.getPosition() = pos and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, ReturnPosition pos |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
exists(ParamNodeEx p, Ap ap |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(
|
||||
Ap returnAp0, ArgNodeEx arg, FlowState state, boolean toReturn, ApOption returnAp, Ap ap
|
||||
ReturnPosition returnPos0, Ap returnAp0, ArgNodeEx arg, FlowState state,
|
||||
ReturnCtx returnCtx, ApOption returnAp, Ap ap
|
||||
|
|
||||
revFlow(arg, state, toReturn, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
revFlow(arg, state, returnCtx, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1754,13 +1795,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, Configuration config
|
||||
) {
|
||||
fwd = true and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, config)) and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, config)) and
|
||||
fields = count(TypedContent f0 | fwdConsCand(f0, _, config)) and
|
||||
conscand = count(TypedContent f0, Ap ap | fwdConsCand(f0, ap, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, argAp, ap, config)
|
||||
count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, summaryCtx, argAp, ap, config)
|
||||
)
|
||||
or
|
||||
fwd = false and
|
||||
@@ -1769,8 +1810,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
conscand = count(TypedContent f0, Ap ap | consCand(f0, ap, config)) and
|
||||
states = count(FlowState state | revFlow(_, state, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, boolean b, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, b, retAp, ap, config)
|
||||
count(NodeEx n, FlowState state, ReturnCtx returnCtx, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, returnCtx, retAp, ap, config)
|
||||
)
|
||||
}
|
||||
/* End: Stage logic. */
|
||||
@@ -1915,7 +1956,7 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
|
||||
exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand1/5;
|
||||
|
||||
@@ -1951,9 +1992,10 @@ private module Stage2 implements StageSig {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand2(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand1(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
Stage2::revFlow(node2, pragma[only_bind_into](config)) and
|
||||
Stage2::revFlowAlias(node1, pragma[only_bind_into](config))
|
||||
}
|
||||
@@ -2021,8 +2063,8 @@ private module LocalFlowBigStep {
|
||||
exists(NodeEx next | Stage2::revFlow(next, state, config) |
|
||||
jumpStep(node, next, config) or
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
flowIntoCallNodeCand2(_, node, next, _, config) or
|
||||
flowOutOfCallNodeCand2(_, node, _, next, _, config) or
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
@@ -2163,7 +2205,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
|
||||
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap, config, _) and exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
@@ -2233,8 +2275,9 @@ private predicate flowCandSummaryCtx(
|
||||
NodeEx node, FlowState state, AccessPathFront argApf, Configuration config
|
||||
) {
|
||||
exists(AccessPathFront apf |
|
||||
Stage3::revFlow(node, state, true, _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), TAccessPathFrontSome(argApf), apf, config)
|
||||
Stage3::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), _, TAccessPathFrontSome(argApf), apf,
|
||||
config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2468,10 +2511,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
exists(FlowState state |
|
||||
flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand2(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
|
||||
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
|
||||
pragma[only_bind_into](config))
|
||||
@@ -2508,13 +2552,13 @@ private Configuration unbindConf(Configuration conf) {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeMayUseSummary0(
|
||||
NodeEx n, DataFlowCallable c, FlowState state, AccessPathApprox apa, Configuration config
|
||||
NodeEx n, ParamNodeEx p, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(AccessPathApprox apa0 |
|
||||
Stage4::parameterMayFlowThrough(_, c, _, _) and
|
||||
Stage4::revFlow(n, state, true, _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
|
||||
n.getEnclosingCallable() = c
|
||||
Stage4::parameterMayFlowThrough(p, _, _) and
|
||||
Stage4::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()),
|
||||
TAccessPathApproxSome(apa), apa0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2522,9 +2566,9 @@ pragma[nomagic]
|
||||
private predicate nodeMayUseSummary(
|
||||
NodeEx n, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(DataFlowCallable c |
|
||||
Stage4::parameterMayFlowThrough(_, c, apa, config) and
|
||||
nodeMayUseSummary0(n, c, state, apa, config)
|
||||
exists(ParamNodeEx p |
|
||||
Stage4::parameterMayFlowThrough(p, apa, config) and
|
||||
nodeMayUseSummary0(n, p, state, apa, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2532,7 +2576,7 @@ private newtype TSummaryCtx =
|
||||
TSummaryCtxNone() or
|
||||
TSummaryCtxSome(ParamNodeEx p, FlowState state, AccessPath ap) {
|
||||
exists(Configuration config |
|
||||
Stage4::parameterMayFlowThrough(p, _, ap.getApprox(), config) and
|
||||
Stage4::parameterMayFlowThrough(p, ap.getApprox(), config) and
|
||||
Stage4::revFlow(p, state, _, config)
|
||||
)
|
||||
}
|
||||
@@ -3453,17 +3497,11 @@ private predicate paramFlowsThrough(
|
||||
ReturnKindExt kind, FlowState state, CallContextCall cc, SummaryCtxSome sc, AccessPath ap,
|
||||
AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(PathNodeMid mid, RetNodeEx ret, ParameterPosition pos |
|
||||
exists(PathNodeMid mid, RetNodeEx ret |
|
||||
pathNode(mid, ret, state, cc, sc, ap, config, _) and
|
||||
kind = ret.getKind() and
|
||||
apa = ap.getApprox() and
|
||||
pos = sc.getParameterPos() and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
sc.getParamNode().allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(sc.getParamNode().asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -319,8 +319,6 @@ private class ParamNodeEx extends NodeEx {
|
||||
}
|
||||
|
||||
ParameterPosition getPosition() { this.isParameterOf(_, result) }
|
||||
|
||||
predicate allowParameterReturnInSelf() { allowParameterReturnInSelfCached(this.asNode()) }
|
||||
}
|
||||
|
||||
private class RetNodeEx extends NodeEx {
|
||||
@@ -608,6 +606,21 @@ private predicate hasSinkCallCtx(Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if flow from `p` to a return node of kind `kind` is allowed.
|
||||
*
|
||||
* We don't expect a parameter to return stored in itself, unless
|
||||
* explicitly allowed
|
||||
*/
|
||||
bindingset[p, kind]
|
||||
private predicate parameterFlowThroughAllowed(ParamNode p, ReturnKindExt kind) {
|
||||
exists(ParameterPosition pos | p.isParameterOf(_, pos) |
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
allowParameterReturnInSelfCached(p)
|
||||
)
|
||||
}
|
||||
|
||||
private module Stage1 implements StageSig {
|
||||
class Ap = Unit;
|
||||
|
||||
@@ -981,21 +994,22 @@ private module Stage1 implements StageSig {
|
||||
* candidate for the origin of a summary.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(ReturnKindExt kind |
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(DataFlowCallable c, ReturnKindExt kind |
|
||||
throughFlowNodeCand(p, config) and
|
||||
returnFlowCallableNodeCand(c, kind, config) and
|
||||
p.getEnclosingCallable() = c and
|
||||
exists(ap) and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(p.asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
throughFlowNodeCand(ret, config) and
|
||||
pos = ret.getReturnPosition()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(ArgNodeEx arg, boolean toReturn |
|
||||
@@ -1052,9 +1066,10 @@ private predicate viableReturnPosOutNodeCand1(
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Configuration config
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
viableReturnPosOutNodeCand1(call, pos, out, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
@@ -1090,7 +1105,7 @@ private predicate flowIntoCallNodeCand1(
|
||||
private int branch(NodeEx n1, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n1, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
flowOutOfCallNodeCand1(_, n1, _, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1102,7 +1117,7 @@ private int branch(NodeEx n1, Configuration conf) {
|
||||
private int join(NodeEx n2, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
flowOutOfCallNodeCand1(_, n, _, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1115,12 +1130,13 @@ private int join(NodeEx n2, Configuration conf) {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, ret, out, config) and
|
||||
flowOutOfCallNodeCand1(call, ret, pos, out, pragma[only_bind_into](config)) and
|
||||
exists(int b, int j |
|
||||
b = branch(ret, config) and
|
||||
j = join(out, config) and
|
||||
b = branch(ret, pragma[only_bind_into](config)) and
|
||||
j = join(out, pragma[only_bind_into](config)) and
|
||||
if b.minimum(j) <= config.fieldFlowBranchLimit()
|
||||
then allowsFieldFlow = true
|
||||
else allowsFieldFlow = false
|
||||
@@ -1156,7 +1172,9 @@ private signature module StageSig {
|
||||
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config);
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config);
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config);
|
||||
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config);
|
||||
|
||||
predicate storeStepCand(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, DataFlowType contentType,
|
||||
@@ -1222,7 +1240,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
);
|
||||
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
);
|
||||
|
||||
predicate flowIntoCall(
|
||||
@@ -1247,14 +1266,16 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughOutOfCall(
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, ReturnKindExt kind, NodeEx out,
|
||||
boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(_, ret.getEnclosingCallable(), _,
|
||||
pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
exists(ReturnPosition pos |
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
kind = pos.getKind() and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::returnMayFlowThrough(ret, pos, pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1262,29 +1283,32 @@ private module MkStage<StageSig PrevStage> {
|
||||
* configuration `config`.
|
||||
*
|
||||
* The call context `cc` records whether the node is reached through an
|
||||
* argument in a call, and if so, `argAp` records the access path of that
|
||||
* argument.
|
||||
* argument in a call, and if so, `summaryCtx` and `argAp` record the
|
||||
* corresponding parameter and access path of that argument, respectively.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate fwdFlow(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow0(node, state, cc, argAp, ap, config) and
|
||||
fwdFlow0(node, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::revFlow(node, state, unbindApa(getApprox(ap)), config) and
|
||||
filter(node, state, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlow0(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
sourceNode(node, state, config) and
|
||||
(if hasSourceCallCtx(config) then cc = ccSomeCall() else cc = ccNone()) and
|
||||
argAp = apNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
ap = getApNil(node)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
@@ -1295,65 +1319,72 @@ private module MkStage<StageSig PrevStage> {
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
jumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(mid, state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(mid, state0, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state0, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(mid, state0, node, state, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(TypedContent tc, Ap ap0 |
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, argAp, config) and
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, summaryCtx, argAp, config) and
|
||||
ap = apCons(tc, ap0)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Ap ap0, Content c |
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, argAp, config) and
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, summaryCtx, argAp, config) and
|
||||
fwdFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(ApApprox apa |
|
||||
fwdFlowIn(_, node, state, _, cc, _, ap, config) and
|
||||
fwdFlowIn(_, node, state, _, cc, _, _, ap, config) and
|
||||
apa = getApprox(ap) and
|
||||
if PrevStage::parameterMayFlowThrough(node, _, apa, config)
|
||||
then argAp = apSome(ap)
|
||||
else argAp = apNone()
|
||||
if PrevStage::parameterMayFlowThrough(node, apa, config)
|
||||
then (
|
||||
summaryCtx = TParamNodeSome(node.asNode()) and argAp = apSome(ap)
|
||||
) else (
|
||||
summaryCtx = TParamNodeNone() and argAp = apNone()
|
||||
)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
fwdFlowOutNotFromArg(node, state, cc, argAp, ap, config)
|
||||
fwdFlowOutNotFromArg(node, state, cc, summaryCtx, argAp, ap, config)
|
||||
or
|
||||
exists(DataFlowCall call, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ParamNode summaryCtx0, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, summaryCtx, argAp, summaryCtx0, argAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowStore(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
exists(DataFlowType contentType |
|
||||
fwdFlow(node1, state, cc, argAp, ap1, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, config) and
|
||||
PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
|
||||
typecheckStore(ap1, contentType)
|
||||
)
|
||||
@@ -1366,7 +1397,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
|
||||
exists(TypedContent tc |
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, config) and
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, _, config) and
|
||||
tc.getContent() = c and
|
||||
cons = apCons(tc, tail)
|
||||
)
|
||||
@@ -1374,21 +1405,21 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
fwdFlow(node1, state, cc, argAp, ap, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::readStepCand(node1, c, node2, config) and
|
||||
getHeadContent(ap) = c
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc, ApOption argAp,
|
||||
Ap ap, Configuration config
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow |
|
||||
fwdFlow(arg, state, outercc, argAp, ap, config) and
|
||||
fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, config) and
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1397,14 +1428,15 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutNotFromArg(
|
||||
NodeEx out, FlowState state, Cc ccOut, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx out, FlowState state, Cc ccOut, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(
|
||||
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
|
||||
DataFlowCallable inner
|
||||
|
|
||||
fwdFlow(ret, state, innercc, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, _, out, allowsFieldFlow, config) and
|
||||
inner = ret.getEnclosingCallable() and
|
||||
ccOut = getCallContextReturn(inner, call, innercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1413,12 +1445,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutFromArg(
|
||||
DataFlowCall call, NodeEx out, FlowState state, Ap argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, NodeEx out, FlowState state, ParamNode summaryCtx, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
exists(RetNodeEx ret, ReturnKindExt kind, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(summaryCtx), apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, kind, out, allowsFieldFlow, config) and
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(summaryCtx, kind)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1428,11 +1462,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIsEntered(
|
||||
DataFlowCall call, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, ParamNode p, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p |
|
||||
fwdFlowIn(call, p, _, cc, _, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
|
||||
exists(ParamNodeEx param |
|
||||
fwdFlowIn(call, param, _, cc, _, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(param, unbindApa(getApprox(ap)), config) and
|
||||
p = param.asNode()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1440,146 +1476,149 @@ private module MkStage<StageSig PrevStage> {
|
||||
private predicate storeStepFwd(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, config) and
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, _, config) and
|
||||
ap2 = apCons(tc, ap1) and
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, config)
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, _, config)
|
||||
}
|
||||
|
||||
private predicate readStepFwd(
|
||||
NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, config) and
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, _, config) and
|
||||
fwdFlowConsCand(ap1, c, ap2, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
|
||||
exists(Ap argAp0, NodeEx out, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(out, state, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlowOutFromArg(call, out, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
|
||||
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
|
||||
pragma[only_bind_into](config))
|
||||
)
|
||||
private predicate returnFlowsThrough(
|
||||
RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNode p, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(p), apSome(argAp), ap, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
parameterFlowThroughAllowed(p, pos.getKind())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughIntoCall(
|
||||
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
fwdFlow(arg, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, _, pragma[only_bind_into](config)) and
|
||||
callMayFlowThroughFwd(call, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate returnNodeMayFlowThrough(
|
||||
RetNodeEx ret, FlowState state, Ap ap, Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(_), ap, config)
|
||||
flowIntoCall(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), allowsFieldFlow,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
returnFlowsThrough(_, _, _, _, p.asNode(), _, _, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` with access path `ap` is part of a path from a source to a
|
||||
* sink in the configuration `config`.
|
||||
*
|
||||
* The Boolean `toReturn` records whether the node must be returned from the
|
||||
* enclosing callable in order to reach a sink, and if so, `returnAp` records
|
||||
* the access path of the returned value.
|
||||
* The parameter `returnCtx` records whether (and how) the node must be returned
|
||||
* from the enclosing callable in order to reach a sink, and if so, `returnAp`
|
||||
* records the access path of the returned value.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
revFlow0(node, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, ap, config)
|
||||
revFlow0(node, state, returnCtx, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlow0(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(node, state, _, _, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config) and
|
||||
sinkNode(node, state, config) and
|
||||
(if hasSinkCallCtx(config) then toReturn = true else toReturn = false) and
|
||||
(
|
||||
if hasSinkCallCtx(config)
|
||||
then returnCtx = TReturnCtxNoFlowThrough()
|
||||
else returnCtx = TReturnCtxNone()
|
||||
) and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
localStep(node, state, mid, state0, true, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, ap, config)
|
||||
revFlow(mid, state0, returnCtx, returnAp, ap, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
localStep(node, pragma[only_bind_into](state), mid, state0, false, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, state0, returnCtx, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
jumpStep(node, mid, config) and
|
||||
revFlow(mid, state, _, _, ap, config) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(node, mid, config) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(node, state, mid, state0, config) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, nil,
|
||||
pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Ap ap0, Content c |
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, toReturn, returnAp, config) and
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, returnCtx, returnAp, config) and
|
||||
revFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Ap ap0 |
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
readStepFwd(node, ap, _, mid, ap0, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
revFlowInNotToReturn(node, state, returnAp, ap, config) and
|
||||
toReturn = false
|
||||
returnCtx = TReturnCtxNone()
|
||||
or
|
||||
exists(DataFlowCall call, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ReturnPosition returnPos0, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
revFlowOut(_, node, state, _, _, ap, config) and
|
||||
toReturn = true and
|
||||
if returnNodeMayFlowThrough(node, state, ap, config)
|
||||
then returnAp = apSome(ap)
|
||||
else returnAp = apNone()
|
||||
exists(ReturnPosition pos |
|
||||
revFlowOut(_, node, pos, state, _, _, ap, config) and
|
||||
if returnFlowsThrough(node, pos, state, _, _, _, ap, config)
|
||||
then (
|
||||
returnCtx = TReturnCtxMaybeFlowThrough(pos) and
|
||||
returnAp = apSome(ap)
|
||||
) else (
|
||||
returnCtx = TReturnCtxNoFlowThrough() and returnAp = apNone()
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowStore(
|
||||
Ap ap0, Content c, Ap ap, NodeEx node, FlowState state, TypedContent tc, NodeEx mid,
|
||||
boolean toReturn, ApOption returnAp, Configuration config
|
||||
ReturnCtx returnCtx, ApOption returnAp, Configuration config
|
||||
) {
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
storeStepFwd(node, ap, tc, mid, ap0, config) and
|
||||
tc.getContent() = c
|
||||
}
|
||||
@@ -1599,12 +1638,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowOut(
|
||||
DataFlowCall call, RetNodeEx ret, FlowState state, boolean toReturn, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state, ReturnCtx returnCtx,
|
||||
ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(NodeEx out, boolean allowsFieldFlow |
|
||||
revFlow(out, state, toReturn, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
revFlow(out, state, returnCtx, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
}
|
||||
@@ -1614,7 +1653,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
ArgNodeEx arg, FlowState state, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, false, returnAp, ap, config) and
|
||||
revFlow(p, state, TReturnCtxNone(), returnAp, ap, config) and
|
||||
flowIntoCall(_, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
@@ -1622,12 +1661,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowInToReturn(
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, Ap returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnPosition returnPos, Ap returnAp,
|
||||
Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, true, apSome(returnAp), ap, config) and
|
||||
revFlow(p, state, TReturnCtxMaybeFlowThrough(returnPos), apSome(returnAp), ap, config) and
|
||||
flowThroughIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1638,11 +1679,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReturned(
|
||||
DataFlowCall call, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ReturnCtx returnCtx, ApOption returnAp, ReturnPosition pos, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, FlowState state, CcCall ccc |
|
||||
revFlowOut(call, ret, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(ret, state, ccc, apSome(_), ap, config) and
|
||||
revFlowOut(call, ret, pos, state, returnCtx, returnAp, ap, config) and
|
||||
returnFlowsThrough(ret, pos, state, ccc, _, _, ap, config) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
@@ -1713,40 +1755,39 @@ private module MkStage<StageSig PrevStage> {
|
||||
validAp(ap, config)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate parameterFlow(
|
||||
ParamNodeEx p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
|
||||
pragma[nomagic]
|
||||
private predicate parameterFlowsThroughRev(
|
||||
ParamNodeEx p, Ap ap, ReturnPosition returnPos, Configuration config
|
||||
) {
|
||||
revFlow(p, _, true, apSome(ap0), ap, config) and
|
||||
c = p.getEnclosingCallable()
|
||||
revFlow(p, _, TReturnCtxMaybeFlowThrough(returnPos), apSome(_), ap, config) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
}
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, FlowState state, Ap ap0, ReturnKindExt kind, ParameterPosition pos |
|
||||
parameterFlow(p, ap, ap0, c, config) and
|
||||
c = ret.getEnclosingCallable() and
|
||||
revFlow(pragma[only_bind_into](ret), pragma[only_bind_into](state), true, apSome(_),
|
||||
pragma[only_bind_into](ap0), pragma[only_bind_into](config)) and
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(ap), ap0, config) and
|
||||
kind = ret.getKind() and
|
||||
p.getPosition() = pos and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, ReturnPosition pos |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
exists(ParamNodeEx p, Ap ap |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(
|
||||
Ap returnAp0, ArgNodeEx arg, FlowState state, boolean toReturn, ApOption returnAp, Ap ap
|
||||
ReturnPosition returnPos0, Ap returnAp0, ArgNodeEx arg, FlowState state,
|
||||
ReturnCtx returnCtx, ApOption returnAp, Ap ap
|
||||
|
|
||||
revFlow(arg, state, toReturn, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
revFlow(arg, state, returnCtx, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1754,13 +1795,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, Configuration config
|
||||
) {
|
||||
fwd = true and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, config)) and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, config)) and
|
||||
fields = count(TypedContent f0 | fwdConsCand(f0, _, config)) and
|
||||
conscand = count(TypedContent f0, Ap ap | fwdConsCand(f0, ap, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, argAp, ap, config)
|
||||
count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, summaryCtx, argAp, ap, config)
|
||||
)
|
||||
or
|
||||
fwd = false and
|
||||
@@ -1769,8 +1810,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
conscand = count(TypedContent f0, Ap ap | consCand(f0, ap, config)) and
|
||||
states = count(FlowState state | revFlow(_, state, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, boolean b, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, b, retAp, ap, config)
|
||||
count(NodeEx n, FlowState state, ReturnCtx returnCtx, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, returnCtx, retAp, ap, config)
|
||||
)
|
||||
}
|
||||
/* End: Stage logic. */
|
||||
@@ -1915,7 +1956,7 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
|
||||
exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand1/5;
|
||||
|
||||
@@ -1951,9 +1992,10 @@ private module Stage2 implements StageSig {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand2(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand1(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
Stage2::revFlow(node2, pragma[only_bind_into](config)) and
|
||||
Stage2::revFlowAlias(node1, pragma[only_bind_into](config))
|
||||
}
|
||||
@@ -2021,8 +2063,8 @@ private module LocalFlowBigStep {
|
||||
exists(NodeEx next | Stage2::revFlow(next, state, config) |
|
||||
jumpStep(node, next, config) or
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
flowIntoCallNodeCand2(_, node, next, _, config) or
|
||||
flowOutOfCallNodeCand2(_, node, _, next, _, config) or
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
@@ -2163,7 +2205,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
|
||||
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap, config, _) and exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
@@ -2233,8 +2275,9 @@ private predicate flowCandSummaryCtx(
|
||||
NodeEx node, FlowState state, AccessPathFront argApf, Configuration config
|
||||
) {
|
||||
exists(AccessPathFront apf |
|
||||
Stage3::revFlow(node, state, true, _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), TAccessPathFrontSome(argApf), apf, config)
|
||||
Stage3::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), _, TAccessPathFrontSome(argApf), apf,
|
||||
config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2468,10 +2511,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
exists(FlowState state |
|
||||
flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand2(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
|
||||
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
|
||||
pragma[only_bind_into](config))
|
||||
@@ -2508,13 +2552,13 @@ private Configuration unbindConf(Configuration conf) {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeMayUseSummary0(
|
||||
NodeEx n, DataFlowCallable c, FlowState state, AccessPathApprox apa, Configuration config
|
||||
NodeEx n, ParamNodeEx p, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(AccessPathApprox apa0 |
|
||||
Stage4::parameterMayFlowThrough(_, c, _, _) and
|
||||
Stage4::revFlow(n, state, true, _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
|
||||
n.getEnclosingCallable() = c
|
||||
Stage4::parameterMayFlowThrough(p, _, _) and
|
||||
Stage4::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()),
|
||||
TAccessPathApproxSome(apa), apa0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2522,9 +2566,9 @@ pragma[nomagic]
|
||||
private predicate nodeMayUseSummary(
|
||||
NodeEx n, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(DataFlowCallable c |
|
||||
Stage4::parameterMayFlowThrough(_, c, apa, config) and
|
||||
nodeMayUseSummary0(n, c, state, apa, config)
|
||||
exists(ParamNodeEx p |
|
||||
Stage4::parameterMayFlowThrough(p, apa, config) and
|
||||
nodeMayUseSummary0(n, p, state, apa, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2532,7 +2576,7 @@ private newtype TSummaryCtx =
|
||||
TSummaryCtxNone() or
|
||||
TSummaryCtxSome(ParamNodeEx p, FlowState state, AccessPath ap) {
|
||||
exists(Configuration config |
|
||||
Stage4::parameterMayFlowThrough(p, _, ap.getApprox(), config) and
|
||||
Stage4::parameterMayFlowThrough(p, ap.getApprox(), config) and
|
||||
Stage4::revFlow(p, state, _, config)
|
||||
)
|
||||
}
|
||||
@@ -3453,17 +3497,11 @@ private predicate paramFlowsThrough(
|
||||
ReturnKindExt kind, FlowState state, CallContextCall cc, SummaryCtxSome sc, AccessPath ap,
|
||||
AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(PathNodeMid mid, RetNodeEx ret, ParameterPosition pos |
|
||||
exists(PathNodeMid mid, RetNodeEx ret |
|
||||
pathNode(mid, ret, state, cc, sc, ap, config, _) and
|
||||
kind = ret.getKind() and
|
||||
apa = ap.getApprox() and
|
||||
pos = sc.getParameterPos() and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
sc.getParamNode().allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(sc.getParamNode().asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -915,6 +915,17 @@ private module Cached {
|
||||
TDataFlowCallNone() or
|
||||
TDataFlowCallSome(DataFlowCall call)
|
||||
|
||||
cached
|
||||
newtype TParamNodeOption =
|
||||
TParamNodeNone() or
|
||||
TParamNodeSome(ParamNode p)
|
||||
|
||||
cached
|
||||
newtype TReturnCtx =
|
||||
TReturnCtxNone() or
|
||||
TReturnCtxNoFlowThrough() or
|
||||
TReturnCtxMaybeFlowThrough(ReturnPosition pos)
|
||||
|
||||
cached
|
||||
newtype TTypedContent = MkTypedContent(Content c, DataFlowType t) { store(_, c, _, _, t) }
|
||||
|
||||
@@ -1304,6 +1315,44 @@ class DataFlowCallOption extends TDataFlowCallOption {
|
||||
}
|
||||
}
|
||||
|
||||
/** An optional `ParamNode`. */
|
||||
class ParamNodeOption extends TParamNodeOption {
|
||||
string toString() {
|
||||
this = TParamNodeNone() and
|
||||
result = "(none)"
|
||||
or
|
||||
exists(ParamNode p |
|
||||
this = TParamNodeSome(p) and
|
||||
result = p.toString()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A return context used to calculate flow summaries in reverse flow.
|
||||
*
|
||||
* The possible values are:
|
||||
*
|
||||
* - `TReturnCtxNone()`: no return flow.
|
||||
* - `TReturnCtxNoFlowThrough()`: return flow, but flow through is not possible.
|
||||
* - `TReturnCtxMaybeFlowThrough(ReturnPosition pos)`: return flow, of kind `pos`, and
|
||||
* flow through may be possible.
|
||||
*/
|
||||
class ReturnCtx extends TReturnCtx {
|
||||
string toString() {
|
||||
this = TReturnCtxNone() and
|
||||
result = "(none)"
|
||||
or
|
||||
this = TReturnCtxNoFlowThrough() and
|
||||
result = "(no flow through)"
|
||||
or
|
||||
exists(ReturnPosition pos |
|
||||
this = TReturnCtxMaybeFlowThrough(pos) and
|
||||
result = pos.toString()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** A `Content` tagged with the type of a containing object. */
|
||||
class TypedContent extends MkTypedContent {
|
||||
private Content c;
|
||||
|
||||
@@ -319,8 +319,6 @@ private class ParamNodeEx extends NodeEx {
|
||||
}
|
||||
|
||||
ParameterPosition getPosition() { this.isParameterOf(_, result) }
|
||||
|
||||
predicate allowParameterReturnInSelf() { allowParameterReturnInSelfCached(this.asNode()) }
|
||||
}
|
||||
|
||||
private class RetNodeEx extends NodeEx {
|
||||
@@ -608,6 +606,21 @@ private predicate hasSinkCallCtx(Configuration config) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if flow from `p` to a return node of kind `kind` is allowed.
|
||||
*
|
||||
* We don't expect a parameter to return stored in itself, unless
|
||||
* explicitly allowed
|
||||
*/
|
||||
bindingset[p, kind]
|
||||
private predicate parameterFlowThroughAllowed(ParamNode p, ReturnKindExt kind) {
|
||||
exists(ParameterPosition pos | p.isParameterOf(_, pos) |
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
allowParameterReturnInSelfCached(p)
|
||||
)
|
||||
}
|
||||
|
||||
private module Stage1 implements StageSig {
|
||||
class Ap = Unit;
|
||||
|
||||
@@ -981,21 +994,22 @@ private module Stage1 implements StageSig {
|
||||
* candidate for the origin of a summary.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(ReturnKindExt kind |
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(DataFlowCallable c, ReturnKindExt kind |
|
||||
throughFlowNodeCand(p, config) and
|
||||
returnFlowCallableNodeCand(c, kind, config) and
|
||||
p.getEnclosingCallable() = c and
|
||||
exists(ap) and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(p.asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
throughFlowNodeCand(ret, config) and
|
||||
pos = ret.getReturnPosition()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(ArgNodeEx arg, boolean toReturn |
|
||||
@@ -1052,9 +1066,10 @@ private predicate viableReturnPosOutNodeCand1(
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Configuration config
|
||||
) {
|
||||
viableReturnPosOutNodeCand1(call, ret.getReturnPosition(), out, config) and
|
||||
viableReturnPosOutNodeCand1(call, pos, out, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
Stage1::revFlow(ret, config) and
|
||||
not outBarrier(ret, config) and
|
||||
not inBarrier(out, config)
|
||||
@@ -1090,7 +1105,7 @@ private predicate flowIntoCallNodeCand1(
|
||||
private int branch(NodeEx n1, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n1, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
flowOutOfCallNodeCand1(_, n1, _, n, conf) or flowIntoCallNodeCand1(_, n1, n, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1102,7 +1117,7 @@ private int branch(NodeEx n1, Configuration conf) {
|
||||
private int join(NodeEx n2, Configuration conf) {
|
||||
result =
|
||||
strictcount(NodeEx n |
|
||||
flowOutOfCallNodeCand1(_, n, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
flowOutOfCallNodeCand1(_, n, _, n2, conf) or flowIntoCallNodeCand1(_, n, n2, conf)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1115,12 +1130,13 @@ private int join(NodeEx n2, Configuration conf) {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand1(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, ret, out, config) and
|
||||
flowOutOfCallNodeCand1(call, ret, pos, out, pragma[only_bind_into](config)) and
|
||||
exists(int b, int j |
|
||||
b = branch(ret, config) and
|
||||
j = join(out, config) and
|
||||
b = branch(ret, pragma[only_bind_into](config)) and
|
||||
j = join(out, pragma[only_bind_into](config)) and
|
||||
if b.minimum(j) <= config.fieldFlowBranchLimit()
|
||||
then allowsFieldFlow = true
|
||||
else allowsFieldFlow = false
|
||||
@@ -1156,7 +1172,9 @@ private signature module StageSig {
|
||||
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config);
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config);
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config);
|
||||
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config);
|
||||
|
||||
predicate storeStepCand(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, DataFlowType contentType,
|
||||
@@ -1222,7 +1240,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
);
|
||||
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
);
|
||||
|
||||
predicate flowIntoCall(
|
||||
@@ -1247,14 +1266,16 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughOutOfCall(
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
DataFlowCall call, CcCall ccc, RetNodeEx ret, ReturnKindExt kind, NodeEx out,
|
||||
boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(_, ret.getEnclosingCallable(), _,
|
||||
pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
exists(ReturnPosition pos |
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, pragma[only_bind_into](config)) and
|
||||
kind = pos.getKind() and
|
||||
PrevStage::callMayFlowThroughRev(call, pragma[only_bind_into](config)) and
|
||||
PrevStage::returnMayFlowThrough(ret, pos, pragma[only_bind_into](config)) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
@@ -1262,29 +1283,32 @@ private module MkStage<StageSig PrevStage> {
|
||||
* configuration `config`.
|
||||
*
|
||||
* The call context `cc` records whether the node is reached through an
|
||||
* argument in a call, and if so, `argAp` records the access path of that
|
||||
* argument.
|
||||
* argument in a call, and if so, `summaryCtx` and `argAp` record the
|
||||
* corresponding parameter and access path of that argument, respectively.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate fwdFlow(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow0(node, state, cc, argAp, ap, config) and
|
||||
fwdFlow0(node, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::revFlow(node, state, unbindApa(getApprox(ap)), config) and
|
||||
filter(node, state, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlow0(
|
||||
NodeEx node, FlowState state, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
sourceNode(node, state, config) and
|
||||
(if hasSourceCallCtx(config) then cc = ccSomeCall() else cc = ccNone()) and
|
||||
argAp = apNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
ap = getApNil(node)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, Ap ap0, LocalCc localCc |
|
||||
fwdFlow(mid, state0, cc, argAp, ap0, config) and
|
||||
fwdFlow(mid, state0, cc, summaryCtx, argAp, ap0, config) and
|
||||
localCc = getLocalCc(mid, cc)
|
||||
|
|
||||
localStep(mid, state0, node, state, true, _, config, localCc) and
|
||||
@@ -1295,65 +1319,72 @@ private module MkStage<StageSig PrevStage> {
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
jumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(mid, state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(mid, node, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(mid, state0, _, _, nil, pragma[only_bind_into](config)) and
|
||||
fwdFlow(mid, state0, _, _, _, nil, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(mid, state0, node, state, config) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argAp = apNone() and
|
||||
ap = getApNil(node)
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(TypedContent tc, Ap ap0 |
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, argAp, config) and
|
||||
fwdFlowStore(_, ap0, tc, node, state, cc, summaryCtx, argAp, config) and
|
||||
ap = apCons(tc, ap0)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(Ap ap0, Content c |
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, argAp, config) and
|
||||
fwdFlowRead(ap0, c, _, node, state, cc, summaryCtx, argAp, config) and
|
||||
fwdFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(ApApprox apa |
|
||||
fwdFlowIn(_, node, state, _, cc, _, ap, config) and
|
||||
fwdFlowIn(_, node, state, _, cc, _, _, ap, config) and
|
||||
apa = getApprox(ap) and
|
||||
if PrevStage::parameterMayFlowThrough(node, _, apa, config)
|
||||
then argAp = apSome(ap)
|
||||
else argAp = apNone()
|
||||
if PrevStage::parameterMayFlowThrough(node, apa, config)
|
||||
then (
|
||||
summaryCtx = TParamNodeSome(node.asNode()) and argAp = apSome(ap)
|
||||
) else (
|
||||
summaryCtx = TParamNodeNone() and argAp = apNone()
|
||||
)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
fwdFlowOutNotFromArg(node, state, cc, argAp, ap, config)
|
||||
fwdFlowOutNotFromArg(node, state, cc, summaryCtx, argAp, ap, config)
|
||||
or
|
||||
exists(DataFlowCall call, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, argAp, argAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ParamNode summaryCtx0, Ap argAp0 |
|
||||
fwdFlowOutFromArg(call, node, state, summaryCtx0, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(call, cc, summaryCtx, argAp, summaryCtx0, argAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowStore(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
exists(DataFlowType contentType |
|
||||
fwdFlow(node1, state, cc, argAp, ap1, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap1, config) and
|
||||
PrevStage::storeStepCand(node1, unbindApa(getApprox(ap1)), tc, node2, contentType, config) and
|
||||
typecheckStore(ap1, contentType)
|
||||
)
|
||||
@@ -1366,7 +1397,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowConsCand(Ap cons, Content c, Ap tail, Configuration config) {
|
||||
exists(TypedContent tc |
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, config) and
|
||||
fwdFlowStore(_, tail, tc, _, _, _, _, _, config) and
|
||||
tc.getContent() = c and
|
||||
cons = apCons(tc, tail)
|
||||
)
|
||||
@@ -1374,21 +1405,21 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRead(
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc, ApOption argAp,
|
||||
Configuration config
|
||||
Ap ap, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Configuration config
|
||||
) {
|
||||
fwdFlow(node1, state, cc, argAp, ap, config) and
|
||||
fwdFlow(node1, state, cc, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::readStepCand(node1, c, node2, config) and
|
||||
getHeadContent(ap) = c
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc, ApOption argAp,
|
||||
Ap ap, Configuration config
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, Cc innercc,
|
||||
ParamNodeOption summaryCtx, ApOption argAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow |
|
||||
fwdFlow(arg, state, outercc, argAp, ap, config) and
|
||||
fwdFlow(arg, state, outercc, summaryCtx, argAp, ap, config) and
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1397,14 +1428,15 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutNotFromArg(
|
||||
NodeEx out, FlowState state, Cc ccOut, ApOption argAp, Ap ap, Configuration config
|
||||
NodeEx out, FlowState state, Cc ccOut, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(
|
||||
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
|
||||
DataFlowCallable inner
|
||||
|
|
||||
fwdFlow(ret, state, innercc, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
fwdFlow(ret, state, innercc, summaryCtx, argAp, ap, config) and
|
||||
flowOutOfCall(call, ret, _, out, allowsFieldFlow, config) and
|
||||
inner = ret.getEnclosingCallable() and
|
||||
ccOut = getCallContextReturn(inner, call, innercc) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
@@ -1413,12 +1445,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutFromArg(
|
||||
DataFlowCall call, NodeEx out, FlowState state, Ap argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, NodeEx out, FlowState state, ParamNode summaryCtx, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
exists(RetNodeEx ret, ReturnKindExt kind, boolean allowsFieldFlow, CcCall ccc |
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(summaryCtx), apSome(argAp), ap, config) and
|
||||
flowThroughOutOfCall(call, ccc, ret, kind, out, allowsFieldFlow, config) and
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(summaryCtx, kind)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1428,11 +1462,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIsEntered(
|
||||
DataFlowCall call, Cc cc, ApOption argAp, Ap ap, Configuration config
|
||||
DataFlowCall call, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, ParamNode p, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p |
|
||||
fwdFlowIn(call, p, _, cc, _, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, unbindApa(getApprox(ap)), config)
|
||||
exists(ParamNodeEx param |
|
||||
fwdFlowIn(call, param, _, cc, _, summaryCtx, argAp, ap, config) and
|
||||
PrevStage::parameterMayFlowThrough(param, unbindApa(getApprox(ap)), config) and
|
||||
p = param.asNode()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1440,146 +1476,149 @@ private module MkStage<StageSig PrevStage> {
|
||||
private predicate storeStepFwd(
|
||||
NodeEx node1, Ap ap1, TypedContent tc, NodeEx node2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, config) and
|
||||
fwdFlowStore(node1, ap1, tc, node2, _, _, _, _, config) and
|
||||
ap2 = apCons(tc, ap1) and
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, config)
|
||||
fwdFlowRead(ap2, tc.getContent(), _, _, _, _, _, _, config)
|
||||
}
|
||||
|
||||
private predicate readStepFwd(
|
||||
NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2, Configuration config
|
||||
) {
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, config) and
|
||||
fwdFlowRead(ap1, c, n1, n2, _, _, _, _, config) and
|
||||
fwdFlowConsCand(ap1, c, ap2, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate callMayFlowThroughFwd(DataFlowCall call, Configuration config) {
|
||||
exists(Ap argAp0, NodeEx out, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(out, state, pragma[only_bind_into](cc), pragma[only_bind_into](argAp), ap,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlowOutFromArg(call, out, state, argAp0, ap, config) and
|
||||
fwdFlowIsEntered(pragma[only_bind_into](call), pragma[only_bind_into](cc),
|
||||
pragma[only_bind_into](argAp), pragma[only_bind_into](argAp0),
|
||||
pragma[only_bind_into](config))
|
||||
)
|
||||
private predicate returnFlowsThrough(
|
||||
RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNode p, Ap argAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, ccc, TParamNodeSome(p), apSome(argAp), ap, config) and
|
||||
pos = ret.getReturnPosition() and
|
||||
parameterFlowThroughAllowed(p, pos.getKind())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowThroughIntoCall(
|
||||
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Configuration config
|
||||
) {
|
||||
flowIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
fwdFlow(arg, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
PrevStage::parameterMayFlowThrough(p, _, _, pragma[only_bind_into](config)) and
|
||||
callMayFlowThroughFwd(call, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate returnNodeMayFlowThrough(
|
||||
RetNodeEx ret, FlowState state, Ap ap, Configuration config
|
||||
) {
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(_), ap, config)
|
||||
flowIntoCall(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), allowsFieldFlow,
|
||||
pragma[only_bind_into](config)) and
|
||||
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](config)) and
|
||||
returnFlowsThrough(_, _, _, _, p.asNode(), _, _, pragma[only_bind_into](config))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `node` with access path `ap` is part of a path from a source to a
|
||||
* sink in the configuration `config`.
|
||||
*
|
||||
* The Boolean `toReturn` records whether the node must be returned from the
|
||||
* enclosing callable in order to reach a sink, and if so, `returnAp` records
|
||||
* the access path of the returned value.
|
||||
* The parameter `returnCtx` records whether (and how) the node must be returned
|
||||
* from the enclosing callable in order to reach a sink, and if so, `returnAp`
|
||||
* records the access path of the returned value.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
additional predicate revFlow(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
revFlow0(node, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, ap, config)
|
||||
revFlow0(node, state, returnCtx, returnAp, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlow0(
|
||||
NodeEx node, FlowState state, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
fwdFlow(node, state, _, _, ap, config) and
|
||||
fwdFlow(node, state, _, _, _, ap, config) and
|
||||
sinkNode(node, state, config) and
|
||||
(if hasSinkCallCtx(config) then toReturn = true else toReturn = false) and
|
||||
(
|
||||
if hasSinkCallCtx(config)
|
||||
then returnCtx = TReturnCtxNoFlowThrough()
|
||||
else returnCtx = TReturnCtxNone()
|
||||
) and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
localStep(node, state, mid, state0, true, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, ap, config)
|
||||
revFlow(mid, state0, returnCtx, returnAp, ap, config)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, pragma[only_bind_into](state), _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
localStep(node, pragma[only_bind_into](state), mid, state0, false, _, config, _) and
|
||||
revFlow(mid, state0, toReturn, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
revFlow(mid, state0, returnCtx, returnAp, nil, pragma[only_bind_into](config)) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
jumpStep(node, mid, config) and
|
||||
revFlow(mid, state, _, _, ap, config) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStep(node, mid, config) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, nil, pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0, ApNil nil |
|
||||
fwdFlow(node, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
fwdFlow(node, _, _, _, _, ap, pragma[only_bind_into](config)) and
|
||||
additionalJumpStateStep(node, state, mid, state0, config) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, nil,
|
||||
pragma[only_bind_into](config)) and
|
||||
toReturn = false and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
// store
|
||||
exists(Ap ap0, Content c |
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, toReturn, returnAp, config) and
|
||||
revFlowStore(ap0, c, ap, node, state, _, _, returnCtx, returnAp, config) and
|
||||
revFlowConsCand(ap0, c, ap, config)
|
||||
)
|
||||
or
|
||||
// read
|
||||
exists(NodeEx mid, Ap ap0 |
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
readStepFwd(node, ap, _, mid, ap0, config)
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
revFlowInNotToReturn(node, state, returnAp, ap, config) and
|
||||
toReturn = false
|
||||
returnCtx = TReturnCtxNone()
|
||||
or
|
||||
exists(DataFlowCall call, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ReturnPosition returnPos0, Ap returnAp0 |
|
||||
revFlowInToReturn(call, node, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
revFlowOut(_, node, state, _, _, ap, config) and
|
||||
toReturn = true and
|
||||
if returnNodeMayFlowThrough(node, state, ap, config)
|
||||
then returnAp = apSome(ap)
|
||||
else returnAp = apNone()
|
||||
exists(ReturnPosition pos |
|
||||
revFlowOut(_, node, pos, state, _, _, ap, config) and
|
||||
if returnFlowsThrough(node, pos, state, _, _, _, ap, config)
|
||||
then (
|
||||
returnCtx = TReturnCtxMaybeFlowThrough(pos) and
|
||||
returnAp = apSome(ap)
|
||||
) else (
|
||||
returnCtx = TReturnCtxNoFlowThrough() and returnAp = apNone()
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowStore(
|
||||
Ap ap0, Content c, Ap ap, NodeEx node, FlowState state, TypedContent tc, NodeEx mid,
|
||||
boolean toReturn, ApOption returnAp, Configuration config
|
||||
ReturnCtx returnCtx, ApOption returnAp, Configuration config
|
||||
) {
|
||||
revFlow(mid, state, toReturn, returnAp, ap0, config) and
|
||||
revFlow(mid, state, returnCtx, returnAp, ap0, config) and
|
||||
storeStepFwd(node, ap, tc, mid, ap0, config) and
|
||||
tc.getContent() = c
|
||||
}
|
||||
@@ -1599,12 +1638,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowOut(
|
||||
DataFlowCall call, RetNodeEx ret, FlowState state, boolean toReturn, ApOption returnAp, Ap ap,
|
||||
Configuration config
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state, ReturnCtx returnCtx,
|
||||
ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(NodeEx out, boolean allowsFieldFlow |
|
||||
revFlow(out, state, toReturn, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, out, allowsFieldFlow, config) and
|
||||
revFlow(out, state, returnCtx, returnAp, ap, config) and
|
||||
flowOutOfCall(call, ret, pos, out, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
}
|
||||
@@ -1614,7 +1653,7 @@ private module MkStage<StageSig PrevStage> {
|
||||
ArgNodeEx arg, FlowState state, ApOption returnAp, Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, false, returnAp, ap, config) and
|
||||
revFlow(p, state, TReturnCtxNone(), returnAp, ap, config) and
|
||||
flowIntoCall(_, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
@@ -1622,12 +1661,14 @@ private module MkStage<StageSig PrevStage> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowInToReturn(
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, Ap returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ArgNodeEx arg, FlowState state, ReturnPosition returnPos, Ap returnAp,
|
||||
Ap ap, Configuration config
|
||||
) {
|
||||
exists(ParamNodeEx p, boolean allowsFieldFlow |
|
||||
revFlow(p, state, true, apSome(returnAp), ap, config) and
|
||||
revFlow(p, state, TReturnCtxMaybeFlowThrough(returnPos), apSome(returnAp), ap, config) and
|
||||
flowThroughIntoCall(call, arg, p, allowsFieldFlow, config) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1638,11 +1679,12 @@ private module MkStage<StageSig PrevStage> {
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate revFlowIsReturned(
|
||||
DataFlowCall call, boolean toReturn, ApOption returnAp, Ap ap, Configuration config
|
||||
DataFlowCall call, ReturnCtx returnCtx, ApOption returnAp, ReturnPosition pos, Ap ap,
|
||||
Configuration config
|
||||
) {
|
||||
exists(RetNodeEx ret, FlowState state, CcCall ccc |
|
||||
revFlowOut(call, ret, state, toReturn, returnAp, ap, config) and
|
||||
fwdFlow(ret, state, ccc, apSome(_), ap, config) and
|
||||
revFlowOut(call, ret, pos, state, returnCtx, returnAp, ap, config) and
|
||||
returnFlowsThrough(ret, pos, state, ccc, _, _, ap, config) and
|
||||
matchesCall(ccc, call)
|
||||
)
|
||||
}
|
||||
@@ -1713,40 +1755,39 @@ private module MkStage<StageSig PrevStage> {
|
||||
validAp(ap, config)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate parameterFlow(
|
||||
ParamNodeEx p, Ap ap, Ap ap0, DataFlowCallable c, Configuration config
|
||||
pragma[nomagic]
|
||||
private predicate parameterFlowsThroughRev(
|
||||
ParamNodeEx p, Ap ap, ReturnPosition returnPos, Configuration config
|
||||
) {
|
||||
revFlow(p, _, true, apSome(ap0), ap, config) and
|
||||
c = p.getEnclosingCallable()
|
||||
revFlow(p, _, TReturnCtxMaybeFlowThrough(returnPos), apSome(_), ap, config) and
|
||||
parameterFlowThroughAllowed(p.asNode(), returnPos.getKind())
|
||||
}
|
||||
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, FlowState state, Ap ap0, ReturnKindExt kind, ParameterPosition pos |
|
||||
parameterFlow(p, ap, ap0, c, config) and
|
||||
c = ret.getEnclosingCallable() and
|
||||
revFlow(pragma[only_bind_into](ret), pragma[only_bind_into](state), true, apSome(_),
|
||||
pragma[only_bind_into](ap0), pragma[only_bind_into](config)) and
|
||||
fwdFlow(ret, state, any(CcCall ccc), apSome(ap), ap0, config) and
|
||||
kind = ret.getKind() and
|
||||
p.getPosition() = pos and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
p.allowParameterReturnInSelf()
|
||||
)
|
||||
pragma[nomagic]
|
||||
predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap, Configuration config) {
|
||||
exists(RetNodeEx ret, ReturnPosition pos |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate returnMayFlowThrough(RetNodeEx ret, ReturnPosition pos, Configuration config) {
|
||||
exists(ParamNodeEx p, Ap ap |
|
||||
returnFlowsThrough(ret, pos, _, _, p.asNode(), ap, _, config) and
|
||||
parameterFlowsThroughRev(p, ap, pos, config)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate callMayFlowThroughRev(DataFlowCall call, Configuration config) {
|
||||
exists(
|
||||
Ap returnAp0, ArgNodeEx arg, FlowState state, boolean toReturn, ApOption returnAp, Ap ap
|
||||
ReturnPosition returnPos0, Ap returnAp0, ArgNodeEx arg, FlowState state,
|
||||
ReturnCtx returnCtx, ApOption returnAp, Ap ap
|
||||
|
|
||||
revFlow(arg, state, toReturn, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, toReturn, returnAp, returnAp0, config)
|
||||
revFlow(arg, state, returnCtx, returnAp, ap, config) and
|
||||
revFlowInToReturn(call, arg, state, returnPos0, returnAp0, ap, config) and
|
||||
revFlowIsReturned(call, returnCtx, returnAp, returnPos0, returnAp0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1754,13 +1795,13 @@ private module MkStage<StageSig PrevStage> {
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, Configuration config
|
||||
) {
|
||||
fwd = true and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, config)) and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, config)) and
|
||||
fields = count(TypedContent f0 | fwdConsCand(f0, _, config)) and
|
||||
conscand = count(TypedContent f0, Ap ap | fwdConsCand(f0, ap, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, config)) and
|
||||
states = count(FlowState state | fwdFlow(_, state, _, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, Cc cc, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, argAp, ap, config)
|
||||
count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap |
|
||||
fwdFlow(n, state, cc, summaryCtx, argAp, ap, config)
|
||||
)
|
||||
or
|
||||
fwd = false and
|
||||
@@ -1769,8 +1810,8 @@ private module MkStage<StageSig PrevStage> {
|
||||
conscand = count(TypedContent f0, Ap ap | consCand(f0, ap, config)) and
|
||||
states = count(FlowState state | revFlow(_, state, _, _, _, config)) and
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, boolean b, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, b, retAp, ap, config)
|
||||
count(NodeEx n, FlowState state, ReturnCtx returnCtx, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, returnCtx, retAp, ap, config)
|
||||
)
|
||||
}
|
||||
/* End: Stage logic. */
|
||||
@@ -1915,7 +1956,7 @@ private module Stage2Param implements MkStage<Stage1>::StageParam {
|
||||
exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand1/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand1/5;
|
||||
|
||||
@@ -1951,9 +1992,10 @@ private module Stage2 implements StageSig {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallNodeCand2(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
flowOutOfCallNodeCand1(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand1(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
Stage2::revFlow(node2, pragma[only_bind_into](config)) and
|
||||
Stage2::revFlowAlias(node1, pragma[only_bind_into](config))
|
||||
}
|
||||
@@ -2021,8 +2063,8 @@ private module LocalFlowBigStep {
|
||||
exists(NodeEx next | Stage2::revFlow(next, state, config) |
|
||||
jumpStep(node, next, config) or
|
||||
additionalJumpStep(node, next, config) or
|
||||
flowIntoCallNodeCand1(_, node, next, config) or
|
||||
flowOutOfCallNodeCand1(_, node, next, config) or
|
||||
flowIntoCallNodeCand2(_, node, next, _, config) or
|
||||
flowOutOfCallNodeCand2(_, node, _, next, _, config) or
|
||||
Stage2::storeStepCand(node, _, _, next, _, config) or
|
||||
Stage2::readStepCand(node, _, next, config)
|
||||
)
|
||||
@@ -2163,7 +2205,7 @@ private module Stage3Param implements MkStage<Stage2>::StageParam {
|
||||
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap, config, _) and exists(lcc)
|
||||
}
|
||||
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/5;
|
||||
predicate flowOutOfCall = flowOutOfCallNodeCand2/6;
|
||||
|
||||
predicate flowIntoCall = flowIntoCallNodeCand2/5;
|
||||
|
||||
@@ -2233,8 +2275,9 @@ private predicate flowCandSummaryCtx(
|
||||
NodeEx node, FlowState state, AccessPathFront argApf, Configuration config
|
||||
) {
|
||||
exists(AccessPathFront apf |
|
||||
Stage3::revFlow(node, state, true, _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), TAccessPathFrontSome(argApf), apf, config)
|
||||
Stage3::revFlow(node, state, TReturnCtxMaybeFlowThrough(_), _, apf, config) and
|
||||
Stage3::fwdFlow(node, state, any(Stage3::CcCall ccc), _, TAccessPathFrontSome(argApf), apf,
|
||||
config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2468,10 +2511,11 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
|
||||
|
||||
pragma[nomagic]
|
||||
predicate flowOutOfCall(
|
||||
DataFlowCall call, RetNodeEx node1, NodeEx node2, boolean allowsFieldFlow, Configuration config
|
||||
DataFlowCall call, RetNodeEx node1, ReturnPosition pos, NodeEx node2, boolean allowsFieldFlow,
|
||||
Configuration config
|
||||
) {
|
||||
exists(FlowState state |
|
||||
flowOutOfCallNodeCand2(call, node1, node2, allowsFieldFlow, config) and
|
||||
flowOutOfCallNodeCand2(call, node1, pos, node2, allowsFieldFlow, config) and
|
||||
PrevStage::revFlow(node2, pragma[only_bind_into](state), _, pragma[only_bind_into](config)) and
|
||||
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _,
|
||||
pragma[only_bind_into](config))
|
||||
@@ -2508,13 +2552,13 @@ private Configuration unbindConf(Configuration conf) {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate nodeMayUseSummary0(
|
||||
NodeEx n, DataFlowCallable c, FlowState state, AccessPathApprox apa, Configuration config
|
||||
NodeEx n, ParamNodeEx p, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(AccessPathApprox apa0 |
|
||||
Stage4::parameterMayFlowThrough(_, c, _, _) and
|
||||
Stage4::revFlow(n, state, true, _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TAccessPathApproxSome(apa), apa0, config) and
|
||||
n.getEnclosingCallable() = c
|
||||
Stage4::parameterMayFlowThrough(p, _, _) and
|
||||
Stage4::revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, apa0, config) and
|
||||
Stage4::fwdFlow(n, state, any(CallContextCall ccc), TParamNodeSome(p.asNode()),
|
||||
TAccessPathApproxSome(apa), apa0, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2522,9 +2566,9 @@ pragma[nomagic]
|
||||
private predicate nodeMayUseSummary(
|
||||
NodeEx n, FlowState state, AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(DataFlowCallable c |
|
||||
Stage4::parameterMayFlowThrough(_, c, apa, config) and
|
||||
nodeMayUseSummary0(n, c, state, apa, config)
|
||||
exists(ParamNodeEx p |
|
||||
Stage4::parameterMayFlowThrough(p, apa, config) and
|
||||
nodeMayUseSummary0(n, p, state, apa, config)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -2532,7 +2576,7 @@ private newtype TSummaryCtx =
|
||||
TSummaryCtxNone() or
|
||||
TSummaryCtxSome(ParamNodeEx p, FlowState state, AccessPath ap) {
|
||||
exists(Configuration config |
|
||||
Stage4::parameterMayFlowThrough(p, _, ap.getApprox(), config) and
|
||||
Stage4::parameterMayFlowThrough(p, ap.getApprox(), config) and
|
||||
Stage4::revFlow(p, state, _, config)
|
||||
)
|
||||
}
|
||||
@@ -3453,17 +3497,11 @@ private predicate paramFlowsThrough(
|
||||
ReturnKindExt kind, FlowState state, CallContextCall cc, SummaryCtxSome sc, AccessPath ap,
|
||||
AccessPathApprox apa, Configuration config
|
||||
) {
|
||||
exists(PathNodeMid mid, RetNodeEx ret, ParameterPosition pos |
|
||||
exists(PathNodeMid mid, RetNodeEx ret |
|
||||
pathNode(mid, ret, state, cc, sc, ap, config, _) and
|
||||
kind = ret.getKind() and
|
||||
apa = ap.getApprox() and
|
||||
pos = sc.getParameterPos() and
|
||||
// we don't expect a parameter to return stored in itself, unless explicitly allowed
|
||||
(
|
||||
not kind.(ParamUpdateReturnKind).getPosition() = pos
|
||||
or
|
||||
sc.getParamNode().allowParameterReturnInSelf()
|
||||
)
|
||||
parameterFlowThroughAllowed(sc.getParamNode().asNode(), kind)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user