mirror of
https://github.com/github/codeql.git
synced 2026-04-27 17:55:19 +02:00
Dataflow: Add type-based call-edge pruning.
This commit is contained in:
@@ -326,13 +326,18 @@ string ppReprType(DataFlowType t) {
|
||||
else result = t.toString()
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate compatibleTypes0(DataFlowType t1, DataFlowType t2) {
|
||||
erasedHaveIntersection(t1, t2)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
|
||||
* a node of type `t1` to a node of type `t2`.
|
||||
*/
|
||||
bindingset[t1, t2]
|
||||
pragma[inline_late]
|
||||
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { erasedHaveIntersection(t1, t2) }
|
||||
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { compatibleTypes0(t1, t2) }
|
||||
|
||||
/** A node that performs a type cast. */
|
||||
class CastNode extends ExprNode {
|
||||
|
||||
@@ -133,6 +133,39 @@ private module Cached {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the value of `node2` is given by `node1`.
|
||||
*/
|
||||
predicate localMustFlowStep(Node node1, Node node2) {
|
||||
exists(Callable c | node1.(InstanceParameterNode).getCallable() = c |
|
||||
exists(InstanceAccess ia |
|
||||
ia = node2.asExpr() and ia.getEnclosingCallable() = c and ia.isOwnInstanceAccess()
|
||||
)
|
||||
or
|
||||
c =
|
||||
node2.(ImplicitInstanceAccess).getInstanceAccess().(OwnInstanceAccess).getEnclosingCallable()
|
||||
)
|
||||
or
|
||||
exists(SsaImplicitInit init |
|
||||
init.isParameterDefinition(node1.asParameter()) and init.getAUse() = node2.asExpr()
|
||||
)
|
||||
or
|
||||
exists(SsaExplicitUpdate upd |
|
||||
upd.getDefiningExpr().(VariableAssign).getSource() = node1.asExpr() and
|
||||
upd.getAUse() = node2.asExpr()
|
||||
)
|
||||
or
|
||||
node2.asExpr().(CastingExpr).getExpr() = node1.asExpr()
|
||||
or
|
||||
node2.asExpr().(AssignExpr).getSource() = node1.asExpr()
|
||||
or
|
||||
node1 =
|
||||
unique(FlowSummaryNode n1 |
|
||||
FlowSummaryImpl::Private::Steps::summaryLocalStep(n1.getSummaryNode(),
|
||||
node2.(FlowSummaryNode).getSummaryNode(), true)
|
||||
)
|
||||
}
|
||||
|
||||
import Cached
|
||||
|
||||
private predicate capturedVariableRead(Node n) {
|
||||
|
||||
@@ -197,6 +197,11 @@ signature module InputSig {
|
||||
*/
|
||||
predicate allowParameterReturnInSelf(ParameterNode p);
|
||||
|
||||
/**
|
||||
* Holds if the value of `node2` is given by `node1`.
|
||||
*/
|
||||
predicate localMustFlowStep(Node node1, Node node2);
|
||||
|
||||
class LambdaCallKind;
|
||||
|
||||
/** Holds if `creation` is an expression that creates a lambda of kind `kind` for `c`. */
|
||||
|
||||
@@ -1289,36 +1289,11 @@ module MakeImpl<InputSig Lang> {
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, state, _, _, _, _, t, ap, apa) and
|
||||
jumpStepEx(mid, node) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argT instanceof TypOption::None and
|
||||
argAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, state, _, _, _, _, _, ap, apa) and
|
||||
additionalJumpStep(mid, node) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argT instanceof TypOption::None and
|
||||
argAp = apNone() and
|
||||
t = getNodeTyp(node) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
fwdFlow(mid, state0, _, _, _, _, _, ap, apa) and
|
||||
additionalJumpStateStep(mid, state0, node, state) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argT instanceof TypOption::None and
|
||||
argAp = apNone() and
|
||||
t = getNodeTyp(node) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
fwdFlowJump(node, state, t, ap, apa) and
|
||||
cc = ccNone() and
|
||||
summaryCtx = TParamNodeNone() and
|
||||
argT instanceof TypOption::None and
|
||||
argAp = apNone()
|
||||
or
|
||||
// store
|
||||
exists(Content c, Typ t0, Ap ap0 |
|
||||
@@ -1346,7 +1321,7 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
or
|
||||
// flow out of a callable
|
||||
fwdFlowOut(node, state, cc, summaryCtx, argT, argAp, t, ap, apa)
|
||||
fwdFlowOut(_, _, node, state, cc, summaryCtx, argT, argAp, t, ap, apa)
|
||||
or
|
||||
// flow through a callable
|
||||
exists(
|
||||
@@ -1360,6 +1335,27 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fwdFlowJump(NodeEx node, FlowState state, Typ t, Ap ap, ApApprox apa) {
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, state, _, _, _, _, t, ap, apa) and
|
||||
jumpStepEx(mid, node)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
fwdFlow(mid, state, _, _, _, _, _, ap, apa) and
|
||||
additionalJumpStep(mid, node) and
|
||||
t = getNodeTyp(node) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
fwdFlow(mid, state0, _, _, _, _, _, ap, apa) and
|
||||
additionalJumpStateStep(mid, state0, node, state) and
|
||||
t = getNodeTyp(node) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowStore(
|
||||
NodeEx node1, Typ t1, Ap ap1, Content c, Typ t2, NodeEx node2, FlowState state, Cc cc,
|
||||
@@ -1455,11 +1451,12 @@ module MakeImpl<InputSig Lang> {
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, CcCall innercc,
|
||||
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa
|
||||
private predicate fwdFlowInCand(
|
||||
DataFlowCall call, DataFlowCallable inner, ParamNodeEx p, FlowState state, Cc outercc,
|
||||
CcCall innercc, ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap,
|
||||
ApApprox apa
|
||||
) {
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow, DataFlowCallable inner |
|
||||
exists(ArgNodeEx arg, boolean allowsFieldFlow |
|
||||
fwdFlow(arg, state, outercc, summaryCtx, argT, argAp, t, ap, apa) and
|
||||
(
|
||||
inner = viableImplCallContextReducedInlineLate(call, arg, outercc)
|
||||
@@ -1473,6 +1470,19 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowIn(
|
||||
DataFlowCall call, ParamNodeEx p, FlowState state, Cc outercc, CcCall innercc,
|
||||
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa
|
||||
) {
|
||||
exists(DataFlowCallable inner, boolean cc |
|
||||
fwdFlowInCand(call, inner, p, state, outercc, innercc, summaryCtx, argT, argAp, t, ap,
|
||||
apa) and
|
||||
FwdTypeFlow::typeFlowValidEdgeIn(call, inner, cc) and
|
||||
if outercc instanceof CcCall then cc = true else cc = false
|
||||
)
|
||||
}
|
||||
|
||||
bindingset[ctx, result]
|
||||
pragma[inline_late]
|
||||
private DataFlowCallable viableImplCallContextReducedReverseInlineLate(
|
||||
@@ -1501,16 +1511,12 @@ module MakeImpl<InputSig Lang> {
|
||||
flowOutOfCallApa(call, c, ret, _, out, allowsFieldFlow, apa)
|
||||
}
|
||||
|
||||
// inline to reduce number of iterations
|
||||
pragma[inline]
|
||||
private predicate fwdFlowOut(
|
||||
NodeEx out, FlowState state, CcNoCall outercc, ParamNodeOption summaryCtx, TypOption argT,
|
||||
ApOption argAp, Typ t, Ap ap, ApApprox apa
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowOutCand(
|
||||
DataFlowCall call, DataFlowCallable inner, NodeEx out, FlowState state, CcNoCall outercc,
|
||||
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa
|
||||
) {
|
||||
exists(
|
||||
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
|
||||
DataFlowCallable inner
|
||||
|
|
||||
exists(RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc |
|
||||
fwdFlow(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa) and
|
||||
inner = ret.getEnclosingCallable() and
|
||||
(
|
||||
@@ -1526,6 +1532,63 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate fwdFlowOut(
|
||||
DataFlowCall call, DataFlowCallable inner, NodeEx out, FlowState state, CcNoCall outercc,
|
||||
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa
|
||||
) {
|
||||
fwdFlowOutCand(call, inner, out, state, outercc, summaryCtx, argT, argAp, t, ap, apa) and
|
||||
FwdTypeFlow::typeFlowValidEdgeOut(call, inner)
|
||||
}
|
||||
|
||||
private module FwdTypeFlowInput implements TypeFlowInput {
|
||||
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) {
|
||||
flowIntoCallApa(call, c, _, _, _, _)
|
||||
}
|
||||
|
||||
predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) {
|
||||
flowOutOfCallApa(call, c, _, _, _, _, _)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate dataFlowTakenCallEdgeIn(DataFlowCall call, DataFlowCallable c, boolean cc) {
|
||||
exists(ParamNodeEx p, Cc outercc |
|
||||
fwdFlowIn(call, p, _, outercc, _, _, _, _, _, _, _) and
|
||||
c = p.getEnclosingCallable() and
|
||||
if outercc instanceof CcCall then cc = true else cc = false
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate dataFlowTakenCallEdgeOut(DataFlowCall call, DataFlowCallable c) {
|
||||
fwdFlowOut(call, c, _, _, _, _, _, _, _, _, _)
|
||||
}
|
||||
|
||||
predicate dataFlowNonCallEntry(DataFlowCallable c, boolean cc) {
|
||||
exists(NodeEx node, FlowState state |
|
||||
sourceNode(node, state) and
|
||||
(if hasSourceCallCtx() then cc = true else cc = false) and
|
||||
PrevStage::revFlow(node, state, getApprox(any(ApNil nil))) and
|
||||
c = node.getEnclosingCallable()
|
||||
)
|
||||
or
|
||||
exists(NodeEx node |
|
||||
cc = false and
|
||||
fwdFlowJump(node, _, _, _, _) and
|
||||
c = node.getEnclosingCallable()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private module FwdTypeFlow = TypeFlow<FwdTypeFlowInput>;
|
||||
|
||||
private predicate flowIntoCallApaValid(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p,
|
||||
boolean allowsFieldFlow, ApApprox apa
|
||||
) {
|
||||
flowIntoCallApa(call, c, arg, p, allowsFieldFlow, apa) and
|
||||
FwdTypeFlow::typeFlowValidEdgeIn(call, c, _)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate fwdFlowRetFromArg(
|
||||
RetNodeEx ret, FlowState state, CcCall ccc, ParamNodeEx summaryCtx, Typ argT, Ap argAp,
|
||||
@@ -1625,7 +1688,7 @@ module MakeImpl<InputSig Lang> {
|
||||
exists(ApApprox argApa, Typ argT |
|
||||
returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT),
|
||||
pragma[only_bind_into](argAp), ap) and
|
||||
flowIntoCallApa(call, _, pragma[only_bind_into](arg), p, allowsFieldFlow, argApa) and
|
||||
flowIntoCallApaValid(call, _, pragma[only_bind_into](arg), p, allowsFieldFlow, argApa) and
|
||||
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp),
|
||||
argApa) and
|
||||
if allowsFieldFlow = false then argAp instanceof ApNil else any()
|
||||
@@ -1633,9 +1696,11 @@ module MakeImpl<InputSig Lang> {
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowIntoCallAp(DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, Ap ap) {
|
||||
private predicate flowIntoCallAp(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, Ap ap
|
||||
) {
|
||||
exists(ApApprox apa, boolean allowsFieldFlow |
|
||||
flowIntoCallApa(call, _, arg, p, allowsFieldFlow, apa) and
|
||||
flowIntoCallApaValid(call, c, arg, p, allowsFieldFlow, apa) and
|
||||
fwdFlow(arg, _, _, _, _, _, _, ap, apa) and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
)
|
||||
@@ -1643,13 +1708,17 @@ module MakeImpl<InputSig Lang> {
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate flowOutOfCallAp(
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Ap ap
|
||||
DataFlowCall call, DataFlowCallable c, RetNodeEx ret, ReturnPosition pos, NodeEx out,
|
||||
Ap ap
|
||||
) {
|
||||
exists(ApApprox apa, boolean allowsFieldFlow |
|
||||
flowOutOfCallApa(call, _, ret, _, out, allowsFieldFlow, apa) and
|
||||
flowOutOfCallApa(call, c, ret, _, out, allowsFieldFlow, apa) and
|
||||
fwdFlow(ret, _, _, _, _, _, _, ap, apa) and
|
||||
pos = ret.getReturnPosition() and
|
||||
if allowsFieldFlow = false then ap instanceof ApNil else any()
|
||||
|
|
||||
FwdTypeFlow::typeFlowValidEdgeIn(call, c, _) or
|
||||
FwdTypeFlow::typeFlowValidEdgeOut(call, c)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1694,28 +1763,9 @@ module MakeImpl<InputSig Lang> {
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
jumpStepEx(node, mid) and
|
||||
revFlow(mid, state, _, _, ap) and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
additionalJumpStep(node, mid) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, ap) and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
additionalJumpStateStep(node, state, mid, state0) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, ap) and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone() and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
revFlowJump(node, state, ap) and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
or
|
||||
// store
|
||||
exists(Ap ap0, Content c |
|
||||
@@ -1730,11 +1780,9 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
or
|
||||
// flow into a callable
|
||||
exists(ParamNodeEx p |
|
||||
revFlow(p, state, TReturnCtxNone(), returnAp, ap) and
|
||||
flowIntoCallAp(_, node, p, ap) and
|
||||
returnCtx = TReturnCtxNone()
|
||||
)
|
||||
revFlowIn(_, _, node, state, ap) and
|
||||
returnCtx = TReturnCtxNone() and
|
||||
returnAp = apNone()
|
||||
or
|
||||
// flow through a callable
|
||||
exists(DataFlowCall call, ParamNodeEx p, Ap innerReturnAp |
|
||||
@@ -1755,6 +1803,25 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
private predicate revFlowJump(NodeEx node, FlowState state, Ap ap) {
|
||||
exists(NodeEx mid |
|
||||
jumpStepEx(node, mid) and
|
||||
revFlow(mid, state, _, _, ap)
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid |
|
||||
additionalJumpStep(node, mid) and
|
||||
revFlow(pragma[only_bind_into](mid), state, _, _, ap) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
or
|
||||
exists(NodeEx mid, FlowState state0 |
|
||||
additionalJumpStateStep(node, state, mid, state0) and
|
||||
revFlow(pragma[only_bind_into](mid), pragma[only_bind_into](state0), _, _, ap) and
|
||||
ap instanceof ApNil
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowStore(
|
||||
Ap ap0, Content c, Ap ap, Typ t, NodeEx node, FlowState state, NodeEx mid,
|
||||
@@ -1777,14 +1844,81 @@ module MakeImpl<InputSig Lang> {
|
||||
)
|
||||
}
|
||||
|
||||
private module RevTypeFlowInput implements TypeFlowInput {
|
||||
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) {
|
||||
flowOutOfCallAp(call, c, _, _, _, _)
|
||||
}
|
||||
|
||||
predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) {
|
||||
flowIntoCallAp(call, c, _, _, _)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate dataFlowTakenCallEdgeIn(DataFlowCall call, DataFlowCallable c, boolean cc) {
|
||||
exists(RetNodeEx ret, ReturnCtx returnCtx |
|
||||
revFlowOut(call, ret, _, _, returnCtx, _, _) and
|
||||
c = ret.getEnclosingCallable() and
|
||||
if returnCtx instanceof TReturnCtxNone then cc = false else cc = true
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate dataFlowTakenCallEdgeOut(DataFlowCall call, DataFlowCallable c) {
|
||||
revFlowIn(call, c, _, _, _)
|
||||
}
|
||||
|
||||
predicate dataFlowNonCallEntry(DataFlowCallable c, boolean cc) {
|
||||
exists(NodeEx node, FlowState state, ApNil nil |
|
||||
fwdFlow(node, state, _, _, _, _, _, nil, _) and
|
||||
sinkNode(node, state) and
|
||||
(if hasSinkCallCtx() then cc = true else cc = false) and
|
||||
c = node.getEnclosingCallable()
|
||||
)
|
||||
or
|
||||
exists(NodeEx node |
|
||||
cc = false and
|
||||
revFlowJump(node, _, _) and
|
||||
c = node.getEnclosingCallable()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private module RevTypeFlow = TypeFlow<RevTypeFlowInput>;
|
||||
|
||||
private predicate flowIntoCallApValid(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, Ap ap
|
||||
) {
|
||||
flowIntoCallAp(call, c, arg, p, ap) and
|
||||
RevTypeFlow::typeFlowValidEdgeOut(call, c)
|
||||
}
|
||||
|
||||
private predicate flowOutOfCallApValid(
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Ap ap, boolean cc
|
||||
) {
|
||||
exists(DataFlowCallable c |
|
||||
flowOutOfCallAp(call, c, ret, pos, out, ap) and
|
||||
RevTypeFlow::typeFlowValidEdgeIn(call, c, cc)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate revFlowIn(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, FlowState state, Ap ap
|
||||
) {
|
||||
exists(ParamNodeEx p |
|
||||
revFlow(p, state, TReturnCtxNone(), _, ap) and
|
||||
flowIntoCallApValid(call, c, arg, p, ap)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate revFlowOut(
|
||||
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state,
|
||||
ReturnCtx returnCtx, ApOption returnAp, Ap ap
|
||||
) {
|
||||
exists(NodeEx out |
|
||||
exists(NodeEx out, boolean cc |
|
||||
revFlow(out, state, returnCtx, returnAp, ap) and
|
||||
flowOutOfCallAp(call, ret, pos, out, ap)
|
||||
flowOutOfCallApValid(call, ret, pos, out, ap, cc) and
|
||||
if returnCtx instanceof TReturnCtxNone then cc = false else cc = true
|
||||
)
|
||||
}
|
||||
|
||||
@@ -1921,7 +2055,8 @@ module MakeImpl<InputSig Lang> {
|
||||
}
|
||||
|
||||
additional predicate stats(
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples
|
||||
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges,
|
||||
int tfnodes, int tftuples
|
||||
) {
|
||||
fwd = true and
|
||||
nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _, _, _)) and
|
||||
@@ -1932,7 +2067,13 @@ module MakeImpl<InputSig Lang> {
|
||||
count(NodeEx n, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
|
||||
ApOption argAp, Typ t, Ap ap |
|
||||
fwdFlow(n, state, cc, summaryCtx, argT, argAp, t, ap, _)
|
||||
)
|
||||
) and
|
||||
calledges =
|
||||
count(DataFlowCall call, DataFlowCallable c |
|
||||
FwdTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) or
|
||||
FwdTypeFlowInput::dataFlowTakenCallEdgeOut(call, c)
|
||||
) and
|
||||
FwdTypeFlow::typeFlowStats(tfnodes, tftuples)
|
||||
or
|
||||
fwd = false and
|
||||
nodes = count(NodeEx node | revFlow(node, _, _, _, _)) and
|
||||
@@ -1942,7 +2083,13 @@ module MakeImpl<InputSig Lang> {
|
||||
tuples =
|
||||
count(NodeEx n, FlowState state, ReturnCtx returnCtx, ApOption retAp, Ap ap |
|
||||
revFlow(n, state, returnCtx, retAp, ap)
|
||||
)
|
||||
) and
|
||||
calledges =
|
||||
count(DataFlowCall call, DataFlowCallable c |
|
||||
RevTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) or
|
||||
RevTypeFlowInput::dataFlowTakenCallEdgeOut(call, c)
|
||||
) and
|
||||
RevTypeFlow::typeFlowStats(tfnodes, tftuples)
|
||||
}
|
||||
/* End: Stage logic. */
|
||||
}
|
||||
@@ -3972,51 +4119,68 @@ module MakeImpl<InputSig Lang> {
|
||||
* Calculates per-stage metrics for data flow.
|
||||
*/
|
||||
predicate stageStats(
|
||||
int n, string stage, int nodes, int fields, int conscand, int states, int tuples
|
||||
int n, string stage, int nodes, int fields, int conscand, int states, int tuples,
|
||||
int calledges, int tfnodes, int tftuples
|
||||
) {
|
||||
stage = "1 Fwd" and
|
||||
n = 10 and
|
||||
Stage1::stats(true, nodes, fields, conscand, states, tuples)
|
||||
Stage1::stats(true, nodes, fields, conscand, states, tuples) and
|
||||
calledges = -1 and
|
||||
tfnodes = -1 and
|
||||
tftuples = -1
|
||||
or
|
||||
stage = "1 Rev" and
|
||||
n = 15 and
|
||||
Stage1::stats(false, nodes, fields, conscand, states, tuples)
|
||||
Stage1::stats(false, nodes, fields, conscand, states, tuples) and
|
||||
calledges = -1 and
|
||||
tfnodes = -1 and
|
||||
tftuples = -1
|
||||
or
|
||||
stage = "2 Fwd" and
|
||||
n = 20 and
|
||||
Stage2::stats(true, nodes, fields, conscand, states, tuples)
|
||||
Stage2::stats(true, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "2 Rev" and
|
||||
n = 25 and
|
||||
Stage2::stats(false, nodes, fields, conscand, states, tuples)
|
||||
Stage2::stats(false, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "3 Fwd" and
|
||||
n = 30 and
|
||||
Stage3::stats(true, nodes, fields, conscand, states, tuples)
|
||||
Stage3::stats(true, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "3 Rev" and
|
||||
n = 35 and
|
||||
Stage3::stats(false, nodes, fields, conscand, states, tuples)
|
||||
Stage3::stats(false, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "4 Fwd" and
|
||||
n = 40 and
|
||||
Stage4::stats(true, nodes, fields, conscand, states, tuples)
|
||||
Stage4::stats(true, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "4 Rev" and
|
||||
n = 45 and
|
||||
Stage4::stats(false, nodes, fields, conscand, states, tuples)
|
||||
Stage4::stats(false, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "5 Fwd" and
|
||||
n = 50 and
|
||||
Stage5::stats(true, nodes, fields, conscand, states, tuples)
|
||||
Stage5::stats(true, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "5 Rev" and
|
||||
n = 55 and
|
||||
Stage5::stats(false, nodes, fields, conscand, states, tuples)
|
||||
Stage5::stats(false, nodes, fields, conscand, states, tuples, calledges, tfnodes, tftuples)
|
||||
or
|
||||
stage = "6 Fwd" and n = 60 and finalStats(true, nodes, fields, conscand, states, tuples)
|
||||
stage = "6 Fwd" and
|
||||
n = 60 and
|
||||
finalStats(true, nodes, fields, conscand, states, tuples) and
|
||||
calledges = -1 and
|
||||
tfnodes = -1 and
|
||||
tftuples = -1
|
||||
or
|
||||
stage = "6 Rev" and n = 65 and finalStats(false, nodes, fields, conscand, states, tuples)
|
||||
stage = "6 Rev" and
|
||||
n = 65 and
|
||||
finalStats(false, nodes, fields, conscand, states, tuples) and
|
||||
calledges = -1 and
|
||||
tfnodes = -1 and
|
||||
tftuples = -1
|
||||
}
|
||||
|
||||
module FlowExploration<explorationLimitSig/0 explorationLimit> {
|
||||
|
||||
@@ -890,6 +890,9 @@ module MakeImplCommon<InputSig Lang> {
|
||||
cached
|
||||
predicate allowParameterReturnInSelfCached(ParamNode p) { allowParameterReturnInSelf(p) }
|
||||
|
||||
cached
|
||||
predicate paramMustFlow(ParamNode p, ArgNode arg) { localMustFlowStep+(p, arg) }
|
||||
|
||||
cached
|
||||
newtype TCallContext =
|
||||
TAnyCallContext() or
|
||||
@@ -958,6 +961,364 @@ module MakeImplCommon<InputSig Lang> {
|
||||
TApproxAccessPathFrontSome(ApproxAccessPathFront apf)
|
||||
}
|
||||
|
||||
bindingset[t1, t2]
|
||||
pragma[inline_late]
|
||||
private predicate typeStrongerThan0(DataFlowType t1, DataFlowType t2) { typeStrongerThan(t1, t2) }
|
||||
|
||||
private predicate callEdge(DataFlowCall call, DataFlowCallable c, ArgNode arg, ParamNode p) {
|
||||
viableParamArg(call, p, arg) and
|
||||
c = getNodeEnclosingCallable(p)
|
||||
}
|
||||
|
||||
signature module TypeFlowInput {
|
||||
/** Holds if the edge is possibly needed in the direction `call` to `c`. */
|
||||
predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c);
|
||||
|
||||
/** Holds if the edge is possibly needed in the direction `c` to `call`. */
|
||||
predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c);
|
||||
|
||||
/**
|
||||
* Holds if the edge is followed in data flow in the direction `call` to `c`
|
||||
* and the call context `cc`.
|
||||
*/
|
||||
predicate dataFlowTakenCallEdgeIn(DataFlowCall call, DataFlowCallable c, boolean cc);
|
||||
|
||||
/**
|
||||
* Holds if the edge is followed in data flow in the direction `c` to `call`.
|
||||
*/
|
||||
predicate dataFlowTakenCallEdgeOut(DataFlowCall call, DataFlowCallable c);
|
||||
|
||||
/**
|
||||
* Holds if data flow enters `c` with call context `cc` without using a call
|
||||
* edge.
|
||||
*/
|
||||
predicate dataFlowNonCallEntry(DataFlowCallable c, boolean cc);
|
||||
}
|
||||
|
||||
/**
|
||||
* Given a call graph for a set of flow paths, this module calculates the type
|
||||
* flow between parameter and argument nodes in the cases where it is possible
|
||||
* for a type to first be weakened and then strengthened again. When the
|
||||
* stronger types at the end-points of such a type flow path are incompatible,
|
||||
* the call relevant call edges can be excluded as impossible.
|
||||
*
|
||||
* The predicates `relevantCallEdgeIn` and `relevantCallEdgeOut` give the
|
||||
* graph to be explored prior to the recursion, and the other three predicates
|
||||
* are calculated in mutual recursion with the output of this module, which is
|
||||
* given in `typeFlowValidEdgeIn` and `typeFlowValidEdgeOut`.
|
||||
*/
|
||||
module TypeFlow<TypeFlowInput Input> {
|
||||
private predicate relevantCallEdge(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNode arg, ParamNode p
|
||||
) {
|
||||
callEdge(call, c, arg, p) and
|
||||
(
|
||||
Input::relevantCallEdgeIn(call, c) or
|
||||
Input::relevantCallEdgeOut(call, c)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a sequence calls may propagates the value of `p` to some
|
||||
* argument-to-parameter call edge that strengthens the static type.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate trackedParamTypeCand(ParamNode p) {
|
||||
exists(ArgNode arg |
|
||||
trackedArgTypeCand(arg) and
|
||||
paramMustFlow(p, arg)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a sequence calls may propagates the value of `arg` to some
|
||||
* argument-to-parameter call edge that strengthens the static type.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate trackedArgTypeCand(ArgNode arg) {
|
||||
exists(ParamNode p, DataFlowType at, DataFlowType pt |
|
||||
at = getNodeType(arg) and
|
||||
pt = getNodeType(p) and
|
||||
relevantCallEdge(_, _, arg, p) and
|
||||
typeStrongerThan0(pt, at)
|
||||
)
|
||||
or
|
||||
exists(ParamNode p, DataFlowType at, DataFlowType pt |
|
||||
at = getNodeType(arg) and
|
||||
pt = getNodeType(p) and
|
||||
paramMustFlow(p, arg) and
|
||||
relevantCallEdge(_, _, arg, _) and
|
||||
typeStrongerThan0(at, pt)
|
||||
)
|
||||
or
|
||||
exists(ParamNode p |
|
||||
trackedParamTypeCand(p) and
|
||||
relevantCallEdge(_, _, arg, p)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `p` is part of a value-propagating call path where the
|
||||
* end-points have stronger types than the intermediate parameter and
|
||||
* argument nodes.
|
||||
*/
|
||||
private predicate trackedParamType(ParamNode p) {
|
||||
exists(
|
||||
DataFlowCall call1, DataFlowCallable c1, ArgNode argOut, DataFlowCall call2,
|
||||
DataFlowCallable c2, ArgNode argIn
|
||||
|
|
||||
trackedParamTypeCand(p) and
|
||||
callEdge(call1, c1, argOut, _) and
|
||||
Input::relevantCallEdgeOut(call1, c1) and
|
||||
trackedArgTypeCand(argOut) and
|
||||
paramMustFlow(p, argOut) and
|
||||
callEdge(call2, c2, argIn, _) and
|
||||
Input::relevantCallEdgeIn(call2, c2) and
|
||||
trackedArgTypeCand(argIn) and
|
||||
paramMustFlow(p, argIn)
|
||||
)
|
||||
or
|
||||
exists(ArgNode arg, DataFlowType at, DataFlowType pt |
|
||||
trackedParamTypeCand(p) and
|
||||
at = getNodeType(arg) and
|
||||
pt = getNodeType(p) and
|
||||
relevantCallEdge(_, _, arg, p) and
|
||||
typeStrongerThan0(at, pt)
|
||||
)
|
||||
or
|
||||
exists(ArgNode arg |
|
||||
trackedArgType(arg) and
|
||||
relevantCallEdge(_, _, arg, p) and
|
||||
trackedParamTypeCand(p)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `arg` is part of a value-propagating call path where the
|
||||
* end-points have stronger types than the intermediate parameter and
|
||||
* argument nodes.
|
||||
*/
|
||||
private predicate trackedArgType(ArgNode arg) {
|
||||
exists(ParamNode p |
|
||||
trackedParamType(p) and
|
||||
paramMustFlow(p, arg) and
|
||||
trackedArgTypeCand(arg)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate returnCallDeterminesParam(DataFlowCall call, ParamNode p) {
|
||||
exists(ArgNode arg |
|
||||
trackedArgType(arg) and
|
||||
arg.argumentOf(call, _) and
|
||||
paramMustFlow(p, arg)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate returnCallLeavesParamUndetermined(DataFlowCall call, ParamNode p) {
|
||||
trackedParamType(p) and
|
||||
call.getEnclosingCallable() = getNodeEnclosingCallable(p) and
|
||||
not returnCallDeterminesParam(call, p)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate trackedParamWithType(ParamNode p, DataFlowType t, DataFlowCallable c) {
|
||||
trackedParamType(p) and
|
||||
c = getNodeEnclosingCallable(p) and
|
||||
nodeDataFlowType(p, t)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate dataFlowTakenCallEdgeIn(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNode arg, ParamNode p, boolean cc
|
||||
) {
|
||||
Input::dataFlowTakenCallEdgeIn(call, c, cc) and
|
||||
callEdge(call, c, arg, p) and
|
||||
trackedParamType(p)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate dataFlowTakenCallEdgeOut(
|
||||
DataFlowCall call, DataFlowCallable c, ArgNode arg, ParamNode p
|
||||
) {
|
||||
Input::dataFlowTakenCallEdgeOut(call, c) and
|
||||
callEdge(call, c, arg, p) and
|
||||
trackedArgType(arg) and
|
||||
paramMustFlow(_, arg)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `t` is a possible type for an argument reaching the tracked
|
||||
* parameter `p` through an in-going edge in the current data flow stage.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate typeFlowParamTypeCand(ParamNode p, DataFlowType t) {
|
||||
exists(ArgNode arg, boolean outercc |
|
||||
dataFlowTakenCallEdgeIn(_, _, arg, p, outercc) and
|
||||
if trackedArgType(arg) then typeFlowArgType(arg, t, outercc) else nodeDataFlowType(arg, t)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `t` is a possible type for the tracked parameter `p` in the call
|
||||
* context `cc` and that the current data flow stage has reached this
|
||||
* context.
|
||||
*/
|
||||
private predicate typeFlowParamType(ParamNode p, DataFlowType t, boolean cc) {
|
||||
exists(DataFlowCallable c |
|
||||
Input::dataFlowNonCallEntry(c, cc) and
|
||||
trackedParamWithType(p, t, c)
|
||||
)
|
||||
or
|
||||
exists(DataFlowType t1, DataFlowType t2 |
|
||||
cc = true and
|
||||
typeFlowParamTypeCand(p, t1) and
|
||||
nodeDataFlowType(p, t2) and
|
||||
if typeStrongerThan(t2, t1) then t = t2 else (compatibleTypes(t1, t2) and t = t1)
|
||||
)
|
||||
or
|
||||
exists(ArgNode arg, DataFlowType t1, DataFlowType t2 |
|
||||
cc = false and
|
||||
typeFlowArgTypeFromReturn(arg, t1) and
|
||||
paramMustFlow(p, arg) and
|
||||
nodeDataFlowType(p, t2) and
|
||||
if typeStrongerThan(t2, t1) then t = t2 else (compatibleTypes(t1, t2) and t = t1)
|
||||
)
|
||||
or
|
||||
exists(DataFlowCall call |
|
||||
cc = false and
|
||||
Input::dataFlowTakenCallEdgeOut(call, _) and
|
||||
returnCallLeavesParamUndetermined(call, p) and
|
||||
nodeDataFlowType(p, t)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `t` is a possible type for the tracked argument `arg` and that
|
||||
* the current data flow stage has reached the call of `arg` from one of its
|
||||
* call targets.
|
||||
*/
|
||||
private predicate typeFlowArgTypeFromReturn(ArgNode arg, DataFlowType t) {
|
||||
exists(ParamNode p, DataFlowType t1, DataFlowType t2 |
|
||||
dataFlowTakenCallEdgeOut(_, _, arg, p) and
|
||||
(if trackedParamType(p) then typeFlowParamType(p, t1, false) else nodeDataFlowType(p, t1)) and
|
||||
nodeDataFlowType(arg, t2) and
|
||||
if typeStrongerThan(t2, t1) then t = t2 else (compatibleTypes(t1, t2) and t = t1)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `t` is a possible type for the tracked argument `arg` in the call
|
||||
* context `cc` and that the current data flow stage has reached this
|
||||
* context.
|
||||
*/
|
||||
private predicate typeFlowArgType(ArgNode arg, DataFlowType t, boolean cc) {
|
||||
trackedArgType(arg) and
|
||||
(
|
||||
exists(ParamNode p, DataFlowType t1, DataFlowType t2 |
|
||||
paramMustFlow(p, arg) and
|
||||
typeFlowParamType(p, t1, cc) and
|
||||
nodeDataFlowType(arg, t2) and
|
||||
if typeStrongerThan(t2, t1) then t = t2 else (compatibleTypes(t1, t2) and t = t1)
|
||||
)
|
||||
or
|
||||
cc = [true, false] and
|
||||
not paramMustFlow(_, arg) and
|
||||
nodeDataFlowType(arg, t)
|
||||
)
|
||||
}
|
||||
|
||||
predicate typeFlowStats(int nodes, int tuples) {
|
||||
nodes =
|
||||
count(Node n |
|
||||
typeFlowParamType(n, _, _) or typeFlowArgTypeFromReturn(n, _) or typeFlowArgType(n, _, _)
|
||||
) and
|
||||
tuples =
|
||||
count(Node n, DataFlowType t, boolean cc |
|
||||
typeFlowParamType(n, t, cc)
|
||||
or
|
||||
typeFlowArgTypeFromReturn(n, t) and cc = false
|
||||
or
|
||||
typeFlowArgType(n, t, cc)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `arg`-to-`p` edge should be considered for validation of the
|
||||
* corresponding call edge in the in-going direction.
|
||||
*/
|
||||
private predicate relevantArgParamIn(ArgNode arg, ParamNode p, DataFlowType pt) {
|
||||
exists(DataFlowCall call, DataFlowCallable c |
|
||||
Input::relevantCallEdgeIn(call, c) and
|
||||
callEdge(call, c, arg, p) and
|
||||
paramMustFlow(_, arg) and
|
||||
trackedArgType(arg) and
|
||||
nodeDataFlowType(p, pt)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there is a possible type for `arg` in the call context `cc` that
|
||||
* is consistent with the static type of `p`.
|
||||
*/
|
||||
private predicate validArgParamIn(ArgNode arg, ParamNode p, boolean cc) {
|
||||
exists(DataFlowType t1, DataFlowType t2 |
|
||||
typeFlowArgType(arg, t1, cc) and
|
||||
relevantArgParamIn(arg, p, t2) and
|
||||
compatibleTypes(t1, t2)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the edge `call`-to-`c` is valid in the in-going direction in the
|
||||
* call context `cc`.
|
||||
*/
|
||||
predicate typeFlowValidEdgeIn(DataFlowCall call, DataFlowCallable c, boolean cc) {
|
||||
Input::relevantCallEdgeIn(call, c) and
|
||||
cc = [true, false] and
|
||||
forall(ArgNode arg, ParamNode p |
|
||||
callEdge(call, c, arg, p) and trackedArgType(arg) and paramMustFlow(_, arg)
|
||||
|
|
||||
validArgParamIn(arg, p, cc)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `arg`-to-`p` edge should be considered for validation of the
|
||||
* corresponding call edge in the out-going direction.
|
||||
*/
|
||||
private predicate relevantArgParamOut(ArgNode arg, ParamNode p, DataFlowType argt) {
|
||||
exists(DataFlowCall call, DataFlowCallable c |
|
||||
Input::relevantCallEdgeOut(call, c) and
|
||||
callEdge(call, c, arg, p) and
|
||||
trackedParamType(p) and
|
||||
nodeDataFlowType(arg, argt)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there is a possible type for `p` in the call context `false`
|
||||
* that is consistent with the static type of `arg`.
|
||||
*/
|
||||
private predicate validArgParamOut(ArgNode arg, ParamNode p) {
|
||||
exists(DataFlowType t1, DataFlowType t2 |
|
||||
typeFlowParamType(p, t1, false) and
|
||||
relevantArgParamOut(arg, p, t2) and
|
||||
compatibleTypes(t1, t2)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the edge `call`-to-`c` is valid in the out-going direction.
|
||||
*/
|
||||
predicate typeFlowValidEdgeOut(DataFlowCall call, DataFlowCallable c) {
|
||||
Input::relevantCallEdgeOut(call, c) and
|
||||
forall(ArgNode arg, ParamNode p | callEdge(call, c, arg, p) and trackedParamType(p) |
|
||||
validArgParamOut(arg, p)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the call context `call` either improves virtual dispatch in
|
||||
* `callable` or if it allows us to prune unreachable nodes in `callable`.
|
||||
|
||||
Reference in New Issue
Block a user